108 lines
2.4 KiB
Idris
108 lines
2.4 KiB
Idris
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 %inline
|
||
toConst : Dim 0 -> DimConst
|
||
toConst (K e) = e
|
||
|
||
|
||
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
|