quox/tests/Tests/Parser.idr

323 lines
11 KiB
Idris
Raw Normal View History

2023-03-04 15:02:51 -05:00
module Tests.Parser
import Quox.Parser
import Data.List
import Data.String
import TAP
public export
data Failure =
ParseError Parser.Error
2023-03-04 15:02:51 -05:00
| WrongResult String
| ExpectedFail String
export
ToInfo Parser.Error where
2023-03-04 15:02:51 -05:00
toInfo (LexError err) =
[("type", "LexError"), ("info", show err)]
toInfo (ParseError errs) =
("type", "ParseError") ::
map (bimap show show) ([1 .. length errs] `zip` toList errs)
export
ToInfo Failure where
toInfo (ParseError err) =
toInfo err
2023-03-04 15:02:51 -05:00
toInfo (WrongResult got) =
[("type", "WrongResult"), ("got", got)]
toInfo (ExpectedFail got) =
[("type", "ExpectedFail"), ("got", got)]
parameters {c : Bool} {auto _ : Show a} (grm : Grammar c a)
(inp : String)
parameters {default (ltrim inp) label : String}
parsesWith : (a -> Bool) -> Test
parsesWith p = test label $ do
res <- mapFst ParseError $ lexParseWith grm inp
2023-03-04 15:02:51 -05:00
unless (p res) $ Left $ WrongResult $ show res
parses : Test
parses = parsesWith $ const True
parsesAs : Eq a => a -> Test
parsesAs exp = parsesWith (== exp)
parameters {default "\{ltrim inp} # fails" label : String}
parseFails : Test
parseFails = test label $ do
either (const $ Right ()) (Left . ExpectedFail . show) $
lexParseWith grm inp
2023-03-04 15:02:51 -05:00
export
tests : Test
tests = "parser" :- [
"bound names" :- [
parsesAs bname "_" Nothing,
parsesAs bname "F" (Just "F"),
parseFails bname "a.b.c"
],
"names" :- [
parsesAs name "x"
(MakePName [<] "x"),
2023-03-04 15:02:51 -05:00
parsesAs name "Data.String.length"
(MakePName [< "Data", "String"] "length"),
2023-03-04 15:02:51 -05:00
parseFails name "_"
],
"dimensions" :- [
parsesAs dim "0" (K Zero),
parsesAs dim "1" (K One),
parsesAs dim "𝑖" (V "𝑖"),
2023-03-04 15:02:51 -05:00
parseFails dim "M.x",
parseFails dim "_"
],
"quantities" :- [
parsesAs qty "0" Zero,
parsesAs qty "1" One,
parsesAs qty "ω" Any,
parsesAs qty "#" Any,
parseFails qty "anythingElse",
parseFails qty "_"
],
"enum types" :- [
parsesAs term #"{}"# (Enum []),
parsesAs term #"{a}"# (Enum ["a"]),
parsesAs term #"{a,}"# (Enum ["a"]),
parsesAs term #"{a.b.c.d}"# (Enum ["a.b.c.d"]),
parsesAs term #"{"hel lo"}"# (Enum ["hel lo"]),
parsesAs term #"{a, b}"# (Enum ["a", "b"]),
parsesAs term #"{a, b,}"# (Enum ["a", "b"]),
parsesAs term #"{a, b, ","}"# (Enum ["a", "b", ","]),
parseFails term #"{,}"#
],
"tags" :- [
parsesAs term #" 'a "# (Tag "a"),
parsesAs term #" 'abc "# (Tag "abc"),
parsesAs term #" '"abc" "# (Tag "abc"),
parsesAs term #" '"a b c" "# (Tag "a b c"),
parsesAs term #" 'a b c "# (Tag "a" :@ V "b" :@ V "c")
{label = "'a b c # application to two args"}
],
"universes" :- [
parsesAs term "★₀" (TYPE 0),
parsesAs term "★1" (TYPE 1),
parsesAs term "★ 2" (TYPE 2),
parsesAs term "Type₃" (TYPE 3),
parsesAs term "Type4" (TYPE 4),
parsesAs term "Type 100" (TYPE 100),
parsesAs term "(Type 1000)" (TYPE 1000),
parseFails term "Type",
parseFails term ""
],
"applications" :- [
parsesAs term "f" (V "f"),
parsesAs term "f.x.y" (V $ MakePName [< "f", "x"] "y"),
2023-03-04 15:02:51 -05:00
parsesAs term "f x" (V "f" :@ V "x"),
parsesAs term "f x y" (V "f" :@ V "x" :@ V "y"),
parsesAs term "(f x) y" (V "f" :@ V "x" :@ V "y"),
parsesAs term "f (g x)" (V "f" :@ (V "g" :@ V "x")),
parsesAs term "f (g x) y" (V "f" :@ (V "g" :@ V "x") :@ V "y"),
parsesAs term "f @p" (V "f" :% V "p"),
parsesAs term "f x @p y" (V "f" :@ V "x" :% V "p" :@ V "y")
],
"annotations" :- [
parsesAs term "f :: A" (V "f" :# V "A"),
parsesAs term "f ∷ A" (V "f" :# V "A"),
parsesAs term "f x y ∷ A B C"
((V "f" :@ V "x" :@ V "y") :#
(V "A" :@ V "B" :@ V "C")),
parsesAs term "Type 0 ∷ Type 1 ∷ Type 2"
(TYPE 0 :# (TYPE 1 :# TYPE 2))
],
"binders" :- [
parsesAs term "1.(x : A) → B x" $
2023-03-04 15:02:51 -05:00
Pi One (Just "x") (V "A") (V "B" :@ V "x"),
parsesAs term "1.(x : A) -> B x" $
2023-03-04 15:02:51 -05:00
Pi One (Just "x") (V "A") (V "B" :@ V "x"),
parsesAs term "ω.(x : A) → B x" $
2023-03-04 15:02:51 -05:00
Pi Any (Just "x") (V "A") (V "B" :@ V "x"),
parsesAs term "#.(x : A) -> B x" $
2023-03-04 15:02:51 -05:00
Pi Any (Just "x") (V "A") (V "B" :@ V "x"),
parseFails term "(x : A) → B x",
parsesAs term "1.A → B"
(Pi One Nothing (V "A") (V "B")),
parsesAs term "1.(List A) → List B"
(Pi One Nothing (V "List" :@ V "A") (V "List" :@ V "B")),
parseFails term "1.List A → List B",
2023-03-04 15:02:51 -05:00
parsesAs term "(x : A) × B x" $
Sig (Just "x") (V "A") (V "B" :@ V "x"),
parsesAs term "(x : A) ** B x" $
Sig (Just "x") (V "A") (V "B" :@ V "x"),
parseFails term "1.(x : A) × B x",
parsesAs term "A × B" $
Sig Nothing (V "A") (V "B"),
parsesAs term "A ** B" $
Sig Nothing (V "A") (V "B"),
parsesAs term "A × B × C" $
Sig Nothing (V "A") (Sig Nothing (V "B") (V "C")),
parsesAs term "(A × B) × C" $
Sig Nothing (Sig Nothing (V "A") (V "B")) (V "C")
2023-03-04 15:02:51 -05:00
],
"lambdas" :- [
parsesAs term "λ x ⇒ x" $ Lam (Just "x") (V "x"),
parsesAs term "λ x ⇒ x" $ Lam (Just "x") (V "x"),
parsesAs term "fun x => x" $ Lam (Just "x") (V "x"),
parsesAs term "δ i ⇒ x @i" $ DLam (Just "i") (V "x" :% V "i"),
parsesAs term "dfun i => x @i" $ DLam (Just "i") (V "x" :% V "i"),
parsesAs term "λ x y z ⇒ x z y" $
Lam (Just "x") $ Lam (Just "y") $ Lam (Just "z") $
V "x" :@ V "z" :@ V "y"
],
"pairs" :- [
parsesAs term "(x, y)" $
Pair (V "x") (V "y"),
parsesAs term "(x, y, z)" $
Pair (V "x") (Pair (V "y") (V "z")),
parsesAs term "((x, y), z)" $
Pair (Pair (V "x") (V "y")) (V "z"),
parsesAs term "(f x, g @y)" $
Pair (V "f" :@ V "x") (V "g" :% V "y"),
parsesAs term "((x : A) × B, 0.(x : C) → D)" $
2023-03-04 15:02:51 -05:00
Pair (Sig (Just "x") (V "A") (V "B"))
(Pi Zero (Just "x") (V "C") (V "D")),
parsesAs term "(λ x ⇒ x, δ i ⇒ e @i)" $
Pair (Lam (Just "x") (V "x"))
(DLam (Just "i") (V "e" :% V "i")),
parsesAs term "(x,)" (V "x"), -- i GUESS
parseFails term "(,y)",
parseFails term "(x,,y)"
],
"equality type" :- [
parsesAs term "Eq [i ⇒ A] s t" $
Eq (Just "i", V "A") (V "s") (V "t"),
parsesAs term "Eq [i ⇒ A B (C @i)] (f x y) (g y z)" $
Eq (Just "i", V "A" :@ V "B" :@ (V "C" :% V "i"))
(V "f" :@ V "x" :@ V "y") (V "g" :@ V "y" :@ V "z"),
parsesAs term "Eq [A] s t" $
Eq (Nothing, V "A") (V "s") (V "t"),
parsesAs term "s ≡ t : A" $
Eq (Nothing, V "A") (V "s") (V "t"),
parsesAs term "s == t : A" $
Eq (Nothing, V "A") (V "s") (V "t"),
parsesAs term "f x y ≡ g y z : A B C" $
Eq (Nothing, V "A" :@ V "B" :@ V "C")
(V "f" :@ V "x" :@ V "y") (V "g" :@ V "y" :@ V "z"),
parsesAs term "A × B ≡ A' × B' : ★₁" $
Eq (Nothing, TYPE 1)
(Sig Nothing (V "A") (V "B")) (Sig Nothing (V "A'") (V "B'")),
2023-03-04 15:02:51 -05:00
parseFails term "Eq",
parseFails term "Eq s t",
parseFails term "s ≡ t",
parseFails term ""
],
2023-03-26 08:40:54 -04:00
"naturals" :- [
parsesAs term "" Nat,
parsesAs term "Nat" Nat,
parsesAs term "zero" Zero,
parsesAs term "succ n" (Succ $ V "n"),
parsesAs term "3" (Succ (Succ (Succ Zero)) :# Nat),
parseFails term "succ"
],
2023-03-04 15:02:51 -05:00
"case" :- [
parsesAs term
"case1 f s return x ⇒ A x of { (l, r) ⇒ add l r }" $
Case One (V "f" :@ V "s")
(Just "x", V "A" :@ V "x")
(CasePair (Just "l", Just "r")
(V "add" :@ V "l" :@ V "r")),
parsesAs term
"case1 f s return x ⇒ A x of { (l, r) ⇒ add l r; }" $
Case One (V "f" :@ V "s")
(Just "x", V "A" :@ V "x")
(CasePair (Just "l", Just "r")
(V "add" :@ V "l" :@ V "r")),
parsesAs term
"case 1 . f s return x ⇒ A x of { (l, r) ⇒ add l r }" $
2023-03-04 15:02:51 -05:00
Case One (V "f" :@ V "s")
(Just "x", V "A" :@ V "x")
(CasePair (Just "l", Just "r")
(V "add" :@ V "l" :@ V "r")),
parsesAs term
"case1 t return A of { 'x ⇒ p; 'y ⇒ q; 'z ⇒ r }" $
Case One (V "t")
(Nothing, V "A")
(CaseEnum [("x", V "p"), ("y", V "q"), ("z", V "r")]),
parsesAs term "caseω t return A of {}" $
Case Any (V "t") (Nothing, V "A") (CaseEnum []),
parsesAs term "case# t return A of {}" $
2023-03-26 08:40:54 -04:00
Case Any (V "t") (Nothing, V "A") (CaseEnum []),
parsesAs term "caseω n return A of { 0 ⇒ a; succ n' ⇒ b }" $
Case Any (V "n") (Nothing, V "A") $
CaseNat (V "a") (Just "n'", Zero, Nothing, V "b"),
parsesAs term "caseω n return of { succ _ [1.ih] ⇒ ih; zero ⇒ 0; }" $
Case Any (V "n") (Nothing, Nat) $
CaseNat (Zero :# Nat) (Nothing, One, Just "ih", V "ih"),
parseFails term "caseω n return A of { zero ⇒ a }",
parseFails term "caseω n return of { succ ⇒ 5 }"
2023-03-06 05:35:57 -05:00
],
"definitions" :- [
parsesAs definition "defω x : {a} × {b} = ('a, 'b)" $
MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
2023-03-06 05:35:57 -05:00
(Pair (Tag "a") (Tag "b")),
parsesAs definition "defω x : {a} × {b} = ('a, 'b)" $
MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
2023-03-06 05:35:57 -05:00
(Pair (Tag "a") (Tag "b")),
parsesAs definition "def# x : {a} ** {b} = ('a, 'b)" $
MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
2023-03-06 05:35:57 -05:00
(Pair (Tag "a") (Tag "b")),
parsesAs definition "def ω.x : {a} × {b} = ('a, 'b)" $
MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
2023-03-06 05:35:57 -05:00
(Pair (Tag "a") (Tag "b")),
parsesAs definition "def x : {a} × {b} = ('a, 'b)" $
MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
(Pair (Tag "a") (Tag "b")),
parsesAs definition "def0 A : ★₀ = {a, b, c}" $
MkPDef Zero "A" (Just $ TYPE 0) (Enum ["a", "b", "c"])
],
"top level" :- [
parsesAs input "def0 A : ★₀ = {}; def0 B : ★₁ = A;" $
[PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
parsesAs input "def0 A : ★₀ = {} def0 B : ★₁ = A" $
[PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
parsesAs input "def0 A : ★₀ = {};;; def0 B : ★₁ = A" $
[PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
parsesAs input "" [] {label = "[empty input]"},
2023-03-17 21:47:15 -04:00
parsesAs input ";;;;;;;;;;;;;;;;;;;;;;;;;;" [],
parsesAs input "namespace a {}" [PD $ PNs $ MkPNamespace [< "a"] []],
parsesAs input "namespace a.b.c {}"
[PD $ PNs $ MkPNamespace [< "a", "b", "c"] []],
parsesAs input "namespace a {namespace b {}}"
[PD $ PNs $ MkPNamespace [< "a"] [PNs $ MkPNamespace [< "b"] []]],
parsesAs input "namespace a {def x = 't ∷ {t}}"
[PD $ PNs $ MkPNamespace [< "a"]
[PDef $ MkPDef Any "x" Nothing (Tag "t" :# Enum ["t"])]],
parsesAs input "namespace a {def x = 't ∷ {t}} def y = a.x"
[PD $ PNs $ MkPNamespace [< "a"]
[PDef $ MkPDef Any "x" Nothing (Tag "t" :# Enum ["t"])],
PD $ PDef $ MkPDef Any "y" Nothing (V $ MakePName [< "a"] "x")],
parsesAs input #" load "a.quox"; def b = a.b "#
[PLoad "a.quox",
PD $ PDef $ MkPDef Any "b" Nothing (V $ MakePName [< "a"] "b")]
2023-03-04 15:02:51 -05:00
]
]