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.Universe

import Text.Bounded

-- Definitions -----------------------------------------------------------------

infix 5 ::<

public export
record TyDef (b : Relevance) (ctx : List Relevance) where
  constructor MkDefinition
  name : String
  sort : Universe
  ty : TypeNormalForm ctx
  tm : NormalForm (relevance sort) ctx
  correct : relevance sort = b

-- Properties ------------------------------------------------------------------

freeVars : Context ctx -> List Relevance
freeVars [] = []
freeVars (ctx :< def) = freeVars ctx
freeVars (ctx ::< var) = relevance var.sort :: freeVars ctx

Sorted.Rename Relevance TyDef where
  rename def f = {ty := rename def.ty f, tm := rename def.tm f} def

-- Construction ----------------------------------------------------------------

fromDef : (def : Definition ctx) -> TyDef (relevance def.sort) ctx
fromDef def = MkDefinition
  { name = def.name.val
  , sort = def.sort
  , ty = def.ty
  , tm = def.tm
  , correct = Refl
  }

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
  }

-- Destruction -----------------------------------------------------------------

export
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 ::< param) =
  let (ctx' ** prf) = getContext ctx in
  (relevance param.sort :: ctx' ** cong (relevance param.sort ::) prf)

export
index : Context ctx -> Map ctx TyDef ctx
index [] = absurd
index (ctx :< def) = weaken [_] . add TyDef (fromDef def) (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' : 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 : 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 ::< param) = add (LogNormalForm ann)
  (pure $ point (Just param.name.val) Here)
  (\i => pure $ weaken [_] $ !(reduce ctx i))