module Quox.Syntax.Dim

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

import Decidable.Equality
import Control.Function

%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


export Uninhabited (Zero = One)  where uninhabited _ impossible
export Uninhabited (One  = Zero) where uninhabited _ impossible

export Uninhabited (B i = K e) where uninhabited _ impossible
export Uninhabited (K e = B i) where uninhabited _ impossible

public export %inline Injective B where injective Refl = Refl
public export %inline Injective K where injective Refl = Refl

public export
DecEq DimConst where
  decEq Zero Zero = Yes Refl
  decEq Zero One  = No absurd
  decEq One  Zero = No absurd
  decEq One  One  = Yes Refl

public export
DecEq (Dim d) where
  decEq (K e) (K f) with (decEq e f)
    _ | Yes prf    = Yes $ cong K prf
    _ | No  contra = No  $ contra . injective
  decEq (K e) (B j) = No absurd
  decEq (B i) (K f) = No absurd
  decEq (B i) (B j) with (decEq i j)
    _ | Yes prf    = Yes $ cong B prf
    _ | No  contra = No  $ contra . injective