legacy/inequalities/generate-ineq-syntax.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 "Examples/analysis.ml";;
  10 needs "Examples/transc.ml";;
  11 needs "Jordan/lib_ext.ml";;
  12 needs "Jordan/parse_ext_override_interface.ml";;
  13 unambiguous_interface();;
  14
  15 let kepler_home = Sys.getenv "KEPLER_HOME";;
  16 (*
  17 let kepler_home = "/Users/seanmcl/save/versioned/projects/kepler/src";;
  18 *)
  19 loads (kepler_home ^ "/inequalities/holl/definitions_kepler.ml");;
  20 loads (kepler_home ^ "/inequalities/holl/kep_inequalities.ml");;
  21 loads (kepler_home ^ "/inequalities/holl/kep_ineq_bis.ml");;
  22 loads (kepler_home ^ "/inequalities/holl/kepler_ineq_names.ml");;
  23 loads (kepler_home ^ "/inequalities/holl/dodec_inequalities.ml");;
  24 loads (kepler_home ^ "/inequalities/holl/dodec_ineq_names.ml");;
  25 loads (kepler_home ^ "/inequalities/holl/ocaml_to_sml.ml");;
  26
  27 let kepler_ineqs = Ocaml_sml.translate_list ~ignore:Kepler_ineq_names.ignore ~terms:Kepler_ineq_names.kepler_ineqs;;
  28 let dodec_ineqs = Ocaml_sml.translate_list ~ignore:[] ~terms:Dodec_ineq_names.dodec_ineqs;;
  29
  30 let _ =
  31   Ocaml_sml.ineqs_to_sml
  32     ~file:(kepler_home ^ "/inequalities/kepler-inequality-syntax-base.sml")
  33     ~ineqs:kepler_ineqs
  34     ~univ:"Kepler";;
  35
  36 let _ =
  37   Ocaml_sml.ineqs_to_sml
  38     ~file:(kepler_home ^ "/inequalities/dodec-inequality-syntax-base.sml")
  39     ~ineqs:dodec_ineqs
  40     ~univ:"Dodec";;