more parser tests

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 [
+  "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"
   ]
 ]