Add equality types and casts.

1 files changed, 231 insertions, 21 deletions

diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index bf7ebc1..834dbb7 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -36,6 +36,11 @@ 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 =
@@ -51,11 +56,27 @@ substNtrl  : Neutral n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (
 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
@@ -77,9 +98,9 @@ substCnstr Top f = pure $ Top
 substCnstr Bottom  f = pure $ Bottom
 
 substNtrl (Var var i) f = do
-  Ntrl (Var "" j) <- f i
+  Ntrl (Var var' j) <- f i
     | t => pure t
-  pure (Ntrl (Var var j))
+  pure (Ntrl (Var (mergeName var' var) j))
 substNtrl (App t u) f = do
   t <- substNtrl t f
   u <- subst u f
@@ -91,29 +112,148 @@ 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 "wrong constructor in apply:" $ fatal t
+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 "wrong constructor in fst:" $ fatal 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 "wrong constructor in snd:" $ fatal t
+doSnd (Cnstr t) = inScope "bug" $ inScope "wrong constructor in snd" $ fatal t
 
-partial
-subst1 : NormalForm n -> NormalForm (S n) -> Logging ann (NormalForm n)
-subst1 t u = subst u (add (Logging ann . NormalForm) (pure t) (pure . point))
+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 ------------------------------------------------------------------
 
@@ -155,7 +295,7 @@ convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do
   convert t2 u2 b s'
 -- Default
 convert t u a s =
-  inScope "invalid conversion:" $ fatal $
+  inScope "invalid conversion" $ fatal $
   fillSep {ann} [prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]
 
 
@@ -178,17 +318,19 @@ countVars (ctx :< y)  = weaken $ countVars ctx
 countVars (ctx ::< y) = FS $ countVars ctx
 
 index : TyContext m n -> Fin n -> (NormalForm n, NormalForm n, Sort)
-index (ctx :< def)           FZ     = (weaken 1 def.tm, weaken 1 def.ty, def.sort)
-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
+index (ctx :< def)              FZ     = (weaken 1 def.tm, weaken 1 def.ty, def.sort)
+index (ctx ::< (var, ty, Prop)) FZ     = (Irrel, weaken 1 ty, Prop)
+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
 asSubst : (ctx : TyContext m n) -> Fin n -> Logging ann (NormalForm m)
-asSubst (ctx :< def)           FZ     = subst def.tm (asSubst ctx)
-asSubst (ctx ::< (var, _, _))  FZ     = pure $ Ntrl $ Var var FZ
-asSubst (ctx :< def)           (FS i) = asSubst ctx i
-asSubst (ctx ::< _)            (FS i) = map (weaken 1) (asSubst ctx i)
+asSubst (ctx :< def)             FZ     = subst def.tm (asSubst ctx)
+asSubst (ctx ::< (var, _, Prop)) FZ     = pure Irrel
+asSubst (ctx ::< (var, _, _))    FZ     = pure $ Ntrl (Var var FZ)
+asSubst (ctx :< def)             (FS i) = asSubst ctx i
+asSubst (ctx ::< _)              (FS i) = map (weaken 1) (asSubst ctx i)
 
 -- Checking and Inference ------------------------------------------------------
 
@@ -205,7 +347,9 @@ check ctx tm@(Lambda _ _ t) (Cnstr (Pi s s' var a b)) _ = do
   inScope "check" $ trace $ map (\_ => "binding new variable to \{var}") (fullBounds tm)
   inScope "check" $ trace $ map (\_ => pretty {ann} "checking for type" <++> pretty b) (fullBounds tm)
   t <- check (ctx ::< (var, a, s)) t b s'
-  pure (Cnstr $ Lambda var t)
+  case s' of
+    Prop => pure Irrel
+    _ => pure (Cnstr $ Lambda var t)
 check ctx tm@(Lambda _ _ _) ty _ = typeMismatch (fullBounds tm).bounds (pretty "pi") (pretty ty)
 check ctx tm@(Pair _ t u) (Cnstr (Sigma s s' var a b)) _ = do
   inScope "check" $ trace $ map (\_ => "checking pair") (fullBounds tm)
@@ -215,7 +359,10 @@ check ctx tm@(Pair _ t u) (Cnstr (Sigma s s' var a b)) _ = do
   inScope "check" $ trace $ map (\_ => pretty {ann} "checking second for type" <++> pretty b) (fullBounds tm)
   u <- check ctx u b s'
   inScope "check" $ trace $ map (\_ => pretty {ann} "pair is well typed") (fullBounds tm)
-  pure (Cnstr $ Pair t u)
+  case (s, s') of
+    (Prop, Prop) => pure Irrel
+    _ => pure (Cnstr $ Pair t u)
+check ctx tm@(Pair _ _ _) ty _ = typeMismatch (fullBounds tm).bounds (pretty "sigma") (pretty ty)
 check ctx tm ty s = do
   let bounded = fullBounds tm
   inScope "check" $ trace $ map (\_ => "checking has fallen through") bounded
@@ -232,8 +379,8 @@ infer ctx tm@(Var b i) = do
   inScope "infer" $ trace $ map (\_ => "encountered variable \{b.val}@\{show i}") (fullBounds tm)
   let (t, a, s) = index ctx i
   inScope "infer" $ trace $ map (\_ => pretty {ann} "variable has type" <++> pretty a) (fullBounds tm)
-  pure $ (t, a, s)
-infer ctx (Sort b s) = pure $ (cast s, cast (suc s), suc (suc s))
+  pure (t, a, s)
+infer ctx (Sort b s) = pure (cast s, cast (suc s), suc (suc s))
 infer ctx tm@(Pi _ var a b) = do
   inScope "infer" $ trace $ map (\_ => "encountered Pi type") (fullBounds tm)
   (a, s) <- inferType ctx a
@@ -262,6 +409,7 @@ infer ctx tm@(Sigma _ var a b) = do
   (b, s') <- inferType (ctx ::< (var, a, s)) b
   inScope "infer" $ trace $ map (\_ => pretty {ann} "second has type" <++> pretty b <+> comma <+> softline <+> pretty "so Sigma type has type" <++> pretty (lub s s')) (fullBounds tm)
   pure (Cnstr (Sigma s s' var a b), cast (lub s s'), suc (lub s s'))
+infer ctx tm@(Pair _ _ _) = inScope "cannot infer type" $ fatal (fullBounds tm)
 infer ctx tm@(Fst _ t) = do
   inScope "infer" $ trace $ map (\_ => "encountered first projection") (fullBounds tm)
   let bounded = fullBounds t
@@ -293,6 +441,68 @@ infer ctx tm@(Absurd b a t) = do
   _ <- check ctx t (Cnstr Bottom) Prop
   inScope "infer" $ trace $ map (\_ => "proof of false is well typed") (fullBounds tm)
   pure (Ntrl Absurd, a, s)
+infer ctx tm@(Equal b t u) = do
+  inScope "infer" $ trace $ map (\_ => "encountered equal") (fullBounds tm)
+  (t, a, s) <- infer ctx t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "lhs has type" <++> pretty a) (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking rhs has same type") (fullBounds tm)
+  u <- check ctx u a s
+  inScope "infer" $ trace $ map (\_ => "rhs is well typed") (fullBounds tm)
+  res <- doEqual a t u
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty res) (fullBounds tm)
+  pure (res, cast Prop, Set 0)
+infer ctx tm@(Refl b t) = do
+  inScope "infer" $ trace $ map (\_ => "encountered refl") (fullBounds tm)
+  (t, a, s) <- infer ctx t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) (fullBounds tm)
+  ty <- doEqual a t t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty ty) (fullBounds tm)
+  pure (Irrel, ty, Prop)
+infer ctx tm@(Transp _ t b u t' e) = do
+  inScope "infer" $ trace $ map (\_ => "encountered transp") (fullBounds tm)
+  (t, a, s) <- infer ctx t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "start index has type" <++> pretty a) (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking end index has same type") (fullBounds tm)
+  t' <- check ctx t' a s
+  inScope "infer" $ trace $ map (\_ => "end index is well typed") (fullBounds tm)
+  let bounded = fullBounds b
+  let ty = Cnstr (Pi s (Set 0) "_" a (cast Prop))
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "checkout output is in" <++> pretty ty) (fullBounds tm)
+  b <- check ctx b ty s
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "output is well typed") (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking equality type") (fullBounds tm)
+  eq <- doEqual a t t'
+  _ <- check ctx e eq Prop
+  inScope "infer" $ trace $ map (\_ => "equality is well typed") (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking transformed value") (fullBounds tm)
+  inTy <- doApp b t
+  _ <- check ctx u inTy Prop
+  inScope "infer" $ trace $ map (\_ => "transformed value is well typed") (fullBounds tm)
+  outTy <- doApp b t'
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty outTy) (fullBounds tm)
+  pure (Irrel, outTy, Prop)
+infer ctx tm@(Cast _ b e t) = do
+  inScope "infer" $ trace $ map (\_ => "encountered cast") (fullBounds tm)
+  (t, a, s) <- infer ctx t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "input has type" <++> pretty a) (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking output has same sort") (fullBounds tm)
+  b <- check ctx b (cast s) (suc s)
+  inScope "infer" $ trace $ map (\_ => "output is well sorted") (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking equality type") (fullBounds tm)
+  eq <- doEqual (cast s) a b
+  _ <- check ctx e eq Prop
+  inScope "infer" $ trace $ map (\_ => "equality is well typed") (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty b) (fullBounds tm)
+  res <- doCastL a b t
+  pure (res, b, s)
+infer ctx tm@(CastId _ t) = do
+  inScope "infer" $ trace $ map (\_ => "encountered cast identity proof") (fullBounds tm)
+  (t, a, s) <- infer ctx t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) (fullBounds tm)
+  cast <- doCastL a a t
+  eq <- doEqual a cast t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "producing equality type" <++> pretty eq) (fullBounds tm)
+  pure (Irrel, eq, Prop)
 
 inferType ctx a = do
   (a, Cnstr (Sort s), _) <- infer ctx a