From eb49ef28b93431d9694a17b1ad44d9ea966bcb05 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 7 Jan 2023 22:01:05 +0000
Subject: Add postulates.

---
 src/Obs/Typing/Context.idr | 50 +++++++++++++++-------------------------------
 1 file changed, 16 insertions(+), 34 deletions(-)

(limited to 'src/Obs/Typing/Context.idr')

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
@@ -16,13 +16,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
@@ -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))
-- 
cgit v1.2.3