diff options
Diffstat (limited to 'src/Obs/Typing.idr')
| -rw-r--r-- | src/Obs/Typing.idr | 49 |
1 files changed, 35 insertions, 14 deletions
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr index 8369fe0..e8db1db 100644 --- a/src/Obs/Typing.idr +++ b/src/Obs/Typing.idr @@ -28,18 +28,18 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal -- Checking and Inference ------------------------------------------------------ -check' : (tyCtx : TyContext ctx) +check' : (tyCtx : Context ctx) -> (sort : Universe) -> (type : TypeNormalForm ctx) -> (term : Term (length ctx)) -> Logging ann (NormalForm (relevance sort) ctx) -infer' : (tyCtx : TyContext ctx) +infer' : (tyCtx : Context ctx) -> (term : Term (length ctx)) -> Logging ann (sort : Universe ** (TypeNormalForm ctx, NormalForm (relevance sort) ctx)) inferType' : {default typeMismatch tag : forall a . (expected, actual : Doc ann) -> Logging ann a} - -> (tyCtx : TyContext ctx) + -> (tyCtx : Context ctx) -> (term : Term (length ctx)) -> Logging ann (Universe, TypeNormalForm ctx) inferType' ctx term = do @@ -47,7 +47,7 @@ inferType' ctx term = do | (_ ** (type, term)) => tag (pretty "sort") (pretty type) pure (sort, type) -check : (tyCtx : TyContext ctx) +check : (tyCtx : Context ctx) -> (sort : Universe) -> (type : TypeNormalForm ctx) -> (term : WithBounds (Term (length ctx))) @@ -55,19 +55,19 @@ check : (tyCtx : TyContext ctx) check ctx sort type (MkBounded term irrel bounds) = inBounds (MkBounded (check' ctx sort type term) irrel bounds) -checkType : (tyCtx : TyContext ctx) +checkType : (tyCtx : Context ctx) -> (sort : Universe) -> (term : WithBounds (Term (length ctx))) -> Logging ann (TypeNormalForm ctx) checkType ctx sort term = check ctx (succ sort) (cast sort) term -infer : (tyCtx : TyContext ctx) +infer : (tyCtx : Context ctx) -> (term : WithBounds (Term (length ctx))) -> Logging ann (sort : Universe ** (TypeNormalForm ctx, NormalForm (relevance sort) ctx)) infer ctx (MkBounded term irrel bounds) = inBounds (MkBounded (infer' ctx term) irrel bounds) inferType : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a} - -> (tyCtx : TyContext ctx) + -> (tyCtx : Context ctx) -> (term : WithBounds (Term (length ctx))) -> Logging ann (Universe, TypeNormalForm ctx) inferType ctx (MkBounded term irrel bounds) = @@ -82,7 +82,7 @@ check' ctx sort | No _ => fatal "internal universe mismatch" rewrite functionRelevance domainSort codomainSort - let bodyCtx = ctx ::< MkFreeVar domainSort domain.type var.val + let bodyCtx = ctx ::< MkParameter {sort = domainSort, ty = domain.type, name = var} trace $ pretty {ann} "checking body has type" <++> pretty codomainSort body <- check bodyCtx codomainSort codomain body @@ -202,7 +202,7 @@ infer' ctx (Pi {domain = MkDecl var domain, codomain}) = do (domainSort, domain) <- inferType ctx domain trace $ pretty {ann} "domain type is" <++> pretty domain - let domainVar = MkFreeVar domainSort domain var.val + let domainVar = MkParameter {sort = domainSort, ty = domain, name = var} let codomainCtx = ctx ::< domainVar (codomainSort, codomain) <- inferType codomainCtx codomain @@ -250,7 +250,7 @@ infer' ctx (Sigma {index = MkDecl var index, element}) = do (indexSort, index) <- inferType ctx index trace $ pretty {ann} "index type is" <++> pretty index - let indexVar = MkFreeVar indexSort index var.val + let indexVar = MkParameter {sort = indexSort, ty = index, name = var} let elementCtx = ctx ::< indexVar (elementSort, element) <- inferType elementCtx element @@ -425,7 +425,11 @@ infer' ctx (Sem {pred = MkLambda var pred, arg}) = do let Yes Refl = decEq sort (containerSort container) | No _ => fatal "internal universe mismatch" - let predCtx = ctx ::< MkFreeVar container.outputSort container.output var.val + let predCtx = ctx ::< MkParameter + { sort = container.outputSort + , ty = container.output + , name = var + } (predSort, pred) <- inferType predCtx pred let semSort = container.inputSort ~> max container.shapeSort (container.positionSort ~> predSort) @@ -452,7 +456,7 @@ infer' ctx (If {returnType = MkLambda var returnType, discriminant, true, false} discriminant <- check ctx (Set 0) (Cnstr Bool) discriminant trace "discriminant is well typed" - let returnTypeCtx = ctx ::< MkFreeVar (Set 0) (Cnstr Bool) var.val + let returnTypeCtx = ctx ::< MkParameter {sort = Set 0, ty = Cnstr Bool, name = var} (returnSort, returnType) <- inferType returnTypeCtx returnType trace $ pretty {ann} "result is an index of type" <++> pretty returnType @@ -578,16 +582,29 @@ infer' ctx (CastId {value}) = do -- Checking Definitions and Blocks --------------------------------------------- +checkParam : Context ctx -> Term.Parameter (length ctx) -> Logging ann (NormalForm.Parameter ctx) +checkParam ctx param = + let block = do + debug $ "inferring type of \{param.name.val}" + (sort, ty) <- + inferType {tag = \lhs, rhs => inScope "invalid declaration" $ mismatch lhs rhs} + ctx param.ty + debug $ pretty {ann} "\{param.name.val} has type" <++> pretty ty + + pure $ MkParameter {name = param.name, ty, sort} + + in inBounds $ map (const $ inScope "check" block) param.name + checkDef : Context ctx -> Term.Definition (length ctx) -> Logging ann (NormalForm.Definition ctx) 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 + ctx def.ty debug $ pretty {ann} "\{def.name.val} has type" <++> pretty ty - tm <- check (fromContext ctx) sort ty def.tm + tm <- check 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} @@ -601,3 +618,7 @@ checkBlock (blk :< def) = do (_ ** (ctx, Refl)) <- checkBlock blk def <- checkDef ctx def pure (_ ** (ctx :< def, Refl)) +checkBlock (blk ::< param) = do + (_ ** (ctx, Refl)) <- checkBlock blk + param <- checkParam ctx param + pure (_ ** (ctx ::< param, Refl)) |