diff options
Diffstat (limited to 'src/Obs/Typing.idr')
| -rw-r--r-- | src/Obs/Typing.idr | 22 |
1 files changed, 17 insertions, 5 deletions
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr index 22994ec..e59de5d 100644 --- a/src/Obs/Typing.idr +++ b/src/Obs/Typing.idr @@ -20,12 +20,17 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal -- invariant: all definitions fully expanded -- invariant: m |- t, u <- a : s convert : (t, u, a : NormalForm n) -> Sort -> Bool +-- In sort Prop convert Irrel Irrel a Prop = True +-- In unknown type in set convert t u (Ntrl _) (Set k) = t == u -convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort Prop)) (Set 0) = True +-- In type Set +convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort _)) (Set _) = s' == s'' +convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort _)) (Set _) = True +convert (Cnstr Bottom) (Cnstr Bottom) (Cnstr (Sort _)) (Set _) = True convert (Ntrl t) u (Cnstr (Sort s)) (Set k) = Ntrl t == u convert t (Ntrl u) (Cnstr (Sort s)) (Set k) = t == Ntrl u -convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort s)) (Set k) = s' == s'' +-- Default convert _ _ _ _ = False -- Typing Contexts ------------------------------------------------------------- @@ -61,7 +66,7 @@ check : Context n -> Term n -> NormalForm n -> Sort -> Error ann (NormalForm n) infer : Context n -> Term n -> Error ann (NormalForm n, NormalForm n, Sort) check ctx tm ty s = do - let bounds = fullBounds tm + let bounds = (fullBounds tm).bounds (tm, ty', s') <- infer ctx tm let True = s == s' | False => report bounds @@ -75,13 +80,20 @@ infer ctx (Var b i) = pure $ index ctx i infer ctx (Sort b s) = pure $ (Cnstr (Sort s), Cnstr (Sort (suc s)), suc (suc s)) infer ctx (Top b) = pure $ (Cnstr Top, Cnstr (Sort Prop), Set 0) infer ctx (Point b) = pure $ (Irrel, Cnstr Top, Prop) +infer ctx (Bottom b) = pure $ (Cnstr Bottom, Cnstr (Sort Prop), Set 0) +infer ctx (Absurd b a t) = do + (a, Cnstr (Sort s), _) <- infer ctx a + | (_, ty, _) => report (fullBounds a).bounds + (pretty "type mismatch: expected sort" <+> comma <+> softline <+> "got" <++> pretty ty) + _ <- check ctx t (Cnstr Bottom) Prop + pure (Ntrl Absurd, a, s) -- Checking Definitions and Blocks --------------------------------------------- checkDef : Context n -> Term.Definition n -> Error ann (NormalForm.Definition n) checkDef ctx def = do - let tyBounds = fullBounds def.ty - let tmBounds = fullBounds def.tm + let tyBounds = (fullBounds def.ty).bounds + let tmBounds = (fullBounds def.tm).bounds (ty, Cnstr (Sort sort), _) <- infer ctx def.ty | (_, a, _) => report tyBounds (pretty "invalid declaration: expected sort" <+> comma <+> softline <+> "got" <++> pretty a) |