Add dependent sums.

1 files changed, 77 insertions, 0 deletions

diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index c5d837f..bf7ebc1 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -52,6 +52,10 @@ covering partial
 subst      : NormalForm n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
 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)
 
 substCnstr (Sort s) f = pure $ Sort s
 substCnstr (Pi s s' var a b) f = do
@@ -61,6 +65,14 @@ substCnstr (Pi s s' var a b) f = do
 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
 
@@ -72,6 +84,12 @@ 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
 
 subst (Ntrl t)  f = substNtrl t f
@@ -83,6 +101,16 @@ 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
 
+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
+
+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
+
 partial
 subst1 : NormalForm n -> NormalForm (S n) -> Logging ann (NormalForm n)
 subst1 t u = subst u (add (Logging ann . NormalForm) (pure t) (pure . point))
@@ -102,6 +130,9 @@ convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort _)) (Set _) = pure $ 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
@@ -112,6 +143,16 @@ 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 $
@@ -166,6 +207,15 @@ check ctx tm@(Lambda _ _ t) (Cnstr (Pi s s' var a b)) _ = do
   t <- check (ctx ::< (var, a, s)) t b s'
   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)
+  inScope "check" $ trace $ map (\_ => pretty {ann} "checking first for type" <++> pretty a) (fullBounds tm)
+  t <- check ctx t a s
+  b <- subst1 t b
+  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)
 check ctx tm ty s = do
   let bounded = fullBounds tm
   inScope "check" $ trace $ map (\_ => "checking has fallen through") bounded
@@ -205,6 +255,33 @@ infer ctx tm@(App t u) = do
   ty <- subst1 u b
   inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty ty) (fullBounds tm)
   pure (res, ty, s')
+infer ctx tm@(Sigma _ var a b) = do
+  inScope "infer" $ trace $ map (\_ => "encountered Sigma type") (fullBounds tm)
+  (a, s) <- inferType ctx a
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "first has type" <++> pretty a) (fullBounds tm)
+  (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@(Fst _ t) = do
+  inScope "infer" $ trace $ map (\_ => "encountered first projection") (fullBounds tm)
+  let bounded = fullBounds t
+  (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
+    | (_, t, _) => inScope "wrong type to fst" $ fatal (map (\_ => t) bounded)
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) (fullBounds tm)
+  res <- doFst t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty a) (fullBounds tm)
+  pure (res, a, s)
+infer ctx tm@(Snd _ t) = do
+  inScope "infer" $ trace $ map (\_ => "encountered first projection") (fullBounds tm)
+  let bounded = fullBounds t
+  (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
+    | (_, t, _) => inScope "wrong type to fst" $ fatal (map (\_ => t) bounded)
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) (fullBounds 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) (fullBounds tm)
+  pure (res, b, s')
 infer ctx (Top b) = pure $ (Cnstr Top, cast Prop, Set 0)
 infer ctx (Point b) = pure $ (Irrel, Cnstr Top, Prop)
 infer ctx (Bottom b) = pure $ (Cnstr Bottom, cast Prop, Set 0)