3 * Load HOL Light and the kepler definition and inequality files.
4 * Then use [ocaml_to_sml] to generate an SML file of the
9 needs "Multivariate/vectors.ml";;
10 needs "Examples/analysis.ml";;
11 needs "Examples/transc.ml";;
12 needs "definitions_kepler.ml";;
13 needs "Jordan/lib_ext.ml";;
14 needs "Jordan/parse_ext_override_interface.ml";;
15 unambiguous_interface();;
17 let kepler_home = Sys.getenv "KEPLER_HOME";;
19 let kepler_home = "/Users/seanmcl/save/versioned/projects/kepler/src";;
21 loads (kepler_home ^ "/inequalities/holl/definitions_kepler.ml");;
22 loads (kepler_home ^ "/inequalities/holl/kep_inequalities.ml");;
23 loads (kepler_home ^ "/inequalities/holl/kep_ineq_bis.ml");;
24 loads (kepler_home ^ "/inequalities/holl/kepler_ineq_names.ml");;
25 loads (kepler_home ^ "/inequalities/holl/dodec_inequalities.ml");;
26 loads (kepler_home ^ "/inequalities/holl/dodec_ineq_names.ml");;
27 loads (kepler_home ^ "/inequalities/holl/ocaml_to_sml.ml");;
29 let kepler_ineqs = Ocaml_sml.translate_list ~ignore:Kepler_ineq_names.ignore ~terms:Kepler_ineq_names.kepler_ineqs;;
30 let dodec_ineqs = Ocaml_sml.translate_list ~ignore:[] ~terms:Dodec_ineq_names.dodec_ineqs;;
33 Ocaml_sml.ineqs_to_sml
34 ~file:(kepler_home ^ "/inequalities/kepler-inequality-syntax-base.sml")
39 Ocaml_sml.ineqs_to_sml
40 ~file:(kepler_home ^ "/inequalities/dodec-inequality-syntax-base.sml")