acl2/ml/sexp.sml

2 (* Various ML tools to support ACL2 in HOL including:                        *)
4 (*  1. A printer from HOL to ACL2.                                           *)
8 (*     to HOL term.                                                          *)
97 (* Error reporting function (uses some HOL boilerplate I don't understand)   *)
201 (*  3. Uses the HOL overloading mechanism to introduce "hol_name"            *)
203 (*     a valid HOL identifier name).                                         *)
282    print "\" defined with HOL name \"";
330    print "\" defined with HOL name \"";
348  (out("; File created from HOL using print_lisp_file on " ^ date() ^ "\n\n");
789 (* a negative integer to HOL representation).                                *)
939 (* Get the HOL name from ACL2 name.                                          *)
940 (* If there is no HOL name (e.g. an ACL2 variable) the ACL2 name is          *)
1162 (* Code for processing ACL2 defuns slurped into HOL via Matt's a2ml tool     *)
1197 (* corresponding HOL s-expression (sexp).                                    *)
1216 (* corresponding HOL s-expression (sexp).                                    *)
1234 (* Convert an ML s-expression (mlsexp) to the coresponding HOL               *)
1305 (* Look up the HOL name of an ACL2 name and return the corresponding         *)
1306 (* term.  Return a variable with a supplied type if there is no HOL name.    *)
1468 The method of converting a full ACL2 name pkg::sym to a HOL-friendly
1471  1. First see if the ACL2 name already has a HOL name, and if so
1474  2. Convert sym to a HOL name, say hol_sym, using the ML function
1492 HOL-friendly name as follows.
1511 (* Map from ACL2 characters in names to lists of HOL-friendly characters.    *)
1533 (* Convert a character to a list of HOL-friendly characters by applying      *)
1553 (* ACL2 to HOL name conversion function. Treats first character specially.   *)
1561 (* Create a HOL-friendly name from a full ACL2 name and remember it in       *)
1564 (* The package name is eliminated unless it's needed to disambiguate HOL     *)
1628 (* ML datatype to represent HOL tems and other data (e.g. names) of          *)
1673 (* Used for reproving ACL2 imports inside HOL and for round-trip printing.   *)
2066 (* 2. declare HOL-friendly names (declare_names) using names generated       *)
2069 (* 3. create theorems using mk_oracle_thm then save them with a HOL-friendly *)
2287   out("(* File created from HOL using print_acl2_defun_script on "