Merge pull request #291 from LPCIC/2.0.3

fix parsing of ==>

CHANGES.md

@@ -1,3 +1,12 @@
+# v2.0.3 (November 2024)
+
+Requires Menhir 20211230 and OCaml 4.13 or above.
+
+- Parser:
+  - Fix parsing of infix `==>` so that `A,B ==> C,D` means `A, (B => (C,D))`
+    as it is intended to be.
+
+
 # v2.0.2 (November 2024)
 
 Requires Menhir 20211230 and OCaml 4.13 or above.

src/parser/ast.ml

@@ -146,6 +146,7 @@ let mkSeq ?loc (l : t list) =
  let rec aux = function
     [] -> assert false
   | [e] -> e
+  | { it = Parens it} :: tl -> aux (it :: tl)
   | hd::tl ->
       let tl = aux tl in
       { loc = Loc.merge hd.loc tl.loc; it = App({ it = Const Func.consf; loc = hd.loc },[hd;tl]) }
@@ -170,10 +171,20 @@ let mkApp loc = function
   | [] -> anomaly ~loc "empty application"
   | x::_ -> raise (NotInProlog(loc,"syntax error: the head of an application must be a constant or a variable, got: " ^ best_effort_pp x.it))
 
-let rec mkAppF loc (cloc, c) = function
-  | [] -> anomaly ~loc "empty application"
-  | { loc; it = App({it=Const ","; loc=cloc}, tl1)} ::tl when c="," -> mkAppF loc (cloc, ",") (tl1@tl)
-  | args -> { loc; it = App( { it = Const c; loc = cloc },args) }
+let mkAppF loc (cloc, c) l =
+  if l = [] then anomaly ~loc "empty application";
+  if c = "," then
+      { loc; it =
+        App({ it = Const c; loc = cloc },
+          List.concat_map (function 
+            | { loc; it = Parens { it = App({it=Const ","}, l)}} -> l
+            | { loc; it = App({it=Const ","}, l)} -> l
+            | x -> [x]
+        ) l) }
+  else
+    { loc; it = App({ it = Const c; loc = cloc },l) }
+
+
 
 let last_warn_impl = ref (Loc.initial "(dummy)")
 let warn_impl { it; loc } =

src/parser/grammar.mly

@@ -62,20 +62,36 @@ let desugar_macro loc lhs rhs =
         raise (ParseError(loc,"Illformed macro left hand side"))
 ;;
 
-let mkParens_if_impl loc t =
+let mkParens_if_impl_or_conj loc t =
   match t.it with
   | App({ it = Const c},_) when Func.(equal c implf) -> mkParens loc t
+  | App({ it = Const c},_) when Func.(equal c andf) -> mkParens loc t
   | _ -> t
 
 let mkApp loc = function
   | { it = Const c; loc = cloc } :: a :: { it = App ({ it = Const c1 }, args) } :: [] when Func.(equal c andf && equal c1 andf) ->
       mkAppF loc (cloc,c) (a :: args)
   | l -> mkApp loc l
 
-let mkAppF loc (cloc,c) = function
-  | a :: { it = App ({ it = Const c1 }, args) } :: [] when Func.(equal c andf && equal c1 andf) ->
-      mkAppF loc (cloc,c) (a :: args)
-  | l -> mkAppF loc (cloc,c) l
+let rec unparen = function
+  | [] -> []
+  | { it = Parens { it = App ({ it = Const c1 }, args) } } as x :: xs when Func.(equal c1 implf) -> x :: unparen xs
+  | { it = Parens x} :: xs -> x :: unparen xs
+  | x :: xs -> x :: unparen xs
+
+let mkAppF loc (cloc,c) l =
+  if Func.(equal c implf) then
+    match l with
+    | { it = App ({ it = Const j; loc = jloc }, args) } :: rhs when Func.(equal j andf) ->
+       begin match List.rev args with
+       | last :: ( { loc = dloc } :: _ as rest_rev) ->
+           let jloc = List.fold_left (fun x { loc } -> Loc.merge x loc) dloc rest_rev in
+           let iloc = List.fold_left (fun x { loc } -> Loc.merge x loc) last.loc rhs in
+           { it = App ({ it = Const j; loc = jloc },List.rev rest_rev @ [mkAppF iloc (cloc,c) (last :: rhs)]); loc = loc }
+       | _ -> mkAppF loc (cloc,c) l
+       end
+    | _ -> mkAppF loc (cloc,c) (unparen l)
+  else mkAppF loc (cloc,c) l
 
 let binder l (loc,ty,b) =
   match List.rev l with
@@ -371,7 +387,7 @@ closed_term:
 
 head_term:
 | t = constant { mkConst (loc $loc) t }
-| LPAREN; t = term; RPAREN { mkParens_if_impl (loc $loc) t }
+| LPAREN; t = term; RPAREN { mkParens_if_impl_or_conj (loc $loc) t }
 | LPAREN; t = term; COLON; ty = type_term RPAREN { mkCast (loc $loc) t ty }
 
 list_items:
@@ -430,7 +446,7 @@ clause_hd_term:
 
 clause_hd_closed_term:
 | t = constant { mkConst (loc $sloc) t }
-| LPAREN; t = term; RPAREN { mkParens_if_impl (loc $loc) t }
+| LPAREN; t = term; RPAREN { mkParens_if_impl_or_conj (loc $loc) t }
 
 clause_hd_open_term:
 | hd = PI; args = nonempty_list(constant_w_loc); b = binder_body { desugar_multi_binder (loc $loc) @@ mkApp (loc $loc) (mkConst (loc $loc(hd)) (Func.from_string "pi") :: binder args b) }

src/parser/lexer_config.ml

@@ -37,6 +37,7 @@ type fixed = {
   token : string;
   the_token : string;
   mk_token : Tokens.token;
+  comment : (int * string) option;
 }
 
 type mixfix_kind = Fixed of fixed | Extensible of extensible
@@ -46,18 +47,19 @@ type mixfix = {
   fixity : fixity;
 }
 
-let mkFix token the_token mk_token = Fixed { token; the_token; mk_token }
+let mkFix ?comment token the_token mk_token = Fixed { token; the_token; mk_token; comment }
 
 let mkExt token start ?(non_enclosed=false) ?(at_least_one_char=false) ?(fixed=[]) mk_token =
   Extensible { start; mk_token; token; non_enclosed; at_least_one_char; fixed }
 
+let comment = 1, "The LHS of ==> binds stronger than conjunction, hence (a,b ==> c,d) reads a, (b ==> (c,d))" 
 let mixfix_symbols : mixfix list = [
   { tokens = [ mkFix "VDASH" ":-" VDASH;
                mkFix "QDASH" "?-" QDASH];
     fixity = Infix };
   { tokens = [ mkFix "OR" ";" OR];
     fixity = Infixr };
-  { tokens = [ mkFix "DDARROW" "==>" DDARROW];
+  { tokens = [ mkFix ~comment "DDARROW" "==>" DDARROW];
     fixity = Infixr };
   { tokens = [ mkFix "CONJ" "," CONJ;
                mkFix "CONJ2" "&" CONJ2];

src/parser/parser_config.ml

@@ -71,9 +71,18 @@ let pp_non_enclosed fmt = function
 let pp_tok_list fmt l =
   List.iter (function
     | Extensible { start; fixed; non_enclosed; _ } -> Format.fprintf fmt "%a%s..%a @ " pp_fixed fixed start pp_non_enclosed non_enclosed
-    | Fixed { the_token; _ } -> Format.fprintf fmt "%s @ " the_token)
+    | Fixed { the_token; comment = None; _ } -> Format.fprintf fmt "%s @ " the_token
+    | Fixed { the_token; comment = Some (id,_); _ } -> Format.fprintf fmt "%s (* see note %d *) @ " the_token id)
     l
 
+let pp_tok_list_comments fmt l =
+  List.iter (function
+    | Extensible _ -> ()
+    | Fixed { comment = None; _ } -> ()
+    | Fixed { comment = Some (id,txt); _ } -> Format.fprintf fmt "%d: %s@ " id txt)
+    l
+
+
 let legacy_parser_compat_error =
   let open Format in
   let b = Buffer.create 80 in
@@ -140,6 +149,11 @@ let legacy_parser_compat_error =
   fprintf fmt "%s@;" "verify how the text was parsed. Eg:";
   fprintf fmt "%s@;" "";
   fprintf fmt "%s@;" "echo 'MyFormula = a || b ==> c && d' | elpi -parse-term";
+  fprintf fmt "%s@;" "";
+  fprintf fmt "%s@;" "Notes:";
+  List.iter (fun { tokens; _ } ->
+    fprintf fmt "%a" pp_tok_list_comments tokens;
+  ) mixfix_symbols;
   fprintf fmt "@]";
   pp_print_flush fmt ();
   Buffer.contents b

src/parser/test_parser.ml

@@ -179,6 +179,8 @@ let _ =
   test  "q && r x || s."    1 13 1 0 [] (app "||" 10 [app "&&" 3 [c 1 "q"; app "r" 6 [c 8 "x"]]; c 13 "s"]);
   (*    01234567890123456789012345 *)
   test  "f x ==> y."        1 9 1 0 []  (app "=>" ~len:3 5 [app "f" 1 [c 3 "x"]; c 9 "y"]);
+  test  "x, y ==> z, a."    1 13 1 0 [] (app "," 1 [c 1 "x"; app "=>" ~len:3 6 [c 4 "y"; app "," ~bug 11 [c 10 "z";c 13 "a"]]]);
+  test  "(x, y) ==> z, a."  1 15 1 0 [] (app "=>" ~len:3 8 [app "," ~bug 3 [c ~bug 2 "x"; c 5 "y"]; app "," ~bug 13 [c 12 "z";c 15 "a"]]);
   test  "x ==> y, z."       1 10 1 0 []  (app "=>" ~len:3 3 [c 1 "x"; app "," ~bug 8 [c 7 "y"; c 10 "z"]]);
   test  "x => y, z."        1 9 1 0 [] ~warns:".*infix operator" (app "," ~bug 7 [app "=>" 3 [c 1 "x";c 6 "y"];c 9 "z"]);
   test  "x => y, !."        1 9 1 0 [] (app "," ~bug 7 [app "=>" 3 [c 1 "x";c 6 "y"];c 9 "!"]);