From ede3291facb53f5c0f2baee24263711859bea196 Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Mon, 17 Mar 2025 11:44:42 +0100 Subject: [PATCH 01/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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 From d6d85316c702e8160906bda6bd9a22dcb048cd52 Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Wed, 6 Aug 2025 20:50:43 +0200 Subject: [PATCH 15/16] add support for rocq 9.0 --- .github/workflows/docker-action.yml | 1 + coq-ott.opam | 2 +- revision_history.txt | 113 ++++++++++++++-------------- src/system_pp.ml | 15 ++-- 4 files changed, 67 insertions(+), 64 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 2729929..b302ac7 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -15,6 +15,7 @@ jobs: matrix: image: - 'coqorg/coq:8.20' + - 'rocq/rocq-prover:9.0' fail-fast: false steps: - uses: actions/checkout@v4 diff --git a/coq-ott.opam b/coq-ott.opam index 7ef3dbb..d6f6920 100644 --- a/coq-ott.opam +++ b/coq-ott.opam @@ -18,7 +18,7 @@ this library. build: [make "-j%{jobs}%" "-C" "coq"] install: [make "-C" "coq" "install"] depends: [ - "coq" {>= "8.14"} + ("coq" {>= "8.14" & < "9.0"}) | ("rocq-prover" {>= "9.0"} & "coq" {>= "9.0"}) ] tags: [ "category:Computer Science/Semantics and Compilation/Semantics" diff --git a/revision_history.txt b/revision_history.txt index 9223f06..1c7cefe 100644 --- a/revision_history.txt +++ b/revision_history.txt @@ -2,13 +2,13 @@ 2006.11.01 Version 0.04.2 2006.12.20 Version 0.10 initial public release -2006.12.20 Version 0.10.1 +2006.12.20 Version 0.10.1 - include missing HOL file ottDefine.sml -2006.12.22 Version 0.10.2 +2006.12.22 Version 0.10.2 - include missing ottmode.el -2007.01.19 Version 0.10.3 +2007.01.19 Version 0.10.3 - bugfixes - new examples: various TAPL fragments, and an OCaml fragment with concurrency (peterson_caml.ott) @@ -19,7 +19,7 @@ 2007.01.24 Version 0.10.4 - bugfix: allow "-" in bindspec lexing - + 2007.02.07 Version 0.10.5 - various bugfixes (mostly w.r.t. Coq list support) - various improvements to examples @@ -51,14 +51,14 @@ - add missing file from Coq proof support: ott_list_eq_dec.v 2007.10.18 Version 0.10.13 -- new (experimental!) switch -picky_multiple_parses , +- new (experimental!) switch -picky_multiple_parses , to allow multiple parses if the generated code is identical - at present only for filtered LaTeX - some source documentation - + 2008.02.15 Version 0.10.14 - new parser, with better performance and better support for disambiguation - (see Section 14 "Parsing Priorities" in the manual, and changes to + (see Section 14 "Parsing Priorities" in the manual, and changes to Section 20 "Reference: The language of symbolic terms") - new support for context grammars, with automatically generated hole-filling functions (see Section 13 "Context rules" in the manual) @@ -83,7 +83,7 @@ - fix ocamlvar hom bug - fix bug in Coq backend when dealing with some kinds of dot forms -- suppress printing of number of good/bad definition rules if +- suppress printing of number of good/bad definition rules if there are no rules - change -tex_show_meta false behaviour to not suppress sugar productions @@ -92,13 +92,12 @@ be easy to build from source, but we don't have access to a suitable machine. - 2010.3.24 Version 0.10.18alpha - The previous command-line options -coq, -hol, etc., are no longer - supported; they should be replaced by -o. + supported; they should be replaced by -o. -- By default (unless -merge true is set) the order of the input file +- By default (unless -merge true is set) the order of the input file is preserved, so one can have mixed sequences of definitions of grammar, of inductive relations, and of embed blocks. @@ -113,7 +112,7 @@ - Better tex default spacing, distinguishing alphabetic and other ("symbolic") terminals based on their ott source strings and - wrapping them in \ottkw{} and \ottsym{} respectively. + wrapping them in \ottkw{} and \ottsym{} respectively. - Support for in-line prover code in premises, e.g. @@ -124,7 +123,7 @@ - The {{ phantom }} hom can now be applied to metavariables and to nonterminal rules. In both cases it suppresses generation of a prover or OCaml definition, but any type homs are taken into account when - the metavariable or nonterminal root is output as a type. + the metavariable or nonterminal root is output as a type. - There is a new hom {{ order ... }} that can be applied to productions which lets one specify the order of arguments of a @@ -135,11 +134,11 @@ - There is a new hom {{ coq-universe UniverseName }} that can be applied to metavariable or nonterminal rules, eg to force Ott to - generate definitions in Type instead of in Set. + generate definitions in Type instead of in Set. - Changed some debug options (eg show-pre-sort) -- Ocaml list homs on productions are now permitted +- Ocaml list homs on productions are now permitted - add coq_lngen option for compatibility with the lngen tool @@ -153,11 +152,10 @@ - performance issue when using contextrules [Nicolas Pouillard] - parens in OCaml substitutions for multiple binders [Vilhelm Sjoberg] - 2010.03.29 Version 0.20 - The order among mutually recursive nonterminal definitions in - grammar blocks is now preserved in prover output. + grammar blocks is now preserved in prover output. 2010.04.04 Version 0.20.1 @@ -169,11 +167,9 @@ defn t1 --> t2 :: ::reduce::'' by - -------------------------- :: ax_app (\x.t1) v2 --> {v2/x}t1 - 2010.06.29 - refactor the generated latex for grammars so that condensed grammars @@ -184,7 +180,7 @@ \renewcommand{\ottprodline}[6]{{}\ ${}#1$\mbox{\ {}$#2$}{}} \renewcommand{\ottfirstprodline}[6]{{}\ ${}$\mbox{\ {}$#2$}{}} \renewcommand{\ottprodnewline}{} - \renewcommand{\ottinterrule}{\\[1mm]} + \renewcommand{\ottinterrule}{\\[1mm]} - add experimental option (-ocaml_include_terminals true) to include, in generated OCaml types, an instance of "terminal" in all the places @@ -194,7 +190,7 @@ 2010.11.28 Version 0.20.3 -- fixes to bugs: +- fixes to bugs: 11367 coq-universe Type problem with non-native lists 11368 generation of induction principles in Ott 0.20 @@ -206,7 +202,7 @@ inductive rules for the Coq backend. For instance, adding the [[:RED]] annotation below - t1 --> t1' [[:RED]] + t1 --> t1' [[:RED]] -------------------- :: ctx_app_arg v t1 --> v t1' @@ -226,24 +222,24 @@ names the user specified in the definition of grammar rules. For instance the grammar definition below - grammar - term, t :: 't_' ::= - | x :: :: Var + grammar + term, t :: 't_' ::= + | x :: :: Var | \ x . t :: :: Lam (+ bind x in t +) - | t t' :: :: App - | ( t ) :: S:: Paren {{ icho [[t]] }} + | t t' :: :: App + | ( t ) :: S:: Paren {{ icho [[t]] }} | { t / x } t' :: M:: Tsub {{ icho (tsubst_t [[t]] [[x]] [[t']])}} generates - Inductive term : Set := + Inductive term : Set := | t_var (x:var) | t_lam (x:var) (t:term) | t_app (t:term) (t':term). - instead of + instead of - Inductive term : Set := + Inductive term : Set := | t_var : var -> term | t_lam : var -> term -> term | t_app : term -> term -> term. @@ -262,14 +258,14 @@ in the Ott file below: grammar - n :: 'n_' ::= + n :: 'n_' ::= | 0 :: :: Zero | S n :: :: Succ funs Add ::= {{ hol-proof ... }} fun - n1 + n2 :: n :: add {{ com a function of type num \to num \to num }} + n1 + n2 :: n :: add {{ com a function of type num \to num \to num }} by 0 + n2 === n2 S n1 + n2 === n1 + S n2 @@ -279,7 +275,7 @@ Fixpoint add (x1:num) (x2:num) : num:= match x1,x2 with | n_zero , n2 => n2 - | (n_succ n1) , n2 => (add n1 (n_succ n2) ) + | (n_succ n1) , n2 => (add n1 (n_succ n2) ) end. The "fun n1 + n2 :: n :: add by" declaration specifies: @@ -307,7 +303,7 @@ Coq). Added the -coq_use_filter_fn option for backwards compatibility (*). -- Introduced a new embed hom +- Introduced a new embed hom embed {{ coq-lib foo1 foo2 foo3 }} @@ -337,13 +333,13 @@ This version fixes a packaging problem of the version 0.21. inside. The existing syntax {{ ... }} is also valid. - Added embed tex-wrap-pre/tex-wrap-post homs to customize tex - wrapping: the default LaTeX header can be changed by writing + wrapping: the default LaTeX header can be changed by writing - embed {{ tex-wrap-pre ... }} + embed {{ tex-wrap-pre ... }} - and the default footer by writing + and the default footer by writing - embed {{ tex-wrap-post ... }}. + embed {{ tex-wrap-post ... }}. In addition, the program option -tex_wrap false can be used to omit wraping the tex output (-tex_wrap false overrides any @@ -351,7 +347,6 @@ This version fixes a packaging problem of the version 0.21. - minor updates to the Hol backend to target the new Hol syntax. - 2012.01.04 fix for HOL multiple definitions bug 2012.06.12 fix for HOL syntax change @@ -360,39 +355,37 @@ This version fixes a packaging problem of the version 0.21. 2012.12.04 bugfix 15158 - -2013.04.20 +2013.04.20 - experimental support for generating Lem definitions, including new homs lem, lemvar, ichlo - -2013.06.22 +2013.06.22 - New aux-hom feature: We permit an aux hom on grammar rules. For any rule with such a hom, we transform that rule by appending an "_aux" to its primary nonterminal root name. We then add a synthesised rule with the original nonterminal -root name and a single production, with a shape described by the body of -the aux hom, which must be of the form +root name and a single production, with a shape described by the body of +the aux hom, which must be of the form {{ aux foo1 foo2 _ bar1 bar2 bar3 }} with a single _ and any number of strings fooi and barj before and after, and no Raw_hom_ident's. The _ is replaced by the original -nonterminal root name. +nonterminal root name. For example, given a grammar or metavariable l of source locations, one -might say +might say ntr :: 'NTR_' ::= {{ aux _ l }} | ... -to synthesise grammars ntr_aux and ntr of unannotated and location-annotated -terms, the first with all the original productions and the second with a -single production - | ntr l :: :: NTR_aux. +to synthesise grammars ntr_aux and ntr of unannotated and location-annotated +terms, the first with all the original productions and the second with a +single production + | ntr l :: :: NTR_aux. If the rule has an empty production name wrapper (eg with '' in place of 'NTR_') then the production name is based on the original @@ -405,7 +398,7 @@ for latex output and true for OCaml output. - New {{ texlong }} hom on productions, letting long productions be typeset with the production extending into the space usually used -for comment, pushing that onto the next line. +for comment, pushing that onto the next line. 2013.07.04 @@ -418,7 +411,7 @@ for comment, pushing that onto the next line. 2013.10.24 Version 0.23 -2013.11.17 +2013.11.17 - add command-line option -output_source_locations to include comments in the output giving the source locations: @@ -427,7 +420,7 @@ for comment, pushing that onto the next line. i=2 also adds a location for other components of the output Location annotations are lines of the form - (* #source file FILENAME1 lines M1 - N1 and ... and FILENAMEk lines Mk - Nk *) + (* #source file FILENAME1 lines M1 - N1 and ... and FILENAMEk lines Mk - Nk *) (or with % instead of (* *) for the Latex output). @@ -443,7 +436,7 @@ for comment, pushing that onto the next line. 2016-10-27 Snapshot of 0.25 release moved to github at https://github.com/ott-lang/ott -2017-02-10 Add command-line option -tex_suppress_category to +2017-02-10 Add command-line option -tex_suppress_category to suppress productions or rules with the specified category string. 2017-02-13 Add command-line option -tex_suppress_ntr to @@ -452,7 +445,7 @@ for comment, pushing that onto the next line. 2017-05-28 fixes for Coq 8.5 and 8.6, contributed by palmskog 2017-05-29 - 2017-06-14 Add experimental support for generating a -standalone lexer, menhir parser, and pretty printer, as illustrated in +standalone lexer, menhir parser, and pretty printer, as illustrated in tests/menhir_tests/test10menhir 2017-07-17 fixes for OCaml safe string, contributed by jpdeplaix @@ -475,7 +468,7 @@ tests/menhir_tests/test10menhir - improve menhir parser and pp generation for {{ phantom }} rules -2017-10-11 +2017-10-11 - add highly experimental -aux_style_rules false option, adding aux info as extra constructor arguments rather than additional @@ -493,7 +486,7 @@ tests/menhir_tests/test10menhir 2017-11-27 Version 0.27 2017-12-05 [Brian Campbell] Bugfix: add missing case of Lem auxparam type name -hack when it's hom +hack when it's hom 2018-01 [Peter Sewell, + palmskog for Coq] copy ocaml_light example sources from svn (rsem/ott/old_pre_github/examples/caml) and @@ -581,3 +574,7 @@ Peter Sewell + Thibaut Pérami: Add "menhir-start-type" hom to specify the top l 2024-12 @palmskog: only output plain comments in generated Coq code 2024-12-30 Version 0.34 + +2025-08-06 Version 0.xx + +2025-08 @SergioBenitez: Rocq 9.0 compatibility - update opam dependencies and CI workflow diff --git a/src/system_pp.ml b/src/system_pp.ml index 88f3b2e..409df78 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -33,7 +33,6 @@ open Types;; - (* Print auxiliary lemmas if necessary *) let rec uses_lists_element e = @@ -351,6 +350,12 @@ let pp_systemdefn_core fd m sd lookup = end | _ -> () ) +(* Helper function to format Require Import statements with From Coq prefix for stdlib *) +let format_require_import th = + match th with + | "Arith" | "Bool" | "List" -> "From Coq Require Import " ^ th ^ "." + | _ -> "Require Import " ^ th ^ "." + (* old algorithm, used only when pp with -merge true *) let pp_systemdefn fd m sd lookup fn = @@ -384,14 +389,14 @@ let pp_systemdefn fd m sd lookup fn = then begin Printf.fprintf fd "(* generated by Ott %s, locally-nameless %sfrom: %s *)\n" Version.n (if Auxl.is_lngen m then "lngen " else "") sd.sources; - List.iter (fun th -> Printf.fprintf fd "Require Import %s.\n" th) + List.iter (fun th -> Printf.fprintf fd "%s\n" (format_require_import th)) ( match co.coq_expand_lists with | true -> ["Metalib.Metatheory"] | false -> ["Bool"; "Metalib.Metatheory"; "List"; "Ott.ott_list_core"]) end else begin Printf.fprintf fd "(* generated by Ott %s from: %s *)\n" Version.n sd.sources; - List.iter (fun th -> Printf.fprintf fd "Require Import %s.\n" th) + List.iter (fun th -> Printf.fprintf fd "%s\n" (format_require_import th)) ( match co.coq_expand_lists with | true -> ["Arith"; "Bool"; "List"] | false -> ["Arith"; "Bool"; "List"; "Ott.ott_list_core"]) @@ -433,7 +438,7 @@ let pp_systemdefn_core_io m sd lookup oi merge_fragments = let fd = open_out o in Printf.fprintf fd "(* generated by Ott %s, locally-nameless %sfrom: %s *)\n" Version.n (if Auxl.is_lngen m then "lngen " else "") sd.sources; - List.iter (fun th -> Printf.fprintf fd "Require Import %s.\n" th) + List.iter (fun th -> Printf.fprintf fd "%s\n" (format_require_import th)) ( match co.coq_expand_lists with | true -> ["Metalib.Metatheory"] | false -> ["Bool"; "Metalib.Metatheory"; "List"; "Ott.ott_list_core"]); @@ -476,7 +481,7 @@ let pp_systemdefn_core_io m sd lookup oi merge_fragments = | Coq co -> [ Embed_string (dummy_loc, "(* generated by Ott " ^ Version.n ^ " from: " ^ file_sources ^ " *)\n\n" - ^ String.concat "\n" (List.map (fun th -> "Require Import " ^ th ^ ".") + ^ String.concat "\n" (List.map format_require_import ( match co.coq_expand_lists with | true -> ["Arith"; "Bool"; "List"] | false -> ["Arith"; "Bool"; "List"; "Ott.ott_list_core"])) From bbc1b4c66544080c0f4c02bf0548f91f338d5660 Mon Sep 17 00:00:00 2001 From: Sergio Benitez Date: Wed, 6 Aug 2025 23:03:52 +0200 Subject: [PATCH 16/16] backward-compatibly rename coq items to rocq This commit introduces new homs, CLI flags, and syntax, one for each of the existing Coq versions, with 'rocq' replacing 'coq' in the name. The 'coq' variants remain usable, forwarding to the now canoncial rocq variants. This is a non-breaking change. --- regression/regression.otl | 6 + src/auxl.ml | 13 +- src/coq_induct.ml | 2 +- src/defns.ml | 6 +- src/embed_pp.ml | 4 +- src/grammar_lexer.mll | 11 +- src/grammar_parser.mly | 4 + src/grammar_pp.ml | 33 ++--- src/grammar_typecheck.ml | 63 +++++---- src/ln_transform.ml | 26 ++-- src/main.ml | 108 +++++++++------- src/transform.ml | 17 +-- tests/gmap1.rocq.ott | 14 ++ tests/regexp.rocq.ott | 96 ++++++++++++++ tests/test10.rocq.ott | 45 +++++++ tests/test8.rocq.ott | 240 +++++++++++++++++++++++++++++++++++ tests/test_cr_metahoms.ott | 36 ++++++ tests/test_rocq_keywords.ott | 17 +++ 18 files changed, 624 insertions(+), 117 deletions(-) create mode 100644 tests/gmap1.rocq.ott create mode 100644 tests/regexp.rocq.ott create mode 100644 tests/test10.rocq.ott create mode 100644 tests/test8.rocq.ott create mode 100644 tests/test_cr_metahoms.ott create mode 100644 tests/test_rocq_keywords.ott diff --git a/regression/regression.otl b/regression/regression.otl index dbc546b..9db842c 100644 --- a/regression/regression.otl +++ b/regression/regression.otl @@ -100,3 +100,9 @@ sys-purercdsub : ../examples/tapl/common.ott ../examples/tapl/common_typing.ott ../tests/test_embed_top_1.ott ../tests/test_merge_embed_location_1-1.ott ../tests/test_merge_embed_location_1-2.ott +../tests/regexp.rocq.ott +../tests/test10.rocq.ott +../tests/test8.rocq.ott +../tests/gmap1.rocq.ott +../tests/test_rocq_keywords.ott +../tests/test_cr_metahoms.ott diff --git a/src/auxl.ml b/src/auxl.ml index 88ee363..57a883d 100644 --- a/src/auxl.ml +++ b/src/auxl.ml @@ -47,7 +47,7 @@ let mode_name m = match m with | Isa _ -> "Isabelle" | Hol _ -> "HOL" | Lem _ -> "Lem" - | Coq _ -> "Coq" + | Coq _ -> "Rocq" | Twf _ -> "Twelf" | Caml _ -> "OCaml" | Lex _ -> "Lex" @@ -252,7 +252,7 @@ let add_to_lib r name def = (* Similar function already in Grammar_pp let pp_type_name m xd (s: string) = let homname = match m with - | Coq _ -> "coq" + | Coq _ -> "rocq" | Hol _ -> "hol" | Isa _ -> "isa" | Twf _ -> "twf" @@ -602,7 +602,7 @@ let hom_name_for_pp_mode m | Isa _ -> "isa" | Hol _ -> "hol" | Lem _ -> "lem" - | Coq _ -> "coq" + | Coq _ -> "rocq" | Twf _ -> "twf" | Caml _ -> "ocaml" | Lex _ -> "lex" @@ -624,7 +624,10 @@ let select_dep_graph_nontran m xddep = let hom_spec_for_hom_name hn homs = try Some (List.assoc hn homs) - with Not_found -> None + with Not_found -> + (* Try the alternate: rocq -> coq *) + let alt = Str.global_replace (Str.regexp "rocq") "coq" hn in + if alt <> hn then try Some (List.assoc alt homs) with Not_found -> None else None let hom_spec_for_pp_mode m homs = hom_spec_for_hom_name (hom_name_for_pp_mode m) homs @@ -1789,7 +1792,7 @@ let filename_check m s = let is_lngen m = let co = match m with Coq co -> co - | _ -> errorm m "ln_transform_syntaxdefn of non-coq target" in + | _ -> errorm m "ln_transform_syntaxdefn of non-rocq target" in co.coq_lngen let require_locally_nameless xd = diff --git a/src/coq_induct.ml b/src/coq_induct.ml index 67fbbc4..ed20735 100644 --- a/src/coq_induct.ml +++ b/src/coq_induct.ml @@ -80,7 +80,7 @@ let rules_needing_induction m xd rs : nontermroot list list = (fun g -> List.for_all (fun ntr -> let r = Auxl.rule_of_ntr xd ntr in - match (Auxl.hom_spec_for_hom_name "coq" r.rule_homs) with + match (Auxl.hom_spec_for_hom_name "rocq" r.rule_homs) with Some _ -> false | None -> true) g) groups diff --git a/src/defns.ml b/src/defns.ml index 5a04aa9..22e6959 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -545,7 +545,9 @@ let pp_defn fd (m:pp_mode) (xd:syntaxdefn) lookup (defnclass_wrapper:string) (un let pp_defnclass fd (m:pp_mode) (xd:syntaxdefn) lookup (dc:defnclass) = - let universe = try Grammar_pp.pp_hom_spec m xd (List.assoc "coq-universe" dc.dc_homs) with Not_found -> "Prop" in + let universe = match Auxl.hom_spec_for_hom_name "rocq-universe" dc.dc_homs with + | Some hs -> Grammar_pp.pp_hom_spec m xd hs + | None -> "Prop" in let isa_type_of_defn (m: pp_mode) (xd: syntaxdefn) (d: defn) : string = (* seems simplest to find the type associated with the production that we added to the language for this defn, rather than build a type @@ -723,7 +725,7 @@ let fundefn_to_int_func (m:pp_mode) (xd:syntaxdefn) (deps:string list) (fd:funde let prod_es = Grammar_pp.apply_hom_order m xd (Auxl.prod_of_prodname xd prod_name) in let struct_on = - match Auxl.hom_spec_for_hom_name "coq-struct" fd.fd_homs with + match Auxl.hom_spec_for_hom_name "rocq-struct" fd.fd_homs with | Some ([Hom_index i]) -> "{struct x" ^ string_of_int (i+1) ^ "} " | Some _ -> Auxl.warning (* TODO *) None "malformed coq-struct homomorphism"; diff --git a/src/embed_pp.ml b/src/embed_pp.ml index 1ab5ef9..b576073 100644 --- a/src/embed_pp.ml +++ b/src/embed_pp.ml @@ -55,7 +55,7 @@ and pp_embedmorphism fd m xd lookup (l,hn,es) = output_string fd " "; output_string fd Grammar_pp.pp_DOUBLERIGHTBRACE; output_string fd "\n"; - | (Coq _, "coq") + | (Coq _, "coq") | (Coq _, "rocq") | (Isa _, "isa") | (Hol _, "hol") | (Lem _, "lem") @@ -66,7 +66,7 @@ and pp_embedmorphism fd m xd lookup (l,hn,es) = | (Lex _, "lex") -> pp_embed_spec fd m xd lookup es; output_string fd "\n" - | (Coq co, "coq-lib") -> + | (Coq co, "coq-lib") | (Coq co, "rocq-lib") -> let x = co.coq_library in x := (fst !x, embed_strings (snd !x) es) | (Isa io, "isa-lib") -> diff --git a/src/grammar_lexer.mll b/src/grammar_lexer.mll index 46b7a31..b6679d4 100644 --- a/src/grammar_lexer.mll +++ b/src/grammar_lexer.mll @@ -62,7 +62,7 @@ type lexer = Lexing.lexbuf -> Grammar_parser.token type token_type = Tok_kw of string | Tok_sym of string*string | Tok_sym_direct of string*string | Tok_user of string -let hom_strings = ["TEX_NAME_PREFIX";"formula";"terminals";"M";"S";"tex";"com";"coq";"hol";"lem";"isa";"ocaml";"icho";"ichlo";"ich";"ichl";"coq-equality";"isasyn";"isaprec";"lex";"texvar";"isavar";"holvar";"lemvar";"ocamlvar";"repr-locally-nameless";"phantom";"coq-struct";"isa-proof";"isa-auxfn-proof";"isa-subrule-proof";"coq-lib"] +let hom_strings = ["TEX_NAME_PREFIX";"formula";"terminals";"M";"S";"tex";"com";"coq";"rocq";"hol";"lem";"isa";"ocaml";"icho";"ichlo";"ich";"ichl";"ir";"rh";"irh";"irho";"irhl";"irhlo";"coq-equality";"rocq-equality";"isasyn";"isaprec";"lex";"texvar";"isavar";"holvar";"lemvar";"ocamlvar";"repr-locally-nameless";"phantom";"coq-struct";"rocq-struct";"isa-proof";"isa-auxfn-proof";"isa-subrule-proof";"coq-lib";"rocq-lib";"coq-universe";"rocq-universe";"coq-notation";"rocq-notation"] let de_lex t = match t with @@ -103,6 +103,9 @@ let de_lex t = match t with | COQSECTIONBEGIN -> Tok_kw "begincoqsection" | COQSECTIONEND -> Tok_kw "endcoqsection" | COQVARIABLE -> Tok_kw "coqvariable" +| ROCQSECTIONBEGIN -> Tok_kw "beginrocqsection" +| ROCQSECTIONEND -> Tok_kw "endrocqsection" +| ROCQVARIABLE -> Tok_kw "rocqvariable" | LTEQ -> Tok_sym ("<=" ,"<=") | BIND_LEFT_DELIM -> Tok_sym ("(+" , "(+") | DOTDOT -> Tok_sym (".." , "..") @@ -259,6 +262,9 @@ rule metalang = parse | "begincoqsection" { COQSECTIONBEGIN } | "endcoqsection" { COQSECTIONEND } | "coqvariable" { COQVARIABLE } + | "beginrocqsection" { ROCQSECTIONBEGIN } + | "endrocqsection" { ROCQSECTIONEND } + | "rocqvariable" { ROCQVARIABLE } | "<=" { LTEQ } | "left" { LEFT } | "right" { RIGHT } @@ -434,6 +440,9 @@ and defnlang = parse | "begincoqsection"-> go_back back metalang lexbuf;COQSECTIONBEGIN | "endcoqsection" -> go_back back metalang lexbuf;COQSECTIONEND | "coqvariable" -> go_back back metalang lexbuf;COQVARIABLE + | "beginrocqsection"-> go_back back metalang lexbuf;ROCQSECTIONBEGIN + | "endrocqsection" -> go_back back metalang lexbuf;ROCQSECTIONEND + | "rocqvariable" -> go_back back metalang lexbuf;ROCQVARIABLE | "defn" -> go_back back elements lexbuf;DEFN | "funs" -> go_back back metalang lexbuf;FUNDEFNCLASS | "fun" -> go_back back elements lexbuf;FUNDEFN diff --git a/src/grammar_parser.mly b/src/grammar_parser.mly index 7e6beab..5ae844d 100644 --- a/src/grammar_parser.mly +++ b/src/grammar_parser.mly @@ -109,6 +109,7 @@ let parse_error s = %token UNION EMPTY %token COQSECTIONBEGIN COQSECTIONEND COQVARIABLE +%token ROCQSECTIONBEGIN ROCQSECTIONEND ROCQVARIABLE %token COMP_LEFT COMP_MIDDLE COMP_RIGHT COMP_IN @@ -154,6 +155,9 @@ item: | COQSECTIONBEGIN coq_section_begin { $2 } | COQSECTIONEND coq_section_end { $2 } | COQVARIABLE coq_variable { $2 } + | ROCQSECTIONBEGIN coq_section_begin { $2 } + | ROCQSECTIONEND coq_section_end { $2 } + | ROCQVARIABLE coq_variable { $2 } metavardefn: metavardefn_int diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 6743c20..73200c7 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -1228,9 +1228,7 @@ and pp_nt_or_mv_root_ty m xd ntmvr = | Mvr mvr -> pp_metavarroot_ty m xd mvr and coq_maybe_decide_equality m xd homs ntmvr loc = - match - try Some (List.assoc "coq-equality" homs) with Not_found -> None - with + match Auxl.hom_spec_for_hom_name "rocq-equality" homs with | None -> "" | Some eh -> let type_name = pp_nt_or_mv_root_ty m xd ntmvr in @@ -1248,7 +1246,7 @@ and coq_maybe_decide_equality m xd homs ntmvr loc = ^ ( match eh with | [ ] -> " decide equality; auto with ott_coq_equality arith." | [ Hom_string s ] -> s - | _ -> Auxl.error (Some loc) "malformed coq-equality homomorphism\n" ) + | _ -> Auxl.error (Some loc) "malformed rocq-equality homomorphism\n" ) ^ "\nDefined.\n" ^ "#[export] Hint Resolve eq_" ^ type_name ^ " : ott_coq_equality.\n" @@ -1275,12 +1273,13 @@ and pp_metavardefn m xd mvd = | Coq co -> let type_name = pp_metavarroot_ty m xd mvd.mvd_name in let universe = - try pp_hom_spec m xd (List.assoc "coq-universe" mvd.mvd_rep) - with Not_found -> "Set" + match Auxl.hom_spec_for_hom_name "rocq-universe" mvd.mvd_rep with + | Some hs -> pp_hom_spec m xd hs + | None -> "Set" in let body = pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc in let sentence = - if List.mem_assoc "coq-notation" mvd.mvd_rep then + if Auxl.hom_spec_for_hom_name "rocq-notation" mvd.mvd_rep <> None then "Notation " ^ type_name ^ " := (" ^ body ^ " : " ^ universe ^ ")." else "Definition " ^ type_name ^ " : " ^ universe ^ " := " ^ body ^ "." @@ -1347,10 +1346,9 @@ and pp_metavarrep m xd mvd_rep type_name loc = pp_hom_spec m xd hs with Not_found -> Auxl.warning (Some loc) ("undefined lem metavarrep for "^type_name^"\n"); "UNDEFINED" ) | Coq co -> - ( try - let hs = List.assoc "coq" mvd_rep in - pp_hom_spec m xd hs - with Not_found -> Auxl.warning (Some loc) ("undefined coq metavarrep for "^type_name^"\n"); "UNDEFINED" ) + ( match Auxl.hom_spec_for_hom_name "rocq" mvd_rep with + | Some hs -> pp_hom_spec m xd hs + | None -> Auxl.warning (Some loc) ("undefined rocq metavarrep for "^type_name^"\n"); "UNDEFINED" ) | Twf wo -> ( try let hs = List.assoc "twf" mvd_rep in @@ -2649,7 +2647,9 @@ and pp_rule m xd r = (* returns a string option *) if r.rule_meta || r.rule_phantom then None else - let universe = try pp_hom_spec m xd (List.assoc "coq-universe" r.rule_homs) with Not_found -> "Set" in + let universe = match Auxl.hom_spec_for_hom_name "rocq-universe" r.rule_homs with + | Some hs -> pp_hom_spec m xd hs + | None -> "Set" in Some (pp_nontermroot_ty m xd r.rule_ntr_name ^ " : "^universe^ " := "^pp_com^"\n" ^ String.concat "\n" @@ -2752,11 +2752,12 @@ and pp_rule_list m xd rs = let homs = (Auxl.rule_of_ntr xd ntr).rule_homs in let type_name = pp_nontermroot_ty m xd ntr in let universe = - try pp_hom_spec m xd (List.assoc "coq-universe" homs) - with Not_found -> "Set" + match Auxl.hom_spec_for_hom_name "rocq-universe" homs with + | Some hs -> pp_hom_spec m xd hs + | None -> "Set" in let body = pp_hom_spec m xd hs in - if List.mem_assoc "coq-notation" homs then + if Auxl.hom_spec_for_hom_name "rocq-notation" homs <> None then "\nNotation " ^ type_name ^ " := (" ^ body ^ " : " ^ universe ^ ").\n" else "\nDefinition " ^ type_name ^ " : " ^ universe ^ " := " ^ body ^ ".\n" @@ -3909,7 +3910,7 @@ and pp_symterm_list_body m xd sie (de :dotenv) tmopt include_terminals prod_es s | [] -> [] | (Lang_nonterm(ntr,_))::t -> let r = Auxl.rule_of_ntr xd ntr in - let b = (List.exists (fun (h,_) -> String.compare h "coq" = 0) r.rule_homs) in + let b = (List.exists (fun (h,_) -> let normalized = Str.global_replace (Str.regexp "rocq") "coq" h in String.compare normalized "coq" = 0) r.rule_homs) in (Auxl.promote_ntr xd ntr,b) :: (intern t) | (Lang_metavar(mvr,_))::t -> (mvr,false) :: (intern t) | (Lang_terminal _)::t -> intern t diff --git a/src/grammar_typecheck.ml b/src/grammar_typecheck.ml index 95e508d..a04c8ee 100644 --- a/src/grammar_typecheck.ml +++ b/src/grammar_typecheck.ml @@ -404,21 +404,21 @@ let subrule (xd:syntaxdefn) (include_meta_prods:bool) let allowable_hom_data = [ - ( Hu_root , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml"], + ( Hu_root , (["isa";"coq";"rocq";"hol";"lem";(*"twf";*)"tex";"ocaml"], "nonterminal, metavar or indexvar root")); - ( Hu_metavar , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";"lex";"texvar";"isavar";"holvar";"lemvar";"ocamlvar";"repr-locally-nameless";(*"repr-nominal";*)"phantom";"ocamllex";"ocamllex-remove";"ocamllex-of-string";"pp";"pp-raw";"pp-suppress"], + ( Hu_metavar , (["isa";"coq";"rocq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"rocq-equality";"coq-notation";"rocq-notation";"coq-universe";"rocq-universe";"lex";"texvar";"isavar";"holvar";"lemvar";"ocamlvar";"repr-locally-nameless";(*"repr-nominal";*)"phantom";"ocamllex";"ocamllex-remove";"ocamllex-of-string";"pp";"pp-raw";"pp-suppress"], "metavar declaration")); - ( Hu_rule , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"phantom";"aux";"auxparam";"menhir-start";"menhir-start-type";"quotient-with";"pp";"pp-raw";"pp-suppress";"pp-params";"lex-comment"], + ( Hu_rule , (["isa";"coq";"rocq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"rocq-equality";"coq-notation";"rocq-notation";"coq-universe";"rocq-universe";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"ir";"rh";"irh";"irho";"irhl";"irhlo";"phantom";"aux";"auxparam";"menhir-start";"menhir-start-type";"quotient-with";"pp";"pp-raw";"pp-suppress";"pp-params";"lex-comment"], "rule")); ( Hu_rule_meta, (["com"], "special rule")); - ( Hu_prod , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"texlong";"ocaml";"com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih"; + ( Hu_prod , (["isa";"coq";"rocq";"hol";"lem";(*"twf";*)"tex";"texlong";"ocaml";"com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"ir";"rh";"irh";"irho";"irhl";"irhlo"; "disambiguate";"prec";"leftassoc";"rightassoc";"menhir";"quotient-remove";"menhir-prec";"pp";"pp-raw"], "production")); ( Hu_prod_tm , (["isa"; "tex";"lex"; "com"; "prec";"leftassoc";"rightassoc"],"production of the terminals grammar")); ( Hu_drule , ([ "com"],"definition rule")); ( Hu_defn , ([ "tex"; "com";"isasyn";"isaprec";"disambiguate";"lemwcf"],"definition")); - ( Hu_defnclass, (["coq-universe"],"defns block")); - ( Hu_fundefn , (["isa";"coq";"hol";"lem";(*"twf";*)"tex"; "com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"coq-struct"],"function definition")); + ( Hu_defnclass, (["coq-universe";"rocq-universe"],"defns block")); + ( Hu_fundefn , (["isa";"coq";"rocq";"hol";"lem";(*"twf";*)"tex"; "com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"ir";"rh";"irh";"irho";"irhl";"irhlo";"coq-struct";"rocq-struct"],"function definition")); ( Hu_fundefnclass, ([(* "isa-proof";*)"hol-proof"],"funs block")); ( Hu_subrule, (["isa-proof"],"subrule definition")); ( Hu_subst, (["isa-proof"],"substitution definition")); @@ -428,6 +428,7 @@ let allowable_hom_data = ] let embed_allowable_homs = ["coq";"coq-lib";"coq-preamble"; + "rocq";"rocq-lib";"rocq-preamble"; "isa";"isa-import";"isa-auxfn-proof";"isa-subrule-proof";"isa-lib";"isa-preamble"; "hol";"hol-preamble"; "lem";"lem-preamble"; @@ -436,7 +437,7 @@ let embed_allowable_homs = ["coq";"coq-lib";"coq-preamble"; "ocaml";"ocaml-preamble"; "menhir"] -let list_form_allowable_homs =["isa";"coq";"hol";"lem";"ic";"ch";"ih";"ich";"ichl";"icho";"ichlo";(*"icht";*)"coq-struct";"ocaml"] +let list_form_allowable_homs =["isa";"coq";"rocq";"hol";"lem";"ic";"ch";"ih";"ich";"ichl";"icho";"ichlo";"ir";"rh";"irh";"irhl";"irho";"irhlo";(*"icht";*)"coq-struct";"rocq-struct";"ocaml"] let cd_disambiguate_hom name rhs hs = try @@ -664,21 +665,33 @@ and cd_homs_icho (c: cd_env) (hs: homomorphism list) : homomorphism list = | [] -> [] | (hn,hs)::hs' -> if hn = "ic" then - ("isa",hs)::("coq",hs)::(cd_homs_icho c hs') + ("isa",hs)::("rocq",hs)::(cd_homs_icho c hs') else if hn = "ih" then ("isa",hs)::("hol",hs)::(cd_homs_icho c hs') else if hn = "ch" then - ("hol",hs)::("coq",hs)::(cd_homs_icho c hs') + ("hol",hs)::("rocq",hs)::(cd_homs_icho c hs') else if hn = "ich" then - ("isa",hs)::("hol",hs)::("coq",hs)::(cd_homs_icho c hs') + ("isa",hs)::("hol",hs)::("rocq",hs)::(cd_homs_icho c hs') (* else if hn = "icht" then *) -(* ("isa",hs)::("hol",hs)::("coq",hs)::("twf",hs)::(cd_homs_icho c hs') *) +(* ("isa",hs)::("hol",hs)::("rocq",hs)::("twf",hs)::(cd_homs_icho c hs') *) else if hn = "icho" then - ("isa",hs)::("hol",hs)::("coq",hs)::("ocaml",hs)::(cd_homs_icho c hs') + ("isa",hs)::("hol",hs)::("rocq",hs)::("ocaml",hs)::(cd_homs_icho c hs') else if hn = "ichl" then - ("isa",hs)::("hol",hs)::("coq",hs)::("lem",hs)::(cd_homs_icho c hs') + ("isa",hs)::("hol",hs)::("rocq",hs)::("lem",hs)::(cd_homs_icho c hs') else if hn = "ichlo" then - ("isa",hs)::("hol",hs)::("coq",hs)::("lem",hs)::("ocaml",hs)::(cd_homs_icho c hs') + ("isa",hs)::("hol",hs)::("rocq",hs)::("lem",hs)::("ocaml",hs)::(cd_homs_icho c hs') + else if hn = "ir" then + ("isa",hs)::("rocq",hs)::(cd_homs_icho c hs') + else if hn = "rh" then + ("rocq",hs)::("hol",hs)::(cd_homs_icho c hs') + else if hn = "irh" then + ("isa",hs)::("rocq",hs)::("hol",hs)::(cd_homs_icho c hs') + else if hn = "irho" then + ("isa",hs)::("rocq",hs)::("hol",hs)::("ocaml",hs)::(cd_homs_icho c hs') + else if hn = "irhl" then + ("isa",hs)::("rocq",hs)::("hol",hs)::("lem",hs)::(cd_homs_icho c hs') + else if hn = "irhlo" then + ("isa",hs)::("rocq",hs)::("hol",hs)::("lem",hs)::("ocaml",hs)::(cd_homs_icho c hs') else (hn,hs)::(cd_homs_icho c hs') @@ -817,7 +830,7 @@ and cd_prod c (rn:string) (pnw:string) (targets:string list) (rule_homs_for_targ List.filter (fun h -> match h with Hom_index _ -> true | _ -> false) (List.assoc "order" homs) in - let oh_coq = ( "coq", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in + let oh_coq = ( "rocq", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_isa = ( "isa", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_hol = let of_s = if List.length oh = 0 then "" else " of " in @@ -841,7 +854,7 @@ and cd_prod c (rn:string) (pnw:string) (targets:string list) (rule_homs_for_targ (List.filter (function Lang_nonterm _ | Lang_metavar _ -> true | _ -> false) elems)) [] in - let oh_coq = ( "coq", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in + let oh_coq = ( "rocq", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_isa = ( "isa", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_hol = ( "hol", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_lem = ( "lem", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in @@ -878,7 +891,12 @@ and cd_prod c (rn:string) (pnw:string) (targets:string list) (rule_homs_for_targ then ty_error2 p.raw_prod_loc ("illegal hom \"order\" in meta or sugar production") ""; List.iter (function target -> - if not (List.mem target def_homs) + let target_ok = + if target = "rocq" then + (List.mem "coq" def_homs) || (List.mem "rocq" def_homs) + else + List.mem target def_homs in + if not target_ok then ty_error2 p.raw_prod_loc ("meta or sugar production must have a hom for each target - here \"" ^target^"\" is missing") "") @@ -1481,7 +1499,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b raw_prod_flavour = Bar; raw_prod_categories = []; (* fd.raw_fd_categories; *) raw_prod_es = fd.raw_fd_es @ [ Raw_ident (dummy_loc,(dummy_loc,"===")); Raw_ident (dummy_loc,fd.raw_fd_result) ]; - raw_prod_homs = List.filter (function (hn,_,_) -> not (List.mem hn ["coq-struct"])) fd.raw_fd_homs; + raw_prod_homs = List.filter (function (hn,_,_) -> not (List.mem hn ["coq-struct";"rocq-struct"])) fd.raw_fd_homs; raw_prod_bs = []; raw_prod_loc = fd.raw_fd_loc } in @@ -1544,7 +1562,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b raw_prod_flavour = Bar; raw_prod_categories = [(dummy_loc,"M"); (dummy_loc,"F")]; (* fd.raw_fd_categories; *) (* FUNTODO: M ? *) raw_prod_es = fd.raw_fd_es; - raw_prod_homs = List.filter (function (hn,_,_) -> not (List.mem hn ["coq-struct"])) fd.raw_fd_homs; + raw_prod_homs = List.filter (function (hn,_,_) -> not (List.mem hn ["coq-struct";"rocq-struct"])) fd.raw_fd_homs; raw_prod_bs = []; raw_prod_loc = fd.raw_fd_loc } in @@ -1931,7 +1949,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b r.raw_rule_homs) in let rule_homs = if r.raw_rule_ntr_name = "formula" then - [("coq", [Hom_string "Prop"]); ("hol", [Hom_string "bool"]); + [("rocq", [Hom_string "Prop"]); ("hol", [Hom_string "bool"]); ("lem", [Hom_string "bool"]); ("isa", [Hom_string "bool"]); ("ocaml", [Hom_string "bool"])] else rule_homs in @@ -1965,7 +1983,8 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b | "tex-preamble" -> Some (l,"tex",he) | "tex-wrap-pre" | "tex-wrap-post" -> Some (l,hn,he) - | "coq-preamble" -> Some (l,"coq",he) + | "coq-preamble" -> Some (l,"rocq",he) + | "rocq-preamble" -> Some (l,"rocq",he) | "isa-preamble" -> Some (l,"isa",he) | "hol-preamble" -> Some (l,"hol",he) | "lem-preamble" -> Some (l,"lem",he) @@ -2000,7 +2019,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b mvd_names = List.map (function s,rhoms->(s,List.map (cd_hom Hu_root c []) rhoms)) mvd.raw_mvd_names; - mvd_rep = if ln then ("coq",[(Hom_string "var")])::mvd_rep else mvd_rep; + mvd_rep = if ln then ("rocq",[(Hom_string "var")])::mvd_rep else mvd_rep; mvd_indexvar = mvd.raw_mvd_indexvar; mvd_locally_nameless = ln; mvd_phantom = diff --git a/src/ln_transform.ml b/src/ln_transform.ml index f11be18..6b3d817 100644 --- a/src/ln_transform.ml +++ b/src/ln_transform.ml @@ -279,7 +279,7 @@ let ln_transform_rule (m:pp_mode) (xd:syntaxdefn) (r:rule) : rule = if bound_by_auxfn xd mvr then [ Lang_metavar ("nat",("nat",[Si_num "1"])); Lang_metavar ("nat",("nat",[Si_num "2"])) ] else [ Lang_metavar ("nat",("nat",[])) ]; - prod_homs = ("coq-ln_splitted",[Hom_string mvr])::p.prod_homs; + prod_homs = ("rocq-ln_splitted",[Hom_string mvr])::p.prod_homs; prod_disambiguate = None; prod_bs = []; prod_loc = p.prod_loc }; @@ -313,7 +313,7 @@ let ln_transform_rule (m:pp_mode) (xd:syntaxdefn) (r:rule) : rule = prod_es = [ Lang_terminal (open_name xd false r.rule_ntr_name wrt); Lang_nonterm (wrt,(wrt,[])); Lang_nonterm (r.rule_ntr_name,(r.rule_ntr_name,[])) ]; - prod_homs = [ ( "coq", + prod_homs = [ ( "rocq", [ Hom_string "("; Hom_string (open_name xd false r.rule_ntr_name wrt); Hom_index 0; @@ -422,7 +422,7 @@ let ln_add_cofinite_formula m xd mvrs = Lang_nonterm ("var_sets",("var_sets",[])); Lang_metavar (mvr, (mvr,[])); Lang_nonterm ("formula",("formula",[])) ]; - prod_homs = [ ("coq", [ Hom_string "("; + prod_homs = [ ("rocq", [ Hom_string "("; Hom_string "forall"; Hom_index 1; Hom_string ","; @@ -452,7 +452,7 @@ let ln_add_universal_formula m xd mvrs = prod_es = [ Lang_terminal "univ"; Lang_metavar (mvr, (mvr,[])); Lang_nonterm ("formula",("formula",[])) ]; - prod_homs = [ ("coq", [ Hom_string "("; + prod_homs = [ ("rocq", [ Hom_string "("; Hom_string "forall"; Hom_index 0; Hom_string ","; @@ -479,7 +479,7 @@ let ln_transform_syntaxdefn (m:pp_mode) (xd:syntaxdefn) : syntaxdefn = then [ { mvd_name = "var"; mvd_names = [ ("var",[]) ]; - mvd_rep = [("coq",[Hom_string "var"]) ]; + mvd_rep = [("rocq",[Hom_string "var"]) ]; mvd_indexvar = false; mvd_locally_nameless = false; mvd_phantom = true; @@ -488,7 +488,7 @@ let ln_transform_syntaxdefn (m:pp_mode) (xd:syntaxdefn) : syntaxdefn = @ ( { mvd_name = "nat"; mvd_names = [ ("nat",[]) ]; - mvd_rep = [("coq",[Hom_string "nat"]) ]; + mvd_rep = [("rocq",[Hom_string "nat"]) ]; mvd_indexvar = false; mvd_locally_nameless = false; mvd_phantom = true; @@ -496,7 +496,7 @@ let ln_transform_syntaxdefn (m:pp_mode) (xd:syntaxdefn) : syntaxdefn = :: { mvd_name = "vars"; mvd_names = [ ("vars",[]); ("L",[]) ]; - mvd_rep = [("coq",[Hom_string "vars"]) ]; + mvd_rep = [("rocq",[Hom_string "vars"]) ]; mvd_indexvar = false; mvd_locally_nameless = false; mvd_phantom = true; @@ -513,7 +513,7 @@ let ln_transform_syntaxdefn (m:pp_mode) (xd:syntaxdefn) : syntaxdefn = prod_sugar = false; prod_categories = StringSet.empty; prod_es = [ Lang_metavar ("vars",("vars",[])) ]; - prod_homs = [ ("coq", [ Hom_index 0 ]) ]; + prod_homs = [ ("rocq", [ Hom_index 0 ]) ]; prod_disambiguate = None; prod_bs = []; prod_loc = dummy_loc }; @@ -525,7 +525,7 @@ let ln_transform_syntaxdefn (m:pp_mode) (xd:syntaxdefn) : syntaxdefn = prod_es = [ Lang_nonterm ("var_sets",("var_sets",[])); Lang_terminal "union"; Lang_metavar ("var",("var",[])) ]; - prod_homs = [ ("coq", [ Hom_index 0; Hom_string "\\u {{"; Hom_index 1; Hom_string "}}" ]) ]; + prod_homs = [ ("rocq", [ Hom_index 0; Hom_string "\\u {{"; Hom_index 1; Hom_string "}}" ]) ]; prod_disambiguate = None; prod_bs = []; prod_loc = dummy_loc } @@ -638,7 +638,7 @@ and pp_open_symterm_list_body m xd mvr wrt s unshifted_nonterms ov sie de stlb = ^ de1i.de1_pattern^" => " ^pp_body^" end) " ^ de1i.de1_compound_id ^ ")", List.concat list_funcs ) - | _ -> ("<>",[]) + | _ -> ("<>",[]) @@ -656,7 +656,7 @@ let pp_open_prod m xd mvr wrt (ov:string) (rule_ntr_name:nontermroot) (p:prod) : (* we distinguish the case of the prod that splits mvr *) let splits = try - match List.assoc "coq-ln_splitted" p.prod_homs with + match List.assoc "rocq-ln_splitted" p.prod_homs with | [(Hom_string mvr1)] -> String.compare mvr mvr1 = 0 | _ -> false with Not_found -> false in @@ -979,7 +979,7 @@ let pp_lcs fd m xd : unit = let lcs_drule_from_prod r p = try - let _ = List.assoc "coq-ln_splitted" p.prod_homs + let _ = List.assoc "rocq-ln_splitted" p.prod_homs in None with Not_found -> let premises = make_premises r p in @@ -1491,7 +1491,7 @@ let ln_transform_symterms (m:pp_mode) (xd:syntaxdefn) (stlp:(string option * sym p.prod_bs in let nbss = (* nts that should not be opened wrt variables - look at homs *) try - let h = List.assoc "coq" p.prod_homs in + let h = List.assoc "rocq" p.prod_homs in Auxl.option_map ( fun hse -> match hse with | Hom_ln_free_index (fvis, nti) -> Some ((nti+1), (List.map (List.nth stnb.st_es) fvis)) diff --git a/src/main.ml b/src/main.ml index caa120f..a8ce304 100644 --- a/src/main.ml +++ b/src/main.ml @@ -56,9 +56,9 @@ let hol_filter_filename_dsts = ref ([] : string list) let lem_filter_filenames = ref ([] : (string * string) list) let lem_filter_filename_srcs = ref ([] : string list) let lem_filter_filename_dsts = ref ([] : string list) -let coq_filter_filenames = ref ([] : (string * string) list) -let coq_filter_filename_srcs = ref ([] : string list) -let coq_filter_filename_dsts = ref ([] : string list) +let rocq_filter_filenames = ref ([] : (string * string) list) +let rocq_filter_filename_srcs = ref ([] : string list) +let rocq_filter_filename_dsts = ref ([] : string list) let twf_filter_filenames = ref ([] : (string * string) list) let twf_filter_filename_srcs = ref ([] : string list) let twf_filter_filename_dsts = ref ([] : string list) @@ -88,11 +88,11 @@ let isa_syntax = ref false let isa_primrec = ref true let isa_inductive = ref true let isa_generate_lemmas = ref true -let coq_avoid = ref 1 -let coq_expand_lists = ref false -let coq_lngen = ref false -let coq_names_in_rules = ref true -let coq_use_filter_fn = ref false +let rocq_avoid = ref 1 +let rocq_expand_lists = ref false +let rocq_lngen = ref false +let rocq_names_in_rules = ref true +let rocq_use_filter_fn = ref false let merge_fragments = ref false let picky_multiple_parses = ref false let caml_include_terminals = ref false @@ -124,10 +124,10 @@ let options = Arg.align [ Arg.Tuple[Arg.String (fun s -> tex_filter_filename_srcs := s :: !tex_filter_filename_srcs); Arg.String (fun s -> tex_filter_filename_dsts := s :: !tex_filter_filename_dsts)], " Files to TeX filter" ); - ( "-coq_filter", - Arg.Tuple[Arg.String (fun s -> coq_filter_filename_srcs := s :: !coq_filter_filename_srcs); - Arg.String (fun s -> coq_filter_filename_dsts := s :: !coq_filter_filename_dsts)], - " Files to Coq filter" ); + ( "-rocq_filter", + Arg.Tuple[Arg.String (fun s -> rocq_filter_filename_srcs := s :: !rocq_filter_filename_srcs); + Arg.String (fun s -> rocq_filter_filename_dsts := s :: !rocq_filter_filename_dsts)], + " Files to Rocq filter" ); ( "-hol_filter", Arg.Tuple[Arg.String (fun s -> hol_filter_filename_srcs := s :: !hol_filter_filename_srcs); Arg.String (fun s -> hol_filter_filename_dsts := s :: !hol_filter_filename_dsts)], @@ -231,22 +231,22 @@ let options = Arg.align [ Arg.Bool (fun b -> isa_generate_lemmas := b), "<"^string_of_bool !isa_syntax ^"> Lemmas for collapsed functions in Isabelle" ); -(* options for coq output *) - ( "-coq_avoid", - Arg.Int (fun i -> coq_avoid := i), - "<"^string_of_int !coq_avoid^"> coq type-name avoidance\n (0=nothing, 1=avoid, 2=secondaryify)" ); - ( "-coq_expand_list_types", - Arg.Bool (fun b -> coq_expand_lists := b), - "<"^string_of_bool !coq_expand_lists^"> Expand list types in Coq output" ); - ( "-coq_lngen", - Arg.Bool (fun b -> coq_lngen := b), - "<"^string_of_bool !coq_lngen^"> lngen compatibility" ); - ( "-coq_names_in_rules", - Arg.Bool (fun b -> coq_names_in_rules := b), - "<"^string_of_bool !coq_names_in_rules^"> Copy user names in rule definitions" ); - ( "-coq_use_filter_fn", - Arg.Bool (fun b -> coq_use_filter_fn := b), - "<"^string_of_bool !coq_use_filter_fn^"> Use list_filter instead of list_minus2 in substitutions" ); +(* options for rocq output *) + ( "-rocq_avoid", + Arg.Int (fun i -> rocq_avoid := i), + "<"^string_of_int !rocq_avoid^"> rocq type-name avoidance\n (0=nothing, 1=avoid, 2=secondaryify)" ); + ( "-rocq_expand_list_types", + Arg.Bool (fun b -> rocq_expand_lists := b), + "<"^string_of_bool !rocq_expand_lists^"> Expand list types in Rocq output" ); + ( "-rocq_lngen", + Arg.Bool (fun b -> rocq_lngen := b), + "<"^string_of_bool !rocq_lngen^"> lngen compatibility" ); + ( "-rocq_names_in_rules", + Arg.Bool (fun b -> rocq_names_in_rules := b), + "<"^string_of_bool !rocq_names_in_rules^"> Copy user names in rule definitions" ); + ( "-rocq_use_filter_fn", + Arg.Bool (fun b -> rocq_use_filter_fn := b), + "<"^string_of_bool !rocq_use_filter_fn^"> Use list_filter instead of list_minus2 in substitutions" ); (* options for OCaml output *) ( "-ocaml_include_terminals", Arg.Bool (fun b -> caml_include_terminals := b), @@ -303,27 +303,40 @@ let usage_msg = let _ = print_string ("Ott version "^Version.n^" distribution of "^Version.d^"\n") -let _ = +(* Normalize flag names: replace "coq" with "rocq" for backward compatibility *) +let normalize_flag flag = + if String.length flag >= 4 && String.sub flag 0 4 = "-coq" then + "-rocq" ^ String.sub flag 4 (String.length flag - 4) + else + flag + +let _ = let extra_arguments = ref [] in - Arg.parse options - (fun s -> - if !i_arguments - then Auxl.exit_with None "must either use -i or specify all input filenames at the end of the command line" - else extra_arguments := (In,s) ::(!extra_arguments)) - usage_msg; + let normalized_argv = Array.map normalize_flag Sys.argv in + (try + Arg.parse_argv normalized_argv options + (fun s -> + if !i_arguments + then Auxl.exit_with None "must either use -i or specify all input filenames at the end of the command line" + else extra_arguments := (In,s) ::(!extra_arguments)) + usage_msg + with + | Arg.Help msg -> print_string msg; exit 0 + | Arg.Bad msg -> print_string msg; exit 2); file_arguments := !file_arguments @ !extra_arguments let _ = tex_filter_filenames := List.combine (!tex_filter_filename_srcs) (!tex_filter_filename_dsts) let _ = hol_filter_filenames := List.combine (!hol_filter_filename_srcs) (!hol_filter_filename_dsts) let _ = lem_filter_filenames := List.combine (!lem_filter_filename_srcs) (!lem_filter_filename_dsts) let _ = isa_filter_filenames := List.combine (!isa_filter_filename_srcs) (!isa_filter_filename_dsts) -let _ = coq_filter_filenames := List.combine (!coq_filter_filename_srcs) (!coq_filter_filename_dsts) +let _ = rocq_filter_filenames := List.combine (!rocq_filter_filename_srcs) (!rocq_filter_filename_dsts) let _ = twf_filter_filenames := List.combine (!twf_filter_filename_srcs) (!twf_filter_filename_dsts) let _ = caml_filter_filenames := List.combine (!caml_filter_filename_srcs) (!caml_filter_filename_dsts) let types_of_extensions = [ "ott","ott"; "tex","tex"; + "v", "rocq"; "v", "coq"; "thy","isa"; "sml","hol"; @@ -345,7 +358,7 @@ let file_type name = with _ -> None -let non_tex_output_types = ["coq"; "isa"; "hol"; "lem"; "twf"; "ocaml"] +let non_tex_output_types = ["rocq"; "coq"; "isa"; "hol"; "lem"; "twf"; "ocaml"] let output_types = "tex" :: "lex" :: "menhir" :: non_tex_output_types let input_types = "ott" :: output_types @@ -373,7 +386,7 @@ let classify_file_argument arg = (* *) (* values, containing first all the ott source files from the end of *) (* the command line, if any, then all the explicit -in and -out arguments, *) -(* and finally any -tex/-coq/-hol/-isabelle/-lem/-ocaml arguments *) +(* and finally any -tex/-rocq/-hol/-isabelle/-lem/-ocaml arguments *) let all_file_arguments = List.map classify_file_argument (List.rev (!file_arguments)) @@ -392,7 +405,7 @@ let targets_in ts = let targets_non_tex = targets_in non_tex_output_types let targets = targets_in output_types -let targets_for_non_picky = targets_in [(*"lex";"ocaml";*)"hol";"lem";"isa";"twf";"coq";"tex"] +let targets_for_non_picky = targets_in [(*"lex";"ocaml";*)"hol";"lem";"isa";"twf";"rocq";"coq";"tex"] (* collect the source filenames *) let source_filenames = @@ -426,7 +439,7 @@ let m_hol = Hol { hol_library = ref ("",[]); } let m_lem = Lem { lem_library = ref ("",[]); } let m_twf = Twf { twf_current_defn = ref ""; twf_library = ref ("",[]) } -let m_coq = Coq { coq_expand_lists = !coq_expand_lists; +let m_coq = Coq { coq_expand_lists = !rocq_expand_lists; coq_quantified_vars_from_de = ref []; coq_non_local_hyp_defn = ref ""; coq_non_local_hyp_defn_vars = ref []; @@ -435,9 +448,9 @@ let m_coq = Coq { coq_expand_lists = !coq_expand_lists; coq_list_aux_defns = { defined = ref []; newly_defined = ref [] }; coq_library = ref ("",[]); coq_locally_nameless = ref false; - coq_lngen = !coq_lngen; - coq_use_filter_fn = !coq_use_filter_fn; - coq_names_in_rules = !coq_names_in_rules } + coq_lngen = !rocq_lngen; + coq_use_filter_fn = !rocq_use_filter_fn; + coq_names_in_rules = !rocq_names_in_rules } let oo = { ppo_include_terminals = !caml_include_terminals; caml_library = ref ("",[]) } let m_caml = Caml oo @@ -527,6 +540,7 @@ let _ = "lem",m_lem; "isa",m_isa; "twf",m_twf; + "rocq",m_coq ; "coq",m_coq ; "tex",m_tex ]) targets_for_non_picky) @@ -765,13 +779,13 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = match t with | "tex" -> System_pp.pp_systemdefn_core_tex m_tex sd lookup fi - | "coq" -> + | "rocq" | "coq" -> let sd = - ( match !coq_avoid with + ( match !rocq_avoid with | 0 -> sd | 1 -> Auxl.avoid_primaries_systemdefn false sd | 2 -> Auxl.avoid_primaries_systemdefn true sd - | _ -> Auxl.error None "coq type-name avoidance must be in {0,1,2}" ) in + | _ -> Auxl.error None "rocq type-name avoidance must be in {0,1,2}" ) in System_pp.pp_systemdefn_core_io m_coq sd lookup fi !merge_fragments | "isa" -> System_pp.pp_systemdefn_core_io m_isa sd lookup fi !merge_fragments @@ -860,7 +874,7 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = in (List.iter (filter m_tex) (!tex_filter_filenames)); - (List.iter (filter m_coq) (!coq_filter_filenames)); + (List.iter (filter m_coq) (!rocq_filter_filenames)); (List.iter (filter m_isa) (!isa_filter_filenames)); (List.iter (filter m_hol) (!hol_filter_filenames)); (List.iter (filter m_lem) (!lem_filter_filenames)); diff --git a/src/transform.ml b/src/transform.ml index fbf123c..346c35c 100644 --- a/src/transform.ml +++ b/src/transform.ml @@ -34,7 +34,7 @@ open Types (* FZ: is this comment outdated ? *) -(* FZ: only for Coq, only the bare grammar (no homs...), *) +(* FZ: only for Rocq, only the bare grammar (no homs...), *) (* only for very simple suffixes *) type int_code = @@ -140,8 +140,9 @@ let expand_element (m:pp_mode) (xd:syntaxdefn) (bs:bindspec list) (e:element) : List.map (fun mvntr -> match mvntr with | Ntr ntr -> - ( try Grammar_pp.pp_hom_spec m xd (List.assoc "coq-universe" (Auxl.rule_of_ntr xd ntr).rule_homs) - with Not_found -> "Set" ) + ( match Auxl.hom_spec_for_hom_name "rocq-universe" (Auxl.rule_of_ntr xd ntr).rule_homs with + | Some hs -> Grammar_pp.pp_hom_spec m xd hs + | None -> "Set" ) | Mvr _ -> "Set") ss in if List.for_all (fun s -> String.compare s "Set" = 0) universes then "Set" @@ -238,7 +239,7 @@ let expand_element (m:pp_mode) (xd:syntaxdefn) (bs:bindspec list) (e:element) : rule_ntr_names = [ (id,[]) ]; rule_pn_wrapper = ""; rule_ps = [ nil_prod; cons_prod ]; - rule_homs = [("coq-universe", [Hom_string id_universe])]; + rule_homs = [("rocq-universe", [Hom_string id_universe])]; rule_meta = false; rule_semi_meta = false; rule_phantom = false; @@ -274,7 +275,7 @@ let expand_prod (m:pp_mode) (xd:syntaxdefn) (p:prod) : prod * rule list * (auxfn let expand_rule (m:pp_mode) (xd:syntaxdefn) (r:rule) : rule list * string list * (auxfn * auxfn_type) list = if (String.compare r.rule_ntr_name "formula" = 0) || - (List.exists (fun (h,_) -> String.compare h "coq" = 0) r.rule_homs) + (List.exists (fun (h,_) -> String.compare h "coq" = 0 || String.compare h "rocq" = 0) r.rule_homs) then ([r],[],[]) else let expanded_prods, new_rules, extended_auxfns = @@ -335,7 +336,7 @@ let expand_lists_in_syntaxdefn (m:pp_mode) (xd:syntaxdefn) (structure: structure if exp_list_aux_funcs = "" then [(Struct_rs (!newstruct@br), Some exp)] else [(Struct_rs (!newstruct@br), Some exp); - (Struct_embed (dummy_loc, "coq", [Embed_string (dummy_loc, exp_list_aux_funcs)]), None)] in + (Struct_embed (dummy_loc, "rocq", [Embed_string (dummy_loc, exp_list_aux_funcs)]), None)] in let (expanded_structure,exp) = List.split (List.concat (List.map @@ -405,10 +406,10 @@ let expand_lists_in_syntaxdefn (m:pp_mode) (xd:syntaxdefn) (structure: structure let expanded_deps = Dependency.compute_dependencies - { xd with xd_rs = expanded_rules; xd_dep = [] } "coq" in + { xd with xd_rs = expanded_rules; xd_dep = [] } "rocq" in { xd with xd_rs = expanded_rules; - xd_dep = [ ("coq", expanded_deps); ("ascii", expanded_deps) ]; + xd_dep = [ ("rocq", expanded_deps); ("ascii", expanded_deps) ]; xd_axs = expanded_auxfns }, expanded_structure diff --git a/tests/gmap1.rocq.ott b/tests/gmap1.rocq.ott new file mode 100644 index 0000000..052c495 --- /dev/null +++ b/tests/gmap1.rocq.ott @@ -0,0 +1,14 @@ +embed +{{ rocq +From stdpp Require Import gmap. +}} +metavar context ::= + {{ rocq gmap nat nat }} + {{ rocq-universe Type }} + {{ rocq-notation }} +embed +{{ rocq +Fact insert_lookup_ne_context: forall (C:context) i j x y, + i <> j -> C !! i = Some x -> <[j:=y]> C !! i = Some x. +Proof. by intros; simplify_map_eq. Qed. +}} diff --git a/tests/regexp.rocq.ott b/tests/regexp.rocq.ott new file mode 100644 index 0000000..0b37a86 --- /dev/null +++ b/tests/regexp.rocq.ott @@ -0,0 +1,96 @@ +embed +{{ rocq +Import ListNotations. +Section RegExp. +Variable char : Type. +}} +metavar c ::= + {{ lex alphanum }} + {{ com character }} + {{ rocq char }} + {{ hol char }} + {{ rocq-universe Type }} +grammar +s :: s_ ::= + {{ com string }} + {{ rocq list char }} + {{ hol char list }} + {{ rocq-universe Type }} + | e :: M :: empty + {{ rocq [] }} + {{ hol [] }} + {{ tex \epsilon }} + | c :: M :: char + {{ rocq ([[c]] :: []) }} + {{ hol ([[c]] :: []) }} + | s s' :: M :: concat + {{ rocq ([[s]] ++ [[s']]) }} + {{ hol ([[s]] ++ [[s']]) }} + +r :: r_ ::= + {{ com regexp }} + {{ rocq-universe Type }} + | 0 :: :: zero + | 1 :: :: unit + | c :: :: char + | r + r' :: :: plus + | r r' :: :: times + | r * :: :: star + {{ tex [[r]]^* }} + +terminals :: terminals_ ::= + | in :: :: in {{ tex \in }} + | L :: :: L {{ tex \mathit{L} }} + +formula :: formula_ ::= + | judgement :: :: judgement + +defns + regexp_ins :: '' ::= + +defn + s in L ( r ) :: :: s_in_regexp_lang :: s_in_regexp_lang_ + {{ com string in regexp language }} by + + --------- :: unit + e in L(1) + + ---------- :: char + c in L(c) + + s in L(r1) + ------------- :: plus_1 + s in L(r1+r2) + + s in L(r2) + ------------- :: plus_2 + s in L(r1+r2) + + s in L(r1) + s' in L(r2) + ---------------- :: times + s s' in L(r1 r2) + + ---------- :: star_1 + e in L(r*) + + s in L(r) + s' in L(r*) + ------------- :: star_2 + s s' in L(r*) + +defns + regexp_ins_c :: '' ::= + +defn + s in L ( r ; c ) :: :: s_in_regexp_c_lang :: s_in_regexp_c_lang_ + {{ com string in regexp c language }} by + + c s in L(r) + ----------- :: cs + s in L(r;c) + +embed +{{ rocq +End RegExp. +}} diff --git a/tests/test10.rocq.ott b/tests/test10.rocq.ott new file mode 100644 index 0000000..26133f0 --- /dev/null +++ b/tests/test10.rocq.ott @@ -0,0 +1,45 @@ +metavar var, x ::= {{ com term variable }} +{{ isa string}} {{ rocq nat}} {{ hol string}} {{ lem string }} {{ rocq-equality }} +{{ ocaml int}} {{ lex alphanum}} {{ tex \mathit{[[var]]} }} + +grammar +term, t :: 't_' ::= {{ com term }} + | x :: :: var {{ com variable}} + | \ x . t :: :: lam (+ bind x in t +) {{ com lambda }} + | t t' :: :: app {{ com app }} + | ( t ) :: S :: paren {{ icho [[t]] }} {{ lem [[t]] }} + | { t / x } t' :: M :: sub + {{ icho (tsubst_term [[t]] [[x]] [[t']])}} + {{ lem (tsubst_term [[t]] [[x]] [[t']]) }} +val,v :: 'v_' ::= {{ com value }} + | \ x . t :: :: lam {{ com lambda }} + +terminals :: 'terminals_' ::= + | \ :: :: lambda {{ tex \lambda }} + | --> :: :: red {{ tex \longrightarrow }} + +subrules + val <:: term + +substitutions + 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' + + diff --git a/tests/test8.rocq.ott b/tests/test8.rocq.ott new file mode 100644 index 0000000..0f1aa00 --- /dev/null +++ b/tests/test8.rocq.ott @@ -0,0 +1,240 @@ +metavar value_name, x ::= + {{ isa string }} {{ rocq nat }} {{ rocq-equality }} {{ hol string }} {{ ocaml int }} + {{ lex alphanum }} +metavar ident ::= + {{ isa string }} {{ rocq nat }} {{ hol string }} {{ ocaml int }} + {{ lex Alphanum }} +metavar integer_literal ::= + {{ isa int }} {{ rocq nat }} {{ hol num }} {{ ocaml int }} + {{ lex numeral }} +indexvar index, i, j, n, m ::= + {{ isa nat }} {{ rocq nat }} {{ hol num }} {{ ocaml int }} + {{ lex numeral }} +% the lex specifications above are not accurate - negative numerals, especially, +% should be supported + +grammar +typeconstr :: TC_ ::= + | unit :: :: unit + | bool :: :: bool + | int :: :: int + +typvar, tv :: TV_ ::= {{ rocq-equality decide equality. apply eq_value_name. }} + | ' ident :: :: ident + +typexpr, t :: TE_ ::= + | typvar :: :: var + | typexpr -> typexpr' :: :: arrow + | typeconstr :: :: constr0 + | ( typexpr ) :: S :: paren {{ ich [[typexpr]] }} {{ ocaml [[typexpr]] }} + +typscheme, ts :: TS_ ::= + | ( typvar1 , .. , typvarn ) typexpr :: :: ts (+ bind typvar1 .. typvarn in typexpr +) + + | generalise ( G , t ) :: M :: ts3 + {{ isa (TS_ts (List.remdups (list_minus (ftv_typexpr [[t]]) (ftv_G [[G]]))) [[t]]) }} + {{ rocq (TS_ts (remove_duplicates (make_list_typvar (list_minus eq_typvar (ftv_typexpr [[t]]) (ftv_G [[G]])))) [[t]]) }} + {{ hol (TS_ts (remove_duplicates (list_minus (ftv_typexpr [[t]]) (ftv_G [[G]]))) [[t]]) }} + {{ ocaml TODO }} + +%TODO: it might be nicer to have ftv remove duplicates, or indeed +%return a set + +constant, c :: CONST_ ::= + | integer_literal :: :: int + | false :: :: false + | true :: :: true + | () :: :: unit + | (&&) :: :: and + | not :: :: not + +expr, e :: E_ ::= + | value_name :: :: ident + | constant :: :: constant + | expr expr' :: :: apply + | function value_name -> expr :: :: function (+ bind value_name in expr +) + | let value_name = expr in expr' :: :: let (+ bind value_name in expr' +) + | ( expr ) :: S :: paren {{ ich [[expr]] }} {{ ocaml [[expr]] }} + | { v / x } e :: M :: subst + {{ isa subst_expr [[v]] [[x]] [[e]] }} + {{ ch (subst_expr [[v]] [[x]] [[e]]) }} + {{ ocaml (subst_expr [[v]] [[x]] [[e]]) }} + +value, v :: V_ ::= + | constant :: :: constant + | function value_name -> expr :: :: function + +G {{ tex \Gamma }} :: G_ ::= + | empty :: :: em + | G , value_name : typscheme :: :: vn + +formula :: formula_ ::= + | judgement :: :: judgement + | not ( formula ) :: :: not + {{ isa Not([[formula]]) }} + {{ rocq not([[formula]]) }} + {{ hol ~([[formula]]) }} + {{ ocaml TODO }} + + | typscheme > t :: :: gen + {{ isa ? typvars . ? typexpr . ? s . + [[typscheme]] = TS_ts typvars typexpr + & typvars=List.map fst s + & tsubst_typexpr s typexpr = [[t]] }} + {{ rocq (exists tvs, exists txp, exists s, + [[typscheme]] = TS_ts tvs txp + /\ tvs = make_list_typvar + (List.map (fun (x:typvar*typexpr) => match x with (x1,x2) => x1 end) + s) + /\ tsubst_typexpr s txp = [[t]]) }} + {{ hol ? typvars typexpr s . + ([[typscheme]] = TS_ts typvars typexpr ) + /\ (typvars=MAP FST s ) + /\ (tsubst_typexpr s typexpr = [[t]]) }} + {{ ocaml TODO }} + + | typscheme = typscheme' :: :: eqt + {{ ich [[typscheme]]=[[typscheme']] }} {{ ocaml TODO }} + | value_name = value_name' :: :: eqv + {{ ich [[value_name]]=[[value_name']] }} {{ ocaml TODO }} + +terminals :: terminals_ ::= + | -> :: :: arrow {{ tex \rightarrow }} + | function :: :: function {{ tex \textbf{function} }} + | |- :: :: turnstile {{ tex \vdash }} + | --> :: :: red {{ tex \longrightarrow }} + | '{' :: :: leftbrace {{ tex \{ }} + | '}' :: :: rightbrace {{ tex \} }} + + +subrules + v <:: expr + +substitutions + single expr value_name :: subst + multiple typexpr typvar :: tsubst + +freevars + typexpr typvar :: ftv + +embed + {{ coq +Fixpoint remove_duplicates (l:list_typvar) : list_typvar := + match l with + | Nil_list_typvar => Nil_list_typvar + | Cons_list_typvar h t => + if (list_mem eq_typvar h (unmake_list_typvar t)) + then remove_duplicates t + else Cons_list_typvar h (remove_duplicates t) +end. }} + + {{ hol +val _ = Define ` + (remove_duplicates [] = []) /\ + (remove_duplicates (x::xs) = if (MEM x xs) then remove_duplicates xs + else x::(remove_duplicates xs)) +`; }} + + +defns +Jtype :: '' ::= + +defn +value_name : typscheme in G :: :: VTSin :: VTSin_ by + +--------------------------------------------------- :: vn1 +value_name : typscheme in G, value_name:typscheme + +value_name : typscheme in G +not(value_name = value_name') +--------------------------------------------------- :: vn2 +value_name : typscheme in G, value_name':typscheme' + + + +defn +G |- constant : t :: :: G_constant :: constant_ by + +-------------------------- :: int +G |- integer_literal : int + +----------------- :: false +G |- false : bool + +---------------- :: true +G |- true : bool + +-------------- :: unit +G |- () : unit + +------------------------------------ :: and +G |- (&&) : bool -> ( bool -> bool ) + +----------------------- :: not +G |- not : bool -> bool + + +defn +G |- e : t :: :: Get :: Get_ by + +x:typscheme in G +typscheme > t +---------------- :: value_name +G |- x:t + +:G_constant: G |- constant : t +------------------------------ :: constant +G |- constant : t + +G |- e : t1->t2 +G |- e' : t1 +---------------- :: apply +G |- e e' : t2 + +G,x1: ( ) t1 |- e : t +--------------------------- I :: lambda +G |- function x1->e : t1->t + +G |- e : t +G,x:typscheme |- e':t' +typscheme = generalise(G,t) +--------------------------- :: let +G |- let x=e in e' : t' + + +defns +Jop :: JO_ ::= + +defn +e --> e' :: :: red :: red_ by + +------------------------------- :: app +(function x->e) v --> {v/x} e + +--------------------------- :: let +let x = v in e --> {v/x} e + +e --> e' +-------------- :: context_app1 +e e1 --> e' e1 + +e --> e' +------------ :: context_app2 +v e --> v e' + +e --> e' +-------------------------------- :: context_let +let x=e in e1 --> let x=e' in e1 + +------------------ :: not_1 +not true --> false + +------------------ :: not_2 +not false --> true + +------------------- :: and_1 +((&&) true) e --> e + +------------------------ :: and_2 +((&&) false) e --> false + diff --git a/tests/test_cr_metahoms.ott b/tests/test_cr_metahoms.ott new file mode 100644 index 0000000..7e06b74 --- /dev/null +++ b/tests/test_cr_metahoms.ott @@ -0,0 +1,36 @@ +% Test file for all metahoms containing 'c' or 'r' +% This tests both backward compatibility (c-prefixed) and new Rocq naming (r-prefixed) + +grammar + +% Test all c-prefixed and r-prefixed metahoms in one nonterminal +nonterminal :: T ::= + % Old c-prefixed metahoms (backward compatibility) + | x :: :: var_ic + {{ ic isa rocq old style }} + | T '+' T :: :: plus_ch + {{ ch hol rocq old style }} + | '(' T ')' :: :: paren_ich + {{ ich isa hol rocq old style }} + | T '*' T :: :: mult_icho + {{ icho isa hol rocq ocaml old style }} + | T '-' T :: :: minus_ichl + {{ ichl isa hol rocq lem old style }} + | T '/' T :: :: div_ichlo + {{ ichlo isa hol rocq lem ocaml old style }} + % New r-prefixed metahoms (Rocq naming) + | y :: :: var_ir + {{ ir isa rocq new style }} + | T '&' T :: :: and_rh + {{ rh rocq hol new style }} + | '[' T ']' :: :: bracket_irh + {{ irh isa rocq hol new style }} + | T '^' T :: :: exp_irho + {{ irho isa rocq hol ocaml new style }} + | T '%' T :: :: mod_irhl + {{ irhl isa rocq hol lem new style }} + | T '~' T :: :: tilde_irhlo + {{ irhlo isa rocq hol lem ocaml new style }} + % Test ih metahom (contains h but not c, should still work) + | z :: :: var_ih + {{ ih isa hol no change needed }} \ No newline at end of file diff --git a/tests/test_rocq_keywords.ott b/tests/test_rocq_keywords.ott new file mode 100644 index 0000000..d70bc62 --- /dev/null +++ b/tests/test_rocq_keywords.ott @@ -0,0 +1,17 @@ +% Test file for rocq keywords (beginrocqsection, endrocqsection, rocqvariable) + +grammar +t :: 't_' ::= {{ com term }} + | x :: :: var {{ com variable }} + | t t' :: :: app {{ com application }} + +beginrocqsection TestSection + +rocqvariable x + +embed +{{ rocq +Definition test_fun (x : nat) : nat := x + 1. +}} + +endrocqsection TestSection