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