legacy/load_def_kepler.ml

   1
   2 (*
   3  * Load HOL Light and the kepler definition and inequality files.
   4  * Then use [ocaml_to_sml] to generate an SML file of the
   5  * inequality syntax.
   6  *)
   7
   8 #use "hol.ml";;
   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();;
  16
  17 let kepler_home = Sys.getenv "KEPLER_HOME";;
  18 (*
  19 let kepler_home = "/Users/seanmcl/save/versioned/projects/kepler/src";;
  20 *)
  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");;
  28
  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;;
  31
  32 let _ =
  33   Ocaml_sml.ineqs_to_sml
  34     ~file:(kepler_home ^ "/inequalities/kepler-inequality-syntax-base.sml")
  35     ~ineqs:kepler_ineqs
  36     ~univ:"Kepler";;
  37
  38 let _ =
  39   Ocaml_sml.ineqs_to_sml
  40     ~file:(kepler_home ^ "/inequalities/dodec-inequality-syntax-base.sml")
  41     ~ineqs:dodec_ineqs
  42     ~univ:"Dodec";;