cleanup some work in progress; consistency with new outputs for tests

StdLib/Nat.gr

@@ -48,12 +48,3 @@ mult_r [n] (S m') = add n (mult_r [n] m')
 div2 : forall {n : Nat} . N (2 * n) -> N n
 div2 Z = Z;
 div2 (S (S x)) = S (div2 x)
-
---- Existential nat
-data NX where
-  NX : ∀ {n : Nat} . N n → NX
-
-
-natToNX : Int → NX
-natToNX 0 = NX Z;
-natToNX n = let (NX m) = natToNX (n - 1) in NX (S m)

frontend/tests/cases/negative/CrossDefPolymorphism.gr.output

@@ -0,0 +1,3 @@
+Type checking failed: 
+  Unification failed: 6:7:
+  Cannot unify universally quantified type variable `s`` of kind `Type` with a concrete type `s [2]`

frontend/tests/cases/negative/approximation2.gr.output

@@ -1,4 +1,4 @@
 Type checking failed: 
   Falsifiable theorem: 5:1:
   The following theorem associated with `borg` is falsifiable:
-	(prom_[x]0 + prom_[x] ≤ 5..6) ∧ (3..4 ≤ prom_[x]) ∧ (0..1 ≤ prom_[x]0)
+	( -> (prom_[x]1 * 1 : Interval Nat + prom_[x]0 * 1 : Interval Nat ≤ 5..6) ∧ (3..4 ≤ prom_[x]0) ∧ (0..1 ≤ prom_[x]1))

frontend/tests/cases/negative/badExistential.gr.output

@@ -1,3 +1,3 @@
 Type checking failed: 
   Type error: 4:23:
-  Expected `f t -> a` but got `f a -> a`
+  Expected `f t -> a` but got `f a0.0 -> a`

frontend/tests/cases/negative/badExistential2.gr.output

@@ -1,3 +1,3 @@
 Type checking failed: 
   Operator resolution failed: 6:14:
-  Could not resolve operator `+` at type `a -> Int -> ..`
+  Could not resolve operator `+` at type `a0.0 -> Int -> ..`

frontend/tests/cases/negative/badIndexingMatch.gr.output

@@ -0,0 +1,3 @@
+Type checking failed: 
+  Unification failed: 7:11:
+  Cannot unify universally quantified type variable `a`` of kind `Type` with a concrete type `Maybe t1.0`

frontend/tests/cases/negative/badPoly.gr.output

@@ -1,3 +1,3 @@
 Type checking failed: 
   Type error: 2:14:
-  Expected `a -> a -> (a, b)` but got `a -> b -> (a, b)`
+  Expected `a -> a -> (a, b)` but got `a0 -> b0 -> (a0, b0)`

frontend/tests/cases/negative/badRecursiveArgument.gr.output

@@ -0,0 +1,4 @@
+Type checking failed: 
+  Counter example: 7:1:
+  The following theorem associated with `fibble` is falsifiable:
+	∀ [(n0.0, ↑Nat),(t1.0, ↑Nat)] . ((t1.0 = n0.0 + 1) ∧ (n = t1.0) -> (n1 = n1 + 1) ∧ (n0.0 = n1))

frontend/tests/cases/negative/bool.gr.output

@@ -1,3 +1,3 @@
 Type checking failed: 
-  Wrong return type in data constructor: 2:3:
+  Wrong return type in value constructor: 2:3:
   Expected type constructor `Bool`, but got `Int`

frontend/tests/cases/negative/cartesianCase.gr.output

@@ -1,4 +1,3 @@
 Type checking failed: 
-  Falsifiable theorem: 5:1:
-  The following theorem associated with `foo` is falsifiable:
-	(1 ≤ ∞) ∧ (1 ≤ ∞)
+  Pattern match impossible: 8:6:
+  Pattern match in an equation of `case` is impossible as it implies the unsatisfiable condition (1 ≤ ∞)

frontend/tests/cases/negative/case.gr.output

@@ -1,4 +1,2 @@
-Type checking failed: 
-  Counter example: 5:1:
-  The following theorem associated with `foo` is falsifiable:
-	(0 ≤ n) ∧ ∀ n.80,t.53 . ((0 ≤ 0) ∧ (n = n80 + 1) ∧ ∃ t52 : Type . ¬((n = 0)) -> (0 ≤ n) ∧ (n81 + 1 ≤ n) ∧ (0 ≤ 0) ∧ (n80 = n81)) ∧ ∀ t.52 . ((n = 0) -> (0 ≤ n))
+Parse error: 
+  lexical error at line 4, column 61

frontend/tests/cases/negative/disallowZeroBoundFromUnifyingPatterns.gr.output

@@ -1,3 +1,3 @@
 Type checking failed: 
-  Grading error: 9:6:
-  1 is not approximatable by 0 for type Nat because Nat denotes precise usage.
+  Pattern match impossible: 9:5:
+  Pattern match in an equation of `case` is impossible as it implies the unsatisfiable condition (1 ≤ 0)

frontend/tests/cases/negative/everyOtherBroken.gr.output

@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 8:1:
   The following theorem associated with `everyOther` is falsifiable:
-	∀ n,a.1,n.0,a.2 . ((0..0 ≤ 0..1) ∧ (n + 1 = n0 + 1 + 1) ∧ ∃ a : Type . ¬((n + 1 = 0)) -> (1..1 ≤ 0..1) ∧ (1 + n2 ≤ n + 1) ∧ (n1 + 1 = n1 + 1 + 1) ∧ (n2 = n1) ∧ (0..1 ≤ 0..1) ∧ (n1 = n2))
+	∀ [(n0.0, ↑Nat),(a1.0, Type),(t2.0, Type),(t3.0, ↑Nat),(n0.1, ↑Nat),(a1.1, Type),(t2.1, Type),(t3.1, ↑Nat)] . ((0 : Interval Nat ≤ 0..1) ∧ (t3.1 = n0.1 + 1) ∧ (t3.1 = n0.0) ∧ (t3.0 = n0.0 + 1) ∧ (n = t3.0) -> (1 : Interval Nat ≤ 0..1) ∧ (1 + n1 * 1 ≤ n) ∧ (n0.2 + 1 = n0.0 + 1) ∧ (n1 = n0.2) ∧ (0..1 ≤ 0..1) ∧ (n0.1 = n1))

frontend/tests/cases/negative/everyOtherBroken2.gr.output

@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 9:1:
   The following theorem associated with `everyOther` is falsifiable:
-	∀ a.1,n,a.2,n.0 . ((0..0 ≤ 0..1) ∧ (n + 1 = n0 + 1 + 1) ∧ ∃ a : Type . ¬((n + 1 = 0)) -> (1..1 ≤ 0..1) ∧ (1 + n2 ≤ n + 1) ∧ (n1 + 1 = n1 + 1 + 1) ∧ (n2 = n1) ∧ (0..1 ≤ 0..1) ∧ (n1 = n2))
+	∀ [(a1.0, Type),(n0.0, ↑Nat),(t2.0, Type),(t3.0, ↑Nat),(a1.1, Type),(n0.1, ↑Nat),(t2.1, Type),(t3.1, ↑Nat)] . ((0 : Interval Nat ≤ 0..1) ∧ (t3.1 = n0.1 + 1) ∧ (t3.1 = n0.0) ∧ (t3.0 = n0.0 + 1) ∧ (n = t3.0) -> (1 : Interval Nat ≤ 0..1) ∧ (1 + n1 * 1 ≤ n) ∧ (n0.2 + 1 = n0.0 + 1) ∧ (n1 = n0.2) ∧ (0..1 ≤ 0..1) ∧ (n0.1 = n1))

frontend/tests/cases/negative/fact-inf.gr.output

@@ -1,4 +1,3 @@
 Type checking failed: 
-  Counter example: 4:1:
-  The following theorem associated with `fact` is falsifiable:
-	(1..1 ≤ ∞..∞)
+  Pattern match impossible: 5:1:
+  Pattern match in an equation of `fact` is impossible as it implies the unsatisfiable condition (t1.13 = n0.13 + 1) ∧ (n = t1.13) ∧ (1 : Interval (Ext Nat) ≤ ∞..∞)

frontend/tests/cases/negative/flat.gr.output

@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 2:1:
   The following theorem associated with `flatten` is falsifiable:
-	(1 ≤ d + 1) ∧ ((c + 1) * (d + 1) = c + 1)
+	( -> (1 ≤ d + 1) ∧ ( -> (((c + 1) * (d + 1)) * 1 = c + 1)))

frontend/tests/cases/negative/flatten/flattenByLet.gr.output

@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 2:1:
   The following theorem associated with `flatten` is falsifiable:
-	(m * n = m * n)
+	( -> ( -> (1 = n) ∧ ( -> ((m * n) * 1 = m))))

frontend/tests/cases/negative/flatten/flattenLevel.gr.output

@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 2:1:
   The following theorem associated with `flattenLevel` is falsifiable:
-	(k /\ l ≤ l \/ k)
+	( -> ((k /\ l) * 1 : Level ≤ l \/ k))

frontend/tests/cases/negative/flatten/flattenNat.gr.output

@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 2:1:
   The following theorem associated with `flattenNat` is falsifiable:
-	(m + n ≤ n * m)
+	( -> ((m + n) * 1 ≤ n * m))

frontend/tests/cases/negative/headAlt.gr.output

@@ -1,3 +1,3 @@
 Type checking failed: 
-  Pattern unreachable: 6:1:
-  Pattern guard for equation of `headAlt` is impossible. Its condition is Falsifiable
+  Pattern match impossible: 6:1:
+  Pattern match in an equation of `headAlt` is impossible as it implies the unsatisfiable condition (t1.0 = 0) ∧ (n = t1.0) ∧ (1 : Interval Nat ≤ 0..1) ∧ (n > 0)

frontend/tests/cases/negative/headAlt2.gr.output

@@ -1,4 +1,4 @@
 Type checking failed: 
   Falsifiable theorem: 10:1:
   The following theorem associated with `foo` is falsifiable:
-	(0..1 ≤ 0..1) ∧ (0 > 0)
+	( -> (n1 = 0) ∧ (0..1 ≤ 0..1) ∧ (n1 > 0))

frontend/tests/cases/negative/headAlt3.gr.output

@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 9:1:
   The following theorem associated with `headAlt'` is falsifiable:
-	((n > 0) -> (n = n0) ∧ (0..1 ≤ 0..1) ∧ (n > 1))
+	((n > 0) -> (n = n1) ∧ (0..1 ≤ 0..1) ∧ (n1 > 1))

frontend/tests/cases/negative/impossiblePat.gr.output

@@ -1,3 +1,4 @@
 Type checking failed: 
-  Pattern unreachable: 6:1:
-  Pattern guard for equation of `last` is impossible. Its condition is Falsifiable
+  Counter example: 8:1:
+  The following theorem associated with `last` is falsifiable:
+	∀ [(n0.1, ↑Nat),(t3.1, Type),(t4.1, Type),(t5.1, ↑Nat)] . ((0 : Interval Nat ≤ 0..1) ∧ (t5.1 = n0.1 + 1) ∧ (t5.1 = n + 1) -> (0..1 ≤ 0..1) ∧ (n0.1 = n1 + 1))

frontend/tests/cases/negative/noConsumption.gr.output

@@ -1,5 +1,4 @@
 Type checking failed: 
-  Pattern unreachable: 4:1:
-  Pattern guard for equation of `and` is impossible.
-	0 is not approximatable by 1 for type Nat because Nat denotes precise usage.
-	0 is not approximatable by 1 for type Nat because Nat denotes precise usage.
+  Pattern match impossible: 4:1:
+  Pattern match in an equation of `and` is impossible as it implies the unsatisfiable condition (0 ≤ 1)
+(0 ≤ 1)

frontend/tests/cases/negative/polarity.gr.output

@@ -1,7 +1,7 @@
 Type checking failed: 
   Unification failed: 3:40:
-  Trying to match a polymorphic type  `a` with monomorphic type `a [0]`
+  Cannot unify universally quantified type variable `a`` of kind `Type` with a concrete type `a [0]`
 
 Falsifiable theorem: 7:1:
   The following theorem associated with `secondOrderAlt` is falsifiable:
-	(prom_[x] ≤ 0) ∧ (prom_[x] ≤ 1)
+	( -> (prom_[x]0 * 1 ≤ 0) ∧ (prom_[x]0 ≤ 1))

frontend/tests/cases/negative/poly.gr.output

@@ -1,3 +1,3 @@
 Type checking failed: 
   Unification failed: 2:9:
-  Type `Int` is not unifiable with `a`
+  Cannot unify universally quantified type variable `a`` of kind `Type` with a concrete type `Int`

frontend/tests/cases/negative/predicateFalseInDef.gr.output

@@ -1,3 +1,3 @@
 Type checking failed: 
-  Pattern unreachable: 6:1:
-  Pattern guard for equation of `headAlt` is impossible. Its condition is Falsifiable
+  Pattern match impossible: 6:1:
+  Pattern match in an equation of `headAlt` is impossible as it implies the unsatisfiable condition (t1.0 = 0) ∧ (n = t1.0) ∧ (1 : Interval Nat ≤ 0..1) ∧ (n > 0)

frontend/tests/cases/negative/predicateFalseInUse.gr.output

@@ -1,4 +1,4 @@
 Type checking failed: 
   Falsifiable theorem: 9:1:
   The following theorem associated with `foo` is falsifiable:
-	(0..1 ≤ 0..1) ∧ (0 > 0)
+	( -> (n1 = 0) ∧ (0..1 ≤ 0..1) ∧ (n1 > 0))

frontend/tests/cases/negative/universal.gr.output

@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 2:1:
   The following theorem associated with `foo` is falsifiable:
-	(2 ≤ n)
+	( -> (1 + 1 ≤ n))

StdLib/Choice.gr → work-in-progress/Choice.gr

@@ -40,5 +40,11 @@
 data Choice : Type -> Type -> Nat -> Type where
   MkChoice : forall {a : Type, b : Type,  m : Nat,  n : Nat}. a [0..m] -> b [0..n] -> Choice a b (m + n)
 
-chooseA : forall {a : Type, b : Type,  m : Nat,  n : Nat}. Choice a b (n + 1) -> (a, Choice a b n)
+chooseA : forall {a : Type, b : Type, n : Nat}. Choice a b (n + 1) -> (a, Choice a b n)
 chooseA (MkChoice [a] [b]) = (a, MkChoice [a] [b])
+
+chooseLeft : forall {a : Type, b : Type,  m : Nat,  n : Nat}. Choice a b 1 -> a
+chooseLeft (MkChoice [a] [_]) = a
+
+chooseRight : forall {a : Type, b : Type,  m : Nat,  n : Nat}. Choice a b 1 -> b
+chooseRight (MkChoice [_] [b]) = b

work-in-progress/existentialNat.gr

@@ -0,0 +1,11 @@
+import Nat
+
+-- Recent changes means this doesn't work
+
+--- Existential nat
+data NX where
+  NX : ∀ {n : Nat} . N n → NX
+
+natToNX : Int → NX
+natToNX 0 = NX Z;
+natToNX n = let (NX m) = natToNX (n - 1) in NX (S m)