Merge branch 'equality' of https://github.com/dorchard/gmtt into equa…

…lity

StdLib/Choice.gr

@@ -1,45 +1,44 @@
-------
---- Module: Choice
---- Description: A datatype with two elements. The only way to consume it is by either
----   choosing the first or the second element. You must choose exactly one.
---- Note: still need to encapsulate the `OneOf` constructor—pattern matching on it is BAD!
---- Authors: Vilem-Benjamin Liepelt
---- License: BSD3
---- Copyright: (c) Authors 2018
---- Issue-tracking: https://github.com/dorchard/granule/issues
---- Repository: https://github.com/dorchard/granule
-------
-
-data Choice a b = OneOf (a [0..1]) (b [0..1]) -- TODO: don't export
-
-choice : forall {a : Type, b : Type} . a [0..1] -> b [0..1] -> Choice a b
-choice x y = OneOf x y
-
--- To construct a `Choice a b`, we need an `a [0..1]` and a `b [0..1]` because
--- the consumer can pick either the `a` or the `b`, not both. (That is currently
--- a lie, we need to be able to make the Choice constructor abstract, i.e. not
--- export it, for this to hold.)
---
--- NB: Polymorphism allows further nonlinearity to be encapsulated inside of the
--- `a` and `b`. In other words, `[0..1]` is just the minimum amount of linearity
--- required. Example:
---
--- ```granule
--- choiceExample : forall a : Type, b : Type
---   . a [0..2] -> b [0..1] -> Choice (a [1..2]) b
--- choiceExample aBox bBox = choice (unflatten aBox) bBox
--- ```
-
-choose1 : forall a : Type, b : Type . Choice a b -> a
-choose1 (OneOf [x] [_]) = x
-
-choose2 : forall a : Type, b : Type . Choice a b -> b
-choose2 (OneOf [_] [y]) = y
-
--- TODO: Use the following when existentials are fixed
--- data Choice : Type -> Type -> Nat -> Type where
---   Choices : forall a : Type, b : Type, m : Nat, n : Nat
---           . a [m] -> b [n] -> Choice a b (m + n)
---
--- getA : forall a : Type, b : Type . Choice a b 1 -> a
--- getA (Choices [a] [b]) = a
+-- ------
+-- --- Module: Choice
+-- --- Description: A datatype with two elements. The only way to consume it is by either
+-- ---   choosing the first or the second element. You must choose exactly one.
+-- --- Note: still need to encapsulate the `OneOf` constructor—pattern matching on it is BAD!
+-- --- Authors: Vilem-Benjamin Liepelt
+-- --- License: BSD3
+-- --- Copyright: (c) Authors 2018
+-- --- Issue-tracking: https://github.com/dorchard/granule/issues
+-- --- Repository: https://github.com/dorchard/granule
+-- ------
+
+-- data Choice a b = OneOf (a [0..1]) (b [0..1]) -- TODO: don't export
+
+-- choice : forall {a : Type, b : Type} . a [0..1] -> b [0..1] -> Choice a b
+-- choice x y = OneOf x y
+
+-- -- To construct a `Choice a b`, we need an `a [0..1]` and a `b [0..1]` because
+-- -- the consumer can pick either the `a` or the `b`, not both. (That is currently
+-- -- a lie, we need to be able to make the Choice constructor abstract, i.e. not
+-- -- export it, for this to hold.)
+-- --
+-- -- NB: Polymorphism allows further nonlinearity to be encapsulated inside of the
+-- -- `a` and `b`. In other words, `[0..1]` is just the minimum amount of linearity
+-- -- required. Example:
+-- --
+-- -- ```granule
+-- -- choiceExample : forall a : Type, b : Type
+-- --   . a [0..2] -> b [0..1] -> Choice (a [1..2]) b
+-- -- choiceExample aBox bBox = choice (unflatten aBox) bBox
+-- -- ```
+
+-- choose1 : forall a : Type, b : Type . Choice a b -> a
+-- choose1 (OneOf [x] [_]) = x
+
+-- choose2 : forall a : Type, b : Type . Choice a b -> b
+-- choose2 (OneOf [_] [y]) = y
+
+
+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 (MkChoice [a] [b]) = (a, MkChoice [a] [b])

frontend/src/Language/Granule/Checker/Checker.hs

@@ -1275,7 +1275,7 @@ checkGuardsForImpossibility s name = do
   -- For each guard predicate
   forM_ ps $ \((ctxt, p), s) -> do
 
-    -- p <- simplifyPred p
+    p <- simplifyPred p
 
     -- Existentially quantify those variables occuring in the pattern in scope
     let thm = foldr (uncurry Exists) p ctxt