rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity
quox/tests/Tests/Parser.idr

510 lines
20 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Tests.Parser
import Quox.Parser
import Data.List
import Data.String
import TAP
import Language.Reflection
%language ElabReflection
public export
data Failure =
ParseError Parser.Error
| WrongResult String
| ExpectedFail String
export
ToInfo Parser.Error where
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
toInfo (WrongResult got) =
[("type", "WrongResult"), ("got", got)]
toInfo (ExpectedFail got) =
[("type", "ExpectedFail"), ("got", got)]
parameters {auto _ : (Show a, Eq a)} {c : Bool} (grm : FileName -> Grammar c a)
parsesWith : String -> (a -> Bool) -> Test
parsesWith inp p = test (ltrim inp) $ do
res <- mapFst ParseError $ lexParseWith (grm "<test>") inp
unless (p res) $ Left $ WrongResult $ show res
parsesAs : String -> a -> Test
parsesAs inp exp = parsesWith inp (== exp)
%macro
parseMatch : String -> TTImp -> Elab Test
parseMatch inp pat =
parsesWith inp <$> check `(\case ~(pat) => True; _ => False)
parseFails : String -> Test
parseFails inp = test "\{ltrim inp} # fails" $ do
either (const $ Right ()) (Left . ExpectedFail . show) $
lexParseWith (grm "‹test›") inp
export
tests : Test
tests = "parser" :- [
"pattern vars" :- [
parseMatch patVar "_" `(Unused _),
parseMatch patVar "F" `(PV "F" _),
parseFails patVar "a.b.c"
],
"names" :- [
parsesAs (const qname) "x"
(MakePName [<] "x"),
parsesAs (const qname) "Data.String.length"
(MakePName [< "Data", "String"] "length"),
parseFails (const qname) "_"
],
"dimensions" :- [
parseMatch dim "0" `(K Zero _),
parseMatch dim "1" `(K One _),
parseMatch dim "𝑖" `(V "𝑖" {}),
parseFails dim "M.x",
parseFails dim "_"
],
"quantities" :- [
parseMatch qty "0" `(PQ Zero _),
parseMatch qty "1" `(PQ One _),
parseMatch qty "ω" `(PQ Any _),
parseMatch qty "#" `(PQ Any _),
parseFails qty "anythingElse",
parseFails qty "_"
],
"enum types" :- [
parseMatch term #"{}"# `(Enum [] _),
parseMatch term #"{a}"# `(Enum ["a"] _),
parseMatch term #"{a,}"# `(Enum ["a"] _),
parseMatch term #"{a.b.c.d}"# `(Enum ["a.b.c.d"] _),
parseMatch term #"{"hel lo"}"# `(Enum ["hel lo"] _),
parseMatch term #"{a, b}"# `(Enum ["a", "b"] _),
parseMatch term #"{a, b,}"# `(Enum ["a", "b"] _),
parseMatch term #"{a, b, ","}"# `(Enum ["a", "b", ","] _),
parseFails term #"{,}"#
],
"tags" :- [
parseMatch term #" 'a "# `(Tag "a" _),
parseMatch term #" 'abc "# `(Tag "abc" _),
parseMatch term #" '"abc" "# `(Tag "abc" _),
parseMatch term #" '"a b c" "# `(Tag "a b c" _),
note "application to two arguments",
parseMatch term #" 'a b c "#
`(App (App (Tag "a" _) (V "b" {}) _) (V "c" {}) _)
],
"universes" :- [
parseMatch term "★⁰" `(TYPE 0 _),
parseMatch term "★1" `(TYPE 1 _),
parseMatch term "★ 2" `(TYPE 2 _),
parseMatch term "Type³" `(TYPE 3 _),
parseMatch term "Type4" `(TYPE 4 _),
parseMatch term "Type 100" `(TYPE 100 _),
parseMatch term "(Type 1000)" `(TYPE 1000 _),
parseMatch term "Type" `(TYPE 0 _),
parseMatch term "★" `(TYPE 0 _)
],
"applications" :- [
parseMatch term "f"
`(V "f" {}),
parseMatch term "f.x.y"
`(V (MakePName [< "f", "x"] "y") {}),
parseMatch term "f x"
`(App (V "f" {}) (V "x" {}) _),
parseMatch term "f x y"
`(App (App (V "f" {}) (V "x" {}) _) (V "y" {}) _),
parseMatch term "(f x) y"
`(App (App (V "f" {}) (V "x" {}) _) (V "y" {}) _),
parseMatch term "f (g x)"
`(App (V "f" {}) (App (V "g" {}) (V "x" {}) _) _),
parseMatch term "f (g x) y"
`(App (App (V "f" {}) (App (V "g" {}) (V "x" {}) _) _) (V "y" {}) _),
parseMatch term "f @p"
`(DApp (V "f" {}) (V "p" {}) _),
parseMatch term "f x @p y"
`(App (DApp (App (V "f" {}) (V "x" {}) _) (V "p" {}) _) (V "y" {}) _)
],
"annotations" :- [
parseMatch term "f :: A"
`(Ann (V "f" {}) (V "A" {}) _),
parseMatch term "f ∷ A"
`(Ann (V "f" {}) (V "A" {}) _),
parseMatch term "f x y ∷ A B C"
`(Ann (App (App (V "f" {}) (V "x" {}) _) (V "y" {}) _)
(App (App (V "A" {}) (V "B" {}) _) (V "C" {}) _) _),
parseMatch term "Type 0 ∷ Type 1 ∷ Type 2"
`(Ann (TYPE 0 _) (Ann (TYPE 1 _) (TYPE 2 _) _) _)
],
"binders" :- [
parseMatch term "1.(x : A) → B x"
`(Pi (PQ One _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
parseMatch term "1.(x : A) -> B x"
`(Pi (PQ One _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
parseMatch term "ω.(x : A) → B x"
`(Pi (PQ Any _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
parseMatch term "#.(x : A) -> B x"
`(Pi (PQ Any _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
parseMatch term "1.(x y : A) -> B x"
`(Pi (PQ One _) (PV "x" _) (V "A" {})
(Pi (PQ One _) (PV "y" _) (V "A" {})
(App (V "B" {}) (V "x" {}) _) _) _),
parseMatch term "(x : A) → B x"
`(Pi (PQ One _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
parseFails term "(x : A) → (y : B x)",
parseFails term "(x : A) → 1.(B x)",
parseMatch term "1.A → B"
`(Pi (PQ One _) (Unused _) (V "A" {}) (V "B" {}) _),
parseMatch term "A → B"
`(Pi (PQ One _) (Unused _) (V "A" {}) (V "B" {}) _),
parseMatch term "A → B → C"
`(Pi (PQ One _) (Unused _) (V "A" {})
(Pi (PQ One _) (Unused _) (V "B" {}) (V "C" {}) _) _),
parseMatch term "1.(List A) → List B"
`(Pi (PQ One _) (Unused _)
(App (V "List" {}) (V "A" {}) _)
(App (V "List" {}) (V "B" {}) _) _),
parseMatch term "0.★⁰ → ★⁰"
`(Pi (PQ Zero _) (Unused _) (TYPE 0 _) (TYPE 0 _) _),
parseFails term "1.List A → List B",
parseMatch term "(x : A) × B x"
`(Sig (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
parseMatch term "(x : A) ** B x"
`(Sig (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
parseMatch term "(x y : A) × B" $
`(Sig (PV "x" _) (V "A" {}) (Sig (PV "y" _) (V "A" {}) (V "B" {}) _) _),
parseFails term "1.(x : A) × B x",
parseMatch term "A × B"
`(Sig (Unused _) (V "A" {}) (V "B" {}) _),
parseMatch term "A ** B"
`(Sig (Unused _) (V "A" {}) (V "B" {}) _),
parseMatch term "A × B × C" $
`(Sig (Unused _) (V "A" {}) (Sig (Unused _) (V "B" {}) (V "C" {}) _) _),
parseMatch term "(A × B) × C" $
`(Sig (Unused _) (Sig (Unused _) (V "A" {}) (V "B" {}) _) (V "C" {}) _),
parseMatch term "A × B → C" $
`(Pi (PQ One _) (Unused _)
(Sig (Unused _) (V "A" {}) (V "B" {}) _)
(V "C" {}) _),
parseMatch term "A → B × C" $
`(Pi (PQ One _) (Unused _)
(V "A" {})
(Sig (Unused _) (V "B" {}) (V "C" {}) _) _),
parseMatch term "A → B × C → D" $
`(Pi (PQ One _) (Unused _)
(V "A" {})
(Pi (PQ One _) (Unused _)
(Sig (Unused _) (V "B" {}) (V "C" {}) _)
(V "D" {}) _) _)
],
"lambdas" :- [
parseMatch term "λ x ⇒ x"
`(Lam (PV "x" _) (V "x" {}) _),
parseMatch term "fun x => x"
`(Lam (PV "x" _) (V "x" {}) _),
parseMatch term "δ i ⇒ x @i"
`(DLam (PV "i" _) (DApp (V "x" {}) (V "i" {}) _) _),
parseMatch term "dfun i => x @i"
`(DLam (PV "i" _) (DApp (V "x" {}) (V "i" {}) _) _),
parseMatch term "λ x y z ⇒ x z y"
`(Lam (PV "x" _)
(Lam (PV "y" _)
(Lam (PV "z" _)
(App (App (V "x" {}) (V "z" {}) _) (V "y" {}) _) _) _) _)
],
"pairs" :- [
parseMatch term "(x, y)"
`(Pair (V "x" {}) (V "y" {}) _),
parseMatch term "(x, y, z)"
`(Pair (V "x" {}) (Pair (V "y" {}) (V "z" {}) _) _),
parseMatch term "((x, y), z)"
`(Pair (Pair (V "x" {}) (V "y" {}) _) (V "z" {}) _),
parseMatch term "(f x, g @y)"
`(Pair (App (V "f" {}) (V "x" {}) _) (DApp (V "g" {}) (V "y" {}) _) _),
parseMatch term "((x : A) × B, 0.(x : C) → D)"
`(Pair (Sig (PV "x" _) (V "A" {}) (V "B" {}) _)
(Pi (PQ Zero _) (PV "x" _) (V "C" {}) (V "D" {}) _) _),
parseMatch term "(λ x ⇒ x, δ i ⇒ e @i)"
`(Pair (Lam (PV "x" _) (V "x" {}) _)
(DLam (PV "i" _) (DApp (V "e" {}) (V "i" {}) _) _) _),
parseMatch term "(x,)" `(V "x" {}), -- i GUESS
parseFails term "(,y)",
parseFails term "(x,,y)"
],
"w" :- [
parseMatch term "(x : A) ⊲ B"
`(W (PV "x" _) (V "A" {}) (V "B" {}) _),
parseFails term "(x y : A) ⊲ B",
parseFails term "1.(x : A) ⊲ B",
parseMatch term "(x : A) ⊲ (y : B) ⊲ C"
`(W (PV "x" _) (V "A" {})
(W (PV "y" _) (V "B" {}) (V "C" {}) _) _),
parseMatch term "A ⊲ B"
`(W _ (V "A" {}) (V "B" {}) _),
parseMatch term "A <| B"
`(W _ (V "A" {}) (V "B" {}) _),
parseFails term "A ⊲ (y : B)",
parseMatch term "(x : A) ⊲ B x × C"
`(W (PV "x" _) (V "A" {})
(Sig _ (App (V "B" {}) (V "x" {}) _) (V "C" {}) _) _),
parseMatch term "A ⊲ B → C"
`(Pi _ _ (W _ (V "A" {}) (V "B" {}) _) (V "C" {}) _),
parseMatch term "A → B ⊲ C"
`(Pi _ _ (V "A" {}) (W _ (V "B" {}) (V "C" {}) _) _)
],
"sup" :- [
parseMatch term "s ⋄ t"
`(Sup (V "s" {}) (V "t" {}) _),
parseMatch term "s ⋄ t ⋄ u"
`(Sup (V "s" {}) (Sup (V "t" {}) (V "u" {}) _) _),
parseMatch term "s <> t"
`(Sup (V "s" {}) (V "t" {}) _),
parseMatch term "a b ⋄ c d"
`(Sup (App (V "a" {}) (V "b" {}) _) (App (V "c" {}) (V "d" {}) _) _),
parseMatch term "a ⋄ b ≡ a' ⋄ b' : (A ⊲ B)"
`(Eq (_, W _ (V "A" {}) (V "B" {}) _)
(Sup (V "a" {}) (V "b" {}) _)
(Sup (V "a'" {}) (V "b'" {}) _) _)
],
"equality type" :- [
parseMatch term "Eq (i ⇒ A) s t"
`(Eq (PV "i" _, V "A" {}) (V "s" {}) (V "t" {}) _),
parseMatch term "Eq (i ⇒ A (B @i)) (f x) (g y)"
`(Eq (PV "i" _, App (V "A" {}) (DApp (V "B" {}) (V "i" {}) _) _)
(App (V "f" {}) (V "x" {}) _)
(App (V "g" {}) (V "y" {}) _) _),
parseMatch term "Eq A s t"
`(Eq (Unused _, V "A" {}) (V "s" {}) (V "t" {}) _),
parseMatch term "s ≡ t : A"
`(Eq (Unused _, V "A" {}) (V "s" {}) (V "t" {}) _),
parseMatch term "s == t : A"
`(Eq (Unused _, V "A" {}) (V "s" {}) (V "t" {}) _),
parseMatch term "f x ≡ g y : A B"
`(Eq (Unused _, App (V "A" {}) (V "B" {}) _)
(App (V "f" {}) (V "x" {}) _)
(App (V "g" {}) (V "y" {}) _) _),
parseMatch term "(A × B) ≡ (A' × B') : ★¹"
`(Eq (Unused _, TYPE 1 _)
(Sig (Unused _) (V "A" {}) (V "B" {}) _)
(Sig (Unused _) (V "A'" {}) (V "B'" {}) _) _),
note "A × (B ≡ A' × B' : ★¹)",
parseMatch term "A × B ≡ A' × B' : ★¹"
`(Sig (Unused _) (V "A" {})
(Eq (Unused _, TYPE 1 _)
(V "B" {}) (Sig (Unused _) (V "A'" {}) (V "B'" {}) _) _) _),
parseFails term "Eq",
parseFails term "Eq s t",
parseFails term "s ≡ t",
parseFails term "≡"
],
"naturals" :- [
parseMatch term "ℕ" `(Nat _),
parseMatch term "Nat" `(Nat _),
parseMatch term "zero" `(Zero _),
parseMatch term "succ n" `(Succ (V "n" {}) _),
parseMatch term "3"
`(Succ (Succ (Succ (Zero _) _) _) _),
parseMatch term "succ (succ 1)"
`(Succ (Succ (Succ (Zero _) _) _) _),
parseFails term "succ succ 5",
parseFails term "succ"
],
"box" :- [
parseMatch term "[1.ℕ]"
`(BOX (PQ One _) (Nat _) _),
parseMatch term "[ω. ℕ × ℕ]"
`(BOX (PQ Any _) (Sig (Unused _) (Nat _) (Nat _) _) _),
parseMatch term "[a]"
`(Box (V "a" {}) _),
parseMatch term "[0]"
`(Box (Zero _) _),
parseMatch term "[1]"
`(Box (Succ (Zero _) _) _)
],
"coe" :- [
parseMatch term "coe A @p @q x"
`(Coe (Unused _, V "A" {}) (V "p" {}) (V "q" {}) (V "x" {}) _),
parseMatch term "coe (i ⇒ A) @p @q x"
`(Coe (PV "i" _, V "A" {}) (V "p" {}) (V "q" {}) (V "x" {}) _),
parseMatch term "coe A x"
`(Coe (Unused _, V "A" {}) (K Zero _) (K One _) (V "x" {}) _),
parseFails term "coe A @p @q",
parseFails term "coe (i ⇒ A) @p q x"
],
"comp" :- [
parseMatch term "comp A @p @q s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }"
`(Comp (Unused _, V "A" {}) (V "p" {}) (V "q" {}) (V "s" {}) (V "r" {})
(PV "𝑗" _, V "s₀" {}) (PV "𝑘" _, V "s₁" {}) _),
parseMatch term "comp (𝑖 ⇒ A) @p @q s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }"
`(Comp (PV "𝑖" _, V "A" {}) (V "p" {}) (V "q" {}) (V "s" {}) (V "r" {})
(PV "𝑗" _, V "s₀" {}) (PV "𝑘" _, V "s₁" {}) _),
parseMatch term "comp A @p @q s @r { 1 𝑗 ⇒ s₀; 0 𝑘 ⇒ s₁; }"
`(Comp (Unused _, V "A" {}) (V "p" {}) (V "q" {}) (V "s" {}) (V "r" {})
(PV "𝑘" _, V "s₁" {}) (PV "𝑗" _, V "s₀" {}) _),
parseMatch term "comp A s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }"
`(Comp (Unused _, V "A" {}) (K Zero _) (K One _) (V "s" {}) (V "r" {})
(PV "𝑗" _, V "s₀" {}) (PV "𝑘" _, V "s₁" {}) _),
parseFails term "comp A @p @q s @r { 1 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁; }",
parseFails term "comp A @p @q s @r { 0 𝑗 ⇒ s₀ }",
parseFails term "comp A @p @q s @r { }"
],
"case" :- [
parseMatch term
"case1 f s return x ⇒ A x of { (l, r) ⇒ r l }"
`(Case (PQ One _) (App (V "f" {}) (V "s" {}) _)
(PV "x" _, App (V "A" {}) (V "x" {}) _)
(CasePair (PV "l" _, PV "r" _)
(App (V "r" {}) (V "l" {}) _) _) _),
parseMatch term
"case1 f s return x => A x of { (l, r) ⇒ r l; }"
`(Case (PQ One _) (App (V "f" {}) (V "s" {}) _)
(PV "x" _, App (V "A" {}) (V "x" {}) _)
(CasePair (PV "l" _, PV "r" _)
(App (V "r" {}) (V "l" {}) _) _) _),
parseMatch term
"case 1. f s return x ⇒ A x of { (l, r) ⇒ r l }"
`(Case (PQ One _) (App (V "f" {}) (V "s" {}) _)
(PV "x" _, App (V "A" {}) (V "x" {}) _)
(CasePair (PV "l" _, PV "r" _)
(App (V "r" {}) (V "l" {}) _) _) _),
parseMatch term
"caseω f s return x ⇒ A x of { (l, r) ⇒ r l }"
`(Case (PQ Any _) (App (V "f" {}) (V "s" {}) _)
(PV "x" _, App (V "A" {}) (V "x" {}) _)
(CasePair (PV "l" _, PV "r" _)
(App (V "r" {}) (V "l" {}) _) _) _),
parseMatch term
"case0 f s return x ⇒ A x of { (l, r) ⇒ r l }"
`(Case (PQ Zero _) (App (V "f" {}) (V "s" {}) _)
(PV "x" _, App (V "A" {}) (V "x" {}) _)
(CasePair (PV "l" _, PV "r" _)
(App (V "r" {}) (V "l" {}) _) _) _),
parseMatch term
"case f s return x ⇒ A x of { (l, r) ⇒ r l }"
`(Case (PQ One _) (App (V "f" {}) (V "s" {}) _)
(PV "x" _, App (V "A" {}) (V "x" {}) _)
(CasePair (PV "l" _, PV "r" _)
(App (V "r" {}) (V "l" {}) _) _) _),
parseMatch term
"case1 t return A of { 'x ⇒ p; 'y ⇒ q; 'z ⇒ r }"
`(Case (PQ One _) (V "t" {})
(Unused _, V "A" {})
(CaseEnum [(PT "x" _, V "p" {}),
(PT "y" _, V "q" {}),
(PT "z" _, V "r" {})] _) _),
parseMatch term "caseω t return A of {}"
`(Case (PQ Any _) (V "t" {}) (Unused _, V "A" {}) (CaseEnum [] _) _),
parseMatch term "case# t return A of {}"
`(Case (PQ Any _) (V "t" {}) (Unused _, V "A" {}) (CaseEnum [] _) _),
parseMatch term "caseω n return A of { 0 ⇒ a; succ n' ⇒ b }"
`(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 _)
(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 _)
(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 _)
(CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
parseMatch term "caseω n return ℕ of { succ _, _ ⇒ ih; zero ⇒ 0; }"
`(Case (PQ Any _) (V "n" {}) (Unused _, Nat _)
(CaseNat (Zero _) (Unused _, PQ Zero _, Unused _, V "ih" {}) _) _),
parseFails term "caseω n return A of { zero ⇒ a }",
parseFails term "caseω n return ℕ of { succ ⇒ 5 }",
parseMatch term "case e return z ⇒ C of { a ⋄ b, ω.ih ⇒ u }"
`(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
(CaseW (PV "a" _) (PV "b" _) (PQ Any _, PV "ih" _) (V "u" {}) _) _),
parseMatch term "case e return z ⇒ C of { a ⋄ b, ih ⇒ u }"
`(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
(CaseW (PV "a" _) (PV "b" _) (PQ One _, PV "ih" _) (V "u" {}) _) _),
parseMatch term "case e return z ⇒ C of { a ⋄ b ⇒ u }"
`(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
(CaseW (PV "a" _) (PV "b" _) (PQ Zero _, Unused _) (V "u" {}) _) _),
parseMatch term "case e return z ⇒ C of { a ⋄ b, _ ⇒ u }"
`(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
(CaseW (PV "a" _) (PV "b" _) (PQ Zero _, Unused _) (V "u" {}) _) _)
],
"definitions" :- [
parseMatch definition "defω x : {a} × {b} = ('a, 'b);"
`(MkPDef (PQ Any _) "x"
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _) _),
parseMatch definition "def# x : {a} ** {b} = ('a, 'b)"
`(MkPDef (PQ Any _) "x"
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _) _),
parseMatch definition "def ω.x : {a} × {b} = ('a, 'b)"
`(MkPDef (PQ Any _) "x"
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _) _),
parseMatch definition "def x : {a} × {b} = ('a, 'b)"
`(MkPDef (PQ Any _) "x"
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _) _),
parseMatch definition "def0 A : ★⁰ = {a, b, c}"
`(MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _)
(Enum ["a", "b", "c"] _) _)
],
"top level" :- [
parseMatch input "def0 A : ★⁰ = {}; def0 B : ★¹ = A;"
`([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _,
PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _]),
parseMatch input "def0 A : ★⁰ = {} def0 B : ★¹ = A" $
`([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _,
PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _]),
note "empty input",
parsesAs input "" [],
parseFails input ";;;;;;;;;;;;;;;;;;;;;;;;;;",
parseMatch input "namespace a {}"
`([PD $ PNs $ MkPNamespace [< "a"] [] _]),
parseMatch input "namespace a.b.c {}"
`([PD $ PNs $ MkPNamespace [< "a", "b", "c"] [] _]),
parseMatch input "namespace a {namespace b {}}"
`([PD $ PNs $ MkPNamespace [< "a"] [PNs $ MkPNamespace [< "b"] [] _] _]),
parseMatch input "namespace a {def x = 't ∷ {t}}"
`([PD $ PNs $ MkPNamespace [< "a"]
[PDef $ MkPDef (PQ Any _) "x" Nothing
(Ann (Tag "t" _) (Enum ["t"] _) _) _] _]),
parseMatch input "namespace a {def x = 't ∷ {t}} def y = a.x"
`([PD $ PNs $ MkPNamespace [< "a"]
[PDef $ MkPDef (PQ Any _) "x" Nothing
(Ann (Tag "t" _) (Enum ["t"] _) _) _] _,
PD $ PDef $ MkPDef (PQ Any _) "y" Nothing
(V (MakePName [< "a"] "x") {}) _]),
parseMatch input #" load "a.quox"; def b = a.b "#
`([PLoad "a.quox" _,
PD $ PDef $ MkPDef (PQ Any _) "b" Nothing
(V (MakePName [< "a"] "b") {}) _])
]
]
Reference in a new issue View git blame Copy permalink