diff options
Diffstat (limited to 'src/Obs/Typing.idr')
| -rw-r--r-- | src/Obs/Typing.idr | 92 |
1 files changed, 46 insertions, 46 deletions
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr index 4cc6d8e..7bb5deb 100644 --- a/src/Obs/Typing.idr +++ b/src/Obs/Typing.idr @@ -9,11 +9,11 @@ import Decidable.Equality import Obs.Logging import Obs.NormalForm import Obs.NormalForm.Normalise -import Obs.Sort import Obs.Substitution import Obs.Term import Obs.Typing.Context import Obs.Typing.Conversion +import Obs.Universe import System @@ -33,44 +33,44 @@ mismatch lhs rhs = fatal $ typeMismatch : Doc ann -> Doc ann -> Logging ann a typeMismatch lhs rhs = inScope "type mismatch" $ mismatch lhs rhs -sortMismatch : Doc ann -> Doc ann -> Logging ann a -sortMismatch lhs rhs = inScope "sort mismatch" $ mismatch lhs rhs +universeMismatch : Doc ann -> Doc ann -> Logging ann a +universeMismatch lhs rhs = inScope "universe mismatch" $ mismatch lhs rhs -- Utilities ------------------------------------------------------------------- -MkPair : (s, s' : Sort) - -> NormalForm (isSet s) ctx - -> NormalForm (isSet s') ctx - -> NormalForm (isSet (max s s')) ctx +MkPair : (s, s' : Universe) + -> NormalForm (relevance s) ctx + -> NormalForm (relevance s') ctx + -> NormalForm (relevance (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 +MkPair Prop s'@(Set _) t u = Cnstr $ Pair Prop s' Set t u +MkPair s@(Set _) s' t u = Cnstr $ Pair s s' Set t u -- Checking and Inference ------------------------------------------------------ check : (tyCtx : TyContext ctx) - -> (s : Sort) - -> NormalForm True ctx + -> (s : Universe) + -> TypeNormalForm ctx -> WithBounds (Term (length ctx)) - -> Logging ann (NormalForm (isSet s) ctx) + -> Logging ann (NormalForm (relevance s) ctx) checkType : (tyCtx : TyContext ctx) - -> (s : Sort) + -> (s : Universe) -> WithBounds (Term (length ctx)) - -> Logging ann (NormalForm True ctx) -checkType ctx s tm = check ctx (suc s) (cast s) tm + -> Logging ann (TypeNormalForm ctx) +checkType ctx s tm = check ctx (succ s) (cast s) tm infer : (tyCtx : TyContext ctx) -> WithBounds (Term (length ctx)) - -> Logging ann (s ** (NormalForm True ctx, NormalForm (isSet s) 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) -> WithBounds (Term (length ctx)) - -> Logging ann (Sort, NormalForm True ctx) + -> Logging ann (Universe, TypeNormalForm ctx) inferType ctx tm = inBounds tm.bounds $ do - (Set _ ** (Cnstr (Sort s), a)) <- infer ctx tm - | (_ ** (a, t)) => tag (pretty "sort") (pretty a) + (Set _ ** (Cnstr (Universe s), a)) <- infer ctx tm + | (_ ** (a, t)) => tag (pretty "universe") (pretty a) pure (s, a) check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of @@ -79,7 +79,7 @@ check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of 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" + | No _ => fatal "internal universe mismatch" pure $ case l' of Prop => Irrel Set _ => Cnstr (Lambda l var.val t) @@ -92,7 +92,7 @@ check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of 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" + | No _ => fatal "internal universe mismatch" pure $ MkPair l l' t u (_, Pair t u) => typeMismatch (pretty "pair type") (pretty ty) (_, Absurd t) => do @@ -108,7 +108,7 @@ check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of | 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' + Just _ <- inScope "convert" $ runMaybeT $ convert (succ s) (cast s) a' b' | Nothing => inScope "conversion failed" $ mismatch (pretty a) (pretty b) pure t @@ -117,16 +117,16 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of 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)) + (Universe s) => do + info $ pretty {ann} "encountered universe" <++> pretty tm.val + pure (succ (succ s) ** (cast (succ s), cast s)) (Pi var a b) => 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 (suc (s ~> s') ** (cast (s ~> s'), Cnstr (Pi s s' var.val a 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 info "encountered application" @@ -137,17 +137,17 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of 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" + | No _ => fatal "internal universe mismatch" ty <- subst1 u b tm <- doApp t u - pure (l' ** (ty, rewrite sym $ impredicative l l' in tm)) + pure (l' ** (ty, rewrite sym $ functionRelevance l l' in tm)) (Sigma var a b) => 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 (suc (max s s') ** (cast (max s s'), Cnstr (Sigma s s' var.val a 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 info "encountered first" @@ -155,9 +155,9 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of | (_ ** (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" + | No _ => fatal "internal universe mismatch" let ty = a - tm <- doFst (isSet l) (isSet l') (rewrite sym $ maxIsSet l l' in t) + tm <- doFst (relevance l) (relevance l') (rewrite sym $ pairRelevance l l' in t) pure (l ** (ty, tm)) (Snd t) => do info "encountered second" @@ -165,11 +165,11 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of | (_ ** (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 + | 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 (isSet l) (isSet l') t + tm <- doSnd (relevance l) (relevance l') t pure (l' ** (ty, tm)) Bool => do info "encountered bool" @@ -197,13 +197,13 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of pure (s ** (ty, tm)) Top => do info "encountered top" - pure (Set 0 ** (cast Prop, Cnstr Top)) + pure (Set 0 ** (Cnstr (Universe 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)) + pure (Set 0 ** (Cnstr (Universe Prop), Cnstr Bottom)) (Absurd t) => fatal "cannot infer type of absurd" (Equal t u) => do info "encountered equal" @@ -211,13 +211,13 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of 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)) + eq <- doEqual (relevance s) a t u + pure (Set 0 ** (Cnstr (Universe Prop), eq)) (Refl t) => do info "encountered refl" (s ** (a, t)) <- infer ctx (assert_smaller tm t) trace "argument is well typed" - eq <- doEqual (isSet s) a t t + eq <- doEqual (relevance s) a t t pure (Prop ** (eq, Irrel)) (Transp b t u t' e) => do info "encountered transp" @@ -225,12 +225,12 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of 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) + 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 (isSet s) a t t' + 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) trace "equality is well typed" @@ -242,19 +242,19 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of 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 + eq <- doEqual Relevant (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 + tm <- doCast (relevance s) a b t pure (s ** (b, tm)) (CastId t) => do 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 + lhs <- doCast (relevance s) a a t + ret <- doEqual (relevance s) a lhs t pure (Prop ** (ret, Irrel)) -- Checking Definitions and Blocks --------------------------------------------- |