From 50a2ec02cb48468515ca6b6cf5cabb924309c624 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 8 May 2022 20:03:05 +0200
Subject: [PATCH] parser stuff

---
 lib/Quox/Parser.idr    | 31 ++++++++++++++++++++++---------
 tests/Tests/Parser.idr | 34 ++++++++++++++++------------------
 2 files changed, 38 insertions(+), 27 deletions(-)

diff --git a/lib/Quox/Parser.idr b/lib/Quox/Parser.idr
index f1b36aa..7975688 100644
--- a/lib/Quox/Parser.idr
+++ b/lib/Quox/Parser.idr
@@ -87,9 +87,23 @@ find _  _                     = Nothing
 
 
 export
-bound : (what : String) -> Vars k -> Grammar True (Var k)
-bound what vs = terminal "bound \{what} variable" $
-                \case Name x => find1 vs x; _ => Nothing
+checkAvoid1 : Vars n -> String -> Grammar False ()
+checkAvoid1 avoid y =
+  when (isJust $ find1 avoid y) $
+    fail "wrong type of bound variable: \{show y}"
+
+export
+checkAvoid : Vars n -> Name -> Grammar False ()
+checkAvoid avoid (MakeName [<] (UN y)) = checkAvoid1 avoid y
+checkAvoid _     _                     = pure ()
+
+export
+bound : (what : String) -> (bound : Vars k) -> (avoid : Vars n) ->
+        Grammar True (Var k)
+bound what vs avoid = do
+  x <- terminal "bound \{what} variable" $ \case Name x => Just x; _ => Nothing
+  checkAvoid1 avoid x
+  maybe (fail "not in scope: \{x}") pure $ find1 vs x
 
 export
 sname : Grammar True String
@@ -106,24 +120,23 @@ nameWith : (bound : Vars k) -> (avoid : Vars n) ->
            Grammar True (Either (Var k) Name)
 nameWith bound avoid = do
   y <- qname
-  when (isJust $ find avoid y) $
-    fail "wrong type of bound variable: \{show y}"
+  checkAvoid avoid y
   pure $ maybe (Right y) Left $ find bound y
 
 
 export
-dimension : Vars d -> Grammar True (Dim d)
-dimension vs =
+dimension : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Dim d)
+dimension dvars tvars =
       K Zero <$  zero
   <|> K One  <$  one
-  <|> B      <$> bound "dimension" vs
+  <|> B      <$> bound "dimension" {bound = dvars, avoid = tvars}
 
 
 mutual
   export
   term : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Term d n)
   term dvars tvars =
-        E <$> squares (elim dvars tvars)
+        E <$> squares (elim {dvars, tvars})
 
   export
   elim : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Elim d n)
diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr
index 5d55ab6..dfd39bc 100644
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@@ -61,7 +61,7 @@ parameters {c : Bool} (grm : Grammar c a) (note : String) (input : String)
          Left  err => Left $ Parser err
 
   rejectsNote : Show a => Test
-  rejectsNote = test "\"\{input}\"\{note}  (reject)" $ do
+  rejectsNote = test "\"\{input}\"\{note} ‹reject›" $ do
     case lexParseAll grm input of
          Left  err => Right ()
          Right val => Left $ ShouldFail val
@@ -74,7 +74,6 @@ parameters {c : Bool} (grm : Grammar c a) (input : String)
   rejects = rejectsNote grm "" input
 
 tests = "parser" :- [
-  skip $
   "numbers" :-
   let parses = parses number
   in [
@@ -83,20 +82,19 @@ tests = "parser" :- [
     parses "1000" 1000
   ],
 
-  skip $
-  "bound vars (x, y, z ⊢)" :-
-  let grm = bound "test" [< "x", "y", "z"]
-      parses = parses grm; rejects = rejects grm
+  "bound vars (x, y, z | a ⊢)" :-
+  let grm = bound "test" {bound = [< "x", "y", "z"], avoid = [< "a"]}
+      parses = parses grm; rejects = rejects grm; rejectsNote = rejectsNote grm
   in [
     parses  "x" (V 2),
     parses  "y" (V 1),
     parses  "z" (V 0),
     rejects "M.x",
     rejects "x.a",
-    rejects "a"
+    rejectsNote " (avoid)"        "a",
+    rejectsNote " (not in scope)" "c"
   ],
 
-  skip $
   "bound or free vars (x, y, z ⊢)" :-
   let parses = parses $ nameWith {bound = [< "x", "y", "z"], avoid = [<]}
   in [
@@ -110,25 +108,25 @@ tests = "parser" :- [
     parses "x.a"       (Right (MakeName [< "x"]      (UN "a")))
   ],
 
-  skip $
-  "dimension (x, y, z | · ⊢)" :-
-  let grm = dimension [< "x", "y", "z"]
-      parses = parses grm; rejects = rejects grm
+  "dimension (i, j | x, y, z ⊢)" :-
+  let grm = dimension {dvars = [< "i", "j"], tvars = [< "x", "y", "z"]}
+      parses = parses grm; rejects = rejects grm; rejectsNote = rejectsNote grm
   in [
     parses  "0" (K Zero),
     parses  "1" (K One),
     rejects "2",
-    parses  "x" (B (V 2)),
-    rejects "a"
+    parses  "i" (B (V 1)),
+    rejectsNote " (tvar)"         "x",
+    rejectsNote " (not in scope)" "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)"
+      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),