module Quox.Syntax.Dim

import Quox.Syntax.Var
import Quox.Syntax.Subst
import Quox.Pretty

%default total


public export
data DimConst = Zero | One
%name DimConst e

private DCRepr : Type
DCRepr = Nat

private %inline dcrepr : DimConst -> DCRepr
dcrepr e = case e of Zero => 0; One => 1

export Eq  DimConst where (==) = (==) `on` dcrepr
export Ord DimConst where compare = compare `on` dcrepr


public export
data Dim : Nat -> Type where
  K : DimConst -> Dim d
  B : Var d -> Dim d
%name Dim.Dim p, q

private DRepr : Type
DRepr = Nat

private %inline drepr : Dim n -> DRepr
drepr p = case p of K i => dcrepr i; B i => 2 + i.nat

export Eq  (Dim n) where (==) = (==) `on` drepr
export Ord (Dim n) where compare = compare `on` drepr

export
PrettyHL DimConst where
  prettyM Zero = hl Dim <$> ifUnicode "𝟬" "0"
  prettyM One  = hl Dim <$> ifUnicode "𝟭" "1"

export
PrettyHL (Dim n) where
  prettyM (K e) = prettyM e
  prettyM (B i) = prettyVar DVar DVarErr (!ask).dnames i


public export
DSubst : Nat -> Nat -> Type
DSubst = Subst Dim


export %inline
prettyDSubst : Pretty.HasEnv m => DSubst from to -> m (Doc HL)
prettyDSubst th =
  prettySubstM prettyM (!ask).dnames DVar
    !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th


export FromVar Dim where fromVar = B

export
CanShift Dim where
  K e // _  = K e
  B i // by = B (i // by)

export
CanSubst Dim Dim where
  K e // _  = K e
  B i // th = th !! i