quox/lib/Quox/Syntax/DimEq.idr

175 lines
4.3 KiB
Idris

module Quox.Syntax.DimEq
import public Quox.Syntax.Var
import public Quox.Syntax.Dim
import public Quox.Syntax.Subst
import public Quox.Context
import Data.Maybe
import Data.Nat
import Data.DPair
import Data.Fun.Graph
import Decidable.Decidable
import Decidable.Equality
%default total
public export
DimEq' : Nat -> Type
DimEq' = Context (Maybe . Dim)
public export
data DimEq : Nat -> Type where
ZeroIsOne : DimEq d
C : (eqs : DimEq' d) -> DimEq d
%name DimEq eqs
export
zeroEq : DimEq 0
zeroEq = C [<]
export
new' : {d : Nat} -> DimEq' d
new' {d = 0} = [<]
new' {d = S d} = new' :< Nothing
export %inline
new : {d : Nat} -> DimEq d
new = C new'
private %inline
shiftMay : Maybe (Dim from) -> Shift from to -> Maybe (Dim to)
shiftMay p by = map (// by) p
export %inline
get' : DimEq' d -> Var d -> Maybe (Dim d)
get' = getWith shiftMay
private %inline
getShift' : Shift len out -> DimEq' len -> Var len -> Maybe (Dim out)
getShift' = getShiftWith shiftMay
export %inline
get : DimEq' d -> Dim d -> Dim d
get _ (K e) = K e
get eqs (B i) = fromMaybe (B i) $ get' eqs i
export %inline
equal : DimEq d -> (p, q : Dim d) -> Bool
equal ZeroIsOne p q = True
equal (C eqs) p q = get eqs p == get eqs q
infixl 5 :<?
export %inline
(:<?) : DimEq d -> Maybe (Dim d) -> DimEq (S d)
ZeroIsOne :<? d = ZeroIsOne
C eqs :<? d = C $ eqs :< d
private %inline
ifVar : Var d -> Dim d -> Maybe (Dim d) -> Maybe (Dim d)
ifVar i p = map $ \q => if isYes $ q `decEq` B i then p else q
private %inline
checkConst : (e, f : DimConst) -> (eqs : Lazy (DimEq' d)) -> DimEq d
checkConst Zero Zero eqs = C eqs
checkConst One One eqs = C eqs
checkConst _ _ _ = ZeroIsOne
export
setConst : Var d -> DimConst -> DimEq' d -> DimEq d
setConst VZ e (eqs :< Nothing) = C $ eqs :< Just (K e)
setConst VZ e (eqs :< Just (K f)) = checkConst e f $ eqs :< Just (K f)
setConst VZ e (eqs :< Just (B i)) = setConst i e eqs :<? Just (K e)
setConst (VS i) e (eqs :< p) = setConst i e eqs :<? ifVar i (K e) p
mutual
private
setVar' : (i, j : Var d) -> i `LT` j -> DimEq' d -> DimEq d
setVar' VZ (VS i) LTZ (eqs :< Nothing) =
C $ eqs :< Just (B i)
setVar' VZ (VS i) LTZ (eqs :< Just (K e)) =
setConst i e eqs :<? Just (K e)
setVar' VZ (VS i) LTZ (eqs :< Just (B j)) =
setVar i j eqs :<? Just (B (max i j))
setVar' (VS i) (VS j) (LTS lt) (eqs :< p) =
setVar' i j lt eqs :<? ifVar i (B j) p
export %inline
setVar : (i, j : Var d) -> DimEq' d -> DimEq d
setVar i j eqs with (compareP i j)
_ | IsLT lt = setVar' i j lt eqs
setVar i i eqs | IsEQ = C eqs
_ | IsGT gt = setVar' j i gt eqs
export %inline
set : (p, q : Dim d) -> DimEq d -> DimEq d
set _ _ ZeroIsOne = ZeroIsOne
set (K e) (K f) (C eqs) = checkConst e f eqs
set (K e) (B i) (C eqs) = setConst i e eqs
set (B i) (K e) (C eqs) = setConst i e eqs
set (B i) (B j) (C eqs) = setVar i j eqs
public export %inline
Split : Nat -> Type
Split d = (DimEq' d, DSubst (S d) d)
export %inline
split1 : DimConst -> DimEq' (S d) -> Maybe (Split d)
split1 e eqs = case setConst VZ e eqs of
ZeroIsOne => Nothing
C (eqs :< _) => Just (eqs, K e ::: id)
export %inline
split : DimEq' (S d) -> List (Split d)
split eqs = toList (split1 Zero eqs) <+> toList (split1 One eqs)
export
splits' : DimEq' d -> List (DSubst d 0)
splits' [<] = [id]
splits' eqs@(_ :< _) = [th . ph | (eqs', th) <- split eqs, ph <- splits' eqs']
export %inline
splits : DimEq d -> List (DSubst d 0)
splits ZeroIsOne = []
splits (C eqs) = splits' eqs
private
0 newGetShift : (d : Nat) -> (i : Var d) -> (by : Shift d d') ->
getShift' by (new' {d}) i = Nothing
newGetShift (S d) VZ by = Refl
newGetShift (S d) (VS i) by = newGetShift d i (drop1 by)
export
0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' {d}) i = Nothing
newGet' d i = newGetShift d i SZ
export
0 newGet : (d : Nat) -> (p : Dim d) -> get (new' {d}) p = p
newGet d (K e) = Refl
newGet d (B i) = rewrite newGet' d i in Refl
export
0 setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs
setSelf p ZeroIsOne = Refl
setSelf (K Zero) (C eqs) = Refl
setSelf (K One) (C eqs) = Refl
setSelf (B i) (C eqs) = rewrite comparePSelf i in Refl
-- [todo] "well formed" dimeqs
-- [todo] operations maintain well-formedness
-- [todo] if 'Wf eqs' then 'equal eqs' is an equivalence
-- [todo] 'set' never breaks existing equalities