Add postulates.

7 files changed, 118 insertions, 58 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 25c4210..16b0c92 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -132,6 +132,12 @@ abstractSyntaxBounds ctx val@(MkBounded v irrel bnds) = do
   term <- inBounds $ (MkBounded (abstractSyntax ctx v) irrel bnds)
   pure $ map (const term) val
 
+abstractParameter : Context n -> Parameter -> Logging ann (Parameter n)
+abstractParameter ctx param = pure $ MkParameter
+  { name = param.name
+  , ty = !(abstractSyntaxBounds ctx param.ty)
+  }
+
 abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
 abstractDefinition ctx def = pure $ MkDefinition
   { name = def.name
@@ -140,14 +146,20 @@ abstractDefinition ctx def = pure $ MkDefinition
   }
 
 export
-abstractBlock : (defs : List Definition) -> Logging ann (Block (length defs))
+abstractBlock : (defs : List (Either Parameter Definition)) -> Logging ann (Block (length defs))
 abstractBlock defs =
   let asContext : Block n -> Context n
       asContext []            = []
-      asContext (defs :< def) = bind (asContext defs) def.name.val
-  in let helper : Block n -> (defs : List Definition) -> Logging ann (Block (length defs + n))
+      asContext (blk :< def) = bind (asContext blk) def.name.val
+      asContext (blk ::< param) = bind (asContext blk) param.name.val
+  in let helper : Block n ->
+           (defs : List (Either Parameter Definition)) ->
+           Logging ann (Block (length defs + n))
          helper blk []            = pure blk
-         helper blk (def :: defs) = do
+         helper blk (Left param :: defs) = do
+           param <- abstractParameter (asContext blk) param
+           (rewrite plusSuccRightSucc (length defs) n in helper (blk ::< param) defs)
+         helper blk (Right def :: defs) = do
            def <- abstractDefinition (asContext blk) def
            (rewrite plusSuccRightSucc (length defs) n in helper (blk :< def) defs)
   in rewrite sym $ plusZeroRightNeutral (length defs) in helper [] defs
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index b4b9f94..d325f1a 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -87,6 +87,13 @@ data NormalForm : Sorted.Family Relevance where
 %name NormalForm t, u, v
 
 public export
+record Parameter (ctx : List Relevance) where
+  constructor MkParameter
+  name : WithBounds String
+  sort : Universe
+  ty : TypeNormalForm ctx
+
+public export
 record Definition (ctx : List Relevance) where
   constructor MkDefinition
   name : WithBounds String
@@ -98,6 +105,7 @@ public export
 data Context : List Relevance -> Type where
   Nil  : Context []
   (:<) : Context ctx -> (def : Definition ctx) -> Context (relevance def.sort :: ctx)
+  (::<) : Context ctx -> (param : Parameter ctx) -> Context (relevance param.sort :: ctx)
 
 %name Context ctx, ctx', ctx''
 
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index d0a9fb8..c1bd468 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -61,6 +61,7 @@ data ObsTokenKind
   | OTAOpen
   | OTAClose
   -- Other Symbols
+  | OTPostulate
   | OTComma
   | OTTilde
   | OTEqual
@@ -111,6 +112,7 @@ Eq ObsTokenKind where
   OTAOpen == OTAOpen = True
   OTAClose == OTAClose = True
 
+  OTPostulate == OTPostulate = True
   OTComma == OTComma = True
   OTTilde == OTTilde = True
   OTEqual == OTEqual = True
@@ -163,6 +165,7 @@ Show ObsTokenKind where
   show OTAOpen = "<"
   show OTAClose = ">"
 
+  show OTPostulate = "postulate"
   show OTComma = ","
   show OTTilde = "~"
   show OTEqual = "="
@@ -217,6 +220,7 @@ TokenKind ObsTokenKind where
   tokValue OTAOpen s = ()
   tokValue OTAClose s = ()
 
+  tokValue OTPostulate s = ()
   tokValue OTComma s = ()
   tokValue OTTilde s = ()
   tokValue OTEqual s = ()
@@ -261,6 +265,8 @@ keywords =
   , ("if", OTIf)
 
   , ("Container", OTContainer)
+
+  , ("postulate", OTPostulate)
   ]
 
 obsTokenMap : TokenMap ObsToken
@@ -453,20 +459,24 @@ def : Grammar state ObsToken True (WithBounds String, WithBounds Syntax)
 def = [| MkPair (ident <* whitespace <* match' OTEqual <* whitespace) exp |]
 
 partial
+param : Grammar state ObsToken True Parameter
+param = map (\(MkDecl name ty) => MkParameter {name, ty}) $
+  match OTPostulate *> commit *> whitespace *> decl exp
+
+partial
 fullDef : Grammar state ObsToken True Definition
 fullDef =
   seq
     [| MkPair (decl exp <* commit) (optional whitespace *> match' OTNewlines *> def <* commit) |]
     (\((MkDecl name ty), (name', tm)) =>
       if name.val == name'.val
-        then pure (MkDefinition {name = name, ty, tm})
+        then pure (MkDefinition {name, ty, tm})
         else fatalLoc name.bounds "name mismatch' for declaration and definition")
 
 partial
-file : Grammar state ObsToken False (List Definition)
-file =
-  optional (whitespace *> match' OTNewlines) *>
-  sepEndBy (optional whitespace *> match' OTNewlines) (fullDef <* commit)
+file : Grammar state ObsToken False (List (Either Parameter Definition))
+file = many (whitespace *> match' OTNewlines) *>
+  sepEndBy (optional whitespace *> match' OTNewlines) (choose param fullDef <* commit)
 
 whitespaceIrrelevant : WithBounds ObsToken -> WithBounds ObsToken
 whitespaceIrrelevant a = case (a.val.kind) of
@@ -495,7 +505,7 @@ castErr (Left errs) = do
 
 partial
 export
-parse : String -> Logging ann (List Definition)
+parse : String -> Logging ann (List (Either Parameter Definition))
 parse str = do
   let (toks, _, _, "") = lex obsTokenMap str
     | (toks, l, c, rem) => inScope "lex" $ do
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 868e761..ea7772e 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -72,6 +72,12 @@ record Definition where
   ty     : WithBounds Syntax
   tm     : WithBounds Syntax
 
+public export
+record Parameter where
+  constructor MkParameter
+  name : WithBounds String
+  ty : WithBounds Syntax
+
 -- Pretty Print ----------------------------------------------------------------
 
 prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
@@ -159,3 +165,8 @@ Pretty Definition where
   pretty def = group $
     pretty def.name.val <++> colon <+> softline <+> pretty def.ty.val <+> hardline <+>
     pretty def.name.val <++> equals <+> softline <+> pretty def.tm.val
+
+export
+Pretty Parameter where
+  pretty param = group $
+    pretty "parameter" <++> pretty param.name.val <++> colon <+> softline <+> pretty param.ty.val
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 5126d99..8829038 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,6 +12,8 @@ import Text.Bounded
 
 -- Definition ------------------------------------------------------------------
 
+infix 5 ::<
+
 data Term : Nat -> Type
 
 public export
@@ -74,6 +76,12 @@ data Term : Nat -> Type where
   CastId : (value : WithBounds (Term n)) -> Term n
 
 public export
+record Parameter (n : Nat) where
+  constructor MkParameter
+  name : WithBounds String
+  ty : WithBounds (Term n)
+
+public export
 record Definition (n : Nat) where
   constructor MkDefinition
   name : WithBounds String
@@ -84,6 +92,7 @@ public export
 data Block : Nat -> Type where
   Nil  : Block 0
   (:<) : Block n -> Definition n -> Block (S n)
+  (::<) : Block n -> Parameter n -> Block (S n)
 
 -- Pretty Print ----------------------------------------------------------------
 
@@ -168,6 +177,11 @@ Pretty (Term n) where
   prettyPrec = Term.prettyPrec
 
 export
+Pretty (Parameter n) where
+  pretty param = group $
+    pretty "parameter" <++> pretty param.name.val <++> colon <+> softline <+> pretty param.ty.val
+
+export
 Pretty (Definition n) where
   pretty def = group $
     pretty def.name.val <++> colon <+> softline <+> pretty def.ty.val <+> hardline <+>
@@ -177,4 +191,6 @@ export
 Pretty (Block n) where
   pretty []           = neutral
   pretty ([] :< def)  = pretty def
+  pretty ([] ::< param)  = pretty param
   pretty (blk :< def) = pretty blk <+> hardline <+> hardline <+> pretty def
+  pretty (blk ::< param) = pretty blk <+> hardline <+> hardline <+> pretty param
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))
diff --git a/src/Obs/Typing/Context.idr b/src/Obs/Typing/Context.idr
index ad1d0a7..a630fcb 100644
--- a/src/Obs/Typing/Context.idr
+++ b/src/Obs/Typing/Context.idr
@@ -17,13 +17,6 @@ import Text.Bounded
 infix 5 ::<
 
 public export
-record FreeVar (ctx : List Relevance) where
-  constructor MkFreeVar
-  sort : Universe
-  ty : TypeNormalForm ctx
-  name : String
-
-public export
 record TyDef (b : Relevance) (ctx : List Relevance) where
   constructor MkDefinition
   name : String
@@ -32,15 +25,9 @@ record TyDef (b : Relevance) (ctx : List Relevance) where
   tm : NormalForm (relevance sort) ctx
   correct : relevance sort = b
 
-public export
-data TyContext : Unsorted.Family Relevance where
-  Nil   : TyContext []
-  (:<)  : TyContext ctx -> (def : Definition ctx) -> TyContext (relevance def.sort :: ctx)
-  (::<) : TyContext ctx -> (var : FreeVar ctx) -> TyContext (relevance var.sort :: ctx)
-
 -- Properties ------------------------------------------------------------------
 
-freeVars : TyContext ctx -> List Relevance
+freeVars : Context ctx -> List Relevance
 freeVars [] = []
 freeVars (ctx :< def) = freeVars ctx
 freeVars (ctx ::< var) = relevance var.sort :: freeVars ctx
@@ -59,50 +46,45 @@ fromDef def = MkDefinition
   , correct = Refl
   }
 
-fromVar : (var : FreeVar ctx) -> TyDef (relevance var.sort) (relevance var.sort :: ctx)
-fromVar var = MkDefinition
-  { name = var.name
-  , sort = var.sort
-  , ty = weaken [relevance var.sort] var.ty
-  , tm = point (Just var.name) Here
+fromParam : (param : Parameter ctx) -> TyDef (relevance param.sort) (relevance param.sort :: ctx)
+fromParam param = MkDefinition
+  { name = param.name.val
+  , sort = param.sort
+  , ty = weaken [relevance param.sort] param.ty
+  , tm = point (Just param.name.val) Here
   , correct = Refl
   }
 
-export
-fromContext : Context ctx -> TyContext ctx
-fromContext []           = []
-fromContext (ctx :< def) = fromContext ctx :< def
-
 -- Destruction -----------------------------------------------------------------
 
 export
-getContext : TyContext ctx -> (ctx' ** ctx = ctx')
+getContext : Context ctx -> (ctx' ** ctx = ctx')
 getContext [] = ([] ** Refl)
 getContext (ctx :< def) =
   let (ctx' ** prf) = getContext ctx in
   (relevance def.sort :: ctx' ** cong (relevance def.sort ::) prf)
-getContext (ctx ::< var) =
+getContext (ctx ::< param) =
   let (ctx' ** prf) = getContext ctx in
-  (relevance var.sort :: ctx' ** cong (relevance var.sort ::) prf)
+  (relevance param.sort :: ctx' ** cong (relevance param.sort ::) prf)
 
 export
-index : TyContext ctx -> Map ctx TyDef ctx
+index : Context ctx -> Map ctx TyDef ctx
 index [] = absurd
 index (ctx :< def) = weaken [_] . add TyDef (fromDef def) (index ctx)
-index (ctx ::< var) = add TyDef (fromVar var) (weaken [_] . index ctx)
+index (ctx ::< param) = add TyDef (fromParam param) (weaken [_] . index ctx)
 
 finToElem : {xs : List a} -> (i : Fin (length xs)) -> Elem (index' xs i) xs
 finToElem {xs = (x :: xs)} FZ = Here
 finToElem {xs = (x :: xs)} (FS i) = There (finToElem i)
 
 export
-index' : TyContext ctx -> (i : Fin (length ctx)) -> TyDef (index' ctx i) ctx
+index' : Context ctx -> (i : Fin (length ctx)) -> TyDef (index' ctx i) ctx
 index' ctx i = let (ctx' ** Refl) = getContext ctx in index ctx (finToElem i)
 
 export
-reduce : (tyCtx : TyContext ctx) -> Map ctx (LogNormalForm ann) (freeVars tyCtx)
+reduce : (tyCtx : Context ctx) -> Map ctx (LogNormalForm ann) (freeVars tyCtx)
 reduce [] = absurd
 reduce (ctx :< def) = add (LogNormalForm ann) (subst def.tm (reduce ctx)) (reduce ctx)
-reduce (ctx ::< var) = add (LogNormalForm ann)
-  (pure $ point (Just var.name) Here)
+reduce (ctx ::< param) = add (LogNormalForm ann)
+  (pure $ point (Just param.name.val) Here)
   (\i => pure $ weaken [_] $ !(reduce ctx i))