Skip to content

Commit

Permalink
Replace Int constructor with num_of_int
Browse files Browse the repository at this point in the history 
This replaces the Num.Int constructor with Num.num_of_int function.
This is to prepare removing dependency on Num and using Zarith.

The script which was used for this patch is as follows (in bash, Linux):

```
set -x

replace_all () {

find . -not \( -path "./_opam" -type d -prune \) \
       -not \( -type f -wholename "./RichterHilbertAxiomGeometry/Topology.ml" \) \
       -type f -name "*.ml" -print0 | \
  xargs --no-run-if-empty -0 sed -i -e "$1"

find . -not \( -path "./_opam" -type d -prune \) \
       -type f -name "*.hl" -print0 | \
  xargs --no-run-if-empty -0 sed -i -e "$1"

}

replace_all 's/module Int /MODULE_INT_SAVED/g'

replace_all 's/ Int / Num.num_of_int /g'
replace_all 's/ Int(/ Num.num_of_int(/g'

replace_all 's/(Int /(Num.num_of_int /g'
replace_all 's/(Int(/(Num.num_of_int(/g'

replace_all 's/[Int /[Num.num_of_int /g'
replace_all 's/[Int(/[Num.num_of_int(/g'

replace_all 's/,Int /,Num.num_of_int /g'
replace_all 's/,Int(/,Num.num_of_int(/g'

replace_all 's/=Int /=Num.num_of_int /g'
replace_all 's/=Int(/=Num.num_of_int(/g'

replace_all 's/(Num.Int /(Num.num_of_int /g'
replace_all 's/(Num.Int(/(Num.num_of_int(/g'

replace_all 's/MODULE_INT_SAVED/module Int /g'
```
  • Loading branch information
@aqjune
aqjune committed Apr 3, 2024
1 parent c153f40 commit ed5a56b
Show file tree
Hide file tree
Showing 43 changed files with 433 additions and 433 deletions.
34 changes: 17 additions & 17 deletions 100/bertrand.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ let num_of_float =
let u2 = int_of_float(y2 *. p22) in
let y3 = p22 *. y2 -. float_of_int u2 in
if y3 <> 0.0 then failwith "num_of_float: inexactness!" else
(Int u0 // q22 +/ Int u1 // q44 +/ Int u2 // q66) */ pow2 n;;
(Num.num_of_int u0 // q22 +/ Num.num_of_int u1 // q44 +/ Num.num_of_int u2 // q66) */ pow2 n;;

(* ------------------------------------------------------------------------- *)
(* Integer truncated square root *)
Expand Down Expand Up @@ -126,9 +126,9 @@ let LN_N_CONV =
if ltm <> ln_tm then failwith "expected ln(ratconst)" else
let x = rat_of_term tm in
let rec dlog n y =
let y' = y +/ y // Int 8 in
let y' = y +/ y // Num.num_of_int 8 in
if y' </ x then dlog (n + 1) y' else n in
let n = dlog 0 (Int 1) in
let n = dlog 0 (Num.num_of_int 1) in
let th1 = INST [mk_small_numeral n,n_tm; tm,x_tm] pth in
let th2 = AP_TERM ltm th1 in
let th3 = PART_MATCH (lhs o rand) qth (rand(concl th2)) in
Expand Down Expand Up @@ -159,9 +159,9 @@ let LN_N2_CONV =
if ltm <> ln_tm then failwith "expected ln(ratconst)" else
let x = rat_of_term tm in
let rec dlog n y =
let y' = y */ Int 2 in
let y' = y */ Num.num_of_int 2 in
if y' </ x then dlog (n + 1) y' else n in
let n = dlog 0 (Int 1) in
let n = dlog 0 (Num.num_of_int 1) in
let th1 = INST [mk_small_numeral n,n_tm; tm,x_tm] pth in
let th2 = AP_TERM ltm th1 in
let th3 = PART_MATCH (lhs o rand) qth (rand(concl th2)) in
Expand Down Expand Up @@ -359,7 +359,7 @@ let PRIME_PRIMEPOW = prove
(* ------------------------------------------------------------------------- *)

let rec bezout (m,n) =
if m =/ Int 0 then (Int 0,Int 1) else if n =/ Int 0 then (Int 1,Int 0)
if m =/ Num.num_of_int 0 then (Num.num_of_int 0,Num.num_of_int 1) else if n =/ Num.num_of_int 0 then (Num.num_of_int 1,Num.num_of_int 0)
else if m <=/ n then
let q = quo_num n m and r = mod_num n m in
let (x,y) = bezout(m,r) in
Expand Down Expand Up @@ -412,8 +412,8 @@ let PRIMEPOW_CONV =
let ptm,tm = dest_comb tm0 in
if ptm <> primepow_tm then failwith "expected primepow(numeral)" else
let q = dest_numeral tm in
if q =/ Int 0 then pth0
else if q =/ Int 1 then pth1 else
if q =/ Num.num_of_int 0 then pth0
else if q =/ Num.num_of_int 1 then pth1 else
match factor q with
[] -> failwith "internal failure in PRIMEPOW_CONV"
| [p,k] -> let th1 = INST [mk_numeral q,q_tm;
Expand All @@ -425,7 +425,7 @@ let PRIMEPOW_CONV =
let d = q // (p */ r) in
let (x,y) = bezout(p,r) in
let p,r,x,y =
if x </ Int 0 then r,p,y,minus_num x
if x </ Num.num_of_int 0 then r,p,y,minus_num x
else p,r,x,minus_num y in
let th1 = INST [mk_numeral q,q_tm;
mk_numeral p,p_tm;
Expand All @@ -449,7 +449,7 @@ let APRIMEDIVISOR_CONV =
let ptm,tm = dest_comb tm0 in
if ptm <> aprimedivisor_tm then failwith "expected primepow(numeral)" else
let q = dest_numeral tm in
if q =/ Int 0 then failwith "APRIMEDIVISOR_CONV: not a prime power" else
if q =/ Num.num_of_int 0 then failwith "APRIMEDIVISOR_CONV: not a prime power" else
match factor q with
[p,k] -> let th1 = INST [mk_numeral q,q_tm;
mk_numeral p,p_tm;
Expand Down Expand Up @@ -1027,8 +1027,8 @@ let MANGOLDT_CONV =
let ptm,tm = dest_comb tm0 in
if ptm <> mangoldt_tm then failwith "expected mangoldt(numeral)" else
let q = dest_numeral tm in
if q =/ Int 0 then pth0
else if q =/ Int 1 then pth1 else
if q =/ Num.num_of_int 0 then pth0
else if q =/ Num.num_of_int 1 then pth1 else
match factor q with
[] -> failwith "internal failure in MANGOLDT_CONV"
| [p,k] -> let th1 = INST [mk_numeral q,q_tm;
Expand All @@ -1040,7 +1040,7 @@ let MANGOLDT_CONV =
let d = q // (p */ r) in
let (x,y) = bezout(p,r) in
let p,r,x,y =
if x </ Int 0 then r,p,y,minus_num x
if x </ Num.num_of_int 0 then r,p,y,minus_num x
else p,r,x,minus_num y in
let th1 = INST [mk_numeral q,q_tm;
mk_numeral p,p_tm;
Expand Down Expand Up @@ -1145,14 +1145,14 @@ let DOUBLE_CASES_RULE th =
let ant,cons = dest_imp bod in
let m = dest_numeral (rand ant)
and c = rat_of_term (lhand(lhand(rand cons))) in
let x = float_of_num(m +/ Int 1) in
let x = float_of_num(m +/ Num.num_of_int 1) in
let d = (4.0 *. log x +. 3.0) /. (x *. log 2.0) in
let c' = c // Int 2 +/ Int 1 +/
(floor_num(num_of_float(1024.0 *. d)) +/ Int 2) // Int 1024 in
let c' = c // Num.num_of_int 2 +/ Num.num_of_int 1 +/
(floor_num(num_of_float(1024.0 *. d)) +/ Num.num_of_int 2) // Num.num_of_int 1024 in
let c'' = max_num c c' in
let tm = mk_forall
(`n:num`,
subst [mk_numeral(Int 2 */ m),rand ant;
subst [mk_numeral(Num.num_of_int 2 */ m),rand ant;
term_of_rat c'',lhand(lhand(rand cons))] bod) in
prove(tm,
REPEAT STRIP_TAC THEN
Expand Down
10 changes: 5 additions & 5 deletions Complex/complex_grobner.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ let grob_const =
try let l,r = dest_comb tm in
if l = cx_tm then
let x = rat_of_term r in
if x =/ Int 0 then [] else [x,map (fun v -> 0) vars]
if x =/ Num.num_of_int 0 then [] else [x,map (fun v -> 0) vars]
else failwith ""
with Failure _ -> failwith "grob_const";;

Expand Down Expand Up @@ -89,7 +89,7 @@ let rec grob_add l1 l2 =
| ((c1,m1)::o1,(c2,m2)::o2) ->
if m1 = m2 then
let c = c1+/c2 and rest = grob_add o1 o2 in
if c =/ Int 0 then rest else (c,m1)::rest
if c =/ Num.num_of_int 0 then rest else (c,m1)::rest
else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
else (c2,m2)::(grob_add l1 o2);;

Expand Down Expand Up @@ -121,7 +121,7 @@ let mdiv (c1,m1) (c2,m2) =
(* Lowest common multiple of two monomials. *)
(* ------------------------------------------------------------------------- *)

let mlcm (c1,m1) (c2,m2) = (Int 1,map2 max m1 m2);;
let mlcm (c1,m1) (c2,m2) = (Num.num_of_int 1,map2 max m1 m2);;

(* ------------------------------------------------------------------------- *)
(* Reduce monomial cm by polynomial pol, returning replacement for cm. *)
Expand Down Expand Up @@ -183,7 +183,7 @@ let monic (pol,hist) =
if pol = [] then (pol,hist) else
let c',m' = hd pol in
(map (fun (c,m) -> (c//c',m)) pol,
Mmul((Int 1 // c',map (K 0) m'),hist));;
Mmul((Num.num_of_int 1 // c',map (K 0) m'),hist));;

(* ------------------------------------------------------------------------- *)
(* The most popular heuristic is to order critical pairs by LCM monomial. *)
Expand Down Expand Up @@ -344,7 +344,7 @@ let string_of_monomial vars (c,m) =
let xnstrs = map
(fun (x,n) -> x^(if n = 1 then "" else "^"^(string_of_int n))) xns in
if xns = [] then Num.string_of_num c else
let basstr = if c =/ Int 1 then "" else (Num.string_of_num c)^" * " in
let basstr = if c =/ Num.num_of_int 1 then "" else (Num.string_of_num c)^" * " in
basstr ^ end_itlist (fun s t -> s^" * "^t) xnstrs;;
let string_of_polynomial vars l =
Expand Down
2 changes: 1 addition & 1 deletion EC/excluderoots.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ needs "Library/pocklington.ml";;
let num_modinv =
let rec gcdex(m,n) =
if n </ m then let (x,y) = gcdex(n,m) in (y,x)
else if m =/ Int 0 then (Int 0,Int 1) else
else if m =/ Num.num_of_int 0 then (Num.num_of_int 0,Num.num_of_int 1) else
let q = quo_num n m in
let r = n -/ q */ m in
let (x,y) = gcdex(r,m) in (y -/ q */ x,x) in
Expand Down
26 changes: 13 additions & 13 deletions Examples/cooper.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -455,7 +455,7 @@ let is_int_const =
let mk_int_const,dest_int_const =
let ptm = `(--)` in
(fun n -> if n </ Int 0 then mk_comb(ptm,mk_num_const(minus_num n))
(fun n -> if n </ Num.num_of_int 0 then mk_comb(ptm,mk_num_const(minus_num n))
else mk_num_const n),
(fun tm -> if try rator tm = ptm with Failure _ -> false then
minus_num (dest_num_const(rand tm))
Expand Down Expand Up @@ -767,13 +767,13 @@ let LINEARIZE_CONV =
let coefficient x tm =
try let l,r = dest_add tm in
if l = x then Int 1 else
if l = x then Num.num_of_int 1 else
let c,y = dest_mul l in
if y = x then dest_int_const c else Int 0
if y = x then dest_int_const c else Num.num_of_int 0
with Failure _ -> try
let c,y = dest_mul tm in
if y = x then dest_int_const c else Int 0
with Failure _ -> Int 1;;
if y = x then dest_int_const c else Num.num_of_int 0
with Failure _ -> Num.num_of_int 1;;
(* ------------------------------------------------------------------------- *)
(* Find (always positive) LCM of all the multiples of x in formula tm. *)
Expand All @@ -787,9 +787,9 @@ let rec formlcm x tm =
lcm_num (formlcm x (lhand tm)) (formlcm x (rand tm))
else if is_forall tm || is_exists tm then
formlcm x (body(rand tm))
else if not(mem x (frees tm)) then Int 1
else if not(mem x (frees tm)) then Num.num_of_int 1
else let c = coefficient x (rand tm) in
if c =/ Int 0 then Int 1 else c;;
if c =/ Num.num_of_int 0 then Num.num_of_int 1 else c;;
(* ------------------------------------------------------------------------- *)
(* Switch from "x [+ ...]" to "&1 * x [+ ...]" to suit later proforma. *)
Expand Down Expand Up @@ -853,16 +853,16 @@ let ADJUSTCOEFF_CONV =
let lop,t = dest_comb tm in
let op,z = dest_comb lop in
let c = coefficient (hd vars) t in
if c =/ Int 0 then REFL tm else
if c =/ Num.num_of_int 0 then REFL tm else
let th1 =
if c =/ l then REFL tm else
let m = l // c in
let th0 = if op = op_eq then pth_eq
else if op = op_divides then pth_divides
else if op = op_lt then
if m >/ Int 0 then pth_lt_pos else pth_lt_neg
if m >/ Num.num_of_int 0 then pth_lt_pos else pth_lt_neg
else if op = op_gt then
if m >/ Int 0 then pth_gt_pos else pth_gt_neg
if m >/ Num.num_of_int 0 then pth_gt_pos else pth_gt_neg
else failwith "ADJUSTCOEFF_CONV: unknown predicate" in
let th1 = INST [mk_int_const m,d_tm; z,c_tm; t,e_tm] th0 in
let tm1 = lhand(concl th1) in
Expand All @@ -881,7 +881,7 @@ let ADJUSTCOEFF_CONV =
else
let tm2 = rator(rand(concl th3)) in
TRANS th3 (AP_TERM tm2 (LINEAR_CMUL vars m t)) in
if l =/ Int 1 then
if l =/ Num.num_of_int 1 then
CONV_RULE(funpow 2 RAND_CONV (MULTIPLY_1_CONV vars)) th1
else th1 in
ADJUSTCOEFF_CONV;;
Expand All @@ -899,7 +899,7 @@ let NORMALIZE_COEFF_CONV =
let x,bod = dest_exists tm in
let l = formlcm x tm in
let th1 = ADJUSTCOEFF_CONV (x::vars) l tm in
let th2 = if l =/ Int 1 then EXISTS_MULTIPLE_THM_1
let th2 = if l =/ Num.num_of_int 1 then EXISTS_MULTIPLE_THM_1
else INST [mk_int_const l,c_tm] pth in
TRANS th1 (REWR_CONV th2 (rand(concl th1))) in
NORMALIZE_COEFF_CONV;;
Expand Down Expand Up @@ -963,7 +963,7 @@ let dplcm =
if hop = divides_tm || hop = ndivides_tm then dest_int_const (hd args)
else if hop = and_tm || hop = or_tm
then end_itlist lcm_num (map dplcm args)
else Int 1 in
else Num.num_of_int 1 in
dplcm;;
(* ------------------------------------------------------------------------- *)
Expand Down
8 changes: 4 additions & 4 deletions Examples/lucas_lehmer.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -324,14 +324,14 @@ let LUCAS_LEHMER_RULE =
(INST [mk_small_numeral p,p_tm] pth_base)
and th_step = CONV_RULE(RAND_CONV(LAND_CONV NUM_REDUCE_CONV))
(INST [mk_small_numeral p,p_tm] pth_step)
and pp1 = pow2 p -/ Int 1 in
and pp1 = pow2 p -/ Num.num_of_int 1 in
let rec lucas_lehmer k =
if k = 0 then th_base,dest_numeral(rand(concl th_base)) else
let th1,mval = lucas_lehmer (k - 1) in
let gofer() =
let mtm = rand(concl th1) in
let yval = power_num mval (Int 2) in
let qval = quo_num yval pp1 and rval = mod_num yval pp1 -/ Int 2 in
let yval = power_num mval (Num.num_of_int 2) in
let qval = quo_num yval pp1 and rval = mod_num yval pp1 -/ Num.num_of_int 2 in
let th3 = INST [mk_small_numeral(k - 1),n_tm; mtm,m_tm;
mk_numeral qval,q_tm; mk_numeral rval,r_tm] th_step in
let th4 = MP th3 th1 in
Expand All @@ -344,7 +344,7 @@ let LUCAS_LEHMER_RULE =
time gofer())
else gofer() in
let th1,y = lucas_lehmer (p - 2) in
if y <>/ Int 0 then failwith "LUCAS_LEHMER_RULE: not a prime" else
if y <>/ Num.num_of_int 0 then failwith "LUCAS_LEHMER_RULE: not a prime" else
let th2 = SPEC(mk_small_numeral p) LUCAS_LEHMER in
let th3 = CONV_RULE
(LAND_CONV(RAND_CONV(LAND_CONV
Expand Down
46 changes: 23 additions & 23 deletions Examples/machin.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -478,21 +478,21 @@ let mclaurin_atn_rule,MCLAURIN_ATN_RULE =
let pth = SPECL [x_tm; n_tm; k_tm] MCLAURIN_ATN_APPROX
and CLEAN_RULE = REWRITE_RULE[real_pow]
and MATCH_REAL_LE_TRANS = MATCH_MP REAL_LE_TRANS
and num_0 = Int 0
and num_1 = Int 1 in
and num_0 = Num.num_of_int 0
and num_1 = Num.num_of_int 1 in
let mclaurin_atn_rule k0 p0 =
if k0 = 0 then failwith "mclaurin_atn_rule: must have |x| <= 1/2" else
let k = Int k0
and p = Int p0 in
let k = Num.num_of_int k0
and p = Num.num_of_int p0 in
let n = Num.int_of_num(ceiling_num ((p +/ k) // k)) in
let ns = if n mod 2 = 0 then 0--(n - 1) else 0--(n - 2) in
map (fun m -> if m mod 2 = 0 then num_0 else
(if (m - 1) mod 4 = 0 then I else minus_num)
(num_1 // Int m)) ns
(num_1 // Num.num_of_int m)) ns
and MCLAURIN_ATN_RULE k0 p0 =
if k0 = 0 then failwith "MCLAURIN_ATN_RULE: must have |x| <= 1/2" else
let k = Int k0
and p = Int p0 in
let k = Num.num_of_int k0
and p = Num.num_of_int p0 in
let n = ceiling_num ((p +/ k) // k) in
let th1 = INST [mk_numeral k,k_tm; mk_numeral n,n_tm] pth in
let th2 = ASSUME (lhand(lhand(concl th1)))
Expand Down Expand Up @@ -684,9 +684,9 @@ let rec POLY l x =
let atn_approx_conv,ATN_APPROX_CONV =
let atn_tm = `atn`
and num_0 = Int 0
and num_1 = Int 1
and num_2 = Int 2 in
and num_0 = Num.num_of_int 0
and num_1 = Num.num_of_int 1
and num_2 = Num.num_of_int 2 in
let rec log_2 x = if x <=/ num_1 then log_2 (num_2 */ x) -/ num_1
else if x >/ num_2 then log_2 (x // num_2) +/ num_1
else num_1 in
Expand Down Expand Up @@ -718,12 +718,12 @@ let atn_approx_conv,ATN_APPROX_CONV =
(* ------------------------------------------------------------------------- *)
let pi_approx_rule,PI_APPROX_RULE =
let const_1_8 = Int 1 // Int 8
and const_1_57 = Int 1 // Int 57
and const_1_239 = Int 1 // Int 239
and const_24 = Int 24
and const_8 = Int 8
and const_4 = Int 4
let const_1_8 = Num.num_of_int 1 // Num.num_of_int 8
and const_1_57 = Num.num_of_int 1 // Num.num_of_int 57
and const_1_239 = Num.num_of_int 1 // Num.num_of_int 239
and const_24 = Num.num_of_int 24
and const_8 = Num.num_of_int 8
and const_4 = Num.num_of_int 4
and tm_1_8 = `atn(&1 / &8)`
and tm_1_57 = `atn(&1 / &57)`
and tm_1_239 = `atn(&1 / &239)`
Expand Down Expand Up @@ -802,14 +802,14 @@ let pi_approx_binary_rule,PI_APPROX_BINARY_RULE =
ARITH_RULE `SUC p - p = 1`; SUB_REFL] THEN
UNDISCH_TAC `abs (&2 pow p * r - a) <= inv (&2)` THEN
CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV)
and num_2 = Int 2 in
and num_2 = Num.num_of_int 2 in
let pi_approx_binary_rule p =
let ppow = power_num num_2 (Int p) in
let ppow = power_num num_2 (Num.num_of_int p) in
let r = pi_approx_rule (p + 1) in
let a = round_num (ppow */ r) in
a // ppow
and PI_APPROX_BINARY_RULE p =
let ppow = power_num num_2 (Int p) in
let ppow = power_num num_2 (Num.num_of_int p) in
let th1 = PI_APPROX_RULE (p + 1) in
let th2 = CONV_RULE(funpow 3 RAND_CONV num_CONV) th1 in
let r = rat_of_term(rand(rand(lhand(concl th2)))) in
Expand All @@ -823,10 +823,10 @@ let pi_approx_binary_rule,PI_APPROX_BINARY_RULE =
(* ------------------------------------------------------------------------- *)
let ATN_EXPAND_CONV =
let num_0 = Int 0
and num_1 = Int 1
and num_2 = Int 2
and eighth = Int 1 // Int 8
let num_0 = Num.num_of_int 0
and num_1 = Num.num_of_int 1
and num_2 = Num.num_of_int 2
and eighth = Num.num_of_int 1 // Num.num_of_int 8
and atn_tm = `atn`
and eighth_tm = `&1 / &8`
and mk_mul = mk_binop `(*)`
Expand Down
Loading

0 comments on commit ed5a56b

Please sign in to comment.