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

remove Loc suffix from fromVar and Context.get

Browse source
This commit is contained in:
rhiannon morris 2024-05-05 19:44:27 +02:00
parent d9a383d8bb
commit e880b7165a
5 changed files with 16 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
lib/Quox/Syntax/Dim.idr
View file

@ -84,7 +84,7 @@ DSubst : Nat -> Nat -> Type
DSubst = Subst Dim DSubst = Subst Dim
public export FromVar Dim where fromVarLoc = B public export FromVar Dim where fromVar = B
export export
@ -95,7 +95,7 @@ CanShift Dim where
export export
CanSubstSelf Dim where CanSubstSelf Dim where
K e loc // _ = K e loc K e loc // _ = K e loc
B i loc // th = getLoc th i loc B i loc // th = get th i loc
export Uninhabited (B i loc1 = K e loc2) where uninhabited _ impossible export Uninhabited (B i loc1 = K e loc2) where uninhabited _ impossible

12
lib/Quox/Syntax/Subst.idr
View file

@ -49,10 +49,10 @@ interface FromVar term => CanSubstSelf term where
public export public export
getLoc : FromVar term => Subst term from to -> Var from -> Loc -> term to get : FromVar term => Subst term from to -> Var from -> Loc -> term to
getLoc (Shift by) i loc = fromVarLoc (shift by i) loc get (Shift by) i loc = fromVar (shift by i) loc
getLoc (t ::: th) VZ _ = t get (t ::: th) VZ _ = t
getLoc (t ::: th) (VS i) loc = getLoc th i loc get (t ::: th) (VS i) loc = get th i loc
public export public export
@ -97,7 +97,7 @@ map f (t ::: th) = f t ::: map f th
public export %inline public export %inline
push : CanSubstSelf f => Loc -> Subst f from to -> Subst f (S from) (S to) push : CanSubstSelf f => Loc -> Subst f from to -> Subst f (S from) (S to)
push loc th = fromVarLoc VZ loc ::: (th . shift 1) push loc th = fromVar VZ loc ::: (th . shift 1)
-- [fixme] a better way to do this? -- [fixme] a better way to do this?
public export public export
@ -107,7 +107,7 @@ pushN 0 _ th = th
pushN (S s) loc th = pushN (S s) loc th =
rewrite plusSuccRightSucc s from in rewrite plusSuccRightSucc s from in
rewrite plusSuccRightSucc s to in rewrite plusSuccRightSucc s to in
pushN s loc $ fromVarLoc VZ loc ::: (th . shift 1) pushN s loc $ fromVar VZ loc ::: (th . shift 1)
public export public export
drop1 : Subst f (S from) to -> Subst f from to drop1 : Subst f (S from) to -> Subst f from to

8
lib/Quox/Syntax/Term/Subst.idr
View file

@ -60,8 +60,8 @@ namespace DSubst.DScopeTermN
S ns (N body) // th = S ns $ N $ body // th S ns (N body) // th = S ns $ N $ body // th
export %inline FromVar (Elim d) where fromVarLoc = B export %inline FromVar (Elim d) where fromVar = B
export %inline FromVar (Term d) where fromVarLoc = E .: fromVarLoc export %inline FromVar (Term d) where fromVar = E .: fromVar
||| does the minimal reasonable work: ||| does the minimal reasonable work:
@ -73,7 +73,7 @@ export %inline FromVar (Term d) where fromVarLoc = E .: fromVarLoc
export export
CanSubstSelf (Elim d) where CanSubstSelf (Elim d) where
F x u loc // _ = F x u loc F x u loc // _ = F x u loc
B i loc // th = getLoc th i loc B i loc // th = get th i loc
CloE (Sub e ph) // th = assert_total CloE $ Sub e $ ph . th CloE (Sub e ph) // th = assert_total CloE $ Sub e $ ph . th
e // th = case force th of e // th = case force th of
Shift SZ => e Shift SZ => e
@ -272,7 +272,7 @@ PushSubsts Elim Subst.isCloE where
pushSubstsWith th ph (F x u loc) = pushSubstsWith th ph (F x u loc) =
nclo $ F x u loc nclo $ F x u loc
pushSubstsWith th ph (B i loc) = pushSubstsWith th ph (B i loc) =
let res = getLoc ph i loc in let res = get ph i loc in
case nchoose $ isCloE res of case nchoose $ isCloE res of
Left yes => assert_total pushSubsts res Left yes => assert_total pushSubsts res
Right no => Element res no Right no => Element res no

4
lib/Quox/Untyped/Syntax.idr
View file

@ -255,7 +255,7 @@ USubst : Nat -> Nat -> Type
USubst = Subst Term USubst = Subst Term
public export FromVar Term where fromVarLoc = B public export FromVar Term where fromVar = B
public export public export
@ -264,7 +264,7 @@ CanSubstSelf Term where
F x loc => F x loc =>
F x loc F x loc
B i loc => B i loc =>
getLoc th i loc get th i loc
Lam x body loc => Lam x body loc =>
Lam x (assert_total $ body // push x.loc th) loc Lam x (assert_total $ body // push x.loc th) loc
App fun arg loc => App fun arg loc =>

4
lib/Quox/Var.idr
View file

@ -139,10 +139,10 @@ weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
public export public export
interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n interface FromVar f where %inline fromVar : Var n -> Loc -> f n
public export FromVar Var where fromVarLoc x _ = x public export FromVar Var where fromVar x _ = x
export export
tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) -> tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->