rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

WIP: 𝕎 #25

Closed
rhi wants to merge 8 commits from 𝕎 into 🐉
pull from: 𝕎
merge into: rhi:🐉
Conversation 1 Commits 8 Files changed 31 +1010 -295
31 changed files with 1010 additions and 295 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
examples/bool.quox
View file

@ -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
View 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)
}
}

5
lib/Quox/Displace.idr
View file

@ -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) =

20
lib/Quox/EffExtra.idr
View file

@ -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) =>

118
lib/Quox/Equal.idr
View file

@ -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, _})
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

6
lib/Quox/Loc.idr
View file

@ -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

25
lib/Quox/Name.idr
View file

@ -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

15
lib/Quox/No.idr
View file

@ -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

31
lib/Quox/Parser/FromParser.idr
View file

@ -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

2
lib/Quox/Parser/Lexer.idr
View file

@ -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",

183
lib/Quox/Parser/Parser.idr
View file

@ -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,6 +227,7 @@ 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
@ -235,6 +237,7 @@ Located PCasePat where
(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

7
lib/Quox/Parser/Syntax.idr
View file

@ -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
@ -132,6 +138,7 @@ Located PTerm where
export
Located PCaseBody where
(CasePair _ _ loc).loc = loc
(CaseW _ _ _ _ loc).loc = loc
(CaseEnum _ loc).loc = loc
(CaseNat _ _ loc).loc = loc
(CaseBox _ _ loc).loc = loc

14
lib/Quox/Pretty.idr
View file

@ -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 ","

405
lib/Quox/Reduce.idr
View file

@ -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

2
lib/Quox/Syntax/Dim.idr
View file

@ -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

12
lib/Quox/Syntax/DimEq.idr
View file

@ -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)

14
lib/Quox/Syntax/Subst.idr
View file

@ -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

29
lib/Quox/Syntax/Term/Base.idr
View file

@ -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

52
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -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)
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 (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
_ | 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

30
lib/Quox/Syntax/Term/Subst.idr
View file

@ -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

20
lib/Quox/Syntax/Term/Tighten.idr
View file

@ -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

3
lib/Quox/Syntax/Term/TyConKind.idr
View file

@ -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

8
lib/Quox/Syntax/Var.idr
View file

@ -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) ->

102
lib/Quox/Typechecker.idr
View file

@ -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

20
lib/Quox/Typing.idr
View file

@ -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)

2
lib/Quox/Typing/Context.idr
View file

@ -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
}

8
lib/Quox/Typing/Error.idr
View file

@ -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
View file

@ -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.

2
tests/Tests/DimEq.idr
View file

@ -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",

14
tests/Tests/Equal.idr
View file

@ -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",

56
tests/Tests/Parser.idr
View file

@ -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" :- [