From ede3291facb53f5c0f2baee24263711859bea196 Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Mon, 17 Mar 2025 11:44:42 +0100 Subject: [PATCH 01/14] update regression tester for ocaml 5.3 --- regression/Makefile | 8 ++++---- regression/regression.ml | 2 +- regression/regression_p_client.ml | 2 +- regression/regression_p_master.ml | 2 +- regression/regression_para.ml | 2 +- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/regression/Makefile b/regression/Makefile index da75cef..202cb98 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -36,11 +36,11 @@ all: regression regression: regression.ml - ocamlc unix.cma str.cma -o regression -dtypes regression.ml + ocamlc -I +unix -I +str unix.cma str.cma -o regression -dtypes regression.ml regression_p: regression_p_client.ml regression_p_master.ml - ocamlc unix.cma str.cma -o regression_p_client regression_p_client.ml - ocamlc unix.cma str.cma -o regression_p_master regression_p_master.ml + ocamlc -I +unix -I +str unix.cma str.cma -o regression_p_client regression_p_client.ml + ocamlc -I +unix -I +str unix.cma str.cma -o regression_p_master regression_p_master.ml regression_para: regression_para.ml ocamlp3lopt -par unix.cmxa str.cmxa -o regression_para regression_para.ml @@ -77,7 +77,7 @@ clean-regr: # Jenkins -# regression-jenkins: +# regression-jenkins: # ocamlc unix.cma str.cma -o regression-jenkins -dtypes regression-jenkins.ml run-jenkins: regression diff --git a/regression/regression.ml b/regression/regression.ml index 3cd122c..49759ca 100644 --- a/regression/regression.ml +++ b/regression/regression.ml @@ -92,7 +92,7 @@ let latex_regressions = ref 0 (* let twelf_progressions = ref 0 *) (* let twelf_regressions = ref 0 *) let summary = ref [] -let report_fd = ref Pervasives.stdout +let report_fd = ref Stdlib.stdout let config_state = ref [] let _ = diff --git a/regression/regression_p_client.ml b/regression/regression_p_client.ml index 4246cbf..83f5ed8 100644 --- a/regression/regression_p_client.ml +++ b/regression/regression_p_client.ml @@ -71,7 +71,7 @@ let latex_regressions = ref 0 let twelf_progressions = ref 0 let twelf_regressions = ref 0 let summary = ref [] -let report_fd = ref Pervasives.stdout +let report_fd = ref Stdlib.stdout (* let _ = *) (* putenv "CVSROOT" ":pserver:zappa@localhost:/usr/groups/netsem/dynsem/cvs"; *) diff --git a/regression/regression_p_master.ml b/regression/regression_p_master.ml index 5d21ab1..96d5160 100644 --- a/regression/regression_p_master.ml +++ b/regression/regression_p_master.ml @@ -67,7 +67,7 @@ let latex_progressions = ref 0 let latex_regressions = ref 0 let twelf_progressions = ref 0 let twelf_regressions = ref 0 -let report_fd = ref Pervasives.stdout +let report_fd = ref Stdlib.stdout (* let _ = *) (* if !night then begin *) diff --git a/regression/regression_para.ml b/regression/regression_para.ml index 7645a8f..3798a74 100644 --- a/regression/regression_para.ml +++ b/regression/regression_para.ml @@ -83,7 +83,7 @@ let latex_regressions = ref 0 let twelf_progressions = ref 0 let twelf_regressions = ref 0 let summary = ref [] -let report_fd = ref Pervasives.stdout +let report_fd = ref Stdlib.stdout let config_state = ref [] let _ = From b2b9863043f3ed5aa7fadb8ac750d5f0e0c61f82 Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Mon, 17 Mar 2025 12:46:00 +0100 Subject: [PATCH 02/14] update regression tester for coq 8.19+ --- regression/regression.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/regression.ml b/regression/regression.ml index 49759ca..2be9408 100644 --- a/regression/regression.ml +++ b/regression/regression.ml @@ -354,7 +354,7 @@ let run_test i n (tn,tl) = if (command cmd) = 0 then begin pp_success tgt name; - let cmd = "coqc -init-file _ott_coqrc.v "^name^".v > " ^ name ^ ".coq.out" (* was "/dev/null"*) in + let cmd = "coqc -Q ../coq Ott "^name^".v > " ^ name ^ ".coq.out" (* was "/dev/null"*) in let tgt = "Coq" in pp_tgt i_of_n tgt cmd; if (command cmd) = 0 then begin @@ -382,7 +382,7 @@ let run_test i n (tn,tl) = if (command cmd) = 0 then begin pp_success tgt name; - let cmd = "coqc -init-file _ott_coqrc.v "^name^".v" in + let cmd = "coqc -Q ../coq Ott "^name^".v" in let tgt = "Coq" in pp_tgt i_of_n tgt cmd; if (command cmd) = 0 then begin From f7ca37b5efc5d58bd80a59654568e434b2c8acfa Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Wed, 19 Mar 2025 12:05:12 +0100 Subject: [PATCH 03/14] exit with status code 1 on regression failure --- regression/regression.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/regression/regression.ml b/regression/regression.ml index 2be9408..c50bec9 100644 --- a/regression/regression.ml +++ b/regression/regression.ml @@ -575,7 +575,7 @@ let report tp a b = progressions := !progressions + 1; ott_progressions := !ott_progressions + 1 end else - if not a.ott && b.ott + if not a.ott && b.ott && not (a.tp = Skipped || b.tp = Skipped) then begin regressions := !regressions + 1; ott_regressions := !ott_regressions + 1 @@ -839,4 +839,6 @@ let _ = end; output_string fd "\n"; close_out fd - end + end; + + if !regressions != 0 then exit 1 From 3dc401bbdbc317b456acb264a9b39a34a96329ca Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Wed, 19 Mar 2025 15:21:15 +0100 Subject: [PATCH 04/14] add regression binary to gitignore --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 1f0ab2c..3ffc21f 100644 --- a/.gitignore +++ b/.gitignore @@ -20,3 +20,4 @@ ocamlgraph-1.7 .merlin make_merlin.sh ott.install +regression/regression From b773d5d0e5a228e75a195b228d2aeaacab32623f Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Wed, 19 Mar 2025 13:08:53 +0100 Subject: [PATCH 05/14] add subrule bound mixing and precondition test Co-authored-by: Joey Eremondi --- tests/test_lists_coq_defn_subrule_4.ott | 79 +++++++++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 tests/test_lists_coq_defn_subrule_4.ott diff --git a/tests/test_lists_coq_defn_subrule_4.ott b/tests/test_lists_coq_defn_subrule_4.ott new file mode 100644 index 0000000..0b2bf2a --- /dev/null +++ b/tests/test_lists_coq_defn_subrule_4.ott @@ -0,0 +1,79 @@ +% Mixing list bounds with subrules +% Should pass on all targets, but previous versions failed +% in Coq with "The variable tau_ is bound several times in pattern" +% due to an error in how bound were calculated for sub-non-terminals + +metavar var, X ::= {{ coq nat }} + +indexvar n ::= {{ coq nat }} + +grammar + +Kind, K :: kind_ ::= + | KindStar :: :: KindStar + +typexpr, T :: T_ ::= + | X :: :: var + | ForAll << X1 , .. , Xn >> . T :: :: polyarrow + | [ X1 |-> tau1 .. Xn |-> taun ] T :: M :: tsub {{ icho [[T]] }} + +tau, t :: tau_ ::= + | X :: :: var + +formula :: 'formula_' ::= + | judgement :: :: judgement + | formula1 .. formulan :: :: dots + +subrules + tau <:: T + +defns + Jtype :: '' ::= + +defn + |- t : K :: :: kind :: Kind +by + + ------------------------------------ :: Var + |- t : KindStar + +defn + is t :: :: Simpl :: '' +by + + ------------------------------------ :: Basic + is X + +defn + |- T <: T' :: :: sub :: Sub +by + + + ------------------------------------------ :: InstL + |- ForAll << >> . T <: [ taun // n /> ] T + + is t + ------------------------------------------ :: Sub + |- t <: X + +embed {{ coq + +Require Import List. +Import ListNotations. + +Lemma test_is_tau_premise_needed : + (sub (T_polyarrow nil (T_var 0)) (T_var 1)) -> Is_true (is_tau_of_typexpr (T_polyarrow [] (T_var 0))). +Proof. + intros. + inversion H. + assumption. +Qed. + +Theorem is_tau_required_for_kind : + forall t, kind t kind_KindStar -> Is_true (is_tau_of_typexpr t). +Proof. + intros. + inversion H. + assumption. +Qed. +}} From d3acdacf177bc11bfc97f3de753155198e18b732 Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Wed, 19 Mar 2025 14:06:29 +0100 Subject: [PATCH 06/14] coalesce subrule bounds and conditions --- src/bounds.ml | 81 +++++++++++++++++++++++++++++++++++++++++++++- src/subrules_pp.ml | 42 +++++++++++------------- 2 files changed, 99 insertions(+), 24 deletions(-) diff --git a/src/bounds.ml b/src/bounds.ml index 2959d16..6a19157 100644 --- a/src/bounds.ml +++ b/src/bounds.ml @@ -170,6 +170,84 @@ let split_bounded : f [] [] xbos +(* Coalesce nonterminals with the same name and compatible bounds *) +let coalesce_bounds xd loc x : ((nt_or_mv * subntr_data) * bound option) list = + (* Group by nonterminal name and suffix *) + let by_name_and_suffix = + Auxl.remove_duplicates + (List.map (fun (((ntmv, sf), _), _) -> (ntmv, sf)) x) + in + + (* Get all entries for a given nonterminal and suffix *) + let entries_for ntmv sf = + List.filter (fun (((nm, sf'), _), _) -> nm = ntmv && sf = sf') x + in + + (* Check if two subntr_data are compatible *) + let compatible_subntr_data d1 d2 = match (d1, d2) with + | (None, _) | (_, None) -> true + | (Some (ntrl1, ntrt1), Some (ntrl2, ntrt2)) -> + ntrl1 = ntrl2 && ntrt1 = ntrt2 + in + + (* Check if two bounds are compatible *) + let compatible_bounds b1 b2 = match (b1, b2) with + | (None, _) | (_, None) -> true + | (Some b1, Some b2) -> b1 = b2 + in + + (* Merge entries for a nonterminal *) + let merge_entries entries = + let rec find_best_entry remaining best = + match remaining with + | [] -> best + | entry :: rest -> + let (((_, _), sd), bo) = entry in + let (((_, _), best_sd), best_bo) = best in + + (* Prefer entries with subrule data over those without *) + let better = + match sd, best_sd with + | Some _, None -> true + | None, Some _ -> false + | _, _ -> + (* If both have or don't have subrule data, prefer those with bounds *) + match bo, best_bo with + | Some _, None -> true + | None, Some _ -> false + | _, _ -> false + in + + find_best_entry rest (if better then entry else best) + in + + match entries with + | [] -> failwith "Empty entries list in coalesce_bounds" + | first :: rest -> find_best_entry rest first + in + + (* Process each nonterminal and suffix pair *) + List.map (fun (ntmv, sf) -> + let entries = entries_for ntmv sf in + + (* Check for incompatible entries *) + List.iter (fun e1 -> + List.iter (fun e2 -> + let ((_, sd1), bo1) = e1 in + let ((_, sd2), bo2) = e2 in + + if not (compatible_subntr_data sd1 sd2) then + raise (Bounds (loc, "incompatible subntr_data for nonterminal " ^ + (Grammar_pp.pp_nt_or_mv Types.pp_ascii_opts_default xd (ntmv, sf)))) + else if not (compatible_bounds bo1 bo2) then + raise (Bounds (loc, "incompatible bounds for nonterminal " ^ + (Grammar_pp.pp_nt_or_mv Types.pp_ascii_opts_default xd (ntmv, sf)))) + ) entries + ) entries; + + merge_entries entries + ) by_name_and_suffix + (*invert, calculating, for each bound, the nt_or_mv that have that bound*) let nt_or_mv_per_bound : ((nt_or_mv*subntr_data) * bound ) list -> (bound * (nt_or_mv*subntr_data) list) list @@ -325,7 +403,8 @@ let dotenv23 ntmvsn_without_bounds ntmvsn_with_bounds = let bound_extraction m xd loc sts : dotenv * dotenv3 * string = try - let x = nt_or_mv_of_symterms sts in + let x_raw = nt_or_mv_of_symterms sts in + let x = coalesce_bounds xd loc x_raw in let bounds = check_length_consistency loc x in let pp_bounds = String.concat " " (List.map Grammar_pp.pp_plain_bound bounds) in diff --git a/src/subrules_pp.ml b/src/subrules_pp.ml index 002ccec..19c7570 100644 --- a/src/subrules_pp.ml +++ b/src/subrules_pp.ml @@ -117,30 +117,26 @@ let pp_subrules m xd srs : int_funcs_collapsed = let rec pp_subelement = fun sie de isa_list_name_flag pu srl sru el eu -> match el,eu with Lang_nonterm (ntrpl,ntl), Lang_nonterm (ntrpu,ntu) -> - (* TODO: THIS IS PROBABLY WRONG WRONG WRONG *) -(* if (ntrpl=ntrpu) then *) -(* try *) -(* let ntr_upper = List.assoc ntrpl non_free_ntrs in *) -(* [ "(" ^ (Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)) ^ " " *) -(* ^ Grammar_pp.pp_nonterm_with_sie m xd sie ntu *) -(* ^ ")"], [Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)], [] *) -(* with Not_found -> [],[],[] *) -(* else if *) -(* List.exists *) -(* (function sr -> sr.sr_lower=ntrpl && sr.sr_upper=ntrpu) *) -(* xd.xd_srs *) -(* then *) -(* [ "(" ^ (Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)) ^ " " *) -(* ^ Grammar_pp.pp_nonterm_with_sie m xd sie ntu ^")"], *) -(* [Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)], [] *) -(* else [],[],[] *) - - (try - let ntr_upper = List.assoc ntrpl non_free_ntrs in - [ "(" ^ (Auxl.pp_is ntrpl ntr_upper) ^ " " + (* Check if there's a direct subrule relationship *) + let direct_subrule = + List.exists + (function sr -> sr.sr_lower=ntrpl && sr.sr_upper=ntrpu) + xd.xd_srs + in + + if direct_subrule then + [ "(" ^ (Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)) ^ " " ^ Grammar_pp.pp_nonterm_with_sie m xd sie ntu - ^ ")"], [Auxl.pp_is ntrpl ntr_upper], [] - with Not_found -> [],[],[]) + ^ ")"], [Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)], [] + else + (* Try to find the top-level nonterminal for this subrule *) + (try + let ntr_upper = List.assoc ntrpl non_free_ntrs in + let promoted_upper = Auxl.promote_ntr xd ntr_upper in + [ "(" ^ (Auxl.pp_is ntrpl promoted_upper) ^ " " + ^ Grammar_pp.pp_nonterm_with_sie m xd sie ntu + ^ ")"], [Auxl.pp_is ntrpl promoted_upper], [] + with Not_found -> [],[],[]) | Lang_metavar _, Lang_metavar _ -> [],[],[] | Lang_terminal _, Lang_terminal _ -> [],[],[] From 803bce7c6d293fdac589473d28db17e98c106e9c Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Thu, 20 Mar 2025 03:56:25 +0100 Subject: [PATCH 07/14] fix subrule aliasing in premise generation --- src/defns.ml | 13 ++++++++++++- src/subrules_pp.ml | 17 ++++++++++++++--- 2 files changed, 26 insertions(+), 4 deletions(-) diff --git a/src/defns.ml b/src/defns.ml index 90727f6..5a04aa9 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -258,7 +258,18 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = let ntr_upper = List.assoc ntr non_free_ntrs in Some (ntr,ntr_upper,(ntr,suffix)) with - Not_found -> None) + Not_found -> + (* Try with the primary nonterminal to handle aliases *) + let primary_ntr = + try Auxl.primary_ntr_of_ntr xd ntr + with Not_found -> ntr in + if primary_ntr = ntr then None + else + try + let ntr_upper = List.assoc primary_ntr non_free_ntrs in + Some (primary_ntr,ntr_upper,(ntr,suffix)) + with + Not_found -> None) | (Ntr ntr,suffix),Some(ntrl,ntru) -> Some (ntrl,ntru,(ntr,suffix)) | (Mvr mvr,suffix),_ -> None) ntmvsns in diff --git a/src/subrules_pp.ml b/src/subrules_pp.ml index 19c7570..5638bb0 100644 --- a/src/subrules_pp.ml +++ b/src/subrules_pp.ml @@ -117,10 +117,16 @@ let pp_subrules m xd srs : int_funcs_collapsed = let rec pp_subelement = fun sie de isa_list_name_flag pu srl sru el eu -> match el,eu with Lang_nonterm (ntrpl,ntl), Lang_nonterm (ntrpu,ntu) -> - (* Check if there's a direct subrule relationship *) + (* Check if there's a direct subrule relationship, checking both the nonterminal + and its primary form to handle alias cases *) let direct_subrule = + let primary_ntrpl = + try Auxl.primary_ntr_of_ntr xd ntrpl + with Not_found -> ntrpl in List.exists - (function sr -> sr.sr_lower=ntrpl && sr.sr_upper=ntrpu) + (function sr -> + (sr.sr_lower=ntrpl || sr.sr_lower=primary_ntrpl) && + sr.sr_upper=ntrpu) xd.xd_srs in @@ -131,7 +137,12 @@ let pp_subrules m xd srs : int_funcs_collapsed = else (* Try to find the top-level nonterminal for this subrule *) (try - let ntr_upper = List.assoc ntrpl non_free_ntrs in + let primary_ntrpl = + try Auxl.primary_ntr_of_ntr xd ntrpl + with Not_found -> ntrpl in + let ntr_upper = + try List.assoc ntrpl non_free_ntrs + with Not_found -> List.assoc primary_ntrpl non_free_ntrs in let promoted_upper = Auxl.promote_ntr xd ntr_upper in [ "(" ^ (Auxl.pp_is ntrpl promoted_upper) ^ " " ^ Grammar_pp.pp_nonterm_with_sie m xd sie ntu From bb7fe10d959620b16228073726325ffcf8b8f940 Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Mon, 24 Mar 2025 14:38:50 +0100 Subject: [PATCH 08/14] update regression baseline --- regression/baseline-2025-03.bl | Bin 0 -> 5268 bytes regression/baseline-2025-03.txt | 103 ++++++++++++++++++++++++++++++++ regression/baseline-jenkins.txt | 102 +++++++++++++++++++++++++++++++ regression/regression.otl | 1 + 4 files changed, 206 insertions(+) create mode 100644 regression/baseline-2025-03.bl create mode 100644 regression/baseline-2025-03.txt create mode 100644 regression/baseline-jenkins.txt diff --git a/regression/baseline-2025-03.bl b/regression/baseline-2025-03.bl new file mode 100644 index 0000000000000000000000000000000000000000..55f75748bcc446ad0fd46614b30a4ec4736df7ff GIT binary patch literal 5268 zcmb7|dz4jG9mi+R`3;4FU}6edi@;U9?l1$)3&8-j)l$-QN#!GNcV^CI?sQ+=hs}r> z35pup4+W&8I%1FkiL0cS7A_b%cHP-QjERi&m*p~6WlTvZ$El1~8RfboCs#|8{gGrMUx>z1-HD~e zL}AcdY2iY3Ymif1_w?%MRDU*7$i>omKMG%XlT%fus!TCcxNcirjAswkDJm0G#;csH zGRt-6R!g&Fop5rkp8h12_p5xgv_xr{GhBC8RfMmctTIXETryT^R{3~sg<4y@DI+Q~ zRF;$`K2hbuq2)KFY;B45Wl~;x(xK9>5>=U~@>!M3Y7L`K-)*E4y;*O{8Rq0X5sKiv3t6a&xPOL5jGe_fz9Dnx3 zl5sB#=a;Ljp&%;Ps;sUni(kKlN}tL)3Zim>%FT7cS>B8o&Z*o^ElPQAsuRxkgez38 zQrSuoR2-Ept~;mN@a%3+xlv_<%6gSsOBwF0n{tjP#Gb0`A$^rWl^@hqx2@UVW(Zgy(`&15+xXK+W ze+ZHKY2osxDle(*RN0~O7uRjCu2fs|9KTlBd|c%S$*b&E`B#{>$14{;f2VSk>{T98 z`EQuE*VAJ31#M~^N&YJP7}1xiuW@TzbDJl|>fex@Km}BuVl*~H>~%2X^;IMvpav?> zGnx=0?(k;D>|01aLKRg0%;>Z_al60A#%)vMd!dy=sJz0cIYjR5v+>*1_&zwDTBy9q zs53Y2*EML?7aL2o5s-U|m30V9BB_S;xb47z0yb zO6|9fKfN(-jRMm%UV|fy`If5wGV)K6#f`KU0Nutq1LniLTD5k&k zEYLixOTbiRqw7w|59TA?nM{&5xV0QiGIv5R+ySoZPBofXE>Y++qHDpJ{w}0p2W)rU z=|)sc7Y4IVuaSKPZiXMi0PKc)UANiDvc;T}Po%O*$0)xFn}C*JZH0&6LD!vTl!Zax zoAI;-ehF(~A3Vx;p;6^Cxk4r$FD8?fS&hA&@LSjePr(i^mqO87n&x8t3?2b<_30Vb zb6zeblf`c1@F(yv{1vtXox*yND{0owWr|Dtl7rQY8(!=A=}*Vy!Hn|^K6)$LyB zffY&M3+{%O zShwc#r<~kUhu4B>bd}X3K@WM7uwTLJzzu literal 0 HcmV?d00001 diff --git a/regression/baseline-2025-03.txt b/regression/baseline-2025-03.txt new file mode 100644 index 0000000..54ea8ae --- /dev/null +++ b/regression/baseline-2025-03.txt @@ -0,0 +1,103 @@ + Coq CoqNL Isa HOL OCaml LaTeX + - - - + + - + + ../tests/leroy-jfp96.ott + - - - - - + + ../tests/test-j.ott + + - + - + - + - + - + + ../tests/test-lj-list_ambiguity.ott + + + + + - - - + - ../tests/test-mjp-trans.ott + + - + - + - + - + - + + ../tests/test-mjp.ott + + + + + + + + + + + + + ../tests/test-pottier1.ott + + + + + + + + + + - + + ../tests/test1.ott + + + + + + + + + + + + + ../tests/test10.ott + + + + + + + + + - + + ../tests/test10_homs.ott + + + + + + + - - + + ../tests/test10_isasyn.ott + + + + + + + + + - + + ../tests/test10st.ott + + - + - + - - - + + ../tests/test10st_fe.ott + + + + + + + + + - + + ../tests/test10st_first_half.ott + + + + + + + + + + + + + ../tests/test11.ott + + + + + + + + + + + + + ../tests/test12.ott + + + + + + + + + + + + + ../tests/test13.ott + + - + - + - + - + + + + ../tests/test13b.ott + + + + + + + + + + + + + ../tests/test14.ott + + + + + + + + + + + + + ../tests/test15.0.ott + + + + + + + + + + + + + ../tests/test15.1.ott + + + + + + + + + + + + + ../tests/test15.2.ott + + + + + + + + + + + + + ../tests/test15.3.ott + + + + + + + + + + + + + ../tests/test15.4.ott + + + + + + + + + + + + + ../tests/test15.4b.ott + + + + + + + + + + + + + ../tests/test15.4c.ott + + + + + + + + + + + + + ../tests/test15.4d.ott + + + + + + + + + + + + + ../tests/test15.5.ott + + + + + + + + + + + + + ../tests/test15.6.ott + + + + + + + + + + + + + ../tests/test15.7.ott + + + + + + + + + + + + + ../tests/test16.0.ott + + + + + + + + + + + + + ../tests/test16.1.ott + + + + + + + + + + + + + ../tests/test16.2.ott + + + + + + + + + + + + + ../tests/test16.3.ott + + + + + + + + + + + + + ../tests/test16.4.ott + + + + + + + + + + + + + ../tests/test16.5.ott + + + + + + + + + + + + + ../tests/test16.6.ott + + + + + + + + + + + + + ../tests/test17.0.ott + + + + + + + + + + + + + ../tests/test17.1.ott + + + + + + - + + - + + ../tests/test17.10.ott + + - + - + - + + - + + ../tests/test17.11.ott + + + + + + - + + - + + ../tests/test17.12.ott + + + + + + + + + + + + + ../tests/test17.13.ott + + + + + + + + + + + + + ../tests/test17.14.ott + + + + + + + + + + + + + ../tests/test17.2.ott + + + + + + + + + + + + + ../tests/test17.3.ott + + + + + + + + + + + + + ../tests/test17.4.ott + + + + + + + + + + + + + ../tests/test17.5.ott + + + + + + + + + + + + + ../tests/test17.6.ott + + + + + + + + + + + + + ../tests/test17.7.ott + + + + + + - + + + + + + ../tests/test17.8.ott + + + + + + - + + + + + + ../tests/test17.9.ott + + + + + + + + + + + + + ../tests/test18.0.ott + + + + + + + + + + + + + ../tests/test18.1.ott + + + + + + + + + + + + + ../tests/test18.2.ott + + - + - + - + + - + + ../tests/test19.0.ott + + + + + + + + - + + + + ../tests/test2.ott + - - - - - + + ../tests/test3.ott + + + + + + + + - + - + + ../tests/test4.ott + - - - - - + + ../tests/test5.ott + - - - - - + + ../tests/test6-tex.ott + - - - - - + + ../tests/test6.ott + + - + - + + + + + + + + ../tests/test8.ott + - - - - - + + ../tests/test8p.ott + - - - - - + + ../tests/test_jan_2006-09-08.ott + + - + - + - + - - + + ../tests/test_lists_1.ott + + + + + + + + - + + + + ../tests/test_lists_freevars_1.ott + + + + + + + + + - + + sys-bool + + + + + + + + + - + + sys-arith + + + + + + + + + - + + sys-untyped + + + + + + - + - - + + sys-puresimple + + + + + + + + + - + + sys-tybool + + + + + + - + + - + - sys-sortoffullsimple + + - + - + - + - - + + sys-tuple + + + + + + + + + - + + sys-puresub + + + + + + - + + - + - sys-roughlyfullsimple + + - + - + - + + - + + sys-purercdsub + - - - - - - ../tests/test_bind_aux_empty_1.ott + - - - - - - ../tests/test_bind_dots_1.ott + + + + + + - + - + - + + ../tests/test_bind_isa_1.ott + + + + + + + + - + + + + ../tests/test_coq_equality_x_1.ott + + + + + + - + - + + + + ../tests/test_defn_repeated_nonterminal_1.ott + + + + + + + + + + + + + ../tests/test_embed_top_1.ott + + - + - + - + - + + + + ../tests/test_empty_defn.ott + + - + - + - + - - + + ../tests/test_lists_1.ott + + + + + + - + - + + + + ../tests/test_lists_coq_bind_1.ott + + + + + + + + + + + + + ../tests/test_lists_coq_defn_subrule_1.ott + + + + + + + + + + + + + ../tests/test_lists_coq_defn_subrule_2.ott + + + + + + - + + + + + + ../tests/test_lists_coq_defn_subrule_3.ott + + + + + + - + - + - + + ../tests/test_lists_coq_defn_subrule_4.ott + + + + + + - + - + + + + ../tests/test_lists_coq_defn_tuple_1.ott + + + + + + - + + + + + + ../tests/test_lists_coq_defn_tuple_2.ott + + + + + + - + - - + - ../tests/test_lists_coq_list_functions_1.ott + + + + + + - + + + + + + ../tests/test_lists_coq_list_functions_2.ott + + + + + + - + - + + + + ../tests/test_lists_defn_list_form_1.ott + + - + - + - + + - + + ../tests/test_lists_coq_list_functions_3.ott + + - + - + - + + + + + + ../tests/test_lists_coq_list_functions_4.ott + + + + + + - + - + + + + ../tests/test_subrules_1.ott + - - - - - - ../tests/test_lists_terminal_1.ott + + + + + + - + + - + + ../tests/test_embed_location_1.ott + + + + + + + + + + + + + ../tests/test_embed_top_1.ott + + + + + + + + + + + + + ../tests/test_merge_embed_location_1-1.ott + + + + + + - + + - + + ../tests/test_merge_embed_location_1-2.ott diff --git a/regression/baseline-jenkins.txt b/regression/baseline-jenkins.txt new file mode 100644 index 0000000..d294265 --- /dev/null +++ b/regression/baseline-jenkins.txt @@ -0,0 +1,102 @@ + Coq CoqNL Isa HOL OCaml LaTeX + - - - + - - + + ../tests/leroy-jfp96.ott + - - - - - + + ../tests/test-j.ott + + - + - + - + - + - + + ../tests/test-lj-list_ambiguity.ott + + + + - - - - + - ../tests/test-mjp-trans.ott + + - + - + - + - + - + + ../tests/test-mjp.ott + + + + - + - + + + + + + ../tests/test-pottier1.ott + + + + - + - + + + - + + ../tests/test1.ott + + + + - + - + + + + + + ../tests/test10.ott + + + + - + - + + - + + ../tests/test10_homs.ott + + + + - + - - - + + ../tests/test10_isasyn.ott + + + + - + - + + - + + ../tests/test10st.ott + + - + - + - - - + + ../tests/test10st_fe.ott + + + + - + - + + - + + ../tests/test10st_first_half.ott + + + + - + - + + + + + + ../tests/test11.ott + + + + - + - + + + + + + ../tests/test12.ott + + + + - + - + + + + + + ../tests/test13.ott + + - + - + - + - + + + + ../tests/test13b.ott + + + + - + - + + + + + + ../tests/test14.ott + + + + - + - + + + + + + ../tests/test15.0.ott + + + + - + - + + + + + + ../tests/test15.1.ott + + + + - + - + + + + + + ../tests/test15.2.ott + + + + - + - + + + + + + ../tests/test15.3.ott + + + + - + - + + + + + + ../tests/test15.4.ott + + + + - + - + + + + + + ../tests/test15.4b.ott + + + + - + - + + + + + + ../tests/test15.4c.ott + + + + - + - + + + + + + ../tests/test15.4d.ott + + + + - + - + + + + + + ../tests/test15.5.ott + + + + - + - + + + + + + ../tests/test15.6.ott + + + + - + - + + + + + + ../tests/test15.7.ott + + + + - + - + + + + + + ../tests/test16.0.ott + + + + - + - + + + + + + ../tests/test16.1.ott + + + + - + - + + + + + + ../tests/test16.2.ott + + + + - + - + + + + + + ../tests/test16.3.ott + + + + - + - + + + + + + ../tests/test16.4.ott + + + + - + - + + + + + + ../tests/test16.5.ott + + + + - + - + + + + + + ../tests/test16.6.ott + + + + - + - + + + + + + ../tests/test17.0.ott + + + + - + - + + + + + + ../tests/test17.1.ott + + + + - + - + + - + + ../tests/test17.10.ott + + + + - + - + + - + + ../tests/test17.11.ott + + + + - + - + + - + + ../tests/test17.12.ott + + + + - + - + + + + + + ../tests/test17.13.ott + + + + - + - + + + + + + ../tests/test17.14.ott + + + + - + - + + + + + + ../tests/test17.2.ott + + + + - + - + + + + + + ../tests/test17.3.ott + + + + - + - + + + + + + ../tests/test17.4.ott + + + + - + - + + + + + + ../tests/test17.5.ott + + + + - + - + + + + + + ../tests/test17.6.ott + + + + - + - + + + + + + ../tests/test17.7.ott + + + + - + - + + + + + + ../tests/test17.8.ott + + + + - + - + + + + + + ../tests/test17.9.ott + + + + - + - + + + + + + ../tests/test18.0.ott + + + + - + - + + + + + + ../tests/test18.1.ott + + + + - + - + + + + + + ../tests/test18.2.ott + + + + - + - + + - + + ../tests/test19.0.ott + + + + - + - + - + + + + ../tests/test2.ott + - - - - - + + ../tests/test3.ott + + + + - + - + - + - + + ../tests/test4.ott + - - - - - + + ../tests/test5.ott + - - - - - + + ../tests/test6-tex.ott + - - - - - + + ../tests/test6.ott + + - + - + - + + + + + + ../tests/test8.ott + - - - - - + + ../tests/test8p.ott + - - - - - + + ../tests/test_jan_2006-09-08.ott + + - + - + - + - - + + ../tests/test_lists_1.ott + + + + - + - + - + + + + ../tests/test_lists_freevars_1.ott + + - + - + - + + - + + sys-bool + + - + - + - + + - + + sys-arith + + - + - + - + + - + + sys-untyped + + - + - + - + - - + + sys-puresimple + + - + - + - + + - + + sys-tybool + + - + - + - + + - + - sys-sortoffullsimple + + - + - + - + - - + + sys-tuple + + - + - + - + + - + + sys-puresub + + - + - + - + + - + - sys-roughlyfullsimple + + - + - + - + + - + + sys-purercdsub + - - - - - - ../tests/test_bind_aux_empty_1.ott + - - - - - - ../tests/test_bind_dots_1.ott + + + + - + - + - + - + + ../tests/test_bind_isa_1.ott + + + + - + - + - + + + + ../tests/test_coq_equality_x_1.ott + + + + - + - + - + + + + ../tests/test_defn_repeated_nonterminal_1.ott + + + + - + - + + + + + + ../tests/test_embed_top_1.ott + + - + - + - + - + + + + ../tests/test_empty_defn.ott + + - + - + - + - - + + ../tests/test_lists_1.ott + + + + - + - + - + + + + ../tests/test_lists_coq_bind_1.ott + + - + - + - + + + + + + ../tests/test_lists_coq_defn_subrule_1.ott + + + + - + - + + + + + + ../tests/test_lists_coq_defn_subrule_2.ott + + + + - + - + + + + + + ../tests/test_lists_coq_defn_subrule_3.ott + + - + - + - + - + + + + ../tests/test_lists_coq_defn_tuple_1.ott + + + + - + - + - + + + + ../tests/test_lists_coq_defn_tuple_2.ott + + - + - + - + - - + - ../tests/test_lists_coq_list_functions_1.ott + + + + - + - + + + + + + ../tests/test_lists_coq_list_functions_2.ott + + + + - + - + - + + + + ../tests/test_lists_defn_list_form_1.ott + + - + - + - + + - + + ../tests/test_lists_coq_list_functions_3.ott + + - + - + - + + + + + + ../tests/test_lists_coq_list_functions_4.ott + + + + - + - + - + + + + ../tests/test_subrules_1.ott + - - - - - - ../tests/test_lists_terminal_1.ott + + + + - + - + + - + + ../tests/test_embed_location_1.ott + + + + - + - + + + + + + ../tests/test_embed_top_1.ott + + + + - + - + + + + + + ../tests/test_merge_embed_location_1-1.ott + + + + - + - + + - + + ../tests/test_merge_embed_location_1-2.ott diff --git a/regression/regression.otl b/regression/regression.otl index 04d939d..dbc546b 100644 --- a/regression/regression.otl +++ b/regression/regression.otl @@ -86,6 +86,7 @@ sys-purercdsub : ../examples/tapl/common.ott ../examples/tapl/common_typing.ott ../tests/test_lists_coq_defn_subrule_1.ott ../tests/test_lists_coq_defn_subrule_2.ott ../tests/test_lists_coq_defn_subrule_3.ott +../tests/test_lists_coq_defn_subrule_4.ott ../tests/test_lists_coq_defn_tuple_1.ott ../tests/test_lists_coq_defn_tuple_2.ott ../tests/test_lists_coq_list_functions_1.ott From 559b1f07a76ec5bd31aef09b4a5f219d8baa3ac6 Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Thu, 27 Mar 2025 00:14:45 +0100 Subject: [PATCH 09/14] pin coq to 8.20 in github action --- .github/workflows/docker-action.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 0a7614b..2729929 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -14,7 +14,7 @@ jobs: strategy: matrix: image: - - 'coqorg/coq:dev' + - 'coqorg/coq:8.20' fail-fast: false steps: - uses: actions/checkout@v4 From b887eacf67ec1775324644dd58315eae81e5c042 Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Thu, 20 Mar 2025 09:22:37 +0100 Subject: [PATCH 10/14] add failing menhir subrules tests --- tests/menhir_tests/test_subrules/Makefile | 47 +++++++++++++++++++ tests/menhir_tests/test_subrules/main.ml | 27 +++++++++++ .../test_subrules/test_subrules.ott | 37 +++++++++++++++ 3 files changed, 111 insertions(+) create mode 100644 tests/menhir_tests/test_subrules/Makefile create mode 100644 tests/menhir_tests/test_subrules/main.ml create mode 100644 tests/menhir_tests/test_subrules/test_subrules.ott diff --git a/tests/menhir_tests/test_subrules/Makefile b/tests/menhir_tests/test_subrules/Makefile new file mode 100644 index 0000000..24d4d84 --- /dev/null +++ b/tests/menhir_tests/test_subrules/Makefile @@ -0,0 +1,47 @@ +# make -C ../.. && make clean && make + +ROOT := test_subrules + +OTTDIR := ../../.. + +OTT := $(OTTDIR)/bin/ott + +MENHIR_EXTRA_LIB:= $(OTTDIR)/menhir/menhir_library_extra.mly + +MENHIR := menhir + +MENHIRFLAGS := --infer --explain --unused-tokens --trace --base $(ROOT)_parser + +OCAMLBUILD := ocamlbuild -use-ocamlfind -package pprint \ + -use-menhir -menhir "$(MENHIR) $(MENHIRFLAGS) ../$(MENHIR_EXTRA_LIB) " + +MAIN := main + +all: $(ROOT)_ast.ml $(ROOT)_parser.mly $(ROOT)_parser_pp.ml $(ROOT)_lexer.mll main.ml + $(OCAMLBUILD) $(MAIN).byte + +pdf: $(ROOT)_quotiented.pdf $(ROOT)_unquotiented.pdf + +# generate the ocaml AST type, ocamllex lexer, menhir parser, and ocaml pretty printers for the AST, all from the Ott soruce +$(ROOT)_ast.ml $(ROOT)_lexer.mll $(ROOT)_parser.mly $(ROOT)_parser_pp.ml $(ROOT)_ast.tex : $(ROOT).ott + $(OTT) -show_sort true -quotient_rules false -i $(ROOT).ott -o $(ROOT)_parser.mly -o $(ROOT)_lexer.mll -o $(ROOT)_ast.ml -o $(ROOT).tex + +$(ROOT)_quotiented.pdf: $(ROOT).ott Makefile + $(OTT) -quotient_rules true -i $(ROOT).ott -o $(ROOT)_quotiented.tex + pdflatex $(ROOT)_quotiented.tex + +$(ROOT)_unquotiented.pdf: $(ROOT).ott Makefile + $(OTT) -quotient_rules false -i $(ROOT).ott -o $(ROOT)_unquotiented.tex + pdflatex $(ROOT)_unquotiented.tex + +clean: + rm -rf *~ + rm -rf _build + rm -rf $(ROOT)_ast.ml $(ROOT)_parser.mly $(ROOT)_lexer.mll $(ROOT)_parser_pp.ml + rm -rf *.aux *.log *.tex + rm -rf main.native main.byte + $(OCAMLBUILD) -clean + +realclean: + $(MAKE) clean + rm -rf *.pdf diff --git a/tests/menhir_tests/test_subrules/main.ml b/tests/menhir_tests/test_subrules/main.ml new file mode 100644 index 0000000..fb6c2cd --- /dev/null +++ b/tests/menhir_tests/test_subrules/main.ml @@ -0,0 +1,27 @@ +open Test_subrules_ast + +module Lexer = Test_subrules_lexer +module Parser = Test_subrules_parser +module PP = Test_subrules_parser_pp + +let process (line : string) = + let linebuf = Lexing.from_string line in + try + (* Run the parser on this line of input. *) + let t = (Parser.expr_start Lexer.token linebuf) in + Printf.printf " "; PPrint.ToChannel.compact stdout (PP.pp_raw_expr t); Printf.printf "\n"; + Printf.printf " "; PPrint.ToChannel.compact stdout (PP.pp_expr t); Printf.printf "\n" + with + | Lexer.Error msg -> + Printf.fprintf stdout "%s" msg + | Parser.Error -> + Printf.fprintf stdout "%s^\nAt offset %d: syntax error.\n" (String.make (Lexing.lexeme_start linebuf) ' ') (Lexing.lexeme_start linebuf) + +let () = Printf.printf "Enter a Test_subrules expression:\n" + +let rec run () = + let s = read_line () in + process s; flush stdout; + run () + +let () = run () diff --git a/tests/menhir_tests/test_subrules/test_subrules.ott b/tests/menhir_tests/test_subrules/test_subrules.ott new file mode 100644 index 0000000..42ee7ce --- /dev/null +++ b/tests/menhir_tests/test_subrules/test_subrules.ott @@ -0,0 +1,37 @@ +metavar nat, k ::= + {{ com natural numbers }} + {{ lex numeral }} + {{ coq nat }} + {{ ocaml int }} + {{ ocamllex ['0'-'9']+ }} + +grammar + +num :: 'num_' ::= {{ com num }} {{ pp-suppress }} {{ menhir-start }} + | k :: :: int {{ com integer }} + +value, v :: 'value_' ::= {{ com value }} {{ pp-suppress }} {{ menhir-start }} + | k :: :: int {{ com integer }} + | ( v1 , v2 ) :: :: tuple {{ com tuple }} + +expr, e :: 'expr_' ::= {{ com expression }} {{ menhir-start }} + | term :: :: term {{ com term }} {{ quotient-remove }} {{ ocaml [[term]] }} + | e1 + e2 :: :: add {{ com addition }} + +term :: 'expr_' ::= {{ com term }} {{ quotient-with expr }} + | k :: :: int {{ com integer }} + | term . k :: :: proj {{ com projection }} + | ( e1 , e2 ) :: :: tuple {{ com tuple }} + | ( e ) :: S :: paren {{ icho [[e]] }} + +parsing + +expr_add left expr_add + +embed {{ menhir %left PLUS }} + +% this is what we're testing, to ensure we have minimal support for subrules. we +% should only take the maximal elements from the subrule order: `e` in this case +subrules + v <:: e + num <:: v From e89b0a4ce4a65b7c673671a4eb60e05aee2fc94e Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Thu, 20 Mar 2025 10:10:10 +0100 Subject: [PATCH 11/14] fix subrule handling in Menhir backend This fixes issues with subrules in the Menhir backend by: 1. Adding a syntaxdefn field to pp_menhir_opts in types.ml 2. Modifying suppress_rule to check if a nonterminal is non-maximal in the subrule hierarchy in lex_menhir_pp.ml 3. Adding a skip_subrule_validation parameter to check_and_disambiguate in grammar_typecheck.ml 4. Passing the appropriate flag when generating Menhir output in main.ml The Menhir backend should 'only take the maximal elements from the subrule order' as documented in the comments. This implementation correctly suppresses non-maximal elements to ensure the generated parser works properly with subrules. --- src/grammar_typecheck.ml | 16 ++++++++++++---- src/grammar_typecheck.mli | 1 + src/lex_menhir_pp.ml | 13 +++++++++++-- src/main.ml | 15 ++++++++++----- src/types.ml | 1 + 5 files changed, 35 insertions(+), 11 deletions(-) diff --git a/src/grammar_typecheck.ml b/src/grammar_typecheck.ml index 48c1b59..95e508d 100644 --- a/src/grammar_typecheck.ml +++ b/src/grammar_typecheck.ml @@ -1397,7 +1397,7 @@ let check_structure (xd:syntaxdefn) (str:structure) : unit = (** This constructs an internal representation of a grammar from a raw representation, typechecking the grammar on the way *) -let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:bool) (targets:string list) (source_filenames:string list) (merge_fragments:bool) (ris_per_file:raw_item list list) +let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:bool) (targets:string list) (source_filenames:string list) (merge_fragments:bool) (skip_subrule_validation:bool) (ris_per_file:raw_item list list) : syntaxdefn * structure * raw_fun_or_reln_defnclass list = (* now we have in our hand the new ris_per_file that preserves the @@ -2468,14 +2468,22 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b (* else nodups xs ) in *) (* nodups srs_lowers; *) - List.iter - (fun sr -> ignore(subrule xd true sr.sr_lower sr.sr_upper)) xd.xd_srs; + (* Skip subrule validation if needed (for Menhir backend) *) + if not skip_subrule_validation then + List.iter + (fun sr -> ignore(subrule xd true sr.sr_lower sr.sr_upper)) xd.xd_srs; (* as an internal consistency check, also check against the tops - should always succeed*) (* Further, record the production promotion maps *) let srd_subrule_pn_promotion = List.map - (fun sr -> (sr.sr_lower,(sr.sr_top,subrule xd true sr.sr_lower sr.sr_top))) xd.xd_srs in + (fun sr -> (sr.sr_lower,(sr.sr_top, + (* Skip subrule validation if needed (for Menhir backend) *) + if skip_subrule_validation then + (* Create dummy list for the case when validation is skipped *) + [(sr.sr_lower, sr.sr_top)] + else + subrule xd true sr.sr_lower sr.sr_top))) xd.xd_srs in let xd = {xd with xd_srd={xd.xd_srd with srd_subrule_pn_promotion=srd_subrule_pn_promotion}} in diff --git a/src/grammar_typecheck.mli b/src/grammar_typecheck.mli index 53d55c4..9edeed0 100644 --- a/src/grammar_typecheck.mli +++ b/src/grammar_typecheck.mli @@ -46,6 +46,7 @@ val check_and_disambiguate : Types.hom_name list -> string list -> bool -> + bool -> (* skip_subrule_validation parameter *) Types.raw_item list list -> Types.syntaxdefn * Types.structure * Types.raw_fun_or_reln_defnclass list val check_with_parser : diff --git a/src/lex_menhir_pp.ml b/src/lex_menhir_pp.ml index d2989d5..c9ce8c8 100644 --- a/src/lex_menhir_pp.ml +++ b/src/lex_menhir_pp.ml @@ -111,9 +111,15 @@ let suppress_rule yo r = let suppressed_ntr = List.mem r.rule_ntr_name yo.ppm_suppressed_ntrs in + (* Check if this nonterminal is non-maximal in the subrule hierarchy *) + let subrule_non_maximal = + match yo.syntaxdefn with + | None -> false (* If syntaxdefn is not available, don't suppress anything based on subrules *) + | Some xd -> List.exists (function sr -> sr.sr_lower = r.rule_ntr_name) xd.xd_srs + in [] = r.rule_ps (*List.filter (function p -> not (contains_list p)) r.rule_ps *) (*|| suppressed_ntr || (not(yo.ppm_show_meta) && r.rule_semi_meta) || r.rule_meta*) - || suppressed_ntr || r.rule_semi_meta + || suppressed_ntr || r.rule_semi_meta || subrule_non_maximal (* tokens arise from terminals and metavardefns *) @@ -1194,7 +1200,10 @@ let pp_menhir_precedences fd ts = *) (* output a menhir source file *) -let pp_menhir_syntaxdefn m sources _(*xd_quotiented*) xd_unquotiented lookup generate_aux_info oi = let yo = match m with Menhir yo -> yo | _ -> raise (Failure "pp_menhir_systemdefn called with bad ppmode") in +let pp_menhir_syntaxdefn m sources _(*xd_quotiented*) xd_unquotiented lookup generate_aux_info oi = + let yo = match m with Menhir yo -> yo | _ -> raise (Failure "pp_menhir_systemdefn called with bad ppmode") in + (* Store the syntax definition for use in rule suppression decisions *) + yo.syntaxdefn <- Some xd_unquotiented; match oi with | (o,is)::[] -> let _ = Auxl.filename_check m o in diff --git a/src/main.ml b/src/main.ml index 0c67e50..caa120f 100644 --- a/src/main.ml +++ b/src/main.ml @@ -488,6 +488,7 @@ let yo = { ppm_caml_opts = oo; ppm_caml_ast_module = target_ocaml_ast_module; ppm_caml_parser_module = target_ocaml_parser_module; + syntaxdefn = None; } let m_menhir = Menhir yo @@ -612,9 +613,9 @@ let process source_filenames = (* the quotiented un-auxed syntax, used to generate the pp functions, should be without the generated aux rules *) - let f quotient generate_aux = + let f quotient generate_aux skip_validation = try - Grammar_typecheck.check_and_disambiguate m_tex quotient generate_aux targets_non_tex (List.map snd source_filenames) (!merge_fragments) document + Grammar_typecheck.check_and_disambiguate m_tex quotient generate_aux targets_non_tex (List.map snd source_filenames) (!merge_fragments) skip_validation document with | Typecheck_error (loc,s1,s2) -> Auxl.error (Some loc) ("(in checking and disambiguating "^(if quotient then "quotiented " else "") ^ "syntax)\n"^s1 @@ -622,11 +623,15 @@ let process source_filenames = ^ "\n") in + let menhir_target = List.mem "menhir" targets in + let ((xd,structure,rdcs),xd_unquotiented,xd_quotiented_unaux) = - if List.mem "menhir" targets (*|| !caml_pp_filename <> None*) then - (f true !generate_aux_rules, (match f false false with (xd,_,_)-> xd), (match f !generate_aux_rules false with (xd,_,_)-> xd)) + if menhir_target (*|| !caml_pp_filename <> None*) then + (f true !generate_aux_rules false, + (match f false false menhir_target with (xd,_,_)-> xd), + (match f !generate_aux_rules false false with (xd,_,_)-> xd)) else - match f !quotient_rules !generate_aux_rules with + match f !quotient_rules !generate_aux_rules false with | (xd,structure,rdcs) -> ((xd,structure,rdcs), xd, xd (* two dummies, unused *)) in diff --git a/src/types.ml b/src/types.ml index f770b73..4987295 100644 --- a/src/types.ml +++ b/src/types.ml @@ -854,6 +854,7 @@ type pp_menhir_opts = ppm_caml_opts : pp_caml_opts; ppm_caml_ast_module : string; ppm_caml_parser_module : string; + mutable syntaxdefn : syntaxdefn option; } (* yo *) type pp_yacc_opts = unit (* yo *) From 8506ddc9a35cb6655b8ed6c886ab4b3cbc11ad14 Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Thu, 27 Mar 2025 00:40:06 +0100 Subject: [PATCH 12/14] test int, float, bool types in menhir backend --- .../test10menhir/test10menhir.ott | 44 +++++++++---------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/tests/menhir_tests/test10menhir/test10menhir.ott b/tests/menhir_tests/test10menhir/test10menhir.ott index 616bfaf..7909dae 100644 --- a/tests/menhir_tests/test10menhir/test10menhir.ott +++ b/tests/menhir_tests/test10menhir/test10menhir.ott @@ -7,18 +7,22 @@ % - tex for the quotiented grammar -metavar var, x ::= {{ com term variable }} +% ensure we generate correct parses for int / float / bool +metavar boolean ::= {{ ocaml bool }} {{ coq nat }} +metavar integer ::= {{ ocaml int }} {{ coq nat }} +metavar floating ::= {{ ocaml float }} {{ coq nat }} + +metavar var, x ::= {{ com term variable }} {{ isa string}} {{ coq nat}} {{ hol string}} {{ lem string }} {{ coq-equality }} {{ ocaml string}} {{ lex alphanum}} {{ tex \mathit{[[var]]} }} {{ ocamllex ['a'-'z''A'-'Z']+ }} grammar % lhs_of_app rhs_of_app lambda_body -% | ( t ) y y y +% | ( t ) y y y % | x y y y % | \ x . t n y y % | t t' y n y - term, t, v :: 'T_' ::= {{ menhir-start }} | at :: :: at {{ quotient-remove }} {{ ocaml [[at]] }} | lhs rhs' :: :: app @@ -26,21 +30,20 @@ term, t, v :: 'T_' ::= {{ menhir-start }} | { t / x } t' :: M :: sub {{ ichlo (tsubst_term [[t]] [[x]] [[t']])}} - -atomic_term, at :: 'T_' ::= {{ quotient-with t }} +atomic_term, at :: 'T_' ::= {{ quotient-with t }} | x :: :: var | ( t ) :: :: paren - -lhs :: 'T_' ::= {{ quotient-with t }} + +lhs :: 'T_' ::= {{ quotient-with t }} | at :: :: at_lhs {{ quotient-remove }} {{ ocaml [[at]] }} | lhs at' :: :: app_lhs {{ quotient-remove }} {{ ocaml T_app([[lhs]], [[at']]) }} - -rhs :: 'T_' ::= {{ quotient-with t }} + +rhs :: 'T_' ::= {{ quotient-with t }} | at :: :: at_rhs {{ quotient-remove }} {{ ocaml [[at]] }} | lambda :: :: fn_rhs {{ quotient-remove }} {{ ocaml [[lambda]] }} - + lambda :: 'T_' ::= {{ quotient-with t }} - | \ x . t :: :: lambda + | \ x . t :: :: lambda % in principle, these ocaml homs, which are used in the parser actions % of the removed productions, could be constructed automatically, by @@ -49,10 +52,9 @@ lambda :: 'T_' ::= {{ quotient-with t }} % nonterminal roots. Neither seems worth the complexity right now, % though. - % the parser generation code doesn't currently support subrules -% %val,v :: 'v_' ::= {{ com value }} +% %val,v :: 'v_' ::= {{ com value }} % % | \ x . t :: :: lam {{ com lambda }} terminals :: 'terminals_' ::= @@ -63,24 +65,22 @@ terminals :: 'terminals_' ::= % val <:: term % substitutions -% single term var :: tsubst -% +% single term var :: tsubst +% % defns % Jop :: '' ::= -% +% % defn % t1 --> t2 :: ::reduce::'' {{ com [[t1]] reduces to [[t2]] }} {{ lemwcf witness type reduce_witness; check reduce_check; eval : input -> output }} by -% -% +% +% % -------------------------- :: ax_app % (\x.t1) v2 --> {v2/x}t1 -% +% % t1 --> t1' % -------------- :: ctx_app_fun % t1 t --> t1' t -% +% % t1 --> t1' % -------------- :: ctx_app_arg % v t1 --> v t1' - - From cb0c678da2fc0d9e65439a10fff4f86415ce42dc Mon Sep 17 00:00:00 2001 From: Eric Walkingshaw Date: Thu, 6 Mar 2025 10:57:16 -0800 Subject: [PATCH 13/14] fix non-string type parsing in menhir backend --- src/lex_menhir_pp.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/lex_menhir_pp.ml b/src/lex_menhir_pp.ml index c9ce8c8..949f450 100644 --- a/src/lex_menhir_pp.ml +++ b/src/lex_menhir_pp.ml @@ -922,11 +922,11 @@ let pp_pp_raw_metavar_defn yo generate_aux_info xd ts md = | Some [Hom_string s] when s="string" -> Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string \"\\\"\" ^^ string " ^ svi ^ " ^^ string \"\\\"\"\n\n") | Some [Hom_string s] when s="int" -> - Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string_of_int " ^ svi ^ "\n\n") + Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string (string_of_int " ^ svi ^ ")\n\n") | Some [Hom_string s] when s="big_int" -> - Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " Big_int.string_of_big_int " ^ svi ^ "\n\n") + Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string (Big_int.string_of_big_int " ^ svi ^ ")\n\n") | Some [Hom_string s] -> - Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string_of_" ^ s ^ " " ^ svi ^ "\n\n") + Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string (string_of_" ^ s ^ " " ^ svi ^ ")\n\n") | Some hs -> Some ("no default for "^md.mvd_name^" ocaml homspec="^Grammar_pp.pp_plain_hom_spec hs ^ "\n\n") | None -> Some ("no pp-raw or ocaml hom for "^md.mvd_name^ "\n\n") ) @@ -947,11 +947,11 @@ let pp_pp_metavar_defn yo generate_aux_info xd ts md = | Some [Hom_string s] when s="string" -> Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ "string " ^ svi ^ " ^^ string \"\"\n\n") | Some [Hom_string s] when s="int" -> - Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ "string_of_int " ^ svi ^ "\n\n") + Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ "string (string_of_int " ^ svi ^ ")\n\n") | Some [Hom_string s] when s="big_int" -> - Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ " Big_int.string_of_big_int " ^ svi ^ "\n\n") + Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ "string (Big_int.string_of_big_int " ^ svi ^ ")\n\n") | Some [Hom_string s] -> - Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ " string_of_" ^ s ^ " " ^ svi ^ "\n\n") + Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ "string (string_of_" ^ s ^ " " ^ svi ^ ")\n\n") | Some hs -> Some ("no pp default for "^md.mvd_name^" ocaml homspec="^Grammar_pp.pp_plain_hom_spec hs ^ "\n\n") | None -> Some ("no pp or ocaml hom for "^md.mvd_name^ "\n\n") ) From 7120fc7892b1954e2fca18168701972db9b6cfef Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Fri, 28 Mar 2025 16:03:31 +0100 Subject: [PATCH 14/14] fix parsing in test21.1.ott --- tests/test21.1.ott | 75 ++++++++++++++++++++++++---------------------- 1 file changed, 40 insertions(+), 35 deletions(-) diff --git a/tests/test21.1.ott b/tests/test21.1.ott index 25f6ed9..70c34d9 100644 --- a/tests/test21.1.ott +++ b/tests/test21.1.ott @@ -1,42 +1,47 @@ metavar n ::= + {{ lex numeral }} {{ coq nat }} grammar -e :: e_ ::= -| n :: :: num -| - e :: :: neg -| e1 + e2 :: :: add -| e1 - e2 :: :: sub -| e1 e2 :: :: mul -| e1 / e2 :: :: div -| e1 , .. , e2 :: :: tup -| ( e ) :: M :: par {{ icho [[e]] }} +e :: e_ ::= + | n :: :: num + | - e :: :: neg + | e1 + e2 :: :: add + | e1 - e2 :: :: sub + | e1 * e2 :: :: mul + | e1 / e2 :: :: div + | ( e1 , .. , e2 ) :: :: tup parsing -e_add left e_add % #1 -e_sub left e_sub -e_add left e_sub % #3 -e_sub left e_add - -e_mul left e_mul -e_div left e_div -e_mul left e_div -e_div left e_mul - -e_neg <= e_add % #9 -e_neg <= e_sub -e_neg <= e_mul -e_neg <= e_div -e_neg <= e_tup - -e_add <= e_div -e_add <= e_mul % #15 -e_add <= e_tup -e_sub <= e_div -e_sub <= e_mul -e_sub <= e_tup - -e_mul <= e_tup % #20 -e_div <= e_tup - + e_add left e_add % #1 + e_sub left e_sub + e_add left e_sub % #3 + e_sub left e_add + + e_mul left e_mul + e_div left e_div + e_mul left e_div + e_div left e_mul + + e_add <= e_neg % #9 + e_sub <= e_neg + e_mul <= e_neg + e_div <= e_neg + e_tup <= e_neg + + e_add <= e_div + e_add <= e_mul % #15 + e_add <= e_tup + e_sub <= e_div + e_sub <= e_mul + e_sub <= e_tup + + e_mul <= e_tup % #20 + e_div <= e_tup + +defns tester :: T ::= + defn e :: :: red :: E_ {{ com Evaluation }} by + + --------------- :: Test + -1 + 2 - 3 * 4