From fa7f82ae5a9f61af0302ee3c6c3e64ed786960ff Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 2 Nov 2023 18:14:22 +0100 Subject: [PATCH] rename Nat to NAT in AST --- lib/Quox/Displace.idr | 2 +- lib/Quox/Equal.idr | 16 +++++++-------- lib/Quox/FreeVars.idr | 4 ++-- lib/Quox/Parser/FromParser.idr | 2 +- lib/Quox/Parser/Parser.idr | 2 +- lib/Quox/Parser/Syntax.idr | 4 ++-- lib/Quox/Syntax/Term/Base.idr | 8 ++++---- lib/Quox/Syntax/Term/Pretty.idr | 2 +- lib/Quox/Syntax/Term/Subst.idr | 4 ++-- lib/Quox/Syntax/Term/Tighten.idr | 10 +++++----- lib/Quox/Typechecker.idr | 12 +++++------ lib/Quox/Typing.idr | 10 +++++----- lib/Quox/Typing/Error.idr | 8 ++++---- lib/Quox/Untyped/Erase.idr | 8 ++++---- lib/Quox/Whnf/Coercion.idr | 4 ++-- lib/Quox/Whnf/Interface.idr | 8 ++++---- lib/Quox/Whnf/Main.idr | 8 ++++---- lib/Quox/Whnf/TypeCase.idr | 2 +- tests/Tests/Equal.idr | 34 ++++++++++++++++---------------- tests/Tests/FromPTerm.idr | 2 +- tests/Tests/Parser.idr | 18 ++++++++--------- tests/Tests/PrettyTerm.idr | 2 +- tests/Tests/Reduce.idr | 12 +++++------ tests/Tests/Typechecker.idr | 2 +- 24 files changed, 92 insertions(+), 92 deletions(-) diff --git a/lib/Quox/Displace.idr b/lib/Quox/Displace.idr index 25353a1..14a3ce5 100644 --- a/lib/Quox/Displace.idr +++ b/lib/Quox/Displace.idr @@ -27,7 +27,7 @@ parameters (k : Universe) doDisplace (Eq ty l r loc) = Eq (doDisplaceDS ty) (doDisplace l) (doDisplace r) loc doDisplace (DLam body loc) = DLam (doDisplaceDS body) loc - doDisplace (Nat loc) = Nat loc + doDisplace (NAT loc) = NAT loc doDisplace (Zero loc) = Zero loc doDisplace (Succ p loc) = Succ (doDisplace p) loc doDisplace (STRING loc) = STRING loc diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 29084a8..33892c1 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -57,8 +57,8 @@ sameTyCon (Enum {}) (Enum {}) = True sameTyCon (Enum {}) _ = False sameTyCon (Eq {}) (Eq {}) = True sameTyCon (Eq {}) _ = False -sameTyCon (Nat {}) (Nat {}) = True -sameTyCon (Nat {}) _ = False +sameTyCon (NAT {}) (NAT {}) = True +sameTyCon (NAT {}) _ = False sameTyCon (STRING {}) (STRING {}) = True sameTyCon (STRING {}) _ = False sameTyCon (BOX {}) (BOX {}) = True @@ -90,7 +90,7 @@ isEmpty defs ctx sg ty0 = do Enum {cases, _} => pure $ null cases Eq {} => pure False - Nat {} => pure False + NAT {} => pure False STRING {} => pure False BOX {ty, _} => isEmpty defs ctx sg ty E _ => pure False @@ -124,7 +124,7 @@ isSubSing defs ctx sg ty0 = do Enum {cases, _} => pure $ length (SortedSet.toList cases) <= 1 Eq {} => pure True - Nat {} => pure False + NAT {} => pure False STRING {} => pure False BOX {ty, _} => isSubSing defs ctx sg ty E _ => pure False @@ -276,7 +276,7 @@ namespace Term -- Γ ⊢ e = f ⇐ Eq [i ⇒ A] s t pure () - compare0' defs ctx sg nat@(Nat {}) s t = local_ Equal $ + compare0' defs ctx sg nat@(NAT {}) s t = local_ Equal $ case (s, t) of -- --------------- -- Γ ⊢ 0 = 0 ⇐ ℕ @@ -403,7 +403,7 @@ compareType' defs ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do -- a runtime coercion unless (tags1 == tags2) $ clashTy s.loc ctx s t -compareType' defs ctx (Nat {}) (Nat {}) = +compareType' defs ctx (NAT {}) (NAT {}) = -- ------------ -- Γ ⊢ ℕ <: ℕ pure () @@ -626,10 +626,10 @@ namespace Elim try $ do compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term Term.compare0 defs ctx sg - (sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc)) + (sub1 eret (Ann (Zero ezer.loc) (NAT ezer.loc) ezer.loc)) ezer fzer Term.compare0 defs - (extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx) sg + (extendTyN [< (epi, p, NAT p.loc), (epi', ih, eret.term)] ctx) sg (substCaseSuccRet esuc.names eret) esuc.term fsuc.term expectEqualQ e.loc epi fpi expectEqualQ e.loc epi' fpi' diff --git a/lib/Quox/FreeVars.idr b/lib/Quox/FreeVars.idr index 6b73d63..929eb71 100644 --- a/lib/Quox/FreeVars.idr +++ b/lib/Quox/FreeVars.idr @@ -190,7 +190,7 @@ HasFreeVars (Term d) where fv (Tag {}) = none fv (Eq {ty, l, r, _}) = fvD ty <+> fv l <+> fv r fv (DLam {body, _}) = fvD body - fv (Nat {}) = none + fv (NAT {}) = none fv (Zero {}) = none fv (Succ {p, _}) = fv p fv (STRING {}) = none @@ -268,7 +268,7 @@ HasFreeDVars Term where 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 (NAT {}) = none fdv (Zero {}) = none fdv (Succ {p, _}) = fdv p fdv (STRING {}) = none diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index ff2f97b..0979915 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -188,7 +188,7 @@ mutual <*> assert_total fromPTermEnumArms loc ds ns arms <*> pure loc - Nat loc => pure $ Nat loc + NAT loc => pure $ NAT loc Zero loc => pure $ Zero loc Succ n loc => [|Succ (fromPTermWith ds ns n) (pure loc)|] diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index 043e691..b687cba 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -296,7 +296,7 @@ termArg fname = withLoc fname $ <|> [|Enum enumType|] <|> [|Tag tag|] <|> const <$> boxTerm fname - <|> Nat <$ res "ℕ" + <|> NAT <$ res "ℕ" <|> Zero <$ res "zero" <|> STRING <$ res "String" <|> [|Str strLit|] diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr index 1b60348..d6c13a6 100644 --- a/lib/Quox/Parser/Syntax.idr +++ b/lib/Quox/Parser/Syntax.idr @@ -85,7 +85,7 @@ namespace PTerm | DLam PatVar PTerm Loc | DApp PTerm PDim Loc - | Nat Loc + | NAT Loc | Zero Loc | Succ PTerm Loc | STRING Loc -- "String" is a reserved word in idris @@ -129,7 +129,7 @@ Located PTerm where (Eq _ _ _ loc).loc = loc (DLam _ _ loc).loc = loc (DApp _ _ loc).loc = loc - (Nat loc).loc = loc + (NAT loc).loc = loc (Zero loc).loc = loc (Succ _ loc).loc = loc (STRING loc).loc = loc diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr index 810d8fe..8ec1838 100644 --- a/lib/Quox/Syntax/Term/Base.idr +++ b/lib/Quox/Syntax/Term/Base.idr @@ -87,7 +87,7 @@ mutual DLam : (body : DScopeTerm d n) -> (loc : Loc) -> Term d n ||| natural numbers (temporary until 𝐖 gets added) - Nat : (loc : Loc) -> Term d n + NAT : (loc : Loc) -> Term d n -- [todo] can these be elims? Zero : (loc : Loc) -> Term d n Succ : (p : Term d n) -> (loc : Loc) -> Term d n @@ -342,7 +342,7 @@ public export %inline typeCase1Y : Elim d n -> Term d n -> (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) -> (loc : Loc) -> - {default (Nat loc) def : Term d n} -> + {default (NAT loc) def : Term d n} -> Elim d n typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc @@ -378,7 +378,7 @@ Located (Term d n) where (Tag _ loc).loc = loc (Eq _ _ _ loc).loc = loc (DLam _ loc).loc = loc - (Nat loc).loc = loc + (NAT loc).loc = loc (Zero loc).loc = loc (STRING loc).loc = loc (Str _ loc).loc = loc @@ -441,7 +441,7 @@ Relocatable (Term d n) where setLoc loc (Tag tag _) = Tag tag loc setLoc loc (Eq ty l r _) = Eq ty l r loc setLoc loc (DLam body _) = DLam body loc - setLoc loc (Nat _) = Nat loc + setLoc loc (NAT _) = NAT loc setLoc loc (Zero _) = Zero loc setLoc loc (Succ p _) = Succ p loc setLoc loc (STRING _) = STRING loc diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index 4559235..ecb5821 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -449,7 +449,7 @@ prettyTerm dnames tnames (Eq ty l r _) = prettyTerm dnames tnames s@(DLam {}) = prettyLambda dnames tnames s -prettyTerm dnames tnames (Nat _) = natD +prettyTerm dnames tnames (NAT _) = natD prettyTerm dnames tnames (Zero _) = hl Syntax "0" prettyTerm dnames tnames (Succ p _) = do succD <- succD diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr index 584c7b0..8610b78 100644 --- a/lib/Quox/Syntax/Term/Subst.idr +++ b/lib/Quox/Syntax/Term/Subst.idr @@ -272,8 +272,8 @@ mutual nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc pushSubstsWith th ph (DLam body loc) = nclo $ DLam (body // th // ph) loc - pushSubstsWith _ _ (Nat loc) = - nclo $ Nat loc + pushSubstsWith _ _ (NAT loc) = + nclo $ NAT loc pushSubstsWith _ _ (Zero loc) = nclo $ Zero loc pushSubstsWith th ph (Succ n loc) = diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr index 46d26c5..83ea7e0 100644 --- a/lib/Quox/Syntax/Term/Tighten.idr +++ b/lib/Quox/Syntax/Term/Tighten.idr @@ -61,8 +61,8 @@ mutual Eq <$> tightenDS p ty <*> tightenT p l <*> tightenT p r <*> pure loc tightenT' p (DLam body loc) = DLam <$> tightenDS p body <*> pure loc - tightenT' p (Nat loc) = - pure $ Nat loc + tightenT' p (NAT loc) = + pure $ NAT loc tightenT' p (Zero loc) = pure $ Zero loc tightenT' p (Succ s loc) = @@ -186,8 +186,8 @@ mutual Eq <$> dtightenDS p ty <*> dtightenT p l <*> dtightenT p r <*> pure loc dtightenT' p (DLam body loc) = DLam <$> dtightenDS p body <*> pure loc - dtightenT' p (Nat loc) = - pure $ Nat loc + dtightenT' p (NAT loc) = + pure $ NAT loc dtightenT' p (Zero loc) = pure $ Zero loc dtightenT' p (Succ s loc) = @@ -331,7 +331,7 @@ public export %inline typeCase1T : Elim d n -> Term d n -> (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) -> (loc : Loc) -> - {default (Nat loc) def : Term d n} -> + {default (NAT loc) def : Term d n} -> Elim d n typeCase1T ty ret k ns body loc {def} = typeCase ty ret [(k ** ST ns body)] def loc diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index a0695f6..2273a08 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -188,14 +188,14 @@ mutual -- then Ψ | Γ ⊢ σ · (δ i ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ pure qout - check' ctx sg t@(Nat {}) ty = toCheckType ctx sg t ty + check' ctx sg t@(NAT {}) ty = toCheckType ctx sg t ty check' ctx sg (Zero {}) ty = do - expectNat !(askAt DEFS) ctx SZero ty.loc ty + expectNAT !(askAt DEFS) ctx SZero ty.loc ty pure $ zeroFor ctx check' ctx sg (Succ n {}) ty = do - expectNat !(askAt DEFS) ctx SZero ty.loc ty + expectNAT !(askAt DEFS) ctx SZero ty.loc ty checkC ctx sg n ty check' ctx sg t@(STRING {}) ty = toCheckType ctx sg t ty @@ -275,7 +275,7 @@ mutual checkType' ctx t@(DLam {}) u = throw $ NotType t.loc ctx t - checkType' ctx (Nat {}) u = pure () + checkType' ctx (NAT {}) u = pure () checkType' ctx t@(Zero {}) u = throw $ NotType t.loc ctx t checkType' ctx t@(Succ {}) u = throw $ NotType t.loc ctx t @@ -415,7 +415,7 @@ mutual -- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn nres <- inferC ctx sg n let nat = nres.type - expectNat !(askAt DEFS) ctx SZero n.loc nat + expectNAT !(askAt DEFS) ctx SZero n.loc nat -- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing -- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz @@ -424,7 +424,7 @@ mutual -- with ρ₂ ≤ π'σ, (ρ₁ + ρ₂) ≤ πσ let [< p, ih] = suc.names pisg = pi * sg.qty - sucCtx = extendTyN [< (pisg, p, Nat p.loc), (pi', ih, ret.term)] ctx + sucCtx = extendTyN [< (pisg, p, NAT p.loc), (pi', ih, ret.term)] ctx sucType = substCaseSuccRet suc.names ret sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType expectCompatQ loc qih (pi' * sg.qty) diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr index 9f96291..31c059f 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -54,7 +54,7 @@ substCasePairRet [< x, y] dty retty = public export substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n) substCaseSuccRet [< p, ih] retty = - let arg = Ann (Succ (BVT 1 p.loc) p.loc) (Nat noLoc) $ p.loc `extendL` ih.loc + let arg = Ann (Succ (BVT 1 p.loc) p.loc) (NAT noLoc) $ p.loc `extendL` ih.loc in retty.term // (arg ::: shift 2) @@ -104,8 +104,8 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)} expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r)) export covering %inline - expectNat : Term d n -> Eff fs () - expectNat = expect ExpectedNat `(Nat {}) `(()) + expectNAT : Term d n -> Eff fs () + expectNAT = expect ExpectedNAT `(NAT {}) `(()) export covering %inline expectSTRING : Term d n -> Eff fs () @@ -155,8 +155,8 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)} expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r)) export covering %inline - expectNat : Term 0 n -> Eff fs () - expectNat = expect ExpectedNat `(Nat {}) `(()) + expectNAT : Term 0 n -> Eff fs () + expectNAT = expect ExpectedNAT `(NAT {}) `(()) export covering %inline expectSTRING : Term 0 n -> Eff fs () diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr index 3ac54ba..68683be 100644 --- a/lib/Quox/Typing/Error.idr +++ b/lib/Quox/Typing/Error.idr @@ -67,7 +67,7 @@ data Error | 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) +| 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 @@ -127,7 +127,7 @@ Located Error where (ExpectedSig loc _ _).loc = loc (ExpectedEnum loc _ _).loc = loc (ExpectedEq loc _ _).loc = loc - (ExpectedNat loc _ _).loc = loc + (ExpectedNAT loc _ _).loc = loc (ExpectedSTRING loc _ _).loc = loc (ExpectedBOX loc _ _).loc = loc (BadUniverse loc _ _).loc = loc @@ -290,10 +290,10 @@ parameters {opts : LayoutOpts} (showContext : Bool) hangDSingle "expected an enumeration type, but got" !(prettyTerm ctx.dnames ctx.tnames s) - ExpectedNat _ ctx s => + ExpectedNAT _ ctx s => hangDSingle ("expected the type" <++> - !(prettyTerm [<] [<] $ Nat noLoc) <+> ", but got") + !(prettyTerm [<] [<] $ NAT noLoc) <+> ", but got") !(prettyTerm ctx.dnames ctx.tnames s) ExpectedSTRING _ ctx s => diff --git a/lib/Quox/Untyped/Erase.idr b/lib/Quox/Untyped/Erase.idr index 98505e9..349d9fd 100644 --- a/lib/Quox/Untyped/Erase.idr +++ b/lib/Quox/Untyped/Erase.idr @@ -186,7 +186,7 @@ eraseTerm ctx ty (DLam body loc) = do a <- fst <$> wrapExpect `(expectEq) ctx loc ty eraseTerm (extendDim body.name ctx) a.term body.term -eraseTerm ctx _ s@(Nat {}) = +eraseTerm ctx _ s@(NAT {}) = throw $ CompileTimeOnly ctx s -- 0 ⤋ 0 ⇐ ℕ @@ -365,12 +365,12 @@ eraseElim ctx e@(CaseEnum qty tag ret arms loc) = do eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = do let ty = sub1 ret nat enat <- eraseElim ctx nat - zero <- eraseTerm ctx (sub1 ret (Ann (Zero loc) (Nat loc) loc)) zero + zero <- eraseTerm ctx (sub1 ret (Ann (Zero loc) (NAT loc) loc)) zero let [< p, ih] = succ.names succ' <- eraseTerm - (extendTyN [< (qty, p, Nat loc), + (extendTyN [< (qty, p, NAT loc), (qtyIH, ih, sub1 (ret // shift 1) (BV 0 loc))] ctx) - (sub1 (ret // shift 2) (Ann (Succ (BVT 1 loc) loc) (Nat loc) loc)) + (sub1 (ret // shift 2) (Ann (Succ (BVT 1 loc) loc) (NAT loc) loc)) succ.term let succ = case isErased qtyIH of Kept => NSRec p ih succ' diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr index f70df4f..0e35665 100644 --- a/lib/Quox/Whnf/Coercion.idr +++ b/lib/Quox/Whnf/Coercion.idr @@ -211,8 +211,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} (ty // one q) loc -- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ) - Nat tyLoc => - whnf defs ctx sg $ Ann s (Nat tyLoc) loc + NAT tyLoc => + whnf defs ctx sg $ Ann s (NAT tyLoc) loc -- (coe String @_ @_ s) ⇝ (s ∷ String) STRING tyLoc => diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr index bbd3f1b..b3f7331 100644 --- a/lib/Quox/Whnf/Interface.idr +++ b/lib/Quox/Whnf/Interface.idr @@ -84,8 +84,8 @@ isTagHead _ = False ||| an expression like `0 ∷ ℕ` or `suc n ∷ ℕ` public export %inline isNatHead : Elim {} -> Bool -isNatHead (Ann (Zero {}) (Nat {}) _) = True -isNatHead (Ann (Succ {}) (Nat {}) _) = True +isNatHead (Ann (Zero {}) (NAT {}) _) = True +isNatHead (Ann (Succ {}) (NAT {}) _) = True isNatHead (Coe {}) = True isNatHead _ = False @@ -121,7 +121,7 @@ isTyCon (Enum {}) = True isTyCon (Tag {}) = False isTyCon (Eq {}) = True isTyCon (DLam {}) = False -isTyCon (Nat {}) = True +isTyCon (NAT {}) = True isTyCon (Zero {}) = False isTyCon (Succ {}) = False isTyCon (STRING {}) = True @@ -168,7 +168,7 @@ canPushCoe sg (Enum {}) _ = True canPushCoe sg (Tag {}) _ = False canPushCoe sg (Eq {}) _ = True canPushCoe sg (DLam {}) _ = False -canPushCoe sg (Nat {}) _ = True +canPushCoe sg (NAT {}) _ = True canPushCoe sg (Zero {}) _ = False canPushCoe sg (Succ {}) _ = False canPushCoe sg (STRING {}) _ = True diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr index ffb82b0..3d7f94b 100644 --- a/lib/Quox/Whnf/Main.idr +++ b/lib/Quox/Whnf/Main.idr @@ -113,10 +113,10 @@ CanWhnf Elim Interface.isRedexE where Left _ => let ty = sub1 ret nat in case nat of - Ann (Zero _) (Nat _) _ => + Ann (Zero _) (NAT _) _ => whnf defs ctx sg $ Ann zer ty zer.loc - Ann (Succ n succLoc) (Nat natLoc) _ => - let nn = Ann n (Nat natLoc) succLoc + Ann (Succ n succLoc) (NAT natLoc) _ => + let nn = Ann n (NAT natLoc) succLoc tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc] in whnf defs ctx sg $ Ann tm ty caseLoc @@ -235,7 +235,7 @@ CanWhnf Term Interface.isRedexT where 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@(NAT {}) = pure $ nred t whnf _ _ _ t@(Zero {}) = pure $ nred t whnf _ _ _ t@(Succ {}) = pure $ nred t whnf _ _ _ t@(STRING {}) = pure $ nred t diff --git a/lib/Quox/Whnf/TypeCase.idr b/lib/Quox/Whnf/TypeCase.idr index 569a88d..a42c0d9 100644 --- a/lib/Quox/Whnf/TypeCase.idr +++ b/lib/Quox/Whnf/TypeCase.idr @@ -156,7 +156,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} ret loc -- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q - Nat {} => + NAT {} => whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KNat arms) ret loc -- (type-case String ∷ _ return Q of { String ⇒ s; ⋯ }) ⇝ s ∷ Q diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index 818e7c2..61926b0 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -19,7 +19,7 @@ defGlobals = fromList ("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))))] + ("two", mkDef GAny (^NAT) (^Succ (^Succ (^Zero))))] parameters (label : String) (act : Eff Equal ()) {default defGlobals globals : Definitions} @@ -447,30 +447,30 @@ tests = "equality & subtyping" :- [ ], "natural type" :- [ - testEq "ℕ = ℕ" $ equalTy empty (^Nat) (^Nat), - testEq "ℕ = ℕ : ★₀" $ equalT empty (^TYPE 0) (^Nat) (^Nat), - testEq "ℕ = ℕ : ★₆₉" $ equalT empty (^TYPE 69) (^Nat) (^Nat), - testNeq "ℕ ≠ {}" $ equalTy empty (^Nat) (^enum []), - testEq "0=1 ⊢ ℕ = {}" $ equalTy empty01 (^Nat) (^enum []) + testEq "ℕ = ℕ" $ equalTy empty (^NAT) (^NAT), + testEq "ℕ = ℕ : ★₀" $ equalT empty (^TYPE 0) (^NAT) (^NAT), + testEq "ℕ = ℕ : ★₆₉" $ equalT empty (^TYPE 69) (^NAT) (^NAT), + testNeq "ℕ ≠ {}" $ equalTy empty (^NAT) (^enum []), + testEq "0=1 ⊢ ℕ = {}" $ equalTy empty01 (^NAT) (^enum []) ], "natural numbers" :- [ - testEq "0 = 0" $ equalT empty (^Nat) (^Zero) (^Zero), + testEq "0 = 0" $ equalT empty (^NAT) (^Zero) (^Zero), testEq "succ two = succ two" $ - equalT empty (^Nat) (^Succ (^FT "two" 0)) (^Succ (^FT "two" 0)), + equalT empty (^NAT) (^Succ (^FT "two" 0)) (^Succ (^FT "two" 0)), testNeq "succ two ≠ two" $ - equalT empty (^Nat) (^Succ (^FT "two" 0)) (^FT "two" 0), + equalT empty (^NAT) (^Succ (^FT "two" 0)) (^FT "two" 0), testNeq "0 ≠ 1" $ - equalT empty (^Nat) (^Zero) (^Succ (^Zero)), + equalT empty (^NAT) (^Zero) (^Succ (^Zero)), testEq "0=1 ⊢ 0 = 1" $ - equalT empty01 (^Nat) (^Zero) (^Succ (^Zero)) + equalT empty01 (^NAT) (^Zero) (^Succ (^Zero)) ], "natural elim" :- [ testEq "caseω 0 return {a,b} of {zero ⇒ 'a; succ _ ⇒ 'b} = 'a" $ equalT empty (^enum ["a", "b"]) - (E $ ^CaseNat Any Zero (^Ann (^Zero) (^Nat)) + (E $ ^CaseNat Any Zero (^Ann (^Zero) (^NAT)) (SN $ ^enum ["a", "b"]) (^Tag "a") (SN $ ^Tag "b")) @@ -478,16 +478,16 @@ tests = "equality & subtyping" :- [ testEq "caseω 1 return {a,b} of {zero ⇒ 'a; succ _ ⇒ 'b} = 'b" $ equalT empty (^enum ["a", "b"]) - (E $ ^CaseNat Any Zero (^Ann (^Succ (^Zero)) (^Nat)) + (E $ ^CaseNat Any Zero (^Ann (^Succ (^Zero)) (^NAT)) (SN $ ^enum ["a", "b"]) (^Tag "a") (SN $ ^Tag "b")) (^Tag "b"), testEq "caseω 4 return ℕ of {0 ⇒ 0; succ n ⇒ n} = 3" $ equalT empty - (^Nat) - (E $ ^CaseNat Any Zero (^Ann (^makeNat 4) (^Nat)) - (SN $ ^Nat) + (^NAT) + (E $ ^CaseNat Any Zero (^Ann (^makeNat 4) (^NAT)) + (SN $ ^NAT) (^Zero) (SY [< "n", ^BN Unused] $ ^BVT 1)) (^makeNat 3) @@ -513,7 +513,7 @@ tests = "equality & subtyping" :- [ (^Pair (^Tag "b") (^Tag "a")), testEq "0=1 ⊢ ('a, 'b) = ('b, 'a) : ℕ" $ equalT empty01 - (^Nat) + (^NAT) (^Pair (^Tag "a") (^Tag "b")) (^Pair (^Tag "b") (^Tag "a")) ], diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr index b3451a9..b7bbf6e 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) (^Zero))] + 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 122be48..d74a65d 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -282,8 +282,8 @@ tests = "parser" :- [ ], "naturals" :- [ - parseMatch term "ℕ" `(Nat _), - parseMatch term "Nat" `(Nat _), + parseMatch term "ℕ" `(NAT _), + parseMatch term "Nat" `(NAT _), parseMatch term "zero" `(Zero _), parseMatch term "succ n" `(Succ (V "n" {}) _), parseMatch term "3" @@ -296,9 +296,9 @@ tests = "parser" :- [ "box" :- [ parseMatch term "[1.ℕ]" - `(BOX (PQ One _) (Nat _) _), + `(BOX (PQ One _) (NAT _) _), parseMatch term "[ω. ℕ × ℕ]" - `(BOX (PQ Any _) (Sig (Unused _) (Nat _) (Nat _) _) _), + `(BOX (PQ Any _) (Sig (Unused _) (NAT _) (NAT _) _) _), parseMatch term "[a]" `(Box (V "a" {}) _), parseMatch term "[0]" @@ -388,13 +388,13 @@ tests = "parser" :- [ `(Case (PQ Any _) (V "n" {}) (Unused _, V "A" {}) (CaseNat (V "a" {}) (PV "n'" _, PQ Zero _, Unused _, V "b" {}) _) _), parseMatch term "caseω n return ℕ of { succ _, 1.ih ⇒ ih; zero ⇒ 0; }" - `(Case (PQ Any _) (V "n" {}) (Unused _, Nat _) + `(Case (PQ Any _) (V "n" {}) (Unused _, NAT _) (CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _), parseMatch term "caseω n return ℕ of { succ _, ω.ih ⇒ ih; zero ⇒ 0; }" - `(Case (PQ Any _) (V "n" {}) (Unused _, Nat _) + `(Case (PQ Any _) (V "n" {}) (Unused _, NAT _) (CaseNat (Zero _) (Unused _, PQ Any _, PV "ih" _, V "ih" {}) _) _), parseMatch term "caseω n return ℕ of { succ _, ih ⇒ ih; zero ⇒ 0; }" - `(Case (PQ Any _) (V "n" {}) (Unused _, Nat _) + `(Case (PQ Any _) (V "n" {}) (Unused _, NAT _) (CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _), parseFails term "caseω n return A of { zero ⇒ a }", parseFails term "caseω n return ℕ of { succ ⇒ 5 }" @@ -425,9 +425,9 @@ tests = "parser" :- [ `(MkPDef (PQ Zero _) "A" (PConcrete (Just $ TYPE 0 _) (Enum ["a", "b", "c"] _)) _), parseMatch definition "postulate yeah : ℕ" - `(MkPDef (PQ Any _) "yeah" (PPostulate (Nat _)) _), + `(MkPDef (PQ Any _) "yeah" (PPostulate (NAT _)) _), parseMatch definition "postulateω yeah : ℕ" - `(MkPDef (PQ Any _) "yeah" (PPostulate (Nat _)) _), + `(MkPDef (PQ Any _) "yeah" (PPostulate (NAT _)) _), parseMatch definition "postulate0 FileHandle : ★" `(MkPDef (PQ Zero _) "FileHandle" (PPostulate (TYPE 0 _)) _), parseFails definition "postulate not-a-postulate : ℕ = 69", diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr index 71e183f..11356f7 100644 --- a/tests/Tests/PrettyTerm.idr +++ b/tests/Tests/PrettyTerm.idr @@ -210,7 +210,7 @@ tests = "pretty printing terms" :- [ "type-case" :- [ testPrettyE [<] [<] {label = "type-case ℕ ∷ ★⁰ return ★⁰ of { ⋯ }"} - (^TypeCase (^Ann (^Nat) (^TYPE 0)) (^TYPE 0) empty (^Nat)) + (^TypeCase (^Ann (^NAT) (^TYPE 0)) (^TYPE 0) empty (^NAT)) "type-case ℕ ∷ ★⁰ return ★⁰ of { _ ⇒ ℕ }" "type-case Nat :: Type 0 return Type 0 of { _ => Nat }" ], diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr index 7e81a7a..66595cb 100644 --- a/tests/Tests/Reduce.idr +++ b/tests/Tests/Reduce.idr @@ -52,7 +52,7 @@ tests = "whnf" :- [ ], "neutrals" :- [ - testNoStep "x" (ctx [< ("A", ^Nat)]) $ ^BV 0, + testNoStep "x" (ctx [< ("A", ^NAT)]) $ ^BV 0, testNoStep "a" empty $ ^F "a" 0, testNoStep "f a" empty $ ^App (^F "f" 0) (^FT "a" 0), testNoStep "★₀ ∷ ★₁" empty $ ^Ann (^TYPE 0) (^TYPE 1) @@ -81,13 +81,13 @@ tests = "whnf" :- [ ], "elim closure" :- [ - testWhnf "x{}" (ctx [< ("x", ^Nat)]) + testWhnf "x{}" (ctx [< ("x", ^NAT)]) (CloE (Sub (^BV 0) id)) (^BV 0), testWhnf "x{a/x}" empty (CloE (Sub (^BV 0) (^F "a" 0 ::: id))) (^F "a" 0), - testWhnf "x{a/y}" (ctx [< ("x", ^Nat)]) + testWhnf "x{a/y}" (ctx [< ("x", ^NAT)]) (CloE (Sub (^BV 0) (^BV 0 ::: ^F "a" 0 ::: id))) (^BV 0), testWhnf "x{(y{a/y})/x}" empty @@ -96,7 +96,7 @@ tests = "whnf" :- [ testWhnf "(x y){f/x,a/y}" empty (CloE (Sub (^App (^BV 0) (^BVT 1)) (^F "f" 0 ::: ^F "a" 0 ::: id))) (^App (^F "f" 0) (^FT "a" 0)), - testWhnf "(y ∷ x){A/x}" (ctx [< ("x", ^Nat)]) + testWhnf "(y ∷ x){A/x}" (ctx [< ("x", ^NAT)]) (CloE (Sub (^Ann (^BVT 1) (^BVT 0)) (^F "A" 0 ::: id))) (^BV 0), testWhnf "(y ∷ x){A/x,a/y}" empty @@ -129,10 +129,10 @@ tests = "whnf" :- [ ^App (^F "f" 0) (E $ ^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0))) (^FT "a" 0)), - testNoStep "λx. (y x){x/x,a/y}" (ctx [< ("y", ^Nat)]) $ + testNoStep "λx. (y x){x/x,a/y}" (ctx [< ("y", ^NAT)]) $ ^LamY "x" (CloT $ Sub (E $ ^App (^BV 1) (^BVT 0)) (^BV 0 ::: ^F "a" 0 ::: id)), - testNoStep "f (y x){x/x,a/y}" (ctx [< ("y", ^Nat)]) $ + testNoStep "f (y x){x/x,a/y}" (ctx [< ("y", ^NAT)]) $ ^App (^F "f" 0) (CloT (Sub (E $ ^App (^BV 1) (^BVT 0)) (^BV 0 ::: ^F "a" 0 ::: id))) diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr index 1418643..f99886a 100644 --- a/tests/Tests/Typechecker.idr +++ b/tests/Tests/Typechecker.idr @@ -79,7 +79,7 @@ sndDef = (SY [< "x", "y"] $ ^BVT 0)))) nat : Term d n -nat = ^Nat +nat = ^NAT apps : Elim d n -> List (Term d n) -> Elim d n apps = foldl (\f, s => ^App f s)