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

always vsep scheme lets, otherwise they are unreadable

Browse source
This commit is contained in:
rhiannon morris 2023-11-01 15:17:15 +01:00
parent 4cc50c6bcd
commit e0ed37720f
29 changed files with 474 additions and 301 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
lib/Quox/Displace.idr
View file

@ -16,6 +16,7 @@ parameters (k : Universe)
namespace Term
doDisplace (TYPE l loc) = TYPE (k + l) loc
doDisplace (IOState loc) = IOState loc
doDisplace (Pi qty arg res loc) =
Pi qty (doDisplace arg) (doDisplaceS res) loc
doDisplace (Lam body loc) = Lam (doDisplaceS body) loc
@ -29,6 +30,8 @@ parameters (k : Universe)
doDisplace (Nat loc) = Nat loc
doDisplace (Zero loc) = Zero loc
doDisplace (Succ p loc) = Succ (doDisplace p) loc
doDisplace (STRING loc) = STRING loc
doDisplace (Str s loc) = Str s loc
doDisplace (BOX qty ty loc) = BOX qty (doDisplace ty) loc
doDisplace (Box val loc) = Box (doDisplace val) loc
doDisplace (E e) = E (doDisplace e)

182
lib/Quox/Equal.idr
View file

@ -45,22 +45,26 @@ public export %inline
sameTyCon : (s, t : Term d n) ->
(0 ts : So (isTyConE s)) => (0 tt : So (isTyConE t)) =>
Bool
sameTyCon (TYPE {}) (TYPE {}) = True
sameTyCon (TYPE {}) _ = False
sameTyCon (Pi {}) (Pi {}) = True
sameTyCon (Pi {}) _ = False
sameTyCon (Sig {}) (Sig {}) = True
sameTyCon (Sig {}) _ = False
sameTyCon (Enum {}) (Enum {}) = True
sameTyCon (Enum {}) _ = False
sameTyCon (Eq {}) (Eq {}) = True
sameTyCon (Eq {}) _ = False
sameTyCon (Nat {}) (Nat {}) = True
sameTyCon (Nat {}) _ = False
sameTyCon (BOX {}) (BOX {}) = True
sameTyCon (BOX {}) _ = False
sameTyCon (E {}) (E {}) = True
sameTyCon (E {}) _ = False
sameTyCon (TYPE {}) (TYPE {}) = True
sameTyCon (TYPE {}) _ = False
sameTyCon (IOState {}) (IOState {}) = True
sameTyCon (IOState {}) _ = False
sameTyCon (Pi {}) (Pi {}) = True
sameTyCon (Pi {}) _ = False
sameTyCon (Sig {}) (Sig {}) = True
sameTyCon (Sig {}) _ = False
sameTyCon (Enum {}) (Enum {}) = True
sameTyCon (Enum {}) _ = False
sameTyCon (Eq {}) (Eq {}) = True
sameTyCon (Eq {}) _ = False
sameTyCon (Nat {}) (Nat {}) = True
sameTyCon (Nat {}) _ = False
sameTyCon (STRING {}) (STRING {}) = True
sameTyCon (STRING {}) _ = False
sameTyCon (BOX {}) (BOX {}) = True
sameTyCon (BOX {}) _ = False
sameTyCon (E {}) (E {}) = True
sameTyCon (E {}) _ = False
||| true if a type is known to be empty.
@ -78,6 +82,7 @@ isEmpty defs ctx sg ty0 = do
| Right n => pure False
case ty0 of
TYPE {} => pure False
IOState {} => pure False
Pi {arg, res, _} => pure False
Sig {fst, snd, _} =>
isEmpty defs ctx sg fst `orM`
@ -86,6 +91,7 @@ isEmpty defs ctx sg ty0 = do
pure $ null cases
Eq {} => pure False
Nat {} => pure False
STRING {} => pure False
BOX {ty, _} => isEmpty defs ctx sg ty
E _ => pure False
@ -108,6 +114,7 @@ isSubSing defs ctx sg ty0 = do
| Right n => pure False
case ty0 of
TYPE {} => pure False
IOState {} => pure False
Pi {arg, res, _} =>
isEmpty defs ctx sg arg `orM`
isSubSing defs (extendTy0 res.name arg ctx) sg res.term
@ -118,6 +125,7 @@ isSubSing defs ctx sg ty0 = do
pure $ length (SortedSet.toList cases) <= 1
Eq {} => pure True
Nat {} => pure False
STRING {} => pure False
BOX {ty, _} => isSubSing defs ctx sg ty
E _ => pure False
@ -171,21 +179,32 @@ namespace Term
Eff EqualInner ()
compare0' defs ctx sg (TYPE {}) s t = compareType defs ctx s t
compare0' defs ctx sg ty@(IOState {}) s t =
-- Γ ⊢ e = f ⇒ IOState
-- ----------------------
-- Γ ⊢ e = f ⇐ IOState
--
-- (no canonical values, ofc)
case (s, t) of
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
(E _, _) => wrongType t.loc ctx ty t
_ => wrongType s.loc ctx ty s
compare0' defs ctx sg ty@(Pi {qty, arg, res, _}) s t = local_ Equal $
-- Γ ⊢ A empty
-- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
if !(isEmpty defs ctx sg arg) then pure () else
case (s, t) of
-- Γ, x : A ⊢ s = t : B
-- Γ, x : A ⊢ s = t ⇐ B
-- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
(Lam b1 {}, Lam b2 {}) =>
compare0 defs ctx' sg res.term b1.term b2.term
-- Γ, x : A ⊢ s = e x : B
-- Γ, x : A ⊢ s = e x ⇐ B
-- -----------------------------------
-- Γ ⊢ (λ x ⇒ s) = e : (π·x : A) → B
-- Γ ⊢ (λ x ⇒ s) = e ⇐ (π·x : A) → B
(E e, Lam b {}) => eta s.loc e b
(Lam b {}, E e) => eta s.loc e b
@ -207,9 +226,9 @@ namespace Term
compare0' defs ctx sg ty@(Sig {fst, snd, _}) s t = local_ Equal $
case (s, t) of
-- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x}
-- Γ ⊢ s₁ = t₁ ⇐ A Γ ⊢ s₂ = t₂ ⇐ B{s₁/x}
-- --------------------------------------------
-- Γ ⊢ (s₁, t₁) = (s₂,t₂) : (x : A) × B
-- Γ ⊢ (s₁, t₁) = (s₂,t₂) ⇐ (x : A) × B
--
-- [todo] η for π ≥ 0 maybe
(Pair sFst sSnd {}, Pair tFst tSnd {}) => do
@ -236,7 +255,7 @@ namespace Term
compare0' defs ctx sg ty@(Enum {}) s t = local_ Equal $
case (s, t) of
-- --------------------
-- Γ ⊢ `t = `t : {ts}
-- Γ ⊢ `t = `t ⇐ {ts}
--
-- t ∈ ts is in the typechecker, not here, ofc
(Tag t1 {}, Tag t2 {}) =>
@ -254,18 +273,18 @@ namespace Term
-- ✨ uip ✨
--
-- ----------------------------
-- Γ ⊢ e = f : Eq [i ⇒ A] s t
-- Γ ⊢ e = f ⇐ Eq [i ⇒ A] s t
pure ()
compare0' defs ctx sg nat@(Nat {}) s t = local_ Equal $
case (s, t) of
-- ---------------
-- Γ ⊢ 0 = 0 : ℕ
-- Γ ⊢ 0 = 0 ⇐ ℕ
(Zero {}, Zero {}) => pure ()
-- Γ ⊢ s = t : ℕ
-- Γ ⊢ s = t ⇐ ℕ
-- -------------------------
-- Γ ⊢ succ s = succ t : ℕ
-- Γ ⊢ succ s = succ t ⇐ ℕ
(Succ s' {}, Succ t' {}) => compare0 defs ctx sg nat s' t'
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
@ -282,11 +301,24 @@ namespace Term
(E _, t) => wrongType t.loc ctx nat t
(s, _) => wrongType s.loc ctx nat s
compare0' defs ctx sg str@(STRING {}) s t = local_ Equal $
case (s, t) of
(Str x _, Str y _) => unless (x == y) $ clashT s.loc ctx str s t
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
(Str {}, E _) => clashT s.loc ctx str s t
(E _, Str {}) => clashT s.loc ctx str s t
(Str {}, _) => wrongType t.loc ctx str t
(E _, _) => wrongType t.loc ctx str t
_ => wrongType s.loc ctx str s
compare0' defs ctx sg bty@(BOX q ty {}) s t = local_ Equal $
case (s, t) of
-- Γ ⊢ s = t : A
-- Γ ⊢ s = t ⇐ A
-- -----------------------
-- Γ ⊢ [s] = [t] : [π.A]
-- Γ ⊢ [s] = [t] ⇐ [π.A]
(Box s _, Box t _) => compare0 defs ctx sg ty s t
-- Γ ⊢ s = (case1 e return A of {[x] ⇒ x}) ⇐ A
@ -329,6 +361,10 @@ compareType' defs ctx a@(TYPE k {}) (TYPE l {}) =
-- Γ ⊢ Type 𝓀 <: Type ℓ
expectModeU a.loc !mode k l
compareType' defs ctx a@(IOState {}) (IOState {}) =
-- Γ ⊢ IOState <: IOState
pure ()
compareType' defs ctx (Pi {qty = sQty, arg = sArg, res = sRes, loc})
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
@ -372,6 +408,11 @@ compareType' defs ctx (Nat {}) (Nat {}) =
-- Γ ⊢ ℕ <: ℕ
pure ()
compareType' defs ctx (STRING {}) (STRING {}) =
-- ------------
-- Γ ⊢ String <: String
pure ()
compareType' defs ctx (BOX pi a loc) (BOX rh b {}) = do
expectEqualQ loc pi rh
compareType defs ctx a b
@ -392,6 +433,36 @@ lookupFree defs ctx x u loc =
Just d => pure $ d.typeWithAt [|Z|] ctx.termLen u
export
typecaseTel : (k : TyConKind) -> BContext (arity k) -> Universe ->
CtxExtension d n (arity k + n)
typecaseTel k xs u = case k of
KTYPE => [<]
KIOState => [<]
-- 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)]
KEnum => [<]
-- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
KEq =>
let [< a0, a1, a, l, r] = xs in
[< (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 => [<]
KString => [<]
-- A : ★ᵤ
KBOX => let [< a] = xs in [< (Zero, a, TYPE u a.loc)]
namespace Elim
private data InnerErr : Type where
@ -437,51 +508,12 @@ namespace Elim
(def : Term 0 n) ->
Eff EqualElim ()
compareArm {b1 = Nothing, b2 = Nothing, _} = pure ()
compareArm defs ctx k ret u b1 b2 def =
let def = SN def in
compareArm_ defs ctx k ret u (fromMaybe def b1) (fromMaybe def b2)
where
compareArm_ : Definitions -> EqContext n -> (k : TyConKind) ->
(ret : Term 0 n) -> (u : Universe) ->
(b1, b2 : TypeCaseArmBody k 0 n) ->
Eff EqualElim ()
compareArm_ defs ctx KTYPE ret u b1 b2 =
try $ Term.compare0 defs ctx SZero ret b1.term b2.term
compareArm_ defs ctx KPi ret u b1 b2 = do
let [< a, b] = b1.names
ctx = extendTyN0
[< (a, TYPE u a.loc),
(b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
try $ Term.compare0 defs ctx SZero (weakT 2 ret) b1.term b2.term
compareArm_ defs ctx KSig ret u b1 b2 = do
let [< a, b] = b1.names
ctx = extendTyN0
[< (a, TYPE u a.loc),
(b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
try $ Term.compare0 defs ctx SZero (weakT 2 ret) b1.term b2.term
compareArm_ defs ctx KEnum ret u b1 b2 =
try $ Term.compare0 defs ctx SZero ret b1.term b2.term
compareArm_ defs ctx KEq ret u b1 b2 = do
let [< a0, a1, a, l, r] = b1.names
ctx = extendTyN0
[< (a0, TYPE u a0.loc),
(a1, TYPE u a1.loc),
(a, Eq0 (TYPE u a.loc) (BVT 1 a0.loc) (BVT 0 a1.loc) a.loc),
(l, BVT 2 a0.loc),
(r, BVT 2 a1.loc)] ctx
try $ Term.compare0 defs ctx SZero (weakT 5 ret) b1.term b2.term
compareArm_ defs ctx KNat ret u b1 b2 =
try $ Term.compare0 defs ctx SZero ret b1.term b2.term
compareArm_ defs ctx KBOX ret u b1 b2 = do
let ctx = extendTy0 b1.name (TYPE u b1.name.loc) ctx
try $ Term.compare0 defs ctx SZero (weakT 1 ret) b1.term b1.term
compareArm defs ctx k ret u b1 b2 def = do
let def = SN def
left = fromMaybe def b1; right = fromMaybe def b2
names = (fromMaybe def $ b1 <|> b2).names
try $ compare0 defs (extendTyN (typecaseTel k names u) ctx)
SZero (weakT (arity k) ret) left.term right.term
private covering
compare0Inner : Definitions -> EqContext n -> (sg : SQty) ->

74
lib/Quox/FreeVars.idr
View file

@ -180,23 +180,26 @@ export HasFreeVars (Elim d)
export
HasFreeVars (Term d) where
fv (TYPE {}) = none
fv (Pi {arg, res, _}) = fv arg <+> fv res
fv (Lam {body, _}) = fv body
fv (Sig {fst, snd, _}) = fv fst <+> fv snd
fv (Pair {fst, snd, _}) = fv fst <+> fv snd
fv (Enum {}) = none
fv (Tag {}) = none
fv (Eq {ty, l, r, _}) = fvD ty <+> fv l <+> fv r
fv (DLam {body, _}) = fvD body
fv (Nat {}) = none
fv (Zero {}) = none
fv (Succ {p, _}) = fv p
fv (BOX {ty, _}) = fv ty
fv (Box {val, _}) = fv val
fv (E e) = fv e
fv (CloT s) = fv s
fv (DCloT s) = fv s.term
fv (TYPE {}) = none
fv (IOState {}) = none
fv (Pi {arg, res, _}) = fv arg <+> fv res
fv (Lam {body, _}) = fv body
fv (Sig {fst, snd, _}) = fv fst <+> fv snd
fv (Pair {fst, snd, _}) = fv fst <+> fv snd
fv (Enum {}) = none
fv (Tag {}) = none
fv (Eq {ty, l, r, _}) = fvD ty <+> fv l <+> fv r
fv (DLam {body, _}) = fvD body
fv (Nat {}) = none
fv (Zero {}) = none
fv (Succ {p, _}) = fv p
fv (STRING {}) = none
fv (Str {}) = none
fv (BOX {ty, _}) = fv ty
fv (Box {val, _}) = fv val
fv (E e) = fv e
fv (CloT s) = fv s
fv (DCloT s) = fv s.term
export
HasFreeVars (Elim d) where
@ -255,23 +258,26 @@ export HasFreeDVars Elim
export
HasFreeDVars Term where
fdv (TYPE {}) = none
fdv (Pi {arg, res, _}) = fdv arg <+> fdvT res
fdv (Lam {body, _}) = fdvT body
fdv (Sig {fst, snd, _}) = fdv fst <+> fdvT snd
fdv (Pair {fst, snd, _}) = fdv fst <+> fdv snd
fdv (Enum {}) = none
fdv (Tag {}) = none
fdv (Eq {ty, l, r, _}) = fdv @{DScope} ty <+> fdv l <+> fdv r
fdv (DLam {body, _}) = fdv @{DScope} body
fdv (Nat {}) = none
fdv (Zero {}) = none
fdv (Succ {p, _}) = fdv p
fdv (BOX {ty, _}) = fdv ty
fdv (Box {val, _}) = fdv val
fdv (E e) = fdv e
fdv (CloT s) = fdv s @{WithSubst}
fdv (DCloT s) = fdvSubst s
fdv (TYPE {}) = none
fdv (IOState {}) = none
fdv (Pi {arg, res, _}) = fdv arg <+> fdvT res
fdv (Lam {body, _}) = fdvT body
fdv (Sig {fst, snd, _}) = fdv fst <+> fdvT snd
fdv (Pair {fst, snd, _}) = fdv fst <+> fdv snd
fdv (Enum {}) = none
fdv (Tag {}) = none
fdv (Eq {ty, l, r, _}) = fdv @{DScope} ty <+> fdv l <+> fdv r
fdv (DLam {body, _}) = fdv @{DScope} body
fdv (Nat {}) = none
fdv (Zero {}) = none
fdv (Succ {p, _}) = fdv p
fdv (STRING {}) = none
fdv (Str {}) = none
fdv (BOX {ty, _}) = fdv ty
fdv (Box {val, _}) = fdv val
fdv (E e) = fdv e
fdv (CloT s) = fdv s @{WithSubst}
fdv (DCloT s) = fdvSubst s
export
HasFreeDVars Elim where

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

@ -142,6 +142,9 @@ mutual
TYPE k loc =>
pure $ TYPE k loc
IOState loc =>
pure $ IOState loc
Pi pi x s t loc =>
Pi (fromPQty pi)
<$> fromPTermWith ds ns s
@ -189,6 +192,9 @@ mutual
Zero loc => pure $ Zero loc
Succ n loc => [|Succ (fromPTermWith ds ns n) (pure loc)|]
STRING loc => pure $ STRING loc
Str str loc => pure $ Str str loc
Case pi nat (r, ret) (CaseNat zer (s, pi', ih, suc) _) loc =>
map E $ CaseNat (fromPQty pi) (fromPQty pi')
<$> fromPTermElim ds ns nat

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

@ -222,6 +222,8 @@ reserved =
Word "ω" `Or` Sym "#",
Sym "★" `Or` Word "Type",
Word "ℕ" `Or` Word "Nat",
Word1 "IOState",
Word1 "String",
Word1 "zero", Word1 "succ",
Word1 "coe", Word1 "comp",
Word1 "def",

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

@ -292,11 +292,14 @@ export
termArg : FileName -> Grammar True PTerm
termArg fname = withLoc fname $
[|TYPE universe1|]
<|> IOState <$ res "IOState"
<|> [|Enum enumType|]
<|> [|Tag tag|]
<|> const <$> boxTerm fname
<|> Nat <$ res "ℕ"
<|> Zero <$ res "zero"
<|> STRING <$ res "String"
<|> [|Str strLit|]
<|> [|fromNat nat|]
<|> [|V qname displacement|]
<|> const <$> tupleTerm fname

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

@ -67,6 +67,8 @@ namespace PTerm
data PTerm =
TYPE Universe Loc
| IOState Loc
| Pi PQty PatVar PTerm PTerm Loc
| Lam PatVar PTerm Loc
| App PTerm PTerm Loc
@ -86,6 +88,9 @@ namespace PTerm
| Nat Loc
| Zero Loc | Succ PTerm Loc
| STRING Loc -- "String" is a reserved word in idris
| Str String Loc
| BOX PQty PTerm Loc
| Box PTerm Loc
@ -109,29 +114,32 @@ namespace PTerm
export
Located PTerm where
(TYPE _ loc).loc = loc
(Pi _ _ _ _ loc).loc = loc
(Lam _ _ loc).loc = loc
(App _ _ loc).loc = loc
(Sig _ _ _ loc).loc = loc
(Pair _ _ loc).loc = loc
(Fst _ loc).loc = loc
(Snd _ loc).loc = loc
(Case _ _ _ _ loc).loc = loc
(Enum _ loc).loc = loc
(Tag _ loc).loc = loc
(Eq _ _ _ loc).loc = loc
(DLam _ _ loc).loc = loc
(DApp _ _ loc).loc = loc
(Nat loc).loc = loc
(Zero loc).loc = loc
(Succ _ loc).loc = loc
(BOX _ _ loc).loc = loc
(Box _ loc).loc = loc
(V _ _ loc).loc = loc
(Ann _ _ loc).loc = loc
(Coe _ _ _ _ loc).loc = loc
(Comp _ _ _ _ _ _ _ loc).loc = loc
(TYPE _ loc).loc = loc
(IOState loc).loc = loc
(Pi _ _ _ _ loc).loc = loc
(Lam _ _ loc).loc = loc
(App _ _ loc).loc = loc
(Sig _ _ _ loc).loc = loc
(Pair _ _ loc).loc = loc
(Fst _ loc).loc = loc
(Snd _ loc).loc = loc
(Case _ _ _ _ loc).loc = loc
(Enum _ loc).loc = loc
(Tag _ loc).loc = loc
(Eq _ _ _ loc).loc = loc
(DLam _ _ loc).loc = loc
(DApp _ _ loc).loc = loc
(Nat loc).loc = loc
(Zero loc).loc = loc
(Succ _ loc).loc = loc
(STRING loc).loc = loc
(Str _ loc).loc = loc
(BOX _ _ loc).loc = loc
(Box _ loc).loc = loc
(V _ _ loc).loc = loc
(Ann _ _ loc).loc = loc
(Coe _ _ _ _ loc).loc = loc
(Comp _ _ _ _ _ _ _ loc).loc = loc
export
Located PCaseBody where

16
lib/Quox/Pretty.idr
View file

@ -248,11 +248,12 @@ prettyDBind = hl DVar . prettyBind'
export %inline
typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
typeD, ioStateD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
stringD, eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD :
{opts : LayoutOpts} -> Eff Pretty (Doc opts)
typeD = hl Syntax . text =<< ifUnicode "★" "Type"
ioStateD = hl Syntax $ text "IOState"
arrowD = hl Delim . text =<< ifUnicode "→" "->"
darrowD = hl Delim . text =<< ifUnicode "⇒" "=>"
timesD = hl Delim . text =<< ifUnicode "×" "**"
@ -261,6 +262,7 @@ eqndD = hl Delim . text =<< ifUnicode "≡" "=="
dlamD = hl Syntax . text =<< ifUnicode "δ" "dfun"
annD = hl Delim . text =<< ifUnicode "∷" "::"
natD = hl Syntax . text =<< ifUnicode "ℕ" "Nat"
stringD = hl Syntax $ text "String"
eqD = hl Syntax $ text "Eq"
colonD = hl Delim $ text ":"
commaD = hl Delim $ text ","
@ -329,3 +331,13 @@ prettyLoc (L (YesLoc file b)) =
export
prettyTag : {opts : _} -> String -> Eff Pretty (Doc opts)
prettyTag tag = hl Tag $ text $ "'" ++ quoteTag tag
export
prettyStrLit : {opts : _} -> String -> Eff Pretty (Doc opts)
prettyStrLit s =
let s = concatMap esc1 $ unpack s in
hl Syntax $ hcat ["\"", text s, "\""]
where
esc1 : Char -> String
esc1 '"' = "\""; esc1 '\\' = "\\"
esc1 c = singleton c

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

@ -61,6 +61,10 @@ mutual
||| type of types
TYPE : (l : Universe) -> (loc : Loc) -> Term d n
||| IO state token. this is a builtin because otherwise #[main] being a
||| builtin makes no sense
IOState : (loc : Loc) -> Term d n
||| function type
Pi : (qty : Qty) -> (arg : Term d n) ->
(res : ScopeTerm d n) -> (loc : Loc) -> Term d n
@ -88,6 +92,10 @@ mutual
Zero : (loc : Loc) -> Term d n
Succ : (p : Term d n) -> (loc : Loc) -> Term d n
||| strings
STRING : (loc : Loc) -> Term d n
Str : (str : String) -> (loc : Loc) -> Term d n
||| "box" (package a value up with a certain quantity)
BOX : (qty : Qty) -> (ty : Term d n) -> (loc : Loc) -> Term d n
Box : (val : Term d n) -> (loc : Loc) -> Term d n
@ -361,6 +369,7 @@ Located (Elim d n) where
export
Located (Term d n) where
(TYPE _ loc).loc = loc
(IOState loc).loc = loc
(Pi _ _ _ loc).loc = loc
(Lam _ loc).loc = loc
(Sig _ _ loc).loc = loc
@ -371,6 +380,8 @@ Located (Term d n) where
(DLam _ loc).loc = loc
(Nat loc).loc = loc
(Zero loc).loc = loc
(STRING loc).loc = loc
(Str _ loc).loc = loc
(Succ _ loc).loc = loc
(BOX _ _ loc).loc = loc
(Box _ loc).loc = loc
@ -421,6 +432,7 @@ Relocatable (Elim d n) where
export
Relocatable (Term d n) where
setLoc loc (TYPE l _) = TYPE l loc
setLoc loc (IOState _) = IOState loc
setLoc loc (Pi qty arg res _) = Pi qty arg res loc
setLoc loc (Lam body _) = Lam body loc
setLoc loc (Sig fst snd _) = Sig fst snd loc
@ -432,6 +444,8 @@ Relocatable (Term d n) where
setLoc loc (Nat _) = Nat loc
setLoc loc (Zero _) = Zero loc
setLoc loc (Succ p _) = Succ p loc
setLoc loc (STRING _) = STRING loc
setLoc loc (Str s _) = Str s loc
setLoc loc (BOX qty ty _) = BOX qty ty loc
setLoc loc (Box val _) = Box val loc
setLoc loc (E e) = E $ setLoc loc e

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

@ -343,6 +343,7 @@ prettyTyCasePat : {opts : _} ->
(k : TyConKind) -> BContext (arity k) ->
Eff Pretty (Doc opts)
prettyTyCasePat KTYPE [<] = typeD
prettyTyCasePat KIOState [<] = ioStateD
prettyTyCasePat KPi [< a, b] =
parens . hsep =<< sequence [prettyTBind a, arrowD, prettyTBind b]
prettyTyCasePat KSig [< a, b] =
@ -351,6 +352,7 @@ prettyTyCasePat KEnum [<] = hl Syntax $ text "{}"
prettyTyCasePat KEq [< a0, a1, a, l, r] =
hsep <$> sequence (eqD :: map prettyTBind [a0, a1, a, l, r])
prettyTyCasePat KNat [<] = natD
prettyTyCasePat KString [<] = stringD
prettyTyCasePat KBOX [< a] = bracks =<< prettyTBind a
@ -392,6 +394,9 @@ prettyTerm dnames tnames (TYPE l _) =
pure $ hcat [star, level]
Ascii => [|hl Syntax "Type" <++> hl Universe (text $ show l)|]
prettyTerm dnames tnames (IOState _) =
ioStateD
prettyTerm dnames tnames (Pi qty arg res _) =
parensIfM Outer =<< do
let MkSplitPi {binds, cod} = splitPi [< (qty, res.name, arg)] res.term
@ -459,6 +464,9 @@ prettyTerm dnames tnames (Succ p _) = do
prettyTerm dnames tnames $ assert_smaller s s'
either succ (hl Syntax . text . show . S) =<< toNat p
prettyTerm dnames tnames (STRING _) = stringD
prettyTerm dnames tnames (Str s _) = prettyStrLit s
prettyTerm dnames tnames (BOX qty ty _) =
bracks . hcat =<<
sequence [prettyQty qty, dotD,

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

@ -254,6 +254,8 @@ mutual
PushSubsts Term Subst.isCloT where
pushSubstsWith th ph (TYPE l loc) =
nclo $ TYPE l loc
pushSubstsWith th ph (IOState loc) =
nclo $ IOState loc
pushSubstsWith th ph (Pi qty a body loc) =
nclo $ Pi qty (a // th // ph) (body // th // ph) loc
pushSubstsWith th ph (Lam body loc) =
@ -276,6 +278,10 @@ mutual
nclo $ Zero loc
pushSubstsWith th ph (Succ n loc) =
nclo $ Succ (n // th // ph) loc
pushSubstsWith _ _ (STRING loc) =
nclo $ STRING loc
pushSubstsWith _ _ (Str s loc) =
nclo $ Str s loc
pushSubstsWith th ph (BOX pi ty loc) =
nclo $ BOX pi (ty // th // ph) loc
pushSubstsWith th ph (Box val loc) =

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

@ -44,6 +44,7 @@ mutual
tightenT' : OPE n1 n2 -> (t : Term d n2) -> (0 nt : NotClo t) =>
Maybe (Term d n1)
tightenT' p (TYPE l loc) = pure $ TYPE l loc
tightenT' p (IOState loc) = pure $ IOState loc
tightenT' p (Pi qty arg res loc) =
Pi qty <$> tightenT p arg <*> tightenS p res <*> pure loc
tightenT' p (Lam body loc) =
@ -66,6 +67,10 @@ mutual
pure $ Zero loc
tightenT' p (Succ s loc) =
Succ <$> tightenT p s <*> pure loc
tightenT' p (STRING loc) =
pure $ STRING loc
tightenT' p (Str s loc) =
pure $ Str s loc
tightenT' p (BOX qty ty loc) =
BOX qty <$> tightenT p ty <*> pure loc
tightenT' p (Box val loc) =
@ -163,6 +168,8 @@ mutual
Maybe (Term d1 n)
dtightenT' p (TYPE l loc) =
pure $ TYPE l loc
dtightenT' p (IOState loc) =
pure $ IOState loc
dtightenT' p (Pi qty arg res loc) =
Pi qty <$> dtightenT p arg <*> dtightenS p res <*> pure loc
dtightenT' p (Lam body loc) =
@ -185,6 +192,10 @@ mutual
pure $ Zero loc
dtightenT' p (Succ s loc) =
Succ <$> dtightenT p s <*> pure loc
dtightenT' p (STRING loc) =
pure $ STRING loc
dtightenT' p (Str s loc) =
pure $ Str s loc
dtightenT' p (BOX qty ty loc) =
BOX qty <$> dtightenT p ty <*> pure loc
dtightenT' p (Box val loc) =

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

@ -9,7 +9,8 @@ import Generics.Derive
public export
data TyConKind = KTYPE | KPi | KSig | KEnum | KEq | KNat | KBOX
data TyConKind =
KTYPE | KIOState | KPi | KSig | KEnum | KEq | KNat | KString | KBOX
%name TyConKind k
%runElab derive "TyConKind" [Eq.Eq, Ord.Ord, Show.Show, Generic, Meta, DecEq]
@ -25,10 +26,12 @@ allKinds = %runElab do
||| in `type-case`, how many variables are bound in this branch
public export %inline
arity : TyConKind -> Nat
arity KTYPE = 0
arity KPi = 2
arity KSig = 2
arity KEnum = 0
arity KEq = 5
arity KNat = 0
arity KBOX = 1
arity KTYPE = 0
arity KIOState = 0
arity KPi = 2
arity KSig = 2
arity KEnum = 0
arity KEq = 5
arity KNat = 0
arity KString = 0
arity KBOX = 1

43
lib/Quox/Typechecker.idr
View file

@ -41,34 +41,6 @@ lubs ctx [] = zeroFor ctx
lubs ctx (x :: xs) = lubs1 $ x ::: xs
export
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)]
KEnum => [<]
-- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
KEq =>
let [< a0, a1, a, l, r] = xs in
[< (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)]
mutual
||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
|||
@ -164,6 +136,8 @@ mutual
check' ctx sg t@(TYPE {}) ty = toCheckType ctx sg t ty
check' ctx sg t@(IOState {}) ty = toCheckType ctx sg t ty
check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
check' ctx sg (Lam body loc) ty = do
@ -224,6 +198,12 @@ mutual
expectNat !(askAt DEFS) ctx SZero ty.loc ty
checkC ctx sg n ty
check' ctx sg t@(STRING {}) ty = toCheckType ctx sg t ty
check' ctx sg t@(Str s {}) ty = do
expectSTRING !(askAt DEFS) ctx SZero ty.loc ty
pure $ zeroFor ctx
check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
check' ctx sg (Box val loc) ty = do
@ -252,6 +232,9 @@ mutual
Just l => unless (k < l) $ throw $ BadUniverse loc k l
Nothing => pure ()
checkType' ctx (IOState loc) u = pure ()
-- Ψ | Γ ⊢₀ IOState ⇒ Type ℓ
checkType' ctx (Pi qty arg res _) u = do
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
checkTypeC ctx arg u
@ -296,6 +279,10 @@ mutual
checkType' ctx t@(Zero {}) u = throw $ NotType t.loc ctx t
checkType' ctx t@(Succ {}) u = throw $ NotType t.loc ctx t
checkType' ctx (STRING loc) u = pure ()
-- Ψ | Γ ⊢₀ STRING ⇒ Type ℓ
checkType' ctx t@(Str {}) u = throw $ NotType t.loc ctx t
checkType' ctx (BOX q ty _) u = checkType ctx ty u
checkType' ctx t@(Box {}) u = throw $ NotType t.loc ctx t

8
lib/Quox/Typing.idr
View file

@ -107,6 +107,10 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
expectNat : Term d n -> Eff fs ()
expectNat = expect ExpectedNat `(Nat {}) `(())
export covering %inline
expectSTRING : Term d n -> Eff fs ()
expectSTRING = expect ExpectedSTRING `(STRING {}) `(())
export covering %inline
expectBOX : Term d n -> Eff fs (Qty, Term d n)
expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
@ -154,6 +158,10 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
expectNat : Term 0 n -> Eff fs ()
expectNat = expect ExpectedNat `(Nat {}) `(())
export covering %inline
expectSTRING : Term 0 n -> Eff fs ()
expectSTRING = expect ExpectedSTRING `(STRING {}) `(())
export covering %inline
expectBOX : Term 0 n -> Eff fs (Qty, Term 0 n)
expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))

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

@ -62,17 +62,18 @@ namespace WhnfContext
public export
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)
| ExpectedEnum Loc (NameContexts d n) (Term d n)
| ExpectedEq Loc (NameContexts d n) (Term d n)
| ExpectedNat Loc (NameContexts d n) (Term d n)
| ExpectedBOX Loc (NameContexts d n) (Term d n)
| BadUniverse Loc Universe Universe
| TagNotIn Loc TagVal (SortedSet TagVal)
| BadCaseEnum Loc (SortedSet TagVal) (SortedSet TagVal)
| BadQtys Loc String (TyContext d n) (List (QOutput n, Term d n))
= ExpectedTYPE Loc (NameContexts d n) (Term d n)
| ExpectedPi Loc (NameContexts d n) (Term d n)
| ExpectedSig 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)
| ExpectedSTRING Loc (NameContexts d n) (Term d n)
| ExpectedBOX Loc (NameContexts d n) (Term d n)
| BadUniverse Loc Universe Universe
| TagNotIn Loc TagVal (SortedSet TagVal)
| BadCaseEnum Loc (SortedSet TagVal) (SortedSet TagVal)
| BadQtys Loc String (TyContext d n) (List (QOutput n, Term d n))
-- first term arg of ClashT is the type
| ClashT Loc (EqContext n) EqMode (Term 0 n) (Term 0 n) (Term 0 n)
@ -127,6 +128,7 @@ Located Error where
(ExpectedEnum loc _ _).loc = loc
(ExpectedEq loc _ _).loc = loc
(ExpectedNat loc _ _).loc = loc
(ExpectedSTRING loc _ _).loc = loc
(ExpectedBOX loc _ _).loc = loc
(BadUniverse loc _ _).loc = loc
(TagNotIn loc _ _).loc = loc
@ -294,6 +296,12 @@ parameters {opts : LayoutOpts} (showContext : Bool)
!(prettyTerm [<] [<] $ Nat noLoc) <+> ", but got")
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedSTRING _ ctx s =>
hangDSingle
("expected the type" <++>
!(prettyTerm [<] [<] $ STRING noLoc) <+> ", but got")
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedBOX _ ctx s =>
hangDSingle "expected a box type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)

14
lib/Quox/Untyped/Erase.idr
View file

@ -135,6 +135,9 @@ eraseElim : ErasureContext d n -> (tm : Q.Elim d n) ->
eraseTerm ctx _ s@(TYPE {}) =
throw $ CompileTimeOnly ctx s
eraseTerm ctx _ s@(IOState {}) =
throw $ CompileTimeOnly ctx s
eraseTerm ctx _ s@(Pi {}) =
throw $ CompileTimeOnly ctx s
@ -197,6 +200,13 @@ eraseTerm ctx ty (Succ p loc) = do
p <- eraseTerm ctx ty p
pure $ Succ p loc
eraseTerm ctx ty s@(STRING {}) =
throw $ CompileTimeOnly ctx s
-- s ⤋ s ⇐ String
eraseTerm _ _ (Str s loc) =
pure $ Str s loc
eraseTerm ctx ty s@(BOX {}) =
throw $ CompileTimeOnly ctx s
@ -428,7 +438,7 @@ eraseElim ctx (DCloE (Sub term th)) =
export
uses : Var n -> Term n -> Nat
uses i (F x _) = 0
uses i (F _ _) = 0
uses i (B j _) = if i == j then 1 else 0
uses i (Lam x body _) = uses (VS i) body
uses i (App fun arg _) = uses i fun + uses i arg
@ -445,6 +455,7 @@ uses i (CaseNat nat zer suc _) = uses i nat + max (uses i zer) (uses' suc)
where uses' : CaseNatSuc n -> Nat
uses' (NSRec _ _ s) = uses (VS (VS i)) s
uses' (NSNonrec _ s) = uses (VS i) s
uses i (Str _ _) = 0
uses i (Let x rhs body _) = uses i rhs + uses (VS i) body
uses i (Erased _) = 0
@ -478,6 +489,7 @@ trimLets (CaseNat nat zer suc loc) =
where trimLets' : CaseNatSuc n -> CaseNatSuc n
trimLets' (NSRec x ih s) = NSRec x ih $ trimLets s
trimLets' (NSNonrec x s) = NSNonrec x $ trimLets s
trimLets (Str s loc) = Str s loc
trimLets (Let x rhs body loc) =
let rhs' = trimLets rhs
body' = trimLets body in

38
lib/Quox/Untyped/Scheme.idr
View file

@ -94,6 +94,7 @@ data Sexp =
| L (List Sexp)
| Q Sexp
| N Nat
| S String
| Lambda (List Id) Sexp
| LambdaC (List Id) Sexp -- curried lambda
| Let Id Sexp Sexp
@ -162,16 +163,16 @@ freshInBC = freshInBT
export covering
toScheme : Context' Id n -> Term n -> Eff Scheme Sexp
toScheme xs (F x loc) = pure $ V $ makeId x
toScheme xs (F x _) = pure $ V $ makeId x
toScheme xs (B i loc) = pure $ V $ xs !!! i
toScheme xs (B i _) = pure $ V $ xs !!! i
toScheme xs (Lam x body loc) =
toScheme xs (Lam x body _) =
let Evidence n' (ys, body) = splitLam [< x] body in
freshInBT ys $ \ys => do
pure $ LambdaC (toList' ys) !(toScheme (xs . ys) body)
toScheme xs (App fun arg loc) = do
toScheme xs (App fun arg _) = do
let (fun, args) = splitApp fun
fun <- toScheme xs fun
args <- traverse (toScheme xs) args
@ -180,34 +181,34 @@ toScheme xs (App fun arg loc) = do
then L [fun, arg]
else L $ "%" :: fun :: toList (args :< arg)
toScheme xs (Pair fst snd loc) =
toScheme xs (Pair fst snd _) =
pure $ L ["cons", !(toScheme xs fst), !(toScheme xs snd)]
toScheme xs (Fst pair loc) =
toScheme xs (Fst pair _) =
pure $ L ["car", !(toScheme xs pair)]
toScheme xs (Snd pair loc) =
toScheme xs (Snd pair _) =
pure $ L ["cdr", !(toScheme xs pair)]
toScheme xs (Tag tag loc) =
toScheme xs (Tag tag _) =
pure $ Q $ fromString tag
toScheme xs (CaseEnum tag cases loc) =
toScheme xs (CaseEnum tag cases _) =
Case <$> toScheme xs tag
<*> for cases (\(t, rhs) => ([fromString t],) <$> toScheme xs rhs)
toScheme xs (Absurd loc) =
toScheme xs (Absurd _) =
pure $ Q "absurd"
toScheme xs (Zero loc) =
toScheme xs (Zero _) =
pure $ N 0
toScheme xs (Succ nat loc) =
toScheme xs (Succ nat _) =
case !(toScheme xs nat) of
N n => pure $ N $ S n
s => pure $ L ["+", s, N 1]
toScheme xs (CaseNat nat zer (NSRec p ih suc) loc) =
toScheme xs (CaseNat nat zer (NSRec p ih suc) _) =
freshInBC [< p, ih] $ \[< p, ih] =>
pure $
L ["case-nat-rec",
@ -215,7 +216,9 @@ toScheme xs (CaseNat nat zer (NSRec p ih suc) loc) =
Lambda [p, ih] !(toScheme (xs :< p :< ih) suc),
!(toScheme xs nat)]
toScheme xs (CaseNat nat zer (NSNonrec p suc) loc) =
toScheme xs (Str s _) = pure $ S s
toScheme xs (CaseNat nat zer (NSNonrec p suc) _) =
freshInB p $ \p =>
pure $
L ["case-nat-nonrec",
@ -223,11 +226,11 @@ toScheme xs (CaseNat nat zer (NSNonrec p suc) loc) =
Lambda [p] !(toScheme (xs :< p) suc),
!(toScheme xs nat)]
toScheme xs (Let x rhs body loc) =
toScheme xs (Let x rhs body _) =
freshInB x $ \x =>
pure $ Let x !(toScheme xs rhs) !(toScheme (xs :< x) body)
toScheme xs (Erased loc) =
toScheme xs (Erased _) =
pure $ Q "erased"
@ -317,7 +320,7 @@ prettyLet ps (Let x rhs body) = prettyLet (ps :< (x, rhs)) body
prettyLet ps e =
pure $ orIndent
(hsep [!(hl Syntax "let*"),
!(bracks . sep . toList =<< traverse prettyBind ps)])
!(bracks . vsep . toList =<< traverse prettyBind ps)])
!(prettySexp e)
private covering
@ -339,6 +342,7 @@ prettySexp (L (x :: xs)) = do
prettySexp (Q (V x)) = hl Tag $ "'" <+> prettyId' x
prettySexp (Q x) = pure $ hcat [!(hl Tag "'"), !(prettySexp x)]
prettySexp (N n) = hl Tag $ pshow n
prettySexp (S s) = prettyStrLit s
prettySexp (Lambda xs e) = prettyLambda "lambda" xs e
prettySexp (LambdaC xs e) = prettyLambda "lambda%" xs e
prettySexp (Let x rhs e) = prettyLet [< (x, rhs)] e

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

@ -47,6 +47,8 @@ data Term where
Loc ->
Term n
Str : (str : String) -> Loc -> Term n
Let : (x : BindName) -> (rhs : Term n) -> (body : Term (S n)) -> Loc ->
Term n
@ -77,6 +79,7 @@ Located (Term n) where
(Zero loc).loc = loc
(Succ _ loc).loc = loc
(CaseNat _ _ _ loc).loc = loc
(Str _ loc).loc = loc
(Let _ _ _ loc).loc = loc
(Erased loc).loc = loc
@ -233,6 +236,8 @@ prettyTerm xs (Succ nat _) =
Right doc => prettyApp' !succD [< doc]
prettyTerm xs (CaseNat nat zer suc _) =
prettyCase xs pure nat [MkPrettyCaseArm !zeroD [] zer, !(sucCaseArm suc)]
prettyTerm xs (Str s _) =
prettyStrLit s
prettyTerm xs (Let x rhs body _) =
parensIfM Outer =<< do
let Evidence n' (lets, body) = splitLet [< (x, rhs)] body
@ -300,6 +305,8 @@ CanSubstSelf Term where
CaseNat nat zer suc loc =>
CaseNat (nat // th) (zer // th)
(assert_total substSuc suc th) loc
Str s loc =>
Str s loc
Let x rhs body loc =>
Let x (rhs // th) (assert_total $ body // push th) loc
Erased loc =>

8
lib/Quox/Whnf/Coercion.idr
View file

@ -158,6 +158,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
TYPE l tyLoc =>
whnf defs ctx sg $ Ann s (TYPE l tyLoc) loc
-- (coe IOState @_ @_ s) ⇝ (s ∷ IOState)
IOState tyLoc =>
whnf defs ctx sg $ Ann s (IOState tyLoc) loc
-- η expand it so that whnf for App can deal with it
--
-- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s)
@ -210,6 +214,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
Nat tyLoc =>
whnf defs ctx sg $ Ann s (Nat tyLoc) loc
-- (coe String @_ @_ s) ⇝ (s ∷ String)
STRING tyLoc =>
whnf defs ctx sg $ Ann s (STRING tyLoc) loc
-- η expand
--
-- (coe (𝑖 ⇒ [π. A]) @p @q s)

76
lib/Quox/Whnf/Interface.idr
View file

@ -111,23 +111,26 @@ isAnn _ = False
||| a syntactic type
public export %inline
isTyCon : Term {} -> Bool
isTyCon (TYPE {}) = True
isTyCon (Pi {}) = True
isTyCon (Lam {}) = False
isTyCon (Sig {}) = True
isTyCon (Pair {}) = False
isTyCon (Enum {}) = True
isTyCon (Tag {}) = False
isTyCon (Eq {}) = True
isTyCon (DLam {}) = False
isTyCon (Nat {}) = True
isTyCon (Zero {}) = False
isTyCon (Succ {}) = False
isTyCon (BOX {}) = True
isTyCon (Box {}) = False
isTyCon (E {}) = False
isTyCon (CloT {}) = False
isTyCon (DCloT {}) = False
isTyCon (TYPE {}) = True
isTyCon (IOState {}) = True
isTyCon (Pi {}) = True
isTyCon (Lam {}) = False
isTyCon (Sig {}) = True
isTyCon (Pair {}) = False
isTyCon (Enum {}) = True
isTyCon (Tag {}) = False
isTyCon (Eq {}) = True
isTyCon (DLam {}) = False
isTyCon (Nat {}) = True
isTyCon (Zero {}) = False
isTyCon (Succ {}) = False
isTyCon (STRING {}) = True
isTyCon (Str {}) = False
isTyCon (BOX {}) = True
isTyCon (Box {}) = False
isTyCon (E {}) = False
isTyCon (CloT {}) = False
isTyCon (DCloT {}) = False
||| a syntactic type, or a neutral
public export %inline
@ -154,24 +157,27 @@ isK _ = False
||| - `val` is a constructor form
public export %inline
canPushCoe : SQty -> (ty, val : Term {}) -> Bool
canPushCoe sg (TYPE {}) _ = True
canPushCoe sg (Pi {}) _ = True
canPushCoe sg (Lam {}) _ = False
canPushCoe sg (Sig {}) (Pair {}) = True
canPushCoe sg (Sig {}) _ = False
canPushCoe sg (Pair {}) _ = False
canPushCoe sg (Enum {}) _ = True
canPushCoe sg (Tag {}) _ = False
canPushCoe sg (Eq {}) _ = True
canPushCoe sg (DLam {}) _ = False
canPushCoe sg (Nat {}) _ = True
canPushCoe sg (Zero {}) _ = False
canPushCoe sg (Succ {}) _ = False
canPushCoe sg (BOX {}) _ = True
canPushCoe sg (Box {}) _ = False
canPushCoe sg (E {}) _ = False
canPushCoe sg (CloT {}) _ = False
canPushCoe sg (DCloT {}) _ = False
canPushCoe sg (TYPE {}) _ = True
canPushCoe sg (IOState {}) _ = True
canPushCoe sg (Pi {}) _ = True
canPushCoe sg (Lam {}) _ = False
canPushCoe sg (Sig {}) (Pair {}) = True
canPushCoe sg (Sig {}) _ = False
canPushCoe sg (Pair {}) _ = False
canPushCoe sg (Enum {}) _ = True
canPushCoe sg (Tag {}) _ = False
canPushCoe sg (Eq {}) _ = True
canPushCoe sg (DLam {}) _ = False
canPushCoe sg (Nat {}) _ = True
canPushCoe sg (Zero {}) _ = False
canPushCoe sg (Succ {}) _ = False
canPushCoe sg (STRING {}) _ = True
canPushCoe sg (Str {}) _ = False
canPushCoe sg (BOX {}) _ = True
canPushCoe sg (Box {}) _ = False
canPushCoe sg (E {}) _ = False
canPushCoe sg (CloT {}) _ = False
canPushCoe sg (DCloT {}) _ = False
mutual

31
lib/Quox/Whnf/Main.idr
View file

@ -225,20 +225,23 @@ CanWhnf Elim Interface.isRedexE where
covering
CanWhnf Term Interface.isRedexT where
whnf _ _ _ t@(TYPE {}) = pure $ nred t
whnf _ _ _ t@(Pi {}) = pure $ nred t
whnf _ _ _ t@(Lam {}) = pure $ nred t
whnf _ _ _ t@(Sig {}) = pure $ nred t
whnf _ _ _ t@(Pair {}) = pure $ nred t
whnf _ _ _ t@(Enum {}) = pure $ nred t
whnf _ _ _ t@(Tag {}) = pure $ nred t
whnf _ _ _ t@(Eq {}) = pure $ nred t
whnf _ _ _ t@(DLam {}) = pure $ nred t
whnf _ _ _ t@(Nat {}) = pure $ nred t
whnf _ _ _ t@(Zero {}) = pure $ nred t
whnf _ _ _ t@(Succ {}) = pure $ nred t
whnf _ _ _ t@(BOX {}) = pure $ nred t
whnf _ _ _ t@(Box {}) = pure $ nred t
whnf _ _ _ t@(TYPE {}) = pure $ nred t
whnf _ _ _ t@(IOState {}) = pure $ nred t
whnf _ _ _ t@(Pi {}) = pure $ nred t
whnf _ _ _ t@(Lam {}) = pure $ nred t
whnf _ _ _ t@(Sig {}) = pure $ nred t
whnf _ _ _ t@(Pair {}) = pure $ nred t
whnf _ _ _ t@(Enum {}) = pure $ nred t
whnf _ _ _ t@(Tag {}) = pure $ nred t
whnf _ _ _ t@(Eq {}) = pure $ nred t
whnf _ _ _ t@(DLam {}) = pure $ nred t
whnf _ _ _ t@(Nat {}) = pure $ nred t
whnf _ _ _ t@(Zero {}) = pure $ nred t
whnf _ _ _ t@(Succ {}) = pure $ nred t
whnf _ _ _ t@(STRING {}) = pure $ nred t
whnf _ _ _ t@(Str {}) = pure $ nred t
whnf _ _ _ t@(BOX {}) = pure $ nred t
whnf _ _ _ t@(Box {}) = pure $ nred t
-- s ∷ A ⇝ s (in term context)
whnf defs ctx sg (E e) = do

9
lib/Quox/Whnf/TypeCase.idr
View file

@ -99,7 +99,6 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
pure (a0, a1, a, l, r)
tycaseEq t = throw $ ExpectedEq t.loc ctx.names t
||| reduce a type-case applied to a type constructor
|||
||| `reduceTypeCase A i Q arms def _` reduces an expression
@ -114,6 +113,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
TYPE {} =>
whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KTYPE arms) ret loc
-- (type-case IOState ∷ _ return Q of { IOState ⇒ s; ⋯ }) ⇝ s ∷ Q
IOState {} =>
whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KIOState arms) ret loc
-- (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, _} =>
@ -156,6 +159,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
Nat {} =>
whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KNat arms) ret loc
-- (type-case String ∷ _ return Q of { String ⇒ s; ⋯ }) ⇝ s ∷ Q
STRING {} =>
whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KString arms) ret loc
-- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
BOX {ty = a, loc = boxLoc, _} =>
whnf defs ctx SZero $ Ann

10
tests/AstExtra.idr
View file

@ -31,3 +31,13 @@ ctx tel = let (ns, ts) = unzip tel in
MkTyContext new [<] ts ns anys
ctx01 tel = let (ns, ts) = unzip tel in
MkTyContext ZeroIsOne [<] ts ns anys
export
mkDef : GQty -> Term 0 0 -> Term 0 0 -> Definition
mkDef q ty tm = Definition.mkDef q ty tm Nothing False noLoc
%hide Definition.mkDef
export
mkPostulate : GQty -> Term 0 0 -> Definition
mkPostulate q ty = Definition.mkPostulate q ty Nothing False noLoc
%hide Definition.mkPostulate

55
tests/Tests/Equal.idr
View file

@ -9,18 +9,17 @@ import Quox.EffExtra
import AstExtra
defGlobals : Definitions
defGlobals = fromList
[("A", ^mkPostulate GZero (^TYPE 0)),
("B", ^mkPostulate GZero (^TYPE 0)),
("a", ^mkPostulate GAny (^FT "A" 0)),
("a'", ^mkPostulate GAny (^FT "A" 0)),
("b", ^mkPostulate GAny (^FT "B" 0)),
("f", ^mkPostulate GAny (^Arr One (^FT "A" 0) (^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))))]
[("A", mkPostulate GZero (^TYPE 0)),
("B", mkPostulate GZero (^TYPE 0)),
("a", mkPostulate GAny (^FT "A" 0)),
("a'", mkPostulate GAny (^FT "A" 0)),
("b", mkPostulate GAny (^FT "B" 0)),
("f", mkPostulate GAny (^Arr One (^FT "A" 0) (^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))))]
parameters (label : String) (act : Eff Equal ())
{default defGlobals globals : Definitions}
@ -156,7 +155,7 @@ tests = "equality & subtyping" :- [
let tm = ^Eq0 (^TYPE 1) (^TYPE 0) (^TYPE 0) in
equalT empty (^TYPE 2) tm tm,
testEq "A ≔ ★₁ ⊢ (★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : A)"
{globals = fromList [("A", ^mkDef GZero (^TYPE 2) (^TYPE 1))]} $
{globals = fromList [("A", mkDef GZero (^TYPE 2) (^TYPE 1))]} $
equalT empty (^TYPE 2)
(^Eq0 (^TYPE 1) (^TYPE 0) (^TYPE 0))
(^Eq0 (^FT "A" 0) (^TYPE 0) (^TYPE 0)),
@ -176,7 +175,7 @@ tests = "equality & subtyping" :- [
testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q (free)"
{globals =
let def = ^mkPostulate GZero
let def = mkPostulate GZero
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))
in defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
equalE empty (^F "p" 0) (^F "q" 0),
@ -195,32 +194,32 @@ tests = "equality & subtyping" :- [
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef GZero (^TYPE 0)
[("E", mkDef GZero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
("EE", ^mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
("EE", mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
equalE
(extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "EE" 0)] empty)
(^BV 0) (^BV 1),
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef GZero (^TYPE 0)
[("E", mkDef GZero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
("EE", ^mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
("EE", mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
equalE
(extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "E" 0)] empty)
(^BV 0) (^BV 1),
testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef GZero (^TYPE 0)
[("E", mkDef GZero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
equalE (extendTyN [< (Any, "x", ^FT "E" 0), (Any, "y", ^FT "E" 0)] empty)
(^BV 0) (^BV 1),
testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef GZero (^TYPE 0)
[("E", mkDef GZero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
let ty : forall n. Term 0 n := ^Sig (^FT "E" 0) (SN $ ^FT "E" 0) in
equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
@ -228,9 +227,9 @@ tests = "equality & subtyping" :- [
testEq "E ≔ a ≡ a' : A, W ≔ E × E ∥ x : W, y : E×E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef GZero (^TYPE 0)
[("E", mkDef GZero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
("W", ^mkDef GZero (^TYPE 0) (^And (^FT "E" 0) (^FT "E" 0)))]} $
("W", mkDef GZero (^TYPE 0) (^And (^FT "E" 0) (^FT "E" 0)))]} $
equalE
(extendTyN [< (Any, "x", ^FT "W" 0),
(Any, "y", ^And (^FT "E" 0) (^FT "E" 0))] empty)
@ -280,11 +279,11 @@ tests = "equality & subtyping" :- [
"free var" :-
let au_bu = fromList
[("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", ^mkDef GAny (^TYPE 1) (^TYPE 0))]
[("A", mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", mkDef GAny (^TYPE 1) (^TYPE 0))]
au_ba = fromList
[("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", ^mkDef GAny (^TYPE 1) (^FT "A" 0))]
[("A", mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", mkDef GAny (^TYPE 1) (^FT "A" 0))]
in [
testEq "A = A" $
equalE empty (^F "A" 0) (^F "A" 0),
@ -305,13 +304,13 @@ tests = "equality & subtyping" :- [
testNeq "A ≮: B" $
subE empty (^F "A" 0) (^F "B" 0),
testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
{globals = fromList [("A", ^mkDef GAny (^TYPE 3) (^TYPE 0)),
("B", ^mkDef GAny (^TYPE 3) (^TYPE 2))]} $
{globals = fromList [("A", mkDef GAny (^TYPE 3) (^TYPE 0)),
("B", mkDef GAny (^TYPE 3) (^TYPE 2))]} $
subE empty (^F "A" 0) (^F "B" 0),
note "(A and B in different universes)",
testEq "A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
{globals = fromList [("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", ^mkDef GAny (^TYPE 3) (^TYPE 2))]} $
{globals = fromList [("A", mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", mkDef GAny (^TYPE 3) (^TYPE 2))]} $
subE empty (^F "A" 0) (^F "B" 0),
testEq "0=1 ⊢ A <: B" $
subE empty01 (^F "A" 0) (^F "B" 0)

2
tests/Tests/FromPTerm.idr
View file

@ -85,7 +85,7 @@ tests = "PTerm → Term" :- [
],
"terms" :-
let defs = fromList [("f", mkDef GAny (Nat noLoc) (Zero noLoc) noLoc)]
let defs = fromList [("f", mkDef GAny (^Nat) (^Zero))]
-- doesn't have to be well typed yet, just well scoped
fromPTerm = runFromParser {defs} .
fromPTermWith [< "𝑖", "𝑗"] [< "A", "x", "y", "z"]

4
tests/Tests/Parser.idr
View file

@ -64,8 +64,8 @@ tests = "parser" :- [
"names" :- [
parsesAs (const qname) "x"
(MakePName [<] "x"),
parsesAs (const qname) "Data.String.length"
(MakePName [< "Data", "String"] "length"),
parsesAs (const qname) "Data.List.length"
(MakePName [< "Data", "List"] "length"),
parseFails (const qname) "_"
],

4
tests/Tests/Reduce.idr
View file

@ -73,10 +73,10 @@ tests = "whnf" :- [
"definitions" :- [
testWhnf "a (transparent)" empty
{defs = fromList [("a", ^mkDef GZero (^TYPE 1) (^TYPE 0))]}
{defs = fromList [("a", ^mkDef GZero (^TYPE 1) (^TYPE 0) Nothing False)]}
(^F "a" 0) (^Ann (^TYPE 0) (^TYPE 1)),
testNoStep "a (opaque)" empty
{defs = fromList [("a", ^mkPostulate GZero (^TYPE 1))]}
{defs = fromList [("a", ^mkPostulate GZero (^TYPE 1) Nothing False)]}
(^F "a" 0)
],

38
tests/Tests/Typechecker.idr
View file

@ -87,28 +87,28 @@ apps = foldl (\f, s => ^App f s)
defGlobals : Definitions
defGlobals = fromList
[("A", ^mkPostulate GZero (^TYPE 0)),
("B", ^mkPostulate GZero (^TYPE 0)),
("C", ^mkPostulate GZero (^TYPE 1)),
("D", ^mkPostulate GZero (^TYPE 1)),
("P", ^mkPostulate GZero (^Arr Any (^FT "A" 0) (^TYPE 0))),
("a", ^mkPostulate GAny (^FT "A" 0)),
("a'", ^mkPostulate GAny (^FT "A" 0)),
("b", ^mkPostulate GAny (^FT "B" 0)),
("c", ^mkPostulate GAny (^FT "C" 0)),
("d", ^mkPostulate GAny (^FT "D" 0)),
("f", ^mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "A" 0))),
("fω", ^mkPostulate GAny (^Arr Any (^FT "A" 0) (^FT "A" 0))),
("g", ^mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "B" 0))),
("f2", ^mkPostulate GAny
[("A", mkPostulate GZero (^TYPE 0)),
("B", mkPostulate GZero (^TYPE 0)),
("C", mkPostulate GZero (^TYPE 1)),
("D", mkPostulate GZero (^TYPE 1)),
("P", mkPostulate GZero (^Arr Any (^FT "A" 0) (^TYPE 0))),
("a", mkPostulate GAny (^FT "A" 0)),
("a'", mkPostulate GAny (^FT "A" 0)),
("b", mkPostulate GAny (^FT "B" 0)),
("c", mkPostulate GAny (^FT "C" 0)),
("d", mkPostulate GAny (^FT "D" 0)),
("f", mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "A" 0))),
("fω", mkPostulate GAny (^Arr Any (^FT "A" 0) (^FT "A" 0))),
("g", mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "B" 0))),
("f2", mkPostulate GAny
(^Arr One (^FT "A" 0) (^Arr One (^FT "A" 0) (^FT "B" 0)))),
("p", ^mkPostulate GAny
("p", mkPostulate GAny
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
("q", ^mkPostulate GAny
("q", mkPostulate GAny
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
("refl", ^mkDef GAny reflTy reflDef),
("fst", ^mkDef GAny fstTy fstDef),
("snd", ^mkDef GAny sndTy sndDef)]
("refl", mkDef GAny reflTy reflDef),
("fst", mkDef GAny fstTy fstDef),
("snd", mkDef GAny sndTy sndDef)]
parameters (label : String) (act : Lazy (Eff Test ()))
{default defGlobals globals : Definitions}