Skip to content

Commit

Permalink
Merge pull request #105 from aqjune-aws/module1
Browse files Browse the repository at this point in the history 
Enable using pa_j as a standalone camlp5r preprocessor
  • Loading branch information
@jrh13
jrh13 committed Aug 6, 2024
2 parents 321103a + 7b2d535 commit 7f7808d
Show file tree
Hide file tree
Showing 11 changed files with 143 additions and 61 deletions.
17 changes: 13 additions & 4 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Expand Down Expand Up @@ -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;
4 changes: 1 addition & 3 deletions bignum_num.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,6 @@
(* Load in the bignum library. *)
(* ------------------------------------------------------------------------- *)

#load "nums.cma";;

include Num;;

let num = Num.num_of_int;;
Expand All @@ -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;;
26 changes: 12 additions & 14 deletions bignum_zarith.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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 =
Expand All @@ -160,4 +158,4 @@ module NumExt = struct

end;;

open NumExt;;
include NumExt;;
5 changes: 2 additions & 3 deletions hol.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
4 changes: 2 additions & 2 deletions miz3/Samples/irrat2.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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`;;
Expand Down
23 changes: 22 additions & 1 deletion pa_j/pa_j_4.xx_7.06.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
23 changes: 22 additions & 1 deletion pa_j/pa_j_4.xx_7.xx.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
25 changes: 23 additions & 2 deletions pa_j/pa_j_4.xx_8.00.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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;
Expand Down
25 changes: 23 additions & 2 deletions pa_j/pa_j_4.xx_8.02.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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;
Expand Down
25 changes: 23 additions & 2 deletions pa_j/pa_j_4.xx_8.03.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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;
Expand Down
27 changes: 0 additions & 27 deletions system.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;;

0 comments on commit 7f7808d

Please sign in to comment.