From 4a98f8d21bb19a310354f868814ad0a57e187fc7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 27 Nov 2024 16:39:06 +0100 Subject: [PATCH] fix parsing of ==> --- CHANGES.md | 9 +++++++++ src/parser/ast.ml | 19 +++++++++++++++---- src/parser/grammar.mly | 30 +++++++++++++++++++++++------- src/parser/lexer_config.ml | 6 ++++-- src/parser/parser_config.ml | 16 +++++++++++++++- src/parser/test_parser.ml | 2 ++ 6 files changed, 68 insertions(+), 14 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 05ec02869..57008bba7 100644 --- a/CHANGES.md +++ b/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. diff --git a/src/parser/ast.ml b/src/parser/ast.ml index e5a244d4c..ae750e24e 100644 --- a/src/parser/ast.ml +++ b/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 } = diff --git a/src/parser/grammar.mly b/src/parser/grammar.mly index 2a061e41f..b4033c307 100644 --- a/src/parser/grammar.mly +++ b/src/parser/grammar.mly @@ -62,9 +62,10 @@ 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 @@ -72,10 +73,25 @@ let mkApp loc = function 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) } diff --git a/src/parser/lexer_config.ml b/src/parser/lexer_config.ml index 33ce2bcb1..07df386c8 100644 --- a/src/parser/lexer_config.ml +++ 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]; diff --git a/src/parser/parser_config.ml b/src/parser/parser_config.ml index abdcf00e6..66a6fe140 100644 --- a/src/parser/parser_config.ml +++ b/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 diff --git a/src/parser/test_parser.ml b/src/parser/test_parser.ml index 7c602947b..fb6d0005f 100644 --- a/src/parser/test_parser.ml +++ 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 "!"]);