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

remove most noLocs

Browse source
This commit is contained in:
rhiannon morris 2023-11-27 21:01:36 +01:00
parent 1f01cec322
commit f337625801
16 changed files with 178 additions and 161 deletions
Download patch file Download diff file Expand all files Collapse all files

11
lib/Quox/Whnf/Coercion.idr
View file

@ -63,11 +63,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
(tfst, tsnd) <- tycaseSig defs ctx1 ty
let [< x, y] = body.names
a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc
a' = CoeT i (weakT 2 tfst) p q (BVT 1 x.loc) x.loc
tsnd' = tsnd.term //
(CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2))
(weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2)
b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc
(CoeT i (weakT 2 $ tfst // (B VZ tsnd.loc ::: shift 2))
(weakD 1 p) (B VZ i.loc) (BVT 1 tsnd.loc) y.loc ::: shift 2)
b' = CoeT i tsnd' p q (BVT 0 y.loc) y.loc
whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret
(ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
@ -141,7 +141,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
ta <- tycaseBOX defs ctx1 ty
let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc
let xloc = body.name.loc
let a' = CoeT i (weakT 1 ta) p q (BVT 0 xloc) xloc
whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret
(ST body.names $ body.term // (a' ::: shift 1)) loc

14
lib/Quox/Whnf/TypeCase.idr
View file

@ -120,9 +120,9 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
-- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
Pi {arg, res, loc = piLoc, _} =>
let arg' = Ann arg (TYPE u noLoc) arg.loc
let arg' = Ann arg (TYPE u arg.loc) arg.loc
res' = Ann (Lam res res.loc)
(Arr Zero arg (TYPE u noLoc) arg.loc) res.loc
(Arr Zero arg (TYPE u arg.loc) arg.loc) res.loc
in
whnf defs ctx SZero $
Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc
@ -130,9 +130,9 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
-- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
Sig {fst, snd, loc = sigLoc, _} =>
let fst' = Ann fst (TYPE u noLoc) fst.loc
let fst' = Ann fst (TYPE u fst.loc) fst.loc
snd' = Ann (Lam snd snd.loc)
(Arr Zero fst (TYPE u noLoc) fst.loc) snd.loc
(Arr Zero fst (TYPE u fst.loc) fst.loc) snd.loc
in
whnf defs ctx SZero $
Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc
@ -150,8 +150,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
let a0 = a.zero; a1 = a.one in
whnf defs ctx SZero $ Ann
(subN (tycaseRhsDef def KEq arms)
[< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) a.loc,
Ann (DLam a a.loc) (Eq0 (TYPE u noLoc) a0 a1 a.loc) a.loc,
[< Ann a0 (TYPE u a.loc) a.loc, Ann a1 (TYPE u a.loc) a.loc,
Ann (DLam a a.loc) (Eq0 (TYPE u a.loc) a0 a1 a.loc) a.loc,
Ann l a0 l.loc, Ann r a1 r.loc])
ret loc
@ -166,5 +166,5 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
BOX {ty = a, loc = boxLoc, _} =>
whnf defs ctx SZero $ Ann
(sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u noLoc) a.loc))
(sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u a.loc) a.loc))
ret loc