Add sum types.

1 files changed, 58 insertions, 272 deletions

diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 3ec91f7..b327397 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -4,9 +4,11 @@ import Data.Vect
 
 import Obs.Logging
 import Obs.NormalForm
+import Obs.NormalForm.Normalise
 import Obs.Sort
 import Obs.Substitution
 import Obs.Term
+import Obs.Typing.Conversion
 
 import System
 
@@ -34,271 +36,6 @@ typeMismatch bounds lhs rhs = inScope "type mismatch" $ mismatch bounds lhs rhs
 sortMismatch : Bounds -> Doc ann -> Doc ann -> Logging ann a
 sortMismatch bounds lhs rhs = inScope "sort mismatch" $ mismatch bounds lhs rhs
 
--- Substitution ----------------------------------------------------------------
-
-mergeName : String -> String -> String
-mergeName "" s' = s'
-mergeName "_" s' = s'
-mergeName s s' = s
-
-wkn : Vect k String -> (Fin n -> Logging ann (NormalForm m)) -> Fin (k + n) -> Logging ann (NormalForm (k + m))
-wkn []            f = f
-wkn (var :: vars) f =
-  add
-    (Logging ann . NormalForm)
-    (pure $ Ntrl $ Var var FZ)
-    (\i => pure $ rename !(wkn vars f i) FS)
-
-covering partial
-substCnstr : Constructor n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (Constructor m)
-covering partial
-substNtrl  : Neutral n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
-covering partial
-subst      : NormalForm n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
-covering partial
-subst1     : NormalForm n -> NormalForm (S n) -> Logging ann (NormalForm n)
-covering partial
-doApp      : NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doFst      : NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doSnd      : NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doEqual    : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doEqualL   : Nat -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doEqualR   : Nat -> Constructor n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doEqualU   : Nat -> Constructor n -> Constructor n -> Logging ann (NormalForm n)
-covering partial
-doCastL    : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doCastR    : Constructor n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doCastU    : Constructor n -> Constructor n -> NormalForm n -> Logging ann (NormalForm n)
-
-substCnstr (Sort s) f = pure $ Sort s
-substCnstr (Pi s s' var a b) f = do
-  a <- subst a f
-  b <- subst b (wkn [var] f)
-  pure (Pi s s' var a b)
-substCnstr (Lambda var t) f = do
-  t <- subst t (wkn [var] f)
-  pure (Lambda var t)
-substCnstr (Sigma s s' var a b) f = do
-  a <- subst a f
-  b <- subst b (wkn [var] f)
-  pure (Sigma s s' var a b)
-substCnstr (Pair t u) f = do
-  t <- subst t f
-  u <- subst u f
-  pure (Pair t u)
-substCnstr Top f = pure $ Top
-substCnstr Bottom  f = pure $ Bottom
-
-substNtrl (Var var i) f = do
-  Ntrl (Var var' j) <- f i
-    | t => pure t
-  pure (Ntrl (Var (mergeName var' var) j))
-substNtrl (App t u) f = do
-  t <- substNtrl t f
-  u <- subst u f
-  doApp t u
-substNtrl (Fst t) f = do
-  t <- substNtrl t f
-  doFst t
-substNtrl (Snd t) f = do
-  t <- substNtrl t f
-  doSnd t
-substNtrl Absurd f = pure $ Ntrl Absurd
-substNtrl (Equal a t u) f = do
-  a <- substNtrl a f
-  t <- subst t f
-  u <- subst u f
-  doEqual a t u
-substNtrl (EqualL i t u) f = do
-  t <- substNtrl t f
-  u <- subst u f
-  doEqualL i t u
-substNtrl (EqualR i t u) f = do
-  t <- substCnstr t f
-  u <- substNtrl u f
-  doEqualR i t u
-substNtrl (EqualU i t u) f = do
-  t <- substCnstr t f
-  u <- substCnstr u f
-  doEqualU i t u
-substNtrl (CastL a b t) f = do
-  a <- substNtrl a f
-  b <- subst b f
-  t <- subst t f
-  doCastL a b t
-substNtrl (CastR a b t) f = do
-  a <- substCnstr a f
-  b <- substNtrl b f
-  t <- subst t f
-  doCastR a b t
-substNtrl (CastU a b t) f = do
-  a <- substCnstr a f
-  b <- substCnstr b f
-  t <- subst t f
-  doCastU a b t
-
-subst (Ntrl t)  f = substNtrl t f
-subst (Cnstr t) f = map Cnstr $ substCnstr t f
-subst Irrel     f = pure Irrel
-
-subst1 t u = subst u (add (Logging ann . NormalForm) (pure t) (pure . point))
-
-doApp (Ntrl t) u = pure $ Ntrl (App t u)
-doApp Irrel u = pure $ Irrel
-doApp (Cnstr (Lambda var t)) u = subst t (add (Logging ann . NormalForm) (pure u) (pure . point))
-doApp (Cnstr t) u = inScope "bug" $ inScope "wrong constructor in apply" $ fatal t
-
-doFst (Ntrl t) = pure $ Ntrl (Fst t)
-doFst Irrel = pure $ Irrel
-doFst (Cnstr (Pair t u)) = pure $ t
-doFst (Cnstr t) = inScope "bug" $ inScope "wrong constructor in fst" $ fatal t
-
-doSnd (Ntrl t) = pure $ Ntrl (Snd t)
-doSnd Irrel = pure $ Irrel
-doSnd (Cnstr (Pair t u)) = pure $ u
-doSnd (Cnstr t) = inScope "bug" $ inScope "wrong constructor in snd" $ fatal t
-
-doEqual (Ntrl a) t u = pure $ Ntrl (Equal a t u)
-doEqual Irrel t u = inScope "bug" $ inScope "wrong type over equal" $ fatal "Irrel"
-doEqual (Cnstr (Sort Prop)) t u =
-  pure $
-  Cnstr (Sigma Prop Prop "_"
-    (Cnstr $ Pi Prop Prop "_" t (weaken 1 u))
-    (weaken 1 $ Cnstr $ Pi Prop Prop "_" u (weaken 1 t)))
-doEqual (Cnstr (Sort (Set k))) t u = doEqualL k t u
-doEqual (Cnstr (Pi s s' var a b)) t u = do
-  eqLhs <- doApp (weaken 1 t) (Ntrl $ Var var FZ)
-  eqRhs <- doApp (weaken 1 u) (Ntrl $ Var var FZ)
-  eq <- doEqual b eqLhs eqRhs -- b in Set because Pi in Set.
-  pure $ Cnstr (Pi s Prop var a eq)
-doEqual (Cnstr (Sigma s s' var a b)) t u = do
-  t1 <- doFst t
-  u1 <- doFst u
-  eq1 <- case s of
-    Prop => pure $ Cnstr Top
-    (Set i) => doEqual a t1 u1
-  eq2 <- case s' of
-    Prop => pure $ Cnstr Top
-    (Set i) => do
-      bt <- subst1 t1 b
-      bu <- subst1 u1 b
-      t2 <- doSnd t
-      t2 <- doCastL bt bu t2
-      u2 <- doSnd u
-      doEqual bu t2 u2
-  pure $ Cnstr (Sigma Prop Prop "_" eq1 (weaken 1 eq2))
-doEqual (Cnstr Top) t u = pure $ Cnstr Top
-doEqual (Cnstr Bottom) t u = pure $ Cnstr Top
-
-doEqualL i (Ntrl t) u = pure $ Ntrl (EqualL i t u)
-doEqualL i Irrel u = inScope "bug" $ inScope "wrong type under equalL" $ fatal "Irrel"
-doEqualL i (Cnstr t) u = doEqualR i t u
-
-doEqualR i t (Ntrl u) = pure $ Ntrl (EqualR i t u)
-doEqualR i t Irrel = inScope "bug" $ inScope "wrong type under equalR" $ fatal "Irrel"
-doEqualR i t (Cnstr u) = doEqualU i t u
-
-doEqualU i (Sort s) (Sort s') = pure $ Cnstr Top -- have suc s = i = suc s', and suc injective
-doEqualU i (Pi s s' _ a b) (Pi l l' var a' b') = case (s == s' && l == l') of
-  False => pure $ Cnstr Bottom
-  True => do
-    eqLhs <- doEqual (cast s) a' a
-    let x = Ntrl $ Var var FZ
-    b <- subst b (add (Logging ann . NormalForm) (doCastL (weaken 1 a') (weaken 1 a) x) (pure . Ntrl . Var "" . FS))
-    eqRhs <- doEqual (cast s') b b'
-    pure $ Cnstr (Sigma Prop Prop "" eqLhs $ weaken 1 $ Cnstr (Pi s Prop var a' eqRhs))
-doEqualU i (Sigma s s' _ a b) (Sigma l l' var a' b') = case (s == s' && l == l') of
-  False => pure $ Cnstr Bottom
-  True => do
-    eqLhs <- doEqual (cast s) a' a
-    let x = Ntrl $ Var var FZ
-    b <- subst b (add (Logging ann . NormalForm) (doCastL (weaken 1 a') (weaken 1 a) x) (pure . Ntrl . Var "" . FS))
-    eqRhs <- doEqual (cast s') b b'
-    pure $ Cnstr (Sigma Prop Prop "" eqLhs $ weaken 1 $ Cnstr (Pi s Prop var a' eqRhs))
-doEqualU i t u = pure $ Ntrl (EqualU i t u) -- assumption: only logical values reach this far
-
-doCastL (Ntrl a) b t = pure $ Ntrl (CastL a b t)
-doCastL Irrel b t = inScope "bug" $ inScope "wrong type for cast" $ fatal "Irrel"
-doCastL (Cnstr a) b t = doCastR a b t
-
-doCastR a (Ntrl b) t = pure $ Ntrl (CastR a b t)
-doCastR a Irrel t = inScope "bug" $ inScope "wrong type for cast" $ fatal "Irrel"
-doCastR a (Cnstr b) t = doCastU a b t
-
-doCastU (Sort s) (Sort s') t = pure t
-doCastU (Pi s s' _ a b) (Pi l l' var a' b') t = do
-  let x' = Ntrl $ Var var FZ
-  let x = doCastL (weaken 1 a') (weaken 1 a) x'
-  b <- subst b (add (Logging ann . NormalForm) x (pure . Ntrl . Var "" . FS))
-  b' <- subst b' (add (Logging ann . NormalForm) (pure x') (pure . Ntrl . Var "" . FS))
-  fx <- doApp (weaken 1 t) !x
-  cast <- doCastL b b' fx
-  pure $ Cnstr (Lambda var cast)
-doCastU (Sigma s s' _ a b) (Sigma l l' var a' b') t = do
-  t1 <- doFst t
-  t2 <- doSnd t
-  t1' <- doCastL a a' t1
-  b <- subst1 t1 b
-  b' <- subst1 t1' b'
-  t2' <- doCastL b b' t2
-  pure $ Cnstr (Pair t1' t2')
-
-doCastU Top Top t = pure Irrel
-doCastU Bottom Bottom t = pure Irrel
-doCastU a b t = pure $ Ntrl (CastU a b t)
-
--- Conversion ------------------------------------------------------------------
-
--- invariant: all definitions fully expanded
--- invariant: m |- t, u <- a : s
-covering partial
-convert : (t, u, a : NormalForm n) -> Sort -> 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 (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort _)) (Set _) = pure $ s' == s''
-convert (Cnstr (Pi s s' _ a b)) (Cnstr (Pi l l' _ a' b')) (Cnstr (Sort _)) (Set _) =
-  pure $
-  s == l && s' == l' && !(convert a a' (cast s) (suc s)) && !(convert b b' (cast s') (suc s'))
-convert (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) (Cnstr (Sort _)) (Set _) =
-  pure $
-  s == l && s' == l' && !(convert a a' (cast s) (suc s)) && !(convert b b' (cast s') (suc s'))
-convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort _)) (Set _) = pure True
-convert (Cnstr Bottom) (Cnstr Bottom) (Cnstr (Sort _)) (Set _) = pure True
-convert (Ntrl t) u (Cnstr (Sort s)) (Set k) = pure $ Ntrl t == u
-convert t (Ntrl u) (Cnstr (Sort s)) (Set k) = pure $ t == Ntrl u
-convert t u (Cnstr (Sort s)) (Set k) = pure $ False
--- 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'
--- Default
-convert t u a s =
-  inScope "invalid conversion" $ fatal $
-  fillSep {ann} [prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]
-
-
 -- Typing Contexts -------------------------------------------------------------
 
 infix 5 ::<
@@ -324,7 +61,7 @@ index (ctx ::< (var, ty, s))    FZ     = (Ntrl $ Var var FZ, weaken 1 ty, s)
 index (ctx :< _)                (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
 index (ctx ::< _)               (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
 
-covering partial
+partial
 asSubst : (ctx : TyContext m n) -> Fin n -> Logging ann (NormalForm m)
 asSubst (ctx :< def)             FZ     = subst def.tm (asSubst ctx)
 asSubst (ctx ::< (var, _, Prop)) FZ     = pure Irrel
@@ -334,11 +71,11 @@ asSubst (ctx ::< _)              (FS i) = map (weaken 1) (asSubst ctx i)
 
 -- Checking and Inference ------------------------------------------------------
 
-covering partial
+partial
 check : TyContext m n -> WithBounds (Term n) -> NormalForm n -> Sort -> Logging ann (NormalForm n)
-covering partial
+partial
 infer : TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, NormalForm n, Sort)
-covering partial
+partial
 inferType : {default typeMismatch tag : forall a . Bounds -> Doc ann -> Doc ann -> Logging ann a}
   -> TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, Sort)
 
@@ -364,6 +101,20 @@ check ctx tm ty s = case (tm.val, ty) of
       (Prop, Prop) => pure Irrel
       _ => pure (Cnstr $ Pair t u)
   (Pair _ _, ty) => typeMismatch tm.bounds (pretty "sigma") (pretty ty)
+  (Left t, Cnstr (Sum s s' a b)) => do
+    inScope "check" $ trace $ map (\_ => "checking left injection") tm
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking subterm for type" <++> pretty a) tm
+    t <- check ctx t a s
+    inScope "check" $ trace $ map (\_ => " subterm is well typed") tm
+    pure (Cnstr $ Left t)
+  (Left _, ty) => typeMismatch tm.bounds (pretty "sum") (pretty ty)
+  (Right t, Cnstr (Sum s s' a b)) => do
+    inScope "check" $ trace $ map (\_ => "checking right injection") tm
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking subterm for type" <++> pretty b) tm
+    t <- check ctx t b s'
+    inScope "check" $ trace $ map (\_ => " subterm is well typed") tm
+    pure (Cnstr $ Right t)
+  (Right _, ty) => typeMismatch tm.bounds (pretty "sum") (pretty ty)
   (_, _) => do
     inScope "check" $ trace $ map (\_ => "checking has fallen through") tm
     (v, a, s') <- infer ctx tm
@@ -421,13 +172,48 @@ infer ctx tm = case tm.val of
   (Snd t) => do
     inScope "infer" $ trace $ map (\_ => "encountered first projection") tm
     (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
-      | (_, ty, _) => inScope "wrong type to fst" $ fatal (map (\_ => ty) tm)
+      | (_, ty, _) => inScope "wrong type to snd" $ fatal (map (\_ => ty) tm)
     inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) tm
     t1 <- doFst t
     res <- doSnd t
     b <- subst1 t1 b
     inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty b) tm
     pure (res, b, s')
+  (Sum a b) => do
+    inScope "infer" $ trace $ map (\_ => "encountered sum type") tm
+    (a, s) <- inferType ctx a
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "left has type" <++> pretty a) tm
+    (b, s') <- inferType ctx b
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "right has type" <++> pretty b) tm
+    pure (Cnstr (Sum s s' a b), cast (ensureSet (lub s s')), suc (ensureSet (lub s s')))
+  (Left _) => inScope "cannot infer type" $ fatal tm
+  (Right _) => inScope "cannot infer type" $ fatal tm
+  (Case t l out f g) => do
+    inScope "infer" $ trace $ map (\_ => "encountered case") tm
+    (t, ty@(Cnstr (Sum s s' a b)), s'') <- infer ctx t
+      | (_, ty, _) => inScope "wrong type to case" $ fatal (map (\_ => ty) tm)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "sum has type" <++> pretty ty) tm
+    (Cnstr (Sort l), _) <- inferType ctx l
+      | (s, _) => typeMismatch l.bounds (pretty "sort") (pretty s)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "output has sort" <++> pretty l) tm
+    let ty' = Cnstr (Pi s'' (suc l) "x" ty (cast l))
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking output has type" <++> pretty ty') tm
+    out <- check ctx out ty' (s'' ~> suc l)
+    inScope "infer" $ trace $ map (\_ => "output is well typed") tm
+    outL <- doApp (weaken 1 out) (Cnstr (Left (Ntrl (Var "x" 0))))
+    let fTy = Cnstr (Pi s l "x" a outL)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking left branch has type" <++> pretty fTy) tm
+    f <- check ctx f fTy (s ~> l)
+    inScope "infer" $ trace $ map (\_ => "left branch is well typed") tm
+    outR <- doApp (weaken 1 out) (Cnstr (Right (Ntrl (Var "x" 0))))
+    let gTy = Cnstr (Pi s' l "x" b outR)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking right branch has type" <++> pretty gTy) tm
+    g <- check ctx g gTy (s' ~> l)
+    inScope "infer" $ trace $ map (\_ => "right branch is well typed") tm
+    res <- doCase t f g
+    out <- doApp out t
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty out) tm
+    pure (res, out, l)
   Top => pure $ (Cnstr Top, cast Prop, Set 0)
   Point => pure $ (Irrel, Cnstr Top, Prop)
   Bottom  => pure $ (Cnstr Bottom, cast Prop, Set 0)
@@ -508,7 +294,7 @@ inferType ctx a = do
 
 -- Checking Definitions and Blocks ---------------------------------------------
 
-covering partial
+partial
 checkDef : Context n -> Term.Definition n -> Logging ann (NormalForm.Definition n)
 checkDef ctx def = do
   (ty, sort) <-
@@ -519,7 +305,7 @@ checkDef ctx def = do
   inScope "check" $ debug $ map (\name => pretty {ann} "\{name} is well typed with value" <++> pretty tm) def.name
   pure $ MkDefinition {name = def.name, ty, tm, sort}
 
-covering partial
+partial
 export
 checkBlock : Block n -> Logging ann (Context n)
 checkBlock [] = pure []