diff --git a/examples/bool.quox b/examples/bool.quox index 055e28f..7d3a065 100644 --- a/examples/bool.quox +++ b/examples/bool.quox @@ -1,34 +1,35 @@ -load "misc.quox"; +load "misc.quox" namespace bool { -def0 Bool : ★ = {true, false}; +def0 Bool : ★ = {true, false} def if-dep : 0.(P : Bool → ★) → (b : Bool) → ω.(P 'true) → ω.(P 'false) → P b = - λ P b t f ⇒ case b return b' ⇒ P b' of { 'true ⇒ t; 'false ⇒ f }; + λ P b t f ⇒ case b return b' ⇒ P b' of { 'true ⇒ t; 'false ⇒ f } -def if : 0.(A : ★) → (b : Bool) → ω.A → ω.A → A = - λ A ⇒ if-dep (λ _ ⇒ A); +def if : 0.(A : ★) → Bool → ω.A → ω.A → A = + λ A ⇒ if-dep (λ _ ⇒ A) def0 if-same : (A : ★) → (b : Bool) → (x : A) → if A b x x ≡ x : A = - λ A b x ⇒ if-dep (λ b' ⇒ if A b' x x ≡ x : A) b (δ _ ⇒ x) (δ _ ⇒ x); + λ A b x ⇒ if-dep (λ b' ⇒ if A b' x x ≡ x : A) b (δ _ ⇒ x) (δ _ ⇒ x) def if2 : 0.(A B : ★) → (b : Bool) → ω.A → ω.B → if¹ ★ b A B = - λ A B ⇒ if-dep (λ b ⇒ if-dep¹ (λ _ ⇒ ★) b A B); + λ A B ⇒ if-dep (λ b ⇒ if¹ ★ b A B) -def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False; +def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False -def boolω : Bool → [ω.Bool] = - λ b ⇒ if [ω.Bool] b ['true] ['false]; +def dup : Bool → [ω.Bool] = + λ b ⇒ if [ω.Bool] b ['true] ['false] -def true-not-false : Not ('true ≡ 'false : Bool) = - λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true; +def0 true-not-false : Not ('true ≡ 'false : Bool) = + λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true -- [todo] infix -def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false; -def or : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b; +def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false +def or : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b } -def0 Bool = bool.Bool; +def0 Bool = bool.Bool +def if = bool.if diff --git a/examples/natw.quox b/examples/natw.quox new file mode 100644 index 0000000..1922b87 --- /dev/null +++ b/examples/natw.quox @@ -0,0 +1,36 @@ +load "misc.quox" + +namespace natw { + +def0 Tag : ★ = {z, s} + +def0 Child : Tag → ★ = + λ t ⇒ case t return ★ of { 'z ⇒ {}; 's ⇒ {pred} } + +def0 NatW : ★ = (t : Tag) ⊲ Child t + +def Zero : NatW = + 'z ⋄ (λ v ⇒ case v return NatW of {}) + +def Suc : ω.NatW → NatW = + λ n ⇒ 's ⋄ (λ u ⇒ case u return NatW of { 'pred ⇒ n }) + +def elim : 0.(P : NatW → ★) → + ω.(P Zero) → + ω.(0.(n : NatW) → ω.(P n) → P (Suc n)) → + ω.(n : NatW) → P n = + λ P pz ps n ⇒ + caseω n return n' ⇒ P n' of { + t ⋄ f, ω.ih ⇒ + (case t + return t' ⇒ 0.(eq : t ≡ t' : Tag) → + P (t' ⋄ coe (𝑖 ⇒ ω.(Child (eq @𝑖)) → NatW) f) + of { + 'z ⇒ λ _ ⇒ pz; + 's ⇒ λ eq ⇒ + ps (f (coe (𝑖 ⇒ Child (eq @𝑖)) @1 @0 'pred)) + (ih (coe (𝑖 ⇒ Child (eq @𝑖)) @1 @0 'pred)) + }) (δ 𝑖 ⇒ t) + } + +} diff --git a/lib/Quox/Displace.idr b/lib/Quox/Displace.idr index c7d5e02..5d3b2fb 100644 --- a/lib/Quox/Displace.idr +++ b/lib/Quox/Displace.idr @@ -19,6 +19,9 @@ parameters (k : Universe) doDisplace (Lam body loc) = Lam (doDisplaceS body) loc doDisplace (Sig fst snd loc) = Sig (doDisplace fst) (doDisplaceS snd) loc doDisplace (Pair fst snd loc) = Pair (doDisplace fst) (doDisplace snd) loc + doDisplace (W shape body loc) = + W (doDisplace shape) (doDisplaceS body) loc + doDisplace (Sup root sub loc) = Sup (doDisplace root) (doDisplace sub) loc doDisplace (Enum cases loc) = Enum cases loc doDisplace (Tag tag loc) = Tag tag loc doDisplace (Eq ty l r loc) = @@ -47,6 +50,8 @@ parameters (k : Universe) doDisplace (App fun arg loc) = App (doDisplace fun) (doDisplace arg) loc doDisplace (CasePair qty pair ret body loc) = CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) loc + doDisplace (CaseW qty qtyIH tree ret body loc) = + CaseW qty qtyIH (doDisplace tree) (doDisplaceS ret) (doDisplaceS body) loc doDisplace (CaseEnum qty tag ret arms loc) = CaseEnum qty (doDisplace tag) (doDisplaceS ret) (map doDisplace arms) loc doDisplace (CaseNat qty qtyIH nat ret zero succ loc) = diff --git a/lib/Quox/EffExtra.idr b/lib/Quox/EffExtra.idr index e80a922..49479a3 100644 --- a/lib/Quox/EffExtra.idr +++ b/lib/Quox/EffExtra.idr @@ -26,6 +26,26 @@ local_ : Has (State s) fs => s -> Eff fs a -> Eff fs a local_ = localAt_ () +public export +record StateRes s a where + constructor SR + state : s + result : a + +export +stateAt : (0 lbl : tag) -> Has (StateL lbl s) fs => + (s -> StateRes s a) -> Eff fs a +stateAt lbl f = do + s <- getAt lbl + let out = f s + putAt lbl out.state + pure out.result + +export %inline +state : Has (State s) fs => (s -> StateRes s a) -> Eff fs a +state = stateAt () + + export hasDrop : (0 neq : Not (a = b)) -> (ha : Has a fs) => (hb : Has b fs) => diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index c3e49dc..91a612a 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -79,6 +79,8 @@ sameTyCon (Pi {}) (Pi {}) = True sameTyCon (Pi {}) _ = False sameTyCon (Sig {}) (Sig {}) = True sameTyCon (Sig {}) _ = False +sameTyCon (W {}) (W {}) = True +sameTyCon (W {}) _ = False sameTyCon (Enum {}) (Enum {}) = True sameTyCon (Enum {}) _ = False sameTyCon (Eq {}) (Eq {}) = True @@ -111,6 +113,7 @@ isSubSing defs ctx ty0 = do Sig {fst, snd, _} => isSubSing defs ctx fst `andM` isSubSing defs (extendTy Zero snd.name fst ctx) snd.term + W {} => pure False Enum {cases, _} => pure $ length (SortedSet.toList cases) <= 1 Eq {} => pure True @@ -120,6 +123,7 @@ isSubSing defs ctx ty0 = do E _ => pure False Lam {} => pure False Pair {} => pure False + Sup {} => pure False Tag {} => pure False DLam {} => pure False Zero {} => pure False @@ -209,9 +213,9 @@ parameters (defs : Definitions) case (s, t) of -- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x} -- -------------------------------------------- - -- Γ ⊢ (s₁, t₁) = (s₂,t₂) : (x : A) × B + -- Γ ⊢ (s₁, t₁) = (s₂, t₂) : (x : A) × B -- - -- [todo] η for π ≥ 0 maybe + -- [todo] η for π ≰ 1 maybe (Pair sFst sSnd {}, Pair tFst tSnd {}) => do compare0 ctx fst sFst tFst compare0 ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd @@ -225,6 +229,27 @@ parameters (defs : Definitions) (E _, t) => wrongType t.loc ctx ty t (s, _) => wrongType s.loc ctx ty s + compare0' ctx ty@(W {shape, body, _}) s t = + case (s, t) of + -- Γ ⊢ s₁ = t₁ : A + -- Γ ⊢ s₂ = t₂ : ω.B[s₁∷A/x] → (x : A) ⊲ B + -- ----------------------------------------- + -- Γ ⊢ s₁⋄s₂ = t₁⋄t₂ : (x : A) ⊲ B + (Sup sRoot sSub {}, Sup tRoot tSub {}) => do + compare0 ctx shape sRoot tRoot + let arg = sub1 body (Ann sRoot shape sRoot.loc) + subTy = Arr Any arg ty ty.loc + compare0 ctx subTy sSub tSub + + (E e, E f) => Elim.compare0 ctx e f + + (Sup {}, E {}) => clashT s.loc ctx ty s t + (E {}, Sup {}) => clashT s.loc ctx ty s t + + (Sup {}, t) => wrongType t.loc ctx ty t + (E {}, t) => wrongType t.loc ctx ty t + (s, _) => wrongType s.loc ctx ty s + compare0' ctx ty@(Enum {}) s t = local_ Equal $ case (s, t) of -- -------------------- @@ -322,12 +347,16 @@ parameters (defs : Definitions) -- Γ ⊢ Type 𝓀 <: Type ℓ expectModeU a.loc !mode k l - compareType' ctx a@(Pi {qty = sQty, arg = sArg, res = sRes, _}) - (Pi {qty = tQty, arg = tArg, res = tRes, _}) = do + compareType' ctx (Pi {qty = sQty, arg = sArg, res = sRes, loc}) + (Pi {qty = tQty, arg = tArg, res = tRes, _}) = do -- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂ -- ---------------------------------------- - -- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂ - expectEqualQ a.loc sQty tQty + -- Γ ⊢ π.(x : A₁) → B₁ <: π.(x : A₂) → B₂ + -- + -- no quantity subtyping since that would need a runtime coercion + -- e.g. if ⌊0.A → B⌋ ⇝ ⌊B⌋, then the promotion to ω.A → B would need + -- to re-add the abstraction + expectEqualQ loc sQty tQty local flip $ compareType ctx sArg tArg -- contra compareType (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term @@ -339,12 +368,20 @@ parameters (defs : Definitions) compareType ctx sFst tFst compareType (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term + compareType' ctx (W {shape = sShape, body = sBody, loc}) + (W {shape = tShape, body = tBody, _}) = do + -- Γ ⊢ A₁ <: A₂ Γ, x : A₁ ⊢ B₁ <: B₂ + -- -------------------------------------- + -- Γ ⊢ (x : A₁) ⊲ B₁ <: (x : A₂) ⊲ B₂ + compareType ctx sShape tShape + compareType (extendTy Zero sBody.name sShape ctx) sBody.term tBody.term + compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _}) (Eq {ty = tTy, l = tl, r = tr, _}) = do -- Γ ⊢ A₁‹ε/i› <: A₂‹ε/i› - -- Γ ⊢ l₁ = l₂ : A₁‹𝟎/i› Γ ⊢ r₁ = r₂ : A₁‹𝟏/i› + -- Γ ⊢ l₁ = l₂ : A₁‹0/i› Γ ⊢ r₁ = r₂ : A₁‹1/i› -- ------------------------------------------------ - -- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂ + -- Γ ⊢ Eq (i ⇒ A₁) l₁ r₂ <: Eq (i ⇒ A₂) l₂ r₂ compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero compareType (extendDim sTy.name One ctx) sTy.one tTy.one let ty = case !mode of Super => sTy; _ => tTy @@ -366,6 +403,9 @@ parameters (defs : Definitions) pure () compareType' ctx (BOX pi a loc) (BOX rh b {}) = do + -- Γ ⊢ A <: B + -- -------------------- + -- Γ ⊢ [π.A] <: [π.B] expectEqualQ loc pi rh compareType ctx a b @@ -439,6 +479,36 @@ parameters (defs : Definitions) expectEqualQ e.loc epi fpi compare0' ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f + -- Ψ | Γ ⊢ e = f ⇒ (x : A) ⊲ B + -- Ψ | Γ, p : (x : A) ⊲ B ⊢ Q = R ⇐ Type + -- Ψ | Γ, x : A, y : ω.B → (x : A) ⊲ B, ih : 1.(z : B) → Q[y z/p] + -- ⊢ s = t ⇐ Q[(x⋄y ∷ (x : A) ⊲ B)/p] + -- ---------------------------------------------------------------- + -- Ψ | Γ ⊢ caseπ e return Q of { x ⋄ y, ς.ih ⇒ s } + -- = caseπ f return R of { x ⋄ y, ς.ih ⇒ t } ⇒ Q[e/p] + compare0' ctx (CaseW epi epi' e eret ebody eloc) + (CaseW fpi fpi' f fret fbody floc) ne nf = + local_ Equal $ do + compare0 ctx e f + ety <- computeElimTypeE defs ctx e @{noOr1 ne} + compareType (extendTy Zero eret.name ety ctx) eret.term fret.term + (shape, tbody) <- expectW defs ctx eloc ety + let [< x, y, ih] = ebody.names + z <- mnb "z" ih.loc + let xbind = (epi, x, shape) + ybind = (epi, y, Arr Any tbody.term (weakT 1 ety) y.loc) + ihbind = (epi', ih, + PiY One z + (sub1 (weakS 2 tbody) (BV 1 x.loc)) + (sub1 (weakS 3 eret) (App (BV 1 y.loc) (BVT 0 z.loc) ih.loc)) + ih.loc) + ctx' = extendTyN [< xbind, ybind, ihbind] ctx + Term.compare0 ctx' (substCaseWRet ebody.names ety eret) + ebody.term fbody.term + expectEqualQ e.loc epi fpi + expectEqualQ e.loc epi' fpi' + compare0' ctx e@(CaseW {}) f _ _ = clashE e.loc ctx e f + -- Ψ | Γ ⊢ e = f ⇒ {𝐚s} -- Ψ | Γ, x : {𝐚s} ⊢ Q = R -- Ψ | Γ ⊢ sᵢ = tᵢ ⇐ Q[𝐚ᵢ∷{𝐚s}] @@ -451,10 +521,13 @@ parameters (defs : Definitions) compare0 ctx e f ety <- computeElimTypeE defs ctx e @{noOr1 ne} compareType (extendTy Zero eret.name ety ctx) eret.term fret.term - for_ !(expectEnum defs ctx eloc ety) $ \t => do - l <- lookupArm eloc t earms + for_ (SortedMap.toList earms) $ \(t, l) => do r <- lookupArm floc t farms compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r + -- for_ !(expectEnum defs ctx eloc ety) $ \t => do + -- l <- lookupArm eloc t earms + -- r <- lookupArm floc t farms + -- compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r expectEqualQ eloc epi fpi where lookupArm : Loc -> TagVal -> CaseEnumArms d n -> Equal_ (Term d n) @@ -522,16 +595,18 @@ parameters (defs : Definitions) -- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖› -- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖› - -- Ψ | Γ ⊢ e <: f ⇒ _ - -- (non-neutral forms have the coercion already pushed in) + -- Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖› -- ----------------------------------------------------------- - -- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ e - -- <: coe [𝑖 ⇒ B] @p₂ @q₂ f ⇒ B‹q₂/𝑖› - compare0' ctx (Coe ty1 p1 q1 (E val1) _) - (Coe ty2 p2 q2 (E val2) _) ne nf = do - compareType ctx (dsub1 ty1 p1) (dsub1 ty2 p2) - compareType ctx (dsub1 ty1 q1) (dsub1 ty2 q2) - compare0 ctx val1 val2 + -- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s + -- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖› + compare0' ctx (Coe ty1 p1 q1 val1 _) + (Coe ty2 p2 q2 val2 _) ne nf = do + let typ1 = dsub1 ty1 p1; tyq1 = dsub1 ty1 q1 + typ2 = dsub1 ty2 p2; tyq2 = dsub1 ty2 q2 + compareType ctx typ1 typ2 + compareType ctx tyq1 tyq2 + let ty = case !mode of Super => typ1; _ => typ2 + Term.compare0 ctx ty val1 val2 compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f -- (no neutral compositions in a closed dctx) @@ -598,6 +673,13 @@ parameters (defs : Definitions) (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx compare0 ctx (weakT 2 ret) b1.term b2.term + compareArm_ ctx KW ret u b1 b2 = do + let [< a, b] = b1.names + ctx = extendTyN + [< (Zero, a, TYPE u a.loc), + (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx + compare0 ctx (weakT 2 ret) b1.term b2.term + compareArm_ ctx KEnum ret u b1 b2 = compare0 ctx ret b1.term b2.term diff --git a/lib/Quox/Loc.idr b/lib/Quox/Loc.idr index cd63e2f..7bf5151 100644 --- a/lib/Quox/Loc.idr +++ b/lib/Quox/Loc.idr @@ -109,10 +109,16 @@ or (L l1) (L l2) = L $ l1 `or_` l2 public export interface Located a where (.loc) : a -> Loc +export %inline Located Loc where l.loc = l + public export 0 Located1 : (a -> Type) -> Type Located1 f = forall x. Located (f x) +public export +0 Located2 : (a -> b -> Type) -> Type +Located2 f = forall x, y. Located (f x y) + public export interface Located a => Relocatable a where setLoc : Loc -> a -> a diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr index 57c6754..c6b3435 100644 --- a/lib/Quox/Name.idr +++ b/lib/Quox/Name.idr @@ -4,7 +4,7 @@ import Quox.Loc import Quox.CharExtra import public Data.SnocList import Data.List -import Control.Eff +import Quox.EffExtra import Text.Lexer import Derive.Prelude @@ -178,23 +178,22 @@ export runNameGen : Has NameGen fs => Eff fs a -> Eff (fs - NameGen) a runNameGen = map fst . runNameGenWith 0 +export +gen : Has NameGen fs => Eff fs Nat +gen = stateAt GEN $ \i => SR {result = i, state = S i} + ||| generate a fresh name with the given base export mn : Has NameGen fs => PBaseName -> Eff fs BaseName -mn base = do - i <- getAt GEN - modifyAt GEN S - pure $ MN base i +mn base = MN base <$> gen -||| generate a fresh binding name with the given base and -||| (optionally) location `loc` +||| generate a fresh binding name with the given base and location `loc` export -mnb : Has NameGen fs => - PBaseName -> {default noLoc loc : Loc} -> Eff fs BindName -mnb base = pure $ BN !(mn base) loc +mnb : Has NameGen fs => PBaseName -> Loc -> Eff fs BindName +mnb base loc = pure $ BN !(mn base) loc export fresh : Has NameGen fs => BindName -> Eff fs BindName -fresh (BN (UN str) loc) = mnb str {loc} -fresh (BN (MN str k) loc) = mnb str {loc} -fresh (BN Unused loc) = mnb "x" {loc} +fresh (BN (UN str) loc) = mnb str loc +fresh (BN (MN str k) loc) = mnb str loc +fresh (BN Unused loc) = mnb "x" loc diff --git a/lib/Quox/No.idr b/lib/Quox/No.idr index 948eaf6..56f9a07 100644 --- a/lib/Quox/No.idr +++ b/lib/Quox/No.idr @@ -52,3 +52,18 @@ export %inline nchoose : (b : Bool) -> Either (So b) (No b) nchoose True = Left Oh nchoose False = Right Ah + + +private +0 notFalseTrue : (a : Bool) -> not a = True -> a = False +notFalseTrue False Refl = Refl + +export %inline +soNot : So (not a) -> No a +soNot x with 0 (not a) proof eq + soNot Oh | True = + rewrite notFalseTrue a eq in Ah + +export %inline +soNot' : So a -> No (not a) +soNot' Oh = Ah diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index 7ca26e5..4514245 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -150,6 +150,23 @@ mutual Pair s t loc => Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t <*> pure loc + W x s t loc => + W <$> fromPTermWith ds ns s + <*> fromPTermTScope ds ns [< x] t + <*> pure loc + + Sup s t loc => + Sup <$> fromPTermWith ds ns s + <*> fromPTermWith ds ns t + <*> pure loc + + Case pi tree (r, ret) (CaseW x y (rh, ih) body _) loc => + map E $ CaseW (fromPQty pi) (fromPQty rh) + <$> fromPTermElim ds ns tree + <*> fromPTermTScope ds ns [< r] ret + <*> fromPTermTScope ds ns [< x, y, ih] body + <*> pure loc + Case pi pair (r, ret) (CasePair (x, y) body _) loc => map E $ CasePair (fromPQty pi) <$> fromPTermElim ds ns pair @@ -157,13 +174,6 @@ mutual <*> fromPTermTScope ds ns [< x, y] body <*> pure loc - Case pi tag (r, ret) (CaseEnum arms _) loc => - map E $ CaseEnum (fromPQty pi) - <$> fromPTermElim ds ns tag - <*> fromPTermTScope ds ns [< r] ret - <*> assert_total fromPTermEnumArms ds ns arms - <*> pure loc - Nat loc => pure $ Nat loc Zero loc => pure $ Zero loc Succ n loc => [|Succ (fromPTermWith ds ns n) (pure loc)|] @@ -185,6 +195,13 @@ mutual Tag str loc => pure $ Tag str loc + Case pi tag (r, ret) (CaseEnum arms _) loc => + map E $ CaseEnum (fromPQty pi) + <$> fromPTermElim ds ns tag + <*> fromPTermTScope ds ns [< r] ret + <*> assert_total fromPTermEnumArms ds ns arms + <*> pure loc + Eq (i, ty) s t loc => Eq <$> fromPTermDScope ds ns [< i] ty <*> fromPTermWith ds ns s diff --git a/lib/Quox/Parser/Lexer.idr b/lib/Quox/Parser/Lexer.idr index a6b1fee..d0bbbdd 100644 --- a/lib/Quox/Parser/Lexer.idr +++ b/lib/Quox/Parser/Lexer.idr @@ -197,6 +197,8 @@ reserved = Sym "×" `Or` Sym "**", Sym "≡" `Or` Sym "==", Sym "∷" `Or` Sym "::", + Sym "⊲" `Or` Sym "<|", + Sym "⋄" `Or` Sym "<>", Punc1 '.', Word1 "case", Word1 "case0", Word1 "case1", diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index 549d09d..88c7cfc 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -212,7 +212,8 @@ export qtyPatVar : FileName -> Grammar True (PQty, PatVar) qtyPatVar fname = [|(,) (qty fname) (needRes "." *> patVar fname)|] - <|> [|(,) (defLoc fname $ PQ One) (patVar fname)|] + <|> do name <- patVar fname + pure (PQ (if isUnused name then Zero else One) name.loc, name) export @@ -226,15 +227,17 @@ data PCasePat = | PZero Loc | PSucc PatVar PQty PatVar Loc | PBox PatVar Loc + | PSup PatVar PatVar PQty PatVar Loc %runElab derive "PCasePat" [Eq, Ord, Show] export Located PCasePat where - (PPair _ _ loc).loc = loc - (PTag _ loc).loc = loc - (PZero loc).loc = loc - (PSucc _ _ _ loc).loc = loc - (PBox _ loc).loc = loc + (PPair _ _ loc).loc = loc + (PTag _ loc).loc = loc + (PZero loc).loc = loc + (PSucc _ _ _ loc).loc = loc + (PBox _ loc).loc = loc + (PSup _ _ _ _ loc).loc = loc ||| either `zero` or `0` export @@ -251,6 +254,11 @@ casePat fname = withLoc fname $ ih <- resC "," *> qtyPatVar fname <|> [|(,) (defLoc fname $ PQ Zero) (unused fname)|] pure $ PSucc p (fst ih) (snd ih) + <|> do x <- patVar fname + y <- resC "⋄" *> patVar fname + ih <- resC "," *> qtyPatVar fname + <|> [|(,) (defLoc fname $ PQ Zero) (unused fname)|] + pure $ PSup x y (fst ih) (snd ih) <|> delim "[" "]" [|PBox (patVar fname)|] <|> fatalError "invalid pattern" @@ -405,12 +413,19 @@ appTerm fname = <|> succTerm fname <|> normalAppTerm fname +export +supTerm : FileName -> Grammar True PTerm +supTerm fname = withLoc fname $ do + l <- appTerm fname; commit + r <- optional $ res "⋄" *> assert_total supTerm fname + pure $ \loc => maybe l (\r => Sup l r loc) r + export infixEqTerm : FileName -> Grammar True PTerm infixEqTerm fname = withLoc fname $ do - l <- appTerm fname; commit + l <- supTerm fname; commit rest <- optional $ res "≡" *> - [|(,) (assert_total term fname) (needRes ":" *> appTerm fname)|] + [|(,) (assert_total term fname) (needRes ":" *> supTerm fname)|] let u = Unused $ onlyStart l.loc pure $ \loc => maybe l (\rest => Eq (u, snd rest) l (fst rest) loc) rest @@ -430,8 +445,38 @@ lamTerm fname = withLoc fname $ do body <- assert_total term fname; commit pure $ \loc => foldr (\x, s => k x s loc) body xs + +private +data BindType = BPi | BW | BSig +%runElab derive "BindType" [Eq, Ord] + +private +data BindSequence' b a = BLast a | BMore a b (BindSequence' b a) + +private +data BindTypeL = BTL BindType Loc +%runElab derive "BindTypeL" [Eq, Ord] + +private +data BindPart = BT (Maybe PQty) (List1 PatVar) PTerm +Located BindPart where + (BT q xs t).loc = maybe (head xs).loc (.loc) q `extendL` t.loc + + +private +BindSequence : Type +BindSequence = BindSequence' BindTypeL BindPart + +private +bindType : FileName -> Grammar True BindTypeL +bindType fname = bt BPi "→" <|> bt BW "⊲" <|> bt BSig "×" +where + bt : BindType -> (s : String) -> (0 _ : IsReserved s) => + Grammar True BindTypeL + bt t str = withLoc fname $ resC str $> BTL t + -- [todo] fix the backtracking in e.g. (F x y z × B) -export +private properBinders : FileName -> Grammar True (List1 PatVar, PTerm) properBinders fname = assert_total $ do -- putting assert_total directly on `term`, in this one function, @@ -441,61 +486,85 @@ properBinders fname = assert_total $ do t <- term fname; needRes ")" pure (xs, t) -export -sigmaTerm : FileName -> Grammar True PTerm -sigmaTerm fname = - (properBinders fname >>= continueDep) - <|> (annTerm fname >>= continueNondep) -where - continueDep : (List1 PatVar, PTerm) -> Grammar True PTerm - continueDep (names, fst) = withLoc fname $ do - snd <- needRes "×" *> sigmaTerm fname - pure $ \loc => foldr (\x, snd => Sig x fst snd loc) snd names +private +bindPart : FileName -> Grammar True BindPart +bindPart fname = do + qty <- optional $ qty fname <* resC "." + bnd <- properBinders fname + <|> do n <- unused fname + t <- if isJust qty then termArg fname else annTerm fname + pure (singleton n, t) + pure $ uncurry (BT qty) bnd - cross : PTerm -> PTerm -> PTerm - cross l r = let loc = extend' l.loc r.loc.bounds in - Sig (Unused $ onlyStart l.loc) l r loc +private +bindSequence : FileName -> Grammar True BindSequence +bindSequence fname = do + x <- bindPart fname + by <- optional $ do + b <- bindType fname + y <- mustWork $ assert_total bindSequence fname + pure (b, y) + pure $ maybe (BLast x) (\by => BMore x (fst by) (snd by)) by - continueNondep : PTerm -> Grammar False PTerm - continueNondep fst = do - rest <- optional $ resC "×" *> sepBy1 (res "×") (annTerm fname) - pure $ foldr1 cross $ fst ::: maybe [] toList rest +private +fromBindSequence : BindSequence -> Grammar False PTerm +fromBindSequence as = go [<] as where + -- the ol’ shunty + data Elem = E BindPart BindTypeL + + fatalLoc' : Located z => z -> String -> Grammar False a + fatalLoc' z = maybe fatalError fatalLoc z.loc.bounds + + toTerm : BindPart -> Grammar False PTerm + toTerm (BT Nothing (Unused _ ::: []) s) = pure s + toTerm s = fatalLoc' s $ + "binder with no following body\n" ++ + "(maybe some missing parens)" + + fromTerm : PTerm -> BindPart + fromTerm t = BT Nothing (singleton $ Unused t.loc) t + + checkNoQty : String -> Maybe PQty -> Grammar False () + checkNoQty s (Just q) = fatalLoc' q "no quantity allowed with \{s}" + checkNoQty _ _ = pure () + + apply : Elem -> PTerm -> Grammar False PTerm + apply (E s'@(BT mqty xs s) (BTL b _)) t = case b of + BPi => do + let q = fromMaybe (PQ One s.loc) mqty + loc = s'.loc `extendL` t.loc + pure $ foldr (\x, t => Pi q x s t loc) t xs + BW => do + checkNoQty "⊲" mqty + when (length xs /= 1) $ do + let loc = foldr1 extendL $ map (.loc) xs + fatalLoc' loc "only one binding allowed with ⊲" + pure $ W (head xs) s t (s.loc `extendL` t.loc) + BSig => do + checkNoQty "×" mqty + let loc = s'.loc `extendL` t.loc + pure $ foldr (\x, t => Sig x s t loc) t xs + + end : SnocList Elem -> PTerm -> Grammar False PTerm + end [<] t = pure t + end (es :< e) t = end es !(apply e t) + + go : SnocList Elem -> BindSequence -> Grammar False PTerm + go es (BLast a) = do + end es !(toTerm a) + go [<] (BMore a b as) = + go [< E a b] as + go (es :< e@(E a' b')) (BMore a b as) = + if b' > b then do + t <- apply e !(toTerm a) + go (es :< E (fromTerm t) b) as + else + go (es :< e :< E a b) as export -piTerm : FileName -> Grammar True PTerm -piTerm fname = withLoc fname $ do - q <- [|GivenQ $ qty fname <* resC "."|] <|> defLoc fname DefaultQ - dom <- [|Dep $ properBinders fname|] <|> [|Nondep $ ndDom q fname|] - cod <- optional $ do resC "→"; assert_total term fname <* commit - when (needCod q dom && isNothing cod) $ fail "missing function type result" - pure $ maybe (const $ toTerm dom) (makePi q dom) cod -where - data PiQty = GivenQ PQty | DefaultQ Loc - data PiDom = Dep (List1 PatVar, PTerm) | Nondep PTerm +bindTerm : FileName -> Grammar True PTerm +bindTerm fname = fromBindSequence !(bindSequence fname) - ndDom : PiQty -> FileName -> Grammar True PTerm - ndDom (GivenQ _) = termArg -- ｢1.(List A)｣, not ｢1.List A｣ - ndDom (DefaultQ _) = sigmaTerm - - needCod : PiQty -> PiDom -> Bool - needCod (DefaultQ _) (Nondep _) = False - needCod _ _ = True - - toTerm : PiDom -> PTerm - toTerm (Dep (_, s)) = s - toTerm (Nondep s) = s - - toQty : PiQty -> PQty - toQty (GivenQ qty) = qty - toQty (DefaultQ loc) = PQ One loc - - toDoms : PQty -> PiDom -> List1 (PQty, PatVar, PTerm) - toDoms qty (Dep (xs, s)) = [(qty, x, s) | x <- xs] - toDoms qty (Nondep s) = singleton (qty, Unused s.loc, s) - - makePi : PiQty -> PiDom -> PTerm -> Loc -> PTerm - makePi q doms cod loc = - foldr (\(q, x, s), t => Pi q x s t loc) cod $ toDoms (toQty q) doms public export PCaseArm : Type @@ -529,6 +598,9 @@ checkCaseArms loc ((PSucc p q ih _, rhs1) :: rest) = do checkCaseArms loc ((PBox x _, rhs) :: rest) = if null rest then pure $ CaseBox x rhs loc else fatalError "unexpected pattern after box" +checkCaseArms loc ((PSup x y rh ih _, rhs) :: rest) = + if null rest then pure $ CaseW x y (rh, ih) rhs loc + else fatalError "unexpected pattern after sup" export caseBody : FileName -> Grammar True PCaseBody @@ -557,8 +629,7 @@ caseTerm fname = withLoc fname $ do -- term : FileName -> Grammar True PTerm term fname = lamTerm fname <|> caseTerm fname - <|> piTerm fname - <|> sigmaTerm fname + <|> bindTerm fname export diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr index 335eb49..d08ab65 100644 --- a/lib/Quox/Parser/Syntax.idr +++ b/lib/Quox/Parser/Syntax.idr @@ -74,6 +74,9 @@ namespace PTerm | Pair PTerm PTerm Loc | Case PQty PTerm (PatVar, PTerm) PCaseBody Loc + | W PatVar PTerm PTerm Loc + | Sup PTerm PTerm Loc + | Enum (List TagVal) Loc | Tag TagVal Loc @@ -98,6 +101,7 @@ namespace PTerm public export data PCaseBody = CasePair (PatVar, PatVar) PTerm Loc + | CaseW PatVar PatVar (PQty, PatVar) PTerm Loc | CaseEnum (List (PTagVal, PTerm)) Loc | CaseNat PTerm (PatVar, PQty, PatVar, PTerm) Loc | CaseBox PatVar PTerm Loc @@ -114,6 +118,8 @@ Located PTerm where (Sig _ _ _ loc).loc = loc (Pair _ _ loc).loc = loc (Case _ _ _ _ loc).loc = loc + (W _ _ _ loc).loc = loc + (Sup _ _ loc).loc = loc (Enum _ loc).loc = loc (Tag _ loc).loc = loc (Eq _ _ _ loc).loc = loc @@ -131,10 +137,11 @@ Located PTerm where export Located PCaseBody where - (CasePair _ _ loc).loc = loc - (CaseEnum _ loc).loc = loc - (CaseNat _ _ loc).loc = loc - (CaseBox _ _ loc).loc = loc + (CasePair _ _ loc).loc = loc + (CaseW _ _ _ _ loc).loc = loc + (CaseEnum _ loc).loc = loc + (CaseNat _ _ loc).loc = loc + (CaseBox _ _ loc).loc = loc public export diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr index f90e5ec..b8873de 100644 --- a/lib/Quox/Pretty.idr +++ b/lib/Quox/Pretty.idr @@ -24,9 +24,13 @@ data PPrec = Outer | Times -- "_ × _" | InTimes -- arguments of × +| W -- "_ ⊲ _" +| InW -- arguments of ⊲ | AnnL -- left of "∷" | Eq -- "_ ≡ _ : _" | InEq -- arguments of ≡ +| Sup -- "_ ⋄ _" +| InSup -- arguments of ⋄ -- ... | App -- term/dimension application | Arg -- argument to nonfix function @@ -229,10 +233,10 @@ prettyDBind = hl DVar . prettyBind' export %inline -typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD, -eqD, colonD, commaD, semiD, caseD, typecaseD, returnD, -ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD : - {opts : _} -> Eff Pretty (Doc opts) +typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD, triD, diamondD, +eqD, colonD, commaD, semiD, caseD, typecaseD, returnD, ofD, dotD, zeroD, succD, +coeD, compD, undD, cstD, pipeD : + {opts : LayoutOpts} -> Eff Pretty (Doc opts) typeD = hl Syntax . text =<< ifUnicode "★" "Type" arrowD = hl Delim . text =<< ifUnicode "→" "->" darrowD = hl Delim . text =<< ifUnicode "⇒" "=>" @@ -242,6 +246,8 @@ eqndD = hl Delim . text =<< ifUnicode "≡" "==" dlamD = hl Syntax . text =<< ifUnicode "δ" "dfun" annD = hl Delim . text =<< ifUnicode "∷" "::" natD = hl Syntax . text =<< ifUnicode "ℕ" "Nat" +triD = hl Syntax . text =<< ifUnicode "⊲" "<|" +diamondD = hl Syntax . text =<< ifUnicode "⋄" "<>" eqD = hl Syntax $ text "Eq" colonD = hl Delim $ text ":" commaD = hl Delim $ text "," diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr index 8bc1d9a..4257743 100644 --- a/lib/Quox/Reduce.idr +++ b/lib/Quox/Reduce.idr @@ -78,6 +78,12 @@ isPairHead (Ann (Pair {}) (Sig {}) _) = True isPairHead (Coe {}) = True isPairHead _ = False +public export %inline +isWHead : Elim {} -> Bool +isWHead (Ann (Sup {}) (W {}) _) = True +isWHead (Coe {}) = True +isWHead _ = False + public export %inline isTagHead : Elim {} -> Bool isTagHead (Ann (Tag {}) (Enum {}) _) = True @@ -115,6 +121,8 @@ isTyCon (Pi {}) = True isTyCon (Lam {}) = False isTyCon (Sig {}) = True isTyCon (Pair {}) = False +isTyCon (W {}) = True +isTyCon (Sup {}) = False isTyCon (Enum {}) = True isTyCon (Tag {}) = False isTyCon (Eq {}) = True @@ -128,6 +136,37 @@ isTyCon (E {}) = False isTyCon (CloT {}) = False isTyCon (DCloT {}) = False +||| canPushCoe A s is true if a coercion along (𝑖 ⇒ A) on s can be pushed. +||| for a type with η like functions, or a ground type like ℕ, +||| this is true for any s. +||| otherwise, like for pairs, it is only true if s is a constructor form. +||| if A isn't a type, or isn't in whnf, then the question is meaningless. but +||| it returns False anyway. +public export %inline +canPushCoe : Term (S d) n -> Term d n -> Bool +canPushCoe (TYPE {}) _ = True +canPushCoe (Pi {}) _ = True +canPushCoe (Lam {}) _ = False +canPushCoe (Sig {}) (Pair {}) = True +canPushCoe (Sig {}) _ = False +canPushCoe (Pair {}) _ = False +canPushCoe (W {}) (Sup {}) = True +canPushCoe (W {}) _ = False +canPushCoe (Sup {}) _ = False +canPushCoe (Enum {}) _ = True +canPushCoe (Tag {}) _ = False +canPushCoe (Eq {}) _ = True +canPushCoe (DLam {}) _ = False +canPushCoe (Nat {}) _ = True +canPushCoe (Zero {}) _ = False +canPushCoe (Succ {}) _ = False +canPushCoe (BOX {}) _ = True +canPushCoe (Box {}) _ = False +canPushCoe (E {}) _ = False +canPushCoe (CloT {}) _ = False +canPushCoe (DCloT {}) _ = False + + ||| true if a term is syntactically a type, or a neutral. public export %inline isTyConE : Term {} -> Bool @@ -155,6 +194,8 @@ mutual isRedexE defs fun || isLamHead fun isRedexE defs (CasePair {pair, _}) = isRedexE defs pair || isPairHead pair + isRedexE defs (CaseW {tree, _}) = + isRedexE defs tree || isWHead tree isRedexE defs (CaseEnum {tag, _}) = isRedexE defs tag || isTagHead tag isRedexE defs (CaseNat {nat, _}) = @@ -165,8 +206,9 @@ mutual isRedexE defs fun || isDLamHead fun || isK arg isRedexE defs (Ann {tm, ty, _}) = isE tm || isRedexT defs tm || isRedexT defs ty - isRedexE defs (Coe {val, _}) = - isRedexT defs val || not (isE val) + isRedexE defs (Coe {ty, val, _}) = + let ty = assert_smaller ty ty.term in + isRedexT defs ty || canPushCoe ty val isRedexE defs (Comp {ty, r, _}) = isRedexT defs ty || isK r isRedexE defs (TypeCase {ty, ret, _}) = @@ -204,16 +246,36 @@ tycaseRhsDef0 : Term d n -> (k : TyConKind) -> TypeCaseArms d n -> tycaseRhsDef0 def k arms = fromMaybe def $ tycaseRhs0 k arms +export +weakAtT : (CanTSubst f, Located2 f) => (by, at : Nat) -> + f d (at + n) -> f d (at + (by + n)) +weakAtT by at t = t `CanTSubst.(//)` pushN at (shift by) t.loc -private -weakDS : (by : Nat) -> DScopeTerm d n -> DScopeTerm d (by + n) -weakDS by (S names (Y body)) = S names $ Y $ weakT by body -weakDS by (S names (N body)) = S names $ N $ weakT by body +export +weakAtD : (CanDSubst f, Located2 f) => (by, at : Nat) -> + f (at + d) n -> f (at + (by + d)) n +weakAtD by at t = t `CanDSubst.(//)` pushN at (shift by) t.loc -private -dweakS : (by : Nat) -> ScopeTerm d n -> ScopeTerm (by + d) n -dweakS by (S names (Y body)) = S names $ Y $ dweakT by body -dweakS by (S names (N body)) = S names $ N $ dweakT by body +parameters {s : Nat} + export + weakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s d (by + n) + weakS by (S names (Y body)) = S names $ Y $ weakAtT by s body + weakS by (S names (N body)) = S names $ N $ weakT by body + + export + weakDS : (by : Nat) -> DScopeTermN s d n -> DScopeTermN s d (by + n) + weakDS by (S names (Y body)) = S names $ Y $ weakT by body + weakDS by (S names (N body)) = S names $ N $ weakT by body + + export + dweakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s (by + d) n + dweakS by (S names (Y body)) = S names $ Y $ dweakT by body + dweakS by (S names (N body)) = S names $ N $ dweakT by body + + export + dweakDS : (by : Nat) -> DScopeTermN s d n -> DScopeTermN s (by + d) n + dweakDS by (S names (Y body)) = S names $ Y $ weakAtD by s body + dweakDS by (S names (N body)) = S names $ N $ dweakT by body private coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d -> Loc -> @@ -246,6 +308,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) | t => throw $ ExpectedPi loc ctx.names t pure $ sub1 res $ Ann s arg loc computeElimType (CasePair {pair, ret, _}) = pure $ sub1 ret pair + computeElimType (CaseW {tree, ret, _}) = pure $ sub1 ret tree computeElimType (CaseEnum {tag, ret, _}) = pure $ sub1 ret tag computeElimType (CaseNat {nat, ret, _}) = pure $ sub1 ret nat computeElimType (CaseBox {box, ret, _}) = pure $ sub1 ret box @@ -269,7 +332,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n) tycasePi (E e) {tnf} = do ty <- computeElimType defs ctx e @{noOr2 tnf} let loc = e.loc - narg = mnb "Arg"; nret = mnb "Ret" + narg = mnb "Arg" loc; nret = mnb "Ret" loc arg = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret] (BVT 0 loc) loc @@ -287,7 +350,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n) tycaseSig (E e) {tnf} = do ty <- computeElimType defs ctx e @{noOr2 tnf} let loc = e.loc - nfst = mnb "Fst"; nsnd = mnb "Snd" + nfst = mnb "Fst" loc; nsnd = mnb "Snd" loc fst = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd] (BVT 0 loc) loc @@ -295,6 +358,24 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n) pure (fst, snd) tycaseSig t = throw $ ExpectedSig t.loc ctx.names t + ||| for (x : A) ⊲ B, returns (A, B); + ||| for an elim returns a pair of type-cases that will reduce to that; + ||| for other intro forms error + private covering + tycaseW : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) => + Eff Whnf (Term (S d) n, ScopeTerm (S d) n) + tycaseW (W {shape, body, _}) = pure (shape, body) + tycaseW (E e) {tnf} = do + ty <- computeElimType defs ctx e @{noOr2 tnf} + let loc = e.loc + nshape = mnb "Shape" loc; nbody = mnb "Body" loc + shape = E $ typeCase1Y e ty KW [< !nshape, !nbody] (BVT 1 loc) loc + body' = typeCase1Y e (Arr Zero shape ty loc) KW [< !nshape, !nbody] + (BVT 0 loc) loc + body = ST [< !nshape] $ E $ App (weakE 1 body') (BVT 0 loc) loc + pure (shape, body) + tycaseW t = throw $ ExpectedW t.loc ctx.names t + ||| for [π. A], returns A; ||| for an elim returns a type-case that will reduce to that; ||| for other intro forms error @@ -303,8 +384,9 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n) Eff Whnf (Term (S d) n) tycaseBOX (BOX {ty, _}) = pure ty tycaseBOX (E e) {tnf} = do + let loc = e.loc ty <- computeElimType defs ctx e @{noOr2 tnf} - pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty")] (BVT 0 e.loc) e.loc + pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty" loc)] (BVT 0 loc) loc tycaseBOX t = throw $ ExpectedBOX t.loc ctx.names t ||| for Eq [i ⇒ A] l r, returns (A‹0/i›, A‹1/i›, A, l, r); @@ -318,11 +400,11 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n) tycaseEq (E e) {tnf} = do ty <- computeElimType defs ctx e @{noOr2 tnf} let loc = e.loc - names = traverse' (\x => mnb x) [< "A0", "A1", "A", "L", "R"] + names = traverse' (\x => mnb x loc) [< "A0", "A1", "A", "l", "r"] a0 = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc a1 = E $ typeCase1Y e ty KEq !names (BVT 3 loc) loc a' = typeCase1Y e (Eq0 ty a0 a1 loc) KEq !names (BVT 2 loc) loc - a = DST [< !(mnb "i")] $ E $ DApp (dweakE 1 a') (B VZ loc) loc + a = DST [< !(mnb "i" loc)] $ E $ DApp (dweakE 1 a') (B VZ loc) loc l = E $ typeCase1Y e a0 KEq !names (BVT 1 loc) loc r = E $ typeCase1Y e a1 KEq !names (BVT 0 loc) loc pure (a0, a1, a, l, r) @@ -337,9 +419,12 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) (val, s : Term d n) -> Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) piCoe sty@(S [< i] ty) p q val s loc = do - -- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝ - -- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›) - -- where 𝒔‹j› ≔ coe [i ⇒ A] @q @j s + -- 𝒮‹𝑘› ≔ π.(x : A‹𝑘/𝑖›) → B‹𝑘/𝑖› + -- 𝓈‹𝑘› ≔ coe [𝑖 ⇒ A] @q @𝑘 s + -- ------------------------------------------------------- + -- (coe [𝑖 ⇒ 𝒮‹𝑖›] @p @q t) s + -- ⇝ + -- coe [i ⇒ B[𝓈‹i›/x] @p @q ((t ∷ 𝒮‹p›) 𝓈‹p›) -- -- type-case is used to expose A,B if the type is neutral let ctx1 = extendDim i ctx @@ -358,11 +443,11 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) sigCoe qty sty@(S [< i] ty) p q val ret body loc = do - -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e } + -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ u } -- ⇝ -- caseπ s ∷ ((x : A) × B)‹p/i› return z ⇒ C -- of { (a, b) ⇒ - -- e[(coe [i ⇒ A] @p @q a)/a, + -- u[(coe [i ⇒ A] @p @q a)/a, -- (coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i a)/x]] @p @q b)/b] } -- -- type-case is used to expose A,B if the type is neutral @@ -370,14 +455,58 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) Element ty tynf <- whnf defs ctx1 ty.term (tfst, tsnd) <- tycaseSig defs ctx1 ty let [< x, y] = body.names - a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc + a' = CoeT i (weakT 2 tfst) p q (BVT 1 x.loc) x.loc tsnd' = tsnd.term // - (CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2)) - (weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2) - b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc - whnf defs ctx $ CasePair qty (Ann val (ty // one p) val.loc) ret + (CoeT !(fresh i) (weakT 2 $ tfst // (B VZ i.loc ::: shift 2)) + (weakD 1 p) (B VZ i.loc) (BVT 1 x.loc) y.loc ::: shift 2) + b' = CoeT i tsnd' p q (BVT 0 y.loc) y.loc + whnf defs ctx $ CasePair qty (Ann val (dsub1 sty p) val.loc) ret (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc + ||| reduce a w elimination `CaseW pi piIH (Coe ty p q val) ret body loc` + private covering + wCoe : (qty, qtyIH : Qty) -> + (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> + (ret : ScopeTerm d n) -> (body : ScopeTermN 3 d n) -> Loc -> + Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) + wCoe qty qtyIH sty@(S [< i] ty) p q val ret body loc = do + -- 𝒮‹𝑘› ≔ ((x : A) ⊲ B)‹𝑘/𝑖› + -- 𝒶‹𝑘› ≔ coe [𝑖 ⇒ A] @p @𝑘 a + -- : A‹𝑘/𝑖› + -- 𝒷‹𝑘› ≔ coe [𝑖 ⇒ ω.B[𝒶‹𝑖›/x] → 𝒮‹𝑖›] @p @𝑘 b + -- : ω.B‹𝑘/𝑖›[𝒶‹𝑘›/x] → 𝒮‹𝑘› + -- 𝒾𝒽 ≔ coe [𝑖 ⇒ π.(z : B[𝒶‹𝑖›/x]) → C[𝒷‹𝑖› z/p]] @p @q ih + -- : π.(z : B‹q/𝑖›[𝒶‹q›/x]) → C[𝒷‹q› z/p] + -- -------------------------------------------------------------------- + -- caseπ (coe [𝑖 ⇒ 𝒮‹𝑖›] @p @q s) return z ⇒ C of { a ⋄ b, ς.ih ⇒ u } + -- ⇝ + -- caseπ s ∷ 𝒮‹p› return z ⇒ C + -- of { a ⋄ b, ς.ih ⇒ u[𝒶‹q›/a, 𝒷‹q›/b, 𝒾𝒽/ih] } + let ctx1 = extendDim i ctx + Element ty tynf <- whnf defs ctx1 ty.term + (shape, tbody) <- tycaseW defs ctx1 ty + let [< a, b, ih] = body.names + ai <- fresh i; bi <- fresh i; ihi <- fresh i; z <- mnb "z" ih.loc + let a', b' : forall d'. (by : Shift d d') => Dim d' -> Elim d' (3 + n) + a' k = + let shape' = shape // Shift (weak 1 by) // shift 3 in + CoeT ai shape' (p // by) k (BVT 2 a.loc) a.loc + b' k = + let tbody' = tbody.term // Shift (weak 1 by) + // (a' (BV 0 bi.loc) ::: shift 3) + ty' = ty // Shift (weak 1 by) // shift 3 + in + CoeT bi (Arr Any tbody' ty' b.loc) (p // by) k (BVT 1 b.loc) b.loc + ih' : Elim d (3 + n) := + let tbody' = tbody.term // (a' (BV 0 ihi.loc) ::: shift 3) + ret' = sub1 (weakS 4 $ dweakS 1 ret) $ + App (weakE 1 $ b' (BV 0 ihi.loc)) (BVT 0 z.loc) ih.loc + ty = PiY qty z tbody' ret' ih.loc + in + CoeT ihi ty p q (BVT 0 ih.loc) ih.loc + whnf defs ctx $ CaseW qty qtyIH (Ann val (dsub1 sty p) val.loc) ret + (ST body.names $ body.term // (a' q ::: b' q ::: ih' ::: shift 3)) loc + ||| reduce a dimension application `DApp (Coe ty p q val) r loc` private covering eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> @@ -392,7 +521,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) Element ty tynf <- whnf defs ctx1 ty.term (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty let a' = dsub1 a (weakD 1 r) - val' = E $ DApp (Ann val (ty // one p) val.loc) r loc + val' = E $ DApp (Ann val (dsub1 sty p) val.loc) r loc whnf defs ctx $ CompH j a' p q val' r j s j t loc ||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body` @@ -409,8 +538,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) let ctx1 = extendDim i ctx Element ty tynf <- whnf defs ctx1 ty.term ta <- tycaseBOX defs ctx1 ty - let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc - whnf defs ctx $ CaseBox qty (Ann val (ty // one p) val.loc) ret + let a' = CoeT i (weakT 1 ta) p q (BVT 0 body.name.loc) body.name.loc + whnf defs ctx $ CaseBox qty (Ann val (dsub1 sty p) val.loc) ret (ST body.names $ body.term // (a' ::: shift 1)) loc @@ -429,19 +558,29 @@ reduceTypeCase defs ctx ty u ret arms def loc = case ty of -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝ -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q Pi {arg, res, loc = piLoc, _} => - let arg' = Ann arg (TYPE u noLoc) arg.loc + let arg' = Ann arg (TYPE u arg.loc) arg.loc res' = Ann (Lam res res.loc) - (Arr Zero arg (TYPE u noLoc) arg.loc) res.loc + (Arr Zero arg (TYPE u arg.loc) arg.loc) res.loc in whnf defs ctx $ Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc + -- (type-case (x : A) ⊲ π.B ∷ ★ᵢ return Q of { (a ⊲ b) ⇒ s; ⋯ }) ⇝ + -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q + W {shape, body, loc = wLoc, _} => + let shape' = Ann shape (TYPE u shape.loc) shape.loc + body' = Ann (Lam body body.loc) + (Arr Zero shape (TYPE u shape.loc) shape.loc) body.loc + in + whnf defs ctx $ + Ann (subN (tycaseRhsDef def KW arms) [< shape', body']) ret loc + -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝ -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q Sig {fst, snd, loc = sigLoc, _} => - let fst' = Ann fst (TYPE u noLoc) fst.loc + let fst' = Ann fst (TYPE u fst.loc) fst.loc snd' = Ann (Lam snd snd.loc) - (Arr Zero fst (TYPE u noLoc) fst.loc) snd.loc + (Arr Zero fst (TYPE u fst.loc) fst.loc) snd.loc in whnf defs ctx $ Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc @@ -459,8 +598,8 @@ reduceTypeCase defs ctx ty u ret arms def loc = case ty of let a0 = a.zero; a1 = a.one in whnf defs ctx $ Ann (subN (tycaseRhsDef def KEq arms) - [< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) a.loc, - Ann (DLam a a.loc) (Eq0 (TYPE u noLoc) a0 a1 a.loc) a.loc, + [< Ann a0 (TYPE u a.loc) a.loc, Ann a1 (TYPE u a.loc) a.loc, + Ann (DLam a a.loc) (Eq0 (TYPE u a.loc) a0 a1 a.loc) a.loc, Ann l a0 l.loc, Ann r a1 r.loc]) ret loc @@ -471,99 +610,113 @@ reduceTypeCase defs ctx ty u ret arms def loc = case ty of -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q BOX {ty = a, loc = boxLoc, _} => whnf defs ctx $ Ann - (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u noLoc) a.loc)) + (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u a.loc) a.loc)) ret loc ||| pushes a coercion inside a whnf-ed term private covering pushCoe : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n -> - BindName -> - (ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) => + BindName -> (ty : Term (S d) n) -> Dim d -> Dim d -> - (s : Term d n) -> (0 snf : No (isRedexT defs s)) => Loc -> + (s : Term d n) -> (0 snf : No (isRedexT defs s)) => + (0 pc : So (canPushCoe ty s)) => Loc -> Eff Whnf (NonRedex Elim d n defs) pushCoe defs ctx i ty p q s loc = if p == q then whnf defs ctx $ Ann s (ty // one q) loc else - case s of - -- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ) - TYPE {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - Pi {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - Sig {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - Enum {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - Eq {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - Nat {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - BOX {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc + case ty of + -- (coe ★ᵢ @p @q s) ⇝ (s ∷ ★ᵢ) + -- + -- no η (what would that even mean), but ground type + TYPE {l, loc = tyLoc} => + whnf defs ctx $ Ann s (TYPE l tyLoc) loc -- just η expand it. then whnf for App will handle it later -- this is how @xtt does it -- - -- (coe [i ⇒ A] @p @q (λ x ⇒ s)) ⇝ - -- (λ y ⇒ (coe [i ⇒ A] @p @q (λ x ⇒ s)) y) ∷ A‹q/i› ⇝ ⋯ - lam@(Lam {body, _}) => do - let lam' = CoeT i ty p q lam loc - term' = LamY !(fresh body.name) - (E $ App (weakE 1 lam') (BVT 0 noLoc) loc) loc - type' = ty // one q - whnf defs ctx $ Ann term' type' loc + -- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) ⇝ + -- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) + -- ∷ (π.(x : A) → B)‹q/𝑖› + Pi {} => do + y <- mnb "y" loc + let s' = Coe (SY [< i] ty) p q s loc + body = SY [< y] $ E $ App (weakE 1 s') (BVT 0 y.loc) s.loc + ret = ty // one q + whnf defs ctx $ Ann (Lam body loc) ret loc -- (coe [i ⇒ (x : A) × B] @p @q (s, t)) ⇝ -- (coe [i ⇒ A] @p @q s, -- coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i s)/x]] @p @q t) -- ∷ (x : A‹q/i›) × B‹q/i› -- - -- can't use η here because... it doesn't exist - Pair {fst, snd, loc = pairLoc} => do - let Sig {fst = tfst, snd = tsnd, loc = sigLoc} = ty - | _ => throw $ ExpectedSig ty.loc (extendDim i ctx.names) ty - let fst' = E $ CoeT i tfst p q fst fst.loc - tfst' = tfst // (B VZ noLoc ::: shift 2) + -- no η so only reduce on an actual pair 🍐 + Sig {fst = tfst, snd = tsnd, loc = tyLoc} => do + let Pair fst snd sLoc = s + fst' = E $ CoeT i tfst p q fst fst.loc + tfst' = tfst // (B VZ i.loc ::: shift 2) tsnd' = sub1 tsnd $ - CoeT !(fresh i) tfst' (weakD 1 p) (B VZ noLoc) - (dweakT 1 fst) fst.loc + CoeT !(fresh i) tfst' (weakD 1 p) (B VZ snd.loc) + (dweakT 1 fst) snd.loc snd' = E $ CoeT i tsnd' p q snd snd.loc - pure $ - Element (Ann (Pair fst' snd' pairLoc) - (Sig (tfst // one q) (tsnd // one q) sigLoc) loc) Ah + pure $ nred $ + Ann (Pair fst' snd' sLoc) + (Sig (tfst // one q) (tsnd // one q) tyLoc) loc + + -- (coe [i ⇒ (x : A) ⊲ π.B] @p @q (s ⋄ t) ⇝ + -- (coe [i ⇒ A] @p @q s ⋄ + -- coe [i ⇒ ω.B[coe [j ⇒ A‹j/i›] @p @i s/x] → (x : A) ⊲ B] t) + -- ∷ ((x : A) ⊲ B)‹q/i› + -- + -- again, no η + W {shape, body, loc = tyLoc} => do + let Sup root sub sLoc = s + root' = E $ CoeT i shape p q root root.loc + shape' = shape // (B VZ i.loc ::: shift 2) + coeRoot = + CoeT (setLoc shape.loc !(fresh i)) shape' + (weakD 1 p) (B VZ i.loc) (dweakT 1 root) root.loc + tsub' = Arr Any (sub1 body coeRoot) ty sub.loc + sub' = E $ CoeT i tsub' p q sub sub.loc + pure $ nred $ + Ann (Sup root' sub' sLoc) + (W (shape // one q) (body // one q) tyLoc) loc + + -- (coe {𝗮, …} @p @q s) ⇝ (s ∷ {𝗮, …}) + -- + -- no η, but ground type + Enum {cases, loc = tyLoc} => + whnf defs ctx $ Ann s (Enum cases tyLoc) loc -- η expand, like for Lam -- - -- (coe [i ⇒ A] @p @q (δ j ⇒ s)) ⇝ - -- (δ k ⇒ (coe [i ⇒ A] @p @q (δ j ⇒ s)) @k) ∷ A‹q/i› ⇝ ⋯ - dlam@(DLam {body, _}) => do - let dlam' = CoeT i ty p q dlam loc - term' = DLamY !(mnb "j") - (E $ DApp (dweakE 1 dlam') (B VZ noLoc) loc) loc - type' = ty // one q - whnf defs ctx $ Ann term' type' loc + -- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) ⇝ + -- (δ k ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @k) + -- ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖› + Eq {} => do + k <- mnb "k" loc + let s' = Coe (SY [< i] ty) p q s loc + term = DLam (SY [< k] $ E $ DApp (dweakE 1 s') (BV 0 k.loc) loc) loc + ret = ty // one q + whnf defs ctx $ Ann term ret loc - -- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯}) - Tag {tag, loc = tagLoc} => do - let Enum {cases, loc = enumLoc} = ty - | _ => throw $ ExpectedEnum ty.loc (extendDim i ctx.names) ty - pure $ Element (Ann (Tag tag tagLoc) (Enum cases enumLoc) loc) Ah + -- (coe ℕ @p @q s) ⇝ (s ∷ ℕ) + -- + -- no η, but ground type + Nat {loc = tyLoc} => + whnf defs ctx $ Ann s (Nat tyLoc) loc - -- (coe [_ ⇒ ℕ] @_ @_ n) ⇝ (n ∷ ℕ) - Zero {loc = zeroLoc} => do - pure $ Element (Ann (Zero zeroLoc) (Nat ty.loc) loc) Ah - Succ {p = pred, loc = succLoc} => do - pure $ Element (Ann (Succ pred succLoc) (Nat ty.loc) loc) Ah - - -- (coe [i ⇒ [π.A]] @p @q [s]) ⇝ - -- [coe [i ⇒ A] @p @q s] ∷ [π. A‹q/i›] - Box {val, loc = boxLoc} => do - let BOX {qty, ty = a, loc = tyLoc} = ty - | _ => throw $ ExpectedBOX ty.loc (extendDim i ctx.names) ty - pure $ Element - (Ann (Box (E $ CoeT i a p q val val.loc) boxLoc) - (BOX qty (a // one q) tyLoc) loc) - Ah - - E e => pure $ Element (CoeT i ty p q (E e) e.loc) (snf `orNo` Ah) -where - unwrapTYPE : Term (S d) n -> Eff Whnf Universe - unwrapTYPE (TYPE {l, _}) = pure l - unwrapTYPE ty = throw $ ExpectedTYPE ty.loc (extendDim i ctx.names) ty + -- (coe (𝑖 ⇒ [π. A]) @p @q s) ⇝ + -- [coe (𝑖 ⇒ A) @p @q (case1 s ∷ [π. A‹p/𝑖›] return A‹p/𝑖› of {[x] ⇒ x})] + -- ∷ [π. A‹q/𝑖›] + -- + -- [todo] box should probably have an η rule + BOX {qty, ty = innerTy, loc = tyLoc} => do + let s' = Ann s (BOX qty (innerTy // one p) tyLoc) s.loc + inner' = CaseBox One s' (SN $ innerTy // one p) + (SY [< !(mnb "x" s.loc)] $ BVT 0 s.loc) s.loc + inner = Box (E $ CoeT i innerTy p q (E inner') loc) loc + ret = BOX qty (innerTy // one q) tyLoc + whnf defs ctx $ Ann inner ret loc export covering @@ -585,8 +738,12 @@ CanWhnf Elim Reduce.isRedexE where Coe ty p q val _ => piCoe defs ctx ty p q val s appLoc Right nlh => pure $ Element (App f s appLoc) $ fnf `orNo` nlh - -- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝ - -- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p] + -- s' ≔ s ∷ A + -- t' ≔ t ∷ B[s'/x] + -- st' ≔ (s, t) ∷ (x : A) × B + -- C' ≔ C[st'/p] + -- --------------------------------------------------------------- + -- case st' return p ⇒ C of { (a, b) ⇒ u } ⇝ u[s'/a, t'/x]] ∷ C' whnf defs ctx (CasePair pi pair ret body caseLoc) = do Element pair pairnf <- whnf defs ctx pair case nchoose $ isPairHead pair of @@ -601,6 +758,43 @@ CanWhnf Elim Reduce.isRedexE where Right np => pure $ Element (CasePair pi pair ret body caseLoc) $ pairnf `orNo` np + -- s' ≔ s ∷ A + -- t' ≔ t ∷ ω.B[s'/x] → (x : A) ⊲ B + -- ih' ≔ (λ x ⇒ caseπ t x return p ⇒ C of { (a ⋄ b), ς.ih ⇒ u }) ∷ + -- π.(y : B[s'/x]) → C[t' y/p] + -- st' ≔ s ⋄ t ∷ (x : A) ⊲ B + -- C' ≔ C[st'/p] + -- -------------------------------------------------------------------- + -- caseπ st' return p ⇒ C of { a ⋄ b, ς.ih ⇒ u } + -- ⇝ + -- u[s'/a, t'/b, ih'/ih] ∷ C' + whnf defs ctx (CaseW qty qtyIH tree ret body caseLoc) = do + Element tree treenf <- whnf defs ctx tree + case nchoose $ isWHead tree of + Left _ => case tree of + Ann (Sup {root, sub, _}) + w@(W {shape, body = wbody, _}) treeLoc => + let root = Ann root shape root.loc + wbody' = sub1 wbody root + tsub = Arr Any wbody' w sub.loc + sub = Ann sub tsub sub.loc + ih' = LamY !(mnb "y" caseLoc) -- [todo] better name + (E $ CaseW qty qtyIH + (App (weakE 1 sub) (BVT 0 sub.loc) sub.loc) + (weakS 1 ret) (weakS 1 body) caseLoc) sub.loc + ihret = sub1 (weakS 1 ret) + (App (weakE 1 sub) (BVT 0 sub.loc) caseLoc) + tih = PiY qty !(mnb "y" caseLoc) + wbody' ihret caseLoc + ih = Ann ih' tih caseLoc + in + whnf defs ctx $ + Ann (subN body [< root, sub, ih]) (sub1 ret tree) tree.loc + Coe ty p q val _ => do + wCoe defs ctx qty qtyIH ty p q val ret body caseLoc + Right nw => pure $ + Element (CaseW qty qtyIH tree ret body caseLoc) $ treenf `orNo` nw + -- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝ -- u ∷ C['a∷{a,…}/p] whnf defs ctx (CaseEnum pi tag ret arms caseLoc) = do @@ -695,7 +889,10 @@ CanWhnf Elim Reduce.isRedexE where whnf defs ctx (Coe (S [< i] (Y ty)) p q val coeLoc) = do Element ty tynf <- whnf defs (extendDim i ctx) ty Element val valnf <- whnf defs ctx val - pushCoe defs ctx i ty p q val coeLoc + case nchoose $ canPushCoe ty val of + Right n => pure $ Element (Coe (SY [< i] ty) p q val coeLoc) $ + tynf `orNo` n + Left y => pushCoe defs ctx i ty p q val coeLoc whnf defs ctx (Comp ty p q val r zero one compLoc) = -- comp [A] @p @p s { ⋯ } ⇝ s ∷ A @@ -730,6 +927,8 @@ CanWhnf Term Reduce.isRedexT where whnf _ _ t@(Lam {}) = pure $ nred t whnf _ _ t@(Sig {}) = pure $ nred t whnf _ _ t@(Pair {}) = pure $ nred t + whnf _ _ t@(W {}) = pure $ nred t + whnf _ _ t@(Sup {}) = pure $ nred t whnf _ _ t@(Enum {}) = pure $ nred t whnf _ _ t@(Tag {}) = pure $ nred t whnf _ _ t@(Eq {}) = pure $ nred t diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr index 363e082..2b2b7c1 100644 --- a/lib/Quox/Syntax/Dim.idr +++ b/lib/Quox/Syntax/Dim.idr @@ -83,7 +83,7 @@ DSubst : Nat -> Nat -> Type DSubst = Subst Dim -public export FromVar Dim where fromVarLoc = B +public export FromVar Dim where fromVar = B export diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr index c8079d8..0f47bd0 100644 --- a/lib/Quox/Syntax/DimEq.idr +++ b/lib/Quox/Syntax/DimEq.idr @@ -70,13 +70,13 @@ toMaybe (Just x) = Just x export -fromGround' : Context' DimConst d -> DimEq' d -fromGround' [<] = [<] -fromGround' (ctx :< e) = fromGround' ctx :< Just (K e noLoc) +fromGround' : BContext d -> Context' DimConst d -> DimEq' d +fromGround' [<] [<] = [<] +fromGround' (xs :< x) (ctx :< e) = fromGround' xs ctx :< Just (K e x.loc) export -fromGround : Context' DimConst d -> DimEq d -fromGround = C . fromGround' +fromGround : BContext d -> Context' DimConst d -> DimEq d +fromGround = C .: fromGround' public export %inline @@ -243,7 +243,7 @@ prettyCsts : {opts : _} -> BContext d -> DimEq' d -> prettyCsts [<] [<] = pure [<] prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs prettyCsts dnames (eqs :< Just q) = - [|prettyCsts (tail dnames) eqs :< prettyCst dnames (BV 0 noLoc) (weakD 1 q)|] + [|prettyCsts (tail dnames) eqs :< prettyCst dnames (BV 0 q.loc) (weakD 1 q)|] export prettyDimEq' : {opts : _} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts) diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr index 976f7bb..0615879 100644 --- a/lib/Quox/Syntax/Subst.idr +++ b/lib/Quox/Syntax/Subst.idr @@ -49,7 +49,7 @@ interface FromVar term => CanSubstSelf term where public export getLoc : FromVar term => Subst term from to -> Var from -> Loc -> term to -getLoc (Shift by) i loc = fromVarLoc (shift by i) loc +getLoc (Shift by) i loc = fromVar (shift by i) loc getLoc (t ::: th) VZ _ = t getLoc (t ::: th) (VS i) loc = getLoc th i loc @@ -95,18 +95,18 @@ map f (t ::: th) = f t ::: map f th public export %inline -push : CanSubstSelf f => Subst f from to -> Subst f (S from) (S to) -push th = fromVar VZ ::: (th . shift 1) +push : CanSubstSelf f => Subst f from to -> Loc -> Subst f (S from) (S to) +push th loc = fromVar VZ loc ::: (th . shift 1) -- [fixme] a better way to do this? public export pushN : CanSubstSelf f => (s : Nat) -> - Subst f from to -> Subst f (s + from) (s + to) -pushN 0 th = th -pushN (S s) th = + Subst f from to -> Loc -> Subst f (s + from) (s + to) +pushN 0 th _ = th +pushN (S s) th loc = rewrite plusSuccRightSucc s from in rewrite plusSuccRightSucc s to in - pushN s $ fromVar VZ ::: (th . shift 1) + pushN s (fromVar VZ loc ::: (th . shift 1)) loc public export drop1 : Subst f (S from) to -> Subst f from to diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr index 5682c73..23342d7 100644 --- a/lib/Quox/Syntax/Term/Base.idr +++ b/lib/Quox/Syntax/Term/Base.idr @@ -102,6 +102,16 @@ mutual ||| pair value Pair : (fst, snd : Term d n) -> (loc : Loc) -> Term d n + ||| inductive (w) type `(x : A) ⊲ B` + W : (shape : Term d n) -> + (body : ScopeTerm d n) -> (loc : Loc) -> Term d n + ||| subterms for `(x : A) ⊲ B` are: + ||| 1. `x : A` + ||| (the "constructor" and non-recursive fields) + ||| 2. `f : 1.(B x) → (x : A) ⊲ B` + ||| (the recursive fields, one for each element of B x) + Sup : (root, sub : Term d n) -> (loc : Loc) -> Term d n + ||| enumeration type Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n ||| enumeration value @@ -155,6 +165,13 @@ mutual (loc : Loc) -> Elim d n + ||| recursion + CaseW : (qty, qtyIH : Qty) -> (tree : Elim d n) -> + (ret : ScopeTerm d n) -> + (body : ScopeTermN 3 d n) -> + (loc : Loc) -> + Elim d n + ||| enum matching CaseEnum : (qty : Qty) -> (tag : Elim d n) -> (ret : ScopeTerm d n) -> @@ -344,6 +361,11 @@ public export %inline enum : List TagVal -> Loc -> Term d n enum ts loc = Enum (SortedSet.fromList ts) loc +public export %inline +caseEnum : Qty -> Elim d n -> ScopeTerm d n -> List (TagVal, Term d n) -> Loc -> + Elim d n +caseEnum q e ret arms loc = CaseEnum q e ret (SortedMap.fromList arms) loc + public export %inline typeCase : Elim d n -> Term d n -> List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n @@ -364,6 +386,7 @@ Located (Elim d n) where (B _ loc).loc = loc (App _ _ loc).loc = loc (CasePair _ _ _ _ loc).loc = loc + (CaseW _ _ _ _ _ loc).loc = loc (CaseEnum _ _ _ _ loc).loc = loc (CaseNat _ _ _ _ _ _ loc).loc = loc (CaseBox _ _ _ _ loc).loc = loc @@ -382,6 +405,8 @@ Located (Term d n) where (Lam _ loc).loc = loc (Sig _ _ loc).loc = loc (Pair _ _ loc).loc = loc + (W _ _ loc).loc = loc + (Sup _ _ loc).loc = loc (Enum _ loc).loc = loc (Tag _ loc).loc = loc (Eq _ _ _ loc).loc = loc @@ -412,6 +437,8 @@ Relocatable (Elim d n) where setLoc loc (App fun arg _) = App fun arg loc setLoc loc (CasePair qty pair ret body _) = CasePair qty pair ret body loc + setLoc loc (CaseW qty qtyIH tree ret body _) = + CaseW qty qtyIH tree ret body loc setLoc loc (CaseEnum qty tag ret arms _) = CaseEnum qty tag ret arms loc setLoc loc (CaseNat qty qtyIH nat ret zero succ _) = @@ -440,6 +467,8 @@ Relocatable (Term d n) where setLoc loc (Lam body _) = Lam body loc setLoc loc (Sig fst snd _) = Sig fst snd loc setLoc loc (Pair fst snd _) = Pair fst snd loc + setLoc loc (W shape body _) = W shape body loc + setLoc loc (Sup root sub _) = Sup root sub loc setLoc loc (Enum cases _) = Enum cases loc setLoc loc (Tag tag _) = Tag tag loc setLoc loc (Eq ty l r _) = Eq ty l r loc diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index 3b91f49..18644ce 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -346,6 +346,8 @@ prettyTyCasePat KPi [< a, b] = parens . hsep =<< sequence [prettyTBind a, arrowD, prettyTBind b] prettyTyCasePat KSig [< a, b] = parens . hsep =<< sequence [prettyTBind a, timesD, prettyTBind b] +prettyTyCasePat KW [< a, b] = + parens . hsep =<< sequence [prettyTBind a, triD, prettyTBind b] prettyTyCasePat KEnum [<] = hl Syntax $ text "{}" prettyTyCasePat KEq [< a0, a1, a, l, r] = hsep <$> sequence (eqD :: map prettyTBind [a0, a1, a, l, r]) @@ -420,6 +422,21 @@ prettyTerm dnames tnames p@(Pair fst snd _) = withPrec Outer $ prettyTerm dnames tnames $ assert_smaller p t pure $ separateTight !commaD lines +prettyTerm dnames tnames (W a b _) = do + parensIfM W =<< do + left <- prettySigBind1 b.name dnames tnames a + right <- withPrec InW $ + prettyTerm dnames (tnames :< b.name) (assert_smaller b b.term) + pure $ sep [hsep [left, !triD], right] + +prettyTerm dnames tnames (Sup root sub _) = do + parensIfM Sup =<< do + left <- withPrec InSup $ prettyTerm dnames tnames root + right <- withPrec InSup $ prettyTerm dnames tnames sub + pure $ + hsep [left, !diamondD, right] <|> + vsep [hsep [left, !diamondD], !(indentD right)] + prettyTerm dnames tnames (Enum cases _) = prettyEnum $ SortedSet.toList cases @@ -446,17 +463,22 @@ prettyTerm dnames tnames s@(DLam {}) = prettyTerm dnames tnames (Nat _) = natD prettyTerm dnames tnames (Zero _) = hl Syntax "0" prettyTerm dnames tnames (Succ p _) = do - succD <- succD - let succ : Doc opts -> Eff Pretty (Doc opts) - succ t = prettyAppD succD [t] - toNat : Term d n -> Eff Pretty (Either (Doc opts) Nat) - toNat s with (pushSubsts' s) - _ | Zero _ = pure $ Right 0 - _ | Succ d _ = bitraverse succ (pure . S) =<< - toNat (assert_smaller s d) - _ | s' = map Left . withPrec Arg $ - prettyTerm dnames tnames $ assert_smaller s s' - either succ (hl Syntax . text . show . S) =<< toNat p + s <- succD + either (succ s) prettyNat =<< tryToNat s p +where + succ : Doc opts -> Doc opts -> Eff Pretty (Doc opts) + succ s t = prettyAppD s [t] + + tryToNat : Doc opts -> Term d n -> Eff Pretty (Either (Doc opts) Nat) + tryToNat s t with (pushSubsts' t) + _ | Zero _ = pure $ Right 0 + _ | Succ d _ = bitraverse (succ s) (pure . S) =<< + tryToNat s (assert_smaller t d) + _ | t' = map Left . withPrec Arg $ + prettyTerm dnames tnames $ assert_smaller t t' + + prettyNat : Nat -> Eff Pretty (Doc opts) + prettyNat = hl Syntax . text . show . S prettyTerm dnames tnames (BOX qty ty _) = bracks . hcat =<< @@ -493,6 +515,16 @@ prettyElim dnames tnames (CasePair qty pair ret body _) = do prettyCase dnames tnames qty pair ret [MkCaseArm pat [<] [< x, y] body.term] +prettyElim dnames tnames (CaseW qty qtyIH tree ret body _) = do + let [< t, r, ih] = body.names + pat0 <- hsep <$> sequence [prettyTBind t, diamondD, prettyTBind r] + ihpat <- map hcat $ sequence [prettyQty qtyIH, dotD, prettyTBind ih] + pat <- if ih.name == Unused + then pure pat0 + else pure $ hsep [pat0 <+> !commaD, ihpat] + let arm = MkCaseArm pat [<] [< t, r, ih] body.term + prettyCase dnames tnames qty tree ret [arm] + prettyElim dnames tnames (CaseEnum qty tag ret arms _) = do arms <- for (SortedMap.toList arms) $ \(tag, body) => pure $ MkCaseArm !(prettyTag tag) [<] [<] body diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr index 6a9c899..eceffec 100644 --- a/lib/Quox/Syntax/Term/Subst.idr +++ b/lib/Quox/Syntax/Term/Subst.idr @@ -56,12 +56,12 @@ namespace DSubst.DScopeTermN (//) : {s : Nat} -> DScopeTermN s d1 n -> Lazy (DSubst d1 d2) -> DScopeTermN s d2 n - S ns (Y body) // th = S ns $ Y $ body // pushN s th + S ns (Y body) // th = S ns $ Y $ body // pushN s th body.loc S ns (N body) // th = S ns $ N $ body // th -export %inline FromVar (Elim d) where fromVarLoc = B -export %inline FromVar (Term d) where fromVarLoc = E .: fromVar +export %inline FromVar (Elim d) where fromVar = B +export %inline FromVar (Term d) where fromVar = E .: fromVar ||| does the minimal reasonable work: @@ -104,7 +104,7 @@ namespace ScopeTermN (//) : {s : Nat} -> ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> ScopeTermN s d n2 - S ns (Y body) // th = S ns $ Y $ body // pushN s th + S ns (Y body) // th = S ns $ Y $ body // pushN s th body.loc S ns (N body) // th = S ns $ N $ body // th namespace DScopeTermN @@ -147,24 +147,24 @@ weakE by t = t // shift by parameters {s : Nat} namespace ScopeTermBody - export %inline + public export %inline (.term) : ScopedBody s (Term d) n -> Term d (s + n) (Y b).term = b (N b).term = weakT s b namespace ScopeTermN - export %inline + public export %inline (.term) : ScopeTermN s d n -> Term d (s + n) t.term = t.body.term namespace DScopeTermBody - export %inline + public export %inline (.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n (Y b).term = b (N b).term = dweakT s b namespace DScopeTermN - export %inline + public export %inline (.term) : DScopeTermN s d n -> Term (s + d) n t.term = t.body.term @@ -189,12 +189,12 @@ dsub1 t p = dsubN t [< p] public export %inline -(.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n -body.zero = dsub1 body $ K Zero loc +(.zero) : DScopeTerm d n -> Term d n +body.zero = dsub1 body $ K Zero body.loc public export %inline -(.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n -body.one = dsub1 body $ K One loc +(.one) : DScopeTerm d n -> Term d n +body.one = dsub1 body $ K One body.loc public export @@ -261,6 +261,10 @@ mutual nclo $ Sig (a // th // ph) (b // th // ph) loc pushSubstsWith th ph (Pair s t loc) = nclo $ Pair (s // th // ph) (t // th // ph) loc + pushSubstsWith th ph (W a b loc) = + nclo $ W (a // th // ph) (b // th // ph) loc + pushSubstsWith th ph (Sup s t loc) = + nclo $ Sup (s // th // ph) (t // th // ph) loc pushSubstsWith th ph (Enum tags loc) = nclo $ Enum tags loc pushSubstsWith th ph (Tag tag loc) = @@ -299,6 +303,8 @@ mutual nclo $ App (f // th // ph) (s // th // ph) loc pushSubstsWith th ph (CasePair pi p r b loc) = nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc + pushSubstsWith th ph (CaseW pi pi' e r b loc) = + nclo $ CaseW pi pi' (e // th // ph) (r // th // ph) (b // th // ph) loc pushSubstsWith th ph (CaseEnum pi t r arms loc) = nclo $ CaseEnum pi (t // th // ph) (r // th // ph) (map (\b => b // th // ph) arms) loc diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr index 24c7018..8aaaa1a 100644 --- a/lib/Quox/Syntax/Term/Tighten.idr +++ b/lib/Quox/Syntax/Term/Tighten.idr @@ -52,6 +52,10 @@ mutual Sig <$> tightenT p fst <*> tightenS p snd <*> pure loc tightenT' p (Pair fst snd loc) = Pair <$> tightenT p fst <*> tightenT p snd <*> pure loc + tightenT' p (W shape body loc) = + W <$> tightenT p shape <*> tightenS p body <*> pure loc + tightenT' p (Sup root sub loc) = + Sup <$> tightenT p root <*> tightenT p sub <*> pure loc tightenT' p (Enum cases loc) = pure $ Enum cases loc tightenT' p (Tag tag loc) = @@ -87,6 +91,12 @@ mutual <*> tightenS p ret <*> tightenS p body <*> pure loc + tightenE' p (CaseW qty qtyIH tree ret body loc) = + CaseW qty qtyIH + <$> tightenE p tree + <*> tightenS p ret + <*> tightenS p body + <*> pure loc tightenE' p (CaseEnum qty tag ret arms loc) = CaseEnum qty <$> tightenE p tag <*> tightenS p ret @@ -167,6 +177,10 @@ mutual Sig <$> dtightenT p fst <*> dtightenS p snd <*> pure loc dtightenT' p (Pair fst snd loc) = Pair <$> dtightenT p fst <*> dtightenT p snd <*> pure loc + dtightenT' p (W shape body loc) = + W <$> dtightenT p shape <*> dtightenS p body <*> pure loc + dtightenT' p (Sup root sub loc) = + Sup <$> dtightenT p root <*> dtightenT p sub <*> pure loc dtightenT' p (Enum cases loc) = pure $ Enum cases loc dtightenT' p (Tag tag loc) = @@ -202,6 +216,12 @@ mutual <*> dtightenS p ret <*> dtightenS p body <*> pure loc + dtightenE' p (CaseW qty qtyIH tree ret body loc) = + CaseW qty qtyIH + <$> dtightenE p tree + <*> dtightenS p ret + <*> dtightenS p body + <*> pure loc dtightenE' p (CaseEnum qty tag ret arms loc) = CaseEnum qty <$> dtightenE p tag <*> dtightenS p ret diff --git a/lib/Quox/Syntax/Term/TyConKind.idr b/lib/Quox/Syntax/Term/TyConKind.idr index 6bacf77..58ed05e 100644 --- a/lib/Quox/Syntax/Term/TyConKind.idr +++ b/lib/Quox/Syntax/Term/TyConKind.idr @@ -9,7 +9,7 @@ import Generics.Derive public export -data TyConKind = KTYPE | KPi | KSig | KEnum | KEq | KNat | KBOX +data TyConKind = KTYPE | KPi | KSig | KW | KEnum | KEq | KNat | KBOX %name TyConKind k %runElab derive "TyConKind" [Eq.Eq, Ord.Ord, Show.Show, Generic, Meta, DecEq] @@ -28,6 +28,7 @@ arity : TyConKind -> Nat arity KTYPE = 0 arity KPi = 2 arity KSig = 2 +arity KW = 2 arity KEnum = 0 arity KEq = 5 arity KNat = 0 diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr index f9a648e..28cac7a 100644 --- a/lib/Quox/Syntax/Var.idr +++ b/lib/Quox/Syntax/Var.idr @@ -139,13 +139,9 @@ weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i) public export -interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n +interface FromVar f where %inline fromVar : Var n -> Loc -> f n -public export %inline -fromVar : FromVar f => Var n -> {default noLoc loc : Loc} -> f n -fromVar x = fromVarLoc x loc - -public export FromVar Var where fromVarLoc x _ = x +public export FromVar Var where fromVar x _ = x export tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) -> diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index d5cb0e6..cc463ed 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -57,27 +57,40 @@ typecaseTel : (k : TyConKind) -> BContext (arity k) -> Universe -> CtxExtension d n (arity k + n) typecaseTel k xs u = case k of KTYPE => [<] - -- A : ★ᵤ, B : 0.A → ★ᵤ - KPi => - let [< a, b] = xs in - [< (Zero, a, TYPE u a.loc), - (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] - KSig => - let [< a, b] = xs in - [< (Zero, a, TYPE u a.loc), - (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] + KPi => binaryTyCon xs + KSig => binaryTyCon xs + KW => binaryTyCon xs KEnum => [<] - -- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀ - KEq => - let [< a0, a1, a, l, r] = xs in + KEq => eqCon xs + KNat => [<] + KBOX => unaryTyCon xs +where + -- 0.A : ★ᵤ + unaryTyCon : BContext 1 -> CtxExtension d n (S n) + unaryTyCon [< a] = [< (Zero, a, TYPE u a.loc)] + + -- 0.A : ★ᵤ, 0.B : 0.A → ★ᵤ + binaryTyCon : BContext 2 -> CtxExtension d n (2 + n) + binaryTyCon [< a, b] = + [< (Zero, a, TYPE u a.loc), + (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] + + -- 0.A₀ : ★ᵤ, 0.A₁ : ★ᵤ, 0.A : (A₀ ≡ A₁ : ★ᵤ), 0.L : A₀, 0.R : A₁ + eqCon : BContext 5 -> CtxExtension d n (5 + n) + eqCon [< a0, a1, a, l, r] = [< (Zero, a0, TYPE u a0.loc), (Zero, a1, TYPE u a1.loc), (Zero, a, Eq0 (TYPE u a.loc) (BVT 1 a.loc) (BVT 0 a.loc) a.loc), (Zero, l, BVT 2 l.loc), (Zero, r, BVT 2 r.loc)] - KNat => [<] - -- A : ★ᵤ - KBOX => let [< a] = xs in [< (Zero, a, TYPE u a.loc)] + +||| if a ⋄ b : (x : A) ⊲ B, then b : `supSubTy a A B _` +||| i.e. ω.B[a∷A/x] → ((x : A) ⊲ B) +export +supSubTy : (root, rootTy : Term d n) -> + (body : ScopeTerm d n) -> Loc -> Term d n +supSubTy root rootTy body loc = + Arr Any (sub1 body (Ann root rootTy root.loc)) (W rootTy body loc) loc mutual @@ -188,6 +201,17 @@ mutual check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty + check' ctx sg t@(W {}) ty = toCheckType ctx sg t ty + + check' ctx sg (Sup root sub loc) ty = do + (shape, body) <- expectW !(askAt DEFS) ctx ty.loc ty + -- if Ψ | Γ ⊢ σ · a ⇐ A ⊳ Σ₁ + qroot <- checkC ctx sg root shape + -- if Ψ | Γ ⊢ σ · b ⇐ ω.B[a∷A/x] → ((x : A) ⊲ B) ⊳ Σ₂ + qsub <- checkC ctx sg sub (supSubTy root shape body sub.loc) + -- then Ψ | Γ ⊢ σ · (a ⋄ b) ⇐ ((x : A) ⊲ B) ⊳ Σ₁+ωΣ₂ + pure $ qroot + Any * qsub + check' ctx sg (Pair fst snd loc) ty = do (tfst, tsnd) <- expectSig !(askAt DEFS) ctx ty.loc ty -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁ @@ -281,6 +305,16 @@ mutual checkType' ctx t@(Pair {}) u = throw $ NotType t.loc ctx t + checkType' ctx (W shape body _) u = do + -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ + checkTypeC ctx shape u + -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ + checkTypeScope ctx shape body u + -- then Ψ | Γ ⊢₀ (x : A) ⊲ π.B ⇐ Type ℓ + + checkType' ctx t@(Sup {}) u = + throw $ NotType t.loc ctx t + checkType' ctx (Enum {}) u = pure () -- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ @@ -313,7 +347,7 @@ mutual infres <- inferC ctx szero e -- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀 case u of - Just u => lift $ subtype e.loc ctx infres.type (TYPE u noLoc) + Just u => lift $ subtype e.loc ctx infres.type (TYPE u e.loc) Nothing => ignore $ expectTYPE !(askAt DEFS) ctx e.loc infres.type -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀 @@ -388,6 +422,42 @@ mutual qout = pi * pairres.qout + bodyout } + infer' ctx sg (CaseW pi si tree ret body loc) = do + -- if 1 ≤ π + expectCompatQ loc One pi + -- if Ψ | Γ ⊢ σ · e ⇒ ((x : A) ⊲ B) ⊳ Σ₁ + InfRes {type = w, qout = qtree} <- inferC ctx sg tree + -- if Ψ | Γ, p : (x : A) ⊲ B ⊢₀ C ⇐ Type + checkTypeC (extendTy Zero ret.name w ctx) ret.term Nothing + (shape, tbody) <- expectW !(askAt DEFS) ctx tree.loc w + -- if Ψ | Γ, x : A, y : ω.B → (x : A) ⊲ B, + -- ih : π.(z : B) → C[y z/p] + -- ⊢ σ · u ⇐ C[((x ⋄ y) ∷ (x : A) ⊲ B)/p] + -- ⊳ Σ₂, π'.x, ς₁.y, ς₂.ih + -- with π' ≤ σπ, ς₂ ≤ σς, ς₁+ς₂ ≤ σπ + let [< x, y, ih] = body.names + -- ω.B → (x : A) ⊲ B + tsub = Arr Any tbody.term (weakT 1 w) y.loc + -- y z + ihret = App (BV 1 y.loc) (BVT 0 ih.loc) y.loc + -- π.(z : B) → C[y z/p] + tih = PiY pi !(mnb "z" ih.loc) + (tbody.term // (BV 1 x.loc ::: shift 2)) + (ret.term // (ihret ::: shift 3)) ih.loc + sp = sg.fst * pi; ss = sg.fst * si + ctx' = extendTyN [< (sp, x, shape), (sp, y, tsub), (ss, ih, tih)] ctx + qbody' <- checkC ctx' sg body.term $ substCaseWRet body.names w ret + let qbody :< qx :< qy :< qih = qbody' + expectCompatQ x.loc qx sp + expectCompatQ (ih.loc `or` loc) qih ss + expectCompatQ y.loc (qy + qih) sp -- [todo] better error message + -- then Ψ | Γ ⊢ σ · caseπ e return p ⇒ C of { x ⋄ y, ς.ih ⇒ u } + -- ⇒ C[e/p] ⊳ Σ₁+Σ₂ + pure $ InfRes { + type = sub1 ret tree, + qout = qtree + qbody + } + infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁ tres <- inferC ctx sg t diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr index 2d0a215..20aa27d 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -47,14 +47,22 @@ public export substCasePairRet : BContext 2 -> Term d n -> ScopeTerm d n -> Term d (2 + n) substCasePairRet [< x, y] dty retty = let tm = Pair (BVT 1 x.loc) (BVT 0 y.loc) $ x.loc `extendL` y.loc - arg = Ann tm (dty // fromNat 2) tm.loc + arg = Ann tm (dty // shift 2) tm.loc in retty.term // (arg ::: shift 2) +public export +substCaseWRet : BContext 3 -> Term d n -> ScopeTerm d n -> Term d (3 + n) +substCaseWRet [< x, y, ih] dty retty = + let tm = Sup (BVT 2 x.loc) (BVT 1 y.loc) $ x.loc `extendL` y.loc + arg = Ann tm (dty // shift 3) tm.loc + in + sub1 (weakS 3 retty) arg + public export substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n) substCaseSuccRet [< p, ih] retty = - let arg = Ann (Succ (BVT 1 p.loc) p.loc) (Nat noLoc) $ p.loc `extendL` ih.loc + let arg = Ann (Succ (BVT 1 p.loc) p.loc) (Nat p.loc) $ p.loc `extendL` ih.loc in retty.term // (arg ::: shift 2) @@ -95,6 +103,10 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)} expectSig : Term d n -> Eff fs (Term d n, ScopeTerm d n) expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd)) + export covering %inline + expectW : Term d n -> Eff fs (Term d n, ScopeTerm d n) + expectW = expect ExpectedW `(W {shape, body, _}) `((shape, body)) + export covering %inline expectEnum : Term d n -> Eff fs (SortedSet TagVal) expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases) @@ -143,6 +155,10 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)} expectSig : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n) expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd)) + export covering %inline + expectW : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n) + expectW = expect ExpectedW `(W {shape, body, _}) `((shape, body)) + export covering %inline expectEnum : Term 0 n -> Eff fs (SortedSet TagVal) expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases) diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr index c1db5fe..8447a9a 100644 --- a/lib/Quox/Typing/Context.idr +++ b/lib/Quox/Typing/Context.idr @@ -197,7 +197,7 @@ namespace EqContext toTyContext : (e : EqContext n) -> TyContext e.dimLen n toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) = MkTyContext { - dctx = fromGround dassign, + dctx = fromGround dnames dassign, tctx = map (// shift0 dimLen) tctx, dnames, tnames, qtys } diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr index 5975445..e618b5a 100644 --- a/lib/Quox/Typing/Error.idr +++ b/lib/Quox/Typing/Error.idr @@ -58,6 +58,7 @@ data Error = ExpectedTYPE Loc (NameContexts d n) (Term d n) | ExpectedPi Loc (NameContexts d n) (Term d n) | ExpectedSig Loc (NameContexts d n) (Term d n) +| ExpectedW Loc (NameContexts d n) (Term d n) | ExpectedEnum Loc (NameContexts d n) (Term d n) | ExpectedEq Loc (NameContexts d n) (Term d n) | ExpectedNat Loc (NameContexts d n) (Term d n) @@ -116,6 +117,7 @@ Located Error where (ExpectedTYPE loc _ _).loc = loc (ExpectedPi loc _ _).loc = loc (ExpectedSig loc _ _).loc = loc + (ExpectedW loc _ _).loc = loc (ExpectedEnum loc _ _).loc = loc (ExpectedEq loc _ _).loc = loc (ExpectedNat loc _ _).loc = loc @@ -256,12 +258,16 @@ prettyErrorNoLoc showContext = \case hangDSingle "expected a pair type, but got" !(prettyTerm ctx.dnames ctx.tnames s) + ExpectedW _ ctx s => + hangDSingle "expected an inductive (W) type, but got" + !(prettyTerm ctx.dnames ctx.tnames s) + ExpectedEnum _ ctx s => hangDSingle "expected an enumeration type, but got" !(prettyTerm ctx.dnames ctx.tnames s) ExpectedEq _ ctx s => - hangDSingle "expected an enumeration type, but got" + hangDSingle "expected an equality type, but got" !(prettyTerm ctx.dnames ctx.tnames s) ExpectedNat _ ctx s => diff --git a/syntax.ebnf b/syntax.ebnf index ff78604..7531d2a 100644 --- a/syntax.ebnf +++ b/syntax.ebnf @@ -24,7 +24,7 @@ dim arg = "@", dim. pat var = NAME | "_". -term = lambda | case | pi | sigma | ann. +term = lambda | case | pi | w | sigma | ann. lambda = ("λ" | "δ"), {pat var}+, "⇒", term. @@ -39,17 +39,22 @@ pattern = "zero" | "0" (* default qty for IH is 1 *) | TAG | "[", pat var, "]" - | "(", pat var, ",", pat var, ")". + | "(", pat var, ",", pat var, ")" + | pat var, "⋄", pat var, [",", [qty, "."], pat var]. (* default qty is 1 *) pi = [qty, "."], (binder | term arg), "→", term. binder = "(", {NAME}+, ":", term, ")". +w = binder, "⊲", ann. + sigma = (binder | ann), "×", (sigma | ann). ann = infix eq, ["∷", term]. -infix eq = app term, ["≡", term, ":", app term]. (* dependent is below *) +infix eq = sup term, ["≡", term, ":", sup term]. (* dependent is below *) + +sup term = app term, ["⋄", app term]. app term = coe | comp | split universe | dep eq | succ | normal app. split universe = "★", NAT. diff --git a/tests/Tests/DimEq.idr b/tests/Tests/DimEq.idr index 7f0a847..b96f7c4 100644 --- a/tests/Tests/DimEq.idr +++ b/tests/Tests/DimEq.idr @@ -97,7 +97,7 @@ tests = "dimension constraints" :- [ testPrettyD iijj ZeroIsOne "𝑖, 𝑗, 0 = 1", testPrettyD [<] new "" {label = "[empty output from empty context]"}, testPrettyD ii new "𝑖", - testPrettyD iijj (fromGround [< Zero, One]) + testPrettyD iijj (fromGround iijj [< Zero, One]) "𝑖, 𝑗, 𝑖 = 0, 𝑗 = 1", testPrettyD iijj (C [< Just (^K Zero), Nothing]) "𝑖, 𝑗, 𝑖 = 0", diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index 7756528..1965421 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -16,6 +16,8 @@ defGlobals = fromList ("a'", ^mkPostulate gany (^FT "A" 0)), ("b", ^mkPostulate gany (^FT "B" 0)), ("f", ^mkPostulate gany (^Arr One (^FT "A" 0) (^FT "A" 0))), + ("absurd", ^mkDef gany (^Arr One (^enum []) (^FT "A" 0)) + (^LamY "v" (E $ ^caseEnum One (^BV 0) (SN $ ^FT "A" 0) []))), ("id", ^mkDef gany (^Arr One (^FT "A" 0) (^FT "A" 0)) (^LamY "x" (^BVT 0))), ("eq-AB", ^mkPostulate gzero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))), ("two", ^mkDef gany (^Nat) (^Succ (^Succ (^Zero))))] @@ -517,6 +519,18 @@ tests = "equality & subtyping" :- [ todo "pair elim", + todo "w types", + + "sup" :- [ + testEq "a ⋄ absurd ≡ a ⋄ absurd : A ⊲ {}" $ + equalT empty + (^W (^FT "A" 0) (SN $ ^enum [])) + (^Sup (^FT "a" 0) (^FT "absurd" 0)) + (^Sup (^FT "a" 0) (^FT "absurd" 0)) + ], + + todo "w elim", + todo "enum types", todo "enum", todo "enum elim", diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index abd2bc7..97a11dc 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -168,6 +168,8 @@ tests = "parser" :- [ (App (V "B" {}) (V "x" {}) _) _) _), parseMatch term "(x : A) → B x" `(Pi (PQ One _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _), + parseFails term "(x : A) → (y : B x)", + parseFails term "(x : A) → 1.(B x)", parseMatch term "1.A → B" `(Pi (PQ One _) (Unused _) (V "A" {}) (V "B" {}) _), parseMatch term "A → B" @@ -249,6 +251,43 @@ tests = "parser" :- [ parseFails term "(x,,y)" ], + "w" :- [ + parseMatch term "(x : A) ⊲ B" + `(W (PV "x" _) (V "A" {}) (V "B" {}) _), + parseFails term "(x y : A) ⊲ B", + parseFails term "1.(x : A) ⊲ B", + parseMatch term "(x : A) ⊲ (y : B) ⊲ C" + `(W (PV "x" _) (V "A" {}) + (W (PV "y" _) (V "B" {}) (V "C" {}) _) _), + parseMatch term "A ⊲ B" + `(W _ (V "A" {}) (V "B" {}) _), + parseMatch term "A <| B" + `(W _ (V "A" {}) (V "B" {}) _), + parseFails term "A ⊲ (y : B)", + parseMatch term "(x : A) ⊲ B x × C" + `(W (PV "x" _) (V "A" {}) + (Sig _ (App (V "B" {}) (V "x" {}) _) (V "C" {}) _) _), + parseMatch term "A ⊲ B → C" + `(Pi _ _ (W _ (V "A" {}) (V "B" {}) _) (V "C" {}) _), + parseMatch term "A → B ⊲ C" + `(Pi _ _ (V "A" {}) (W _ (V "B" {}) (V "C" {}) _) _) + ], + + "sup" :- [ + parseMatch term "s ⋄ t" + `(Sup (V "s" {}) (V "t" {}) _), + parseMatch term "s ⋄ t ⋄ u" + `(Sup (V "s" {}) (Sup (V "t" {}) (V "u" {}) _) _), + parseMatch term "s <> t" + `(Sup (V "s" {}) (V "t" {}) _), + parseMatch term "a b ⋄ c d" + `(Sup (App (V "a" {}) (V "b" {}) _) (App (V "c" {}) (V "d" {}) _) _), + parseMatch term "a ⋄ b ≡ a' ⋄ b' : (A ⊲ B)" + `(Eq (_, W _ (V "A" {}) (V "B" {}) _) + (Sup (V "a" {}) (V "b" {}) _) + (Sup (V "a'" {}) (V "b'" {}) _) _) + ], + "equality type" :- [ parseMatch term "Eq (i ⇒ A) s t" `(Eq (PV "i" _, V "A" {}) (V "s" {}) (V "t" {}) _), @@ -396,8 +435,23 @@ tests = "parser" :- [ parseMatch term "caseω n return ℕ of { succ _, ih ⇒ ih; zero ⇒ 0; }" `(Case (PQ Any _) (V "n" {}) (Unused _, Nat _) (CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _), + parseMatch term "caseω n return ℕ of { succ _, _ ⇒ ih; zero ⇒ 0; }" + `(Case (PQ Any _) (V "n" {}) (Unused _, Nat _) + (CaseNat (Zero _) (Unused _, PQ Zero _, Unused _, V "ih" {}) _) _), parseFails term "caseω n return A of { zero ⇒ a }", - parseFails term "caseω n return ℕ of { succ ⇒ 5 }" + parseFails term "caseω n return ℕ of { succ ⇒ 5 }", + parseMatch term "case e return z ⇒ C of { a ⋄ b, ω.ih ⇒ u }" + `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {}) + (CaseW (PV "a" _) (PV "b" _) (PQ Any _, PV "ih" _) (V "u" {}) _) _), + parseMatch term "case e return z ⇒ C of { a ⋄ b, ih ⇒ u }" + `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {}) + (CaseW (PV "a" _) (PV "b" _) (PQ One _, PV "ih" _) (V "u" {}) _) _), + parseMatch term "case e return z ⇒ C of { a ⋄ b ⇒ u }" + `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {}) + (CaseW (PV "a" _) (PV "b" _) (PQ Zero _, Unused _) (V "u" {}) _) _), + parseMatch term "case e return z ⇒ C of { a ⋄ b, _ ⇒ u }" + `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {}) + (CaseW (PV "a" _) (PV "b" _) (PQ Zero _, Unused _) (V "u" {}) _) _) ], "definitions" :- [