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).
jrh13 · Jul 31, 2024 · 7b2d535 · 7b2d535
1 parent 16b184e
commit 7b2d535
Show file tree

Hide file tree

Showing 11 changed files with 143 additions and 61 deletions.
diff --git 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
@@ -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
@@ -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,24 +134,20 @@ 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);
   Format.pp_close_box fmt ();;
 
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -49,14 +49,35 @@ 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"          *)
 (* ------------------------------------------------------------------------- *)
 
 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
@@ -49,14 +49,35 @@ 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"          *)
 (* ------------------------------------------------------------------------- *)
 
 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
@@ -59,14 +59,35 @@ 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"          *)
 (* ------------------------------------------------------------------------- *)
 
 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
@@ -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;;