rhi/quox
rhi
/
quox
1
0
Fork 0
Code Issues 16 Pull Requests 1 Releases Wiki Activity

rename Nat to NAT in AST

This commit is contained in:
rhiannon morris 2023-11-02 18:14:22 +01:00
parent e0ed37720f
commit fa7f82ae5a
24 changed files with 92 additions and 92 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Quox/Displace.idr
View File

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

16
lib/Quox/Equal.idr
View File

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

4
lib/Quox/FreeVars.idr
View File

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

2
lib/Quox/Parser/FromParser.idr
View File

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

2
lib/Quox/Parser/Parser.idr
View File

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

4
lib/Quox/Parser/Syntax.idr
View File

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

8
lib/Quox/Syntax/Term/Base.idr
View File

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

2
lib/Quox/Syntax/Term/Pretty.idr
View File

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

4
lib/Quox/Syntax/Term/Subst.idr
View File

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

10
lib/Quox/Syntax/Term/Tighten.idr
View File

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

12
lib/Quox/Typechecker.idr
View File

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

10
lib/Quox/Typing.idr
View File

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

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

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

8
lib/Quox/Untyped/Erase.idr
View File

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

4
lib/Quox/Whnf/Coercion.idr
View File

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

8
lib/Quox/Whnf/Interface.idr
View File

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

8
lib/Quox/Whnf/Main.idr
View File

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

2
lib/Quox/Whnf/TypeCase.idr
View File

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

34
tests/Tests/Equal.idr
View File

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

2
tests/Tests/FromPTerm.idr
View File

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

18
tests/Tests/Parser.idr
View File

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

2
tests/Tests/PrettyTerm.idr
View File

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

12
tests/Tests/Reduce.idr
View File

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

2
tests/Tests/Typechecker.idr
View File

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