From 5c4053e9d210c604c76f23dfd98c3e271cc07779 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 9 Aug 2023 11:46:14 +0200 Subject: [PATCH] =?UTF-8?q?add=20some=20needed=20=CF=89s=20for=20w-types?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit i.o.u. linear trees. i'm still thinking --- lib/Quox/Equal.idr | 8 ++++---- lib/Quox/Reduce.idr | 17 +++++++++-------- lib/Quox/Typechecker.idr | 16 ++++++++-------- 3 files changed, 21 insertions(+), 20 deletions(-) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index c40a014..2ed7352 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -232,13 +232,13 @@ parameters (defs : Definitions) compare0' ctx ty@(W {shape, body, _}) s t = case (s, t) of -- Γ ⊢ s₁ = t₁ : A - -- Γ ⊢ s₂ = t₂ : 1.B[s₁∷A/x] → (x : A) ⊲ B + -- Γ ⊢ s₂ = t₂ : ω.B[s₁∷A/x] → (x : A) ⊲ B -- ----------------------------------------- -- Γ ⊢ s₁⋄s₂ = t₁⋄t₂ : (x : A) ⊲ B (Sup sRoot sSub {}, Sup tRoot tSub {}) => do compare0 ctx shape sRoot tRoot let arg = sub1 body (Ann sRoot shape sRoot.loc) - subTy = Arr One arg ty ty.loc + subTy = Arr Any arg ty ty.loc compare0 ctx subTy sSub tSub (E e, E f) => Elim.compare0 ctx e f @@ -481,7 +481,7 @@ parameters (defs : Definitions) -- Ψ | Γ ⊢ e = f ⇒ (x : A) ⊲ B -- Ψ | Γ, p : (x : A) ⊲ B ⊢ Q = R ⇐ Type - -- Ψ | Γ, x : A, y : 1.B → (x : A) ⊲ B, ih : 1.(z : B) → Q[y z/p] + -- Ψ | Γ, x : A, y : ω.B → (x : A) ⊲ B, ih : 1.(z : B) → Q[y z/p] -- ⊢ s = t ⇐ Q[(x⋄y ∷ (x : A) ⊲ B)/p] -- ---------------------------------------------------------------- -- Ψ | Γ ⊢ caseπ e return Q of { x ⋄ y, ς.ih ⇒ s } @@ -496,7 +496,7 @@ parameters (defs : Definitions) let [< x, y, ih] = ebody.names z <- mnb "z" ih.loc let xbind = (epi, x, shape) - ybind = (epi, y, Arr One tbody.term (weakT 1 ety) y.loc) + ybind = (epi, y, Arr Any tbody.term (weakT 1 ety) y.loc) ihbind = (epi', ih, PiY One z (sub1 (weakS 2 tbody) (BV 1 x.loc)) diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr index f9b1857..7af8b45 100644 --- a/lib/Quox/Reduce.idr +++ b/lib/Quox/Reduce.idr @@ -441,8 +441,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) -- 𝒮‹𝑘› ≔ ((x : A) ⊲ B)‹𝑘/𝑖› -- 𝒶‹𝑘› ≔ coe [𝑖 ⇒ A] @p @𝑘 a -- : A‹𝑘/𝑖› - -- 𝒷‹𝑘› ≔ coe [𝑖 ⇒ 1.B[𝒶‹𝑖›/x] → 𝒮‹𝑖›] @p @𝑘 b - -- : 1.B‹𝑘/𝑖›[𝒶‹𝑘›/x] → 𝒮‹𝑘› + -- 𝒷‹𝑘› ≔ coe [𝑖 ⇒ ω.B[𝒶‹𝑖›/x] → 𝒮‹𝑖›] @p @𝑘 b + -- : ω.B‹𝑘/𝑖›[𝒶‹𝑘›/x] → 𝒮‹𝑘› -- 𝒾𝒽 ≔ coe [𝑖 ⇒ π.(z : B[𝒶‹𝑖›/x]) → C[𝒷‹𝑖› z/p]] @p @q ih -- : π.(z : B‹q/𝑖›[𝒶‹q›/x]) → C[𝒷‹q› z/p] -- -------------------------------------------------------------------- @@ -464,7 +464,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) // (a' (BV 0 bi.loc) ::: shift 3) ty' = ty // Shift (weak 1 by) // shift 3 in - CoeT bi (Arr One tbody' ty' b.loc) (p // by) k (BVT 1 b.loc) b.loc + CoeT bi (Arr Any tbody' ty' b.loc) (p // by) k (BVT 1 b.loc) b.loc ih' : Elim d (3 + n) := let tbody' = tbody.term // (a' (BV 0 ihi.loc) ::: shift 3) ret' = sub1 (weakS 4 $ dweakS 1 ret) $ @@ -636,17 +636,18 @@ pushCoe defs ctx i ty p q s loc = -- (coe [i ⇒ (x : A) ⊲ π.B] @p @q (s ⋄ t) ⇝ -- (coe [i ⇒ A] @p @q s ⋄ - -- coe [i ⇒ 1.B[coe [j ⇒ A‹j/i›] @p @i s/x] → (x : A) ⊲ B] t) + -- coe [i ⇒ ω.B[coe [j ⇒ A‹j/i›] @p @i s/x] → (x : A) ⊲ B] t) -- ∷ ((x : A) ⊲ B)‹q/i› Sup {root, sub, loc = supLoc} => do let W {shape, body, loc = wLoc} = ty | _ => throw $ ExpectedW ty.loc (extendDim i ctx.names) ty let root' = E $ CoeT i shape p q root root.loc - tsub' = sub1 body $ + tsub0 = sub1 body $ CoeT !(fresh i) (shape // (B VZ root.loc ::: shift 2)) (weakD 1 p) (BV 0 sub.loc) (dweakT 1 sub) sub.loc - sub' = E $ CoeT i tsub' p q sub sub.loc + tsub' = Arr Any tsub0 ty sub.loc + sub' = E $ CoeT i tsub' p q sub sub.loc pure $ Element (Ann (Sup root' sub' supLoc) (W (shape // one q) (body // one q) wLoc) loc) Ah @@ -731,7 +732,7 @@ CanWhnf Elim Reduce.isRedexE where pure $ Element (CasePair pi pair ret body caseLoc) $ pairnf `orNo` np -- s' ≔ s ∷ A - -- t' ≔ t ∷ 1.B[s'/x] → (x : A) ⊲ B + -- t' ≔ t ∷ ω.B[s'/x] → (x : A) ⊲ B -- ih' ≔ (λ x ⇒ caseπ t x return p ⇒ C of { (a ⋄ b), ς.ih ⇒ u }) ∷ -- π.(y : B[s'/x]) → C[t' y/p] -- st' ≔ s ⋄ t ∷ (x : A) ⊲ B @@ -748,7 +749,7 @@ CanWhnf Elim Reduce.isRedexE where w@(W {shape, body = wbody, _}) treeLoc => let root = Ann root shape root.loc wbody' = sub1 wbody root - tsub = Arr One wbody' w sub.loc + tsub = Arr Any wbody' w sub.loc sub = Ann sub tsub sub.loc ih' = LamY !(mnb "y" caseLoc) -- [todo] better name (E $ CaseW qty qtyIH diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index 03119fb..cc463ed 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -85,12 +85,12 @@ where (Zero, r, BVT 2 r.loc)] ||| if a ⋄ b : (x : A) ⊲ B, then b : `supSubTy a A B _` -||| i.e. 1.B[a∷A/x] → ((x : A) ⊲ B) +||| i.e. ω.B[a∷A/x] → ((x : A) ⊲ B) export supSubTy : (root, rootTy : Term d n) -> (body : ScopeTerm d n) -> Loc -> Term d n supSubTy root rootTy body loc = - Arr One (sub1 body (Ann root rootTy root.loc)) (W rootTy body loc) loc + Arr Any (sub1 body (Ann root rootTy root.loc)) (W rootTy body loc) loc mutual @@ -207,10 +207,10 @@ mutual (shape, body) <- expectW !(askAt DEFS) ctx ty.loc ty -- if Ψ | Γ ⊢ σ · a ⇐ A ⊳ Σ₁ qroot <- checkC ctx sg root shape - -- if Ψ | Γ ⊢ σ · b ⇐ 1.B[a∷A/x] → ((x : A) ⊲ B) ⊳ Σ₂ + -- if Ψ | Γ ⊢ σ · b ⇐ ω.B[a∷A/x] → ((x : A) ⊲ B) ⊳ Σ₂ qsub <- checkC ctx sg sub (supSubTy root shape body sub.loc) - -- then Ψ | Γ ⊢ σ · (a ⋄ b) ⇐ ((x : A) ⊲ B) ⊳ Σ₁+Σ₂ - pure $ qroot + qsub + -- then Ψ | Γ ⊢ σ · (a ⋄ b) ⇐ ((x : A) ⊲ B) ⊳ Σ₁+ωΣ₂ + pure $ qroot + Any * qsub check' ctx sg (Pair fst snd loc) ty = do (tfst, tsnd) <- expectSig !(askAt DEFS) ctx ty.loc ty @@ -430,14 +430,14 @@ mutual -- if Ψ | Γ, p : (x : A) ⊲ B ⊢₀ C ⇐ Type checkTypeC (extendTy Zero ret.name w ctx) ret.term Nothing (shape, tbody) <- expectW !(askAt DEFS) ctx tree.loc w - -- if Ψ | Γ, x : A, y : 1.B → (x : A) ⊲ B, + -- if Ψ | Γ, x : A, y : ω.B → (x : A) ⊲ B, -- ih : π.(z : B) → C[y z/p] -- ⊢ σ · u ⇐ C[((x ⋄ y) ∷ (x : A) ⊲ B)/p] -- ⊳ Σ₂, π'.x, ς₁.y, ς₂.ih -- with π' ≤ σπ, ς₂ ≤ σς, ς₁+ς₂ ≤ σπ let [< x, y, ih] = body.names - -- 1.B → (x : A) ⊲ B - tsub = Arr One tbody.term (weakT 1 w) y.loc + -- ω.B → (x : A) ⊲ B + tsub = Arr Any tbody.term (weakT 1 w) y.loc -- y z ihret = App (BV 1 y.loc) (BVT 0 ih.loc) y.loc -- π.(z : B) → C[y z/p]