[parser] pred i:A i:B is OK, while pred i:A i : B is not

This is a compromise, otherwise (pi i\ f i :- ..) is not accepted
LPCIC · Apr 18, 2022 · 8111a7d · 8111a7d
1 parent dfaf1c4
commit 8111a7d
Show file tree

Hide file tree

Showing 6 changed files with 21 additions and 4 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,3 +1,13 @@
+# v1.15.2 (April 2022)
+
+Requires Menhir 20211230 and OCaml 4.07 or above.
+Camlp5 8.0 or above is optional.
+
+*warning: The parser used by default is not backward compatible with 1.14.x*
+
+- Parser:
+  - Change `pred foo i:A o:B` is valid, `pred foo i:A o :B` is not. This
+    change restores backward compatibility of existing code.
 
 # v1.15.1 (April 2022)
 

diff --git a/src/parser/grammar.mly b/src/parser/grammar.mly
@@ -168,9 +168,7 @@ pred:
        mkApp (loc $loc(c)) [mkCon "->";t;ty]) args (mkCon "prop") }
  }
 pred_item:
-| io = i_o_colon; ty = type_term { (io,ty) }
-i_o_colon:
-| io = IO_COLON { mode_of_IO io }
+| io = IO_COLON; ty = type_term { (mode_of_IO io,ty) }
 
 kind:
 | KIND; names = separated_nonempty_list(CONJ,constant); k = kind_term {

diff --git a/src/parser/lexer.mll.in b/src/parser/lexer.mll.in
@@ -130,7 +130,7 @@ and token = parse
 | "}" { RCURLY }
 | "|" { PIPE }
 | "{{" { skip lexbuf 2; quoted 2 lexbuf }
-| (("i" | "o") as s) (' ' | '\t')* ':' { IO_COLON s }
+| (("i" | "o") as s) ':' { IO_COLON s }
 | ("i" | "o") as s { IO s }
 | "shorten" { SHORTEN }
 | "accumulate" { ACCUMULATE }

diff --git a/src/parser/test_lexer.ml b/src/parser/test_lexer.ml
@@ -195,5 +195,7 @@ a|}                                   [T(CONSTANT "b", 2, 1, 2);T(CONSTANT "c",
   (*    01234567890123456789012345 *)
   test  "i:"                          [T(IO_COLON 'i', 1, 0, 2)];
   test  "o:"                          [T(IO_COLON 'o', 1, 0, 2)];
+  test  "i :"                         [T(IO 'i', 1, 0, 1); T(COLON,1,0,3)];
+  test  "o :"                         [T(IO 'o', 1, 0, 1); T(COLON,1,0,3)];
   test  "i"                           [T(IO 'i', 1, 0, 1)];
   test  "o"                           [T(IO 'o', 1, 0, 1)];
diff --git a/tests/sources/io_colon.elpi b/tests/sources/io_colon.elpi
@@ -0,0 +1 @@
+main :- (pi i\ f i :- true) => f 1.
diff --git a/tests/suite/elpi_specific.ml b/tests/suite/elpi_specific.ml
@@ -283,3 +283,9 @@ X0 || X2 && X3 ==> X4
 [f X0, g X1, (a , b), a + b]
 |})))
   ()
+
+let () = declare "IO_COLON"
+  ~source_elpi:"io_colon.elpi"
+  ~description:"IO_COLON token"
+  ~typecheck:true
+  ()