From e0ed37720f174c1d4e99a5f39d204b1416573df6 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 1 Nov 2023 15:17:15 +0100 Subject: [PATCH] always vsep scheme lets, otherwise they are unreadable --- lib/Quox/Displace.idr | 3 + lib/Quox/Equal.idr | 182 +++++++++++++++++------------ lib/Quox/FreeVars.idr | 74 ++++++------ lib/Quox/Parser/FromParser.idr | 6 + lib/Quox/Parser/Lexer.idr | 2 + lib/Quox/Parser/Parser.idr | 3 + lib/Quox/Parser/Syntax.idr | 54 +++++---- lib/Quox/Pretty.idr | 16 ++- lib/Quox/Syntax/Term/Base.idr | 14 +++ lib/Quox/Syntax/Term/Pretty.idr | 8 ++ lib/Quox/Syntax/Term/Subst.idr | 6 + lib/Quox/Syntax/Term/Tighten.idr | 11 ++ lib/Quox/Syntax/Term/TyConKind.idr | 19 +-- lib/Quox/Typechecker.idr | 43 +++---- lib/Quox/Typing.idr | 8 ++ lib/Quox/Typing/Error.idr | 30 +++-- lib/Quox/Untyped/Erase.idr | 14 ++- lib/Quox/Untyped/Scheme.idr | 38 +++--- lib/Quox/Untyped/Syntax.idr | 7 ++ lib/Quox/Whnf/Coercion.idr | 8 ++ lib/Quox/Whnf/Interface.idr | 76 ++++++------ lib/Quox/Whnf/Main.idr | 31 ++--- lib/Quox/Whnf/TypeCase.idr | 9 +- tests/AstExtra.idr | 10 ++ tests/Tests/Equal.idr | 55 +++++---- tests/Tests/FromPTerm.idr | 2 +- tests/Tests/Parser.idr | 4 +- tests/Tests/Reduce.idr | 4 +- tests/Tests/Typechecker.idr | 38 +++--- 29 files changed, 474 insertions(+), 301 deletions(-) diff --git a/lib/Quox/Displace.idr b/lib/Quox/Displace.idr index 8b8c07c..25353a1 100644 --- a/lib/Quox/Displace.idr +++ b/lib/Quox/Displace.idr @@ -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) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index bbaa6d5..29084a8 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -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) -> diff --git a/lib/Quox/FreeVars.idr b/lib/Quox/FreeVars.idr index ef8c42a..6b73d63 100644 --- a/lib/Quox/FreeVars.idr +++ b/lib/Quox/FreeVars.idr @@ -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 diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index e2f2444..ff2f97b 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -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 diff --git a/lib/Quox/Parser/Lexer.idr b/lib/Quox/Parser/Lexer.idr index 3db9736..8702aa2 100644 --- a/lib/Quox/Parser/Lexer.idr +++ b/lib/Quox/Parser/Lexer.idr @@ -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", diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index fb16aaf..043e691 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -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 diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr index 55cfc6a..1b60348 100644 --- a/lib/Quox/Parser/Syntax.idr +++ b/lib/Quox/Parser/Syntax.idr @@ -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 diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr index 73357ee..b2ab4b9 100644 --- a/lib/Quox/Pretty.idr +++ b/lib/Quox/Pretty.idr @@ -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 diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr index 43c97b3..810d8fe 100644 --- a/lib/Quox/Syntax/Term/Base.idr +++ b/lib/Quox/Syntax/Term/Base.idr @@ -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 diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index a14974c..4559235 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -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, diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr index 4aa3736..584c7b0 100644 --- a/lib/Quox/Syntax/Term/Subst.idr +++ b/lib/Quox/Syntax/Term/Subst.idr @@ -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) = diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr index 0f5a312..46d26c5 100644 --- a/lib/Quox/Syntax/Term/Tighten.idr +++ b/lib/Quox/Syntax/Term/Tighten.idr @@ -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) = diff --git a/lib/Quox/Syntax/Term/TyConKind.idr b/lib/Quox/Syntax/Term/TyConKind.idr index 6bacf77..298173e 100644 --- a/lib/Quox/Syntax/Term/TyConKind.idr +++ b/lib/Quox/Syntax/Term/TyConKind.idr @@ -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 diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index 563e6df..a0695f6 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -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 diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr index cfd402d..9f96291 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -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)) diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr index 1589612..3ac54ba 100644 --- a/lib/Quox/Typing/Error.idr +++ b/lib/Quox/Typing/Error.idr @@ -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) diff --git a/lib/Quox/Untyped/Erase.idr b/lib/Quox/Untyped/Erase.idr index 4161ecf..98505e9 100644 --- a/lib/Quox/Untyped/Erase.idr +++ b/lib/Quox/Untyped/Erase.idr @@ -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 diff --git a/lib/Quox/Untyped/Scheme.idr b/lib/Quox/Untyped/Scheme.idr index db69712..d0fd2de 100644 --- a/lib/Quox/Untyped/Scheme.idr +++ b/lib/Quox/Untyped/Scheme.idr @@ -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 diff --git a/lib/Quox/Untyped/Syntax.idr b/lib/Quox/Untyped/Syntax.idr index 2c4b1e0..0548293 100644 --- a/lib/Quox/Untyped/Syntax.idr +++ b/lib/Quox/Untyped/Syntax.idr @@ -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 => diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr index 7ee26cb..f70df4f 100644 --- a/lib/Quox/Whnf/Coercion.idr +++ b/lib/Quox/Whnf/Coercion.idr @@ -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) diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr index eebdcc9..bbd3f1b 100644 --- a/lib/Quox/Whnf/Interface.idr +++ b/lib/Quox/Whnf/Interface.idr @@ -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 diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr index 264c61a..ffb82b0 100644 --- a/lib/Quox/Whnf/Main.idr +++ b/lib/Quox/Whnf/Main.idr @@ -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 diff --git a/lib/Quox/Whnf/TypeCase.idr b/lib/Quox/Whnf/TypeCase.idr index 0c1f5e1..569a88d 100644 --- a/lib/Quox/Whnf/TypeCase.idr +++ b/lib/Quox/Whnf/TypeCase.idr @@ -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 diff --git a/tests/AstExtra.idr b/tests/AstExtra.idr index 2528d9a..f9cc1fd 100644 --- a/tests/AstExtra.idr +++ b/tests/AstExtra.idr @@ -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 diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index 3b0f212..818e7c2 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -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) diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr index bf8a947..b3451a9 100644 --- a/tests/Tests/FromPTerm.idr +++ b/tests/Tests/FromPTerm.idr @@ -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"] diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index 3884ff6..122be48 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -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) "_" ], diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr index a27c6f0..7e81a7a 100644 --- a/tests/Tests/Reduce.idr +++ b/tests/Tests/Reduce.idr @@ -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) ], diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr index 8a85815..1418643 100644 --- a/tests/Tests/Typechecker.idr +++ b/tests/Tests/Typechecker.idr @@ -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}