Add postulates.

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))