Add sum types.

1 files changed, 70 insertions, 0 deletions

diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
new file mode 100644
index 0000000..20198c5
--- /dev/null
+++ b/src/Obs/Typing/Conversion.idr
@@ -0,0 +1,70 @@
+module Obs.Typing.Conversion
+
+import Data.Fin
+
+import Obs.Logging
+import Obs.NormalForm
+import Obs.NormalForm.Normalise
+import Obs.Sort
+import Obs.Substitution
+
+-- Conversion ------------------------------------------------------------------
+
+-- invariant: all definitions fully expanded
+-- invariant: m |- t, u <- a : s
+partial export
+convert : (t, u, a : NormalForm n) -> Sort -> Logging ann Bool
+partial
+convertSet : (t, u : NormalForm n) -> Logging ann Bool
+partial
+convertSum : (t, u : NormalForm n) -> (s, s' : Sort) -> (a, b : NormalForm n) -> Logging ann Bool
+
+-- In sort Prop
+convert Irrel Irrel a Prop = pure True
+-- In unknown type in set
+convert t u (Ntrl _) (Set k) = pure $ t == u
+-- In type Set
+convert t u (Cnstr (Sort _)) (Set _) = convertSet t u
+-- In type Pi
+convert t u (Cnstr (Pi s s' var a b)) (Set k) = do
+  t <- doApp (weaken 1 t) (Ntrl $ Var var FZ)
+  u <- doApp (weaken 1 u) (Ntrl $ Var var FZ)
+  convert t u b s'
+-- In type Sigma
+convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do
+  t1 <- doFst t
+  u1 <- doFst t
+  True <- convert t1 u1 a s
+    | False => pure False
+  b <- subst1 t1 b
+  t2 <- doSnd t
+  u2 <- doSnd t
+  convert t2 u2 b s'
+-- In type Sum (manually expanding definition of doCase)
+convert t u (Cnstr (Sum s s' a b)) (Set _) = convertSum t u s s' a b
+-- Default
+convert t u a s =
+  inScope "invalid conversion" $ fatal $
+  fillSep {ann} [prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]
+
+convertSet (Cnstr (Sort s')) (Cnstr (Sort s'')) = pure $ s' == s''
+convertSet (Cnstr (Pi s s' _ a b)) (Cnstr (Pi l l' _ a' b')) =
+  pure $
+  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
+convertSet (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) =
+  pure $
+  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
+convertSet (Cnstr (Sum s s' a b)) (Cnstr (Sum l l' a' b')) =
+  pure $
+  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
+convertSet (Cnstr Top) (Cnstr Top) = pure True
+convertSet (Cnstr Bottom) (Cnstr Bottom) = pure True
+convertSet (Ntrl t) u = pure (Ntrl t == u)
+convertSet t (Ntrl u) = pure (t == Ntrl u)
+convertSet t u = pure $ False
+
+convertSum (Cnstr (Left t)) (Cnstr (Left u)) s s' a b = convert t u a s
+convertSum (Cnstr (Right t)) (Cnstr (Right u)) s s' a b = convert t u b s'
+convertSum (Ntrl t) u s s' a b = pure (Ntrl t == u)
+convertSum t (Ntrl u) s s' a b = pure (t == Ntrl u)
+convertSum t u s s' a b = pure False