From 537ebccc670e6466493aed80cb7734bb5096ba5a Mon Sep 17 00:00:00 2001 From: Sal Wolffs Date: Mon, 26 Feb 2018 01:03:48 +0100 Subject: [PATCH 1/2] Made fromIntegerNat use `case` instead of `if` Using `if` with an `assert_smaller` could cause infinite compile-time looping. To prevent this, a pattern match on 0 was needed, but pattern-matching on Integers stops terms from reducing in proofs. This should fix that by avoiding the original issue. --- libs/prelude/Prelude/Nat.idr | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/libs/prelude/Prelude/Nat.idr b/libs/prelude/Prelude/Nat.idr index 029176b1d5..c4d350a633 100644 --- a/libs/prelude/Prelude/Nat.idr +++ b/libs/prelude/Prelude/Nat.idr @@ -72,12 +72,10 @@ mult (S left) right = plus right $ mult left right ||| Convert an Integer to a Nat, mapping negative numbers to 0 fromIntegerNat : Integer -> Nat -fromIntegerNat 0 = Z -fromIntegerNat n = - if (n > 0) then - S (fromIntegerNat (assert_smaller n (n - 1))) - else - Z +fromIntegerNat i = + case (i > 0) of + True => S (fromIntegerNat (assert_smaller i (i - 1))) + False => Z ||| Convert a Nat to an Integer toIntegerNat : Nat -> Integer From 2ee99aa9380699b2d13e7f554d3826364cceb686 Mon Sep 17 00:00:00 2001 From: Sal Wolffs Date: Mon, 26 Feb 2018 03:36:07 +0100 Subject: [PATCH 2/2] Documented s/if/case/ in fromIntegerNat --- libs/prelude/Prelude/Nat.idr | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/libs/prelude/Prelude/Nat.idr b/libs/prelude/Prelude/Nat.idr index c4d350a633..ec29631deb 100644 --- a/libs/prelude/Prelude/Nat.idr +++ b/libs/prelude/Prelude/Nat.idr @@ -72,10 +72,13 @@ mult (S left) right = plus right $ mult left right ||| Convert an Integer to a Nat, mapping negative numbers to 0 fromIntegerNat : Integer -> Nat -fromIntegerNat i = - case (i > 0) of +fromIntegerNat i = + case (i > 0) of True => S (fromIntegerNat (assert_smaller i (i - 1))) False => Z +-- Using if here would cause infinite looping in some cases. +-- This could be fixed by redundantly matching on 0 explicitly, but that would stop +-- fromIntegerNat from reducing in proofs. ||| Convert a Nat to an Integer toIntegerNat : Nat -> Integer