rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

add %inlines

Browse source
This commit is contained in:
rhiannon morris 2022-02-27 01:30:23 +01:00
parent bc3230e000
commit d52d1c3181
1 changed files with 10 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/Quox/Syntax/DimEq.idr
View file

@ -30,7 +30,7 @@ new' : (d : Nat) -> DimEq' d
new' 0 = [<] new' 0 = [<]
new' (S d) = new' d :< Nothing new' (S d) = new' d :< Nothing
export export %inline
new : (d : Nat) -> DimEq d new : (d : Nat) -> DimEq d
new d = C (new' d) new d = C (new' d)
@ -40,14 +40,15 @@ get : DimEq' d -> Dim d -> Dim d
get _ (K e) = K e get _ (K e) = K e
get eqs (B i) = fromMaybe (B i) $ (eqs !! i) @{Compose} get eqs (B i) = fromMaybe (B i) $ (eqs !! i) @{Compose}
export
export %inline
equal : DimEq d -> (p, q : Dim d) -> Bool equal : DimEq d -> (p, q : Dim d) -> Bool
equal ZeroIsOne p q = True equal ZeroIsOne p q = True
equal (C eqs) p q = get eqs p == get eqs q equal (C eqs) p q = get eqs p == get eqs q
infixl 5 :<? infixl 5 :<?
export export %inline
(:<?) : DimEq d -> Maybe (Dim d) -> DimEq (S d) (:<?) : DimEq d -> Maybe (Dim d) -> DimEq (S d)
ZeroIsOne :<? d = ZeroIsOne ZeroIsOne :<? d = ZeroIsOne
C eqs :<? d = C $ eqs :< d C eqs :<? d = C $ eqs :< d
@ -82,7 +83,7 @@ mutual
setVar' (VS i) (VS j) (LTS lt) (eqs :< p) = setVar' (VS i) (VS j) (LTS lt) (eqs :< p) =
setVar' i j lt eqs :<? ifVar i (B j) p setVar' i j lt eqs :<? ifVar i (B j) p
export export %inline
setVar : (i, j : Var d) -> DimEq' d -> DimEq d setVar : (i, j : Var d) -> DimEq' d -> DimEq d
setVar i j eqs with (compareP i j) setVar i j eqs with (compareP i j)
_ | IsLT lt = setVar' i j lt eqs _ | IsLT lt = setVar' i j lt eqs
@ -90,7 +91,7 @@ mutual
_ | IsGT gt = setVar' j i gt eqs _ | IsGT gt = setVar' j i gt eqs
export export %inline
set : (p, q : Dim d) -> DimEq d -> DimEq d set : (p, q : Dim d) -> DimEq d -> DimEq d
set _ _ ZeroIsOne = ZeroIsOne set _ _ ZeroIsOne = ZeroIsOne
set (K e) (K f) (C eqs) = checkConst e f eqs set (K e) (K f) (C eqs) = checkConst e f eqs
@ -111,17 +112,17 @@ setSelf (B i) (C eqs) with (compareP i i)
public export public export %inline
Split : Nat -> Type Split : Nat -> Type
Split d = (DimEq' d, DSubst (S d) d) Split d = (DimEq' d, DSubst (S d) d)
export export %inline
split1 : DimConst -> DimEq' (S d) -> Maybe (Split d) split1 : DimConst -> DimEq' (S d) -> Maybe (Split d)
split1 e eqs = case setConst VZ e eqs of split1 e eqs = case setConst VZ e eqs of
ZeroIsOne => Nothing ZeroIsOne => Nothing
C (eqs :< _) => Just (eqs, K e ::: id) C (eqs :< _) => Just (eqs, K e ::: id)
export export %inline
split : DimEq' (S d) -> List (Split d) split : DimEq' (S d) -> List (Split d)
split eqs = toList (split1 Zero eqs) <+> toList (split1 One eqs) split eqs = toList (split1 Zero eqs) <+> toList (split1 One eqs)
@ -131,7 +132,7 @@ splits' : DimEq' d -> List (DSubst d 0)
splits' [<] = [id] splits' [<] = [id]
splits' eqs@(_ :< _) = [th . ph | (eqs', th) <- split eqs, ph <- splits' eqs'] splits' eqs@(_ :< _) = [th . ph | (eqs', th) <- split eqs, ph <- splits' eqs']
export export %inline
splits : DimEq d -> List (DSubst d 0) splits : DimEq d -> List (DSubst d 0)
splits ZeroIsOne = [] splits ZeroIsOne = []
splits (C eqs) = splits' eqs splits (C eqs) = splits' eqs