parser stuff

lib/Quox/Parser.idr

@@ -4,6 +4,7 @@ import Quox.Syntax
 import Quox.Token
 import Quox.Lexer
 
+import Data.Maybe
 import Data.SnocVect
 import Data.SnocList
 import Text.Parser
@@ -86,9 +87,9 @@ find _  _                     = Nothing
 
 
 export
-bound : Vars k -> Grammar True (Var k)
-bound vs =
-  terminal "bound variable" $ \case Name x => find1 vs x; _ => Nothing
+bound : (what : String) -> Vars k -> Grammar True (Var k)
+bound what vs = terminal "bound \{what} variable" $
+                \case Name x => find1 vs x; _ => Nothing
 
 export
 sname : Grammar True String
@@ -101,10 +102,13 @@ qname = do
   pure $ MakeName {mods = cast $ init parts, base = UN $ last parts}
 
 export
-nameWith : Vars k -> Grammar True (Either (Var k) Name)
-nameWith vs = do
+nameWith : (bound : Vars k) -> (avoid : Vars n) ->
+           Grammar True (Either (Var k) Name)
+nameWith bound avoid = do
   y <- qname
-  pure $ maybe (Right y) Left $ find vs y
+  when (isJust $ find avoid y) $
+    fail "wrong type of bound variable: \{show y}"
+  pure $ maybe (Right y) Left $ find bound y
 
 
 export
@@ -112,4 +116,16 @@ dimension : Vars d -> Grammar True (Dim d)
 dimension vs =
       K Zero <$  zero
   <|> K One  <$  one
-  <|> B      <$> bound vs
+  <|> B      <$> bound "dimension" vs
+
+
+mutual
+  export
+  term : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Term d n)
+  term dvars tvars =
+        E <$> squares (elim dvars tvars)
+
+  export
+  elim : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Elim d n)
+  elim dvars tvars =
+        either B F <$> nameWith {bound = tvars, avoid = dvars}

tests/Tests/Parser.idr

@@ -4,7 +4,9 @@ import Quox.Syntax
 import Quox.Parser
 import Quox.Lexer
 import Tests.Lexer
+import Quox.Pretty
 
+import TermImpls
 import Data.SnocVect
 import Text.Parser
 import TAP
@@ -50,21 +52,29 @@ Show a => ToInfo (Error a) where
   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 $
+parameters {c : Bool} (grm : Grammar c a) (note : String) (input : String)
+  parsesNote : (Show a, Eq a) => a -> Test
+  parsesNote exp = test "\"\{input}\"\{note}" $ 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
+  rejectsNote : Show a => Test
+  rejectsNote = test "\"\{input}\"\{note}  (reject)" $ do
     case lexParseAll grm input of
          Left  err => Right ()
          Right val => Left $ ShouldFail val
 
+parameters {c : Bool} (grm : Grammar c a) (input : String)
+  parses : (Show a, Eq a) => a -> Test
+  parses = parsesNote grm "" input
+
+  rejects : Show a => Test
+  rejects = rejectsNote grm "" input
+
 tests = "parser" :- [
+  skip $
   "numbers" :-
   let parses = parses number
   in [
@@ -73,8 +83,9 @@ tests = "parser" :- [
     parses "1000" 1000
   ],
 
+  skip $
   "bound vars (x, y, z ⊢)" :-
-  let grm = bound [< "x", "y", "z"]
+  let grm = bound "test" [< "x", "y", "z"]
       parses = parses grm; rejects = rejects grm
   in [
     parses  "x" (V 2),
@@ -85,8 +96,9 @@ tests = "parser" :- [
     rejects "a"
   ],
 
+  skip $
   "bound or free vars (x, y, z ⊢)" :-
-  let parses = parses $ nameWith [< "x", "y", "z"]
+  let parses = parses $ nameWith {bound = [< "x", "y", "z"], avoid = [<]}
   in [
     parses "x"         (Left (V 2)),
     parses "y"         (Left (V 1)),
@@ -98,7 +110,8 @@ tests = "parser" :- [
     parses "x.a"       (Right (MakeName [< "x"]      (UN "a")))
   ],
 
-  "dimension (x, y, z ⊢)" :-
+  skip $
+  "dimension (x, y, z | · ⊢)" :-
   let grm = dimension [< "x", "y", "z"]
       parses = parses grm; rejects = rejects grm
   in [
@@ -107,5 +120,20 @@ tests = "parser" :- [
     rejects "2",
     parses  "x" (B (V 2)),
     rejects "a"
+  ],
+
+  "terms & elims (i, j | x, y, z ⊢)" :-
+  let dvars = [< "i", "j"]; tvars = [< "x", "y", "z"]
+      tgrm = term {dvars, tvars}; egrm = elim {dvars, tvars}
+      tparses  = parsesNote  tgrm "  (term)"
+      eparses  = parsesNote  egrm "  (elim)"
+      trejects = rejectsNote tgrm "  (term)"
+      erejects = rejectsNote egrm "  (elim)"
+  in [
+    eparses  "a"   (F "a"),
+    eparses  "x"   (BV 2),
+    trejects "a",
+    tparses  "[a]" (FT "a"),
+    tparses  "[x]" (BVT 2)
   ]
 ]