From 6d0e770c343be16a8eaf9c02dec99352a26f31fd Mon Sep 17 00:00:00 2001 From: Russoul Date: Mon, 3 Aug 2026 12:25:59 +0400 Subject: [PATCH] =?UTF-8?q?The=20non-dependent=20sum=20type=20=E2=8A=8E:?= =?UTF-8?q?=20standalone=20former=20with=20the=20usual=20=CE=B2=20and=20?= =?UTF-8?q?=CE=B7?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .claude/skills/nova/SKILL.md | 7 + docs/NovaElaboration.txt | 62 +++++- docs/NovaFoundation.txt | 177 +++++++++++++++++- docs/NovaKernel.txt | 69 ++++++- src/idris/Nova/Compute.idr | 15 ++ src/idris/Nova/Elaboration.idr | 157 ++++++++++++++++ src/idris/Nova/Elaboration/Named.idr | 30 +++ src/idris/Nova/Elaboration/Parser.idr | 33 +++- src/idris/Nova/Elaboration/Surface.idr | 16 ++ src/idris/Nova/Kernel.idr | 137 ++++++++++++++ src/idris/Nova/Kernel/Beta.idr | 18 ++ src/idris/Nova/Kernel/Parser.idr | 31 ++- src/idris/Nova/Kernel/Subst.idr | 10 + src/idris/Nova/Kernel/Syntax.idr | 40 ++++ src/nova/sum.nova | 60 ++++++ .../elaboration/elab-sum-obligation/expected | 4 + .../elab-sum-obligation/input.nova | 3 + .../nova/elaboration/elab-sum-obligation/run | 2 + tests/nova/elaboration/elab-sum/expected | 5 + tests/nova/elaboration/elab-sum/input.nova | 10 + tests/nova/elaboration/elab-sum/run | 2 + tests/nova/evaluation/eval-sum/expected | 1 + tests/nova/evaluation/eval-sum/input.nova | 4 + tests/nova/evaluation/eval-sum/run | 2 + tests/nova/parser/elem-inj1/expected | 1 + tests/nova/parser/elem-inj1/run | 2 + tests/nova/parser/elem-inj2/expected | 1 + tests/nova/parser/elem-inj2/run | 2 + tests/nova/parser/elem-sumelim/expected | 1 + tests/nova/parser/elem-sumelim/run | 2 + tests/nova/parser/elem-sumty/expected | 1 + tests/nova/parser/elem-sumty/run | 2 + tests/nova/parser/ty-sum-tighter/expected | 1 + tests/nova/parser/ty-sum-tighter/run | 2 + tests/nova/parser/ty-sum/expected | 1 + tests/nova/parser/ty-sum/run | 2 + 36 files changed, 881 insertions(+), 32 deletions(-) create mode 100644 src/nova/sum.nova create mode 100644 tests/nova/elaboration/elab-sum-obligation/expected create mode 100644 tests/nova/elaboration/elab-sum-obligation/input.nova create mode 100755 tests/nova/elaboration/elab-sum-obligation/run create mode 100644 tests/nova/elaboration/elab-sum/expected create mode 100644 tests/nova/elaboration/elab-sum/input.nova create mode 100755 tests/nova/elaboration/elab-sum/run create mode 100644 tests/nova/evaluation/eval-sum/expected create mode 100644 tests/nova/evaluation/eval-sum/input.nova create mode 100755 tests/nova/evaluation/eval-sum/run create mode 100644 tests/nova/parser/elem-inj1/expected create mode 100755 tests/nova/parser/elem-inj1/run create mode 100644 tests/nova/parser/elem-inj2/expected create mode 100755 tests/nova/parser/elem-inj2/run create mode 100644 tests/nova/parser/elem-sumelim/expected create mode 100755 tests/nova/parser/elem-sumelim/run create mode 100644 tests/nova/parser/elem-sumty/expected create mode 100755 tests/nova/parser/elem-sumty/run create mode 100644 tests/nova/parser/ty-sum-tighter/expected create mode 100755 tests/nova/parser/ty-sum-tighter/run create mode 100644 tests/nova/parser/ty-sum/expected create mode 100755 tests/nova/parser/ty-sum/run diff --git a/.claude/skills/nova/SKILL.md b/.claude/skills/nova/SKILL.md index aa4544f9..f42c1c20 100644 --- a/.claude/skills/nova/SKILL.md +++ b/.claude/skills/nova/SKILL.md @@ -117,6 +117,8 @@ data [a : 𝕌] ( … ) -- QIIT signature (see below) ``` Types: `𝟘 𝟙 ℕ 𝕌 Ω`, `(x : T) → U` and `T → U`, `(x : T) ⨯ U`, +`T ⊎ U` (non-dependent disjoint union; binds TIGHTER than → ⨯, so +`A ⊎ B → C` is `(A ⊎ B) → C`), `l ≡ r ∈ T` (SUGAR for `Prf (l ≡ r ∈ T)` — equality is an Ω-valued PROPOSITION), `El t`, `T / (x y. r)` (r is Ω-valued), `Prf p`. `∥T∥` squashes any type to a proposition; `∥Prf p∥ ≜ p`. @@ -126,6 +128,9 @@ Elements: `λx. t`; application by juxtaposition; `(t : T)` ascription projections; `Z`, `S t`; `l ≡ r ∈ T` (the equality prop, at Ω — the ∈-slot takes a TYPE, so write `∈ El a` for a code `a`); `ℕ-elim (n. T) z (n ih. s) t` (motive first); +`inj₁ t`/`inj₂ t` (sum intros, checking-only) and +`⊎-elim (w. T) (a. l) (b. r) t` (motive, left case, right case, +scrutinee — β on both injections); `class t` (quotient intro); `quot-elim (x. T) (a. f) q`; `⋆` (canonical proof; `⋆ e` with explicit witness); `squash-elim e (x. body)`. Universe codes are written like their types @@ -203,6 +208,8 @@ data [a : 𝕌] [r : El a → El a → Ω] - `docs/NovaKernel.txt` — certificates and approximations (A1–A6). - `docs/NovaPipeline.txt` — the trust architecture. - `src/nova/` — the corpus, one topic per file: `nat` (arithmetic), + `sum` (the disjoint union ⊎: inj₁/inj₂, ⊎-elim, β/η, derived + injectivity and disjointness), `equality`/`prop` (≡ and Ω), `quotient`/`quottyuniv` (quotients), `vect`/`vectAppend` (𝕌-indexed families), `qiitNat`/`qiitBag`/ `qiitQuot`/`qiitVec` (QIIT basics), `id` (the identity family — diff --git a/docs/NovaElaboration.txt b/docs/NovaElaboration.txt index d4ad3abe..398fb600 100644 --- a/docs/NovaElaboration.txt +++ b/docs/NovaElaboration.txt @@ -112,7 +112,12 @@ fixity ::= infixl d op | infixr d op # d a digit 0-9 # the context is always implicit in where a subterm sits. T{4} ::= 𝟘 | 𝟙 | ℕ | 𝕌 | Ω | x | (T{≥0}) T{2} ::= El t{≥4} | Prf t{≥4} -T{1} ::= ((x:T{≥0}))+ → T{≥0} | ((x:T{≥0}))+ ⨯ T{≥0} | T{≥2} / (x y. t{≥1}) +T{1} ::= ((x:T{≥0}))+ → T{≥0} | ((x:T{≥0}))+ ⨯ T{≥0} + | T{≥1½} / (x y. t{≥1}) +T{1½} ::= T{≥2} ⊎ T{≥1½} +# ⊎ is NON-DEPENDENT (no binder form), right-associative, and binds +# TIGHTER than → ⨯ / (Agda's convention: A ⊎ B → C is (A ⊎ B) → C); +# the T{1} infixes take their left operand at T{≥1½} T{0} ::= t{≥2} ≡ t{≥2} ∈ T{≥1} # the quotient relation is an Ω-valued ELEMENT (t), not a type. # EQUALITY IS Ω-VALUED (NovaFoundation.txt, Ω block): the surface @@ -140,16 +145,23 @@ t{2} ::= λx. t{≥1½} | 𝟘-elim t{≥4} | S t{≥4} | ℕ-elim (n. T{≥0}) t{≥4} (n ih. t{≥4}) t{≥4} # motive, z, s, scrutinee + | inj₁ t{≥4} + | inj₂ t{≥4} + | ⊎-elim (z. T{≥0}) (a. t{≥0}) (b. t{≥0}) t{≥4} # motive, left case, + # right case, scrutinee | class t{≥4} | quot-elim (z. T{≥0}) (a. t{≥0}) t{≥4} # motive, case fn, scrutinee | squash-elim t{≥4} (x. t{≥0}) # el-squash-e-prf: eliminate a # proof of a squash into a # further proposition | ⋆ t{≥4} # el-squash-i, explicit witness (any A) -t{1} ::= ((x:t{≥0}))+ → t{≥1} | ((x:t{≥0}))+ ⨯ t{≥1} | t{≥2} / (x y. t{≥1}) +t{1} ::= ((x:t{≥0}))+ → t{≥1} | ((x:t{≥0}))+ ⨯ t{≥1} + | t{≥1¼} / (x y. t{≥1}) # universe codes - | t{≥2} ≡ t{≥2} ∈ T{≥2} # the equality PROP (an Ω-element); + | t{≥1¼} ≡ t{≥1¼} ∈ T{≥2} # the equality PROP (an Ω-element); # ∈ embeds a TYPE, like ∥-∥ +t{1¼} ::= t{≥1½} ⊎ t{≥1¼} # the ⊎ code — tighter than the + # t{1} infixes, like its type # ∥T∥ (squash), ≡ (equality props) and ⋆ (the canonical proof) are # the Ω introductions; a squashed type is an Ω-valued element. Bare ⋆ # (t{5}) auto-synthesizes only for evident propositions — a squashed @@ -276,13 +288,14 @@ instead an error asking the user for an ascription or annotation. whnf(–) is weak-head normalization by Foundation's ≜ rules: el-pi-beta, el-sigma-beta₁, el-sigma-beta₂, el-nat-beta-z, -el-nat-beta-s, el-quot-beta, el-qiit-beta (the eliminator at a +el-nat-beta-s, el-sum-beta₁, el-sum-beta₂, el-quot-beta, +el-qiit-beta (the eliminator at a saturated constructor of the nf-identical signature), el-sig-beta/ty-sig-beta (signature unfolding — for DEFINITION entries; a declaration reference is stuck by design, el-sig-decl/ty-sig-decl, and constraint entries are nameless and never referenced), and the El-decoding family (ty-el-zero, ty-el-one, -ty-el-nat, ty-el-pi, ty-el-sigma, ty-el-eq, ty-el-quot — the last +ty-el-nat, ty-el-pi, ty-el-sigma, ty-el-sum, ty-el-eq, ty-el-quot — the last decoding El (A / r) ≜ El A / r, the Ω-valued relation passing through undecoded — and ty-el-qiit, El (𝒮.𝕤 ē) ≜ 𝒮.𝕤 ē; Prf ∥A∥ has no decoding rule). Per @@ -316,6 +329,11 @@ never an unsound acceptance. -------------------------- (e-ty-sigma) # (A ⨯ B) Γ ⊢ (x:T) ⨯ U ⇝ A ⨯ B type +Γ ⊢ T ⇝ A type +Γ ⊢ U ⇝ B type +-------------------------- (e-ty-sum) # (A ⊎ B) +Γ ⊢ T ⊎ U ⇝ A ⊎ B type + Γ ⊢ T ⇝ A type Γ ▷ x:A ▷ y:A[↑] ⊢ r ⇐ Ω ⇝ r̂ # the relation is Ω-valued ------------------------------ (e-ty-quot) # (A / r) @@ -383,6 +401,16 @@ never an unsound acceptance. Γ ⊢ ℕ-elim (n. T) z (n ih. s) t ⇒ A[id, t̂] ⇝ ℕ-elim ẑ ŝ t̂ # (ℕ-elim z s t motive A) +Γ ⊢ t ⇒ C ⇝ t̂ whnf(C) = A ⊎ B +Γ ▷ z:(A ⊎ B) ⊢ T ⇝ M type +Γ ▷ a:A ⊢ l ⇐ M[↑, inj₁ ☐₀] ⇝ l̂ +Γ ▷ b:B ⊢ r ⇐ M[↑, inj₂ ☐₀] ⇝ r̂ +------------------------------------------------------------ (e-sumelim) +Γ ⊢ ⊎-elim (z. T) (a. l) (b. r) t ⇒ M[id, t̂] ⇝ ⊎-elim l̂ r̂ t̂ + # (⊎-elim l r t motive M) +# no side condition beyond the branches themselves — β covers both +# injections, so unlike quot-elim there is no well-definedness premise + Γ ⊢ q ⇒ C ⇝ q̂ whnf(C) = A / r Γ ▷ z:(A / r) ⊢ T ⇝ B type Γ ▷ a:A ⊢ f ⇐ B[↑, class ☐₀] ⇝ f̂ @@ -407,6 +435,11 @@ never an unsound acceptance. Γ ⊢ (x:t) → u ⇒ 𝕌 ⇝ a → b (e-code-sigma analogous for ⨯) # (A ⨯ B : 𝕌) +Γ ⊢ t ⇐ 𝕌 ⇝ a Γ ⊢ u ⇐ 𝕌 ⇝ b +------------------------------------ (e-code-sum) # (A ⊎ B : 𝕌) +Γ ⊢ t ⊎ u ⇒ 𝕌 ⇝ a ⊎ b + # non-dependent: u is checked over Γ, not Γ ▷ El a + Γ ⊢ t ⇐ 𝕌 ⇝ a Γ ▷ x:El a ▷ y:(El a)[↑] ⊢ r ⇐ Ω ⇝ r̂ ------------------------------------------------------------ (e-code-quot) Γ ⊢ t / (x y. r) ⇒ 𝕌 ⇝ a / r̂ # (A / r : 𝕌) @@ -441,6 +474,11 @@ whnf(C) = A ⨯ B Γ ⊢ u ⇐ A ⇝ û Γ ⊢ v ⇐ B[id, û] ⇝ ------------------------------------------------------------------ (e-pair) Γ ⊢ u , v ⇐ C ⇝ û , v̂ # (a, b) +whnf(C) = A ⊎ B Γ ⊢ a ⇐ A ⇝ â +-------------------------------------- (e-inj₁) # (inj₁ a) +Γ ⊢ inj₁ a ⇐ C ⇝ inj₁ â + (e-inj₂ analogous at B) # (inj₂ b) + whnf(C) = A / r Γ ⊢ a ⇐ A ⇝ â -------------------------------------- (e-class) # (class a) Γ ⊢ class a ⇐ C ⇝ class â @@ -588,8 +626,10 @@ whnf(C) = Prf ∥A∥ Γ ⊢ e ⇐ A ⇝ ê # term elaboration. Note the direction of failure: never an error — # the residual equation is assumed and reported. -# Mode inventory. Checking-only forms: λ, pairs, class, ⋆, ⋆ e, -# squash-elim, 𝟘-elim (their types are not determined by their syntax); +# Mode inventory. Checking-only forms: λ, pairs, inj₁, inj₂, class, +# ⋆, ⋆ e, +# squash-elim, 𝟘-elim (their types are not determined by their syntax +# — an injection alone does not determine the OTHER summand); # encountering one in inference position is a structural error whose # fix is an ascription. Everything else — including ∥-∥ — infers and # reaches checking mode through e-switch. @@ -622,6 +662,9 @@ whnf(C) = Prf ∥A∥ Γ ⊢ e ⇐ A ⇝ ê # hypotheses. Decomposition: # A₀ → B₀ ≐ A₁ → B₁ ⇐ A₀ ≐ A₁ type; Γ ▷ A₁ ⊢ B₀ ≐ B₁ type # A₀ ⨯ B₀ ≐ A₁ ⨯ B₁ ⇐ likewise +# A₀ ⊎ B₀ ≐ A₁ ⊎ B₁ ⇐ A₀ ≐ A₁ type; B₀ ≐ B₁ type +# (both over Γ — non-dependent; +# faithful by ty-sum-inj) # A₀ / r₀ ≐ A₁ / r₁ ⇐ A₀ ≐ A₁ type; Γ ▷ A₁ ▷ A₁[↑] ⊢ r₀ ≐ r₁ : Ω # (the relation is compared AT Ω, where # ≐ is iff — ty-quot-cong) @@ -653,6 +696,11 @@ whnf(C) = Prf ∥A∥ Γ ⊢ e ⇐ A ⇝ ê # is a path lemma from E (the data # item's eq-lemmas land there) # S a ≐ S b ⇐ a ≐ b : ℕ +# inj₁ a ≐ inj₁ b ⇐ a ≐ b : A (at A ⊎ B; faithful — +# injection injectivity is derivable; +# likewise inj₂ at B. An inj₁/inj₂ +# HEAD MISMATCH stays an obligation, +# like every rigid mismatch) # class a ≐ class b ⇐ a ≐ b : A, OR — the WITNESS path, # (class⁼ r) — by the shape of the # instantiated relation r[id, a, b] (an diff --git a/docs/NovaFoundation.txt b/docs/NovaFoundation.txt index b1e5c6e1..d6dbb519 100644 --- a/docs/NovaFoundation.txt +++ b/docs/NovaFoundation.txt @@ -1,6 +1,6 @@ ////////// Preface ////////// -#! highlight keywords: ⊦ : ; , · [ ] ‖ .π₁ .π₂ ∈ ∋ ≐ ≜ ≔ ⇒ ⇐ = ⬡ ⬦ ▷ ◁ ⇛ ⇑ 𝕚𝕕 El U ☐ ε ↑ ∘ ⁺ id λ → ⨯ ≡ ∥ / Ω 𝕌 ℕ 𝟘 𝟙 Z S ⋆ Prf class ⌊ ⌋ ⟦ ⟧ ⋈ ⋉ ᴰ 𝟘-elim ℕ-elim quot-elim squash-elim -elim qctx qty qsig ctx type tel mot dalg eprob sect norm small sig nf qpath +#! highlight keywords: ⊦ : ; , · [ ] ‖ .π₁ .π₂ ∈ ∋ ≐ ≜ ≔ ⇒ ⇐ = ⬡ ⬦ ▷ ◁ ⇛ ⇑ 𝕚𝕕 El U ☐ ε ↑ ∘ ⁺ id λ → ⨯ ⊎ ≡ ∥ / Ω 𝕌 ℕ 𝟘 𝟙 Z S ⋆ Prf class inj₁ inj₂ ⌊ ⌋ ⟦ ⟧ ⋈ ⋉ ᴰ 𝟘-elim ℕ-elim quot-elim squash-elim ⊎-elim -elim qctx qty qsig ctx type tel mot dalg eprob sect norm small sig nf qpath #! highlight tos: 𝔄 𝔅 𝕥 𝕦 𝕧 𝕤 𝕔 𝕜 𝕘 𝕒 𝕓 𝕞 Φ 𝒮 ς 𝔎 #! highlight nova: Γ Δ Ξ Σ σ τ δ θ latin #! highlight meta: 𝑤 ρ υ π 𝒞 ℰ @@ -52,6 +52,11 @@ # * Natural numbers type: ℕ # * Dependent product type: (→) # * Dependent sum type: (⨯) +# * Non-dependent sum type: (⊎) — the disjoint union, with injections +# inj₁/inj₂ and a dependent eliminator ⊎-elim (β on each injection, +# uniqueness η in el-nat-eta's style). DEFINABLE as a QIIT (a +# two-point signature — see SUBSUMPTION in the QIIT notes); retained +# as a standalone former, like ℕ and (/) # * Equality proposition: (≡), Ω-valued, with reflection — used through # Prf; proof-irrelevant by el-prf-prop (see the Ω block) # * Quotient type: (/), by an Ω-valued relation @@ -63,12 +68,13 @@ # constructors), the sorts 𝒮.𝕤 ē as types, their constructors 𝒮.𝕔 θ, # the imposed path equations, and a dependent eliminator 𝒮.𝕤-elim with # its computation and uniqueness laws. Every rule is stated against a -# signature (no Σ-entry; 𝒮 is carried by the formers). This subsumes ℕ -# and (/) (each a one-line signature), including indexed inductive types +# signature (no Σ-entry; 𝒮 is carried by the formers). This subsumes ℕ, +# (⊎) and (/) (each a one- or two-line signature), including indexed +# inductive types # and quotient inductive types as special cases; its equation # constructors are INDUCTIVE (they may relate constructor terms across -# indices and participate in the induction). ℕ and (/) are retained for -# now. +# indices and participate in the induction). ℕ, (⊎) and (/) are +# retained for now. ///////////// Syntax /////////////// @@ -114,6 +120,7 @@ T ::= x [e˲] # type in the signature context | Ω # universe of mere propositions | T → T # dependent product type (Π) | T ⨯ T # dependent sum type (Σ) + | T ⊎ T # non-dependent sum type (disjoint union) | El t # Every element of the universe is a type | T / t # quotient type (t an Ω-valued relation) | Prf t # decoding of a proposition (Ω's El; deliberately not @@ -131,11 +138,16 @@ t ::= x [e˲] # element in the signature context | t , t # dependent sum type introduction | t .π₁ # dependent sum type elimination (1) | t .π₂ # dependent sum type elimination (2) + | inj₁ t # non-dependent sum type introduction (left) + | inj₂ t # non-dependent sum type introduction (right) + | ⊎-elim t t t # non-dependent sum type elimination + # (left case, right case, eliminee) | 𝟘 # element of the universe | 𝟙 # element of the universe | ℕ # element of the universe | t → t # element of the universe (encodes Π) | t ⨯ t # element of the universe (encodes Σ) + | t ⊎ t # element of the universe (encodes ⊎) | t ≡ t ∈ T # equality PROPOSITION — an Ω-element; T an # arbitrary TYPE, so equality props exist at # large types (see the Ω block) @@ -553,6 +565,11 @@ e˲ ≐ t˲ : Γ ⇒ Δ' norm ------------------ (ty-sigma) Γ ⊦ A ⨯ B type +Γ ⊦ A type +Γ ⊦ B type +------------------ (ty-sum) # non-dependent: B over Γ, not Γ ▷ A +Γ ⊦ A ⊎ B type + Γ ⊦ A : 𝕌 ----------------- (ty-el) Γ ⊦ El A type @@ -608,6 +625,11 @@ e˲ : Δ ⇒ Γ norm ---------------------------------- (ty-el-sigma) Γ ⊦ El (A ⨯ B) ≜ El A ⨯ El B type +Γ ⊦ A : 𝕌 +Γ ⊦ B : 𝕌 +---------------------------------- (ty-el-sum) +Γ ⊦ El (A ⊎ B) ≜ El A ⊎ El B type + Γ ⊦ A : 𝕌 Γ ▷ El A ▷ (El A)[↑] ⊦ R : Ω ---------------------------------- (ty-el-quot) @@ -661,6 +683,12 @@ e˲ : Δ ⇒ Γ norm --------------------------------------- (ty-sub-sigma) Γ₀ ⊦ (A ⨯ B)[σ] ≜ A[σ] ⨯ B[σ⁺] type +Γ₁ ⊦ A type +Γ₁ ⊦ B type +σ : Γ₀ ⇒ Γ₁ +--------------------------------------- (ty-sub-sum) +Γ₀ ⊦ (A ⊎ B)[σ] ≜ A[σ] ⊎ B[σ] type + Γ₁ ⊦ A type Γ₁ ▷ A ▷ A[↑] ⊦ R : Ω σ : Γ₀ ⇒ Γ₁ @@ -709,6 +737,11 @@ e˲ : Γ₁ ⇒ Γ norm ------------------------------- (ty-sigma-cong) Γ ⊦ A₀ ⨯ B₀ ≐ A₁ ⨯ B₁ type +Γ ⊦ A₀ ≐ A₁ type +Γ ⊦ B₀ ≐ B₁ type +------------------------------- (ty-sum-cong) +Γ ⊦ A₀ ⊎ B₀ ≐ A₁ ⊎ B₁ type + Γ ⊦ A₀ ≐ A₁ type Γ ▷ A₁ ▷ A₁[↑] ⊦ R₀ ≐ R₁ : Ω -------------------------------- (ty-quot-cong) @@ -774,7 +807,13 @@ e˲ : Γ₁ ⇒ Γ norm # the code universes (docs/NovaModel.txt). # * S-injectivity and pair-injectivity need no rules: they are already # derivable (congruence with a ℕ-elim predecessor, respectively the -# projections). +# projections). Ditto inj₁/inj₂-injectivity and -disjointness: +# injectivity by a ⊎-elim retraction at constant motive A whose +# right case returns a fixed default (the compared element itself +# serves), disjointness by a ⊎-elim discriminator at constant +# motive ℕ (Z left, S Z right) followed by the standard Z ≐ S Z +# refutation. The TYPE former ⊎ is injective by rule below, like +# every other structural former. Γ ▷ A₀ ⊦ B₀ type Γ ▷ A₁ ⊦ B₁ type @@ -790,6 +829,11 @@ e˲ : Γ₁ ⇒ Γ norm Γ ⊦ A₀ ≐ A₁ type Γ ▷ A₁ ⊦ B₀ ≐ B₁ type +Γ ⊦ A₀ ⊎ B₀ ≐ A₁ ⊎ B₁ type +------------------------------ (ty-sum-inj) # non-dependent: both +Γ ⊦ A₀ ≐ A₁ type # components over Γ +Γ ⊦ B₀ ≐ B₁ type + Γ ▷ A₀ ▷ A₀[↑] ⊦ R₀ : Ω Γ ▷ A₁ ▷ A₁[↑] ⊦ R₁ : Ω Γ ⊦ A₀ / R₀ ≐ A₁ / R₁ type @@ -820,6 +864,11 @@ e˲ : Γ₁ ⇒ Γ norm Γ ⊦ a₀ ≐ a₁ : 𝕌 Γ ▷ El a₁ ⊦ b₀ ≐ b₁ : 𝕌 +Γ ⊦ a₀ ⊎ b₀ ≐ a₁ ⊎ b₁ : 𝕌 +------------------------------ (code-sum-inj) +Γ ⊦ a₀ ≐ a₁ : 𝕌 +Γ ⊦ b₀ ≐ b₁ : 𝕌 + Γ ▷ El a₀ ▷ (El a₀)[↑] ⊦ r₀ : Ω Γ ▷ El a₁ ▷ (El a₁)[↑] ⊦ r₁ : Ω Γ ⊦ a₀ / r₀ ≐ a₁ / r₁ : 𝕌 @@ -897,6 +946,11 @@ e˲ : Γ₁ ⇒ Γ norm -------------------- (code-sigma) Γ ⊦ A ⨯ B : 𝕌 +Γ ⊦ A : 𝕌 +Γ ⊦ B : 𝕌 +-------------------- (code-sum) +Γ ⊦ A ⊎ B : 𝕌 + Γ ⊦ A : 𝕌 Γ ▷ El A ▷ (El A)[↑] ⊦ R : Ω ------------------------------ (code-quot) @@ -1020,6 +1074,57 @@ e˲ : Γ₁ ⇒ Γ norm ------------------------------------ (el-sigma-eta) Γ ⊦ (t .π₁ , t .π₂) ≐ t : A ⨯ B +# ⊎ — the non-dependent sum (disjoint union). Two injections; the +# eliminator is DEPENDENT (motive C over Γ ▷ A ⊎ B), with β on each +# injection. Uniqueness (η) is stated as elimination into equality — +# el-nat-eta's shape: any map out of A ⊎ B that agrees with the case +# functions on both injections IS the eliminator. + +Γ ⊦ B type +Γ ⊦ a : A +------------------------ (el-sum-i₁) +Γ ⊦ inj₁ a : A ⊎ B + +Γ ⊦ A type +Γ ⊦ b : B +------------------------ (el-sum-i₂) +Γ ⊦ inj₂ b : A ⊎ B + +Γ ▷ A ⊎ B ⊦ C type +Γ ▷ A ⊦ l : C[↑, inj₁ ☐₀] +Γ ▷ B ⊦ r : C[↑, inj₂ ☐₀] +Γ ⊦ t : A ⊎ B +---------------------------------- (el-sum-e, motive C) +Γ ⊦ ⊎-elim l r t : C[id, t] + +Γ ▷ A ⊎ B ⊦ C type +Γ ▷ A ⊦ l : C[↑, inj₁ ☐₀] +Γ ▷ B ⊦ r : C[↑, inj₂ ☐₀] +Γ ⊦ a : A +------------------------------------------------------------ (el-sum-beta₁) +Γ ⊦ ⊎-elim l r (inj₁ a) ≜ l[id, a] : C[id, inj₁ a] + +Γ ▷ A ⊎ B ⊦ C type +Γ ▷ A ⊦ l : C[↑, inj₁ ☐₀] +Γ ▷ B ⊦ r : C[↑, inj₂ ☐₀] +Γ ⊦ b : B +------------------------------------------------------------ (el-sum-beta₂) +Γ ⊦ ⊎-elim l r (inj₂ b) ≜ r[id, b] : C[id, inj₂ b] + +Γ ▷ A ⊎ B ⊦ C type +Γ ▷ A ⊎ B ⊦ g : C +Γ ▷ A ⊦ l : C[↑, inj₁ ☐₀] +Γ ▷ B ⊦ r : C[↑, inj₂ ☐₀] +Γ ▷ A ⊦ g[↑, inj₁ ☐₀] ≐ l : C[↑, inj₁ ☐₀] +Γ ▷ B ⊦ g[↑, inj₂ ☐₀] ≐ r : C[↑, inj₂ ☐₀] +Γ ⊦ t : A ⊎ B +------------------------------------------------- (el-sum-eta, motive C) +Γ ⊦ g[id, t] ≐ ⊎-elim l r t : C[id, t] + +# Corollary (two-candidate form, as at ℕ): two maps out of A ⊎ B that +# agree on both injections are equal — chain el-sum-eta through the +# eliminator they both equal. + # ≡ is Ω-VALUED: formation, introduction and reflection live in the Ω # block below, alongside squash — equality is a proposition, used # through Prf. @@ -1274,9 +1379,10 @@ e˲ : Γ₁ ⇒ Γ norm # signature (⊦ 𝒮 qsig as a premise); a signature is NOT a Σ-entry and # mints no names — 𝒮 is carried by the formers themselves (as A / R # carries A and R). These are the inductive-inductive quotient types of -# Altenkirch–Kaposi. The scheme SUBSUMES ℕ and (/), and covers indexed +# Altenkirch–Kaposi. The scheme SUBSUMES ℕ, (⊎) and (/), and covers +# indexed # inductive types (well-founded trees included) and quotient inductive -# types generally; ℕ and (/) are retained for now. +# types generally; ℕ, (⊎) and (/) are retained for now. # # THE EXTENSIONAL PAYOFF. Under equality reflection (with Ω for # proof-irrelevance) every type is a set: no higher paths, no coherence @@ -1858,7 +1964,12 @@ for each point position 𝕔 of 𝒮 (𝒮(𝕔) = 𝔄, ending in El (𝕤 ī); # NOTES. # * SUBSUMPTION. ℕ is 𝒮.𝕟 · for 𝒮 = (𝕟 : U; Z : El 𝕟; # S : (𝕧 : El 𝕟) ⇛ El 𝕟). The quotient A / R is 𝒮.𝕢 · for the -# signature under IDENTITY above. An indexed inductive type +# signature under IDENTITY above. The disjoint union A ⊎ B is +# 𝒮.𝕤 · for 𝒮 = (𝕤 : U; inl : (x : A) ⇛ El 𝕤; +# inr : (y : B) ⇛ El 𝕤) — two external-domain points, no +# equations; its eliminator's β and η are el-qiit-beta/-eta at +# that signature, which is exactly why ⊎'s standalone rules could +# be READ OFF the scheme. An indexed inductive type # (well-founded trees included) is a sorts-and-points signature: # sorts with index arities over I, one point constructor per node # shape whose inductive binders are the subtrees. Because QIIT @@ -1977,6 +2088,12 @@ e˲ : Δ ⇒ Γ norm ---------------------------------------- (el-sub-code-sigma) Γ₀ ⊦ (A ⨯ B)[σ] ≜ A[σ] ⨯ B[σ⁺] : 𝕌 +Γ₁ ⊦ A : 𝕌 +Γ₁ ⊦ B : 𝕌 +σ : Γ₀ ⇒ Γ₁ +---------------------------------------- (el-sub-code-sum) +Γ₀ ⊦ (A ⊎ B)[σ] ≜ A[σ] ⊎ B[σ] : 𝕌 + Γ₁ ⊦ A : 𝕌 Γ₁ ▷ El A ▷ (El A)[↑] ⊦ R : Ω σ : Γ₀ ⇒ Γ₁ @@ -2017,6 +2134,26 @@ e˲ : Δ ⇒ Γ norm ------------------------------------------------------- (el-sub-proj₂) Γ₀ ⊦ (t .π₂)[σ] ≜ t[σ] .π₂ : B[σ, t[σ] .π₁] +Γ₁ ⊦ B type +Γ₁ ⊦ a : A +σ : Γ₀ ⇒ Γ₁ +------------------------------------------------ (el-sub-inj₁) +Γ₀ ⊦ (inj₁ a)[σ] ≜ inj₁ a[σ] : A[σ] ⊎ B[σ] + +Γ₁ ⊦ A type +Γ₁ ⊦ b : B +σ : Γ₀ ⇒ Γ₁ +------------------------------------------------ (el-sub-inj₂) +Γ₀ ⊦ (inj₂ b)[σ] ≜ inj₂ b[σ] : A[σ] ⊎ B[σ] + +Γ ▷ A ⊎ B ⊦ C type +Γ ▷ A ⊦ l : C[↑, inj₁ ☐₀] +Γ ▷ B ⊦ r : C[↑, inj₂ ☐₀] +Γ ⊦ t : A ⊎ B +σ : Δ ⇒ Γ +------------------------------------------------------------------- (el-sub-sum-e) +Δ ⊦ (⊎-elim l r t)[σ] ≜ ⊎-elim l[σ⁺] r[σ⁺] t[σ] : C[σ, t[σ]] + Γ₁ ⊦ a₀ : A Γ₁ ⊦ a₁ : A σ : Γ₀ ⇒ Γ₁ @@ -2146,6 +2283,23 @@ e˲ : Γ₁ ⇒ Γ norm ------------------------------------------- (el-proj₂-cong) Γ ⊦ t₀ .π₂ ≐ t₁ .π₂ : B[id, t₁ .π₁] +Γ ⊦ B type +Γ ⊦ a₀ ≐ a₁ : A +--------------------------------- (el-inj₁-cong) +Γ ⊦ inj₁ a₀ ≐ inj₁ a₁ : A ⊎ B + +Γ ⊦ A type +Γ ⊦ b₀ ≐ b₁ : B +--------------------------------- (el-inj₂-cong) +Γ ⊦ inj₂ b₀ ≐ inj₂ b₁ : A ⊎ B + +Γ ▷ A ⊎ B ⊦ C type +Γ ▷ A ⊦ l₀ ≐ l₁ : C[↑, inj₁ ☐₀] +Γ ▷ B ⊦ r₀ ≐ r₁ : C[↑, inj₂ ☐₀] +Γ ⊦ t₀ ≐ t₁ : A ⊎ B +------------------------------------------------------ (el-sum-e-cong, motive C) +Γ ⊦ ⊎-elim l₀ r₀ t₀ ≐ ⊎-elim l₁ r₁ t₁ : C[id, t₁] + Γ ⊦ t₀ ≐ t₁ : ℕ ------------------------- (el-suc-cong) Γ ⊦ S t₀ ≐ S t₁ : ℕ @@ -2190,6 +2344,11 @@ e˲ : Γ₁ ⇒ Γ norm ------------------------------- (code-sigma-cong) Γ ⊦ A₀ ⨯ B₀ ≐ A₁ ⨯ B₁ : 𝕌 +Γ ⊦ A₀ ≐ A₁ : 𝕌 +Γ ⊦ B₀ ≐ B₁ : 𝕌 +------------------------------- (code-sum-cong) +Γ ⊦ A₀ ⊎ B₀ ≐ A₁ ⊎ B₁ : 𝕌 + Γ ⊦ A₀ ≐ A₁ : 𝕌 Γ ▷ El A₁ ▷ (El A₁)[↑] ⊦ R₀ ≐ R₁ : Ω --------------------------------------- (code-quot-cong) diff --git a/docs/NovaKernel.txt b/docs/NovaKernel.txt index b9aee284..ebc79075 100644 --- a/docs/NovaKernel.txt +++ b/docs/NovaKernel.txt @@ -51,6 +51,8 @@ of fuel, are exactly: (a , b) .π₂ ≜ b # el-sigma-beta₂ ℕ-elim z s Z ≜ z # el-nat-beta-z ℕ-elim z s (S n) ≜ s[id, n, ℕ-elim z s n] # el-nat-beta-s + ⊎-elim l r (inj₁ a) ≜ l[id, a] # el-sum-beta₁ + ⊎-elim l r (inj₂ b) ≜ r[id, b] # el-sum-beta₂ quot-elim f (class a) ≜ f[id, a] # el-quot-beta 𝒮.𝕤-elim ℰ ē (𝒮′.𝕔 θ) ≜ m_𝕔 θ⟨φᵉˡ⟩ # el-qiit-beta; fires # only when 𝒮 and 𝒮′ are @@ -63,6 +65,7 @@ of fuel, are exactly: El ℕ ≜ ℕ El (a → b) ≜ El a → El b El (a ⨯ b) ≜ El a ⨯ El b + El (a ⊎ b) ≜ El a ⊎ El b El (a / r) ≜ El a / r # the Ω-valued relation is NOT decoded El (𝒮.𝕤 ē) ≜ 𝒮.𝕤 ē # ty-el-qiit @@ -137,6 +140,8 @@ implementation's names): suc (SelSuc) | dom (SelDom) | cod u (SelCod) + | suml (SelSumL) + | sumr (SelSumR) | qdom (SelQDom) | qrel u v (SelQRel) | qidx i (SelQIdx) @@ -160,6 +165,7 @@ implementation's names): | quotCong 𝒞 (FQuotCong) | piCong 𝒞 𝒞 (FPiCong) | sigmaCong 𝒞 𝒞 (FSigmaCong) + | sumCong 𝒞 𝒞 (FSumCong) | qiitCong 𝒞̄ 𝒞̄ (FQiitCong) The three Ω finals: propext is code-prop-eq — the sides are prop codes @@ -187,7 +193,9 @@ Child indexing, shared by paths, the typed descent (§6) and skeletons ℕ-elim z s t → 0, 1(2), 2 λ f → 0(1) f e → 0, 1 (a , b) → 0, 1 t.π₁ / t.π₂ → 0 + inj₁ t / inj₂ t → 0 ⊎-elim l r t → 0(1), 1(1), 2 a →ᶜ b → 0, 1(1) a ⨯ᶜ b → 0, 1(1) + a ⊎ᶜ b → 0, 1 (l ≡ r ∈ T) → 0, 1, 2ᵗ a /ᶜ r → 0, 1(2) x[e˲] → 0.. (left to right) class a → 0 quot-elim f q → 0(1), 1 @@ -196,7 +204,7 @@ Child indexing, shared by paths, the typed descent (§6) and skeletons 𝒮.𝕔 θ → 0.. (the argument spine) 𝒮.𝕤-elim ℰ ē w → 0..n-1 (the index spine), n (the eliminee) types: A → B → 0, 1(1) A ⨯ B → 0, 1(1) - El e → 0ᵉ Prf e → 0ᵉ + A ⊎ B → 0, 1 El e → 0ᵉ Prf e → 0ᵉ A / r → 0, 1ᵉ(2) x[e˲] → 0..ᵉ 𝒮.𝕤 ē → 0..ᵉ (ᶜ marks universe codes; ᵉ marks descent into an element child, ᵗ into @@ -232,7 +240,7 @@ a generic lemma's 𝕌-parameter materialized at a concrete code is a legitimate spine argument — and so does a small signature's sort code, its index spine checked positionally against the reflected arity: - Σ; Γ ⊦ ℕc ⇒ᵖ 𝕌 (likewise 𝟘c, 𝟙c; Π/Σ/quot/≡ codes componentwise) + Σ; Γ ⊦ ℕc ⇒ᵖ 𝕌 (likewise 𝟘c, 𝟙c; Π/Σ/⊎/quot/≡ codes componentwise) 𝒮 small 𝒮(𝕜) = 𝔄 ending in U Σ; Γ ⊦ ē ⇐ᵖ ⌊𝔄⌋ᵗ (entrywise) -------------------------------------------------------------- @@ -255,6 +263,17 @@ introduction forms structurally and falls back to infer-and-compare: Σ; Γ ⊦ class a ⇐ᵖ T --------------------------------- Σ; Γ ⊦ (u , v) ⇐ᵖ T + nf(T) ⇓ A ⊎ B Σ; Γ ⊦ a ⇐ᵖ A nf(T) ⇓ A ⊎ B Σ; Γ ⊦ b ⇐ᵖ B + ----------------------------- ----------------------------- + Σ; Γ ⊦ inj₁ a ⇐ᵖ T Σ; Γ ⊦ inj₂ b ⇐ᵖ T + + Σ; Γ ⊦ t ⇒ᵖ Tt nf(Tt) ⇓ A ⊎ B + Σ; Γ ▷ A ⊦ l ⇐ᵖ T[↑] Σ; Γ ▷ B ⊦ r ⇐ᵖ T[↑] + -------------------------------------------------------------- + Σ; Γ ⊦ ⊎-elim l r t ⇐ᵖ T # CONSTANT-MOTIVE (approximation + # A1, see §9): the instance of + # el-sum-e with motive T[↑] + nf(T) ⇓ 𝒮.𝕤 ē 𝒮(𝕔) = 𝔄 ending in El (𝕤 ī) Σ; Γ ⊦ θ ⇐ᵖ ⌊𝔄⌋ᵗ (entrywise) nf(⌊ī⌋[θ]) = nf(ē) -------------------------------------------------- # el-qiit-intro: @@ -331,6 +350,10 @@ do not match is rejected. cod u : (a₀ → b₀) ≐ (a₁ → b₁) : 𝕌 ⇒ b₀[id,u] ≐ b₁[id,u] : 𝕌 requires Σ; Γ ⊦ u ⇐ᵖ El a₁ # code-pi-inj second component, instantiated at u (el-sub-cong-fix) + suml : (a₀ ⊎ b₀) ≐ (a₁ ⊎ b₁) : 𝕌 ⇒ a₀ ≐ a₁ : 𝕌 + sumr : (a₀ ⊎ b₀) ≐ (a₁ ⊎ b₁) : 𝕌 ⇒ b₀ ≐ b₁ : 𝕌 + # code-sum-inj; non-dependent, so neither component + # crosses a binder and no instantiation element is needed qdom : (a₀ / r₀) ≐ (a₁ / r₁) : 𝕌 ⇒ a₀ ≐ a₁ : 𝕌 # code-quot-inj qrel u v : (a₀ / r₀) ≐ (a₁ / r₁) : 𝕌 ⇒ r₀[id,u,v] ≐ r₁[id,u,v] : Ω requires Σ; Γ ⊦ u ⇐ᵖ El a₁ Σ; Γ ⊦ v ⇐ᵖ El a₁ @@ -394,6 +417,11 @@ type E; — means undetermined): (u , v) child 0 : A when nf(E) ⇓ A ⨯ B child 1 : B[id, u] t.π₁ / t.π₂ child 0 : ⇒ᴺ(t) + inj₁ a child 0 : A when nf(E) ⇓ A ⊎ B + inj₂ b child 0 : B when nf(E) ⇓ A ⊎ B + ⊎-elim l r t children 0, 1 : — # motive-dependent (like + child 2 : ⇒ᴺ(t) # quot-elim's case function) + a ⊎ᶜ b children : 𝕌 a →ᶜ b, a ⨯ᶜ b children : 𝕌 (l ≡ r ∈ T) children 0,1 : T, child 2 : a type child # the Ω-valued equality prop; congruence is @@ -475,7 +503,9 @@ common domain, 𝒞 proves the relations equal at Ω — ty-quot-cong), piCong 𝒞 𝒞 / sigmaCong 𝒞 𝒞 (ty-pi-cong / ty-sigma-cong, componentwise: domain certificate, then codomain certificate under the RIGHT domain — needed exactly when a component's equality is -itself extensional, e.g. a Prf codomain equal only by propext), and +itself extensional, e.g. a Prf codomain equal only by propext), +sumCong 𝒞 𝒞 (ty-sum-cong, componentwise — both components over Γ, +no binder to cross), and qiitCong 𝒞̄p 𝒞̄i (both sides sort applications 𝒮₀.𝕤 ē₀ / 𝒮₁.𝕤 ē₁ AT THE SAME SORT POSITION: 𝒮₀ and 𝒮₁ must be identical nameless ToS syntax up to their embedded Nova pieces — positions, entry shapes, binder @@ -547,6 +577,10 @@ Checking Σ; Γ ⊦ t ⇐ T ⟨sk⟩ : Σ; Γ ⊦ ⋆ ⇐ T ⟨sk⟩ # el-eq-i over replay # disambiguated from the squash rules below by nf(T)'s prop head + nf(T) ⇓ A ⊎ B Σ; Γ ⊦ a ⇐ A ⟨sk.0⟩ + ------------------------------------- # el-sum-i₁ + Σ; Γ ⊦ inj₁ a ⇐ T ⟨sk⟩ (inj₂ analogously at B) + nf(T) ⇓ A / r Σ; Γ ⊦ a ⇐ A ⟨sk.0⟩ ------------------------------------- # el-quot-i Σ; Γ ⊦ class a ⇐ T ⟨sk⟩ @@ -604,6 +638,17 @@ Inference Σ; Γ ⊦ t ⇒ T ⟨sk⟩ : ------------------------------------------------------------ Σ; Γ ⊦ ℕ-elim z s t ⇒ M[id, t] # el-nat-e + ⊎-elim demands its motive; the scrutinee's type is inferred (its + head is neutral or an injection in the emitted fragment): + + sk carries motive M ⟨skM⟩ + Σ; Γ ⊦ t ⇒ Tt ⟨sk.2⟩ nf(Tt) ⇓ A ⊎ B + Σ; Γ ▷ A ⊎ B ⊦ M type ⟨skM⟩ + Σ; Γ ▷ A ⊦ l ⇐ M[↑, inj₁ ☐₀] ⟨sk.0⟩ + Σ; Γ ▷ B ⊦ r ⇐ M[↑, inj₂ ☐₀] ⟨sk.1⟩ + ------------------------------------------------------------ + Σ; Γ ⊦ ⊎-elim l r t ⇒ M[id, t] # el-sum-e + quot-elim demands motive AND well-definedness: sk carries motive M ⟨skM⟩ and wd 𝒞 @@ -650,7 +695,7 @@ Inference Σ; Γ ⊦ t ⇒ T ⟨sk⟩ : ascription payload) is rejected. Formation Σ; Γ ⊦ T type ⟨sk⟩ : structural over the type formers -(ty-pi/sigma/el/prf/quot/ty-prop/ty-sig-var), El's code checked at 𝕌, +(ty-pi/sigma/sum/el/prf/quot/ty-prop/ty-sig-var), El's code checked at 𝕌, Prf's code and the quotient's relation checked at Ω, signature-type arguments checked against their telescope — all with skeleton children along. A sort @@ -693,8 +738,10 @@ EQUATION REPLAY (A1, A2), and three added by the QIIT extension A1 CONSTANT MOTIVE. In proof-argument checking (§3) an ℕ-elim argument is checked by the el-nat-e instance whose motive is - T[↑]; in the typed descent (§6) the z/s positions of an ℕ-elim - are typed by the same reading. Dependent-motive recursors + T[↑], and a ⊎-elim argument by the el-sum-e instance likewise; + in the typed descent (§6) the z/s positions of an ℕ-elim + are typed by the same reading (a ⊎-elim's case positions stay + undetermined there). Dependent-motive recursors cannot be rewritten at those positions and their proofs cannot appear as step arguments; the ITEM level (§8) carries real motives and has no such limit. @@ -722,10 +769,12 @@ EQUATION REPLAY (A1, A2), and three added by the QIIT extension through Σ, where the item level carries the full apparatus (coherences as PQCoh certificates, §8). - A5 NO η CERTIFICATE FOR QIITs. el-qiit-eta (like el-nat-eta and - el-quot-eta before it) has no replay final; uniqueness - arguments live in the elaborator as lemmas, not in kernel - certificates. The Π/Σ η finals are unaffected. + A5 NO η CERTIFICATE FOR QIITs. el-qiit-eta (like el-nat-eta, + el-sum-eta and el-quot-eta before it) has no replay final; + uniqueness arguments live in the elaborator as lemmas, not in + kernel certificates (an el-sum-eta instance is proven as an + ordinary ⊎-elim lemma at an equality motive, β closing both + cases). The Π/Σ η finals are unaffected. A6 FIRST-ORDER SIGNATURE FRAGMENT. The signature checker (§8) covers the fragment the elaborator emits: no equation-code diff --git a/src/idris/Nova/Compute.idr b/src/idris/Nova/Compute.idr index 4048921e..338aca2b 100644 --- a/src/idris/Nova/Compute.idr +++ b/src/idris/Nova/Compute.idr @@ -138,11 +138,19 @@ mutual case whnfElem sig t of SigmaIntro _ b => whnfElem sig b _ => assert_total $ idris_crash "whnfElem: .π₂ scrutinee is not a pair (impossible for a closed, well-typed term)" + whnfElem sig (Inj1 t) = Inj1 t + whnfElem sig (Inj2 t) = Inj2 t + whnfElem sig (SumElim l r t) = + case whnfElem sig t of + Inj1 a => whnfElem sig (substElem l (Ext Id a)) + Inj2 b => whnfElem sig (substElem r (Ext Id b)) + _ => assert_total $ idris_crash "whnfElem: ⊎-elim scrutinee is not an injection (impossible for a closed, well-typed term)" whnfElem sig Elem.ZeroTy = Elem.ZeroTy whnfElem sig Elem.OneTy = Elem.OneTy whnfElem sig Elem.NatTy = Elem.NatTy whnfElem sig (Elem.PiTy a b) = Elem.PiTy a b -- co-data whnfElem sig (Elem.SigmaTy a b) = Elem.SigmaTy a b + whnfElem sig (Elem.SumTy a b) = Elem.SumTy a b whnfElem sig (Elem.EqTy l r t) = Elem.EqTy l r t whnfElem sig (QuotTy a r) = QuotTy a r whnfElem sig (SigVar x es) = @@ -181,6 +189,7 @@ mutual whnfTy sig Ty.UniverseTy = Ty.UniverseTy whnfTy sig (Ty.PiTy a b) = Ty.PiTy a b -- co-data whnfTy sig (Ty.SigmaTy a b) = Ty.SigmaTy a b + whnfTy sig (Ty.SumTy a b) = Ty.SumTy a b whnfTy sig (El e) = case whnfElem sig e of Elem.ZeroTy => Ty.ZeroTy @@ -188,6 +197,7 @@ mutual Elem.NatTy => Ty.NatTy Elem.PiTy a b => Ty.PiTy (El a) (El b) Elem.SigmaTy a b => Ty.SigmaTy (El a) (El b) + Elem.SumTy a b => Ty.SumTy (El a) (El b) QuotTy a r => Quotient (El a) r QSortC sg k es => QSort sg k es -- ty-el-qiit _ => assert_total $ idris_crash "whnfTy: El argument is not a universe code (impossible for a closed, well-typed term)" @@ -225,11 +235,15 @@ mutual go (SigmaIntro a b) = SigmaIntro (nfElem sig a) (nfElem sig b) -- a Σ VALUE: no binder crossed go (SigmaElim1 t) = SigmaElim1 (nfElem sig t) go (SigmaElim2 t) = SigmaElim2 (nfElem sig t) + go (Inj1 t) = Inj1 (nfElem sig t) -- an injection is data: no binder crossed + go (Inj2 t) = Inj2 (nfElem sig t) + go (SumElim l r t) = SumElim l r (nfElem sig t) -- l, r: under a binder, left alone go Elem.ZeroTy = Elem.ZeroTy go Elem.OneTy = Elem.OneTy go Elem.NatTy = Elem.NatTy go (Elem.PiTy a b) = Elem.PiTy a b -- co-data: leave domain/codomain go (Elem.SigmaTy a b) = Elem.SigmaTy (nfElem sig a) b -- b: under a binder, left alone + go (Elem.SumTy a b) = Elem.SumTy (nfElem sig a) (nfElem sig b) -- non-dependent: BOTH recursed go (Elem.EqTy l r t) = Elem.EqTy (nfElem sig l) (nfElem sig r) (nfTy sig t) go (QuotTy a r) = QuotTy (nfElem sig a) r -- r: under a binder, left alone go (SigVar x es) = SigVar x es -- unreachable: whnf always unfolds x[e˲] @@ -257,6 +271,7 @@ mutual go Ty.UniverseTy = Ty.UniverseTy go (Ty.PiTy a b) = Ty.PiTy a b -- co-data: leave domain/codomain go (Ty.SigmaTy a b) = Ty.SigmaTy (nfTy sig a) b -- b: under a binder, left alone + go (Ty.SumTy a b) = Ty.SumTy (nfTy sig a) (nfTy sig b) -- non-dependent: BOTH recursed go (El e) = El (nfElem sig e) go PropTy = PropTy go (Prf e) = Prf (nfElem sig e) diff --git a/src/idris/Nova/Elaboration.idr b/src/idris/Nova/Elaboration.idr index b24f5faa..0932b802 100644 --- a/src/idris/Nova/Elaboration.idr +++ b/src/idris/Nova/Elaboration.idr @@ -253,11 +253,15 @@ mapRefsE f (PiApp g e) = PiApp (mapRefsE f g) (mapRefsE f e) mapRefsE f (SigmaIntro a b) = SigmaIntro (mapRefsE f a) (mapRefsE f b) mapRefsE f (SigmaElim1 t) = SigmaElim1 (mapRefsE f t) mapRefsE f (SigmaElim2 t) = SigmaElim2 (mapRefsE f t) +mapRefsE f (Inj1 t) = Inj1 (mapRefsE f t) +mapRefsE f (Inj2 t) = Inj2 (mapRefsE f t) +mapRefsE f (SumElim l r t) = SumElim (mapRefsE f l) (mapRefsE f r) (mapRefsE f t) mapRefsE f Elem.ZeroTy = Elem.ZeroTy mapRefsE f Elem.OneTy = Elem.OneTy mapRefsE f Elem.NatTy = Elem.NatTy mapRefsE f (Elem.PiTy a b) = Elem.PiTy (mapRefsE f a) (mapRefsE f b) mapRefsE f (Elem.SigmaTy a b) = Elem.SigmaTy (mapRefsE f a) (mapRefsE f b) +mapRefsE f (Elem.SumTy a b) = Elem.SumTy (mapRefsE f a) (mapRefsE f b) mapRefsE f (Elem.EqTy l r t) = Elem.EqTy (mapRefsE f l) (mapRefsE f r) (mapRefsT f t) mapRefsE f (QuotTy a r) = QuotTy (mapRefsE f a) (mapRefsE f r) mapRefsE f (Class a) = Class (mapRefsE f a) @@ -276,6 +280,7 @@ mapRefsT f Ty.NatTy = Ty.NatTy mapRefsT f Ty.UniverseTy = Ty.UniverseTy mapRefsT f (Ty.PiTy a b) = Ty.PiTy (mapRefsT f a) (mapRefsT f b) mapRefsT f (Ty.SigmaTy a b) = Ty.SigmaTy (mapRefsT f a) (mapRefsT f b) +mapRefsT f (Ty.SumTy a b) = Ty.SumTy (mapRefsT f a) (mapRefsT f b) mapRefsT f (El e) = El (mapRefsE f e) mapRefsT f PropTy = PropTy mapRefsT f (Prf e) = Prf (mapRefsE f e) @@ -318,11 +323,15 @@ collectRefsE e = go e go (SigmaIntro a b) = go a ++ go b go (SigmaElim1 t) = go t go (SigmaElim2 t) = go t + go (Inj1 t) = go t + go (Inj2 t) = go t + go (SumElim l r t) = go l ++ go r ++ go t go Elem.ZeroTy = [] go Elem.OneTy = [] go Elem.NatTy = [] go (Elem.PiTy a b) = go a ++ go b go (Elem.SigmaTy a b) = go a ++ go b + go (Elem.SumTy a b) = go a ++ go b go (Elem.EqTy l r t) = go l ++ go r ++ goT t go (QuotTy a r) = go a ++ go r go (Class a) = go a @@ -351,6 +360,7 @@ collectRefsE e = go e goT Ty.UniverseTy = [] goT (Ty.PiTy a b) = goT a ++ goT b goT (Ty.SigmaTy a b) = goT a ++ goT b + goT (Ty.SumTy a b) = goT a ++ goT b goT (El x) = go x goT PropTy = [] goT (Prf x) = go x @@ -460,6 +470,7 @@ codeOf Ty.OneTy = Just Elem.OneTy codeOf Ty.NatTy = Just Elem.NatTy codeOf (Ty.PiTy a b) = Elem.PiTy <$> codeOf a <*> codeOf b codeOf (Ty.SigmaTy a b) = Elem.SigmaTy <$> codeOf a <*> codeOf b +codeOf (Ty.SumTy a b) = Elem.SumTy <$> codeOf a <*> codeOf b -- the relation is an Ω-element in BOTH the type former and the code: -- El (A / R) ≜ El A / R, so it passes through unchanged codeOf (Quotient a r) = QuotTy <$> codeOf a <*> Just r @@ -518,6 +529,10 @@ matchElemP k d b (SigmaIntro u v) (SigmaIntro u' v') = \bs => matchElemP k d b u u' bs >>= matchElemP k d b v v' matchElemP k d b (SigmaElim1 t) (SigmaElim1 t') = matchElemP k d b t t' matchElemP k d b (SigmaElim2 t) (SigmaElim2 t') = matchElemP k d b t t' +matchElemP k d b (Inj1 t) (Inj1 t') = matchElemP k d b t t' +matchElemP k d b (Inj2 t) (Inj2 t') = matchElemP k d b t t' +matchElemP k d b (SumElim l r t) (SumElim l' r' t') = + \bs => matchElemP k d (1 + b) l l' bs >>= matchElemP k d (1 + b) r r' >>= matchElemP k d b t t' matchElemP k d b Elem.ZeroTy Elem.ZeroTy = Just matchElemP k d b Elem.OneTy Elem.OneTy = Just matchElemP k d b Elem.NatTy Elem.NatTy = Just @@ -525,6 +540,8 @@ matchElemP k d b (Elem.PiTy a c) (Elem.PiTy a' c') = \bs => matchElemP k d b a a' bs >>= matchElemP k d (1 + b) c c' matchElemP k d b (Elem.SigmaTy a c) (Elem.SigmaTy a' c') = \bs => matchElemP k d b a a' bs >>= matchElemP k d (1 + b) c c' +matchElemP k d b (Elem.SumTy a c) (Elem.SumTy a' c') = + \bs => matchElemP k d b a a' bs >>= matchElemP k d b c c' matchElemP k d b (Elem.EqTy l r t) (Elem.EqTy l' r' t') = \bs => matchElemP k d b l l' bs >>= matchElemP k d b r r' >>= matchTyP k d b t t' matchElemP k d b (QuotTy a r) (QuotTy a' r') = @@ -605,6 +622,8 @@ matchTyP k d b (Ty.PiTy a c) (Ty.PiTy a' c') = \bs => matchTyP k d b a a' bs >>= matchTyP k d (1 + b) c c' matchTyP k d b (Ty.SigmaTy a c) (Ty.SigmaTy a' c') = \bs => matchTyP k d b a a' bs >>= matchTyP k d (1 + b) c c' +matchTyP k d b (Ty.SumTy a c) (Ty.SumTy a' c') = + \bs => matchTyP k d b a a' bs >>= matchTyP k d b c c' matchTyP k d b (El e) (El e') = matchElemP k d b e e' -- normalization El-decodes codes inside carried signatures (El ℕc ≜ ℕ), -- so a pattern `El e` whose e is parameter-headed can face the DECODED @@ -671,11 +690,15 @@ elemSize (PiApp f e) = S (elemSize f + elemSize e) elemSize (SigmaIntro u v) = S (elemSize u + elemSize v) elemSize (SigmaElim1 t) = S (elemSize t) elemSize (SigmaElim2 t) = S (elemSize t) +elemSize (Inj1 t) = S (elemSize t) +elemSize (Inj2 t) = S (elemSize t) +elemSize (SumElim l r t) = S (elemSize l + elemSize r + elemSize t) elemSize Elem.ZeroTy = 1 elemSize Elem.OneTy = 1 elemSize Elem.NatTy = 1 elemSize (Elem.PiTy a b) = S (elemSize a + elemSize b) elemSize (Elem.SigmaTy a b) = S (elemSize a + elemSize b) +elemSize (Elem.SumTy a b) = S (elemSize a + elemSize b) elemSize (Elem.EqTy l r t) = S (elemSize l + elemSize r + tySize t) elemSize (QuotTy a r) = S (elemSize a + elemSize r) elemSize (SigVar _ es) = S (foldl (\acc, e => acc + elemSize e) 0 es) @@ -699,6 +722,7 @@ tySize Ty.UniverseTy = 1 tySize Ty.PropTy = 1 tySize (Ty.PiTy a b) = S (tySize a + tySize b) tySize (Ty.SigmaTy a b) = S (tySize a + tySize b) +tySize (Ty.SumTy a b) = S (tySize a + tySize b) tySize (El e) = S (elemSize e) tySize (Prf e) = S (elemSize e) tySize (Quotient a r) = S (tySize a + elemSize r) @@ -738,11 +762,15 @@ permutative c = isJust (go 0 c.lhs c.rhs []) go b (SigmaIntro u v) (SigmaIntro u' v') m = go b u u' m >>= go b v v' go b (SigmaElim1 t) (SigmaElim1 t') m = go b t t' m go b (SigmaElim2 t) (SigmaElim2 t') m = go b t t' m + go b (Inj1 t) (Inj1 t') m = go b t t' m + go b (Inj2 t) (Inj2 t') m = go b t t' m + go b (SumElim l r t) (SumElim l' r' t') m = go (1+b) l l' m >>= go (1+b) r r' >>= go b t t' go b Elem.ZeroTy Elem.ZeroTy m = Just m go b Elem.OneTy Elem.OneTy m = Just m go b Elem.NatTy Elem.NatTy m = Just m go b (Elem.PiTy a d) (Elem.PiTy a' d') m = go b a a' m >>= go (1+b) d d' go b (Elem.SigmaTy a d) (Elem.SigmaTy a' d') m = go b a a' m >>= go (1+b) d d' + go b (Elem.SumTy a d) (Elem.SumTy a' d') m = go b a a' m >>= go b d d' go b (Elem.EqTy l r t) (Elem.EqTy l' r' t') m = go b l l' m >>= go b r r' >>= goT b t t' go b (QuotTy a r) (QuotTy a' r') m = go b a a' m >>= go (2+b) r r' go b (SigVar x es) (SigVar x' es') m = @@ -773,6 +801,7 @@ permutative c = isJust (go 0 c.lhs c.rhs []) goT b Ty.PropTy Ty.PropTy m = Just m goT b (Ty.PiTy a d) (Ty.PiTy a' d') m = goT b a a' m >>= goT (1+b) d d' goT b (Ty.SigmaTy a d) (Ty.SigmaTy a' d') m = goT b a a' m >>= goT (1+b) d d' + goT b (Ty.SumTy a d) (Ty.SumTy a' d') m = goT b a a' m >>= goT b d d' goT b (El e) (El e') m = go b e e' m goT b (Prf e) (Prf e') m = go b e e' m goT b (Quotient a r) (Quotient a' r') m = goT b a a' m >>= go (2+b) r r' @@ -880,12 +909,21 @@ rewriteElemS side c pi d t = , at 1 0 v (\v' => SigmaIntro u v') ] descend (SigmaElim1 u) = at 0 0 u SigmaElim1 descend (SigmaElim2 u) = at 0 0 u SigmaElim2 + descend (Inj1 u) = at 0 0 u Inj1 + descend (Inj2 u) = at 0 0 u Inj2 + descend (SumElim l r u) = + first [ at 0 1 l (\l' => SumElim l' r u) + , at 1 1 r (\r' => SumElim l r' u) + , at 2 0 u (\u' => SumElim l r u') ] descend (Elem.PiTy a c') = first [ at 0 0 a (\a' => Elem.PiTy a' c') , at 1 1 c' (\c'' => Elem.PiTy a c'') ] descend (Elem.SigmaTy a c') = first [ at 0 0 a (\a' => Elem.SigmaTy a' c') , at 1 1 c' (\c'' => Elem.SigmaTy a c'') ] + descend (Elem.SumTy a c') = + first [ at 0 0 a (\a' => Elem.SumTy a' c') + , at 1 0 c' (\c'' => Elem.SumTy a c'') ] descend (Elem.EqTy l r u) = first [ at 0 0 l (\l' => Elem.EqTy l' r u) , at 1 0 r (\r' => Elem.EqTy l r' u) ] @@ -935,6 +973,9 @@ rewriteTyS side c pi d (Ty.PiTy a b) = rewriteTyS side c pi d (Ty.SigmaTy a b) = ((\(a', st) => (Ty.SigmaTy a' b, st)) <$> rewriteTyS side c (0 :: pi) d a) <|> ((\(b', st) => (Ty.SigmaTy a b', st)) <$> rewriteTyS side c (1 :: pi) (1 + d) b) +rewriteTyS side c pi d (Ty.SumTy a b) = + ((\(a', st) => (Ty.SumTy a' b, st)) <$> rewriteTyS side c (0 :: pi) d a) + <|> ((\(b', st) => (Ty.SumTy a b', st)) <$> rewriteTyS side c (1 :: pi) d b) rewriteTyS side c pi d (El e) = (\(e', st) => (El e', st)) <$> rewriteElemS side c (0 :: pi) d e rewriteTyS side c pi d (Quotient a r) = @@ -1048,6 +1089,9 @@ closeCand c = go (Elem.SigmaTy a0 b0) (Elem.SigmaTy a1 b1) = comp SelDom a0 a1 ++ closeCand (child (\bs => SelCod <$> lookup 0 bs) 1 [El a1] b0 b1) + go (Elem.SumTy a0 b0) (Elem.SumTy a1 b1) = + -- code-sum-inj: both components at 𝕌, neither under a binder + comp SelSumL a0 a1 ++ comp SelSumR b0 b1 go (QuotTy a0 r0) (QuotTy a1 r1) = comp SelQDom a0 a1 ++ closeCand (child (\bs => [| SelQRel (lookup 1 bs) (lookup 0 bs) |]) 2 @@ -1308,6 +1352,26 @@ mutual -- (pure computation) is safe to accept natFree : ECert -> Maybe (List Step) natFree c = if stepFree c then Just [] else Nothing + spCongC dep st cs ctx (Inj1 x) (Inj1 y) = + -- injection congruence: the component type is unknown here, so + -- only proof-free evidence (pure computation) is safe to accept — + -- like class above + prefixSteps 0 <$> (spEqElemC dep st cs ctx x y Ty.NatTy >>= natFree) + where + natFree : ECert -> Maybe (List Step) + natFree c = if stepFree c then Just [] else Nothing + spCongC dep st cs ctx (Inj2 x) (Inj2 y) = + prefixSteps 0 <$> (spEqElemC dep st cs ctx x y Ty.NatTy >>= natFree) + where + natFree : ECert -> Maybe (List Step) + natFree c = if stepFree c then Just [] else Nothing + spCongC dep st cs ctx (SumElim l r t) (SumElim l' r' t') = + -- ⊎-elim congruence at the scrutinee (like quot-elim's) + if l == l' && r == r' + then case inferNe st ctx t of + Just tyT => prefixSteps 2 <$> (spEqElemC dep st cs ctx t t' tyT >>= flatSteps) + _ => Nothing + else Nothing spCongC dep st cs ctx (Elem.PiTy a b) (Elem.PiTy a' b') = do stA <- spEqElemC dep st cs ctx a a' Ty.UniverseTy >>= flatSteps cB <- spEqElemC dep st (extendCS cs) (ctx :< El a') b b' Ty.UniverseTy @@ -1316,6 +1380,12 @@ mutual stA <- spEqElemC dep st cs ctx a a' Ty.UniverseTy >>= flatSteps cB <- spEqElemC dep st (extendCS cs) (ctx :< El a') b b' Ty.UniverseTy if stepFree cB then Just (prefixSteps 0 stA) else Nothing + spCongC dep st cs ctx (Elem.SumTy a b) (Elem.SumTy a' b') = do + -- non-dependent: BOTH components may carry steps (no binder to + -- take a Γ-level proof out of scope) + stA <- spEqElemC dep st cs ctx a a' Ty.UniverseTy >>= flatSteps + stB <- spEqElemC dep st cs ctx b b' Ty.UniverseTy >>= flatSteps + pure (prefixSteps 0 stA ++ prefixSteps 1 stB) spCongC dep st cs ctx (QuotTy a r) (QuotTy a' r') = do stA <- spEqElemC dep st cs ctx a a' Ty.UniverseTy >>= flatSteps cR <- spEqElemC dep st (extendCS (extendCS cs)) (ctx :< El a' :< substTy (El a') Wk) r r' Ty.PropTy @@ -1462,6 +1532,10 @@ mutual dc <- spEqTyC dep st cs ctx a0 a1 cc <- spEqTyC dep st (extendCS cs) (ctx :< a1) b0 b1 pure (MkECert base (FSigmaCong dc cc)) + congFinal (Ty.SumTy a0 b0) (Ty.SumTy a1 b1) base = do + lc <- spEqTyC dep st cs ctx a0 a1 + rc <- spEqTyC dep st cs ctx b0 b1 + pure (MkECert base (FSumCong lc rc)) congFinal (Ty.Quotient a0 r0) (Ty.Quotient a1 r1) base = if a0 == a1 then do @@ -1490,6 +1564,11 @@ mutual stA <- go a0 a1 sub <- spEqTyC dep st (extendCS cs) (ctx :< a1) b0 b1 if stepFree sub then Just (prefixSteps 0 stA) else Nothing + (Ty.SumTy a0 b0, Ty.SumTy a1 b1) => do + -- non-dependent: both components may carry steps + stA <- go a0 a1 + stB <- go b0 b1 + pure (prefixSteps 0 stA ++ prefixSteps 1 stB) (Ty.Quotient a0 r0, Ty.Quotient a1 r1) => do stA <- go a0 a1 sub <- spEqElemC dep st (extendCS (extendCS cs)) (ctx :< a1 :< substTy a1 Wk) r0 r1 Ty.PropTy @@ -1625,11 +1704,19 @@ mutual case zonkElem st t of SigmaIntro _ b => b t2 => SigmaElim2 t2 + zonkElem st (Inj1 t) = Inj1 (zonkElem st t) + zonkElem st (Inj2 t) = Inj2 (zonkElem st t) + zonkElem st (SumElim l r t) = + case zonkElem st t of + Inj1 a => zonkElem st (substElem l (Ext Id a)) + Inj2 b => zonkElem st (substElem r (Ext Id b)) + t2 => SumElim (zonkElem st l) (zonkElem st r) t2 zonkElem st Elem.ZeroTy = Elem.ZeroTy zonkElem st Elem.OneTy = Elem.OneTy zonkElem st Elem.NatTy = Elem.NatTy zonkElem st (Elem.PiTy a b) = Elem.PiTy (zonkElem st a) (zonkElem st b) zonkElem st (Elem.SigmaTy a b) = Elem.SigmaTy (zonkElem st a) (zonkElem st b) + zonkElem st (Elem.SumTy a b) = Elem.SumTy (zonkElem st a) (zonkElem st b) zonkElem st (Elem.EqTy l r t) = Elem.EqTy (zonkElem st l) (zonkElem st r) (zonkTy st t) zonkElem st (QuotTy a r) = QuotTy (zonkElem st a) (zonkElem st r) zonkElem st (Class a) = Class (zonkElem st a) @@ -1673,6 +1760,7 @@ mutual zonkTy st Ty.UniverseTy = Ty.UniverseTy zonkTy st (Ty.PiTy a b) = Ty.PiTy (zonkTy st a) (zonkTy st b) zonkTy st (Ty.SigmaTy a b) = Ty.SigmaTy (zonkTy st a) (zonkTy st b) + zonkTy st (Ty.SumTy a b) = Ty.SumTy (zonkTy st a) (zonkTy st b) zonkTy st (El e) = case zonkElem st e of Elem.ZeroTy => Ty.ZeroTy @@ -1680,6 +1768,7 @@ mutual Elem.NatTy => Ty.NatTy Elem.PiTy a b => Ty.PiTy (zonkTy st (El a)) (zonkTy st (El b)) Elem.SigmaTy a b => Ty.SigmaTy (zonkTy st (El a)) (zonkTy st (El b)) + Elem.SumTy a b => Ty.SumTy (zonkTy st (El a)) (zonkTy st (El b)) QuotTy a r => Quotient (zonkTy st (El a)) r e2 => El e2 zonkTy st PropTy = PropTy @@ -2260,6 +2349,10 @@ mutual or2 (uniE uctx u v) (uniE (uctx :< El v) c c') (Elem.SigmaTy u c, Elem.SigmaTy v c') => or2 (uniE uctx u v) (uniE (uctx :< El v) c c') + (Elem.SumTy u c, Elem.SumTy v c') => + or2 (uniE uctx u v) (uniE uctx c c') + (Inj1 u, Inj1 v) => uniE uctx u v + (Inj2 u, Inj2 v) => uniE uctx u v (Elem.EqTy l r t, Elem.EqTy l' r' t') => or2 (uniT uctx t t') (or2 (uniE uctx l l') (uniE uctx r r')) (QuotTy u r1, QuotTy v r2) => @@ -2279,6 +2372,7 @@ mutual (El u, El v) => uniE uctx u v (Ty.PiTy u c, Ty.PiTy v c') => or2 (uniT uctx u v) (uniT (uctx :< v) c c') (Ty.SigmaTy u c, Ty.SigmaTy v c') => or2 (uniT uctx u v) (uniT (uctx :< v) c c') + (Ty.SumTy u c, Ty.SumTy v c') => or2 (uniT uctx u v) (uniT uctx c c') (Quotient u r1, Quotient v r2) => or2 (uniT uctx u v) (uniE (uctx :< v :< substTy v Wk) r1 r2) (El u, v) => case codeOf v of @@ -2376,6 +2470,13 @@ mutual (SigmaIntro u v, SigmaIntro u' v', Ty.SigmaTy dom cod) => do ignore $ convElem ctx env site comp' u u' dom ignore $ convElem ctx env site comp' v v' (substTy cod (Ext Id u')) + -- injection decomposition — faithful (injection injectivity + -- is derivable); an inj₁/inj₂ HEAD MISMATCH falls through + -- and stays an obligation like every rigid mismatch + (Inj1 x, Inj1 y, Ty.SumTy dom _) => + ignore $ convElem ctx env site comp' x y dom + (Inj2 x, Inj2 y, Ty.SumTy _ cod) => + ignore $ convElem ctx env site comp' x y cod (Class x, Class y, Ty.Quotient dom rel) => -- witness path: an ∥≡∥-shaped relation reduces the class -- equation to its underlying equation (el-quot-eq after @@ -2390,6 +2491,10 @@ mutual (Elem.SigmaTy x c, Elem.SigmaTy x' c', Ty.UniverseTy) => do ignore $ convElem ctx env site comp' x x' Ty.UniverseTy ignore $ convElem (ctx :< El x') (env :< "x") site comp' c c' Ty.UniverseTy + (Elem.SumTy x c, Elem.SumTy x' c', Ty.UniverseTy) => do + -- code-sum-inj: both components at 𝕌 over Γ (no binder) + ignore $ convElem ctx env site comp' x x' Ty.UniverseTy + ignore $ convElem ctx env site comp' c c' Ty.UniverseTy (QuotTy x r, QuotTy x' r', Ty.UniverseTy) => do ignore $ convElem ctx env site comp' x x' Ty.UniverseTy ignore $ convElem (ctx :< El x' :< substTy (El x') Wk) (env :< "x" :< "y") site comp' r r' Ty.PropTy @@ -2484,6 +2589,10 @@ mutual (Ty.SigmaTy a0 b0, Ty.SigmaTy a1 b1) => do ignore $ convTy ctx env site comp' a0 a1 ignore $ convTy (ctx :< a1) (env :< "x") site comp' b0 b1 + (Ty.SumTy a0 b0, Ty.SumTy a1 b1) => do + -- ty-sum-inj: both components over Γ — faithful + ignore $ convTy ctx env site comp' a0 a1 + ignore $ convTy ctx env site comp' b0 b1 (Ty.Quotient a0 r0, Ty.Quotient a1 r1) => do ignore $ convTy ctx env site comp' a0 a1 ignore $ convElem (ctx :< a1 :< substTy a1 Wk) (env :< "x" :< "y") site comp' r0 r1 Ty.PropTy @@ -2545,6 +2654,12 @@ preferSigma st ctx ty = case rwNfTy st ctx ty of tyX@(Ty.SigmaTy a b) => (\e => (a, b, Just e)) <$> exposeCert st ctx ty tyX _ => Nothing +preferSum : ElabSt -> Ctx -> Ty -> Maybe (Ty, Ty, Maybe (Ty, ECert)) +preferSum st ctx (Ty.SumTy a b) = Just (a, b, Nothing) +preferSum st ctx ty = case rwNfTy st ctx ty of + tyX@(Ty.SumTy a b) => (\e => (a, b, Just e)) <$> exposeCert st ctx ty tyX + _ => Nothing + preferQuot : ElabSt -> Ctx -> Ty -> Maybe (Ty, Elem, Maybe (Ty, ECert)) preferQuot st ctx (Ty.Quotient a r) = Just (a, r, Nothing) preferQuot st ctx ty = case rwNfTy st ctx ty of @@ -2588,6 +2703,10 @@ mutual (a', aSk) <- elabTy ctx env site a (b', bSk) <- elabTy (ctx :< a') (env :< x) site b pure (Ty.SigmaTy a' b', Nd [] [aSk, bSk]) + elabTy ctx env site (STySum a b) = do + (a', aSk) <- elabTy ctx env site a + (b', bSk) <- elabTy ctx env site b + pure (Ty.SumTy a' b', Nd [] [aSk, bSk]) elabTy ctx env site (STyQuot a (nx, nxr) (ny, nyr) r) = do (a', aSk) <- elabTy ctx env site a recordBinder nxr ctx env nx a' @@ -2705,6 +2824,22 @@ mutual (t', tSk) <- checkElem ctx env site t Ty.NatTy pure (NatElim z' s' t', substTy motTy (Ext Id t'), Nd [PMotive motTy motSk] [zSk, sSk, tSk]) + inferElem ctx env site (SSumElim (zn, zr) mot (an, ar) l (bn, br) r t) = do + (t', tTy, tSk) <- inferElem ctx env site t + st <- getSt + case preferSum st ctx tTy of + Just (a, b, _) => do + recordBinder zr ctx env zn (Ty.SumTy a b) + (motTy, motSk) <- elabTy (ctx :< Ty.SumTy a b) (env :< zn) site mot + recordBinder ar ctx env an a + (l', lSk) <- checkElem (ctx :< a) (env :< an) site l + (substTy motTy (Ext Wk (Inj1 (CtxVar 0)))) + recordBinder br ctx env bn b + (r', rSk) <- checkElem (ctx :< b) (env :< bn) site r + (substTy motTy (Ext Wk (Inj2 (CtxVar 0)))) + pure (SumElim l' r' t', substTy motTy (Ext Id t'), + Nd [PMotive motTy motSk] [lSk, rSk, tSk]) + Nothing => throw "\{site}: ⊎-elim scrutinee has non-⊎ type\{structuralHint}" inferElem ctx env site (SQuotElim (zn, zr) mot (an, ar) f q) = do (q', qTy, qSk) <- inferElem ctx env site q st <- getSt @@ -2737,6 +2872,10 @@ mutual (a', aSk) <- checkElem ctx env site a Ty.UniverseTy (b', bSk) <- checkElem (ctx :< El a') (env :< x) site b Ty.UniverseTy pure (Elem.SigmaTy a' b', Ty.UniverseTy, Nd [] [aSk, bSk]) + inferElem ctx env site (SSumC a b) = do + (a', aSk) <- checkElem ctx env site a Ty.UniverseTy + (b', bSk) <- checkElem ctx env site b Ty.UniverseTy + pure (Elem.SumTy a' b', Ty.UniverseTy, Nd [] [aSk, bSk]) inferElem ctx env site (SQuotC a (nx, nxr) (ny, nyr) r) = do (a', aSk) <- checkElem ctx env site a Ty.UniverseTy recordBinder nxr ctx env nx (El a') @@ -2759,6 +2898,10 @@ mutual (l', lSk) <- checkElem ctx env site l t' (r', rSk) <- checkElem ctx env site r t' pure (Elem.EqTy l' r' t', Ty.PropTy, Nd [] [lSk, rSk, tSk]) + inferElem ctx env site (SInj1 _) = + throw "\{site}: cannot infer the type of inj₁ (the other summand is undetermined)\{structuralHint}" + inferElem ctx env site (SInj2 _) = + throw "\{site}: cannot infer the type of inj₂ (the other summand is undetermined)\{structuralHint}" inferElem ctx env site (SLam _ _) = throw "\{site}: cannot infer the type of a λ\{structuralHint}" inferElem ctx env site (SPair _ _) = @@ -2786,6 +2929,20 @@ mutual (v', vSk) <- checkElem ctx env site v (substTy b (Ext Id u')) pure (SigmaIntro u' v', withExpose exp (Nd [] [uSk, vSk])) Nothing => throw "\{site}: pair checked against a non-⨯ type\{structuralHint}" + checkElem ctx env site (SInj1 a) ty = do + st <- getSt + case preferSum st ctx ty of + Just (dom, _, exp) => do + (a', aSk) <- checkElem ctx env site a dom + pure (Inj1 a', withExpose exp (Nd [] [aSk])) + Nothing => throw "\{site}: inj₁ checked against a non-⊎ type\{structuralHint}" + checkElem ctx env site (SInj2 b) ty = do + st <- getSt + case preferSum st ctx ty of + Just (_, cod, exp) => do + (b', bSk) <- checkElem ctx env site b cod + pure (Inj2 b', withExpose exp (Nd [] [bSk])) + Nothing => throw "\{site}: inj₂ checked against a non-⊎ type\{structuralHint}" checkElem ctx env site (SClass a) ty = do st <- getSt case preferQuot st ctx ty of diff --git a/src/idris/Nova/Elaboration/Named.idr b/src/idris/Nova/Elaboration/Named.idr index a9c8c22d..797f864b 100644 --- a/src/idris/Nova/Elaboration/Named.idr +++ b/src/idris/Nova/Elaboration/Named.idr @@ -200,6 +200,7 @@ mutual usesIndexTy k Ty.UniverseTy = False usesIndexTy k (Ty.PiTy a b) = usesIndexTy k a || usesIndexTy (S k) b usesIndexTy k (Ty.SigmaTy a b) = usesIndexTy k a || usesIndexTy (S k) b + usesIndexTy k (Ty.SumTy a b) = usesIndexTy k a || usesIndexTy k b usesIndexTy k (El e) = usesIndexElem k e usesIndexTy k PropTy = False usesIndexTy k (Prf e) = usesIndexElem k e @@ -234,11 +235,15 @@ mutual usesIndexElem k (SigmaIntro e e') = usesIndexElem k e || usesIndexElem k e' usesIndexElem k (SigmaElim1 e) = usesIndexElem k e usesIndexElem k (SigmaElim2 e) = usesIndexElem k e + usesIndexElem k (Inj1 e) = usesIndexElem k e + usesIndexElem k (Inj2 e) = usesIndexElem k e + usesIndexElem k (SumElim l r t) = usesIndexElem (S k) l || usesIndexElem (S k) r || usesIndexElem k t usesIndexElem k Elem.ZeroTy = False usesIndexElem k Elem.OneTy = False usesIndexElem k Elem.NatTy = False usesIndexElem k (Elem.PiTy e e') = usesIndexElem k e || usesIndexElem (S k) e' usesIndexElem k (Elem.SigmaTy e e') = usesIndexElem k e || usesIndexElem (S k) e' + usesIndexElem k (Elem.SumTy e e') = usesIndexElem k e || usesIndexElem k e' usesIndexElem k (Elem.EqTy e0 e1 t2) = usesIndexElem k e0 || usesIndexElem k e1 || usesIndexTy k t2 usesIndexElem k (QuotTy a r) = usesIndexElem k a || usesIndexElem (S (S k)) r usesIndexElem k (SigVar x es) = usesIndexSubNorm k es @@ -306,6 +311,7 @@ mutual then let x = freshGeneric env in "(" ++ x ++ ":" ++ prettyElemN tbl env e ++ ") ⨯ " ++ prettyElemNoCommaN tbl (env :< x) e' else prettyElemOpN tbl env 0 e ++ " ⨯ " ++ prettyElemNoCommaN tbl (env :< wildcard) e' + prettyElemNoCommaN tbl env e@(Elem.SumTy _ _) = prettyElemSumN tbl env e prettyElemNoCommaN tbl env (Elem.EqTy e0 e1 t2) = prettyElemOpN tbl env 0 e0 ++ " ≡ " ++ prettyElemOpN tbl env 0 e1 ++ " ∈ " ++ prettyTyArrowN tbl env t2 prettyElemNoCommaN tbl env (QuotTy e r) = @@ -314,6 +320,14 @@ mutual in prettyElemOpN tbl env 0 e ++ " / (" ++ x ++ " " ++ y ++ ". " ++ prettyElemNoCommaN tbl (env :< x :< y) r ++ ")" prettyElemNoCommaN tbl env e = prettyElemOpN tbl env 0 e + -- the ⊎ code binds tighter than the other infix element formers + -- (chain at its own level; any non-sum component prints at the + -- operator level, which parenthesizes arrows and pairs) + prettyElemSumN : FixTable -> NameEnv -> Elem -> String + prettyElemSumN tbl env (Elem.SumTy e e') = + prettyElemOpN tbl env 0 e ++ " ⊎ " ++ prettyElemSumN tbl env e' + prettyElemSumN tbl env e = prettyElemOpN tbl env 0 e + -- t{1½}: operator applications, precedence-aware — parenthesized -- exactly when the operator binds looser than the context demands. -- An operator with no fixity in scope falls through to the prefix @@ -344,6 +358,14 @@ mutual in "ℕ-elim " ++ prettyElemAtomN tbl env z ++ " (" ++ n ++ " " ++ ih ++ ". " ++ prettyElemAtomN tbl (env :< n :< ih) s ++ ") " ++ prettyElemAtomN tbl env t + prettyElemPrefixN tbl env (Inj1 a) = "inj₁ " ++ prettyElemAtomN tbl env a + prettyElemPrefixN tbl env (Inj2 a) = "inj₂ " ++ prettyElemAtomN tbl env a + prettyElemPrefixN tbl env (SumElim l r t) = + let a = if usesIndexElem 0 l then freshGeneric env else wildcard + b = if usesIndexElem 0 r then freshGeneric env else wildcard + in "⊎-elim (" ++ a ++ ". " ++ prettyElemN tbl (env :< a) l ++ ") (" + ++ b ++ ". " ++ prettyElemN tbl (env :< b) r ++ ") " + ++ prettyElemAtomN tbl env t prettyElemPrefixN tbl env (Class a) = "class " ++ prettyElemAtomN tbl env a prettyElemPrefixN tbl env (QuotElim f q) = let a = if usesIndexElem 0 f then freshGeneric env else wildcard @@ -440,12 +462,20 @@ mutual then let x = freshForTy a env in "(" ++ x ++ ":" ++ prettyTyN tbl env a ++ ") ⨯ " ++ prettyTyArrowN tbl (env :< x) b else prettyTyElN tbl env a ++ " ⨯ " ++ prettyTyArrowN tbl (env :< wildcard) b + prettyTyArrowN tbl env ty@(Ty.SumTy _ _) = prettyTySumN tbl env ty prettyTyArrowN tbl env (Ty.Quotient a r) = let x = freshForTy a env y = freshGeneric (env :< x) in prettyTyElN tbl env a ++ " / (" ++ x ++ " " ++ y ++ ". " ++ prettyElemNoCommaN tbl (env :< x :< y) r ++ ")" prettyTyArrowN tbl env ty = prettyTyElN tbl env ty + -- ⊎ binds tighter than → ⨯ / (its own level; non-sum components + -- print at the El level, which parenthesizes looser forms) + prettyTySumN : FixTable -> NameEnv -> Ty -> String + prettyTySumN tbl env (Ty.SumTy a b) = + prettyTyElN tbl env a ++ " ⊎ " ++ prettyTySumN tbl env b + prettyTySumN tbl env ty = prettyTyElN tbl env ty + prettyTyElN : FixTable -> NameEnv -> Ty -> String prettyTyElN tbl env (El e) = "El " ++ prettyElemAtomN tbl env e prettyTyElN tbl env (Prf e) = "Prf " ++ prettyElemAtomN tbl env e diff --git a/src/idris/Nova/Elaboration/Parser.idr b/src/idris/Nova/Elaboration/Parser.idr index e46c5b23..96471953 100644 --- a/src/idris/Nova/Elaboration/Parser.idr +++ b/src/idris/Nova/Elaboration/Parser.idr @@ -184,12 +184,20 @@ mutual sp (do kw "→"; sp; b <- parseSTy tbl env'; pure (foldGroups STyPi groups b)) <|> (do kw "⨯"; sp; b <- parseSTy tbl env'; pure (foldGroups STySigma groups b))) - <|> (do a <- parseSTyEl tbl env + <|> (do a <- parseSTySum tbl env (do sp; kw "→"; sp; b <- parseSTy tbl (env :< wildcard); pure (STyPi wildcard a b)) <|> (do sp; kw "⨯"; sp; b <- parseSTy tbl (env :< wildcard); pure (STySigma wildcard a b)) <|> (do sp; kw "/"; sp; (x, y, r) <- parseQuotRel tbl env; pure (STyQuot a x y r)) <|> pure a) + -- T{1½}: ⊎ — non-dependent, right-assoc, binds TIGHTER than → ⨯ / + -- (Agda's convention: A ⊎ B → C is (A ⊎ B) → C) + parseSTySum : FixTable -> NameEnv -> Rule STy + parseSTySum tbl env = do + a <- parseSTyEl tbl env + (do sp; kw "⊎"; sp; b <- parseSTySum tbl env; pure (STySum a b)) + <|> pure a + -- one or more (x:T) groups, each scoping over the ones after it parseBinderGroups : FixTable -> NameEnv -> Rule (NameEnv, List (String, STy)) parseBinderGroups tbl env = do @@ -246,16 +254,24 @@ mutual sp (do kw "→"; sp; b <- parseSElemNoComma tbl env'; pure (foldGroups SPiC groups b)) <|> (do kw "⨯"; sp; b <- parseSElemNoComma tbl env'; pure (foldGroups SSigmaC groups b))) - <|> (do e <- parseSElemOp tbl env + <|> (do e <- parseSElemSumC tbl env (do sp; kw "→"; sp; e' <- parseSElemNoComma tbl (env :< wildcard); pure (SPiC wildcard e e')) <|> (do sp; kw "⨯"; sp; e' <- parseSElemNoComma tbl (env :< wildcard); pure (SSigmaC wildcard e e')) <|> (do sp; kw "/"; sp; (x, y, r) <- parseQuotRelC tbl env; pure (SQuotC e x y r)) <|> (do sp; kw "≡"; sp - e1 <- parseSElemOp tbl env; sp; kw "∈"; sp + e1 <- parseSElemSumC tbl env; sp; kw "∈"; sp t2 <- parseSTyEl tbl env pure (SEqC e e1 t2)) <|> pure e) + -- t{1¼}: the ⊎ code — like the ⊎ type, tighter than the other + -- infix code formers + parseSElemSumC : FixTable -> NameEnv -> Rule SElem + parseSElemSumC tbl env = do + e <- parseSElemOp tbl env + (do sp; kw "⊎"; sp; e' <- parseSElemSumC tbl env; pure (SSumC e e')) + <|> pure e + -- t{1½}: declared infix operators — precedence climbing over the -- fixity table. An operator token is a NAME; infix use is -- application of it. @@ -313,6 +329,17 @@ mutual t <- parseSElemAtom tbl env pure (SNatElim n mot z n2 ih s t)) <|> (do kw "S"; space; e <- parseSElemAtom tbl env; pure (SSuc e)) + <|> (do kw "inj₁"; space; e <- parseSElemAtom tbl env; pure (SInj1 e)) + <|> (do kw "inj₂"; space; e <- parseSElemAtom tbl env; pure (SInj2 e)) + <|> (do kw "⊎-elim"; space + kwc '('; sp; z <- parseNameR; sp; kwc '.'; sp + mot <- parseSTy tbl (env :< fst z); sp; kwc ')'; sp + kwc '('; sp; a <- parseNameR; sp; kwc '.'; sp + l <- parseSElem tbl (env :< fst a); sp; kwc ')'; sp + kwc '('; sp; b <- parseNameR; sp; kwc '.'; sp + r <- parseSElem tbl (env :< fst b); sp; kwc ')'; sp + t <- parseSElemAtom tbl env + pure (SSumElim z mot a l b r t)) <|> (do kw "class"; space; e <- parseSElemAtom tbl env; pure (SClass e)) <|> (do kw "quot-elim"; space kwc '('; sp; z <- parseNameR; sp; kwc '.'; sp diff --git a/src/idris/Nova/Elaboration/Surface.idr b/src/idris/Nova/Elaboration/Surface.idr index 79b8639a..f1eb8a3d 100644 --- a/src/idris/Nova/Elaboration/Surface.idr +++ b/src/idris/Nova/Elaboration/Surface.idr @@ -36,6 +36,8 @@ mutual STyPi : (name : String) -> STy -> STy -> STy ||| (x:T) ⨯ U STySigma : (name : String) -> STy -> STy -> STy + ||| T ⊎ U — non-dependent, no binder + STySum : STy -> STy -> STy ||| T / (x y. r) — r is an Ω-valued element STyQuot : STy -> (nx, ny : SName) -> SElem -> STy ||| t ≡ t ∈ T @@ -76,6 +78,8 @@ mutual SPiC : (name : String) -> SElem -> SElem -> SElem ||| (x:t) ⨯ u (code) SSigmaC : (name : String) -> SElem -> SElem -> SElem + ||| t ⊎ u (code — non-dependent, no binder) + SSumC : SElem -> SElem -> SElem ||| t / (x y. r) (code) SQuotC : SElem -> (nx, ny : SName) -> SElem -> SElem ||| t ≡ t ∈ T — the equality PROP (an Ω-element; the ∈-slot @@ -84,6 +88,12 @@ mutual SZeroElim : SElem -> SElem ||| ℕ-elim (n. T) z (n ih. s) t — motive-first SNatElim : (n : SName) -> STy -> SElem -> (n2, ih : SName) -> SElem -> SElem -> SElem + ||| inj₁ t / inj₂ t — sum introductions + SInj1 : SElem -> SElem + SInj2 : SElem -> SElem + ||| ⊎-elim (z. T) (a. l) (b. r) t — motive, left case, right + ||| case, scrutinee + SSumElim : (z : SName) -> STy -> (a : SName) -> SElem -> (b : SName) -> SElem -> SElem -> SElem SClass : SElem -> SElem ||| quot-elim (z. T) (a. f) q — motive-first SQuotElim : (z : SName) -> STy -> (a : SName) -> SElem -> SElem -> SElem @@ -228,6 +238,7 @@ mutual show (STySig x) = "\{x}" show (STyPi x a b) = "Pi \{x} (\{show a}) (\{show b})" show (STySigma x a b) = "Sigma \{x} (\{show a}) (\{show b})" + show (STySum a b) = "Sum (\{show a}) (\{show b})" show (STyQuot a x y r) = "Quot (\{show a}) \{fst x} \{fst y} (\{show r})" show (STyEq l r t) = "Eq (\{show l}) (\{show r}) (\{show t})" show (STyEl e) = "El (\{show e})" @@ -252,11 +263,16 @@ mutual show SNatC = "ℕc" show (SPiC x a b) = "PiC \{x} (\{show a}) (\{show b})" show (SSigmaC x a b) = "SigmaC \{x} (\{show a}) (\{show b})" + show (SSumC a b) = "SumC (\{show a}) (\{show b})" show (SQuotC a x y r) = "QuotC (\{show a}) \{fst x} \{fst y} (\{show r})" show (SEqC l r t) = "EqC (\{show l}) (\{show r}) (\{show t})" show (SZeroElim t) = "ZeroElim (\{show t})" show (SNatElim n mot z n2 ih s t) = "NatElim \{fst n} (\{show mot}) (\{show z}) \{fst n2} \{fst ih} (\{show s}) (\{show t})" + show (SInj1 t) = "Inj1 (\{show t})" + show (SInj2 t) = "Inj2 (\{show t})" + show (SSumElim z mot a l b r t) = + "SumElim \{fst z} (\{show mot}) \{fst a} (\{show l}) \{fst b} (\{show r}) (\{show t})" show (SClass t) = "Class (\{show t})" show (SQuotElim z mot a f q) = "QuotElim \{fst z} (\{show mot}) \{fst a} (\{show f}) (\{show q})" diff --git a/src/idris/Nova/Kernel.idr b/src/idris/Nova/Kernel.idr index dc3a2e70..e806a129 100644 --- a/src/idris/Nova/Kernel.idr +++ b/src/idris/Nova/Kernel.idr @@ -39,6 +39,9 @@ data Sel : Type where SelSuc : Sel -- S x ≐ S y ⇒ x ≐ y : ℕ SelDom : Sel -- (a₀→b₀) ≐ (a₁→b₁) : 𝕌 ⇒ a₀ ≐ a₁ : 𝕌 (also ⨯) SelCod : Elem -> Sel -- ⇒ b₀[id,u] ≐ b₁[id,u] : 𝕌 (also ⨯) + SelSumL : Sel -- (a₀⊎b₀) ≐ (a₁⊎b₁) : 𝕌 ⇒ a₀ ≐ a₁ : 𝕌 + SelSumR : Sel -- ⇒ b₀ ≐ b₁ : 𝕌 (non-dependent: no + -- binder, no instantiation element) SelQDom : Sel -- (a₀/r₀) ≐ (a₁/r₁) : 𝕌 ⇒ a₀ ≐ a₁ : 𝕌 SelQRel : Elem -> Elem -> Sel -- ⇒ r₀[id,u,v] ≐ r₁[id,u,v] : 𝕌 SelQIdx : Nat -> Sel -- 𝒮.s ē₀ ≐ 𝒮.s ē₁ : 𝕌 ⇒ ē₀ᵢ ≐ ē₁ᵢ (QIIT @@ -140,6 +143,10 @@ mutual FPiCong : ECert -> ECert -> Final ||| ty-sigma-cong, same shape FSigmaCong : ECert -> ECert -> Final + ||| ty-sum-cong, componentwise — both components over Γ (no + ||| binder to cross), needed when a component's equality is + ||| extensional and cannot flatten into steps + FSumCong : ECert -> ECert -> Final public export record ECert where @@ -234,11 +241,22 @@ mutual case t' of SigmaIntro _ b => do burn; pure b _ => pure (SigmaElim2 t') + kElem sig (Inj1 t) = Inj1 <$> kElem sig t + kElem sig (Inj2 t) = Inj2 <$> kElem sig t + kElem sig (SumElim l r t) = do + l' <- kElem sig l + r' <- kElem sig r + t' <- kElem sig t + case t' of + Inj1 a => do burn; kElem sig (substElem l' (Ext Id a)) + Inj2 b => do burn; kElem sig (substElem r' (Ext Id b)) + _ => pure (SumElim l' r' t') kElem sig Elem.ZeroTy = pure Elem.ZeroTy kElem sig Elem.OneTy = pure Elem.OneTy kElem sig Elem.NatTy = pure Elem.NatTy kElem sig (Elem.PiTy a b) = [| Elem.PiTy (kElem sig a) (kElem sig b) |] kElem sig (Elem.SigmaTy a b) = [| Elem.SigmaTy (kElem sig a) (kElem sig b) |] + kElem sig (Elem.SumTy a b) = [| Elem.SumTy (kElem sig a) (kElem sig b) |] kElem sig (Elem.EqTy l r t) = [| Elem.EqTy (kElem sig l) (kElem sig r) (kTy sig t) |] kElem sig (QuotTy a r) = [| QuotTy (kElem sig a) (kElem sig r) |] kElem sig (SigVar x es) = do @@ -307,6 +325,7 @@ mutual kTy sig Ty.UniverseTy = pure Ty.UniverseTy kTy sig (Ty.PiTy a b) = [| Ty.PiTy (kTy sig a) (kTy sig b) |] kTy sig (Ty.SigmaTy a b) = [| Ty.SigmaTy (kTy sig a) (kTy sig b) |] + kTy sig (Ty.SumTy a b) = [| Ty.SumTy (kTy sig a) (kTy sig b) |] kTy sig (El e) = do e' <- kElem sig e case e' of @@ -315,6 +334,7 @@ mutual Elem.NatTy => do burn; pure Ty.NatTy Elem.PiTy a b => do burn; kTy sig (Ty.PiTy (El a) (El b)) Elem.SigmaTy a b => do burn; kTy sig (Ty.SigmaTy (El a) (El b)) + Elem.SumTy a b => do burn; kTy sig (Ty.SumTy (El a) (El b)) QuotTy a r => do burn; kTy sig (Quotient (El a) r) QSortC sg k es => do burn; pure (QSort sg k es) -- ty-el-qiit _ => pure (El e') @@ -380,6 +400,14 @@ mutual _ => Left "kernel: bad path" pathE (i :: p) b f (SigmaElim1 t) = if i == 0 then SigmaElim1 <$> pathE p b f t else Left "kernel: bad path" pathE (i :: p) b f (SigmaElim2 t) = if i == 0 then SigmaElim2 <$> pathE p b f t else Left "kernel: bad path" + pathE (i :: p) b f (Inj1 t) = if i == 0 then Inj1 <$> pathE p b f t else Left "kernel: bad path" + pathE (i :: p) b f (Inj2 t) = if i == 0 then Inj2 <$> pathE p b f t else Left "kernel: bad path" + pathE (i :: p) b f (SumElim l r t) = + case i of + 0 => (\l' => SumElim l' r t) <$> pathE p (1 + b) f l + 1 => (\r' => SumElim l r' t) <$> pathE p (1 + b) f r + 2 => (\t' => SumElim l r t') <$> pathE p b f t + _ => Left "kernel: bad path" pathE (i :: p) b f (Elem.PiTy a c) = case i of 0 => (\a' => Elem.PiTy a' c) <$> pathE p b f a @@ -390,6 +418,11 @@ mutual 0 => (\a' => Elem.SigmaTy a' c) <$> pathE p b f a 1 => (\c' => Elem.SigmaTy a c') <$> pathE p (1 + b) f c _ => Left "kernel: bad path" + pathE (i :: p) b f (Elem.SumTy a c) = + case i of + 0 => (\a' => Elem.SumTy a' c) <$> pathE p b f a + 1 => (\c' => Elem.SumTy a c') <$> pathE p b f c + _ => Left "kernel: bad path" pathE (i :: p) b f (Elem.EqTy l r t) = case i of 0 => (\l' => Elem.EqTy l' r t) <$> pathE p b f l @@ -429,6 +462,10 @@ mutual 0 => (\a' => Ty.SigmaTy a' c) <$> pathT p b f a 1 => (\c' => Ty.SigmaTy a c') <$> pathT p (1 + b) f c _ => Left "kernel: bad path" + pathT (i :: p) b f (Ty.SumTy a c) = + case i of + 0 => (\a' => Ty.SumTy a' c) <$> pathT p b f a + 1 => (\c' => Ty.SumTy a c') <$> pathT p b f c _ => Left "kernel: bad path" pathT (i :: p) b f (El e) = if i == 0 then El <$> pathE p b f e else Left "kernel: bad path" pathT (i :: p) b f (Prf e) = if i == 0 then Prf <$> pathE p b f e else Left "kernel: bad path" @@ -516,6 +553,10 @@ mutual checkP sig ctx a Ty.UniverseTy checkP sig (ctx :< El a) b Ty.UniverseTy pure Ty.UniverseTy + inferP sig ctx (Elem.SumTy a b) = do + checkP sig ctx a Ty.UniverseTy + checkP sig ctx b Ty.UniverseTy + pure Ty.UniverseTy inferP sig ctx (QuotTy a r) = do checkP sig ctx a Ty.UniverseTy checkP sig (ctx :< El a :< substTy (El a) Wk) r Ty.PropTy @@ -637,6 +678,26 @@ mutual case ty' of Ty.SigmaTy a b => do checkP sig ctx u a; checkP sig ctx v (substTy b (Ext Id u)) _ => kerr "kernel: pair proof at non-⨯ type" + -- el-sum-i₁ / el-sum-i₂ as proof arguments + checkP sig ctx (Inj1 a) ty = do + ty' <- kTy sig ty + case ty' of + Ty.SumTy dom _ => checkP sig ctx a dom + _ => kerr "kernel: inj₁ proof at non-⊎ type" + checkP sig ctx (Inj2 b) ty = do + ty' <- kTy sig ty + case ty' of + Ty.SumTy _ cod => checkP sig ctx b cod + _ => kerr "kernel: inj₂ proof at non-⊎ type" + -- ⊎-elim with a CONSTANT motive (approximation A1): the el-sum-e + -- instance whose motive is T[↑]; the scrutinee's ⊎-type is inferred + checkP sig ctx (SumElim l r t) ty = do + tTy <- inferP sig ctx t >>= kTy sig + case tTy of + Ty.SumTy a b => do + checkP sig (ctx :< a) l (substTy ty Wk) + checkP sig (ctx :< b) r (substTy ty Wk) + _ => kerr "kernel: ⊎-elim proof scrutinee at non-⊎ type" -- el-qiit-intro as a proof argument (spec §3): the saturated -- constructor at its sort, the term's signature nf-identical to the -- type's, spine checked entrywise, indices compared @@ -750,6 +811,9 @@ mutual checkTyP sig ctx (Ty.SigmaTy a b) = do checkTyP sig ctx a checkTyP sig (ctx :< a) b + checkTyP sig ctx (Ty.SumTy a b) = do + checkTyP sig ctx a + checkTyP sig ctx b checkTyP sig ctx (El e) = checkP sig ctx e Ty.UniverseTy checkTyP sig ctx (Prf p) = checkP sig ctx p Ty.PropTy checkTyP sig ctx (Quotient a r) = do @@ -807,6 +871,9 @@ applySel sig ctx (l, r, _) sel = do (SelCod u, Elem.SigmaTy _ b0, Elem.SigmaTy a1 b1) => do checkP sig ctx u (El a1) pure (substElem b0 (Ext Id u), substElem b1 (Ext Id u), Ty.UniverseTy) + -- code-sum-inj: non-dependent, both components at 𝕌 directly + (SelSumL, Elem.SumTy a0 _, Elem.SumTy a1 _) => pure (a0, a1, Ty.UniverseTy) + (SelSumR, Elem.SumTy _ b0, Elem.SumTy _ b1) => pure (b0, b1, Ty.UniverseTy) (SelQDom, QuotTy a0 _, QuotTy a1 _) => pure (a0, a1, Ty.UniverseTy) -- code-quot-inj: the relation components live at Ω (SelQRel u v, QuotTy _ r0, QuotTy a1 r1) => do @@ -959,6 +1026,21 @@ mutual _ => pure Nothing childTyE sig ctx pexp (SigmaElim1 u) 0 = inferNeK sig ctx u childTyE sig ctx pexp (SigmaElim2 u) 0 = inferNeK sig ctx u + childTyE sig ctx (Just pe) (Inj1 _) 0 = do + t <- kTy sig pe + case t of + Ty.SumTy a _ => pure (Just a) + _ => pure Nothing + childTyE sig ctx (Just pe) (Inj2 _) 0 = do + t <- kTy sig pe + case t of + Ty.SumTy _ b => pure (Just b) + _ => pure Nothing + -- ⊎-elim: the case positions are motive-dependent (undetermined); + -- the scrutinee's type is neutrally inferable + childTyE sig ctx pexp (SumElim _ _ t) 2 = inferNeK sig ctx t + childTyE sig ctx pexp (Elem.SumTy _ _) 0 = pure (Just Ty.UniverseTy) + childTyE sig ctx pexp (Elem.SumTy _ _) 1 = pure (Just Ty.UniverseTy) childTyE sig ctx pexp (Elem.PiTy _ _) 0 = pure (Just Ty.UniverseTy) childTyE sig ctx pexp (Elem.PiTy _ _) 1 = pure (Just Ty.UniverseTy) childTyE sig ctx pexp (Elem.SigmaTy _ _) 0 = pure (Just Ty.UniverseTy) @@ -1078,12 +1160,19 @@ goE sig ctx lic (i :: p) b mexp u = do (PiApp f e, 1) => PiApp f <$> goE sig ctx lic p b childTy e (SigmaElim1 t', 0) => SigmaElim1 <$> goE sig ctx lic p b childTy t' (SigmaElim2 t', 0) => SigmaElim2 <$> goE sig ctx lic p b childTy t' + (Inj1 t', 0) => Inj1 <$> goE sig ctx lic p b childTy t' + (Inj2 t', 0) => Inj2 <$> goE sig ctx lic p b childTy t' + (SumElim l r t', 0) => (\l' => SumElim l' r t') <$> goE sig ctx lic p (1 + b) childTy l + (SumElim l r t', 1) => (\r' => SumElim l r' t') <$> goE sig ctx lic p (1 + b) childTy r + (SumElim l r t', 2) => SumElim l r <$> goE sig ctx lic p b childTy t' (SigmaIntro x y, 0) => (\x' => SigmaIntro x' y) <$> goE sig ctx lic p b childTy x (SigmaIntro x y, 1) => SigmaIntro x <$> goE sig ctx lic p b childTy y (Elem.PiTy a c, 0) => (\a' => Elem.PiTy a' c) <$> goE sig ctx lic p b childTy a (Elem.PiTy a c, 1) => Elem.PiTy a <$> goE sig ctx lic p (1 + b) childTy c (Elem.SigmaTy a c, 0) => (\a' => Elem.SigmaTy a' c) <$> goE sig ctx lic p b childTy a (Elem.SigmaTy a c, 1) => Elem.SigmaTy a <$> goE sig ctx lic p (1 + b) childTy c + (Elem.SumTy a c, 0) => (\a' => Elem.SumTy a' c) <$> goE sig ctx lic p b childTy a + (Elem.SumTy a c, 1) => Elem.SumTy a <$> goE sig ctx lic p b childTy c (Elem.EqTy l r t', 0) => (\l' => Elem.EqTy l' r t') <$> goE sig ctx lic p b childTy l (Elem.EqTy l r t', 1) => (\r' => Elem.EqTy l r' t') <$> goE sig ctx lic p b childTy r (Elem.EqTy l r t', 2) => Elem.EqTy l r <$> goTy sig ctx lic p b t' @@ -1129,6 +1218,11 @@ goTy sig ctx lic (i :: p) b (Ty.SigmaTy a c) = 0 => (\a' => Ty.SigmaTy a' c) <$> goTy sig ctx lic p b a 1 => Ty.SigmaTy a <$> goTy sig ctx lic p (1 + b) c _ => kerr "kernel: bad path" +goTy sig ctx lic (i :: p) b (Ty.SumTy a c) = + case i of + 0 => (\a' => Ty.SumTy a' c) <$> goTy sig ctx lic p b a + 1 => Ty.SumTy a <$> goTy sig ctx lic p b c + _ => kerr "kernel: bad path" goTy sig ctx lic (i :: p) b (El e) = if i == 0 then El <$> goE sig ctx lic p b (Just Ty.UniverseTy) e else kerr "kernel: bad path" @@ -1247,6 +1341,8 @@ wkSubN (S n) = Chain (wkSubN n) Wk isIntro : Elem -> Bool isIntro (PiIntro _) = True isIntro (SigmaIntro _ _) = True +isIntro (Inj1 _) = True +isIntro (Inj2 _) = True isIntro (Class _) = True isIntro (ZeroElim _) = True isIntro Star = True @@ -1322,6 +1418,7 @@ mutual FQuotCong _ => kerr "kernel: quotient-congruence final on an element equation" FPiCong _ _ => kerr "kernel: Π-congruence final on an element equation" FSigmaCong _ _ => kerr "kernel: Σ-congruence final on an element equation" + FSumCong _ _ => kerr "kernel: ⊎-congruence final on an element equation" where goSteps : Ty -> List Step -> Elem -> Elem -> KM (Elem, Elem) goSteps tyU [] l' r' = pure (l', r') @@ -1371,6 +1468,13 @@ mutual kEqTy sig ctx dc d0 d1 kEqTy sig (ctx :< d1) cc c0 c1 _ => kerr "kernel: Σ-congruence final at non-Σ types" + -- ty-sum-cong: componentwise, both components over Γ + FSumCong lc rc => + case (a1, b1) of + (Ty.SumTy l0 r0, Ty.SumTy l1 r1) => do + kEqTy sig ctx lc l0 l1 + kEqTy sig ctx rc r0 r1 + _ => kerr "kernel: ⊎-congruence final at non-⊎ types" _ => kerr "kernel: unsupported final for a type equation" where goSteps : List Step -> Ty -> Ty -> KM (Ty, Ty) @@ -1455,6 +1559,16 @@ mutual _ => kerr "kernel: squash-elim scrutinee at Prf of a non-∥∥ code" _ => kerr "kernel: squash-elim scrutinee has non-Prf type" Nothing => kerr "kernel: ⋆ without its witness or squash-elim annotation" + Inj1 a => do + ty' <- kTy sig ty + case ty' of + Ty.SumTy dom _ => kCheckE sig ctx a dom (skelChild 0 sk) + _ => kerr "kernel: inj₁ checked at a non-⊎ type" + Inj2 a => do + ty' <- kTy sig ty + case ty' of + Ty.SumTy _ cod => kCheckE sig ctx a cod (skelChild 0 sk) + _ => kerr "kernel: inj₂ checked at a non-⊎ type" Class a => do ty' <- kTy sig ty case ty' of @@ -1564,6 +1678,22 @@ mutual kCheckE sig ctx t Ty.NatTy (skelChild 2 sk) pure (substTy mot (Ext Id t)) Nothing => kerr "kernel: ℕ-elim without a motive annotation" + SumElim l r t => + -- el-sum-e: the motive arrives as a payload, the + -- scrutinee's ⊎-type is inferred (like quot-elim's) + case takeP pMotive sk of + Just ((mot, motSk), _) => do + tTy <- kInferE sig ctx t (skelChild 2 sk) >>= kTy sig + case tTy of + Ty.SumTy a b => do + kCheckTyK sig (ctx :< Ty.SumTy a b) mot motSk + kCheckE sig (ctx :< a) l + (substTy mot (Ext Wk (Inj1 (CtxVar 0)))) (skelChild 0 sk) + kCheckE sig (ctx :< b) r + (substTy mot (Ext Wk (Inj2 (CtxVar 0)))) (skelChild 1 sk) + pure (substTy mot (Ext Id t)) + _ => kerr "kernel: ⊎-elim of a non-⊎ scrutinee" + Nothing => kerr "kernel: ⊎-elim without a motive annotation" QuotElim f q => case (takeP pMotive sk, takeP pWD sk) of (Just ((mot, motSk), _), Just (wd, _)) => do @@ -1660,6 +1790,10 @@ mutual kCheckE sig ctx a Ty.UniverseTy (skelChild 0 sk) kCheckE sig (ctx :< El a) b Ty.UniverseTy (skelChild 1 sk) pure Ty.UniverseTy + Elem.SumTy a b => do + kCheckE sig ctx a Ty.UniverseTy (skelChild 0 sk) + kCheckE sig ctx b Ty.UniverseTy (skelChild 1 sk) + pure Ty.UniverseTy QuotTy a r => do kCheckE sig ctx a Ty.UniverseTy (skelChild 0 sk) kCheckE sig (ctx :< El a :< substTy (El a) Wk) r Ty.PropTy (skelChild 1 sk) @@ -1692,6 +1826,9 @@ mutual kCheckTyK sig ctx (Ty.SigmaTy a b) sk = do kCheckTyK sig ctx a (skelChild 0 sk) kCheckTyK sig (ctx :< a) b (skelChild 1 sk) + kCheckTyK sig ctx (Ty.SumTy a b) sk = do + kCheckTyK sig ctx a (skelChild 0 sk) + kCheckTyK sig ctx b (skelChild 1 sk) kCheckTyK sig ctx (El e) sk = kCheckE sig ctx e Ty.UniverseTy (skelChild 0 sk) kCheckTyK sig ctx Ty.PropTy _ = pure () kCheckTyK sig ctx (Prf p) sk = kCheckE sig ctx p Ty.PropTy (skelChild 0 sk) diff --git a/src/idris/Nova/Kernel/Beta.idr b/src/idris/Nova/Kernel/Beta.idr index d45c1035..02592e27 100644 --- a/src/idris/Nova/Kernel/Beta.idr +++ b/src/idris/Nova/Kernel/Beta.idr @@ -62,11 +62,21 @@ mutual case betaElem sig t of SigmaIntro _ b => b t' => SigmaElim2 t' + betaElem sig (Inj1 t) = Inj1 (betaElem sig t) + betaElem sig (Inj2 t) = Inj2 (betaElem sig t) + betaElem sig (SumElim l r t) = + let l' = betaElem sig l + r' = betaElem sig r + in case betaElem sig t of + Inj1 a => betaElem sig (substElem l' (Ext Id a)) + Inj2 b => betaElem sig (substElem r' (Ext Id b)) + t' => SumElim l' r' t' betaElem sig Elem.ZeroTy = Elem.ZeroTy betaElem sig Elem.OneTy = Elem.OneTy betaElem sig Elem.NatTy = Elem.NatTy betaElem sig (Elem.PiTy a b) = Elem.PiTy (betaElem sig a) (betaElem sig b) betaElem sig (Elem.SigmaTy a b) = Elem.SigmaTy (betaElem sig a) (betaElem sig b) + betaElem sig (Elem.SumTy a b) = Elem.SumTy (betaElem sig a) (betaElem sig b) betaElem sig (Elem.EqTy l r t) = Elem.EqTy (betaElem sig l) (betaElem sig r) (betaTy sig t) betaElem sig (QuotTy a r) = QuotTy (betaElem sig a) (betaElem sig r) betaElem sig (SigVar x es) = @@ -142,6 +152,7 @@ mutual betaTy sig Ty.UniverseTy = Ty.UniverseTy betaTy sig (Ty.PiTy a b) = Ty.PiTy (betaTy sig a) (betaTy sig b) betaTy sig (Ty.SigmaTy a b) = Ty.SigmaTy (betaTy sig a) (betaTy sig b) + betaTy sig (Ty.SumTy a b) = Ty.SumTy (betaTy sig a) (betaTy sig b) betaTy sig (El e) = case betaElem sig e of Elem.ZeroTy => Ty.ZeroTy @@ -149,6 +160,7 @@ mutual Elem.NatTy => Ty.NatTy Elem.PiTy a b => betaTy sig (Ty.PiTy (El a) (El b)) Elem.SigmaTy a b => betaTy sig (Ty.SigmaTy (El a) (El b)) + Elem.SumTy a b => betaTy sig (Ty.SumTy (El a) (El b)) QuotTy a r => betaTy sig (Quotient (El a) r) QSortC sg k es => QSort sg k es -- ty-el-qiit e' => El e' @@ -209,6 +221,11 @@ mutual case whnfE sig t of SigmaIntro _ b => whnfE sig b t' => SigmaElim2 t' + whnfE sig (SumElim l r t) = + case whnfE sig t of + Inj1 a => whnfE sig (substElem l (Ext Id a)) + Inj2 b => whnfE sig (substElem r (Ext Id b)) + t' => SumElim l r t' whnfE sig (SigVar x es) = case sigLookup x sig of Just (SigDef _ _ a _) => whnfE sig (substElem a (embed es)) @@ -243,6 +260,7 @@ mutual Elem.NatTy => Ty.NatTy Elem.PiTy a b => Ty.PiTy (El a) (El b) Elem.SigmaTy a b => Ty.SigmaTy (El a) (El b) + Elem.SumTy a b => Ty.SumTy (El a) (El b) QuotTy a r => Quotient (El a) r QSortC sg k es => QSort sg k es -- ty-el-qiit e' => El e' diff --git a/src/idris/Nova/Kernel/Parser.idr b/src/idris/Nova/Kernel/Parser.idr index 0f8b279c..bb51cf78 100644 --- a/src/idris/Nova/Kernel/Parser.idr +++ b/src/idris/Nova/Kernel/Parser.idr @@ -102,16 +102,26 @@ mutual covering parseElemNoComma : Rule Elem parseElemNoComma = do - e <- parseElemPrefix + e <- parseElemSum (do sp; str_ "→"; sp; e' <- parseElemNoComma; pure (Elem.PiTy e e')) <|> (do sp; str_ "⨯"; sp; e' <- parseElemNoComma; pure (Elem.SigmaTy e e')) <|> (do sp; str_ "/"; sp; e' <- parseElemNoComma; pure (Elem.QuotTy e e')) <|> (do sp; str_ "≡"; sp - e1 <- parseElemPrefix; sp; str_ "∈"; sp + e1 <- parseElemSum; sp; str_ "∈"; sp t2 <- parseTyEl pure (Elem.EqTy e e1 t2)) <|> pure e + -- e₁ ⊎ e₂ (right-assoc SumTy element) — non-dependent; binds + -- TIGHTER than the other infix element formers (Agda's convention: + -- a ⊎ b → c is (a ⊎ b) → c) + covering + parseElemSum : Rule Elem + parseElemSum = do + e <- parseElemPrefix + (do sp; str_ "⊎"; sp; e' <- parseElemSum; pure (Elem.SumTy e e')) + <|> pure e + -- Prefix operators: take an atomic argument covering parseElemPrefix : Rule Elem @@ -124,6 +134,13 @@ mutual t <- parseElemAtom pure (NatElim z s t)) <|> (do str_ "S"; space; e <- parseElemAtom; pure (NatIntro1 e)) + <|> (do str_ "inj₁"; space; e <- parseElemAtom; pure (Inj1 e)) + <|> (do str_ "inj₂"; space; e <- parseElemAtom; pure (Inj2 e)) + <|> (do str_ "⊎-elim"; space + l <- parseElemAtom; space + r <- parseElemAtom; space + t <- parseElemAtom + pure (SumElim l r t)) <|> (do str_ "class"; space; e <- parseElemAtom; pure (Class e)) <|> (do str_ "quot-elim"; space f <- parseElemAtom; space @@ -237,12 +254,20 @@ mutual covering parseTyArrow : Rule Ty parseTyArrow = do - a <- parseTyEl + a <- parseTySum (do sp; str_ "→"; sp; b <- parseTyArrow; pure (Ty.PiTy a b)) <|> (do sp; str_ "⨯"; sp; b <- parseTyArrow; pure (Ty.SigmaTy a b)) <|> (do sp; str_ "/"; sp; r <- parseElemNoComma; pure (Ty.Quotient a r)) <|> pure a + -- A ⊎ B (right-assoc, non-dependent) — tighter than → ⨯ / + covering + parseTySum : Rule Ty + parseTySum = do + a <- parseTyEl + (do sp; str_ "⊎"; sp; b <- parseTySum; pure (Ty.SumTy a b)) + <|> pure a + -- El e / Prf e (prefix, argument is an Elem atom) covering parseTyEl : Rule Ty diff --git a/src/idris/Nova/Kernel/Subst.idr b/src/idris/Nova/Kernel/Subst.idr index 97e69950..3389a7e1 100644 --- a/src/idris/Nova/Kernel/Subst.idr +++ b/src/idris/Nova/Kernel/Subst.idr @@ -61,11 +61,15 @@ mutual substElem (SigmaIntro a b) sigma = SigmaIntro (substElem a sigma) (substElem b sigma) substElem (SigmaElim1 t) sigma = SigmaElim1 (substElem t sigma) substElem (SigmaElim2 t) sigma = SigmaElim2 (substElem t sigma) + substElem (Inj1 t) sigma = Inj1 (substElem t sigma) + substElem (Inj2 t) sigma = Inj2 (substElem t sigma) + substElem (SumElim l r t) sigma = SumElim (substElem l (under sigma)) (substElem r (under sigma)) (substElem t sigma) substElem Elem.ZeroTy sigma = Elem.ZeroTy substElem Elem.OneTy sigma = Elem.OneTy substElem Elem.NatTy sigma = Elem.NatTy substElem (Elem.PiTy a b) sigma = Elem.PiTy (substElem a sigma) (substElem b (under sigma)) substElem (Elem.SigmaTy a b) sigma = Elem.SigmaTy (substElem a sigma) (substElem b (under sigma)) + substElem (Elem.SumTy a b) sigma = Elem.SumTy (substElem a sigma) (substElem b sigma) substElem (Elem.EqTy l r t) sigma = Elem.EqTy (substElem l sigma) (substElem r sigma) (substTy t sigma) substElem (QuotTy a r) sigma = QuotTy (substElem a sigma) (substElem r (under (under sigma))) substElem (SigVar x es) sigma = SigVar x (substSubNorm es sigma) @@ -124,6 +128,7 @@ mutual substTy Ty.UniverseTy sigma = Ty.UniverseTy substTy (Ty.PiTy a b) sigma = Ty.PiTy (substTy a sigma) (substTy b (under sigma)) substTy (Ty.SigmaTy a b) sigma = Ty.SigmaTy (substTy a sigma) (substTy b (under sigma)) + substTy (Ty.SumTy a b) sigma = Ty.SumTy (substTy a sigma) (substTy b sigma) substTy (El e) sigma = El (substElem e sigma) substTy PropTy sigma = PropTy substTy (Prf e) sigma = Prf (substElem e sigma) @@ -171,11 +176,15 @@ mutual strengthenElem d (SigmaIntro a b) = SigmaIntro <$> strengthenElem d a <*> strengthenElem d b strengthenElem d (SigmaElim1 t) = SigmaElim1 <$> strengthenElem d t strengthenElem d (SigmaElim2 t) = SigmaElim2 <$> strengthenElem d t + strengthenElem d (Inj1 t) = Inj1 <$> strengthenElem d t + strengthenElem d (Inj2 t) = Inj2 <$> strengthenElem d t + strengthenElem d (SumElim l r t) = SumElim <$> strengthenElem (1 + d) l <*> strengthenElem (1 + d) r <*> strengthenElem d t strengthenElem d Elem.ZeroTy = Just Elem.ZeroTy strengthenElem d Elem.OneTy = Just Elem.OneTy strengthenElem d Elem.NatTy = Just Elem.NatTy strengthenElem d (Elem.PiTy a b) = Elem.PiTy <$> strengthenElem d a <*> strengthenElem (1 + d) b strengthenElem d (Elem.SigmaTy a b) = Elem.SigmaTy <$> strengthenElem d a <*> strengthenElem (1 + d) b + strengthenElem d (Elem.SumTy a b) = Elem.SumTy <$> strengthenElem d a <*> strengthenElem d b strengthenElem d (Elem.EqTy l r t) = Elem.EqTy <$> strengthenElem d l <*> strengthenElem d r <*> strengthenTy d t strengthenElem d (QuotTy a r) = QuotTy <$> strengthenElem d a <*> strengthenElem (2 + d) r strengthenElem d (SigVar x es) = SigVar x <$> strengthenSubNorm d es @@ -228,6 +237,7 @@ mutual strengthenTy d Ty.UniverseTy = Just Ty.UniverseTy strengthenTy d (Ty.PiTy a b) = Ty.PiTy <$> strengthenTy d a <*> strengthenTy (1 + d) b strengthenTy d (Ty.SigmaTy a b) = Ty.SigmaTy <$> strengthenTy d a <*> strengthenTy (1 + d) b + strengthenTy d (Ty.SumTy a b) = Ty.SumTy <$> strengthenTy d a <*> strengthenTy d b strengthenTy d (El e) = El <$> strengthenElem d e strengthenTy d PropTy = Just PropTy strengthenTy d (Prf e) = Prf <$> strengthenElem d e diff --git a/src/idris/Nova/Kernel/Syntax.idr b/src/idris/Nova/Kernel/Syntax.idr index 4f27fe34..1dd021f1 100644 --- a/src/idris/Nova/Kernel/Syntax.idr +++ b/src/idris/Nova/Kernel/Syntax.idr @@ -33,6 +33,9 @@ mutual PiTy : Ty -> Ty -> Ty ||| T ⨯ T (dependent sum type, Σ) SigmaTy : Ty -> Ty -> Ty + ||| T ⊎ T (non-dependent sum type — disjoint union; both + ||| components live over the same context, no binder) + SumTy : Ty -> Ty -> Ty ||| El t (every element of the universe is a type) El : Elem -> Ty ||| Ω (the universe of mere propositions — anti-structural: its @@ -78,6 +81,15 @@ mutual SigmaElim1 : Elem -> Elem ||| t .π₂ (sigma elimination, second projection) SigmaElim2 : Elem -> Elem + ||| inj₁ t (sum type introduction, left) + Inj1 : Elem -> Elem + ||| inj₂ t (sum type introduction, right) + Inj2 : Elem -> Elem + ||| ⊎-elim l r t (sum type elimination: the left case — one + ||| bound variable over the left summand — then the right case + ||| — one bound variable over the right summand — then the + ||| eliminee) + SumElim : Elem -> Elem -> Elem -> Elem ||| 𝟘 (universe element) ZeroTy : Elem ||| 𝟙 (universe element) @@ -88,6 +100,9 @@ mutual PiTy : Elem -> Elem -> Elem ||| t ⨯ t (universe element encoding Σ) SigmaTy : Elem -> Elem -> Elem + ||| t ⊎ t (universe element encoding ⊎ — non-dependent, no + ||| binder in either component) + SumTy : Elem -> Elem -> Elem ||| t ≡ t ∈ T (the equality PROPOSITION — an Ω-element; the ||| third component is an arbitrary TYPE, so equality props ||| exist at large types. code-eq; no 𝕌-code for equality @@ -352,6 +367,7 @@ mutual UniverseTy == UniverseTy = True PiTy a b == PiTy a' b' = a == a' && b == b' SigmaTy a b == SigmaTy a' b' = a == a' && b == b' + SumTy a b == SumTy a' b' = a == a' && b == b' El e == El e' = e == e' PropTy == PropTy = True Prf e == Prf e' = e == e' @@ -374,11 +390,15 @@ mutual SigmaIntro e1 e2 == SigmaIntro e1' e2' = e1 == e1' && e2 == e2' SigmaElim1 e == SigmaElim1 e' = e == e' SigmaElim2 e == SigmaElim2 e' = e == e' + Inj1 e == Inj1 e' = e == e' + Inj2 e == Inj2 e' = e == e' + SumElim l r t == SumElim l' r' t' = l == l' && r == r' && t == t' Elem.ZeroTy == Elem.ZeroTy = True Elem.OneTy == Elem.OneTy = True Elem.NatTy == Elem.NatTy = True Elem.PiTy a b == Elem.PiTy a' b' = a == a' && b == b' Elem.SigmaTy a b == Elem.SigmaTy a' b' = a == a' && b == b' + Elem.SumTy a b == Elem.SumTy a' b' = a == a' && b == b' Elem.EqTy l r t == Elem.EqTy l' r' t' = l == l' && r == r' && t == t' QuotTy a r == QuotTy a' r' = a == a' && r == r' SigVar x s == SigVar x' s' = x == x' && s == s' @@ -449,6 +469,9 @@ mutual compare (SigmaTy a b) (SigmaTy a' b') = compare a a' <+> compare b b' compare (SigmaTy _ _) _ = LT compare _ (SigmaTy _ _) = GT + compare (SumTy a b) (SumTy a' b') = compare a a' <+> compare b b' + compare (SumTy _ _) _ = LT + compare _ (SumTy _ _) = GT compare (El e) (El e') = compare e e' compare (El _) _ = LT compare _ (El _) = GT @@ -502,6 +525,15 @@ mutual compare (SigmaElim2 e) (SigmaElim2 e') = compare e e' compare (SigmaElim2 _) _ = LT compare _ (SigmaElim2 _) = GT + compare (Inj1 e) (Inj1 e') = compare e e' + compare (Inj1 _) _ = LT + compare _ (Inj1 _) = GT + compare (Inj2 e) (Inj2 e') = compare e e' + compare (Inj2 _) _ = LT + compare _ (Inj2 _) = GT + compare (SumElim l r t) (SumElim l' r' t') = compare l l' <+> compare r r' <+> compare t t' + compare (SumElim _ _ _) _ = LT + compare _ (SumElim _ _ _) = GT compare Elem.ZeroTy Elem.ZeroTy = EQ compare Elem.ZeroTy _ = LT compare _ Elem.ZeroTy = GT @@ -517,6 +549,9 @@ mutual compare (Elem.SigmaTy a b) (Elem.SigmaTy a' b') = compare a a' <+> compare b b' compare (Elem.SigmaTy _ _) _ = LT compare _ (Elem.SigmaTy _ _) = GT + compare (Elem.SumTy a b) (Elem.SumTy a' b') = compare a a' <+> compare b b' + compare (Elem.SumTy _ _) _ = LT + compare _ (Elem.SumTy _ _) = GT compare (Elem.EqTy l r t) (Elem.EqTy l' r' t') = compare l l' <+> compare r r' <+> compare t t' compare (Elem.EqTy _ _ _) _ = LT compare _ (Elem.EqTy _ _ _) = GT @@ -594,6 +629,7 @@ mutual show UniverseTy = "UniverseTy" show (PiTy a b) = "PiTy (\{show a}) (\{show b})" show (SigmaTy a b) = "SigmaTy (\{show a}) (\{show b})" + show (SumTy a b) = "SumTy (\{show a}) (\{show b})" show (El e) = "El (\{show e})" show PropTy = "PropTy" show (Prf e) = "Prf (\{show e})" @@ -615,11 +651,15 @@ mutual show (SigmaIntro e1 e2) = "SigmaIntro (\{show e1}) (\{show e2})" show (SigmaElim1 e) = "SigmaElim1 (\{show e})" show (SigmaElim2 e) = "SigmaElim2 (\{show e})" + show (Inj1 e) = "Inj1 (\{show e})" + show (Inj2 e) = "Inj2 (\{show e})" + show (SumElim l r t) = "SumElim (\{show l}) (\{show r}) (\{show t})" show Elem.ZeroTy = "ZeroTy" show Elem.OneTy = "OneTy" show Elem.NatTy = "NatTy" show (Elem.PiTy e1 e2) = "PiTy (\{show e1}) (\{show e2})" show (Elem.SigmaTy e1 e2) = "SigmaTy (\{show e1}) (\{show e2})" + show (Elem.SumTy e1 e2) = "SumTy (\{show e1}) (\{show e2})" show (Elem.EqTy e0 e1 t) = "EqTy (\{show e0}) (\{show e1}) (\{show t})" show (QuotTy a r) = "QuotTy (\{show a}) (\{show r})" show (SigVar x s) = "SigVar \{show x} (\{show s})" diff --git a/src/nova/sum.nova b/src/nova/sum.nova new file mode 100644 index 00000000..5802fed1 --- /dev/null +++ b/src/nova/sum.nova @@ -0,0 +1,60 @@ +-- The non-dependent sum ⊎ (disjoint union) — Agda's notation: inj₁, +-- inj₂, and the dependent motive-first eliminator ⊎-elim (like +-- ℕ-elim). β on each injection is judgemental (el-sum-beta₁/₂); the +-- uniqueness law (el-sum-eta) is stated judgementally in the theory +-- and derivable here, propositionally, by case analysis at an +-- equality motive. Injection injectivity and disjointness need no +-- rules — both are derivable below, exactly as Foundation's +-- injectivity notes say. +import equality (cong, transport) + +-- case analysis at a constant motive: the canonical swap +def swap : (a : 𝕌) (b : 𝕌) → El (a ⊎ b) → El (b ⊎ a) ≔ + λa. λb. λt. ⊎-elim (w. El (b ⊎ a)) (x. inj₂ x) (y. inj₁ y) t + +-- β on each injection, by computation +def swapBeta1 : (a : 𝕌) (b : 𝕌) (x : El a) → swap _ _ (inj₁ x) ≡ inj₂ x ∈ El (b ⊎ _) ≔ + λa. λb. λx. ⋆ +def swapBeta2 : (a : 𝕌) (b : 𝕌) (y : El b) → swap _ _ (inj₂ y) ≡ inj₁ y ∈ El (_ ⊎ a) ≔ + λa. λb. λy. ⋆ + +-- swap is an involution: case analysis with an equality motive, both +-- cases closing by β +def swapInvol : (a : 𝕌) (b : 𝕌) (t : El (a ⊎ b)) → swap _ _ (swap _ _ t) ≡ t ∈ _ ≔ + λa. λb. λt. ⊎-elim (w. swap _ _ (swap _ _ w) ≡ w ∈ _) (x. ⋆) (y. ⋆) t + +-- the uniqueness (η) law, propositionally: any map out of a ⊎ b IS +-- the eliminator over its own injection images (el-sum-eta's content, +-- derived by ⊎-elim at an equality motive) +def sumEta : (a : 𝕌) (b : 𝕌) (c : 𝕌) (f : El (a ⊎ b) → El c) (t : El (a ⊎ b)) → + ⊎-elim (w. El c) (x. f (inj₁ x)) (y. f (inj₂ y)) t ≡ f t ∈ _ ≔ + λa. λb. λc. λf. λt. + ⊎-elim (w. ⊎-elim (v. El c) (x. f (inj₁ x)) (y. f (inj₂ y)) w ≡ f w ∈ _) + (x. ⋆) (y. ⋆) t + +-- the ⊎ TYPE former and its code agree: El (a ⊎ b) ≐ El a ⊎ El b +-- (ty-el-sum), so the conversions between them are the identity +-- case analysis +def toCode : (a : 𝕌) (b : 𝕌) → El a ⊎ El b → El (a ⊎ b) ≔ + λa. λb. λt. ⊎-elim (w. El (a ⊎ b)) (x. inj₁ x) (y. inj₂ y) t +def fromCode : (a : 𝕌) (b : 𝕌) → El (a ⊎ b) → El a ⊎ El b ≔ + λa. λb. λt. ⊎-elim (w. El a ⊎ El b) (x. inj₁ x) (y. inj₂ y) t +def toFromId : (a : 𝕌) (b : 𝕌) (t : El (a ⊎ b)) → toCode _ _ (fromCode _ _ t) ≡ t ∈ _ ≔ + λa. λb. λt. ⊎-elim (w. toCode a b (fromCode a b w) ≡ w ∈ El (a ⊎ b)) (x. ⋆) (y. ⋆) t + +-- inj₁ is injective — DERIVABLE, no rule needed: a ⊎-elim retraction +-- at constant motive El a whose right case returns a fixed default +-- (the compared element itself serves), then congruence +def outl : (a : 𝕌) (b : 𝕌) → El a → El (a ⊎ b) → El a ≔ + λa. λb. λd. λt. ⊎-elim (w. El a) (x. x) (y. d) t +def inj1Injective : (a : 𝕌) (b : 𝕌) (x : El a) (x' : El a) → + (inj₁ x ≡ inj₁ x' ∈ El (_ ⊎ b)) → x ≡ x' ∈ _ ≔ + λa. λb. λx. λx'. λh. cong _ (λw. a) (outl _ _ x) _ _ h + +-- inj₁ and inj₂ are disjoint — also derivable: transport the +-- "is-left" code along the bad equation and land a 𝟙-witness in 𝟘 +def isLeftCode : (a : 𝕌) (b : 𝕌) → El (a ⊎ b) → 𝕌 ≔ + λa. λb. λt. ⊎-elim (w. 𝕌) (x. 𝟙) (y. 𝟘) t +def inj1NotInj2 : (a : 𝕌) (b : 𝕌) (x : El a) (y : El b) → + (inj₁ x ≡ inj₂ y ∈ El (a ⊎ b)) → 𝟘 ≔ + λa. λb. λx. λy. λh. transport _ (isLeftCode _ _) _ _ h () diff --git a/tests/nova/elaboration/elab-sum-obligation/expected b/tests/nova/elaboration/elab-sum-obligation/expected new file mode 100644 index 00000000..788f5d07 --- /dev/null +++ b/tests/nova/elaboration/elab-sum-obligation/expected @@ -0,0 +1,4 @@ +defined bad [+1 obligation] +open obligations (1): + [1] (a : 𝕌) (x : El a) ⊢ inj₁ x ≐ inj₂ x : El a ⊎ El a + at: def bad: checking ⋆ diff --git a/tests/nova/elaboration/elab-sum-obligation/input.nova b/tests/nova/elaboration/elab-sum-obligation/input.nova new file mode 100644 index 00000000..4995b6ce --- /dev/null +++ b/tests/nova/elaboration/elab-sum-obligation/input.nova @@ -0,0 +1,3 @@ +-- an inj₁/inj₂ head mismatch is an OBLIGATION, not an error +-- (no-confusion is a meta-property of consistent contexts) +def bad : (a : 𝕌) (x : El a) → inj₁ x ≡ inj₂ x ∈ El (a ⊎ a) ≔ λa. λx. ⋆ diff --git a/tests/nova/elaboration/elab-sum-obligation/run b/tests/nova/elaboration/elab-sum-obligation/run new file mode 100755 index 00000000..505e6e24 --- /dev/null +++ b/tests/nova/elaboration/elab-sum-obligation/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" elab input.nova diff --git a/tests/nova/elaboration/elab-sum/expected b/tests/nova/elaboration/elab-sum/expected new file mode 100644 index 00000000..40d8c484 --- /dev/null +++ b/tests/nova/elaboration/elab-sum/expected @@ -0,0 +1,5 @@ +defined swap +defined swapBeta1 +defined swapBeta2 +defined swapInvol +Accepted. diff --git a/tests/nova/elaboration/elab-sum/input.nova b/tests/nova/elaboration/elab-sum/input.nova new file mode 100644 index 00000000..5ea889f4 --- /dev/null +++ b/tests/nova/elaboration/elab-sum/input.nova @@ -0,0 +1,10 @@ +-- β on both injections and the propositional η/uniqueness instance, +-- by case analysis at an equality motive +def swap : (a : 𝕌) (b : 𝕌) → El (a ⊎ b) → El (b ⊎ a) ≔ + λa. λb. λt. ⊎-elim (w. El (b ⊎ a)) (x. inj₂ x) (y. inj₁ y) t +def swapBeta1 : (a : 𝕌) (b : 𝕌) (x : El a) → swap a b (inj₁ x) ≡ inj₂ x ∈ El (b ⊎ a) ≔ + λa. λb. λx. ⋆ +def swapBeta2 : (a : 𝕌) (b : 𝕌) (y : El b) → swap a b (inj₂ y) ≡ inj₁ y ∈ El (b ⊎ a) ≔ + λa. λb. λy. ⋆ +def swapInvol : (a : 𝕌) (b : 𝕌) (t : El (a ⊎ b)) → swap b a (swap a b t) ≡ t ∈ El (a ⊎ b) ≔ + λa. λb. λt. ⊎-elim (w. swap b a (swap a b w) ≡ w ∈ El (a ⊎ b)) (x. ⋆) (y. ⋆) t diff --git a/tests/nova/elaboration/elab-sum/run b/tests/nova/elaboration/elab-sum/run new file mode 100755 index 00000000..505e6e24 --- /dev/null +++ b/tests/nova/elaboration/elab-sum/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" elab input.nova diff --git a/tests/nova/evaluation/eval-sum/expected b/tests/nova/evaluation/eval-sum/expected new file mode 100644 index 00000000..4e7eb31e --- /dev/null +++ b/tests/nova/evaluation/eval-sum/expected @@ -0,0 +1 @@ +Inj2 (NatIntro1 (NatIntro0)) diff --git a/tests/nova/evaluation/eval-sum/input.nova b/tests/nova/evaluation/eval-sum/input.nova new file mode 100644 index 00000000..05d7b42a --- /dev/null +++ b/tests/nova/evaluation/eval-sum/input.nova @@ -0,0 +1,4 @@ +-- ⊎-elim reduces at both injections (el-sum-beta₁/₂) +def swap : (a : 𝕌) (b : 𝕌) → El (a ⊎ b) → El (b ⊎ a) ≔ + λa. λb. λt. ⊎-elim (w. El (b ⊎ a)) (x. inj₂ x) (y. inj₁ y) t +def val : El (𝟙 ⊎ ℕ) ≔ swap ℕ 𝟙 (inj₁ (S Z)) diff --git a/tests/nova/evaluation/eval-sum/run b/tests/nova/evaluation/eval-sum/run new file mode 100755 index 00000000..dccbffc8 --- /dev/null +++ b/tests/nova/evaluation/eval-sum/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" eval input.nova val diff --git a/tests/nova/parser/elem-inj1/expected b/tests/nova/parser/elem-inj1/expected new file mode 100644 index 00000000..98f1396f --- /dev/null +++ b/tests/nova/parser/elem-inj1/expected @@ -0,0 +1 @@ +Inj1 (NatIntro0) diff --git a/tests/nova/parser/elem-inj1/run b/tests/nova/parser/elem-inj1/run new file mode 100755 index 00000000..36c463e2 --- /dev/null +++ b/tests/nova/parser/elem-inj1/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" run elem "inj₁ Z" diff --git a/tests/nova/parser/elem-inj2/expected b/tests/nova/parser/elem-inj2/expected new file mode 100644 index 00000000..a5f5c5c9 --- /dev/null +++ b/tests/nova/parser/elem-inj2/expected @@ -0,0 +1 @@ +Inj2 (OneIntro) diff --git a/tests/nova/parser/elem-inj2/run b/tests/nova/parser/elem-inj2/run new file mode 100755 index 00000000..65080097 --- /dev/null +++ b/tests/nova/parser/elem-inj2/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" run elem "inj₂ ()" diff --git a/tests/nova/parser/elem-sumelim/expected b/tests/nova/parser/elem-sumelim/expected new file mode 100644 index 00000000..a454a489 --- /dev/null +++ b/tests/nova/parser/elem-sumelim/expected @@ -0,0 +1 @@ +SumElim (CtxVar 0) (CtxVar 0) (CtxVar 1) diff --git a/tests/nova/parser/elem-sumelim/run b/tests/nova/parser/elem-sumelim/run new file mode 100755 index 00000000..d9a79453 --- /dev/null +++ b/tests/nova/parser/elem-sumelim/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" run elem "⊎-elim ☐₀ ☐₀ ☐₁" diff --git a/tests/nova/parser/elem-sumty/expected b/tests/nova/parser/elem-sumty/expected new file mode 100644 index 00000000..efb467ea --- /dev/null +++ b/tests/nova/parser/elem-sumty/expected @@ -0,0 +1 @@ +SumTy (NatTy) (OneTy) diff --git a/tests/nova/parser/elem-sumty/run b/tests/nova/parser/elem-sumty/run new file mode 100755 index 00000000..a01c24b9 --- /dev/null +++ b/tests/nova/parser/elem-sumty/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" run elem "ℕ ⊎ 𝟙" diff --git a/tests/nova/parser/ty-sum-tighter/expected b/tests/nova/parser/ty-sum-tighter/expected new file mode 100644 index 00000000..594b0a20 --- /dev/null +++ b/tests/nova/parser/ty-sum-tighter/expected @@ -0,0 +1 @@ +PiTy (SumTy (NatTy) (OneTy)) (ZeroTy) diff --git a/tests/nova/parser/ty-sum-tighter/run b/tests/nova/parser/ty-sum-tighter/run new file mode 100755 index 00000000..f8da2b3b --- /dev/null +++ b/tests/nova/parser/ty-sum-tighter/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" run ty "ℕ ⊎ 𝟙 → 𝟘" diff --git a/tests/nova/parser/ty-sum/expected b/tests/nova/parser/ty-sum/expected new file mode 100644 index 00000000..efb467ea --- /dev/null +++ b/tests/nova/parser/ty-sum/expected @@ -0,0 +1 @@ +SumTy (NatTy) (OneTy) diff --git a/tests/nova/parser/ty-sum/run b/tests/nova/parser/ty-sum/run new file mode 100755 index 00000000..3b1850aa --- /dev/null +++ b/tests/nova/parser/ty-sum/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" run ty "ℕ ⊎ 𝟙"