Choice.gr

-- ------
-- --- 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, 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