diff options
Diffstat (limited to 'src/Obs/Typing.idr')
| -rw-r--r-- | src/Obs/Typing.idr | 335 |
1 files changed, 165 insertions, 170 deletions
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr index 834dbb7..3ec91f7 100644 --- a/src/Obs/Typing.idr +++ b/src/Obs/Typing.idr @@ -335,178 +335,175 @@ asSubst (ctx ::< _) (FS i) = map (weaken 1) (asSubst ctx i) -- Checking and Inference ------------------------------------------------------ covering partial -check : TyContext m n -> Term n -> NormalForm n -> Sort -> Logging ann (NormalForm n) +check : TyContext m n -> WithBounds (Term n) -> NormalForm n -> Sort -> Logging ann (NormalForm n) covering partial -infer : TyContext m n -> Term n -> Logging ann (NormalForm n, NormalForm n, Sort) +infer : TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, NormalForm n, Sort) covering partial inferType : {default typeMismatch tag : forall a . Bounds -> Doc ann -> Doc ann -> Logging ann a} - -> TyContext m n -> Term n -> Logging ann (NormalForm n, Sort) - -check ctx tm@(Lambda _ _ t) (Cnstr (Pi s s' var a b)) _ = do - inScope "check" $ trace $ map (\_ => pretty {ann} "checking under lambda with type" <++> pretty a) (fullBounds tm) - 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' - 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) - 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) - 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 - (tm, ty', s') <- infer ctx tm - inScope "check" $ trace $ map (\_ => pretty {ann} "inferred type is" <++> pretty ty') bounded - let True = s == s' - | False => sortMismatch bounded.bounds (pretty s) (pretty s') - True <- convert !(subst ty $ asSubst ctx) !(subst ty' $ asSubst ctx) (cast s) (suc s) - | False => typeMismatch bounded.bounds (pretty ty) (pretty ty') - inScope "check" $ trace $ map (\_ => pretty {ann} "converted" <++> pretty ty' <+> softline <+> pretty "to" <++> pretty ty) bounded - pure tm - -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)) -infer ctx tm@(Pi _ var a b) = do - inScope "infer" $ trace $ map (\_ => "encountered Pi type") (fullBounds tm) - (a, s) <- inferType ctx a - inScope "infer" $ trace $ map (\_ => pretty {ann} "argument has type" <++> pretty a) (fullBounds tm) - (b, s') <- inferType (ctx ::< (var, a, s)) b - inScope "infer" $ trace $ map (\_ => pretty {ann} "result has type" <++> pretty b <+> comma <+> softline <+> pretty "so Pi type has type" <++> pretty (s ~> s')) (fullBounds tm) - pure (Cnstr (Pi s s' var a b), cast (s ~> s'), suc (s ~> s')) -infer ctx tm@(Lambda _ _ _) = inScope "cannot infer type" $ fatal (fullBounds tm) -infer ctx tm@(App t u) = do - inScope "infer" $ trace $ map (\_ => "encountered application") (fullBounds tm) - let bounded = fullBounds t - (t, ty@(Cnstr (Pi s s' _ a b)), _) <- infer ctx t - | (_, t, _) => inScope "wrong type to apply" $ fatal (map (\_ => t) bounded) - inScope "infer" $ trace $ map (\_ => pretty {ann} "function has type" <++> pretty ty) (fullBounds tm) - inScope "infer" $ trace $ map (\_ => pretty {ann} "checking argument has type" <++> pretty a) (fullBounds tm) - u <- check ctx u a s - inScope "infer" $ trace $ map (\_ => "argument is well typed") (fullBounds tm) - res <- doApp t u - 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@(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 - (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) -infer ctx tm@(Absurd b a t) = do - inScope "infer" $ trace $ map (\_ => "encountered absurd") (fullBounds tm) - (a, s) <- inferType ctx a - inScope "infer" $ trace $ map (\_ => pretty {ann} "will fudge to type" <++> pretty a) (fullBounds tm) - inScope "infer" $ trace $ map (\_ => pretty {ann} "checking for proof of false") (fullBounds tm) - _ <- 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) + -> TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, Sort) + +check ctx tm ty s = case (tm.val, ty) of + (Lambda _ t, Cnstr (Pi s s' var a b)) => do + inScope "check" $ trace $ map (\_ => pretty {ann} "checking under lambda with type" <++> pretty a) tm + inScope "check" $ trace $ map (\_ => "binding new variable to \{var}") tm + inScope "check" $ trace $ map (\_ => pretty {ann} "checking for type" <++> pretty b) tm + t <- check (ctx ::< (var, a, s)) t b s' + case s' of + Prop => pure Irrel + _ => pure (Cnstr $ Lambda var t) + (Lambda _ _, ty) => typeMismatch tm.bounds (pretty "pi") (pretty ty) + (Pair t u, Cnstr (Sigma s s' var a b)) => do + inScope "check" $ trace $ map (\_ => "checking pair") tm + inScope "check" $ trace $ map (\_ => pretty {ann} "checking first for type" <++> pretty a) tm + t <- check ctx t a s + b <- subst1 t b + inScope "check" $ trace $ map (\_ => pretty {ann} "checking second for type" <++> pretty b) tm + u <- check ctx u b s' + inScope "check" $ trace $ map (\_ => pretty {ann} "pair is well typed") tm + case (s, s') of + (Prop, Prop) => pure Irrel + _ => pure (Cnstr $ Pair t u) + (Pair _ _, ty) => typeMismatch tm.bounds (pretty "sigma") (pretty ty) + (_, _) => do + inScope "check" $ trace $ map (\_ => "checking has fallen through") tm + (v, a, s') <- infer ctx tm + inScope "check" $ trace $ map (\_ => pretty {ann} "inferred type is" <++> pretty a) tm + let True = s == s' + | False => sortMismatch tm.bounds (pretty s) (pretty s') + True <- convert !(subst ty $ asSubst ctx) !(subst a $ asSubst ctx) (cast s) (suc s) + | False => typeMismatch tm.bounds (pretty ty) (pretty a) + inScope "check" $ trace $ map (\_ => pretty {ann} "converted" <++> pretty a <+> softline <+> pretty "to" <++> pretty ty) tm + pure v + +infer ctx tm = case tm.val of + (Var var i) => do + inScope "infer" $ trace $ map (\_ => "encountered variable \{var}@\{show i}") tm + let (t, a, s) = index ctx i + inScope "infer" $ trace $ map (\_ => pretty {ann} "variable has type" <++> pretty a) tm + pure (t, a, s) + (Sort s) => pure (cast s, cast (suc s), suc (suc s)) + (Pi var a b) => do + inScope "infer" $ trace $ map (\_ => "encountered Pi type") tm + (a, s) <- inferType ctx a + inScope "infer" $ trace $ map (\_ => pretty {ann} "argument has type" <++> pretty a) tm + (b, s') <- inferType (ctx ::< (var.val, a, s)) b + inScope "infer" $ trace $ map (\_ => pretty {ann} "result has type" <++> pretty b <+> comma <+> softline <+> pretty "so Pi type has type" <++> pretty (s ~> s')) tm + pure (Cnstr (Pi s s' var.val a b), cast (s ~> s'), suc (s ~> s')) + (Lambda _ _) => inScope "cannot infer type" $ fatal tm + (App t u) => do + inScope "infer" $ trace $ map (\_ => "encountered application") tm + (t, ty@(Cnstr (Pi s s' _ a b)), _) <- infer ctx t + | (_, ty, _) => inScope "wrong type to apply" $ fatal (map (\_ => ty) tm) + inScope "infer" $ trace $ map (\_ => pretty {ann} "function has type" <++> pretty ty) tm + inScope "infer" $ trace $ map (\_ => pretty {ann} "checking argument has type" <++> pretty a) tm + u <- check ctx u a s + inScope "infer" $ trace $ map (\_ => "argument is well typed") tm + res <- doApp t u + ty <- subst1 u b + inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty ty) tm + pure (res, ty, s') + (Sigma var a b) => do + inScope "infer" $ trace $ map (\_ => "encountered Sigma type") tm + (a, s) <- inferType ctx a + inScope "infer" $ trace $ map (\_ => pretty {ann} "first has type" <++> pretty a) tm + (b, s') <- inferType (ctx ::< (var.val, 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')) tm + pure (Cnstr (Sigma s s' var.val a b), cast (lub s s'), suc (lub s s')) + (Pair _ _) => inScope "cannot infer type" $ fatal tm + (Fst t) => do + inScope "infer" $ trace $ map (\_ => "encountered first projection") tm + (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t + | (_, ty, _) => inScope "wrong type to fst" $ fatal (map (\_ => ty) tm) + inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) tm + res <- doFst t + inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty a) tm + pure (res, a, s) + (Snd t) => do + inScope "infer" $ trace $ map (\_ => "encountered first projection") tm + (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t + | (_, ty, _) => inScope "wrong type to fst" $ fatal (map (\_ => ty) tm) + inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) 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) tm + pure (res, b, s') + Top => pure $ (Cnstr Top, cast Prop, Set 0) + Point => pure $ (Irrel, Cnstr Top, Prop) + Bottom => pure $ (Cnstr Bottom, cast Prop, Set 0) + (Absurd a t) => do + inScope "infer" $ trace $ map (\_ => "encountered absurd") tm + (a, s) <- inferType ctx a + inScope "infer" $ trace $ map (\_ => pretty {ann} "will fudge to type" <++> pretty a) tm + inScope "infer" $ trace $ map (\_ => pretty {ann} "checking for proof of false") tm + _ <- check ctx t (Cnstr Bottom) Prop + inScope "infer" $ trace $ map (\_ => "proof of false is well typed") tm + pure (Ntrl Absurd, a, s) + (Equal t u) => do + inScope "infer" $ trace $ map (\_ => "encountered equal") tm + (t, a, s) <- infer ctx t + inScope "infer" $ trace $ map (\_ => pretty {ann} "lhs has type" <++> pretty a) tm + inScope "infer" $ trace $ map (\_ => "checking rhs has same type") tm + u <- check ctx u a s + inScope "infer" $ trace $ map (\_ => "rhs is well typed") tm + res <- doEqual a t u + inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty res) tm + pure (res, cast Prop, Set 0) + (Refl t) => do + inScope "infer" $ trace $ map (\_ => "encountered refl") tm + (t, a, s) <- infer ctx t + inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) tm + ty <- doEqual a t t + inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty ty) tm + pure (Irrel, ty, Prop) + (Transp t b u t' e) => do + inScope "infer" $ trace $ map (\_ => "encountered transp") tm + (t, a, s) <- infer ctx t + inScope "infer" $ trace $ map (\_ => pretty {ann} "start index has type" <++> pretty a) tm + inScope "infer" $ trace $ map (\_ => "checking end index has same type") tm + t' <- check ctx t' a s + inScope "infer" $ trace $ map (\_ => "end index is well typed") tm + let ty = Cnstr (Pi s (Set 0) "_" a (cast Prop)) + inScope "infer" $ trace $ map (\_ => pretty {ann} "checkout output is in" <++> pretty ty) tm + b <- check ctx b ty s + inScope "infer" $ trace $ map (\_ => pretty {ann} "output is well typed") tm + inScope "infer" $ trace $ map (\_ => "checking equality type") tm + eq <- doEqual a t t' + _ <- check ctx e eq Prop + inScope "infer" $ trace $ map (\_ => "equality is well typed") tm + inScope "infer" $ trace $ map (\_ => "checking transformed value") tm + inTy <- doApp b t + _ <- check ctx u inTy Prop + inScope "infer" $ trace $ map (\_ => "transformed value is well typed") tm + outTy <- doApp b t' + inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty outTy) tm + pure (Irrel, outTy, Prop) + (Cast b e t) => do + inScope "infer" $ trace $ map (\_ => "encountered cast") tm + (t, a, s) <- infer ctx t + inScope "infer" $ trace $ map (\_ => pretty {ann} "input has type" <++> pretty a) tm + inScope "infer" $ trace $ map (\_ => "checking output has same sort") tm + b <- check ctx b (cast s) (suc s) + inScope "infer" $ trace $ map (\_ => "output is well sorted") tm + inScope "infer" $ trace $ map (\_ => "checking equality type") tm + eq <- doEqual (cast s) a b + _ <- check ctx e eq Prop + inScope "infer" $ trace $ map (\_ => "equality is well typed") tm + inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty b) tm + res <- doCastL a b t + pure (res, b, s) + (CastId t) => do + inScope "infer" $ trace $ map (\_ => "encountered cast identity proof") tm + (t, a, s) <- infer ctx t + inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) tm + cast <- doCastL a a t + eq <- doEqual a cast t + inScope "infer" $ trace $ map (\_ => pretty {ann} "producing equality type" <++> pretty eq) tm + pure (Irrel, eq, Prop) inferType ctx a = do (a, Cnstr (Sort s), _) <- infer ctx a - | (_, ty, _) => tag (fullBounds a).bounds (pretty "sort") (pretty ty) + | (_, ty, _) => tag a.bounds (pretty "sort") (pretty ty) pure (a, s) -- Checking Definitions and Blocks --------------------------------------------- @@ -514,14 +511,12 @@ inferType ctx a = do covering partial checkDef : Context n -> Term.Definition n -> Logging ann (NormalForm.Definition n) checkDef ctx def = do - let tyBounds = (fullBounds def.ty).bounds - let tmBounds = (fullBounds def.tm).bounds (ty, sort) <- inferType {tag = \bounds, lhs, rhs => inScope "invalid declaration" $ mismatch bounds lhs rhs} (fromContext ctx) def.ty - inScope "check" $ debug (pretty {ann} "\{def.name} has type" <++> pretty ty) + inScope "check" $ debug $ map (\name => pretty {ann} "\{name} has type" <++> pretty ty) def.name tm <- check (fromContext ctx) def.tm ty sort - inScope "check" $ debug (pretty {ann} "\{def.name} is well typed with value" <++> pretty tm) + inScope "check" $ debug $ map (\name => pretty {ann} "\{name} is well typed with value" <++> pretty tm) def.name pure $ MkDefinition {name = def.name, ty, tm, sort} covering partial |