diff options
Diffstat (limited to 'src/Obs/Typing.idr')
| -rw-r--r-- | src/Obs/Typing.idr | 578 |
1 files changed, 227 insertions, 351 deletions
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr index f814f93..4cc6d8e 100644 --- a/src/Obs/Typing.idr +++ b/src/Obs/Typing.idr @@ -1,6 +1,10 @@ module Obs.Typing -import Data.Vect +import Control.Monad.Maybe + +import Data.Nat + +import Decidable.Equality import Obs.Logging import Obs.NormalForm @@ -8,6 +12,7 @@ import Obs.NormalForm.Normalise import Obs.Sort import Obs.Substitution import Obs.Term +import Obs.Typing.Context import Obs.Typing.Conversion import System @@ -20,384 +25,255 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal -- Loggings ---------------------------------------------------------------------- -Rename (Logging ann . NormalForm) where - rename t f = pure $ rename !t f - -mismatch : Bounds -> Doc ann -> Doc ann -> Logging ann a -mismatch bounds lhs rhs = fatal $ - MkBounded - (pretty "expected" <++> lhs <+> comma <+> softline <+> pretty "got" <++> rhs) - False - bounds - -typeMismatch : Bounds -> Doc ann -> Doc ann -> Logging ann a -typeMismatch bounds lhs rhs = inScope "type mismatch" $ mismatch bounds lhs rhs - -sortMismatch : Bounds -> Doc ann -> Doc ann -> Logging ann a -sortMismatch bounds lhs rhs = inScope "sort mismatch" $ mismatch bounds lhs rhs +mismatch : (expected, got : Doc ann) -> Logging ann a +mismatch lhs rhs = fatal $ + hang 2 (pretty "expected" <+> line <+> lhs) <+> comma <+> line <+> + hang 2 (pretty "got" <+> line <+> align rhs) --- Typing Contexts ------------------------------------------------------------- +typeMismatch : Doc ann -> Doc ann -> Logging ann a +typeMismatch lhs rhs = inScope "type mismatch" $ mismatch lhs rhs -infix 5 ::< +sortMismatch : Doc ann -> Doc ann -> Logging ann a +sortMismatch lhs rhs = inScope "sort mismatch" $ mismatch lhs rhs -data TyContext : Nat -> Nat -> Type where - Nil : TyContext 0 0 - (:<) : TyContext m n -> NormalForm.Definition n -> TyContext m (S n) - (::<) : TyContext m n -> (String, NormalForm n, Sort) -> TyContext (S m) (S n) +-- Utilities ------------------------------------------------------------------- -fromContext : Context n -> TyContext 0 n -fromContext [] = [] -fromContext (ctx :< def) = fromContext ctx :< def +MkPair : (s, s' : Sort) + -> NormalForm (isSet s) ctx + -> NormalForm (isSet s') ctx + -> NormalForm (isSet (max s s')) ctx +MkPair Prop Prop t u = u +MkPair Prop s'@(Set _) t u = Cnstr $ Pair Prop s' Oh t u +MkPair s@(Set _) s' t u = Cnstr $ Pair s s' Oh t u -countVars : TyContext m n -> Fin (S n) -countVars [] = FZ -countVars (ctx :< y) = weaken $ countVars ctx -countVars (ctx ::< y) = FS $ countVars ctx +-- Checking and Inference ------------------------------------------------------ -index : TyContext m n -> Fin n -> (NormalForm n, NormalForm n, Sort) -index (ctx :< def) FZ = (weaken 1 def.tm, weaken 1 def.ty, def.sort) -index (ctx ::< (var, ty, Prop)) FZ = (Irrel, weaken 1 ty, Prop) -index (ctx ::< (var, ty, s)) FZ = (Ntrl $ Var var FZ, weaken 1 ty, s) -index (ctx :< _) (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i -index (ctx ::< _) (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i +check : (tyCtx : TyContext ctx) + -> (s : Sort) + -> NormalForm True ctx + -> WithBounds (Term (length ctx)) + -> Logging ann (NormalForm (isSet s) ctx) -partial -asSubst : (ctx : TyContext m n) -> Fin n -> Logging ann (NormalForm m) -asSubst (ctx :< def) FZ = subst def.tm (asSubst ctx) -asSubst (ctx ::< (var, _, Prop)) FZ = pure Irrel -asSubst (ctx ::< (var, _, _)) FZ = pure $ Ntrl (Var var FZ) -asSubst (ctx :< def) (FS i) = asSubst ctx i -asSubst (ctx ::< _) (FS i) = map (weaken 1) (asSubst ctx i) +checkType : (tyCtx : TyContext ctx) + -> (s : Sort) + -> WithBounds (Term (length ctx)) + -> Logging ann (NormalForm True ctx) +checkType ctx s tm = check ctx (suc s) (cast s) tm --- Checking and Inference ------------------------------------------------------ +infer : (tyCtx : TyContext ctx) + -> WithBounds (Term (length ctx)) + -> Logging ann (s ** (NormalForm True ctx, NormalForm (isSet s) ctx)) -partial -check : TyContext m n -> WithBounds (Term n) -> NormalForm n -> Sort -> Logging ann (NormalForm n) -partial -infer : TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, NormalForm n, Sort) -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 +inferType : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a} + -> (tyCtx : TyContext ctx) + -> WithBounds (Term (length ctx)) + -> Logging ann (Sort, NormalForm True ctx) +inferType ctx tm = inBounds tm.bounds $ do + (Set _ ** (Cnstr (Sort s), a)) <- infer ctx tm + | (_ ** (a, t)) => tag (pretty "sort") (pretty a) + pure (s, a) -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 +check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of + (Cnstr (Pi l l' _ a b), Lambda var t) => do + info "encountered lambda" + trace $ pretty {ann} "checking body has type" <++> pretty b + t <- check (ctx ::< MkFreeVar l a var.val) l' b (assert_smaller tm t) + let Yes Refl = decEq s (l ~> l') + | No _ => fatal "internal sort mismatch" + pure $ case l' of + Prop => Irrel + Set _ => Cnstr (Lambda l var.val t) + (_, Lambda var t) => typeMismatch (pretty "function") (pretty ty) + (Cnstr (Sigma l l' var a b), Pair t u) => do + info "encountered pair" + trace $ pretty {ann} "checking first has type" <++> pretty a + t <- check ctx l a (assert_smaller tm t) 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) - (Left t, Cnstr (Sum s s' a b)) => do - inScope "check" $ trace $ map (\_ => "checking left injection") tm - inScope "check" $ trace $ map (\_ => pretty {ann} "checking subterm for type" <++> pretty a) tm - t <- check ctx t a s - inScope "check" $ trace $ map (\_ => " subterm is well typed") tm - pure (Cnstr $ Left t) - (Left _, ty) => typeMismatch tm.bounds (pretty "sum") (pretty ty) - (Right t, Cnstr (Sum s s' a b)) => do - inScope "check" $ trace $ map (\_ => "checking right injection") tm - inScope "check" $ trace $ map (\_ => pretty {ann} "checking subterm for type" <++> pretty b) tm - t <- check ctx t b s' - 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 - 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 + trace $ pretty {ann} "checking second has type" <++> pretty b + u <- check ctx l' b (assert_smaller tm u) + let Yes Refl = decEq s (max l l') + | No _ => fatal "internal sort mismatch" + pure $ MkPair l l' t u + (_, Pair t u) => typeMismatch (pretty "pair type") (pretty ty) + (_, Absurd t) => do + info "encountered absurd" + trace "checking proof of contradiction" + Irrel <- check ctx Prop (Cnstr Bottom) (assert_smaller tm t) + pure $ doAbsurd _ + (a, t) => do + info "falling through to inference" + (l ** (b, t)) <- infer ctx tm + trace $ pretty {ann} "inferred type is" <++> pretty b + let Yes Refl = decEq s l + | No _ => typeMismatch (pretty a) (pretty b) + a' <- subst a (reduce ctx) + b' <- subst b (reduce ctx) + Just _ <- inScope "convert" $ runMaybeT $ convert (suc s) (cast s) a' b' + | Nothing => inScope "conversion failed" $ mismatch (pretty a) (pretty b) + pure t -infer ctx tm = case tm.val of +infer ctx tm = inBounds tm.bounds $ 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)) + info $ pretty {ann} "encountered variable" <++> pretty tm.val + let def = index' ctx i + pure (def.sort ** (def.ty, def.tm)) + (Sort s) => do + info $ pretty {ann} "encountered sort" <++> pretty tm.val + pure (suc (suc s) ** (cast (suc s), cast 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 + info "encountered pi" + (s, a) <- inferType ctx (assert_smaller tm a) + trace $ pretty {ann} "domain type is" <++> pretty a + (s', b) <- inferType (ctx ::< MkFreeVar s a var.val) (assert_smaller tm b) + trace $ pretty {ann} "codomain type is" <++> pretty b + pure (suc (s ~> s') ** (cast (s ~> s'), Cnstr (Pi s s' var.val a b))) + (Lambda var t) => fatal "cannot infer type of lambda" (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 + info "encountered application" + (s ** (ty@(Cnstr (Pi l l' _ a b)), t)) <- infer ctx (assert_smaller tm t) + | (_ ** (ty, _)) => inBounds t.bounds $ typeMismatch (pretty "function") (pretty ty) + trace $ pretty {ann} "function has type" <++> pretty ty + trace $ pretty {ann} "checking argument has type" <++> pretty a + u <- check ctx l a (assert_smaller tm u) + trace $ pretty {ann} "argument is well typed" + let Yes Refl = decEq s (l ~> l') + | No _ => fatal "internal sort mismatch" 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') + tm <- doApp t u + pure (l' ** (ty, rewrite sym $ impredicative l l' in tm)) (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 + info "encountered sigma" + (s, a) <- inferType ctx (assert_smaller tm a) + trace $ pretty {ann} "first type is" <++> pretty a + (s', b) <- inferType (ctx ::< MkFreeVar s a var.val) (assert_smaller tm b) + trace $ pretty {ann} "second type is" <++> pretty b + pure (suc (max s s') ** (cast (max s s'), Cnstr (Sigma s s' var.val a b))) + (Pair t u) => fatal "cannot infer type of pair" (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) + info "encountered first" + (s ** (ty@(Cnstr (Sigma l l' _ a b)), t)) <- infer ctx (assert_smaller tm t) + | (_ ** (ty, _)) => inBounds t.bounds $ typeMismatch (pretty "pair type") (pretty ty) + trace $ pretty {ann} "pair has type" <++> pretty ty + let Yes Refl = decEq s (max l l') + | No _ => fatal "internal sort mismatch" + let ty = a + tm <- doFst (isSet l) (isSet l') (rewrite sym $ maxIsSet l l' in t) + pure (l ** (ty, tm)) (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 snd" $ 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') - (Sum a b) => do - inScope "infer" $ trace $ map (\_ => "encountered sum type") tm - (a, s) <- inferType ctx a - inScope "infer" $ trace $ map (\_ => pretty {ann} "left has type" <++> pretty a) tm - (b, s') <- inferType ctx b - inScope "infer" $ trace $ map (\_ => pretty {ann} "right has type" <++> pretty b) tm - pure (Cnstr (Sum s s' a b), cast (ensureSet (lub s s')), suc (ensureSet (lub s s'))) - (Left _) => inScope "cannot infer type" $ fatal tm - (Right _) => inScope "cannot infer type" $ fatal tm - (Case t l out f g) => do - inScope "infer" $ trace $ map (\_ => "encountered case") tm - (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 - 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 - out <- check ctx out ty' (s'' ~> suc l) - inScope "infer" $ trace $ map (\_ => "output is well typed") tm - outL <- doApp (weaken 1 out) (Cnstr (Left (Ntrl (Var "x" 0)))) - let fTy = Cnstr (Pi s l "x" a outL) - inScope "infer" $ trace $ map (\_ => pretty {ann} "checking left branch has type" <++> pretty fTy) tm - f <- check ctx f fTy (s ~> l) - inScope "infer" $ trace $ map (\_ => "left branch is well typed") tm - outR <- doApp (weaken 1 out) (Cnstr (Right (Ntrl (Var "x" 0)))) - let gTy = Cnstr (Pi s' l "x" b outR) - inScope "infer" $ trace $ map (\_ => pretty {ann} "checking right branch has type" <++> pretty gTy) tm - g <- check ctx g gTy (s' ~> l) - inScope "infer" $ trace $ map (\_ => "right branch is well typed") tm - res <- doCase t f g - 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) - (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) + info "encountered second" + (s ** (ty@(Cnstr (Sigma l l' _ a b)), t)) <- infer ctx (assert_smaller tm t) + | (_ ** (ty, _)) => inBounds t.bounds $ typeMismatch (pretty "pair type") (pretty ty) + trace $ pretty {ann} "pair has type" <++> pretty ty + let Yes Refl = decEq s (max l l') + | No _ => fatal "internal sort mismatch" + let t = rewrite sym $ maxIsSet l l' in t + fst <- doFst (isSet l) (isSet l') t + ty <- subst1 fst b + tm <- doSnd (isSet l) (isSet l') t + pure (l' ** (ty, tm)) + Bool => do + info "encountered bool" + pure (Set 1 ** (cast (Set 0), Cnstr Bool)) + True => do + info "encountered true" + pure (Set 0 ** (Cnstr Bool, Cnstr True)) + False => do + info "encountered false" + pure (Set 0 ** (Cnstr Bool, Cnstr False)) + (If var a t u v) => do + info "encountered if" + trace "checking discriminant is bool" + t <- check ctx (Set 0) (Cnstr Bool) (assert_smaller tm t) + trace "discriminant is well typed" + (s, a) <- inferType (ctx ::< MkFreeVar (Set 0) (Cnstr Bool) var.val) (assert_smaller tm a) + ty <- subst1 (Cnstr True) a + trace $ pretty {ann} "checking true branch has type" <++> pretty ty + u <- check ctx s ty (assert_smaller tm u) + ty <- subst1 (Cnstr False) a + trace $ pretty {ann} "checking false branch has type" <++> pretty ty + v <- check ctx s ty (assert_smaller tm v) + ty <- subst1 t a + tm <- doIf t u v + pure (s ** (ty, tm)) + Top => do + info "encountered top" + pure (Set 0 ** (cast Prop, Cnstr Top)) + Point => do + info "encountered point" + pure (Prop ** (Cnstr Top, Irrel)) + Bottom => do + info "encountered bottom" + pure (Set 0 ** (cast Prop, Cnstr Bottom)) + (Absurd t) => fatal "cannot infer type of absurd" (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) + info "encountered equal" + (s ** (a, t)) <- infer ctx (assert_smaller tm t) + trace $ pretty {ann} "left side has type" <++> pretty a + u <- check ctx s a (assert_smaller tm u) + trace "right side is well typed" + eq <- doEqual (isSet s) a t u + pure (Set 0 ** (cast Prop, eq)) (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) + info "encountered refl" + (s ** (a, t)) <- infer ctx (assert_smaller tm t) + trace "argument is well typed" + eq <- doEqual (isSet s) a t t + pure (Prop ** (eq, Irrel)) + (Transp b t u t' e) => do + info "encountered transp" + (s ** (a, t)) <- infer ctx (assert_smaller tm t) + trace $ pretty {ann} "index type is" <++> pretty a + t' <- check ctx s a (assert_smaller tm t') + trace "new index is well typed" + b <- check ctx (s ~> Set 0) (Cnstr $ Pi s (Set 0) "" a (cast Prop)) (assert_smaller tm b) + trace "transporting in Prop" + oldB <- doApp b t + u <- check ctx Prop oldB (assert_smaller tm u) + trace "old-indexed proposition is well typed" + eq <- doEqual (isSet s) a t t' + trace $ pretty {ann} "checking equality has type" <++> pretty eq + e <- check ctx Prop eq (assert_smaller tm e) + trace "equality is well typed" + newB <- doApp b t' + pure (Prop ** (newB, Irrel)) + (Cast a b e t) => do + info "encountered cast" + (s, a) <- inferType ctx (assert_smaller tm a) + trace $ pretty {ann} "old type is" <++> pretty a + b <- checkType ctx s (assert_smaller tm b) + trace $ pretty {ann} "new type is" <++> pretty b + eq <- doEqual True (cast s) a b + e <- check ctx Prop eq (assert_smaller tm e) + trace "equality is well typed" + t <- check ctx s a (assert_smaller tm t) + trace "value is well typed" + tm <- doCast (isSet s) a b t + pure (s ** (b, tm)) (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 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 + info "encountered castRefl" + (s ** (a, t)) <- infer ctx (assert_smaller tm t) + trace $ pretty {ann} "argument has type" <++> pretty a + lhs <- doCast (isSet s) a a t + ret <- doEqual (isSet s) a lhs t + pure (Prop ** (ret, Irrel)) -- Checking Definitions and Blocks --------------------------------------------- -partial -checkDef : Context n -> Term.Definition n -> Logging ann (NormalForm.Definition n) -checkDef ctx def = do - (ty, sort) <- - inferType {tag = \bounds, lhs, rhs => inScope "invalid declaration" $ mismatch bounds lhs rhs} +checkDef : Context ctx -> Term.Definition (length ctx) -> Logging ann (NormalForm.Definition ctx) +checkDef ctx def = inBounds def.name.bounds $ inScope "check" $ do + debug $ "inferring type of \{def.name.val}" + (sort, ty) <- + inferType {tag = \lhs, rhs => inScope "invalid declaration" $ mismatch lhs rhs} (fromContext ctx) def.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 $ map (\name => pretty {ann} "\{name} is well typed with value" <++> pretty tm) def.name + debug $ pretty {ann} "\{def.name.val} has type" <++> pretty ty + tm <- check (fromContext ctx) sort ty def.tm + debug $ pretty {ann} "\{def.name.val} is well typed with value" <++> pretty tm pure $ MkDefinition {name = def.name, ty, tm, sort} -partial export -checkBlock : Block n -> Logging ann (Context n) -checkBlock [] = pure [] +checkBlock : Block n -> Logging ann (ctx ** (Context ctx, length ctx = n)) +checkBlock [] = pure ([] ** ([], Refl)) checkBlock (blk :< def) = do - ctx <- checkBlock blk + (_ ** (ctx, Refl)) <- checkBlock blk def <- checkDef ctx def - pure (ctx :< def) + pure (_ ** (ctx :< def, Refl)) |