diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 0a7614b..b302ac7 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -14,7 +14,8 @@ jobs: strategy: matrix: image: - - 'coqorg/coq:dev' + - 'coqorg/coq:8.20' + - 'rocq/rocq-prover:9.0' fail-fast: false steps: - uses: actions/checkout@v4 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 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/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/baseline-2025-03.bl b/regression/baseline-2025-03.bl new file mode 100644 index 0000000..55f7574 Binary files /dev/null and b/regression/baseline-2025-03.bl differ 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.ml b/regression/regression.ml index 3cd122c..c50bec9 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 _ = @@ -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 @@ -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 diff --git a/regression/regression.otl b/regression/regression.otl index 04d939d..9db842c 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 @@ -99,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/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 _ = 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/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/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/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 90727f6..22e6959 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 @@ -534,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 @@ -712,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 48c1b59..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") "") @@ -1397,7 +1415,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 @@ -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 = @@ -2468,14 +2487,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..949f450 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 *) @@ -916,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") ) @@ -941,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") ) @@ -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/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 0c67e50..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 @@ -488,6 +501,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 @@ -526,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) @@ -612,9 +627,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 +637,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 @@ -760,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 @@ -855,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/subrules_pp.ml b/src/subrules_pp.ml index 002ccec..5638bb0 100644 --- a/src/subrules_pp.ml +++ b/src/subrules_pp.ml @@ -117,30 +117,37 @@ 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, 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_lower=primary_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 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 + ^ ")"], [Auxl.pp_is ntrpl promoted_upper], [] + with Not_found -> [],[],[]) | Lang_metavar _, Lang_metavar _ -> [],[],[] | Lang_terminal _, Lang_terminal _ -> [],[],[] 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"])) 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/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 *) 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/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' - - 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 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/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 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_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. +}} 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