WIP: 𝕎 #25
31 changed files with 1010 additions and 295 deletions
|
|
@ -1,34 +1,35 @@
|
||||||
load "misc.quox";
|
load "misc.quox"
|
||||||
|
|
||||||
namespace bool {
|
namespace bool {
|
||||||
|
|
||||||
def0 Bool : ★ = {true, false};
|
def0 Bool : ★ = {true, false}
|
||||||
|
|
||||||
def if-dep : 0.(P : Bool → ★) → (b : Bool) → ω.(P 'true) → ω.(P 'false) → P b =
|
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 =
|
def if : 0.(A : ★) → Bool → ω.A → ω.A → A =
|
||||||
λ A ⇒ if-dep (λ _ ⇒ A);
|
λ A ⇒ if-dep (λ _ ⇒ A)
|
||||||
|
|
||||||
def0 if-same : (A : ★) → (b : Bool) → (x : A) → if A b x x ≡ x : 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 =
|
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] =
|
def dup : Bool → [ω.Bool] =
|
||||||
λ b ⇒ if [ω.Bool] b ['true] ['false];
|
λ b ⇒ if [ω.Bool] b ['true] ['false]
|
||||||
|
|
||||||
def true-not-false : Not ('true ≡ 'false : Bool) =
|
def0 true-not-false : Not ('true ≡ 'false : Bool) =
|
||||||
λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true;
|
λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true
|
||||||
|
|
||||||
|
|
||||||
-- [todo] infix
|
-- [todo] infix
|
||||||
def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false;
|
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 or : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
def0 Bool = bool.Bool;
|
def0 Bool = bool.Bool
|
||||||
|
def if = bool.if
|
||||||
|
|
|
||||||
36
examples/natw.quox
Normal file
36
examples/natw.quox
Normal file
|
|
@ -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)
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
|
@ -19,6 +19,9 @@ parameters (k : Universe)
|
||||||
doDisplace (Lam body loc) = Lam (doDisplaceS body) loc
|
doDisplace (Lam body loc) = Lam (doDisplaceS body) loc
|
||||||
doDisplace (Sig fst snd loc) = Sig (doDisplace fst) (doDisplaceS snd) loc
|
doDisplace (Sig fst snd loc) = Sig (doDisplace fst) (doDisplaceS snd) loc
|
||||||
doDisplace (Pair fst snd loc) = Pair (doDisplace fst) (doDisplace 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 (Enum cases loc) = Enum cases loc
|
||||||
doDisplace (Tag tag loc) = Tag tag loc
|
doDisplace (Tag tag loc) = Tag tag loc
|
||||||
doDisplace (Eq ty l r 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 (App fun arg loc) = App (doDisplace fun) (doDisplace arg) loc
|
||||||
doDisplace (CasePair qty pair ret body loc) =
|
doDisplace (CasePair qty pair ret body loc) =
|
||||||
CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS 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) =
|
doDisplace (CaseEnum qty tag ret arms loc) =
|
||||||
CaseEnum qty (doDisplace tag) (doDisplaceS ret) (map doDisplace arms) loc
|
CaseEnum qty (doDisplace tag) (doDisplaceS ret) (map doDisplace arms) loc
|
||||||
doDisplace (CaseNat qty qtyIH nat ret zero succ loc) =
|
doDisplace (CaseNat qty qtyIH nat ret zero succ loc) =
|
||||||
|
|
|
||||||
|
|
@ -26,6 +26,26 @@ local_ : Has (State s) fs => s -> Eff fs a -> Eff fs a
|
||||||
local_ = localAt_ ()
|
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
|
export
|
||||||
hasDrop : (0 neq : Not (a = b)) ->
|
hasDrop : (0 neq : Not (a = b)) ->
|
||||||
(ha : Has a fs) => (hb : Has b fs) =>
|
(ha : Has a fs) => (hb : Has b fs) =>
|
||||||
|
|
|
||||||
|
|
@ -79,6 +79,8 @@ sameTyCon (Pi {}) (Pi {}) = True
|
||||||
sameTyCon (Pi {}) _ = False
|
sameTyCon (Pi {}) _ = False
|
||||||
sameTyCon (Sig {}) (Sig {}) = True
|
sameTyCon (Sig {}) (Sig {}) = True
|
||||||
sameTyCon (Sig {}) _ = False
|
sameTyCon (Sig {}) _ = False
|
||||||
|
sameTyCon (W {}) (W {}) = True
|
||||||
|
sameTyCon (W {}) _ = False
|
||||||
sameTyCon (Enum {}) (Enum {}) = True
|
sameTyCon (Enum {}) (Enum {}) = True
|
||||||
sameTyCon (Enum {}) _ = False
|
sameTyCon (Enum {}) _ = False
|
||||||
sameTyCon (Eq {}) (Eq {}) = True
|
sameTyCon (Eq {}) (Eq {}) = True
|
||||||
|
|
@ -111,6 +113,7 @@ isSubSing defs ctx ty0 = do
|
||||||
Sig {fst, snd, _} =>
|
Sig {fst, snd, _} =>
|
||||||
isSubSing defs ctx fst `andM`
|
isSubSing defs ctx fst `andM`
|
||||||
isSubSing defs (extendTy Zero snd.name fst ctx) snd.term
|
isSubSing defs (extendTy Zero snd.name fst ctx) snd.term
|
||||||
|
W {} => pure False
|
||||||
Enum {cases, _} =>
|
Enum {cases, _} =>
|
||||||
pure $ length (SortedSet.toList cases) <= 1
|
pure $ length (SortedSet.toList cases) <= 1
|
||||||
Eq {} => pure True
|
Eq {} => pure True
|
||||||
|
|
@ -120,6 +123,7 @@ isSubSing defs ctx ty0 = do
|
||||||
E _ => pure False
|
E _ => pure False
|
||||||
Lam {} => pure False
|
Lam {} => pure False
|
||||||
Pair {} => pure False
|
Pair {} => pure False
|
||||||
|
Sup {} => pure False
|
||||||
Tag {} => pure False
|
Tag {} => pure False
|
||||||
DLam {} => pure False
|
DLam {} => pure False
|
||||||
Zero {} => pure False
|
Zero {} => pure False
|
||||||
|
|
@ -209,9 +213,9 @@ parameters (defs : Definitions)
|
||||||
case (s, t) of
|
case (s, t) of
|
||||||
-- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x}
|
-- Γ ⊢ 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
|
(Pair sFst sSnd {}, Pair tFst tSnd {}) => do
|
||||||
compare0 ctx fst sFst tFst
|
compare0 ctx fst sFst tFst
|
||||||
compare0 ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
|
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
|
(E _, t) => wrongType t.loc ctx ty t
|
||||||
(s, _) => wrongType s.loc ctx ty s
|
(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 $
|
compare0' ctx ty@(Enum {}) s t = local_ Equal $
|
||||||
case (s, t) of
|
case (s, t) of
|
||||||
-- --------------------
|
-- --------------------
|
||||||
|
|
@ -322,12 +347,16 @@ parameters (defs : Definitions)
|
||||||
-- Γ ⊢ Type 𝓀 <: Type ℓ
|
-- Γ ⊢ Type 𝓀 <: Type ℓ
|
||||||
expectModeU a.loc !mode k l
|
expectModeU a.loc !mode k l
|
||||||
|
|
||||||
compareType' ctx a@(Pi {qty = sQty, arg = sArg, res = sRes, _})
|
compareType' ctx (Pi {qty = sQty, arg = sArg, res = sRes, loc})
|
||||||
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
|
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
|
||||||
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
|
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
|
||||||
-- ----------------------------------------
|
-- ----------------------------------------
|
||||||
-- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
|
-- Γ ⊢ π.(x : A₁) → B₁ <: π.(x : A₂) → B₂
|
||||||
expectEqualQ a.loc sQty tQty
|
--
|
||||||
|
-- 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
|
local flip $ compareType ctx sArg tArg -- contra
|
||||||
compareType (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term
|
compareType (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term
|
||||||
|
|
||||||
|
|
@ -339,12 +368,20 @@ parameters (defs : Definitions)
|
||||||
compareType ctx sFst tFst
|
compareType ctx sFst tFst
|
||||||
compareType (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term
|
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, _})
|
compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
|
||||||
(Eq {ty = tTy, l = tl, r = tr, _}) = do
|
(Eq {ty = tTy, l = tl, r = tr, _}) = do
|
||||||
-- Γ ⊢ A₁‹ε/i› <: A₂‹ε/i›
|
-- Γ ⊢ 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 Zero ctx) sTy.zero tTy.zero
|
||||||
compareType (extendDim sTy.name One ctx) sTy.one tTy.one
|
compareType (extendDim sTy.name One ctx) sTy.one tTy.one
|
||||||
let ty = case !mode of Super => sTy; _ => tTy
|
let ty = case !mode of Super => sTy; _ => tTy
|
||||||
|
|
@ -366,6 +403,9 @@ parameters (defs : Definitions)
|
||||||
pure ()
|
pure ()
|
||||||
|
|
||||||
compareType' ctx (BOX pi a loc) (BOX rh b {}) = do
|
compareType' ctx (BOX pi a loc) (BOX rh b {}) = do
|
||||||
|
-- Γ ⊢ A <: B
|
||||||
|
-- --------------------
|
||||||
|
-- Γ ⊢ [π.A] <: [π.B]
|
||||||
expectEqualQ loc pi rh
|
expectEqualQ loc pi rh
|
||||||
compareType ctx a b
|
compareType ctx a b
|
||||||
|
|
||||||
|
|
@ -439,6 +479,36 @@ parameters (defs : Definitions)
|
||||||
expectEqualQ e.loc epi fpi
|
expectEqualQ e.loc epi fpi
|
||||||
compare0' ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f
|
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}
|
-- Ψ | Γ ⊢ e = f ⇒ {𝐚s}
|
||||||
-- Ψ | Γ, x : {𝐚s} ⊢ Q = R
|
-- Ψ | Γ, x : {𝐚s} ⊢ Q = R
|
||||||
-- Ψ | Γ ⊢ sᵢ = tᵢ ⇐ Q[𝐚ᵢ∷{𝐚s}]
|
-- Ψ | Γ ⊢ sᵢ = tᵢ ⇐ Q[𝐚ᵢ∷{𝐚s}]
|
||||||
|
|
@ -451,10 +521,13 @@ parameters (defs : Definitions)
|
||||||
compare0 ctx e f
|
compare0 ctx e f
|
||||||
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
|
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
|
||||||
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
|
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
|
||||||
for_ !(expectEnum defs ctx eloc ety) $ \t => do
|
for_ (SortedMap.toList earms) $ \(t, l) => do
|
||||||
l <- lookupArm eloc t earms
|
|
||||||
r <- lookupArm floc t farms
|
r <- lookupArm floc t farms
|
||||||
compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r
|
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
|
expectEqualQ eloc epi fpi
|
||||||
where
|
where
|
||||||
lookupArm : Loc -> TagVal -> CaseEnumArms d n -> Equal_ (Term d n)
|
lookupArm : Loc -> TagVal -> CaseEnumArms d n -> Equal_ (Term d n)
|
||||||
|
|
@ -522,16 +595,18 @@ parameters (defs : Definitions)
|
||||||
|
|
||||||
-- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
|
-- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
|
||||||
-- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
|
-- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
|
||||||
-- Ψ | Γ ⊢ e <: f ⇒ _
|
-- Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖›
|
||||||
-- (non-neutral forms have the coercion already pushed in)
|
|
||||||
-- -----------------------------------------------------------
|
-- -----------------------------------------------------------
|
||||||
-- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ e
|
-- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
|
||||||
-- <: coe [𝑖 ⇒ B] @p₂ @q₂ f ⇒ B‹q₂/𝑖›
|
-- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖›
|
||||||
compare0' ctx (Coe ty1 p1 q1 (E val1) _)
|
compare0' ctx (Coe ty1 p1 q1 val1 _)
|
||||||
(Coe ty2 p2 q2 (E val2) _) ne nf = do
|
(Coe ty2 p2 q2 val2 _) ne nf = do
|
||||||
compareType ctx (dsub1 ty1 p1) (dsub1 ty2 p2)
|
let typ1 = dsub1 ty1 p1; tyq1 = dsub1 ty1 q1
|
||||||
compareType ctx (dsub1 ty1 q1) (dsub1 ty2 q2)
|
typ2 = dsub1 ty2 p2; tyq2 = dsub1 ty2 q2
|
||||||
compare0 ctx val1 val2
|
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
|
compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f
|
||||||
|
|
||||||
-- (no neutral compositions in a closed dctx)
|
-- (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
|
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
|
||||||
compare0 ctx (weakT 2 ret) b1.term b2.term
|
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 =
|
compareArm_ ctx KEnum ret u b1 b2 =
|
||||||
compare0 ctx ret b1.term b2.term
|
compare0 ctx ret b1.term b2.term
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -109,10 +109,16 @@ or (L l1) (L l2) = L $ l1 `or_` l2
|
||||||
public export
|
public export
|
||||||
interface Located a where (.loc) : a -> Loc
|
interface Located a where (.loc) : a -> Loc
|
||||||
|
|
||||||
|
export %inline Located Loc where l.loc = l
|
||||||
|
|
||||||
public export
|
public export
|
||||||
0 Located1 : (a -> Type) -> Type
|
0 Located1 : (a -> Type) -> Type
|
||||||
Located1 f = forall x. Located (f x)
|
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
|
public export
|
||||||
interface Located a => Relocatable a where setLoc : Loc -> a -> a
|
interface Located a => Relocatable a where setLoc : Loc -> a -> a
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -4,7 +4,7 @@ import Quox.Loc
|
||||||
import Quox.CharExtra
|
import Quox.CharExtra
|
||||||
import public Data.SnocList
|
import public Data.SnocList
|
||||||
import Data.List
|
import Data.List
|
||||||
import Control.Eff
|
import Quox.EffExtra
|
||||||
import Text.Lexer
|
import Text.Lexer
|
||||||
import Derive.Prelude
|
import Derive.Prelude
|
||||||
|
|
||||||
|
|
@ -178,23 +178,22 @@ export
|
||||||
runNameGen : Has NameGen fs => Eff fs a -> Eff (fs - NameGen) a
|
runNameGen : Has NameGen fs => Eff fs a -> Eff (fs - NameGen) a
|
||||||
runNameGen = map fst . runNameGenWith 0
|
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
|
||| generate a fresh name with the given base
|
||||||
export
|
export
|
||||||
mn : Has NameGen fs => PBaseName -> Eff fs BaseName
|
mn : Has NameGen fs => PBaseName -> Eff fs BaseName
|
||||||
mn base = do
|
mn base = MN base <$> gen
|
||||||
i <- getAt GEN
|
|
||||||
modifyAt GEN S
|
|
||||||
pure $ MN base i
|
|
||||||
|
|
||||||
||| generate a fresh binding name with the given base and
|
||| generate a fresh binding name with the given base and location `loc`
|
||||||
||| (optionally) location `loc`
|
|
||||||
export
|
export
|
||||||
mnb : Has NameGen fs =>
|
mnb : Has NameGen fs => PBaseName -> Loc -> Eff fs BindName
|
||||||
PBaseName -> {default noLoc loc : Loc} -> Eff fs BindName
|
mnb base loc = pure $ BN !(mn base) loc
|
||||||
mnb base = pure $ BN !(mn base) loc
|
|
||||||
|
|
||||||
export
|
export
|
||||||
fresh : Has NameGen fs => BindName -> Eff fs BindName
|
fresh : Has NameGen fs => BindName -> Eff fs BindName
|
||||||
fresh (BN (UN str) loc) = mnb str {loc}
|
fresh (BN (UN str) loc) = mnb str loc
|
||||||
fresh (BN (MN str k) loc) = mnb str {loc}
|
fresh (BN (MN str k) loc) = mnb str loc
|
||||||
fresh (BN Unused loc) = mnb "x" {loc}
|
fresh (BN Unused loc) = mnb "x" loc
|
||||||
|
|
|
||||||
|
|
@ -52,3 +52,18 @@ export %inline
|
||||||
nchoose : (b : Bool) -> Either (So b) (No b)
|
nchoose : (b : Bool) -> Either (So b) (No b)
|
||||||
nchoose True = Left Oh
|
nchoose True = Left Oh
|
||||||
nchoose False = Right Ah
|
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
|
||||||
|
|
|
||||||
|
|
@ -150,6 +150,23 @@ mutual
|
||||||
Pair s t loc =>
|
Pair s t loc =>
|
||||||
Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t <*> pure 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 =>
|
Case pi pair (r, ret) (CasePair (x, y) body _) loc =>
|
||||||
map E $ CasePair (fromPQty pi)
|
map E $ CasePair (fromPQty pi)
|
||||||
<$> fromPTermElim ds ns pair
|
<$> fromPTermElim ds ns pair
|
||||||
|
|
@ -157,13 +174,6 @@ mutual
|
||||||
<*> fromPTermTScope ds ns [< x, y] body
|
<*> fromPTermTScope ds ns [< x, y] body
|
||||||
<*> pure loc
|
<*> 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
|
Nat loc => pure $ Nat loc
|
||||||
Zero loc => pure $ Zero loc
|
Zero loc => pure $ Zero loc
|
||||||
Succ n loc => [|Succ (fromPTermWith ds ns n) (pure loc)|]
|
Succ n loc => [|Succ (fromPTermWith ds ns n) (pure loc)|]
|
||||||
|
|
@ -185,6 +195,13 @@ mutual
|
||||||
|
|
||||||
Tag str loc => pure $ Tag str loc
|
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 (i, ty) s t loc =>
|
||||||
Eq <$> fromPTermDScope ds ns [< i] ty
|
Eq <$> fromPTermDScope ds ns [< i] ty
|
||||||
<*> fromPTermWith ds ns s
|
<*> fromPTermWith ds ns s
|
||||||
|
|
|
||||||
|
|
@ -197,6 +197,8 @@ reserved =
|
||||||
Sym "×" `Or` Sym "**",
|
Sym "×" `Or` Sym "**",
|
||||||
Sym "≡" `Or` Sym "==",
|
Sym "≡" `Or` Sym "==",
|
||||||
Sym "∷" `Or` Sym "::",
|
Sym "∷" `Or` Sym "::",
|
||||||
|
Sym "⊲" `Or` Sym "<|",
|
||||||
|
Sym "⋄" `Or` Sym "<>",
|
||||||
Punc1 '.',
|
Punc1 '.',
|
||||||
Word1 "case",
|
Word1 "case",
|
||||||
Word1 "case0", Word1 "case1",
|
Word1 "case0", Word1 "case1",
|
||||||
|
|
|
||||||
|
|
@ -212,7 +212,8 @@ export
|
||||||
qtyPatVar : FileName -> Grammar True (PQty, PatVar)
|
qtyPatVar : FileName -> Grammar True (PQty, PatVar)
|
||||||
qtyPatVar fname =
|
qtyPatVar fname =
|
||||||
[|(,) (qty fname) (needRes "." *> patVar 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
|
export
|
||||||
|
|
@ -226,15 +227,17 @@ data PCasePat =
|
||||||
| PZero Loc
|
| PZero Loc
|
||||||
| PSucc PatVar PQty PatVar Loc
|
| PSucc PatVar PQty PatVar Loc
|
||||||
| PBox PatVar Loc
|
| PBox PatVar Loc
|
||||||
|
| PSup PatVar PatVar PQty PatVar Loc
|
||||||
%runElab derive "PCasePat" [Eq, Ord, Show]
|
%runElab derive "PCasePat" [Eq, Ord, Show]
|
||||||
|
|
||||||
export
|
export
|
||||||
Located PCasePat where
|
Located PCasePat where
|
||||||
(PPair _ _ loc).loc = loc
|
(PPair _ _ loc).loc = loc
|
||||||
(PTag _ loc).loc = loc
|
(PTag _ loc).loc = loc
|
||||||
(PZero loc).loc = loc
|
(PZero loc).loc = loc
|
||||||
(PSucc _ _ _ loc).loc = loc
|
(PSucc _ _ _ loc).loc = loc
|
||||||
(PBox _ loc).loc = loc
|
(PBox _ loc).loc = loc
|
||||||
|
(PSup _ _ _ _ loc).loc = loc
|
||||||
|
|
||||||
||| either `zero` or `0`
|
||| either `zero` or `0`
|
||||||
export
|
export
|
||||||
|
|
@ -251,6 +254,11 @@ casePat fname = withLoc fname $
|
||||||
ih <- resC "," *> qtyPatVar fname
|
ih <- resC "," *> qtyPatVar fname
|
||||||
<|> [|(,) (defLoc fname $ PQ Zero) (unused fname)|]
|
<|> [|(,) (defLoc fname $ PQ Zero) (unused fname)|]
|
||||||
pure $ PSucc p (fst ih) (snd ih)
|
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)|]
|
<|> delim "[" "]" [|PBox (patVar fname)|]
|
||||||
<|> fatalError "invalid pattern"
|
<|> fatalError "invalid pattern"
|
||||||
|
|
||||||
|
|
@ -405,12 +413,19 @@ appTerm fname =
|
||||||
<|> succTerm fname
|
<|> succTerm fname
|
||||||
<|> normalAppTerm 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
|
export
|
||||||
infixEqTerm : FileName -> Grammar True PTerm
|
infixEqTerm : FileName -> Grammar True PTerm
|
||||||
infixEqTerm fname = withLoc fname $ do
|
infixEqTerm fname = withLoc fname $ do
|
||||||
l <- appTerm fname; commit
|
l <- supTerm fname; commit
|
||||||
rest <- optional $ res "≡" *>
|
rest <- optional $ res "≡" *>
|
||||||
[|(,) (assert_total term fname) (needRes ":" *> appTerm fname)|]
|
[|(,) (assert_total term fname) (needRes ":" *> supTerm fname)|]
|
||||||
let u = Unused $ onlyStart l.loc
|
let u = Unused $ onlyStart l.loc
|
||||||
pure $ \loc => maybe l (\rest => Eq (u, snd rest) l (fst rest) loc) rest
|
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
|
body <- assert_total term fname; commit
|
||||||
pure $ \loc => foldr (\x, s => k x s loc) body xs
|
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)
|
-- [todo] fix the backtracking in e.g. (F x y z × B)
|
||||||
export
|
private
|
||||||
properBinders : FileName -> Grammar True (List1 PatVar, PTerm)
|
properBinders : FileName -> Grammar True (List1 PatVar, PTerm)
|
||||||
properBinders fname = assert_total $ do
|
properBinders fname = assert_total $ do
|
||||||
-- putting assert_total directly on `term`, in this one function,
|
-- putting assert_total directly on `term`, in this one function,
|
||||||
|
|
@ -441,61 +486,85 @@ properBinders fname = assert_total $ do
|
||||||
t <- term fname; needRes ")"
|
t <- term fname; needRes ")"
|
||||||
pure (xs, t)
|
pure (xs, t)
|
||||||
|
|
||||||
export
|
private
|
||||||
sigmaTerm : FileName -> Grammar True PTerm
|
bindPart : FileName -> Grammar True BindPart
|
||||||
sigmaTerm fname =
|
bindPart fname = do
|
||||||
(properBinders fname >>= continueDep)
|
qty <- optional $ qty fname <* resC "."
|
||||||
<|> (annTerm fname >>= continueNondep)
|
bnd <- properBinders fname
|
||||||
where
|
<|> do n <- unused fname
|
||||||
continueDep : (List1 PatVar, PTerm) -> Grammar True PTerm
|
t <- if isJust qty then termArg fname else annTerm fname
|
||||||
continueDep (names, fst) = withLoc fname $ do
|
pure (singleton n, t)
|
||||||
snd <- needRes "×" *> sigmaTerm fname
|
pure $ uncurry (BT qty) bnd
|
||||||
pure $ \loc => foldr (\x, snd => Sig x fst snd loc) snd names
|
|
||||||
|
|
||||||
cross : PTerm -> PTerm -> PTerm
|
private
|
||||||
cross l r = let loc = extend' l.loc r.loc.bounds in
|
bindSequence : FileName -> Grammar True BindSequence
|
||||||
Sig (Unused $ onlyStart l.loc) l r loc
|
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
|
private
|
||||||
continueNondep fst = do
|
fromBindSequence : BindSequence -> Grammar False PTerm
|
||||||
rest <- optional $ resC "×" *> sepBy1 (res "×") (annTerm fname)
|
fromBindSequence as = go [<] as where
|
||||||
pure $ foldr1 cross $ fst ::: maybe [] toList rest
|
-- 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
|
export
|
||||||
piTerm : FileName -> Grammar True PTerm
|
bindTerm : FileName -> Grammar True PTerm
|
||||||
piTerm fname = withLoc fname $ do
|
bindTerm fname = fromBindSequence !(bindSequence fname)
|
||||||
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
|
|
||||||
|
|
||||||
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
|
public export
|
||||||
PCaseArm : Type
|
PCaseArm : Type
|
||||||
|
|
@ -529,6 +598,9 @@ checkCaseArms loc ((PSucc p q ih _, rhs1) :: rest) = do
|
||||||
checkCaseArms loc ((PBox x _, rhs) :: rest) =
|
checkCaseArms loc ((PBox x _, rhs) :: rest) =
|
||||||
if null rest then pure $ CaseBox x rhs loc
|
if null rest then pure $ CaseBox x rhs loc
|
||||||
else fatalError "unexpected pattern after box"
|
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
|
export
|
||||||
caseBody : FileName -> Grammar True PCaseBody
|
caseBody : FileName -> Grammar True PCaseBody
|
||||||
|
|
@ -557,8 +629,7 @@ caseTerm fname = withLoc fname $ do
|
||||||
-- term : FileName -> Grammar True PTerm
|
-- term : FileName -> Grammar True PTerm
|
||||||
term fname = lamTerm fname
|
term fname = lamTerm fname
|
||||||
<|> caseTerm fname
|
<|> caseTerm fname
|
||||||
<|> piTerm fname
|
<|> bindTerm fname
|
||||||
<|> sigmaTerm fname
|
|
||||||
|
|
||||||
|
|
||||||
export
|
export
|
||||||
|
|
|
||||||
|
|
@ -74,6 +74,9 @@ namespace PTerm
|
||||||
| Pair PTerm PTerm Loc
|
| Pair PTerm PTerm Loc
|
||||||
| Case PQty PTerm (PatVar, PTerm) PCaseBody Loc
|
| Case PQty PTerm (PatVar, PTerm) PCaseBody Loc
|
||||||
|
|
||||||
|
| W PatVar PTerm PTerm Loc
|
||||||
|
| Sup PTerm PTerm Loc
|
||||||
|
|
||||||
| Enum (List TagVal) Loc
|
| Enum (List TagVal) Loc
|
||||||
| Tag TagVal Loc
|
| Tag TagVal Loc
|
||||||
|
|
||||||
|
|
@ -98,6 +101,7 @@ namespace PTerm
|
||||||
public export
|
public export
|
||||||
data PCaseBody =
|
data PCaseBody =
|
||||||
CasePair (PatVar, PatVar) PTerm Loc
|
CasePair (PatVar, PatVar) PTerm Loc
|
||||||
|
| CaseW PatVar PatVar (PQty, PatVar) PTerm Loc
|
||||||
| CaseEnum (List (PTagVal, PTerm)) Loc
|
| CaseEnum (List (PTagVal, PTerm)) Loc
|
||||||
| CaseNat PTerm (PatVar, PQty, PatVar, PTerm) Loc
|
| CaseNat PTerm (PatVar, PQty, PatVar, PTerm) Loc
|
||||||
| CaseBox PatVar PTerm Loc
|
| CaseBox PatVar PTerm Loc
|
||||||
|
|
@ -114,6 +118,8 @@ Located PTerm where
|
||||||
(Sig _ _ _ loc).loc = loc
|
(Sig _ _ _ loc).loc = loc
|
||||||
(Pair _ _ loc).loc = loc
|
(Pair _ _ loc).loc = loc
|
||||||
(Case _ _ _ _ loc).loc = loc
|
(Case _ _ _ _ loc).loc = loc
|
||||||
|
(W _ _ _ loc).loc = loc
|
||||||
|
(Sup _ _ loc).loc = loc
|
||||||
(Enum _ loc).loc = loc
|
(Enum _ loc).loc = loc
|
||||||
(Tag _ loc).loc = loc
|
(Tag _ loc).loc = loc
|
||||||
(Eq _ _ _ loc).loc = loc
|
(Eq _ _ _ loc).loc = loc
|
||||||
|
|
@ -131,10 +137,11 @@ Located PTerm where
|
||||||
|
|
||||||
export
|
export
|
||||||
Located PCaseBody where
|
Located PCaseBody where
|
||||||
(CasePair _ _ loc).loc = loc
|
(CasePair _ _ loc).loc = loc
|
||||||
(CaseEnum _ loc).loc = loc
|
(CaseW _ _ _ _ loc).loc = loc
|
||||||
(CaseNat _ _ loc).loc = loc
|
(CaseEnum _ loc).loc = loc
|
||||||
(CaseBox _ _ loc).loc = loc
|
(CaseNat _ _ loc).loc = loc
|
||||||
|
(CaseBox _ _ loc).loc = loc
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
|
|
|
||||||
|
|
@ -24,9 +24,13 @@ data PPrec
|
||||||
= Outer
|
= Outer
|
||||||
| Times -- "_ × _"
|
| Times -- "_ × _"
|
||||||
| InTimes -- arguments of ×
|
| InTimes -- arguments of ×
|
||||||
|
| W -- "_ ⊲ _"
|
||||||
|
| InW -- arguments of ⊲
|
||||||
| AnnL -- left of "∷"
|
| AnnL -- left of "∷"
|
||||||
| Eq -- "_ ≡ _ : _"
|
| Eq -- "_ ≡ _ : _"
|
||||||
| InEq -- arguments of ≡
|
| InEq -- arguments of ≡
|
||||||
|
| Sup -- "_ ⋄ _"
|
||||||
|
| InSup -- arguments of ⋄
|
||||||
-- ...
|
-- ...
|
||||||
| App -- term/dimension application
|
| App -- term/dimension application
|
||||||
| Arg -- argument to nonfix function
|
| Arg -- argument to nonfix function
|
||||||
|
|
@ -229,10 +233,10 @@ prettyDBind = hl DVar . prettyBind'
|
||||||
|
|
||||||
|
|
||||||
export %inline
|
export %inline
|
||||||
typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
|
typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD, triD, diamondD,
|
||||||
eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
|
eqD, colonD, commaD, semiD, caseD, typecaseD, returnD, ofD, dotD, zeroD, succD,
|
||||||
ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD :
|
coeD, compD, undD, cstD, pipeD :
|
||||||
{opts : _} -> Eff Pretty (Doc opts)
|
{opts : LayoutOpts} -> Eff Pretty (Doc opts)
|
||||||
typeD = hl Syntax . text =<< ifUnicode "★" "Type"
|
typeD = hl Syntax . text =<< ifUnicode "★" "Type"
|
||||||
arrowD = hl Delim . text =<< ifUnicode "→" "->"
|
arrowD = hl Delim . text =<< ifUnicode "→" "->"
|
||||||
darrowD = hl Delim . text =<< ifUnicode "⇒" "=>"
|
darrowD = hl Delim . text =<< ifUnicode "⇒" "=>"
|
||||||
|
|
@ -242,6 +246,8 @@ eqndD = hl Delim . text =<< ifUnicode "≡" "=="
|
||||||
dlamD = hl Syntax . text =<< ifUnicode "δ" "dfun"
|
dlamD = hl Syntax . text =<< ifUnicode "δ" "dfun"
|
||||||
annD = hl Delim . text =<< ifUnicode "∷" "::"
|
annD = hl Delim . text =<< ifUnicode "∷" "::"
|
||||||
natD = hl Syntax . text =<< ifUnicode "ℕ" "Nat"
|
natD = hl Syntax . text =<< ifUnicode "ℕ" "Nat"
|
||||||
|
triD = hl Syntax . text =<< ifUnicode "⊲" "<|"
|
||||||
|
diamondD = hl Syntax . text =<< ifUnicode "⋄" "<>"
|
||||||
eqD = hl Syntax $ text "Eq"
|
eqD = hl Syntax $ text "Eq"
|
||||||
colonD = hl Delim $ text ":"
|
colonD = hl Delim $ text ":"
|
||||||
commaD = hl Delim $ text ","
|
commaD = hl Delim $ text ","
|
||||||
|
|
|
||||||
|
|
@ -78,6 +78,12 @@ isPairHead (Ann (Pair {}) (Sig {}) _) = True
|
||||||
isPairHead (Coe {}) = True
|
isPairHead (Coe {}) = True
|
||||||
isPairHead _ = False
|
isPairHead _ = False
|
||||||
|
|
||||||
|
public export %inline
|
||||||
|
isWHead : Elim {} -> Bool
|
||||||
|
isWHead (Ann (Sup {}) (W {}) _) = True
|
||||||
|
isWHead (Coe {}) = True
|
||||||
|
isWHead _ = False
|
||||||
|
|
||||||
public export %inline
|
public export %inline
|
||||||
isTagHead : Elim {} -> Bool
|
isTagHead : Elim {} -> Bool
|
||||||
isTagHead (Ann (Tag {}) (Enum {}) _) = True
|
isTagHead (Ann (Tag {}) (Enum {}) _) = True
|
||||||
|
|
@ -115,6 +121,8 @@ isTyCon (Pi {}) = True
|
||||||
isTyCon (Lam {}) = False
|
isTyCon (Lam {}) = False
|
||||||
isTyCon (Sig {}) = True
|
isTyCon (Sig {}) = True
|
||||||
isTyCon (Pair {}) = False
|
isTyCon (Pair {}) = False
|
||||||
|
isTyCon (W {}) = True
|
||||||
|
isTyCon (Sup {}) = False
|
||||||
isTyCon (Enum {}) = True
|
isTyCon (Enum {}) = True
|
||||||
isTyCon (Tag {}) = False
|
isTyCon (Tag {}) = False
|
||||||
isTyCon (Eq {}) = True
|
isTyCon (Eq {}) = True
|
||||||
|
|
@ -128,6 +136,37 @@ isTyCon (E {}) = False
|
||||||
isTyCon (CloT {}) = False
|
isTyCon (CloT {}) = False
|
||||||
isTyCon (DCloT {}) = 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.
|
||| true if a term is syntactically a type, or a neutral.
|
||||||
public export %inline
|
public export %inline
|
||||||
isTyConE : Term {} -> Bool
|
isTyConE : Term {} -> Bool
|
||||||
|
|
@ -155,6 +194,8 @@ mutual
|
||||||
isRedexE defs fun || isLamHead fun
|
isRedexE defs fun || isLamHead fun
|
||||||
isRedexE defs (CasePair {pair, _}) =
|
isRedexE defs (CasePair {pair, _}) =
|
||||||
isRedexE defs pair || isPairHead pair
|
isRedexE defs pair || isPairHead pair
|
||||||
|
isRedexE defs (CaseW {tree, _}) =
|
||||||
|
isRedexE defs tree || isWHead tree
|
||||||
isRedexE defs (CaseEnum {tag, _}) =
|
isRedexE defs (CaseEnum {tag, _}) =
|
||||||
isRedexE defs tag || isTagHead tag
|
isRedexE defs tag || isTagHead tag
|
||||||
isRedexE defs (CaseNat {nat, _}) =
|
isRedexE defs (CaseNat {nat, _}) =
|
||||||
|
|
@ -165,8 +206,9 @@ mutual
|
||||||
isRedexE defs fun || isDLamHead fun || isK arg
|
isRedexE defs fun || isDLamHead fun || isK arg
|
||||||
isRedexE defs (Ann {tm, ty, _}) =
|
isRedexE defs (Ann {tm, ty, _}) =
|
||||||
isE tm || isRedexT defs tm || isRedexT defs ty
|
isE tm || isRedexT defs tm || isRedexT defs ty
|
||||||
isRedexE defs (Coe {val, _}) =
|
isRedexE defs (Coe {ty, val, _}) =
|
||||||
isRedexT defs val || not (isE val)
|
let ty = assert_smaller ty ty.term in
|
||||||
|
isRedexT defs ty || canPushCoe ty val
|
||||||
isRedexE defs (Comp {ty, r, _}) =
|
isRedexE defs (Comp {ty, r, _}) =
|
||||||
isRedexT defs ty || isK r
|
isRedexT defs ty || isK r
|
||||||
isRedexE defs (TypeCase {ty, ret, _}) =
|
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
|
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
|
export
|
||||||
weakDS : (by : Nat) -> DScopeTerm d n -> DScopeTerm d (by + n)
|
weakAtD : (CanDSubst f, Located2 f) => (by, at : Nat) ->
|
||||||
weakDS by (S names (Y body)) = S names $ Y $ weakT by body
|
f (at + d) n -> f (at + (by + d)) n
|
||||||
weakDS by (S names (N body)) = S names $ N $ weakT by body
|
weakAtD by at t = t `CanDSubst.(//)` pushN at (shift by) t.loc
|
||||||
|
|
||||||
private
|
parameters {s : Nat}
|
||||||
dweakS : (by : Nat) -> ScopeTerm d n -> ScopeTerm (by + d) n
|
export
|
||||||
dweakS by (S names (Y body)) = S names $ Y $ dweakT by body
|
weakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s d (by + n)
|
||||||
dweakS by (S names (N body)) = S names $ N $ dweakT by body
|
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
|
private
|
||||||
coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d -> Loc ->
|
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
|
| t => throw $ ExpectedPi loc ctx.names t
|
||||||
pure $ sub1 res $ Ann s arg loc
|
pure $ sub1 res $ Ann s arg loc
|
||||||
computeElimType (CasePair {pair, ret, _}) = pure $ sub1 ret pair
|
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 (CaseEnum {tag, ret, _}) = pure $ sub1 ret tag
|
||||||
computeElimType (CaseNat {nat, ret, _}) = pure $ sub1 ret nat
|
computeElimType (CaseNat {nat, ret, _}) = pure $ sub1 ret nat
|
||||||
computeElimType (CaseBox {box, ret, _}) = pure $ sub1 ret box
|
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
|
tycasePi (E e) {tnf} = do
|
||||||
ty <- computeElimType defs ctx e @{noOr2 tnf}
|
ty <- computeElimType defs ctx e @{noOr2 tnf}
|
||||||
let loc = e.loc
|
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
|
arg = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc
|
||||||
res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret]
|
res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret]
|
||||||
(BVT 0 loc) loc
|
(BVT 0 loc) loc
|
||||||
|
|
@ -287,7 +350,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
|
||||||
tycaseSig (E e) {tnf} = do
|
tycaseSig (E e) {tnf} = do
|
||||||
ty <- computeElimType defs ctx e @{noOr2 tnf}
|
ty <- computeElimType defs ctx e @{noOr2 tnf}
|
||||||
let loc = e.loc
|
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
|
fst = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc
|
||||||
snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd]
|
snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd]
|
||||||
(BVT 0 loc) loc
|
(BVT 0 loc) loc
|
||||||
|
|
@ -295,6 +358,24 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
|
||||||
pure (fst, snd)
|
pure (fst, snd)
|
||||||
tycaseSig t = throw $ ExpectedSig t.loc ctx.names t
|
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 [π. A], returns A;
|
||||||
||| for an elim returns a type-case that will reduce to that;
|
||| for an elim returns a type-case that will reduce to that;
|
||||||
||| for other intro forms error
|
||| 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)
|
Eff Whnf (Term (S d) n)
|
||||||
tycaseBOX (BOX {ty, _}) = pure ty
|
tycaseBOX (BOX {ty, _}) = pure ty
|
||||||
tycaseBOX (E e) {tnf} = do
|
tycaseBOX (E e) {tnf} = do
|
||||||
|
let loc = e.loc
|
||||||
ty <- computeElimType defs ctx e @{noOr2 tnf}
|
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
|
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);
|
||| 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
|
tycaseEq (E e) {tnf} = do
|
||||||
ty <- computeElimType defs ctx e @{noOr2 tnf}
|
ty <- computeElimType defs ctx e @{noOr2 tnf}
|
||||||
let loc = e.loc
|
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
|
a0 = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc
|
||||||
a1 = E $ typeCase1Y e ty KEq !names (BVT 3 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' = 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
|
l = E $ typeCase1Y e a0 KEq !names (BVT 1 loc) loc
|
||||||
r = E $ typeCase1Y e a1 KEq !names (BVT 0 loc) loc
|
r = E $ typeCase1Y e a1 KEq !names (BVT 0 loc) loc
|
||||||
pure (a0, a1, a, l, r)
|
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 ->
|
(val, s : Term d n) -> Loc ->
|
||||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||||
piCoe sty@(S [< i] ty) p q val s loc = do
|
piCoe sty@(S [< i] ty) p q val s loc = do
|
||||||
-- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
|
-- 𝒮‹𝑘› ≔ π.(x : A‹𝑘/𝑖›) → B‹𝑘/𝑖›
|
||||||
-- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
|
-- 𝓈‹𝑘› ≔ coe [𝑖 ⇒ A] @q @𝑘 s
|
||||||
-- where 𝒔‹j› ≔ coe [i ⇒ A] @q @j 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
|
-- type-case is used to expose A,B if the type is neutral
|
||||||
let ctx1 = extendDim i ctx
|
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 ->
|
(ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc ->
|
||||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||||
sigCoe qty sty@(S [< i] ty) p q val ret body loc = do
|
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
|
-- caseπ s ∷ ((x : A) × B)‹p/i› return z ⇒ C
|
||||||
-- of { (a, b) ⇒
|
-- 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] }
|
-- (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
|
-- 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
|
Element ty tynf <- whnf defs ctx1 ty.term
|
||||||
(tfst, tsnd) <- tycaseSig defs ctx1 ty
|
(tfst, tsnd) <- tycaseSig defs ctx1 ty
|
||||||
let [< x, y] = body.names
|
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 //
|
tsnd' = tsnd.term //
|
||||||
(CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2))
|
(CoeT !(fresh i) (weakT 2 $ tfst // (B VZ i.loc ::: shift 2))
|
||||||
(weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.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 noLoc) y.loc
|
b' = CoeT i tsnd' p q (BVT 0 y.loc) y.loc
|
||||||
whnf defs ctx $ CasePair qty (Ann val (ty // one p) val.loc) ret
|
whnf defs ctx $ CasePair qty (Ann val (dsub1 sty p) val.loc) ret
|
||||||
(ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
|
(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`
|
||| reduce a dimension application `DApp (Coe ty p q val) r loc`
|
||||||
private covering
|
private covering
|
||||||
eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
|
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
|
Element ty tynf <- whnf defs ctx1 ty.term
|
||||||
(a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
|
(a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
|
||||||
let a' = dsub1 a (weakD 1 r)
|
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
|
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`
|
||| 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
|
let ctx1 = extendDim i ctx
|
||||||
Element ty tynf <- whnf defs ctx1 ty.term
|
Element ty tynf <- whnf defs ctx1 ty.term
|
||||||
ta <- tycaseBOX defs ctx1 ty
|
ta <- tycaseBOX defs ctx1 ty
|
||||||
let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc
|
let a' = CoeT i (weakT 1 ta) p q (BVT 0 body.name.loc) body.name.loc
|
||||||
whnf defs ctx $ CaseBox qty (Ann val (ty // one p) val.loc) ret
|
whnf defs ctx $ CaseBox qty (Ann val (dsub1 sty p) val.loc) ret
|
||||||
(ST body.names $ body.term // (a' ::: shift 1)) loc
|
(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; ⋯ }) ⇝
|
-- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
|
||||||
-- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
|
-- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
|
||||||
Pi {arg, res, loc = piLoc, _} =>
|
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)
|
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
|
in
|
||||||
whnf defs ctx $
|
whnf defs ctx $
|
||||||
Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc
|
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; ⋯ }) ⇝
|
-- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
|
||||||
-- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
|
-- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
|
||||||
Sig {fst, snd, loc = sigLoc, _} =>
|
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)
|
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
|
in
|
||||||
whnf defs ctx $
|
whnf defs ctx $
|
||||||
Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc
|
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
|
let a0 = a.zero; a1 = a.one in
|
||||||
whnf defs ctx $ Ann
|
whnf defs ctx $ Ann
|
||||||
(subN (tycaseRhsDef def KEq arms)
|
(subN (tycaseRhsDef def KEq arms)
|
||||||
[< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) 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 noLoc) a0 a1 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])
|
Ann l a0 l.loc, Ann r a1 r.loc])
|
||||||
ret 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
|
-- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
|
||||||
BOX {ty = a, loc = boxLoc, _} =>
|
BOX {ty = a, loc = boxLoc, _} =>
|
||||||
whnf defs ctx $ Ann
|
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
|
ret loc
|
||||||
|
|
||||||
|
|
||||||
||| pushes a coercion inside a whnf-ed term
|
||| pushes a coercion inside a whnf-ed term
|
||||||
private covering
|
private covering
|
||||||
pushCoe : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
|
pushCoe : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
|
||||||
BindName ->
|
BindName -> (ty : Term (S d) n) ->
|
||||||
(ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) =>
|
|
||||||
Dim d -> Dim d ->
|
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)
|
Eff Whnf (NonRedex Elim d n defs)
|
||||||
pushCoe defs ctx i ty p q s loc =
|
pushCoe defs ctx i ty p q s loc =
|
||||||
if p == q then whnf defs ctx $ Ann s (ty // one q) loc else
|
if p == q then whnf defs ctx $ Ann s (ty // one q) loc else
|
||||||
case s of
|
case ty of
|
||||||
-- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ)
|
-- (coe ★ᵢ @p @q s) ⇝ (s ∷ ★ᵢ)
|
||||||
TYPE {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
|
--
|
||||||
Pi {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
|
-- no η (what would that even mean), but ground type
|
||||||
Sig {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
|
TYPE {l, loc = tyLoc} =>
|
||||||
Enum {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
|
whnf defs ctx $ Ann s (TYPE l tyLoc) 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
|
|
||||||
|
|
||||||
-- just η expand it. then whnf for App will handle it later
|
-- just η expand it. then whnf for App will handle it later
|
||||||
-- this is how @xtt does it
|
-- this is how @xtt does it
|
||||||
--
|
--
|
||||||
-- (coe [i ⇒ A] @p @q (λ x ⇒ s)) ⇝
|
-- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) ⇝
|
||||||
-- (λ y ⇒ (coe [i ⇒ A] @p @q (λ x ⇒ s)) y) ∷ A‹q/i› ⇝ ⋯
|
-- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y)
|
||||||
lam@(Lam {body, _}) => do
|
-- ∷ (π.(x : A) → B)‹q/𝑖›
|
||||||
let lam' = CoeT i ty p q lam loc
|
Pi {} => do
|
||||||
term' = LamY !(fresh body.name)
|
y <- mnb "y" loc
|
||||||
(E $ App (weakE 1 lam') (BVT 0 noLoc) loc) loc
|
let s' = Coe (SY [< i] ty) p q s loc
|
||||||
type' = ty // one q
|
body = SY [< y] $ E $ App (weakE 1 s') (BVT 0 y.loc) s.loc
|
||||||
whnf defs ctx $ Ann term' type' 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 ⇒ (x : A) × B] @p @q (s, t)) ⇝
|
||||||
-- (coe [i ⇒ A] @p @q s,
|
-- (coe [i ⇒ A] @p @q s,
|
||||||
-- coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i s)/x]] @p @q t)
|
-- coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i s)/x]] @p @q t)
|
||||||
-- ∷ (x : A‹q/i›) × B‹q/i›
|
-- ∷ (x : A‹q/i›) × B‹q/i›
|
||||||
--
|
--
|
||||||
-- can't use η here because... it doesn't exist
|
-- no η so only reduce on an actual pair 🍐
|
||||||
Pair {fst, snd, loc = pairLoc} => do
|
Sig {fst = tfst, snd = tsnd, loc = tyLoc} => do
|
||||||
let Sig {fst = tfst, snd = tsnd, loc = sigLoc} = ty
|
let Pair fst snd sLoc = s
|
||||||
| _ => throw $ ExpectedSig ty.loc (extendDim i ctx.names) ty
|
fst' = E $ CoeT i tfst p q fst fst.loc
|
||||||
let fst' = E $ CoeT i tfst p q fst fst.loc
|
tfst' = tfst // (B VZ i.loc ::: shift 2)
|
||||||
tfst' = tfst // (B VZ noLoc ::: shift 2)
|
|
||||||
tsnd' = sub1 tsnd $
|
tsnd' = sub1 tsnd $
|
||||||
CoeT !(fresh i) tfst' (weakD 1 p) (B VZ noLoc)
|
CoeT !(fresh i) tfst' (weakD 1 p) (B VZ snd.loc)
|
||||||
(dweakT 1 fst) fst.loc
|
(dweakT 1 fst) snd.loc
|
||||||
snd' = E $ CoeT i tsnd' p q snd snd.loc
|
snd' = E $ CoeT i tsnd' p q snd snd.loc
|
||||||
pure $
|
pure $ nred $
|
||||||
Element (Ann (Pair fst' snd' pairLoc)
|
Ann (Pair fst' snd' sLoc)
|
||||||
(Sig (tfst // one q) (tsnd // one q) sigLoc) loc) Ah
|
(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
|
-- η expand, like for Lam
|
||||||
--
|
--
|
||||||
-- (coe [i ⇒ A] @p @q (δ j ⇒ s)) ⇝
|
-- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) ⇝
|
||||||
-- (δ k ⇒ (coe [i ⇒ A] @p @q (δ j ⇒ s)) @k) ∷ A‹q/i› ⇝ ⋯
|
-- (δ k ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @k)
|
||||||
dlam@(DLam {body, _}) => do
|
-- ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›
|
||||||
let dlam' = CoeT i ty p q dlam loc
|
Eq {} => do
|
||||||
term' = DLamY !(mnb "j")
|
k <- mnb "k" loc
|
||||||
(E $ DApp (dweakE 1 dlam') (B VZ noLoc) loc) loc
|
let s' = Coe (SY [< i] ty) p q s loc
|
||||||
type' = ty // one q
|
term = DLam (SY [< k] $ E $ DApp (dweakE 1 s') (BV 0 k.loc) loc) loc
|
||||||
whnf defs ctx $ Ann term' type' loc
|
ret = ty // one q
|
||||||
|
whnf defs ctx $ Ann term ret loc
|
||||||
|
|
||||||
-- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯})
|
-- (coe ℕ @p @q s) ⇝ (s ∷ ℕ)
|
||||||
Tag {tag, loc = tagLoc} => do
|
--
|
||||||
let Enum {cases, loc = enumLoc} = ty
|
-- no η, but ground type
|
||||||
| _ => throw $ ExpectedEnum ty.loc (extendDim i ctx.names) ty
|
Nat {loc = tyLoc} =>
|
||||||
pure $ Element (Ann (Tag tag tagLoc) (Enum cases enumLoc) loc) Ah
|
whnf defs ctx $ Ann s (Nat tyLoc) loc
|
||||||
|
|
||||||
-- (coe [_ ⇒ ℕ] @_ @_ n) ⇝ (n ∷ ℕ)
|
-- (coe (𝑖 ⇒ [π. A]) @p @q s) ⇝
|
||||||
Zero {loc = zeroLoc} => do
|
-- [coe (𝑖 ⇒ A) @p @q (case1 s ∷ [π. A‹p/𝑖›] return A‹p/𝑖› of {[x] ⇒ x})]
|
||||||
pure $ Element (Ann (Zero zeroLoc) (Nat ty.loc) loc) Ah
|
-- ∷ [π. A‹q/𝑖›]
|
||||||
Succ {p = pred, loc = succLoc} => do
|
--
|
||||||
pure $ Element (Ann (Succ pred succLoc) (Nat ty.loc) loc) Ah
|
-- [todo] box should probably have an η rule
|
||||||
|
BOX {qty, ty = innerTy, loc = tyLoc} => do
|
||||||
-- (coe [i ⇒ [π.A]] @p @q [s]) ⇝
|
let s' = Ann s (BOX qty (innerTy // one p) tyLoc) s.loc
|
||||||
-- [coe [i ⇒ A] @p @q s] ∷ [π. A‹q/i›]
|
inner' = CaseBox One s' (SN $ innerTy // one p)
|
||||||
Box {val, loc = boxLoc} => do
|
(SY [< !(mnb "x" s.loc)] $ BVT 0 s.loc) s.loc
|
||||||
let BOX {qty, ty = a, loc = tyLoc} = ty
|
inner = Box (E $ CoeT i innerTy p q (E inner') loc) loc
|
||||||
| _ => throw $ ExpectedBOX ty.loc (extendDim i ctx.names) ty
|
ret = BOX qty (innerTy // one q) tyLoc
|
||||||
pure $ Element
|
whnf defs ctx $ Ann inner ret loc
|
||||||
(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
|
|
||||||
|
|
||||||
|
|
||||||
export covering
|
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
|
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
|
Right nlh => pure $ Element (App f s appLoc) $ fnf `orNo` nlh
|
||||||
|
|
||||||
-- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
|
-- s' ≔ s ∷ A
|
||||||
-- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
|
-- 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
|
whnf defs ctx (CasePair pi pair ret body caseLoc) = do
|
||||||
Element pair pairnf <- whnf defs ctx pair
|
Element pair pairnf <- whnf defs ctx pair
|
||||||
case nchoose $ isPairHead pair of
|
case nchoose $ isPairHead pair of
|
||||||
|
|
@ -601,6 +758,43 @@ CanWhnf Elim Reduce.isRedexE where
|
||||||
Right np =>
|
Right np =>
|
||||||
pure $ Element (CasePair pi pair ret body caseLoc) $ pairnf `orNo` 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 } ⇝
|
-- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
|
||||||
-- u ∷ C['a∷{a,…}/p]
|
-- u ∷ C['a∷{a,…}/p]
|
||||||
whnf defs ctx (CaseEnum pi tag ret arms caseLoc) = do
|
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
|
whnf defs ctx (Coe (S [< i] (Y ty)) p q val coeLoc) = do
|
||||||
Element ty tynf <- whnf defs (extendDim i ctx) ty
|
Element ty tynf <- whnf defs (extendDim i ctx) ty
|
||||||
Element val valnf <- whnf defs ctx val
|
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) =
|
whnf defs ctx (Comp ty p q val r zero one compLoc) =
|
||||||
-- comp [A] @p @p s { ⋯ } ⇝ s ∷ A
|
-- comp [A] @p @p s { ⋯ } ⇝ s ∷ A
|
||||||
|
|
@ -730,6 +927,8 @@ CanWhnf Term Reduce.isRedexT where
|
||||||
whnf _ _ t@(Lam {}) = pure $ nred t
|
whnf _ _ t@(Lam {}) = pure $ nred t
|
||||||
whnf _ _ t@(Sig {}) = pure $ nred t
|
whnf _ _ t@(Sig {}) = pure $ nred t
|
||||||
whnf _ _ t@(Pair {}) = 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@(Enum {}) = pure $ nred t
|
||||||
whnf _ _ t@(Tag {}) = pure $ nred t
|
whnf _ _ t@(Tag {}) = pure $ nred t
|
||||||
whnf _ _ t@(Eq {}) = pure $ nred t
|
whnf _ _ t@(Eq {}) = pure $ nred t
|
||||||
|
|
|
||||||
|
|
@ -83,7 +83,7 @@ DSubst : Nat -> Nat -> Type
|
||||||
DSubst = Subst Dim
|
DSubst = Subst Dim
|
||||||
|
|
||||||
|
|
||||||
public export FromVar Dim where fromVarLoc = B
|
public export FromVar Dim where fromVar = B
|
||||||
|
|
||||||
|
|
||||||
export
|
export
|
||||||
|
|
|
||||||
|
|
@ -70,13 +70,13 @@ toMaybe (Just x) = Just x
|
||||||
|
|
||||||
|
|
||||||
export
|
export
|
||||||
fromGround' : Context' DimConst d -> DimEq' d
|
fromGround' : BContext d -> Context' DimConst d -> DimEq' d
|
||||||
fromGround' [<] = [<]
|
fromGround' [<] [<] = [<]
|
||||||
fromGround' (ctx :< e) = fromGround' ctx :< Just (K e noLoc)
|
fromGround' (xs :< x) (ctx :< e) = fromGround' xs ctx :< Just (K e x.loc)
|
||||||
|
|
||||||
export
|
export
|
||||||
fromGround : Context' DimConst d -> DimEq d
|
fromGround : BContext d -> Context' DimConst d -> DimEq d
|
||||||
fromGround = C . fromGround'
|
fromGround = C .: fromGround'
|
||||||
|
|
||||||
|
|
||||||
public export %inline
|
public export %inline
|
||||||
|
|
@ -243,7 +243,7 @@ prettyCsts : {opts : _} -> BContext d -> DimEq' d ->
|
||||||
prettyCsts [<] [<] = pure [<]
|
prettyCsts [<] [<] = pure [<]
|
||||||
prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs
|
prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs
|
||||||
prettyCsts dnames (eqs :< Just q) =
|
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
|
export
|
||||||
prettyDimEq' : {opts : _} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)
|
prettyDimEq' : {opts : _} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)
|
||||||
|
|
|
||||||
|
|
@ -49,7 +49,7 @@ interface FromVar term => CanSubstSelf term where
|
||||||
|
|
||||||
public export
|
public export
|
||||||
getLoc : FromVar term => Subst term from to -> Var from -> Loc -> term to
|
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) VZ _ = t
|
||||||
getLoc (t ::: th) (VS i) loc = getLoc th i loc
|
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
|
public export %inline
|
||||||
push : CanSubstSelf f => Subst f from to -> Subst f (S from) (S to)
|
push : CanSubstSelf f => Subst f from to -> Loc -> Subst f (S from) (S to)
|
||||||
push th = fromVar VZ ::: (th . shift 1)
|
push th loc = fromVar VZ loc ::: (th . shift 1)
|
||||||
|
|
||||||
-- [fixme] a better way to do this?
|
-- [fixme] a better way to do this?
|
||||||
public export
|
public export
|
||||||
pushN : CanSubstSelf f => (s : Nat) ->
|
pushN : CanSubstSelf f => (s : Nat) ->
|
||||||
Subst f from to -> Subst f (s + from) (s + to)
|
Subst f from to -> Loc -> Subst f (s + from) (s + to)
|
||||||
pushN 0 th = th
|
pushN 0 th _ = th
|
||||||
pushN (S s) th =
|
pushN (S s) th loc =
|
||||||
rewrite plusSuccRightSucc s from in
|
rewrite plusSuccRightSucc s from in
|
||||||
rewrite plusSuccRightSucc s to in
|
rewrite plusSuccRightSucc s to in
|
||||||
pushN s $ fromVar VZ ::: (th . shift 1)
|
pushN s (fromVar VZ loc ::: (th . shift 1)) loc
|
||||||
|
|
||||||
public export
|
public export
|
||||||
drop1 : Subst f (S from) to -> Subst f from to
|
drop1 : Subst f (S from) to -> Subst f from to
|
||||||
|
|
|
||||||
|
|
@ -102,6 +102,16 @@ mutual
|
||||||
||| pair value
|
||| pair value
|
||||||
Pair : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
|
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
|
||| enumeration type
|
||||||
Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n
|
Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n
|
||||||
||| enumeration value
|
||| enumeration value
|
||||||
|
|
@ -155,6 +165,13 @@ mutual
|
||||||
(loc : Loc) ->
|
(loc : Loc) ->
|
||||||
Elim d n
|
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
|
||| enum matching
|
||||||
CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
|
CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
|
||||||
(ret : ScopeTerm d n) ->
|
(ret : ScopeTerm d n) ->
|
||||||
|
|
@ -344,6 +361,11 @@ public export %inline
|
||||||
enum : List TagVal -> Loc -> Term d n
|
enum : List TagVal -> Loc -> Term d n
|
||||||
enum ts loc = Enum (SortedSet.fromList ts) loc
|
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
|
public export %inline
|
||||||
typeCase : Elim d n -> Term d n ->
|
typeCase : Elim d n -> Term d n ->
|
||||||
List (TypeCaseArm d n) -> Term d n -> Loc -> Elim 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
|
(B _ loc).loc = loc
|
||||||
(App _ _ loc).loc = loc
|
(App _ _ loc).loc = loc
|
||||||
(CasePair _ _ _ _ loc).loc = loc
|
(CasePair _ _ _ _ loc).loc = loc
|
||||||
|
(CaseW _ _ _ _ _ loc).loc = loc
|
||||||
(CaseEnum _ _ _ _ loc).loc = loc
|
(CaseEnum _ _ _ _ loc).loc = loc
|
||||||
(CaseNat _ _ _ _ _ _ loc).loc = loc
|
(CaseNat _ _ _ _ _ _ loc).loc = loc
|
||||||
(CaseBox _ _ _ _ loc).loc = loc
|
(CaseBox _ _ _ _ loc).loc = loc
|
||||||
|
|
@ -382,6 +405,8 @@ Located (Term d n) where
|
||||||
(Lam _ loc).loc = loc
|
(Lam _ loc).loc = loc
|
||||||
(Sig _ _ loc).loc = loc
|
(Sig _ _ loc).loc = loc
|
||||||
(Pair _ _ loc).loc = loc
|
(Pair _ _ loc).loc = loc
|
||||||
|
(W _ _ loc).loc = loc
|
||||||
|
(Sup _ _ loc).loc = loc
|
||||||
(Enum _ loc).loc = loc
|
(Enum _ loc).loc = loc
|
||||||
(Tag _ loc).loc = loc
|
(Tag _ loc).loc = loc
|
||||||
(Eq _ _ _ 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 (App fun arg _) = App fun arg loc
|
||||||
setLoc loc (CasePair qty pair ret body _) =
|
setLoc loc (CasePair qty pair ret body _) =
|
||||||
CasePair qty pair ret body loc
|
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 _) =
|
setLoc loc (CaseEnum qty tag ret arms _) =
|
||||||
CaseEnum qty tag ret arms loc
|
CaseEnum qty tag ret arms loc
|
||||||
setLoc loc (CaseNat qty qtyIH nat ret zero succ _) =
|
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 (Lam body _) = Lam body loc
|
||||||
setLoc loc (Sig fst snd _) = Sig fst snd loc
|
setLoc loc (Sig fst snd _) = Sig fst snd loc
|
||||||
setLoc loc (Pair fst snd _) = Pair 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 (Enum cases _) = Enum cases loc
|
||||||
setLoc loc (Tag tag _) = Tag tag loc
|
setLoc loc (Tag tag _) = Tag tag loc
|
||||||
setLoc loc (Eq ty l r _) = Eq ty l r loc
|
setLoc loc (Eq ty l r _) = Eq ty l r loc
|
||||||
|
|
|
||||||
|
|
@ -346,6 +346,8 @@ prettyTyCasePat KPi [< a, b] =
|
||||||
parens . hsep =<< sequence [prettyTBind a, arrowD, prettyTBind b]
|
parens . hsep =<< sequence [prettyTBind a, arrowD, prettyTBind b]
|
||||||
prettyTyCasePat KSig [< a, b] =
|
prettyTyCasePat KSig [< a, b] =
|
||||||
parens . hsep =<< sequence [prettyTBind a, timesD, prettyTBind 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 KEnum [<] = hl Syntax $ text "{}"
|
||||||
prettyTyCasePat KEq [< a0, a1, a, l, r] =
|
prettyTyCasePat KEq [< a0, a1, a, l, r] =
|
||||||
hsep <$> sequence (eqD :: map prettyTBind [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
|
withPrec Outer $ prettyTerm dnames tnames $ assert_smaller p t
|
||||||
pure $ separateTight !commaD lines
|
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 _) =
|
prettyTerm dnames tnames (Enum cases _) =
|
||||||
prettyEnum $ SortedSet.toList cases
|
prettyEnum $ SortedSet.toList cases
|
||||||
|
|
||||||
|
|
@ -446,17 +463,22 @@ prettyTerm dnames tnames s@(DLam {}) =
|
||||||
prettyTerm dnames tnames (Nat _) = natD
|
prettyTerm dnames tnames (Nat _) = natD
|
||||||
prettyTerm dnames tnames (Zero _) = hl Syntax "0"
|
prettyTerm dnames tnames (Zero _) = hl Syntax "0"
|
||||||
prettyTerm dnames tnames (Succ p _) = do
|
prettyTerm dnames tnames (Succ p _) = do
|
||||||
succD <- succD
|
s <- succD
|
||||||
let succ : Doc opts -> Eff Pretty (Doc opts)
|
either (succ s) prettyNat =<< tryToNat s p
|
||||||
succ t = prettyAppD succD [t]
|
where
|
||||||
toNat : Term d n -> Eff Pretty (Either (Doc opts) Nat)
|
succ : Doc opts -> Doc opts -> Eff Pretty (Doc opts)
|
||||||
toNat s with (pushSubsts' s)
|
succ s t = prettyAppD s [t]
|
||||||
_ | Zero _ = pure $ Right 0
|
|
||||||
_ | Succ d _ = bitraverse succ (pure . S) =<<
|
tryToNat : Doc opts -> Term d n -> Eff Pretty (Either (Doc opts) Nat)
|
||||||
toNat (assert_smaller s d)
|
tryToNat s t with (pushSubsts' t)
|
||||||
_ | s' = map Left . withPrec Arg $
|
_ | Zero _ = pure $ Right 0
|
||||||
prettyTerm dnames tnames $ assert_smaller s s'
|
_ | Succ d _ = bitraverse (succ s) (pure . S) =<<
|
||||||
either succ (hl Syntax . text . show . S) =<< toNat p
|
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 _) =
|
prettyTerm dnames tnames (BOX qty ty _) =
|
||||||
bracks . hcat =<<
|
bracks . hcat =<<
|
||||||
|
|
@ -493,6 +515,16 @@ prettyElim dnames tnames (CasePair qty pair ret body _) = do
|
||||||
prettyCase dnames tnames qty pair ret
|
prettyCase dnames tnames qty pair ret
|
||||||
[MkCaseArm pat [<] [< x, y] body.term]
|
[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
|
prettyElim dnames tnames (CaseEnum qty tag ret arms _) = do
|
||||||
arms <- for (SortedMap.toList arms) $ \(tag, body) =>
|
arms <- for (SortedMap.toList arms) $ \(tag, body) =>
|
||||||
pure $ MkCaseArm !(prettyTag tag) [<] [<] body
|
pure $ MkCaseArm !(prettyTag tag) [<] [<] body
|
||||||
|
|
|
||||||
|
|
@ -56,12 +56,12 @@ namespace DSubst.DScopeTermN
|
||||||
(//) : {s : Nat} ->
|
(//) : {s : Nat} ->
|
||||||
DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
|
DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
|
||||||
DScopeTermN s d2 n
|
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
|
S ns (N body) // th = S ns $ N $ body // th
|
||||||
|
|
||||||
|
|
||||||
export %inline FromVar (Elim d) where fromVarLoc = B
|
export %inline FromVar (Elim d) where fromVar = B
|
||||||
export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
|
export %inline FromVar (Term d) where fromVar = E .: fromVar
|
||||||
|
|
||||||
|
|
||||||
||| does the minimal reasonable work:
|
||| does the minimal reasonable work:
|
||||||
|
|
@ -104,7 +104,7 @@ namespace ScopeTermN
|
||||||
(//) : {s : Nat} ->
|
(//) : {s : Nat} ->
|
||||||
ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
|
ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
|
||||||
ScopeTermN s d 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
|
S ns (N body) // th = S ns $ N $ body // th
|
||||||
|
|
||||||
namespace DScopeTermN
|
namespace DScopeTermN
|
||||||
|
|
@ -147,24 +147,24 @@ weakE by t = t // shift by
|
||||||
|
|
||||||
parameters {s : Nat}
|
parameters {s : Nat}
|
||||||
namespace ScopeTermBody
|
namespace ScopeTermBody
|
||||||
export %inline
|
public export %inline
|
||||||
(.term) : ScopedBody s (Term d) n -> Term d (s + n)
|
(.term) : ScopedBody s (Term d) n -> Term d (s + n)
|
||||||
(Y b).term = b
|
(Y b).term = b
|
||||||
(N b).term = weakT s b
|
(N b).term = weakT s b
|
||||||
|
|
||||||
namespace ScopeTermN
|
namespace ScopeTermN
|
||||||
export %inline
|
public export %inline
|
||||||
(.term) : ScopeTermN s d n -> Term d (s + n)
|
(.term) : ScopeTermN s d n -> Term d (s + n)
|
||||||
t.term = t.body.term
|
t.term = t.body.term
|
||||||
|
|
||||||
namespace DScopeTermBody
|
namespace DScopeTermBody
|
||||||
export %inline
|
public export %inline
|
||||||
(.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
|
(.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
|
||||||
(Y b).term = b
|
(Y b).term = b
|
||||||
(N b).term = dweakT s b
|
(N b).term = dweakT s b
|
||||||
|
|
||||||
namespace DScopeTermN
|
namespace DScopeTermN
|
||||||
export %inline
|
public export %inline
|
||||||
(.term) : DScopeTermN s d n -> Term (s + d) n
|
(.term) : DScopeTermN s d n -> Term (s + d) n
|
||||||
t.term = t.body.term
|
t.term = t.body.term
|
||||||
|
|
||||||
|
|
@ -189,12 +189,12 @@ dsub1 t p = dsubN t [< p]
|
||||||
|
|
||||||
|
|
||||||
public export %inline
|
public export %inline
|
||||||
(.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
|
(.zero) : DScopeTerm d n -> Term d n
|
||||||
body.zero = dsub1 body $ K Zero loc
|
body.zero = dsub1 body $ K Zero body.loc
|
||||||
|
|
||||||
public export %inline
|
public export %inline
|
||||||
(.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
|
(.one) : DScopeTerm d n -> Term d n
|
||||||
body.one = dsub1 body $ K One loc
|
body.one = dsub1 body $ K One body.loc
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
|
|
@ -261,6 +261,10 @@ mutual
|
||||||
nclo $ Sig (a // th // ph) (b // th // ph) loc
|
nclo $ Sig (a // th // ph) (b // th // ph) loc
|
||||||
pushSubstsWith th ph (Pair s t loc) =
|
pushSubstsWith th ph (Pair s t loc) =
|
||||||
nclo $ Pair (s // th // ph) (t // th // ph) 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) =
|
pushSubstsWith th ph (Enum tags loc) =
|
||||||
nclo $ Enum tags loc
|
nclo $ Enum tags loc
|
||||||
pushSubstsWith th ph (Tag tag loc) =
|
pushSubstsWith th ph (Tag tag loc) =
|
||||||
|
|
@ -299,6 +303,8 @@ mutual
|
||||||
nclo $ App (f // th // ph) (s // th // ph) loc
|
nclo $ App (f // th // ph) (s // th // ph) loc
|
||||||
pushSubstsWith th ph (CasePair pi p r b loc) =
|
pushSubstsWith th ph (CasePair pi p r b loc) =
|
||||||
nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) 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) =
|
pushSubstsWith th ph (CaseEnum pi t r arms loc) =
|
||||||
nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
|
nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
|
||||||
(map (\b => b // th // ph) arms) loc
|
(map (\b => b // th // ph) arms) loc
|
||||||
|
|
|
||||||
|
|
@ -52,6 +52,10 @@ mutual
|
||||||
Sig <$> tightenT p fst <*> tightenS p snd <*> pure loc
|
Sig <$> tightenT p fst <*> tightenS p snd <*> pure loc
|
||||||
tightenT' p (Pair fst snd loc) =
|
tightenT' p (Pair fst snd loc) =
|
||||||
Pair <$> tightenT p fst <*> tightenT p snd <*> pure 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) =
|
tightenT' p (Enum cases loc) =
|
||||||
pure $ Enum cases loc
|
pure $ Enum cases loc
|
||||||
tightenT' p (Tag tag loc) =
|
tightenT' p (Tag tag loc) =
|
||||||
|
|
@ -87,6 +91,12 @@ mutual
|
||||||
<*> tightenS p ret
|
<*> tightenS p ret
|
||||||
<*> tightenS p body
|
<*> tightenS p body
|
||||||
<*> pure loc
|
<*> 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) =
|
tightenE' p (CaseEnum qty tag ret arms loc) =
|
||||||
CaseEnum qty <$> tightenE p tag
|
CaseEnum qty <$> tightenE p tag
|
||||||
<*> tightenS p ret
|
<*> tightenS p ret
|
||||||
|
|
@ -167,6 +177,10 @@ mutual
|
||||||
Sig <$> dtightenT p fst <*> dtightenS p snd <*> pure loc
|
Sig <$> dtightenT p fst <*> dtightenS p snd <*> pure loc
|
||||||
dtightenT' p (Pair fst snd loc) =
|
dtightenT' p (Pair fst snd loc) =
|
||||||
Pair <$> dtightenT p fst <*> dtightenT p snd <*> pure 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) =
|
dtightenT' p (Enum cases loc) =
|
||||||
pure $ Enum cases loc
|
pure $ Enum cases loc
|
||||||
dtightenT' p (Tag tag loc) =
|
dtightenT' p (Tag tag loc) =
|
||||||
|
|
@ -202,6 +216,12 @@ mutual
|
||||||
<*> dtightenS p ret
|
<*> dtightenS p ret
|
||||||
<*> dtightenS p body
|
<*> dtightenS p body
|
||||||
<*> pure loc
|
<*> 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) =
|
dtightenE' p (CaseEnum qty tag ret arms loc) =
|
||||||
CaseEnum qty <$> dtightenE p tag
|
CaseEnum qty <$> dtightenE p tag
|
||||||
<*> dtightenS p ret
|
<*> dtightenS p ret
|
||||||
|
|
|
||||||
|
|
@ -9,7 +9,7 @@ import Generics.Derive
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
data TyConKind = KTYPE | KPi | KSig | KEnum | KEq | KNat | KBOX
|
data TyConKind = KTYPE | KPi | KSig | KW | KEnum | KEq | KNat | KBOX
|
||||||
%name TyConKind k
|
%name TyConKind k
|
||||||
%runElab derive "TyConKind" [Eq.Eq, Ord.Ord, Show.Show, Generic, Meta, DecEq]
|
%runElab derive "TyConKind" [Eq.Eq, Ord.Ord, Show.Show, Generic, Meta, DecEq]
|
||||||
|
|
||||||
|
|
@ -28,6 +28,7 @@ arity : TyConKind -> Nat
|
||||||
arity KTYPE = 0
|
arity KTYPE = 0
|
||||||
arity KPi = 2
|
arity KPi = 2
|
||||||
arity KSig = 2
|
arity KSig = 2
|
||||||
|
arity KW = 2
|
||||||
arity KEnum = 0
|
arity KEnum = 0
|
||||||
arity KEq = 5
|
arity KEq = 5
|
||||||
arity KNat = 0
|
arity KNat = 0
|
||||||
|
|
|
||||||
|
|
@ -139,13 +139,9 @@ weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n
|
interface FromVar f where %inline fromVar : Var n -> Loc -> f n
|
||||||
|
|
||||||
public export %inline
|
public export FromVar Var where fromVar x _ = x
|
||||||
fromVar : FromVar f => Var n -> {default noLoc loc : Loc} -> f n
|
|
||||||
fromVar x = fromVarLoc x loc
|
|
||||||
|
|
||||||
public export FromVar Var where fromVarLoc x _ = x
|
|
||||||
|
|
||||||
export
|
export
|
||||||
tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->
|
tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->
|
||||||
|
|
|
||||||
|
|
@ -57,27 +57,40 @@ typecaseTel : (k : TyConKind) -> BContext (arity k) -> Universe ->
|
||||||
CtxExtension d n (arity k + n)
|
CtxExtension d n (arity k + n)
|
||||||
typecaseTel k xs u = case k of
|
typecaseTel k xs u = case k of
|
||||||
KTYPE => [<]
|
KTYPE => [<]
|
||||||
-- A : ★ᵤ, B : 0.A → ★ᵤ
|
KPi => binaryTyCon xs
|
||||||
KPi =>
|
KSig => binaryTyCon xs
|
||||||
let [< a, b] = xs in
|
KW => binaryTyCon xs
|
||||||
[< (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)]
|
|
||||||
KEnum => [<]
|
KEnum => [<]
|
||||||
-- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
|
KEq => eqCon xs
|
||||||
KEq =>
|
KNat => [<]
|
||||||
let [< a0, a1, a, l, r] = xs in
|
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, a0, TYPE u a0.loc),
|
||||||
(Zero, a1, TYPE u a1.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, a, Eq0 (TYPE u a.loc) (BVT 1 a.loc) (BVT 0 a.loc) a.loc),
|
||||||
(Zero, l, BVT 2 l.loc),
|
(Zero, l, BVT 2 l.loc),
|
||||||
(Zero, r, BVT 2 r.loc)]
|
(Zero, r, BVT 2 r.loc)]
|
||||||
KNat => [<]
|
|
||||||
-- A : ★ᵤ
|
||| if a ⋄ b : (x : A) ⊲ B, then b : `supSubTy a A B _`
|
||||||
KBOX => let [< a] = xs in [< (Zero, a, TYPE u a.loc)]
|
||| 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
|
mutual
|
||||||
|
|
@ -188,6 +201,17 @@ mutual
|
||||||
|
|
||||||
check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
|
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
|
check' ctx sg (Pair fst snd loc) ty = do
|
||||||
(tfst, tsnd) <- expectSig !(askAt DEFS) ctx ty.loc ty
|
(tfst, tsnd) <- expectSig !(askAt DEFS) ctx ty.loc ty
|
||||||
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
|
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
|
||||||
|
|
@ -281,6 +305,16 @@ mutual
|
||||||
checkType' ctx t@(Pair {}) u =
|
checkType' ctx t@(Pair {}) u =
|
||||||
throw $ NotType t.loc ctx t
|
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 ()
|
checkType' ctx (Enum {}) u = pure ()
|
||||||
-- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ
|
-- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ
|
||||||
|
|
||||||
|
|
@ -313,7 +347,7 @@ mutual
|
||||||
infres <- inferC ctx szero e
|
infres <- inferC ctx szero e
|
||||||
-- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
|
-- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
|
||||||
case u of
|
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
|
Nothing => ignore $ expectTYPE !(askAt DEFS) ctx e.loc infres.type
|
||||||
-- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
|
-- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
|
||||||
|
|
||||||
|
|
@ -388,6 +422,42 @@ mutual
|
||||||
qout = pi * pairres.qout + bodyout
|
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
|
infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
|
||||||
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
|
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
|
||||||
tres <- inferC ctx sg t
|
tres <- inferC ctx sg t
|
||||||
|
|
|
||||||
|
|
@ -47,14 +47,22 @@ public export
|
||||||
substCasePairRet : BContext 2 -> Term d n -> ScopeTerm d n -> Term d (2 + n)
|
substCasePairRet : BContext 2 -> Term d n -> ScopeTerm d n -> Term d (2 + n)
|
||||||
substCasePairRet [< x, y] dty retty =
|
substCasePairRet [< x, y] dty retty =
|
||||||
let tm = Pair (BVT 1 x.loc) (BVT 0 y.loc) $ x.loc `extendL` y.loc
|
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
|
in
|
||||||
retty.term // (arg ::: shift 2)
|
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
|
public export
|
||||||
substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n)
|
substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n)
|
||||||
substCaseSuccRet [< p, ih] retty =
|
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
|
in
|
||||||
retty.term // (arg ::: shift 2)
|
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 : Term d n -> Eff fs (Term d n, ScopeTerm d n)
|
||||||
expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
|
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
|
export covering %inline
|
||||||
expectEnum : Term d n -> Eff fs (SortedSet TagVal)
|
expectEnum : Term d n -> Eff fs (SortedSet TagVal)
|
||||||
expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
|
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 : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n)
|
||||||
expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
|
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
|
export covering %inline
|
||||||
expectEnum : Term 0 n -> Eff fs (SortedSet TagVal)
|
expectEnum : Term 0 n -> Eff fs (SortedSet TagVal)
|
||||||
expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
|
expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
|
||||||
|
|
|
||||||
|
|
@ -197,7 +197,7 @@ namespace EqContext
|
||||||
toTyContext : (e : EqContext n) -> TyContext e.dimLen n
|
toTyContext : (e : EqContext n) -> TyContext e.dimLen n
|
||||||
toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
|
toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
|
||||||
MkTyContext {
|
MkTyContext {
|
||||||
dctx = fromGround dassign,
|
dctx = fromGround dnames dassign,
|
||||||
tctx = map (// shift0 dimLen) tctx,
|
tctx = map (// shift0 dimLen) tctx,
|
||||||
dnames, tnames, qtys
|
dnames, tnames, qtys
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -58,6 +58,7 @@ data Error
|
||||||
= ExpectedTYPE Loc (NameContexts d n) (Term d n)
|
= ExpectedTYPE Loc (NameContexts d n) (Term d n)
|
||||||
| ExpectedPi Loc (NameContexts d n) (Term d n)
|
| ExpectedPi Loc (NameContexts d n) (Term d n)
|
||||||
| ExpectedSig 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)
|
| ExpectedEnum Loc (NameContexts d n) (Term d n)
|
||||||
| ExpectedEq Loc (NameContexts d n) (Term d n)
|
| ExpectedEq Loc (NameContexts d n) (Term d n)
|
||||||
| ExpectedNat 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
|
(ExpectedTYPE loc _ _).loc = loc
|
||||||
(ExpectedPi loc _ _).loc = loc
|
(ExpectedPi loc _ _).loc = loc
|
||||||
(ExpectedSig loc _ _).loc = loc
|
(ExpectedSig loc _ _).loc = loc
|
||||||
|
(ExpectedW loc _ _).loc = loc
|
||||||
(ExpectedEnum loc _ _).loc = loc
|
(ExpectedEnum loc _ _).loc = loc
|
||||||
(ExpectedEq loc _ _).loc = loc
|
(ExpectedEq loc _ _).loc = loc
|
||||||
(ExpectedNat loc _ _).loc = loc
|
(ExpectedNat loc _ _).loc = loc
|
||||||
|
|
@ -256,12 +258,16 @@ prettyErrorNoLoc showContext = \case
|
||||||
hangDSingle "expected a pair type, but got"
|
hangDSingle "expected a pair type, but got"
|
||||||
!(prettyTerm ctx.dnames ctx.tnames s)
|
!(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 =>
|
ExpectedEnum _ ctx s =>
|
||||||
hangDSingle "expected an enumeration type, but got"
|
hangDSingle "expected an enumeration type, but got"
|
||||||
!(prettyTerm ctx.dnames ctx.tnames s)
|
!(prettyTerm ctx.dnames ctx.tnames s)
|
||||||
|
|
||||||
ExpectedEq _ ctx s =>
|
ExpectedEq _ ctx s =>
|
||||||
hangDSingle "expected an enumeration type, but got"
|
hangDSingle "expected an equality type, but got"
|
||||||
!(prettyTerm ctx.dnames ctx.tnames s)
|
!(prettyTerm ctx.dnames ctx.tnames s)
|
||||||
|
|
||||||
ExpectedNat _ ctx s =>
|
ExpectedNat _ ctx s =>
|
||||||
|
|
|
||||||
11
syntax.ebnf
11
syntax.ebnf
|
|
@ -24,7 +24,7 @@ dim arg = "@", dim.
|
||||||
|
|
||||||
pat var = NAME | "_".
|
pat var = NAME | "_".
|
||||||
|
|
||||||
term = lambda | case | pi | sigma | ann.
|
term = lambda | case | pi | w | sigma | ann.
|
||||||
|
|
||||||
lambda = ("λ" | "δ"), {pat var}+, "⇒", term.
|
lambda = ("λ" | "δ"), {pat var}+, "⇒", term.
|
||||||
|
|
||||||
|
|
@ -39,17 +39,22 @@ pattern = "zero" | "0"
|
||||||
(* default qty for IH is 1 *)
|
(* default qty for IH is 1 *)
|
||||||
| TAG
|
| TAG
|
||||||
| "[", pat var, "]"
|
| "[", pat var, "]"
|
||||||
| "(", pat var, ",", pat var, ")".
|
| "(", pat var, ",", pat var, ")"
|
||||||
|
| pat var, "⋄", pat var, [",", [qty, "."], pat var].
|
||||||
|
|
||||||
(* default qty is 1 *)
|
(* default qty is 1 *)
|
||||||
pi = [qty, "."], (binder | term arg), "→", term.
|
pi = [qty, "."], (binder | term arg), "→", term.
|
||||||
binder = "(", {NAME}+, ":", term, ")".
|
binder = "(", {NAME}+, ":", term, ")".
|
||||||
|
|
||||||
|
w = binder, "⊲", ann.
|
||||||
|
|
||||||
sigma = (binder | ann), "×", (sigma | ann).
|
sigma = (binder | ann), "×", (sigma | ann).
|
||||||
|
|
||||||
ann = infix eq, ["∷", term].
|
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.
|
app term = coe | comp | split universe | dep eq | succ | normal app.
|
||||||
split universe = "★", NAT.
|
split universe = "★", NAT.
|
||||||
|
|
|
||||||
|
|
@ -97,7 +97,7 @@ tests = "dimension constraints" :- [
|
||||||
testPrettyD iijj ZeroIsOne "𝑖, 𝑗, 0 = 1",
|
testPrettyD iijj ZeroIsOne "𝑖, 𝑗, 0 = 1",
|
||||||
testPrettyD [<] new "" {label = "[empty output from empty context]"},
|
testPrettyD [<] new "" {label = "[empty output from empty context]"},
|
||||||
testPrettyD ii new "𝑖",
|
testPrettyD ii new "𝑖",
|
||||||
testPrettyD iijj (fromGround [< Zero, One])
|
testPrettyD iijj (fromGround iijj [< Zero, One])
|
||||||
"𝑖, 𝑗, 𝑖 = 0, 𝑗 = 1",
|
"𝑖, 𝑗, 𝑖 = 0, 𝑗 = 1",
|
||||||
testPrettyD iijj (C [< Just (^K Zero), Nothing])
|
testPrettyD iijj (C [< Just (^K Zero), Nothing])
|
||||||
"𝑖, 𝑗, 𝑖 = 0",
|
"𝑖, 𝑗, 𝑖 = 0",
|
||||||
|
|
|
||||||
|
|
@ -16,6 +16,8 @@ defGlobals = fromList
|
||||||
("a'", ^mkPostulate gany (^FT "A" 0)),
|
("a'", ^mkPostulate gany (^FT "A" 0)),
|
||||||
("b", ^mkPostulate gany (^FT "B" 0)),
|
("b", ^mkPostulate gany (^FT "B" 0)),
|
||||||
("f", ^mkPostulate gany (^Arr One (^FT "A" 0) (^FT "A" 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))),
|
("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))),
|
("eq-AB", ^mkPostulate gzero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))),
|
||||||
("two", ^mkDef gany (^Nat) (^Succ (^Succ (^Zero))))]
|
("two", ^mkDef gany (^Nat) (^Succ (^Succ (^Zero))))]
|
||||||
|
|
@ -517,6 +519,18 @@ tests = "equality & subtyping" :- [
|
||||||
|
|
||||||
todo "pair elim",
|
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 types",
|
||||||
todo "enum",
|
todo "enum",
|
||||||
todo "enum elim",
|
todo "enum elim",
|
||||||
|
|
|
||||||
|
|
@ -168,6 +168,8 @@ tests = "parser" :- [
|
||||||
(App (V "B" {}) (V "x" {}) _) _) _),
|
(App (V "B" {}) (V "x" {}) _) _) _),
|
||||||
parseMatch term "(x : A) → B x"
|
parseMatch term "(x : A) → B x"
|
||||||
`(Pi (PQ One _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "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"
|
parseMatch term "1.A → B"
|
||||||
`(Pi (PQ One _) (Unused _) (V "A" {}) (V "B" {}) _),
|
`(Pi (PQ One _) (Unused _) (V "A" {}) (V "B" {}) _),
|
||||||
parseMatch term "A → B"
|
parseMatch term "A → B"
|
||||||
|
|
@ -249,6 +251,43 @@ tests = "parser" :- [
|
||||||
parseFails term "(x,,y)"
|
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" :- [
|
"equality type" :- [
|
||||||
parseMatch term "Eq (i ⇒ A) s t"
|
parseMatch term "Eq (i ⇒ A) s t"
|
||||||
`(Eq (PV "i" _, V "A" {}) (V "s" {}) (V "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; }"
|
parseMatch term "caseω n return ℕ of { succ _, ih ⇒ ih; zero ⇒ 0; }"
|
||||||
`(Case (PQ Any _) (V "n" {}) (Unused _, Nat _)
|
`(Case (PQ Any _) (V "n" {}) (Unused _, Nat _)
|
||||||
(CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
|
(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 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" :- [
|
"definitions" :- [
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue