diff options
Diffstat (limited to 'src/Obs/Typing.idr')
| -rw-r--r-- | src/Obs/Typing.idr | 92 |
1 files changed, 90 insertions, 2 deletions
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 |