diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index 3fb60c8..44043ed 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -52,26 +52,60 @@ Show a => ToInfo (Error a) where parameters {c : Bool} (grm : Grammar c a) (input : String) parses : (Show a, Eq a) => a -> Test - parses exp = test input $ delay $ + 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 $ do + 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, + "numbers" :- + let parses = parses number + in [ + parses "0" 0, + parses "1" 1, parses "1000" 1000 ], - "bound vars" :- let parses = parses (bound [< "x", "y", "z"]) in [ + "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" ] ]