From 7b2d535abe383a6cb2770b827745a73036598e00 Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Mon, 29 Jul 2024 18:12:59 -0500 Subject: [PATCH] Enable using pa_j as a standalone camlp5r preprocessor This patch enables using pa_j.cmo as a standalone camlp5 preprocessor. For example, pa_j.cmo now can be used with camlp5r to preprocess a file 'test.ml' using the following command: ``` ~/hol-light$ ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I . pa_j.cmo" test.ml * HOL-Light syntax in effect * File "test.ml", line 1, characters 8-15: 1 | let x = `1 + 2`;; ^^^^^^^ Error: Unbound value parse_term ``` This is necessary to support module compilation of HOL Light because this patch will enable preprocessing .ml files for compilation. To achieve this, - Printing "* HOL-Light syntax in effect *" is redirected to stderr, not stdout, because ocamlc was consuming the log from from stdout too. - jrh_lexer is enabled by default. - quotexpander is moved to pa_j.ml . - bignum files had to be separately compiled without using pa_j because they were declaring modules which interfere with the preprocessor. pa_j files for OCaml 4.xx were only updated because it was not clear how to support pa_j with OCaml 3. I was curious whether OCaml version 3 should be kept supported, however... Checked that holtest.mk works with OCaml 4.14 + camlp5 8.03 and OCaml 4.05 + camlp5 7.10. The timeouts of a few tactics in miz3 had to be increased (probably due to its nondeterminism). --- Makefile | 17 +++++++++++++---- bignum_num.ml | 4 +--- bignum_zarith.ml | 26 ++++++++++++-------------- hol.ml | 5 ++--- miz3/Samples/irrat2.ml | 4 ++-- pa_j/pa_j_4.xx_7.06.ml | 23 ++++++++++++++++++++++- pa_j/pa_j_4.xx_7.xx.ml | 23 ++++++++++++++++++++++- pa_j/pa_j_4.xx_8.00.ml | 25 +++++++++++++++++++++++-- pa_j/pa_j_4.xx_8.02.ml | 25 +++++++++++++++++++++++-- pa_j/pa_j_4.xx_8.03.ml | 25 +++++++++++++++++++++++-- system.ml | 27 --------------------------- 11 files changed, 143 insertions(+), 61 deletions(-) diff --git a/Makefile b/Makefile index ef57d9ed..70e2f9aa 100644 --- a/Makefile +++ b/Makefile @@ -97,13 +97,22 @@ pa_j.ml: pa_j/pa_j_3.07.ml pa_j/pa_j_3.08.ml pa_j/pa_j_3.09.ml \ else cp pa_j/pa_j_3.1x_${CAMLP5_UNARY_VERSION}.xx.ml pa_j.ml; \ fi +# Choose an appropriate bignum library. + +bignum.cmo: bignum_zarith.ml bignum_num.ml ; \ + if test ${OCAML_VERSION} = "4.14" -o ${OCAML_UNARY_VERSION} = "5" ; \ + then ocamlfind ocamlc -package zarith -c -o bignum.cmo bignum_zarith.ml ; \ + else ocamlc -c -o bignum.cmo bignum_num.ml ; \ + fi + # Create a bash script 'hol.sh' that loads 'hol.ml' in OCaml REPL. -hol.sh: pa_j.cmo ${HOLSRC} update_database.ml ; \ +hol.sh: pa_j.cmo ${HOLSRC} bignum.cmo update_database.ml ; \ if [ `uname` = "Linux" ] || [ `uname` = "Darwin" ] ; then \ if [ ${OCAML_UNARY_VERSION} = "5" ] || [ ${OCAML_VERSION} = "4.14" ] ; \ - then ocamlmktop -o ocaml-hol ; sed "s^__DIR__^`pwd`^g" hol_4.14.sh > hol.sh ; \ - else ocamlmktop -o ocaml-hol nums.cma ; sed "s^__DIR__^`pwd`^g" hol_4.sh > hol.sh ; \ + then ocamlfind ocamlmktop -package zarith -o ocaml-hol zarith.cma bignum.cmo ; \ + sed "s^__DIR__^`pwd`^g" hol_4.14.sh > hol.sh ; \ + else ocamlmktop -o ocaml-hol nums.cma bignum.cmo ; sed "s^__DIR__^`pwd`^g" hol_4.sh > hol.sh ; \ fi ; \ chmod +x hol.sh ; \ else \ @@ -169,4 +178,4 @@ install: hol.sh hol hol.multivariate hol.sosa hol.card hol.complex; cp hol hol.m # Clean up all compiled files -clean:; rm -f update_database.ml pa_j.ml pa_j.cmi pa_j.cmo ocaml-hol hol.sh hol hol.multivariate hol.sosa hol.card hol.complex; +clean:; rm -f bignum.cmo update_database.ml pa_j.ml pa_j.cmi pa_j.cmo ocaml-hol hol.sh hol hol.multivariate hol.sosa hol.card hol.complex; diff --git a/bignum_num.ml b/bignum_num.ml index 6744b0e4..622ec190 100644 --- a/bignum_num.ml +++ b/bignum_num.ml @@ -2,8 +2,6 @@ (* Load in the bignum library. *) (* ------------------------------------------------------------------------- *) -#load "nums.cma";; - include Num;; let num = Num.num_of_int;; @@ -18,4 +16,4 @@ module NumExt = struct num_of_big_int(Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2));; end;; -open NumExt;; +include NumExt;; diff --git a/bignum_zarith.ml b/bignum_zarith.ml index d01a96b5..7f370680 100644 --- a/bignum_zarith.ml +++ b/bignum_zarith.ml @@ -2,8 +2,6 @@ (* Load in the bignum library. *) (* ------------------------------------------------------------------------- *) -Topfind.load_deeply ["zarith"];; - (* A wrapper of Zarith that has an interface of Num. However, this is different from the real Num library because it supports infinity and undef. If exception happens, Failure with the name of the @@ -19,11 +17,6 @@ module Num = struct let float_of_num (n:num):float = Q.to_float n - (* base must be Z.t and exponent - must fit in the range of OCaml int type *) - let power_num (base:num) (exponent:num):num = - let exp_i = int_of_num exponent in - Q.of_bigint (Z.pow (Q.to_bigint base) exp_i) let pow (base:num) (exponent:int):num = Q.of_bigint (Z.pow (Q.to_bigint base) exponent) @@ -106,6 +99,15 @@ module Num = struct let num_of_big_int = Q.of_bigint + (* base must be Z.t and exponent + must fit in the range of OCaml int type *) + let power_num (base:num) (exponent:num):num = + let f (base:num) (exponent:num):num = + let exp_i = int_of_num exponent in + Q.of_bigint (Z.pow (Q.to_bigint base) exp_i) in + if ge_num exponent (num_of_int 0) then f base exponent + else div_num (num_of_int 1) (f base (minus_num exponent));; + end;; module Big_int = struct @@ -132,6 +134,8 @@ let (<=/) x y = Num.le_num x y;; let (>=/) x y = Num.ge_num x y;; +let ( **/) x y = Num.power_num x y;; + let pp_print_num fmt (n:Num.num) = Format.pp_open_hbox fmt (); Format.pp_print_string fmt (Num.string_of_num n); @@ -139,17 +143,11 @@ let pp_print_num fmt (n:Num.num) = let print_num = pp_print_num Format.std_formatter;; -#install_printer pp_print_num;; include Num;; let num = Num.num_of_int;; -let ( **/) x y = - if y >=/ num 0 then Num.power_num x y - else num 1 // Num.power_num x (minus_num y);; - -let power_num = ( **/);; module NumExt = struct let numdom (r:num):num * num = @@ -160,4 +158,4 @@ module NumExt = struct end;; -open NumExt;; +include NumExt;; diff --git a/hol.ml b/hol.ml index 4ff6f2be..dededb1a 100644 --- a/hol.ml +++ b/hol.ml @@ -98,9 +98,8 @@ else loads "load_camlp4.ml";; Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");; -if version_ge_4_14 -then loads "bignum_zarith.ml" -else loads "bignum_num.ml";; +include Bignum;; + (* ------------------------------------------------------------------------- *) (* Bind these to names that are independent of OCaml versions before they *) diff --git a/miz3/Samples/irrat2.ml b/miz3/Samples/irrat2.ml index 4c3a50e4..b1612524 100644 --- a/miz3/Samples/irrat2.ml +++ b/miz3/Samples/irrat2.ml @@ -66,7 +66,7 @@ let NSQRT_2_2 = thm `; (2 * m) * 2 * m = 2 * q * q ==> (q < 2 * m ==> q * q = 2 * m * m ==> m = 0) ==> q = 0 - by TIMED_TAC 2 (CONV_TAC SOS_RULE); + by TIMED_TAC 20 (CONV_TAC SOS_RULE); (q < 2 * m ==> q * q = 2 * m * m ==> m = 0) ==> q = 0 by POP_ASSUM MP_TAC,4 from -; thus q = 0 by FIRST_X_ASSUM @@ -126,7 +126,7 @@ let NSQRT_2_3 = thm `; EVEN p by 2,EVEN_MULT; consider m such that p = 2*m [3] by EVEN_EXISTS; (2*m)*2*m = 2*q*q /\ (q < 2*m /\ q*q = 2*m*m ==> m = 0) ==> q = 0 - from TIMED_TAC 2 (CONV_TAC SOS_RULE); + from TIMED_TAC 20 (CONV_TAC SOS_RULE); thus q = 0 by 1,2,3; end; qed by MATCH_MP_TAC num_WF`;; diff --git a/pa_j/pa_j_4.xx_7.06.ml b/pa_j/pa_j_4.xx_7.06.ml index 76ded4e3..dc12afb3 100644 --- a/pa_j/pa_j_4.xx_7.06.ml +++ b/pa_j/pa_j_4.xx_7.06.ml @@ -767,11 +767,32 @@ value eq_class_expr x y = #load "pa_lexer.cmo"; +(* ------------------------------------------------------------------------- *) +(* Set up a quotation expander for the `...` quotes. *) +(* This includes the case `;...` to support miz3, even if that isn't loaded. *) +(* Other quotations ending in `...:` are treated just as (escaped) strings, *) +(* so they can be parsed in a type context etc. *) +(* ------------------------------------------------------------------------- *) + +value quotexpander s = + if s = "" then failwith "Empty quotation" else + let c = String.sub s 0 1 in + if c = ":" then + "parse_type \""^ + (String.escaped (String.sub s 1 (String.length s - 1)))^"\"" + else if c = ";" then "parse_qproof \""^(String.escaped s)^"\"" else + let n = String.length s - 1 in + if String.sub s n 1 = ":" + then "\""^(String.escaped (String.sub s 0 n))^"\"" + else "parse_term \""^(String.escaped s)^"\""; + +Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander)); + (* ------------------------------------------------------------------------- *) (* Added by JRH as a backdoor to change lexical conventions. *) (* ------------------------------------------------------------------------- *) -value jrh_lexer = ref False; +value jrh_lexer = ref True; open Versdep; diff --git a/pa_j/pa_j_4.xx_7.xx.ml b/pa_j/pa_j_4.xx_7.xx.ml index 4f7ed606..3c678c10 100755 --- a/pa_j/pa_j_4.xx_7.xx.ml +++ b/pa_j/pa_j_4.xx_7.xx.ml @@ -767,11 +767,32 @@ value eq_class_expr x y = #load "pa_lexer.cmo"; +(* ------------------------------------------------------------------------- *) +(* Set up a quotation expander for the `...` quotes. *) +(* This includes the case `;...` to support miz3, even if that isn't loaded. *) +(* Other quotations ending in `...:` are treated just as (escaped) strings, *) +(* so they can be parsed in a type context etc. *) +(* ------------------------------------------------------------------------- *) + +value quotexpander s = + if s = "" then failwith "Empty quotation" else + let c = String.sub s 0 1 in + if c = ":" then + "parse_type \""^ + (String.escaped (String.sub s 1 (String.length s - 1)))^"\"" + else if c = ";" then "parse_qproof \""^(String.escaped s)^"\"" else + let n = String.length s - 1 in + if String.sub s n 1 = ":" + then "\""^(String.escaped (String.sub s 0 n))^"\"" + else "parse_term \""^(String.escaped s)^"\""; + +Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander)); + (* ------------------------------------------------------------------------- *) (* Added by JRH as a backdoor to change lexical conventions. *) (* ------------------------------------------------------------------------- *) -value jrh_lexer = ref False; +value jrh_lexer = ref True; open Versdep; diff --git a/pa_j/pa_j_4.xx_8.00.ml b/pa_j/pa_j_4.xx_8.00.ml index 9bed3c92..ce62d7b3 100755 --- a/pa_j/pa_j_4.xx_8.00.ml +++ b/pa_j/pa_j_4.xx_8.00.ml @@ -49,6 +49,27 @@ value err ctx loc msg = Ploc.raise (ctx.make_lined_loc loc "") (Plexing.Error msg) ; +(* ------------------------------------------------------------------------- *) +(* Set up a quotation expander for the `...` quotes. *) +(* This includes the case `;...` to support miz3, even if that isn't loaded. *) +(* Other quotations ending in `...:` are treated just as (escaped) strings, *) +(* so they can be parsed in a type context etc. *) +(* ------------------------------------------------------------------------- *) + +value quotexpander s = + if s = "" then failwith "Empty quotation" else + let c = String.sub s 0 1 in + if c = ":" then + "parse_type \""^ + (String.escaped (String.sub s 1 (String.length s - 1)))^"\"" + else if c = ";" then "parse_qproof \""^(String.escaped s)^"\"" else + let n = String.length s - 1 in + if String.sub s n 1 = ":" + then "\""^(String.escaped (String.sub s 0 n))^"\"" + else "parse_term \""^(String.escaped s)^"\""; + +Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander)); + (* ------------------------------------------------------------------------- *) (* JRH's hack to make the case distinction "unmixed" versus "mixed" *) (* ------------------------------------------------------------------------- *) @@ -56,7 +77,7 @@ value err ctx loc msg = value is_uppercase s = String.uppercase_ascii s = s; value is_only_lowercase s = String.lowercase_ascii s = s && not(is_uppercase s); -value jrh_lexer = ref False; +value jrh_lexer = ref True; value jrh_identifier find_kwd id = let jflag = jrh_lexer.val in @@ -1075,7 +1096,7 @@ value gmake () = open Asttools; do { - Printf.printf " * HOL-Light syntax in effect *\n\n"; + Printf.eprintf " * HOL-Light syntax in effect *\n\n"; dollar_for_antiquotation.val := False; simplest_raw_strings.val := True; utf8_lexing.val := True; diff --git a/pa_j/pa_j_4.xx_8.02.ml b/pa_j/pa_j_4.xx_8.02.ml index e5b44c4c..56a40108 100644 --- a/pa_j/pa_j_4.xx_8.02.ml +++ b/pa_j/pa_j_4.xx_8.02.ml @@ -49,6 +49,27 @@ value err ctx loc msg = Ploc.raise (ctx.make_lined_loc loc "") (Plexing.Error msg) ; +(* ------------------------------------------------------------------------- *) +(* Set up a quotation expander for the `...` quotes. *) +(* This includes the case `;...` to support miz3, even if that isn't loaded. *) +(* Other quotations ending in `...:` are treated just as (escaped) strings, *) +(* so they can be parsed in a type context etc. *) +(* ------------------------------------------------------------------------- *) + +value quotexpander s = + if s = "" then failwith "Empty quotation" else + let c = String.sub s 0 1 in + if c = ":" then + "parse_type \""^ + (String.escaped (String.sub s 1 (String.length s - 1)))^"\"" + else if c = ";" then "parse_qproof \""^(String.escaped s)^"\"" else + let n = String.length s - 1 in + if String.sub s n 1 = ":" + then "\""^(String.escaped (String.sub s 0 n))^"\"" + else "parse_term \""^(String.escaped s)^"\""; + +Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander)); + (* ------------------------------------------------------------------------- *) (* JRH's hack to make the case distinction "unmixed" versus "mixed" *) (* ------------------------------------------------------------------------- *) @@ -56,7 +77,7 @@ value err ctx loc msg = value is_uppercase s = String.uppercase_ascii s = s; value is_only_lowercase s = String.lowercase_ascii s = s && not(is_uppercase s); -value jrh_lexer = ref False; +value jrh_lexer = ref True; value jrh_identifier find_kwd id = let jflag = jrh_lexer.val in @@ -1075,7 +1096,7 @@ value gmake () = open Asttools; do { - Printf.printf " * HOL-Light syntax in effect *\n\n"; + Printf.eprintf " * HOL-Light syntax in effect *\n\n"; dollar_for_antiquotation.val := False; simplest_raw_strings.val := True; utf8_lexing.val := True; diff --git a/pa_j/pa_j_4.xx_8.03.ml b/pa_j/pa_j_4.xx_8.03.ml index d7c99404..410ec8df 100755 --- a/pa_j/pa_j_4.xx_8.03.ml +++ b/pa_j/pa_j_4.xx_8.03.ml @@ -59,6 +59,27 @@ value err ctx loc msg = Ploc.raise (ctx.make_lined_loc loc "") (Plexing.Error msg) ; +(* ------------------------------------------------------------------------- *) +(* Set up a quotation expander for the `...` quotes. *) +(* This includes the case `;...` to support miz3, even if that isn't loaded. *) +(* Other quotations ending in `...:` are treated just as (escaped) strings, *) +(* so they can be parsed in a type context etc. *) +(* ------------------------------------------------------------------------- *) + +value quotexpander s = + if s = "" then failwith "Empty quotation" else + let c = String.sub s 0 1 in + if c = ":" then + "parse_type \""^ + (String.escaped (String.sub s 1 (String.length s - 1)))^"\"" + else if c = ";" then "parse_qproof \""^(String.escaped s)^"\"" else + let n = String.length s - 1 in + if String.sub s n 1 = ":" + then "\""^(String.escaped (String.sub s 0 n))^"\"" + else "parse_term \""^(String.escaped s)^"\""; + +Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander)); + (* ------------------------------------------------------------------------- *) (* JRH's hack to make the case distinction "unmixed" versus "mixed" *) (* ------------------------------------------------------------------------- *) @@ -66,7 +87,7 @@ value err ctx loc msg = value is_uppercase s = String.uppercase_ascii s = s; value is_only_lowercase s = String.lowercase_ascii s = s && not(is_uppercase s); -value jrh_lexer = ref False; +value jrh_lexer = ref True; value jrh_identifier find_kwd id = let jflag = jrh_lexer.val in @@ -1127,7 +1148,7 @@ open Asttools; do { (*** HOL Light ***) - Printf.printf " * HOL-Light syntax in effect *\n\n"; + Printf.eprintf " * HOL-Light syntax in effect *\n\n"; dollar_for_antiquotation.val := False; simplest_raw_strings.val := True; utf8_lexing.val := True; diff --git a/system.ml b/system.ml index 402cec3a..7be5b6f8 100644 --- a/system.ml +++ b/system.ml @@ -24,30 +24,3 @@ let pp_print_num fmt n = let print_num = pp_print_num Format.std_formatter;; #install_printer pp_print_num;; - -(* ------------------------------------------------------------------------- *) -(* Set up a quotation expander for the `...` quotes. *) -(* This includes the case `;...` to support miz3, even if that isn't loaded. *) -(* Other quotations ending in `...:` are treated just as (escaped) strings, *) -(* so they can be parsed in a type context etc. *) -(* ------------------------------------------------------------------------- *) - -let quotexpander s = - if s = "" then failwith "Empty quotation" else - let c = String.sub s 0 1 in - if c = ":" then - "parse_type \""^ - (String.escaped (String.sub s 1 (String.length s - 1)))^"\"" - else if c = ";" then "parse_qproof \""^(String.escaped s)^"\"" else - let n = String.length s - 1 in - if String.sub s n 1 = ":" - then "\""^(String.escaped (String.sub s 0 n))^"\"" - else "parse_term \""^(String.escaped s)^"\"";; - -Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander));; - -(* ------------------------------------------------------------------------- *) -(* Modify the lexical analysis of uppercase identifiers. *) -(* ------------------------------------------------------------------------- *) - -set_jrh_lexer;;