quox/tests/Tests/Parser.idr

111 lines
2.8 KiB
Idris

module Tests.Parser
import Quox.Syntax
import Quox.Parser
import Quox.Lexer
import Tests.Lexer
import Data.SnocVect
import Text.Parser
import TAP
export
Show tok => ToInfo (ParsingError tok) where
toInfo (Error msg Nothing) = [("msg", msg)]
toInfo (Error msg (Just loc)) = [("loc", show loc), ("msg", msg)]
numberErrs : List1 Info -> Info
numberErrs (head ::: []) = head
numberErrs (head ::: tail) = go 0 (head :: tail) where
number1 : Nat -> Info -> Info
number1 n = map $ \(k, v) => (show n ++ k, v)
go : Nat -> List Info -> Info
go k [] = []
go k (x :: xs) = number1 k x ++ go (S k) xs
export
ToInfo Parser.Error where
toInfo (Lex err) = toInfo err
toInfo (Parse errs) = numberErrs $ map toInfo errs
toInfo (Leftover toks) = toInfo [("leftover", toks)]
RealError = Quox.Parser.Error
%hide Lexer.RealError
%hide Quox.Parser.Error
data Error a
= Parser RealError
| Unexpected a a
| ShouldFail a
export
Show a => ToInfo (Error a) where
toInfo (Parser err) = toInfo err
toInfo (Unexpected exp got) = toInfo $
[("expected", exp), ("received", got)]
toInfo (ShouldFail got) = toInfo [("success", got)]
parameters {c : Bool} (grm : Grammar c a) (input : String)
parses : (Show a, Eq a) => a -> Test
parses exp = test "\"\{input}\"" $ delay $
case lexParseAll grm input of
Right got => if got == exp then Right ()
else Left $ Unexpected exp got
Left err => Left $ Parser err
rejects : Show a => Test
rejects = test "\"\{input}\" (reject)" $ do
case lexParseAll grm input of
Left err => Right ()
Right val => Left $ ShouldFail val
tests = "parser" :- [
"numbers" :-
let parses = parses number
in [
parses "0" 0,
parses "1" 1,
parses "1000" 1000
],
"bound vars (x, y, z ⊢)" :-
let grm = bound [< "x", "y", "z"]
parses = parses grm; rejects = rejects grm
in [
parses "x" (V 2),
parses "y" (V 1),
parses "z" (V 0),
rejects "M.x",
rejects "x.a",
rejects "a"
],
"bound or free vars (x, y, z ⊢)" :-
let parses = parses $ nameWith [< "x", "y", "z"]
in [
parses "x" (Left (V 2)),
parses "y" (Left (V 1)),
parses "z" (Left (V 0)),
parses "a" (Right (MakeName [<] (UN "a"))),
parses "a.b.c" (Right (MakeName [< "a", "b"] (UN "c"))),
parses "a . b . c" (Right (MakeName [< "a", "b"] (UN "c"))),
parses "M.x" (Right (MakeName [< "M"] (UN "x"))),
parses "x.a" (Right (MakeName [< "x"] (UN "a")))
],
"dimension (x, y, z ⊢)" :-
let grm = dimension [< "x", "y", "z"]
parses = parses grm; rejects = rejects grm
in [
parses "0" (K Zero),
parses "1" (K One),
rejects "2",
parses "x" (B (V 2)),
rejects "a"
]
]