diff options
Diffstat (limited to 'src/Obs/Typing.idr')
| -rw-r--r-- | src/Obs/Typing.idr | 468 |
1 files changed, 308 insertions, 160 deletions
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr index 7bb5deb..b3762cf 100644 --- a/src/Obs/Typing.idr +++ b/src/Obs/Typing.idr @@ -48,11 +48,31 @@ MkPair s@(Set _) s' t u = Cnstr $ Pair s s' Set t u -- Checking and Inference ------------------------------------------------------ +check' : (tyCtx : TyContext ctx) + -> (s : Universe) + -> TypeNormalForm ctx + -> Term (length ctx) + -> Logging ann (NormalForm (relevance s) ctx) + +infer' : (tyCtx : TyContext ctx) + -> Term (length ctx) + -> Logging ann (s ** (TypeNormalForm ctx, NormalForm (relevance s) ctx)) + +inferType' : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a} + -> (tyCtx : TyContext ctx) + -> Term (length ctx) + -> Logging ann (Universe, TypeNormalForm ctx) +inferType' ctx t = do + (Set _ ** (Cnstr (Universe s), a)) <- infer' ctx t + | (_ ** (type, a)) => tag (pretty "sort") (pretty type) + pure (s, a) + check : (tyCtx : TyContext ctx) -> (s : Universe) -> TypeNormalForm ctx -> WithBounds (Term (length ctx)) -> Logging ann (NormalForm (relevance s) ctx) +check ctx s a (MkBounded t irrel bounds) = inBounds (MkBounded (check' ctx s a t) irrel bounds) checkType : (tyCtx : TyContext ctx) -> (s : Universe) @@ -63,212 +83,340 @@ checkType ctx s tm = check ctx (succ s) (cast s) tm infer : (tyCtx : TyContext ctx) -> WithBounds (Term (length ctx)) -> Logging ann (s ** (TypeNormalForm ctx, NormalForm (relevance s) ctx)) +infer ctx (MkBounded t irrel bounds) = inBounds (MkBounded (infer' ctx t) irrel bounds) inferType : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a} -> (tyCtx : TyContext ctx) -> WithBounds (Term (length ctx)) -> Logging ann (Universe, TypeNormalForm ctx) -inferType ctx tm = inBounds tm.bounds $ do - (Set _ ** (Cnstr (Universe s), a)) <- infer ctx tm - | (_ ** (a, t)) => tag (pretty "universe") (pretty a) - pure (s, a) +inferType ctx (MkBounded t irrel bounds) = inBounds (MkBounded (inferType' ctx t) irrel bounds) + +check' ctx sort (Cnstr (Pi domainSort codomainSort _ domain codomain)) (Lambda {var, body}) = do + info "encountered lambda" + + let Yes Refl = decEq sort (domainSort ~> codomainSort) + | No _ => fatal "internal universe mismatch" + + let bodyCtx = ctx ::< MkFreeVar domainSort domain var.val + + trace $ pretty {ann} "checking body has type" <++> pretty codomainSort + body <- check bodyCtx codomainSort codomain body + + pure $ case codomainSort of + Prop => Irrel + Set _ => Cnstr (Lambda domainSort var.val body) + +check' ctx sort type (Lambda {var, body}) = typeMismatch (pretty "function") (pretty type) + +check' ctx sort (Cnstr (Sigma indexSort elementSort var index element)) (Pair {first, second}) = do + info "encountered pair" + + let Yes Refl = decEq sort (max indexSort elementSort) + | No _ => fatal "internal universe mismatch" + + trace $ pretty {ann} "checking first has type" <++> pretty index + first <- check ctx indexSort index first + + element <- subst1 first element + trace $ pretty {ann} "checking second has type" <++> pretty element + second <- check ctx elementSort element second + + pure $ MkPair indexSort elementSort first second + +check' ctx sort type (Pair {first, second}) = typeMismatch (pretty "pair type") (pretty type) + +check' ctx sort type (Absurd {contradiction}) = do + info "encountered absurd" + + trace "checking proof of contradiction" + Irrel <- check ctx Prop (Cnstr Bottom) contradiction + + pure $ doAbsurd _ + +check' ctx sort type t = do + info "falling through to inference" + + (inferredSort ** (inferredType, value)) <- infer' ctx t + trace $ pretty {ann} "inferred type is" <++> pretty inferredType + + let Yes Refl = decEq sort inferredSort + | No _ => typeMismatch (pretty type) (pretty inferredType) + + expandedType <- subst type (reduce ctx) + expandedInferredType <- subst inferredType (reduce ctx) + + Just _ <- inScope "convert" $ runMaybeT $ convert (succ sort) (cast sort) expandedType expandedInferredType + | Nothing => inScope "conversion failed" $ mismatch (pretty type) (pretty inferredType) + + pure value + + +infer' ctx tm@(Var {var, i}) = do + info $ pretty {ann} "encountered variable" <++> pretty tm -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 universe 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 - 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 universe 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 (succ s) (cast s) a' b' - | Nothing => inScope "conversion failed" $ mismatch (pretty a) (pretty b) - pure t - -infer ctx tm = inBounds tm.bounds $ case tm.val of - (Var var i) => do - info $ pretty {ann} "encountered variable" <++> pretty tm.val let def = index' ctx i pure (def.sort ** (def.ty, def.tm)) - (Universe s) => do - info $ pretty {ann} "encountered universe" <++> pretty tm.val + +infer' ctx (Universe {s}) = do + info $ pretty {ann} "encountered universe" <++> pretty s + pure (succ (succ s) ** (cast (succ s), cast s)) - (Pi var a b) => do + +infer' ctx (Pi {var, domain, codomain}) = do 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 (succ (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 + + (domainSort, domain) <- inferType ctx domain + trace $ pretty {ann} "domain type is" <++> pretty domain + + let domainVar = MkFreeVar domainSort domain var.val + let codomainCtx = ctx ::< domainVar + + (codomainSort, codomain) <- inferType codomainCtx codomain + trace $ pretty {ann} "codomain type is" <++> pretty codomain + + let piSort = domainVar.sort ~> codomainSort + let term = Cnstr (Pi domainVar.sort codomainSort var.val domain codomain) + pure (succ piSort ** (cast piSort, term)) + +infer' ctx (Lambda {var, body}) = fatal "cannot infer type of lambda" + +infer' ctx (App {fun, arg}) = do 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') + + (piSort ** (funType, funValue)) <- infer ctx fun + trace $ pretty {ann} "function has type" <++> pretty funType + + let Cnstr (Pi domainSort codomainSort _ domain codomain) = funType + | _ => inBounds $ map (const $ typeMismatch (pretty "function") (pretty funType)) fun + + let Yes Refl = decEq piSort (domainSort ~> codomainSort) | No _ => fatal "internal universe mismatch" - ty <- subst1 u b - tm <- doApp t u - pure (l' ** (ty, rewrite sym $ functionRelevance l l' in tm)) - (Sigma var a b) => do + + let fun = funValue + + trace $ pretty {ann} "checking argument has type" <++> pretty domain + arg <- check ctx domainSort domain arg + trace $ pretty {ann} "argument is well typed" + + returnType <- subst1 arg codomain + returnValue <- doApp fun arg + + let returnValue = rewrite sym $ functionRelevance domainSort codomainSort in returnValue + + pure (codomainSort ** (returnType, returnValue)) + +infer' ctx (Sigma {var, index, element}) = do 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 (succ (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 + + (indexSort, index) <- inferType ctx index + trace $ pretty {ann} "index type is" <++> pretty index + + let indexVar = MkFreeVar indexSort index var.val + let elementCtx = ctx ::< indexVar + + (elementSort, element) <- inferType elementCtx element + trace $ pretty {ann} "element type is" <++> pretty element + + let sigmaSort = max indexVar.sort elementSort + let term = Cnstr (Sigma indexVar.sort elementSort var.val index element) + pure (succ sigmaSort ** (cast sigmaSort, term)) + +infer' ctx (Pair {first, second}) = fatal "cannot infer type of pair" + +infer' ctx (First {arg}) = do 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') + + (sigmaSort ** (argType, argValue)) <- infer ctx arg + trace $ pretty {ann} "pair has type" <++> pretty argType + + let Cnstr (Sigma indexSort elementSort _ index element) = argType + | _ => inBounds $ map (const $ typeMismatch (pretty "pair type") (pretty argType)) arg + + let Yes Refl = decEq sigmaSort (max indexSort elementSort) | No _ => fatal "internal universe mismatch" - let ty = a - tm <- doFst (relevance l) (relevance l') (rewrite sym $ pairRelevance l l' in t) - pure (l ** (ty, tm)) - (Snd t) => do + + let argValue = rewrite sym $ pairRelevance indexSort elementSort in argValue + + let returnType = index + returnValue <- doFst (relevance indexSort) (relevance elementSort) argValue + + pure (indexSort ** (returnType, returnValue)) + +infer' ctx (Second {arg}) = do 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') + + (sigmaSort ** (argType, argValue)) <- infer ctx arg + trace $ pretty {ann} "pair has type" <++> pretty argType + + let Cnstr (Sigma indexSort elementSort _ index element) = argType + | _ => inBounds $ map (const $ typeMismatch (pretty "pair type") (pretty argType)) arg + + let Yes Refl = decEq sigmaSort (max indexSort elementSort) | No _ => fatal "internal universe mismatch" - let t = rewrite sym $ pairRelevance l l' in t - fst <- doFst (relevance l) (relevance l') t - ty <- subst1 fst b - tm <- doSnd (relevance l) (relevance l') t - pure (l' ** (ty, tm)) - Bool => do + + let argValue = rewrite sym $ pairRelevance indexSort elementSort in argValue + + indexValue <- doFst (relevance indexSort) (relevance elementSort) argValue + returnType <- subst1 indexValue element + returnValue <- doSnd (relevance indexSort) (relevance elementSort) argValue + + pure (elementSort ** (returnType, returnValue)) + +infer' ctx Bool = do info "encountered bool" pure (Set 1 ** (cast (Set 0), Cnstr Bool)) - True => do + +infer' ctx True = do info "encountered true" pure (Set 0 ** (Cnstr Bool, Cnstr True)) - False => do + +infer' ctx False = do info "encountered false" pure (Set 0 ** (Cnstr Bool, Cnstr False)) - (If var a t u v) => do + +infer' ctx (If {var, returnType, discriminant, true, false}) = do info "encountered if" trace "checking discriminant is bool" - t <- check ctx (Set 0) (Cnstr Bool) (assert_smaller tm t) + + discriminant <- check ctx (Set 0) (Cnstr Bool) discriminant 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 + + let returnTypeCtx = ctx ::< MkFreeVar (Set 0) (Cnstr Bool) var.val + + (returnSort, returnType) <- inferType returnTypeCtx returnType + trace $ pretty {ann} "result is an index of type" <++> pretty returnType + + trueType <- subst1 (Cnstr True) returnType + trace $ pretty {ann} "checking true branch has type" <++> pretty trueType + true <- check ctx returnSort trueType true + trace "true branch is well typed" + + falseType <- subst1 (Cnstr False) returnType + trace $ pretty {ann} "checking false branch has type" <++> pretty falseType + false <- check ctx returnSort falseType false + trace "false branch is well typed" + + returnType <- subst1 discriminant returnType + returnValue <- doIf discriminant true false + + pure (returnSort ** (returnType, returnValue)) + +infer' ctx Top = do info "encountered top" pure (Set 0 ** (Cnstr (Universe Prop), Cnstr Top)) - Point => do + +infer' ctx Point = do info "encountered point" pure (Prop ** (Cnstr Top, Irrel)) - Bottom => do + +infer' ctx Bottom = do info "encountered bottom" pure (Set 0 ** (Cnstr (Universe Prop), Cnstr Bottom)) - (Absurd t) => fatal "cannot infer type of absurd" - (Equal t u) => do + +infer' ctx (Absurd {contradiction}) = fatal "cannot infer type of absurd" + +infer' ctx (Equal {left, right}) = do 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) + + (sort ** (type, left)) <- infer ctx left + trace $ pretty {ann} "left side has type" <++> pretty type + + right <- check ctx sort type right trace "right side is well typed" - eq <- doEqual (relevance s) a t u - pure (Set 0 ** (Cnstr (Universe Prop), eq)) - (Refl t) => do + + let equalitySort = Prop + equalityType <- doEqual (relevance sort) type left right + + pure (succ equalitySort ** (cast equalitySort, equalityType)) + +infer' ctx (Refl {value}) = do info "encountered refl" - (s ** (a, t)) <- infer ctx (assert_smaller tm t) - trace "argument is well typed" - eq <- doEqual (relevance s) a t t - pure (Prop ** (eq, Irrel)) - (Transp b t u t' e) => do + + (sort ** (type, value)) <- infer ctx value + trace $ pretty {ann} "value has type" <++> pretty type + + equalityType <- doEqual (relevance sort) type value value + + pure (Prop ** (equalityType, Irrel)) + +infer' ctx (Transp {indexedType, oldIndex, value, newIndex, equality}) = 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') + + (indexSort ** (indexType, oldIndex)) <- infer ctx oldIndex + trace $ pretty {ann} "index type is" <++> pretty indexType + + newIndex <- check ctx indexSort indexType newIndex trace "new index is well typed" - b <- check ctx (s ~> Set 0) (Cnstr $ Pi s (Set 0) "" a (Cnstr (Universe 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 (relevance s) a t t' - trace $ pretty {ann} "checking equality has type" <++> pretty eq - e <- check ctx Prop eq (assert_smaller tm e) + + let indexedTypeShape = Cnstr $ Pi indexSort (Set 0) "" indexType (Cnstr (Universe Prop)) + indexedType <- check ctx (indexSort ~> Set 0) indexedTypeShape indexedType + trace $ pretty {ann} "result is an index of type" <++> pretty indexedType + + oldType <- doApp indexedType oldIndex + trace $ pretty {ann} "checking value has type" <++> pretty oldType + Irrel <- check ctx Prop oldType value + trace "value is well typed" + + equalityType <- doEqual (relevance indexSort) indexType oldIndex newIndex + trace $ pretty {ann} "checking equality has type" <++> pretty equalityType + equality <- check ctx Prop equalityType equality trace "equality is well typed" - newB <- doApp b t' - pure (Prop ** (newB, Irrel)) - (Cast a b e t) => do + + returnType <- doApp indexedType newIndex + + pure (Prop ** (returnType, Irrel)) + +infer' ctx (Cast {oldType, newType, equality, value}) = 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 Relevant (cast s) a b - e <- check ctx Prop eq (assert_smaller tm e) + + (sort, oldType) <- inferType ctx oldType + trace $ pretty {ann} "old type is" <++> pretty oldType + + newType <- checkType ctx sort newType + trace $ pretty {ann} "new type is" <++> pretty newType + + equalityType <- doEqual Relevant (cast sort) oldType newType + trace $ pretty {ann} "checking equality has type" <++> pretty equalityType + equality <- check ctx Prop equalityType equality trace "equality is well typed" - t <- check ctx s a (assert_smaller tm t) + + trace $ pretty {ann} "checking value has type" <++> pretty oldType + value <- check ctx sort oldType value trace "value is well typed" - tm <- doCast (relevance s) a b t - pure (s ** (b, tm)) - (CastId t) => do + + returnValue <- doCast (relevance sort) oldType newType value + + pure (sort ** (newType, returnValue)) + +infer' ctx (CastId {value}) = do info "encountered castRefl" - (s ** (a, t)) <- infer ctx (assert_smaller tm t) - trace $ pretty {ann} "argument has type" <++> pretty a - lhs <- doCast (relevance s) a a t - ret <- doEqual (relevance s) a lhs t - pure (Prop ** (ret, Irrel)) + + (sort ** (type, value)) <- infer ctx value + trace $ pretty {ann} "value has type" <++> pretty value + + castRefl <- doCast (relevance sort) type type value + + returnType <- doEqual (relevance sort) type castRefl value + + pure (Prop ** (returnType, Irrel)) -- Checking Definitions and Blocks --------------------------------------------- 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 - 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} +checkDef ctx def = + let block = do + debug $ "inferring type of \{def.name.val}" + (sort, ty) <- + inferType {tag = \lhs, rhs => inScope "invalid declaration" $ mismatch lhs rhs} + (fromContext ctx) def.ty + 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} + + in inBounds $ map (const $ inScope "check" block) def.name export checkBlock : Block n -> Logging ann (ctx ** (Context ctx, length ctx = n)) |