From 02cb45707da07d5e6faca92158d10a6e454a6bac Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 22 Dec 2022 00:02:23 +0000
Subject: Add Container types.

---
 src/Obs/Typing.idr | 92 ++++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 90 insertions(+), 2 deletions(-)

(limited to 'src/Obs/Typing.idr')

diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index b327397..f814f93 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -78,6 +78,8 @@ infer : TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, Norma
 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)
+partial
+inferSort : TyContext m n -> WithBounds (Term n) -> Logging ann Sort
 
 check ctx tm ty s = case (tm.val, ty) of
   (Lambda _ t, Cnstr (Pi s s' var a b)) => do
@@ -115,6 +117,22 @@ check ctx tm ty s = case (tm.val, ty) of
     inScope "check" $ trace $ map (\_ => " subterm is well typed") tm
     pure (Cnstr $ Right t)
   (Right _, ty) => typeMismatch tm.bounds (pretty "sum") (pretty ty)
+  (MkContainer t p f, Cnstr (Container s a s' s'')) => do
+    inScope "check" $ trace $ map (\_ => "checking container constructor") tm
+    let tagTy = tagTy s a s'
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking tag for type" <++> pretty tagTy) tm
+    t <- check ctx t (Cnstr tagTy) (s ~> suc s')
+    inScope "check" $ trace $ map (\_ => "tag is well typed") tm
+    positionTy <- positionTy s a s' t s''
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking position for type" <++> pretty positionTy) tm
+    p <- check ctx p (Cnstr positionTy) (s ~> s' ~> suc s'')
+    inScope "check" $ trace $ map (\_ => "position is well typed") tm
+    nextTy <- nextTy s a s' t s'' p
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking next for type" <++> pretty nextTy) tm
+    f <- check ctx f (Cnstr nextTy) (s ~> s' ~> s'' ~> s)
+    inScope "check" $ trace $ map (\_ => "next is well typed") tm
+    pure (Cnstr $ MkContainer t p f)
+  (MkContainer t p f, ty) => typeMismatch tm.bounds (pretty "container") (pretty ty)
   (_, _) => do
     inScope "check" $ trace $ map (\_ => "checking has fallen through") tm
     (v, a, s') <- infer ctx tm
@@ -193,8 +211,7 @@ infer ctx tm = case tm.val of
     (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)
+    l <- inferSort ctx l
     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
@@ -214,6 +231,72 @@ infer ctx tm = case tm.val of
     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)
+  (Container a s' s'') => do
+    inScope "infer" $ trace $ map (\_ => "encountered container") tm
+    (a, s) <- inferType ctx a
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "index has type" <++> pretty a) tm
+    s' <- inferSort ctx s'
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "tag has sort" <++> pretty s') tm
+    s'' <- inferSort ctx s''
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "position has sort" <++> pretty s'') tm
+    pure (Cnstr (Container s a s' s''), cast (lub s (suc $ lub s' s'')), suc (lub s (suc $ lub s' s'')))
+  (MkContainer _ _ _) => inScope "cannot infer type" $ fatal tm
+  (Tag t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered tag") tm
+    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
+      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm
+    tag <- doTag t
+    let out = tagTy s a s'
+    pure (tag, Cnstr out, s ~> suc s')
+  (Position t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered position") tm
+    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
+      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm
+    tag <- doTag t
+    pos <- doPosition t
+    out <- positionTy s a s' tag s''
+    pure (pos, Cnstr out, s ~> s' ~> suc s'')
+  (Next t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered next") tm
+    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
+      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm
+    tag <- doTag t
+    pos <- doPosition t
+    next <- doNext t
+    out <- nextTy s a s' tag s'' pos
+    pure (next, Cnstr out, s ~> s' ~> s'' ~> s)
+  (Sem l b t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered sem") tm
+    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
+      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "interpretting a container" <++> pretty ty) tm
+    l <- inferSort ctx l
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "output has sort" <++> pretty l) tm
+    let outTy = Cnstr (Pi s (suc l) "i" a (cast l))
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking output has type" <++> pretty outTy) tm
+    b <- check ctx b outTy (s ~> suc l)
+    inScope "infer" $ trace $ map (\_ => "output is well typed") tm
+    tag <- doTag t
+    pos <- doPosition t
+    next <- doNext t
+    let i = Ntrl (Var "i" 0)
+    tag <- doApp (weaken 1 tag) i
+    pos <- doApp (weaken 1 pos) i
+    next <- doApp (weaken 1 next) i
+    let t = Ntrl (Var "t" 0)
+    pos <- doApp (weaken 1 pos) t
+    next <- doApp (weaken 1 next) t
+    let p = Ntrl (Var "p" 0)
+    next <- doApp (weaken 1 next) p
+    out <- doApp (weaken 3 b) next
+    let out = Cnstr $ Lambda "i" $
+              Cnstr $ Sigma s' (s'' ~> l) "t" tag $
+              Cnstr $ Pi s'' l "p" pos out
+    let ty = Cnstr $ Pi s (suc (lub s' (s'' ~> l))) "i" a (cast (lub s' (s'' ~> l)))
+    pure (out, ty, suc (s ~> suc (lub s' (s'' ~> l))))
   Top => pure $ (Cnstr Top, cast Prop, Set 0)
   Point => pure $ (Irrel, Cnstr Top, Prop)
   Bottom  => pure $ (Cnstr Bottom, cast Prop, Set 0)
@@ -292,6 +375,11 @@ inferType ctx a = do
     | (_, ty, _) => tag a.bounds (pretty "sort") (pretty ty)
   pure (a, s)
 
+inferSort ctx a = do
+  (Cnstr (Sort s), _, _) <- infer ctx a
+    | (t, _, _) => inScope "infer" $ typeMismatch a.bounds (pretty "sort") (pretty t)
+  pure s
+
 -- Checking Definitions and Blocks ---------------------------------------------
 
 partial
-- 
cgit v1.2.3