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 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
  sort : Universe
  ty : TypeNormalForm ctx
  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 [] = []
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
  }

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
  , 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
  (relevance def.sort :: ctx' ** cong (relevance def.sort ::) prf)
getContext (ctx ::< var) =
  let (ctx' ** prf) = getContext ctx in
  (relevance var.sort :: ctx' ** cong (relevance 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 (Just var.name) Here)
  (\i => pure $ weaken [_] $ !(reduce ctx i))