quox/lib/Quox/Typing/Context.idr

module Quox.Typing.Context

import Quox.Syntax
import Quox.Context
import Quox.Pretty
import public Data.Singleton

%default total


public export
QContext : Type -> Nat -> Type
QContext = Context'

public export
TContext : Type -> Nat -> Nat -> Type
TContext q d = Context (Term q d)

public export
QOutput : Type -> Nat -> Type
QOutput = Context'

public export
DimAssign : Nat -> Type
DimAssign = Context' DimConst


public export
record TyContext q d n where
  constructor MkTyContext
  {auto dimLen  : Singleton d}
  {auto termLen : Singleton n}
  dctx   : DimEq d
  dnames : NContext d
  tctx   : TContext q d n
  tnames : NContext n
  qtys   : QContext q n -- only used for printing
%name TyContext ctx


public export
record EqContext q n where
  constructor MkEqContext
  {dimLen : Nat}
  {auto termLen : Singleton n}
  dassign : DimAssign dimLen -- only used for printing
  dnames  : NContext dimLen -- only used for printing
  tctx    : TContext q 0 n
  tnames  : NContext n
  qtys    : QContext q n -- only used for printing
%name EqContext ctx


namespace TContext
  export %inline
  pushD : TContext q d n -> TContext q (S d) n
  pushD tel = map (// shift 1) tel

  export %inline
  zeroFor : IsQty q => Context tm n -> QOutput q n
  zeroFor ctx = zero <$ ctx

private
extendLen : Telescope a from to -> Singleton from -> Singleton to
extendLen [<]        x = x
extendLen (tel :< _) x = [|S $ extendLen tel x|]

namespace TyContext
  public export %inline
  empty : TyContext q 0 0
  empty =
    MkTyContext {dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<]}

  public export %inline
  null : TyContext q d n -> Bool
  null ctx = null ctx.dnames && null ctx.tnames

  export %inline
  extendTyN : Telescope (\n => (q, BaseName, Term q d n)) from to ->
              TyContext q d from -> TyContext q d to
  extendTyN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
    let (qs, xs, ss) = unzip3 xss in
    MkTyContext {
      dctx, dnames,
      termLen = extendLen xss termLen,
      tctx    = tctx . ss,
      tnames  = tnames . xs,
      qtys    = qtys . qs
    }

  export %inline
  extendTy : q -> BaseName -> Term q d n -> TyContext q d n ->
             TyContext q d (S n)
  extendTy q x s = extendTyN [< (q, x, s)]

  export %inline
  extendDim : BaseName -> TyContext q d n -> TyContext q (S d) n
  extendDim x (MkTyContext {dimLen, dctx, dnames, tctx, tnames, qtys}) =
    MkTyContext {
      dctx   = dctx :<? Nothing,
      dnames = dnames :< x,
      dimLen = [|S dimLen|],
      tctx   = pushD tctx,
      tnames, qtys
    }

  export %inline
  eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n
  eqDim p q = {dctx $= set p q, dimLen $= id, termLen $= id}

  export
  injectT : TyContext q d n -> Term q 0 0 -> Term q d n
  injectT (MkTyContext {dimLen = Val d, termLen = Val n, _}) tm =
    tm // shift0 d // shift0 n

  export
  injectE : TyContext q d n -> Elim q 0 0 -> Elim q d n
  injectE (MkTyContext {dimLen = Val d, termLen = Val n, _}) el =
    el // shift0 d // shift0 n


namespace QOutput
  parameters {auto _ : IsQty q}
    export %inline
    (+) : QOutput q n -> QOutput q n -> QOutput q n
    (+) = zipWith (+)

    export %inline
    (*) : q -> QOutput q n -> QOutput q n
    (*) pi = map (pi *)

    export %inline
    zeroFor : TyContext q _ n -> QOutput q n
    zeroFor ctx = zeroFor ctx.tctx


export
makeDAssign : DSubst d 0 -> DimAssign d
makeDAssign (Shift SZ)   = [<]
makeDAssign (K e ::: th) = makeDAssign th :< e

export
makeEqContext' : {d : Nat} -> TyContext q d n -> DSubst d 0 -> EqContext q n
makeEqContext' ctx th = MkEqContext {
  termLen = ctx.termLen,
  dassign = makeDAssign th,
  dnames  = ctx.dnames,
  tctx    = map (// th) ctx.tctx,
  tnames  = ctx.tnames,
  qtys    = ctx.qtys
}

export
makeEqContext : TyContext q d n -> DSubst d 0 -> EqContext q n
makeEqContext ctx@(MkTyContext {dnames, _}) th =
  let (d' ** Refl) = lengthPrf0 dnames in makeEqContext' ctx th

namespace EqContext
  public export %inline
  empty : EqContext q 0
  empty = MkEqContext {
    dassign = [<], dnames = [<], tctx = [<], tnames = [<], qtys = [<]
  }

  public export %inline
  null : EqContext q n -> Bool
  null ctx = null ctx.dnames && null ctx.tnames

  export %inline
  extendTyN : Telescope (\n => (q, BaseName, Term q 0 n)) from to ->
              EqContext q from -> EqContext q to
  extendTyN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
    let (qs, xs, ss) = unzip3 xss in
    MkEqContext {
      termLen = extendLen xss termLen,
      tctx    = tctx . ss,
      tnames  = tnames . xs,
      qtys    = qtys . qs,
      dassign, dnames
    }

  export %inline
  extendTy : q -> BaseName -> Term q 0 n -> EqContext q n -> EqContext q (S n)
  extendTy q x s = extendTyN [< (q, x, s)]

  export %inline
  extendDim : BaseName -> DimConst -> EqContext q n -> EqContext q n
  extendDim x e (MkEqContext {dassign, dnames, tctx, tnames, qtys}) =
    MkEqContext {dassign = dassign :< e, dnames = dnames :< x,
                 tctx, tnames, qtys}

  export
  toTyContext : (e : EqContext q n) -> TyContext q e.dimLen n
  toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
    MkTyContext {
      dctx = fromGround dassign,
      tctx = map (// shift0 dimLen) tctx,
      dnames, tnames, qtys
    }

  export
  injectT : EqContext q n -> Term q 0 0 -> Term q 0 n
  injectT (MkEqContext {termLen = Val n, _}) tm = tm // shift0 n

  export
  injectE : EqContext q n -> Elim q 0 0 -> Elim q 0 n
  injectE (MkEqContext {termLen = Val n, _}) el = el // shift0 n


private
data CtxBinder a = MkCtxBinder BaseName a

PrettyHL a => PrettyHL (CtxBinder a) where
  prettyM (MkCtxBinder x t) = pure $
    sep [hsep [!(pretty0M $ TV x), colonD], !(pretty0M t)]

parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
  private
  pipeD : Doc HL
  pipeD = hl Syntax "|"

  export covering
  prettyTContext : QContext q n -> NContext n -> TContext q d n -> Doc HL
  prettyTContext qs ns ctx = separate comma $ toList $ go qs ns ctx where
    go : QContext q m -> NContext m -> TContext q d m -> SnocList (Doc HL)
    go [<]       [<]       [<] = [<]
    go (qs :< q) (xs :< x) (ctx :< t) =
      let bind = MkWithQty q $ MkCtxBinder x t in
      go qs xs ctx :< runPretty unicode (pretty0M bind)

  export covering
  prettyTyContext : TyContext q d n -> Doc HL
  prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
    case dctx of
      C [<] => prettyTContext qtys tnames tctx
      _     => sep [prettyDimEq dnames dctx <++> pipeD,
                    prettyTContext qtys tnames tctx]

  export covering
  prettyEqContext : EqContext q n -> Doc HL
  prettyEqContext (MkEqContext dassign dnames tctx tnames qtys) =
    case dassign of
      [<] => prettyTContext qtys tnames tctx
      _   => sep [prettyDimEq dnames (fromGround dassign) <++> pipeD,
                  prettyTContext qtys tnames tctx]