(* -------------------------------------------------------------------------- *)
(* Signature *)
(* -------------------------------------------------------------------------- *)
module type Ocaml_sml =
sig
type const_name = | Dodec_slope
| Dd_31
| Dd_32
| Dd_33
| Dd_41
| Dd_42
| Dd_51
| Doct
| Dodec_trunc
| Pi
| Ppa1
| Ppa2
| Ppd0
| Ppm
| Ppb
| Ppa
| Ppbc
| Ppc
| Ppd
| Ppsolt0
| Pt
| Ss_5
| Sqrt2
| Sqrt8
| Square_2t0
| Sqrt_2t0
| Square_4t0
| Tt_0
| Tt_5
| Two_dodec_trunc
| Two_dodec_trunc_sq
| Two_t0
| Xi_gamma
| Xi'_gamma
| Xiv
| Zz_32
| Zz_33
| Zz_41
| Zz_42
type func_name = | Anc
| Arclength
| Beta
| Chi_x
| Cross_diag_x
| Crown
| Delta_x
| Dih_x
| Dih2_x
| Dih3_x
| Dihr
| Eta_x
| Gamma_x
| Kappa
| Kx
| Mu_flat_x
| Mu_flipped_x
| Mu_upright_x
| Nu_gamma_x
| Nu_x
| Octa_x
| Octavor0_x
| Octavor_analytic_x
| Omega_x
| Overlap_f
| Quo_x
| Rad2_x
| Sigma1_qrtet_x
| Sigma32_qrtet_x
| Sigma_qrtet_x
| Sigmahat_x
| Sol_x
| Squander_x
| Taua_x
| Tauc0_x
| Tauvt_x
| Tau_0_x
| Tau_analytic_x
| Tau_sigma_x
| Tauhat_x
| Tauhatpi_x
| Taumu_flat_x
| Taunu_x
| Truncated_volume_x
| U_x
| V0x
| V1x
| Volume_x
| Vora_x
| Vorc0_x
| Vorc_x
| Vor_0_x
| Vor_0_x_flipped
| Vor_analytic_x
| Vor_analytic_x_flipped
| Vort_x
type const = | Decimal of int * int
| Int of int
| Named of const_name
| Sqr of const
| Sqrt of const
| Cos of const
| Acos of const
| Copp of const
| Cplus of const * const
| Cmul of const * const
| Cdiv of const * const
type expr = | Const of const
| Funcall of func_name * expr list
| Var of string
| Varsqrt of string
| Opp of expr
| Mul of expr * expr
| Div of expr * expr
| Pow of expr * int
| One
type monom = const * expr
type lcomb = monom list
type bounds = {lo : const;
hi : const}
type ineq = {name : string;
vars : (string * bounds) list;
rels : lcomb list}
(*
put the hales inequalities in a normal form
!x_1 ... x_n. ineq [lower_1,x_1,upper_1;
...;
lower_n,x_n,upper_n]
c_1_1 f_1 + ... + c_1_m f_m < &0 \/
... \/
c_k_1 f_k + ... + c_k_m f_m < &0
*)
val normalize : Term.term -> Term.term
(* Translate HOL Light term to OCaml datatype *)
val translate : string * Term.term -> ineq
val translate_list : ignore : string list ->
terms : (string * Term.term) list -> ineq list
(* Print Ocaml datatype as an SML datatype *)
val ineq_to_sml : ineq -> unit
val ineqs_to_sml : file:string -> ineqs:ineq list -> unit
end
(* -------------------------------------------------------------------------- *)
(* Structure *)
(* -------------------------------------------------------------------------- *)
module Ocaml_sml (* : Ocaml_sml *) =
struct
type const_name = | Dodec_slope
| Dd_31
| Dd_32
| Dd_33
| Dd_41
| Dd_42
| Dd_51
| Doct
| Dodec_trunc
| Pi
| Ppa1
| Ppa2
| Ppd0
| Ppm
| Ppb
| Ppa
| Ppbc
| Ppc
| Ppd
| Ppsolt0
| Pt
| Ss_5
| Sqrt2
| Sqrt8
| Square_2t0
| Sqrt_2t0
| Square_4t0
| Tt_0
| Tt_5
| Two_dodec_trunc
| Two_dodec_trunc_sq
| Two_t0
| Xi_gamma
| Xi'_gamma
| Xiv
| Zz_32
| Zz_33
| Zz_41
| Zz_42
type func_name = | Anc
| Arclength
| Beta
| Chi_x
| Cross_diag_x
| Crown
| Delta_x
| Dih_x
| Dih2_x
| Dih3_x
| Dihr
| Eta_x
| Gamma_x
| Kappa
| Kx
| Mu_flat_x
| Mu_flipped_x
| Mu_upright_x
| Nu_gamma_x
| Nu_x
| Octa_x
| Octavor0_x
| Octavor_analytic_x
| Omega_x
| Overlap_f
| Quo_x
| Rad2_x
| Sigma1_qrtet_x
| Sigma32_qrtet_x
| Sigma_qrtet_x
| Sigmahat_x
| Sol_x
| Squander_x
| Taua_x
| Tauc0_x
| Tauvt_x
| Tau_0_x
| Tau_analytic_x
| Tau_sigma_x
| Tauhat_x
| Tauhatpi_x
| Taumu_flat_x
| Taunu_x
| Truncated_volume_x
| U_x
| V0x
| V1x
| Volume_x
| Vora_x
| Vorc0_x
| Vorc_x
| Vor_0_x
| Vor_0_x_flipped
| Vor_analytic_x
| Vor_analytic_x_flipped
| Vort_x
type const = | Decimal of int * int
| Int of int
| Named of const_name
| Sqr of const
| Sqrt of const
| Cos of const
| Acos of const
| Copp of const
| Cplus of const * const
| Cmul of const * const
| Cdiv of const * const
type expr = | Const of const
| Funcall of func_name * expr list
| Var of string
| Varsqrt of string
| Opp of expr
| Mul of expr * expr
| Div of expr * expr
| Pow of expr * int
| One
type monom = const * expr
type lcomb = monom list
type bounds = {lo : const;
hi : const}
type ineq = {name : string;
vars : (string * bounds) list;
rels : lcomb list}
(* -------------------------------------------------------------------------- *)
(* Util *)
(* -------------------------------------------------------------------------- *)
(* remove "kepler'" from the front of a name *)
let unkepler s =
try
let kep = String.sub s 0 7 in
if kep = "kepler'" then String.sub s 7 (String.length s - 7)
else s
with Invalid_argument _ -> s
let const_of_string const = match const with
| "D31" -> Dd_31
| "D32" -> Dd_32
| "D33" -> Dd_33
| "D41" -> Dd_41
| "D42" -> Dd_42
| "D51" -> Dd_51
| "dodecSlope" -> Dodec_slope
| "dodecTrunc" -> Dodec_trunc
| "Z32" -> Zz_32
| "Z33" -> Zz_33
| "Z41" -> Zz_41
| "Z42" -> Zz_42
| "doct" -> Doct
| "pi" -> Pi
| "pp_a1" -> Ppa1
| "pp_a2" -> Ppa2
| "pp_d0" -> Ppd0
| "pp_m" -> Ppm
| "pp_b" -> Ppb
| "pp_a" -> Ppa
| "pp_bc" -> Ppbc
| "pp_c" -> Ppc
| "pp_d" -> Ppd
| "pp_solt0" -> Ppsolt0
| "pt" -> Pt
| "s5" -> Ss_5
| "sqrt2" -> Sqrt2
| "sqrt8" -> Sqrt8
| "sqrt_2t0" -> Sqrt_2t0
| "square_2t0" -> Square_2t0
| "square_4t0" -> Square_4t0
| "t0" -> Tt_0
| "t5" -> Tt_5
| "two_t0" -> Two_t0
| "twoDodecTrunc" -> Two_dodec_trunc
| "twoDodecTruncSq" -> Two_dodec_trunc_sq
| "xi_gamma" -> Xi_gamma
| "xi'_gamma" -> Xi'_gamma
| "xiV" -> Xiv
| _ -> failwith ("not a constant: " ^ const)
let const_of_string = const_of_string o unkepler
let const_to_string const = match const with
| Dd_31 -> "D31"
| Dd_32 -> "D32"
| Dd_33 -> "D33"
| Dd_41 -> "D41"
| Dd_42 -> "D42"
| Dd_51 -> "D51"
| Dodec_slope -> "DodecSlope"
| Dodec_trunc -> "DodecTrunc"
| Zz_32 -> "Z32"
| Zz_33 -> "Z33"
| Zz_41 -> "Z41"
| Zz_42 -> "Z42"
| Doct -> "Doct"
| Pi -> "Pi"
| Ppa1 -> "Ppa1"
| Ppa2 -> "Ppa2"
| Ppd0 -> "Ppd0"
| Ppm -> "Ppm"
| Ppb -> "Ppb"
| Ppa -> "Ppa"
| Ppbc -> "Ppbc"
| Ppc -> "Ppc"
| Ppd -> "Ppd"
| Ppsolt0 -> "Ppsolt0"
| Pt -> "Pt"
| Ss_5 -> "S5"
| Sqrt2 -> "Sqrt2"
| Sqrt8 -> "Sqrt8"
| Sqrt_2t0 -> "Sqrt2t0"
| Square_2t0 -> "Square2t0"
| Square_4t0 -> "Square4t0"
| Tt_0 -> "T0"
| Tt_5 -> "T5"
| Two_dodec_trunc -> "TwoDodecTrunc"
| Two_dodec_trunc_sq -> "TwoDodecTruncSq"
| Two_t0 -> "TwoT0"
| Xi_gamma -> "XiGamma"
| Xi'_gamma -> "Xi'Gamma"
| XiV -> "XiV"
let func_of_string func = match func with
| "anc" -> Anc
| "arclength" -> Arclength
| "beta" -> Beta
| "chi_x" -> Chi_x
| "cross_diag_x" -> Cross_diag_x
| "crown" -> Crown
| "delta_x" -> Delta_x
| "dih2_x" -> Dih2_x
| "dih3_x" -> Dih3_x
| "dihR" -> Dihr
| "dih_x" -> Dih_x
| "eta_x" -> Eta_x
| "gamma_x" -> Gamma_x
| "kappa" -> Kappa
| "KX" -> Kx
| "mu_flat_x" -> Mu_flat_x
| "mu_flipped_x" -> Mu_flipped_x
| "mu_upright_x" -> Mu_upright_x
| "nu_gamma_x" -> Nu_gamma_x
| "nu_x" -> Nu_x
| "octa_x" -> Octa_x
| "octavor0_x" -> Octavor0_x
| "octavor_analytic_x" -> Octavor_analytic_x
| "omega_x" -> Omega_x
| "overlap_f" -> Overlap_f
| "quo_x" -> Quo_x
| "rad2_x" -> Rad2_x
| "sigma1_qrtet_x" -> Sigma1_qrtet_x
| "sigma32_qrtet_x" -> Sigma32_qrtet_x
| "sigma_qrtet_x" -> Sigma_qrtet_x
| "sigmahat_x" -> Sigmahat_x
| "sol_x" -> Sol_x
| "squander_x" -> Squander_x
| "tauA_x" -> Taua_x
| "tauC0_x" -> Tauc0_x
| "tauVt_x" -> Tauvt_x
| "tau_0_x" -> Tau_0_x
| "tau_analytic_x" -> Tau_analytic_x
| "tau_sigma_x" -> Tau_sigma_x
| "tauhat_x" -> Tauhat_x
| "tauhatpi_x" -> Tauhatpi_x
| "taumu_flat_x" -> Taumu_flat_x
| "taunu_x" -> Taunu_x
| "truncated_volume_x" -> Truncated_volume_x
| "u_x" -> U_x
| "v0x" -> V0x
| "v1x" -> V1x
| "volume_x" -> Volume_x
| "vorA_x" -> Vora_x
| "vorC0_x" -> Vorc0_x
| "vorC_x" -> Vorc_x
| "vor_0_x" -> Vor_0_x
| "vor_0_x_flipped" -> Vor_0_x_flipped
| "vor_analytic_x" -> Vor_analytic_x
| "vor_analytic_x_flipped" -> Vor_analytic_x_flipped
| "vort_x" -> Vort_x
| _ -> failwith ("no such const: " ^ func)
let func_of_string = func_of_string o unkepler
let func_to_string func = match func with
| Anc -> "Anc"
| Arclength -> "Arclength"
| Beta -> "Beta"
| Chi_x -> "ChiX"
| Cross_diag_x -> "CrossDiagX"
| Crown -> "Crown"
| Delta_x -> "DeltaX"
| Dih2_x -> "Dih2X"
| Dih3_x -> "Dih3X"
| Dihr -> "Dihr"
| Dih_x -> "DihX"
| Eta_x -> "EtaX"
| Gamma_x -> "GammaX"
| Kappa -> "Kappa"
| Kx -> "Kx"
| Mu_flat_x -> "MuFlatX"
| Mu_flipped_x -> "MuFlippedX"
| Mu_upright_x -> "MuUprightX"
| Nu_gamma_x -> "NuGammaX"
| Nu_x -> "NuX"
| Octa_x -> "OctaX"
| Octavor0_x -> "Octavor0X"
| Octavor_analytic_x -> "OctavorAnalyticX"
| Omega_x -> "OmegaX"
| Overlap_f -> "OverlapF"
| Quo_x -> "QuoX"
| Rad2_x -> "Rad2X"
| Sigma1_qrtet_x -> "Sigma1QrtetX"
| Sigma32_qrtet_x -> "Sigma32QrtetX"
| Sigma_qrtet_x -> "SigmaQrtetX"
| Sigmahat_x -> "SigmahatX"
| Sol_x -> "SolX"
| Squander_x -> "SquanderX"
| Taua_x -> "TauaX"
| Tauc0_x -> "Tauc0X"
| Tauvt_x -> "TauvtX"
| Tau_0_x -> "Tau0X"
| Tau_analytic_x -> "TauAnalyticX"
| Tau_sigma_x -> "TauSigmaX"
| Tauhat_x -> "TauhatX"
| Tauhatpi_x -> "TauhatpiX"
| Taumu_flat_x -> "TaumuFlatX"
| Taunu_x -> "TaunuX"
| Truncated_volume_x -> "TruncatedVolumeX"
| U_x -> "UX"
| V0x -> "V0x"
| V1x -> "V1x"
| Volume_x -> "VolumeX"
| Vora_x -> "VoraX"
| Vorc0_x -> "Vorc0X"
| Vorc_x -> "VorcX"
| Vor_0_x -> "Vor0X"
| Vor_0_x_flipped -> "Vor0XFlipped"
| Vor_analytic_x -> "VorAnalyticX"
| Vor_analytic_x_flipped -> "VorAnalyticXFlipped"
| Vort_x -> "VortX"
let var_to_string v = fst (dest_var v)
let dest_add t = try Some (dest_binop `(+.)` t) with _ -> None
let dest_sub t = try Some (dest_binop `(-.)` t) with _ -> None
let dest_mul t = try Some (dest_binop `( *. )` t) with _ -> None
let dest_div t = try Some (dest_binop `( / )` t) with _ -> None
(* -------------------------------------------------------------------------- *)
(* Translation *)
(* -------------------------------------------------------------------------- *)
(* `#1.35` *)
let translate_decimal t : const option =
try
let dec,numden = strip_comb t in
let num,den = match numden with [num;den] -> num,den | _ -> failwith "" in
if dec = `DECIMAL` then
match dest_numeral num,dest_numeral den with
Num.Int num', Num.Int den' -> Some (Decimal (num',den'))
| _ -> failwith ""
else None
with _ -> None
(* `&5` *)
let translate_rint t : const option =
try
let amp,n = dest_comb t in
if amp = `&.` then
match dest_numeral n with
Num.Int n' -> Some (Int n')
| _ -> None
else None
with _ -> None
(* `5` *)
let translate_int t : int option =
try
match dest_numeral t with
Num.Int n' -> Some n'
| _ -> None
with _ -> None
(* `square_2t0` *)
let translate_named t : const option =
try
let c,_ = dest_const t in
Some (Named (const_of_string c))
with _ -> None
let rec translate_const t : const option =
match translate_decimal t with
Some _ as c -> c
| None ->
match translate_rint t with
Some _ as c -> c
| None ->
match translate_named t with
Some _ as c -> c
| None ->
match translate_cos t with
Some _ as c -> c
| None ->
match translate_acos t with
Some _ as c -> c
| None ->
match translate_sqr t with
Some _ as c -> c
| None ->
match translate_sqrt t with
Some _ as c -> c
| None ->
match translate_copp t with
Some _ as c -> c
| None ->
match translate_cplus t with
Some _ as c -> c
| None ->
match translate_cmul t with
Some _ as c -> c
| None ->
match translate_cdiv t with
Some _ as c -> c
| None -> None
and translate_unop p con t : const option =
try
let p',c = dest_comb t in
if p = p' then
match translate_const c with
Some c -> Some (con c)
| None -> None
else
None
with _ -> None
and translate_binop p con t : const option =
try
let l,r = dest_binop p t in
match translate_const l,translate_const r with
Some l', Some r' -> Some (con(l',r'))
| _ -> None
with _ -> None
and translate_cos t = translate_unop `cos` (fun x -> Cos x) t
and translate_acos t = translate_unop `acs` (fun x -> Acos x) t
and translate_sqr t = translate_unop `square` (fun x -> Sqr x) t
and translate_sqrt t = translate_unop `sqrt` (fun x -> Sqrt x) t
and translate_copp t = translate_unop `(--.)` (fun x -> Copp x) t
and translate_cplus t = translate_binop `(+.)` (fun x,y -> Cplus (x,y)) t
and translate_cmul t = translate_binop `( *. )` (fun x,y -> Cmul (x,y)) t
and translate_cdiv t = translate_binop `( / )` (fun x,y -> Cdiv (x,y)) t
let translate_var t =
if is_var t then Some (Var (fst (dest_var t))) else None
let translate_varsqrt t =
try
let sqrt,x = dest_comb t in
if sqrt = `sqrt` && is_var x then
Some (Varsqrt (fst (dest_var x)))
else None
with _ -> None
let rec translate_expr t : expr option =
match translate_const t with
Some c -> Some (Const c)
| None ->
match translate_funcall t with
Some _ as c -> c
| None ->
match translate_varsqrt t with
Some _ as c -> c
| None ->
match translate_var t with
Some _ as c -> c
| None ->
match translate_opp t with
Some _ as c -> c
| None ->
match translate_mul t with
Some _ as c -> c
| None ->
match translate_div t with
Some _ as c -> c
| None ->
match translate_pow t with
Some _ as c -> c
| None -> failwith "translate_expr"
and translate_funcall t =
try
let f,xs = strip_comb t in
let func_str,_ = dest_const f in
let func = func_of_string func_str in
let xs' = map (fun x -> match translate_expr x with Some e -> e | None -> failwith "") xs in
Some (Funcall(func,xs'))
with _ -> None
and translate_unop p con t : expr option =
try
let p',c = dest_comb t in
if p = p' then
match translate_expr c with
Some c -> Some (con c)
| None -> None
else
None
with _ -> None
and translate_binop p con t : expr option =
try
let l,r = dest_binop p t in
match translate_expr l,translate_expr r with
Some l', Some r' -> Some (con(l',r'))
| _ -> None
with _ -> None
and translate_opp t = translate_unop `(--.)` (fun x -> Opp x) t
and translate_mul t = translate_binop `( *. )` (fun x,y -> Mul (x,y)) t
and translate_div t = translate_binop `( / )` (fun x,y -> Div (x,y)) t
and translate_pow t =
try
let f,[x;n] = strip_comb t in
if not(f = `((pow):real->num->real)`) then None else
let Some x' = translate_expr x in
let Some n' = translate_int n in
Some (Pow(x',n'))
with _ -> None
let translate_monom t : monom option =
match translate_const t with
Some x -> Some (x,One)
| None ->
match dest_mul t with
Some (c,e) ->
(match translate_const c, translate_expr e with
Some c', Some e' -> Some (c',e')
| _ -> match translate_expr t with
Some e -> Some (Int 1,e)
| None -> None)
| None ->
match translate_expr t with
Some e -> Some (Int 1,e)
| None -> None;;
let rec translate_lcomb t =
match dest_add t with
Some (l,r) ->
(match translate_lcomb l ,translate_lcomb r with
Some l', Some r' -> Some (l' @ r')
| _ -> None)
| None ->
match translate_monom t with
Some m -> Some [m]
| None -> None
let translate_rel t =
try
let lcomb,zero = dest_binop `(<.)` t in
let _ = if zero <> `(&0)` then failwith "not zero" else () in
translate_lcomb lcomb
with _ -> failwith "translate_rel"
let translate_ineq t =
try
let _,body = strip_forall t in
let ineq_tm,bounds_rel = strip_comb body in
let bounds,rel = match bounds_rel with [bounds;rel] -> bounds,rel | _ -> failwith "" in
let ineqs = disjuncts rel in
let map_fn q = match translate_rel q with Some l -> l | None -> failwith "" in
let ineqs = map map_fn ineqs in
let dest_trip xyz =
let x,yz = dest_pair xyz in
let x = match translate_const x with Some x -> x | None -> failwith "" in
let y,z = dest_pair yz in
let y,_ = dest_var y in
let z = match translate_const z with Some x -> x | None -> failwith "" in
y,{lo = x; hi = z} in
let bounds' = map dest_trip (dest_list bounds) in
(bounds',ineqs)
with _ -> failwith "translate_ineq"
(* -------------------------------------------------------------------------- *)
(* Normalize *)
(* -------------------------------------------------------------------------- *)
let normalize =
let thms = [
REAL_ARITH `x *. (y + z) = x * y + x * z`;
REAL_ARITH `(x +. y) * z = z * x + z * y`;
REAL_ARITH `&0 *. x = &0`;
REAL_ARITH `x * -- y = -- x * y`;
REAL_ARITH `(x -. y) = x + (-- y)`;
REAL_ARITH `(x +. y) + z = x + y + z`;
REAL_ARITH `--. (x * y) = (--. x) * y`;
REAL_ARITH `-- #0.0 = &0`;
REAL_ARITH `-- &0 = &0`;
REAL_ARITH `x + &0 = x`;
REAL_ARITH `&0 + x = x`;
REAL_ARITH `--. (x + y) = (--. x) + (-- y)`;
REAL_ARITH `--. (-- x) = x`;
REAL_ARITH `!f:real->real->real->real->real->real->real. (-- (f x1 x2 x3 x4 x5 x6)) = (-- (&1) *. (f x1 x2 x3 x4 x5 x6))`;
MESON [] `(a \/ (b \/ c)) = (a \/ b \/ c)`;
pi_prime_tau;
pi_prime_sigma;
LET_DEF;
LET_END_DEF;
] in
let once_thms = [
REAL_ARITH `!x y z:real. (x < y) = x - y < &0`;
REAL_ARITH `!x y z:real. (x > y) = y - x < &0`;
] in
fun x ->
snd (dest_eq (concl (
(DEPTH_CONV BETA_CONV THENC
ONCE_REWRITE_CONV once_thms THENC
REWRITE_CONV thms THENC
NUM_REDUCE_CONV) x)))
let translate (name,q) =
let _ = print_endline ("translating ineq: " ^ name) in
let bounds,rels = translate_ineq (normalize q) in
{name = name;
vars = bounds;
rels = rels}
let translate_list ~ignore ~terms =
map translate (List.filter (fun x,_ -> not (mem x ignore)) terms)
(* -------------------------------------------------------------------------- *)
(* Pretty Printing *)
(* -------------------------------------------------------------------------- *)
open Format
let pp_int n =
begin
open_hbox ();
print_string (string_of_int n);
close_box ();
end
let pp_pair f (l,r) =
begin
open_hbox();
print_string "(";f l;print_string ",";f r;print_string ")";
close_box();
end
let separate =
let rec separate x l str = match l with
| [] -> List.rev str
| [h] -> List.rev (h::str)
| h::h'::t -> separate x (h'::t) (x::h::str) in
fun x l -> separate x l []
let rec iter_butlast f l = match l with
| [] | [_] -> ()
| h::t -> (f h;iter_butlast f t)
let rec last l = match l with
| [] -> failwith ""
| [h] -> h
| _::t -> last t
let pp_list_horiz f l = if l = [] then print_string "[]" else
begin
open_hbox();
print_string "[";
iter_butlast (fun x -> (f x; print_string ", ")) l;
f (last l);
print_string "]";
close_box();
end
let pp_list_vert f l = if l = [] then print_string "[]" else
begin
open_vbox 1;
print_string "[";
iter_butlast (fun x -> (f x; print_string ",";print_cut())) l;
f (last l);
print_string "]";
close_box();
end
let pp_unop p s c =
begin
open_hbox();
print_string s;
print_string "(";
p c;
print_string ")";
close_box();
end
let pp_binop p1 p2 s c1 c2 =
begin
open_hbox();
print_string s;
print_string "(";
p1 c1;
print_string ",";
p2 c2;
print_string ")";
close_box();
end
let pp_decimal (x,y) =
begin
open_hbox();
print_string "Decimal";
pp_pair pp_int (x,y);
close_box();
end
let pp_named n = print_string (const_to_string n)
let rec pp_const c = match c with
| Decimal (x,y) -> pp_decimal(x,y)
| Int n -> (print_string "Int "; pp_int n)
| Named n -> (print_string "Named ";pp_named n)
| Cos c -> pp_cos c
| Acos c -> pp_acos c
| Sqr c -> pp_sqr c
| Sqrt c -> pp_sqrt c
| Copp c -> pp_copp c
| Cplus (x,y) -> pp_cplus x y
| Cmul (x,y) -> pp_cmul x y
| Cdiv (x,y) -> pp_cdiv x y
and pp_cos c = pp_unop pp_const "Cos" c
and pp_acos c = pp_unop pp_const "Acos" c
and pp_sqr c = pp_unop pp_const "Sqr" c
and pp_sqrt c = pp_unop pp_const "Sqrt" c
and pp_copp c = pp_unop pp_const "Copp" c
and pp_cplus c1 c2 = pp_binop pp_const pp_const "Cplus" c1 c2
and pp_cmul c1 c2 = pp_binop pp_const pp_const "Cmul" c1 c2
and pp_cdiv c1 c2 = pp_binop pp_const pp_const "Cdiv" c1 c2
let rec pp_expr e = match e with
| Const c -> (print_string "Const (";pp_const c;print_string ")")
| Funcall (f,xs) -> pp_funcall f xs
| Var v -> pp_var v
| Varsqrt v -> pp_varsqrt v
| Opp e -> pp_opp e
| Mul(x,y) -> pp_mul x y
| Div(x,y) -> pp_div x y
| Pow(x,n) -> pp_pow x n
| One -> print_string "One"
and pp_funcall f xs =
begin
open_hbox();
print_string "Funcall(";
print_string (func_to_string f);
print_string ", ";
pp_list_horiz pp_expr xs;
print_string ")";
close_box();
end
and pp_var v = print_string ("Var \"" ^ v ^ "\"")
and pp_varsqrt v = print_string ("Varsqrt \"" ^ v ^ "\"")
and pp_opp e = pp_unop pp_expr "Opp" e
and pp_mul e1 e2 = pp_binop pp_expr pp_expr "Mul" e1 e2
and pp_div e1 e2 = pp_binop pp_expr pp_expr "Div" e1 e2
and pp_pow e1 e2 = pp_binop pp_expr pp_int "Pow" e1 e2
let pp_monom (c,e) =
begin
open_hbox();
print_string "(";
pp_const c;
print_string ",";
pp_expr e;
print_string ")";
close_box();
end
let pp_lcomb l = pp_list_horiz pp_monom l
let pp_bounds (v, {lo=lo;hi=hi}) =
begin
open_vbox 1;
print_string ("(\"" ^ v ^ "\",");
print_cut();
open_hbox();
print_string "{lo = ";
pp_const lo;
close_box();
print_string ",";
print_cut();
open_hbox();
print_string " hi = ";
pp_const hi;
print_string "})";
close_box();
close_box();
end
let ineq_to_sml q =
begin
open_vbox 1;
print_string "{";
print_string "name = \"";
print_string q.name;
print_string "\",";
print_cut();
print_cut();
print_string "vars = ";
pp_list_vert pp_bounds q.vars;
print_string ",";
print_cut();
print_cut();
print_string "rels = ";
pp_list_vert pp_lcomb q.rels;
print_string "}";
close_box();
end
let ineqs_to_sml qs =
let doit q =
begin
ineq_to_sml q;
print_string ",";
print_cut();
print_cut();
end in
begin
open_vbox 4;
print_cut();
iter_butlast doit qs;
ineq_to_sml (last qs);
close_box();
end
let header univ =
"
(*============================================================================*)
(* THIS FILE IS AUTOGENERATED. DO NOT EDIT!!! *)
(*============================================================================*)
structure " ^ univ ^ "InequalitySyntaxBase:> INEQUALITY_SYNTAX_BASE =
struct
open FunctionUtil
open InequalityUtil
val unexpandedIneqs = [
"
let footer =
"
]
end"
let ineqs_to_sml ~file ~ineqs ~univ =
let chan = open_out file in
try
set_formatter_out_channel chan;
print_string (header univ);
ineqs_to_sml ineqs;
print_string footer;
set_formatter_out_channel stdout;
close_out chan;
with exn ->
set_formatter_out_channel stdout;
close_out chan;
raise exn
end
(*
needs "Examples/analysis.ml";;
needs "Examples/transc.ml";;
needs "Jordan/lib_ext.ml";;
needs "Jordan/parse_ext_override_interface.ml";;
unambiguous_interface();;
#use "../../kepler/sml/inequalities/holl/definitions_kepler.ml";;
#use "../../kepler/sml/inequalities/holl/kep_inequalities.ml";;
#use "../../kepler/sml/inequalities/holl/ineq_names.ml";;
#use "../../kepler/sml/inequalities/holl/ocaml_to_sml.ml";;
let ocaml_ineqs = Ocaml_sml.translate_list ~ignore:Ineq_names.ignore ~terms:Ineq_names.ineqs;;
Ocaml_sml.ineqs_to_sml
~file:"/Users/seanmcl/save/versioned/projects/kepler/sml/inequalities/inequality-syntax.sml"
~ineqs:ocaml_ineqs;;
let file = "/Users/seanmcl/save/versioned/projects/kepler/sml/inequalities/inequality-syntax.sml"
let q = List.nth ocaml_ineqs 0;;
(print_endline ""; Ocaml_sml.ineq_to_sml q; print_endline "";)
let t = Ocaml_sml.normalize x;;
Ocaml_sml.translate_ineq t
#trace Ocaml_sml.;;
#trace Ocaml_sml.normalize;;
#trace Ocaml_sml.translate_const;;
#trace Ocaml_sml.translate_cdiv;;
#trace Ocaml_sml.translate_expr;;
#trace Ocaml_sml.translate_funcall;;
#trace Ocaml_sml.translate_div;;
#trace Ocaml_sml.translate_monom;;
#trace Ocaml_sml.translate_lcomb;;
#trace Ocaml_sml.translate_rel;;
#trace Ocaml_sml.translate_ineq;;
#trace Ocaml_sml.translate_pow;;
#trace Ocaml_sml.translate;;
#untrace_all;;
let x = I_327474205_1
Ocaml_sml.translate_ineq (Ocaml_sml.normalize x)
Ocaml_sml.normalize I_327474205_1
translate_ineq I_867513567_13
let t = `tau_sigma_x x1 x2 x3 x4 x5 x6 -. #0.2529 *. dih_x x1 x2 x3 x4 x5 x6 >.
--. #0.3442`
*)