Index normal forms with relevance.

- Remove container types.
- Replace sum types with booleans.
- Remove type annotation from absurd.
- Add original type as argument to cast.
- Make if (was case) take a lambda for the return type.

1 files changed, 108 insertions, 0 deletions

diff --git a/src/Obs/Typing/Context.idr b/src/Obs/Typing/Context.idr
new file mode 100644
index 0000000..636c9f2
--- /dev/null
+++ b/src/Obs/Typing/Context.idr
@@ -0,0 +1,108 @@
+module Obs.Typing.Context
+
+import Data.Fin
+import public Data.List
+import Data.List.Elem
+
+import Obs.Logging
+import Obs.NormalForm
+import Obs.NormalForm.Normalise
+import Obs.Substitution
+import Obs.Sort
+
+import Text.Bounded
+
+-- Definitions -----------------------------------------------------------------
+
+infix 5 ::<
+
+public export
+record FreeVar (ctx : List Bool) where
+  constructor MkFreeVar
+  sort : Sort
+  ty : NormalForm True ctx
+  name : String
+
+public export
+record TyDef (b : Bool) (ctx : List Bool) where
+  constructor MkDefinition
+  name : String
+  sort : Sort
+  ty : NormalForm True ctx
+  tm : NormalForm (isSet sort) ctx
+  correct : isSet sort = b
+
+public export
+data TyContext : Unsorted.Family Bool where
+  Nil   : TyContext []
+  (:<)  : TyContext ctx -> (def : Definition ctx) -> TyContext (isSet def.sort :: ctx)
+  (::<) : TyContext ctx -> (var : FreeVar ctx) -> TyContext (isSet var.sort :: ctx)
+
+-- Properties ------------------------------------------------------------------
+
+freeVars : TyContext ctx -> List Bool
+freeVars [] = []
+freeVars (ctx :< def) = freeVars ctx
+freeVars (ctx ::< var) = isSet var.sort :: freeVars ctx
+
+Sorted.Rename Bool TyDef where
+  rename def f = {ty := rename def.ty f, tm := rename def.tm f} def
+
+-- Construction ----------------------------------------------------------------
+
+fromDef : (def : Definition ctx) -> TyDef (isSet def.sort) ctx
+fromDef def = MkDefinition
+  { name = def.name.val
+  , sort = def.sort
+  , ty = def.ty
+  , tm = def.tm
+  , correct = Refl
+  }
+
+fromVar : (var : FreeVar ctx) -> TyDef (isSet var.sort) (isSet var.sort :: ctx)
+fromVar var = MkDefinition
+  { name = var.name
+  , sort = var.sort
+  , ty = weaken [isSet var.sort] var.ty
+  , tm = point (var.name, (var.sort ** Refl)) 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 [] = ([] ** Refl)
+getContext (ctx :< def) =
+  let (ctx' ** prf) = getContext ctx in
+  (isSet def.sort :: ctx' ** cong (isSet def.sort ::) prf)
+getContext (ctx ::< var) =
+  let (ctx' ** prf) = getContext ctx in
+  (isSet var.sort :: ctx' ** cong (isSet var.sort ::) prf)
+
+export
+index : TyContext 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)
+
+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' ctx i = let (ctx' ** Refl) = getContext ctx in index ctx (finToElem i)
+
+export
+reduce : (tyCtx : TyContext 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 (var.name, (var.sort ** Refl)) Here)
+  (\i => pure $ weaken [_] $ !(reduce ctx i))