xref: /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/sexp.sml

(*****************************************************************************)
(* Various ML tools to support ACL2 in HOL including:                        *)
(*                                                                           *)
(*  1. A printer from HOL to ACL2.                                           *)
(*                                                                           *)
(*  2. A converter from the ML representation of ACL2 defuns,                *)
(*     defaxioms and defthms generated by Matt's tool a2ml.csh               *)
(*     to HOL term.                                                          *)
(*****************************************************************************)

(*****************************************************************************)
(* Ignore everything up to "END BOILERPLATE"                                 *)
(*****************************************************************************)

(*****************************************************************************)
(* START BOILERPLATE NEEDED FOR COMPILATION                                  *)
(*****************************************************************************)

(******************************************************************************
* Load theories
******************************************************************************)
(* The commented out stuff below should be loaded in interactive sessions
quietdec := true;
map
 load
 ["intSyntax","pairSyntax","listSyntax","stringLib","stringSimps",
  "rich_listTheory","pred_setLib"];
open pairSyntax listSyntax stringLib numLib stringSimps
     rich_listTheory pred_setLib Defn;
printDepth := 1000;
printLength := 1000;
Globals.checking_const_names := false;
quietdec := false;
*)

structure sexp =
struct

(******************************************************************************
* Boilerplate needed for compilation: open HOL4 systems modules
******************************************************************************)
open HolKernel Parse boolLib bossLib;

(******************************************************************************
* Open theories
******************************************************************************)
open intSyntax pairSyntax listSyntax stringLib numLib;

(*****************************************************************************)
(* END BOILERPLATE                                                           *)
(*****************************************************************************)

(*****************************************************************************)
(* Print utility from Michael Norrish (may not end up being used):           *)
(*                                                                           *)
(* > Is there a way of redirecting output from print_term to a file?         *)
(*                                                                           *)
(* You need to turn an outstream (the thing you get back from a call to      *)
(* TextIO.openOut) into a ppstream.  You could do this with                  *)
(*                                                                           *)
(*   fun mk_pp_from_out outstream =                                          *)
(*      PP.mk_ppstream { consumer = (fn s => TextIO.output(outstream,s)),    *)
(*                       linewidth = 80,                                     *)
(*                       flush = (fn () => TextIO.flushOut outstream) }      *)
(*                                                                           *)
(* where I have chosen the linewidth arbitrarily.  Then you would use the    *)
(* ppstream based pretty-printer Parse.pp_term.  So a complete solution      *)
(* for outputting a single term to a given file would be                     *)
(*****************************************************************************)
fun mk_pp_from_out outstream =
   PP.mk_ppstream { consumer = (fn s => TextIO.output(outstream,s)),
                    linewidth = 80,
                    flush = (fn () => TextIO.flushOut outstream) };

fun print_term_to_file fname term = let
  val outstr = TextIO.openOut fname
  val pps = mk_pp_from_out outstr
in
  Parse.pp_term pps term;
  PP.flush_ppstream pps;
  TextIO.closeOut outstr
end;


(*****************************************************************************)
(* Swich off warning messages when defining types and constants with         *)
(* non-standard names (e.g. names originating from ACL2).                    *)
(*****************************************************************************)
val _ = (Globals.checking_const_names := false);

(*****************************************************************************)
(* Flag to determine if HOL_ERR exceptions are printed                       *)
(*****************************************************************************)
val print_err = ref false;

(*****************************************************************************)
(* Error reporting function (uses some HOL boilerplate I don't understand)   *)
(*****************************************************************************)
fun err fn_name msg =
 if !print_err
  then Raise(mk_HOL_ERR "sexp" fn_name msg)
  else raise(mk_HOL_ERR "sexp" fn_name msg);

(*****************************************************************************)
(* Global variable holding current package name. Initially "ACL2".           *)
(*****************************************************************************)
val current_package = ref "ACL2";

(*****************************************************************************)
(* Set value of current package                                              *)
(*****************************************************************************)
fun set_current_package pname =
 (current_package := pname);

(*****************************************************************************)
(* Global updateable  list of ACL2 simplification theorems                   *)
(*****************************************************************************)
val acl2_simps = ref([]:thm list);

(*****************************************************************************)
(* Function to add a list of theorems to acl2_simps                          *)
(*****************************************************************************)
fun add_acl2_simps thl = (acl2_simps := (!acl2_simps) @ thl);

(*****************************************************************************)
(* |- ("T" = "NIL") = F  -- shouldn't need to have to prove this explicitly! *)
(*****************************************************************************)
val T_NIL = EVAL ``"T" = "NIL"``;

val _ = add_acl2_simps[T_NIL];

(*****************************************************************************)
(* Tactics that simplifies with acl2_simps and other theorems supplied       *)
(* explicitly by the user                                                    *)
(*****************************************************************************)
fun ACL2_SIMP_TAC      thl = RW_TAC        list_ss ((!acl2_simps) @ thl)
and ACL2_FULL_SIMP_TAC thl = FULL_SIMP_TAC list_ss ((!acl2_simps) @ thl);

(*****************************************************************************)
(* Global association list of pairs (hol_name, acl2_name).                   *)
(*****************************************************************************)
val acl2_names =
 ref([("ACL2_PAIR", "COMMON-LISP::CONS")]:(string*string)list);

(*****************************************************************************)
(* Test if a name is already used                                            *)
(*****************************************************************************)
fun is_acl2_name s = can (assoc s) (!acl2_names);

(*****************************************************************************)
(* Add a pair (hol_name, acl2_name) to acl2_names after checking that        *)
(* hol_name is not already used.                                             *)
(*****************************************************************************)
fun add_acl2_name (hol_name, acl2_name) =
 let val res = assoc1 hol_name (!acl2_names)
 in
  case res
  of SOME(_,acl2_name')
     => if acl2_name = acl2_name'
         then ()
         else (print "\"";
               print hol_name;
               print "\" is the name of \"";
               print acl2_name';
               print "\n\" so can't use it to name \"";
               print acl2_name; print "\"\n";
               err "add_acl2_name" "name already in use")
  |  NONE
     => (acl2_names := (hol_name, acl2_name) :: (!acl2_names))
 end;

(*****************************************************************************)
(* Function to add an entry to acl2_names                                    *)
(*****************************************************************************)
fun add_acl2_names []      = ()
 |  add_acl2_names (p::pl) = (add_acl2_name p; add_acl2_names pl);

(*****************************************************************************)
(* Print !acl2_names to a string (used in adjoin_to_theory).                 *)
(* There may be a better way of doing this!                                  *)
(*****************************************************************************)
local
fun string_pair_list_to_string_aux [] = ""
 |  string_pair_list_to_string_aux [(hol,acl2)] =
    ("(\"" ^ hol ^ "\",\"" ^ acl2 ^"\")")
 |  string_pair_list_to_string_aux ((hol,acl2)::pl) =
    ("(\"" ^ hol ^ "\",\"" ^ acl2 ^"\")," ^
    string_pair_list_to_string_aux pl)
in
fun string_pair_list_to_string pl =
 ("[" ^ string_pair_list_to_string_aux pl ^ "]")
end;

(*****************************************************************************)
(* declare_names("acl2_name","hol_name")                                     *)
(*                                                                           *)
(*  1. Checks "acl2_name" is the name of exactly one constant.               *)
(*                                                                           *)
(*  2. Checks "hol_name" isn't an existing abbreviation.                     *)
(*                                                                           *)
(*  3. Uses the HOL overloading mechanism to introduce "hol_name"            *)
(*     as an alternative name for "acl2_name" ("hol_name" should be          *)
(*     a valid HOL identifier name).                                         *)
(*****************************************************************************)
fun declare_names (acl2_name,hol_name) =
 let val hol_tml = Term.decls hol_name
     val acl2_tml = Term.decls acl2_name
 in
  if null acl2_tml
   then (print "no constant named: ";
         print acl2_name;
         print "\n";
         err "declare_names" "no term with acl2 name") else
  if not(length acl2_tml = 1)
   then (print "Warning -- there is more than one constant named: ";
         print acl2_name;
         print "\n") else
  if not(length hol_tml = 0)
   then (print "Warning -- there is already a constant named: ";
         print hol_name;
         print "\n")
   else (add_acl2_names[(hol_name,acl2_name)];
         overload_on(hol_name,hd acl2_tml))
 end;

(*****************************************************************************)
(* ``!x1 ... xn. tm`` |--> tm                                                *)
(*****************************************************************************)
val spec_all = snd o strip_forall;

(*****************************************************************************)
(* Three functions from KXS (modified by MJCG) to support non-standard names *)
(*****************************************************************************)
fun dest_hd_eqn eqs =
   let val hd_eqn = if is_conj eqs then fst(dest_conj eqs) else eqs
       val (lhs,rhs) = dest_eq (spec_all hd_eqn)
   in (strip_comb lhs, rhs)
   end;

fun non_standard_name_defn name q =
  let val absyn0 = Parse.Absyn q
      val (qtm,_) = Defn.parse_absyn absyn0
      val ((f,args),rhs) = dest_hd_eqn qtm
      val (fname,fty) = dest_var f
      val qtm' = subst [f |-> mk_var(name,fty)] qtm
  in
   (fname, Defn.mk_defn fname qtm')
  end;

fun non_standard_nameDefine name q =
 let val (hol_name,def) = non_standard_name_defn name q
 in
  ((hol_name, #1(TotalDefn.primDefine def))
   handle e => raise wrap_exn "ACL2 support" "xxDefine" e)
 end;

(*****************************************************************************)
(* acl2Define "acl2_name" `(foo ... = ...) /\ ... ` does the following:      *)
(*                                                                           *)
(*  1. non_standard_nameDefine "acl2_name" `(foo ... = ...) /\ ... `         *)
(*                                                                           *)
(*  2. adds the theorem resulting from the definition to acl2_simps          *)
(*                                                                           *)
(*  3. declare_names("acl2_name","hol_name") ("hol_name" is name of hol)     *)
(*                                                                           *)
(*  4. the definition theorem is returned                                    *)
(*                                                                           *)
(* Example:                                                                  *)
(*                                                                           *)
(* val stringp_def =                                                         *)
(*  acl2Define "COMMON-LISP::STRINGP"                                        *)
(*   `(stringp(str x) = t) /\ (stringp _ = nil)`;                            *)
(*                                                                           *)
(*****************************************************************************)
fun acl2Define acl2_name q =
 let val (hol_name,th) = non_standard_nameDefine acl2_name q
 in
  acl2_simps := (!acl2_simps) @ [th];
  declare_names(acl2_name,hol_name);
  (print"\"";
   print acl2_name;
   print "\" defined with HOL name \"";
   print hol_name; print "\"\n");
  th
 end;

(*****************************************************************************)
(* acl2_tgoal "acl2_name" `(foo ... = ...) /\ ... ` creates a termination    *)
(* goal for the recursive definition with acl2_name replacing foo. Example:  *)
(*                                                                           *)
(*  acl2_tgoal "ACL2::TRUE-LISTP"                                            *)
(*   `true_listp x = ite (consp x) (true_listp (cdr x)) (eq x nil)`          *)
(*                                                                           *)
(*                                                                           *)
(*****************************************************************************)
fun acl2_tgoal acl2_name q =
 let val (hol_name,def) = non_standard_name_defn acl2_name q
 in
  (print "Creating termination goal for ";
   print acl2_name;
   print " ("; print hol_name; print ")\n";
   Defn.tgoal def
   handle e => Raise(wrap_exn "ACL2 support" "Hol_defn" e))
 end;

(*****************************************************************************)
(* acl2_defn "acl2_name" (`(foo ... = ...) /\ ... `, tac) uses tac to        *)
(* solve the termination goal for the recursive definition with acl2_name    *)
(* replacing foo. Makes the definition of acl2_name and then overloads foo   *)
(* on acl2_name. Example:                                                    *)
(*                                                                           *)
(* val (true_listp_def,true_listp_ind) =                                     *)
(*  acl2_defn "ACL2::TRUE-LISTP"                                             *)
(*   (`true_listp x = ite (consp x) (true_listp (cdr x)) (eq x nil)`,        *)
(*    WF_REL_TAC `measure sexp_size`                                         *)
(*     THEN RW_TAC arith_ss [sexp_size_cdr]);                                *)
(*****************************************************************************)
fun acl2_defn acl2_name (q,tac) =
 let val (hol_name,def) = non_standard_name_defn acl2_name q
     val (def_th,ind_th) =
          (Defn.tprove(def,tac)
           handle e => Raise(wrap_exn "ACL2 support" "Defn.tgoal" e))
 in
(*acl2_simps := (!acl2_simps) @ [def_th];*)
  declare_names(acl2_name,hol_name);
  save_thm((hol_name ^ "_def"),def_th);
  save_thm((hol_name ^ "_ind"),ind_th);
  (print"\"";
   print acl2_name;
   print "\" defined with HOL name \"";
   print hol_name; print "\"\n";
   (def_th,ind_th))
 end;

(*****************************************************************************)
(* Generate date and time for making file timestamps                         *)
(*****************************************************************************)
fun date() = Date.fmt "%c" (Date.fromTimeLocal (Time.now ()));

(*****************************************************************************)
(* Create a output stream to a file called file_name.lisp, apply a printer   *)
(* to it and then flush and close the stream.                                *)
(*****************************************************************************)
fun print_lisp_file file_name printer =
 let val outstr = TextIO.openOut(file_name ^ ".lisp")
     fun out s = TextIO.output(outstr,s)
 in
 (out("; File created from HOL using print_lisp_file on " ^ date() ^ "\n\n");
   (* Add time stamp                                                         *)
   (* out("(IN-PACKAGE \"ACL2\")\n\n");                                      *)
   (* ACL2 initialisation (currently commented out at Matt's suggestion)     *)
  printer out;
  TextIO.flushOut outstr;
  TextIO.closeOut outstr)
 end;

(*****************************************************************************)
(* Representation of s-expressions in ML                                     *)
(*                                                                           *)
(* Complex rational a/b + (p/q)i is constructed by mlnum("a","b","p","q").   *)
(* Must use strings, as ML numerals are 32-bit!                              *)
(*                                                                           *)
(*   con mlchr  = fn : char -> mlsexp                                        *)
(*   con mlnum  = fn : string * string * string * string -> mlsexp           *)
(*   con mlpair = fn : mlsexp * mlsexp -> mlsexp                             *)
(*   con mlstr  = fn : string -> mlsexp                                      *)
(*   con mlsym  = fn : string * string -> mlsexp                             *)
(*                                                                           *)
(* Negative numbers are represented by prefixing the numerator with "-",     *)
(* so denominators b and q should be natural number numerals (0,1,2,...),    *)
(* and numerators a and p should be natural number numerals, possibly with   *)
(* a "-" prefix. Thus mlnum("1","-1","0","1") is invalid.                    *)
(*****************************************************************************)
datatype mlsexp =
   mlsym  of string * string
 | mlstr  of string
 | mlchr  of char
 | mlnum  of string * string * string * string
 | mlpair of mlsexp * mlsexp;

val mksym  = curry mlsym
and mkstr  = mlstr
and mkchr  = mlchr o chr
and mknum  = fn numerator_x =>
              fn denominator_x =>
               fn numerator_y =>
                fn denominator_y =>
                 mlnum(numerator_x,denominator_x,numerator_y,denominator_y)
and mkpair = fn x =>
              fn y =>
               mlpair(x,y);

(*****************************************************************************)
(* Test and destructor for mlsym                                             *)
(*****************************************************************************)
fun is_mlsym (mlsym(_,_)) = true
 |  is_mlsym _ = false;

fun dest_mlsym (mlsym(sym_pac,sym_name)) = (sym_pac,sym_name)
 |  dest_mlsym _                         = err "dest_mlsym" "not a sym";

(*****************************************************************************)
(* Alternative name for mlstr used to indicate string originates from a      *)
(* list of characters sent from ACL2.                                        *)
(*****************************************************************************)
val mk_chars_str = mlstr;

(*****************************************************************************)
(* Abbreviation for some symbols.                                            *)
(*****************************************************************************)
val mlnil      = mksym "COMMON-LISP" "NIL"
val mlt        = mksym "COMMON-LISP" "T"
and mlquote    = mksym "COMMON-LISP" "QUOTE"
and mlcons     = mksym "COMMON-LISP" "CONS"
and mllambda   = mksym "COMMON-LISP" "LAMBDA"
and mldefun    = mksym "COMMON-LISP" "DEFUN"
and mldefun_sk = mksym "ACL2"        "DEFUN-SK"
and ml_forall  = mksym "ACL2"        "FORALL"
and ml_exists  = mksym "ACL2"        "EXISTS"
and mlinclude  = mksym "ACL2"        "INCLUDE-BOOK"
and mlmutual   = mksym "ACL2"        "MUTUAL-RECURSION"
and mlencap    = mksym "ACL2"        "ENCAP"
and mldefaxiom = mksym "ACL2"        "DEFAXIOM"
and mldefthm   = mksym "ACL2"        "DEFTHM";

(*****************************************************************************)
(* "tag_ty nam" |--> ("tag_ty","nam")                                        *)
(*****************************************************************************)
val split_tag =
 let
  fun split_tag_chars acc [] = ([],rev acc)
   |  split_tag_chars acc (#" " :: l) = (rev acc,l)
   |  split_tag_chars acc (c :: l) = split_tag_chars (c :: acc) l
 in
  (implode ## implode) o split_tag_chars [] o explode
end;

(*****************************************************************************)
(* "pkg::nam" |--> ("pkg","nam")                                             *)
(*****************************************************************************)
val split_acl2_name =
 let
  fun split_acl2_name_chars acc [] = ([],rev acc)
   |  split_acl2_name_chars acc (#":" :: #":" :: l) = (rev acc,l)
   |  split_acl2_name_chars acc (c :: l) = split_acl2_name_chars (c :: acc) l
 in
  (implode ## implode) o split_acl2_name_chars [] o explode
end;

(*****************************************************************************)
(* Lookup a string in acl2_names. If it corresponds to a full ACL2 name      *)
(* (with package and symbol name separated by "::") then return the ACL2     *)
(* name.  If it corresponds to an ACL2 name without a package name (which    *)
(* shouldn't happen), then add the current_package as package name. If       *)
(* the string isn't in acl2_names and is "ACL2_PAIR" then return             *)
(* mlsym("COMMON-LISP", "CONS"), otherwise split at "::" (or using           *)
(* current_package if no "::") and then use mlsym.                           *)
(*****************************************************************************)
fun string_to_mlsym s =
 case assoc1 s (!acl2_names)
 of SOME(_,acl2_name)
    => let val (pkg,nam) = split_acl2_name acl2_name
       in
        mlsym(if pkg = "" then (!current_package) else pkg, nam)
       end
 |  NONE
   => if s = "ACL2_PAIR"
       then mlcons
       else let val (pkg,nam) = split_acl2_name s
            in
             mlsym(if pkg = "" then (!current_package) else pkg, nam)
            end;

(*****************************************************************************)
(* Test for a proper list: (x1 . (x2 . ... . (xn . nil) ...))                *)
(*****************************************************************************)
fun is_mlsexp_proper_list (sym as mlsym(_,_)) =
     (sym = mlnil)
 |  is_mlsexp_proper_list (mlpair(_,p)) =
     is_mlsexp_proper_list p
 |  is_mlsexp_proper_list _ = false;

(*****************************************************************************)
(* Test for a proper list or an atom                                         *)
(*****************************************************************************)
fun is_mlsexp_list (p as mlpair(_,_)) = is_mlsexp_proper_list p
 |  is_mlsexp_list _                  = true;

(*****************************************************************************)
(* Destruct an ML s-expression list:                                         *)
(*  (x1 . (x2 . ... (xn . nil) ...))  |--> [x1,x2,...,xn]                    *)
(*****************************************************************************)
fun dest_mlsexp_list (sym as mlsym(_,_)) =
     if (sym = mlnil) then [] else [sym]
 |  dest_mlsexp_list (mlpair(p1,p2)) =
     p1 :: dest_mlsexp_list p2
 |  dest_mlsexp_list p = [p];

(*****************************************************************************)
(* [x1,...,xn] --> (mkpair x1 ... (mkpair xn mlnil) ... ))                   *)
(*****************************************************************************)
fun mk_mlsexp_list [] = mlnil
 |  mk_mlsexp_list (x::xl) = mlpair(x, mk_mlsexp_list xl);

(*****************************************************************************)
(* Test for a quote: (QUOTE x)                                               *)
(*****************************************************************************)
fun is_mlquote (mlpair(x,mlpair(_,n))) = (x = mlquote) andalso (n = mlnil)
 |  is_mlquote _                       = false;

(*****************************************************************************)
(* Extract body of a quote: (QUOTE x) |--> x                                 *)
(*****************************************************************************)
fun dest_mlquote (mlpair(_,mlpair(x,_))) = x
 |  dest_mlquote _                       = err "dest_mlquote" "bad argument";

(*****************************************************************************)
(* Make an ML quote x |--> (QUOTE x)                                         *)
(*****************************************************************************)
fun mk_mlquote x = mk_mlsexp_list[mlquote,x];

(*****************************************************************************)
(* Test for a lambda: ((LAMBDA (x1 ... xm) bdy) (a1 ... an))                 *)
(*****************************************************************************)
fun is_mllambda (mlpair(mlpair(x,mlpair(params,mlpair(bdy,n))),args)) =
     (x = mllambda)        andalso
     is_mlsexp_list params andalso
     is_mlsexp_list args   andalso
     is_mlsexp_list bdy    andalso
     (n = mlnil)
 |  is_mllambda _ = false;

(*****************************************************************************)
(* Lambda destructor:                                                        *)
(*   ((LAMBDA (x1 ... xm) bdy) (a1 ... an))                                  *)
(*   |-->                                                                    *)
(*   ([x1, ..., xm], bdy, [a1, ..., an])                                     *)
(*                                                                           *)
(*****************************************************************************)
fun dest_mllambda (mlpair(mlpair(_,mlpair(params,mlpair(bdy,_))),args)) =
     (dest_mlsexp_list params, bdy, dest_mlsexp_list args)
 |  dest_mllambda _ =
     err "dest_mllambda" "bad argument";

(*****************************************************************************)
(* Test for an include-book: (INCLUDE_BOOK book)                             *)
(*****************************************************************************)
fun is_mlinclude
     (mlpair(x,mlpair(mlstr book,n))) =
      (x = mlinclude)       andalso
      (n = mlnil)
 |  is_mlinclude _  = false;

(*****************************************************************************)
(* Include-book destructor: (INCLUDE-BOOK book) |--> book                    *)
(*****************************************************************************)
fun dest_mlinclude b =
     if is_mlinclude b
      then case dest_mlsexp_list b
           of [_,mlstr book] => book
           |  _              => err "dest_mlinclude" "bad case match"
      else err "dest_mlinclude" "not an include-book";

(*****************************************************************************)
(* Include-book Constructor: book |--> (INCLUDE-BOOK book)                   *)
(*****************************************************************************)
fun mk_mlinclude book =
 mk_mlsexp_list [mlinclude, mlstr book];

(*****************************************************************************)
(* Test for a defun: (DEFUN nam (x1 ... xn) bdy)                             *)
(*****************************************************************************)
fun is_mldefun
     (mlpair(x,mlpair(mlsym(_,_),mlpair(params,mlpair(bdy,n))))) =
      (x = mldefun)         andalso
      is_mlsexp_list params andalso
      is_mlsexp_list bdy    andalso
      (n = mlnil)
 |  is_mldefun _  = false;

(*****************************************************************************)
(* Defun destructor: (DEFUN nam (x1 ... xn) bdy) |-->(nam,[x1,...,xn],bdy)   *)
(*****************************************************************************)
fun dest_mldefun d =
     if is_mldefun d
      then case dest_mlsexp_list d
           of [_,nam,params,bdy]
              => (nam, dest_mlsexp_list params, bdy)
           |  _
              => err "dest_mldefun" "bad case match"
      else err "dest_mldefun" "not a defun";

(*****************************************************************************)
(* Defun Constructor: (nam,[x1,...,xn],bdy) |--> (DEFUN nam (x1 ... xn) bdy) *)
(*****************************************************************************)
fun mk_mldefun (nam, params, bdy) =
 mk_mlsexp_list [mldefun, nam, mk_mlsexp_list params, bdy];

(*****************************************************************************)
(* Test for a defun_sk: (DEFUN-SK nam (x1 ... xn) (QUANT (v1 ... vm) bdy))   *)
(*****************************************************************************)
fun is_mldefun_sk
     (mlpair
       (x,
        mlpair
         (mlsym(_,_),
          mlpair
           (params,
             mlpair
              (mlpair(quant, mlpair(qvars, mlpair(bdy,n1))),
              n2))))) =
      (x = mldefun_sk)                  andalso
      is_mlsexp_list params             andalso
      (mem quant [ml_forall,ml_exists]) andalso
      is_mlsexp_list qvars              andalso
      is_mlsexp_list bdy                andalso
      (n1 = mlnil)                      andalso
      (n2 = mlnil)
 |  is_mldefun_sk _  = false;

(*****************************************************************************)
(* Defun destructor:                                                         *)
(* (DEFUN-SK nam (x1 ... xn) (QUANT (v1 ... vm) bdy))                        *)
(* |-->                                                                      *)
(* (nam, [x1,...,xn], quant, qvars, bdy)                                     *)
(*****************************************************************************)
fun dest_mldefun_sk d =
     if is_mldefun_sk d
      then case dest_mlsexp_list d
           of [_,nam,params,quant_bdy]
              => (case dest_mlsexp_list quant_bdy
                  of [quant,qvars,bdy]
                     => (nam, dest_mlsexp_list params,
                         quant, dest_mlsexp_list qvars, bdy)
                  |  _
                     => err "dest_mldefun_sk" "bad quant case match")
           |  _
              => err "dest_mldefun_sk" "bad case match"
      else err "dest_mldefun" "not a defun";

(*****************************************************************************)
(* Defun Constructor:                                                        *)
(* (nam,[x1,...,xn],quant,qvars,bdy)                                         *)
(* |-->                                                                      *)
(* (DEFUN-SK nam (x1 ... xn) (quant qvars bdy))                              *)
(*****************************************************************************)
fun mk_mldefun_sk (nam, params, quant, qvars, bdy) =
 mk_mlsexp_list
  [mldefun_sk, nam, mk_mlsexp_list params,
   mk_mlsexp_list [quant, mk_mlsexp_list qvars, bdy]];

(*****************************************************************************)
(* Test for a defaxiom: (DEFAXIOM nam bdy)                                   *)
(*****************************************************************************)
fun is_mldefaxiom
     (mlpair(x,mlpair(mlsym(_,_),mlpair(bdy,n)))) =
      (x = mldefaxiom)   andalso
      is_mlsexp_list bdy andalso
      (n = mlnil)
 |  is_mldefaxiom _  = false;

(*****************************************************************************)
(* Defaxiom destructor: (DEFAXIOM nam bdy) |--> (nam,bdy)                    *)
(*****************************************************************************)
fun dest_mldefaxiom
     (mlpair(_,mlpair(nam,mlpair(bdy,_)))) = (nam, bdy)
 |  dest_mldefaxiom _ = err "dest_mldefaxiom" "bad argument";

(*****************************************************************************)
(* Defaxiom constructor:  (nam,bdy) |--> (DEFAXIOM nam bdy)                  *)
(*****************************************************************************)
fun mk_mldefaxiom(nam,bdy) =
 mk_mlsexp_list [mldefaxiom, nam, bdy];

(*****************************************************************************)
(* Test for a defthm: (DEFTHM nam bdy)                                        *)
(*****************************************************************************)
fun is_mldefthm
     (mlpair(x,mlpair(mlsym(_,_),mlpair(bdy,n)))) =
      (x = mldefthm)     andalso
      is_mlsexp_list bdy andalso
      (n = mlnil)
 |  is_mldefthm _  = false;

(*****************************************************************************)
(* Defthm destructor: (DEFTHM nam bdy) |--> (nam,bdy)                        *)
(*****************************************************************************)
fun dest_mldefthm
     (mlpair(_,mlpair(nam,mlpair(bdy,_)))) = (nam, bdy)
 |  dest_mldefthm _ = err "dest_mldefthm" "bad argument";

(*****************************************************************************)
(* Defthm constructor:  (nam,bdy) |--> (DEFTHM nam bdy)                      *)
(*****************************************************************************)
fun mk_mldefthm(nam,bdy) =
 mk_mlsexp_list [mldefthm, nam, bdy];

(*****************************************************************************)
(* Test for a mutual: (MUTUAL-RECURSION d1 ... dn)                           *)
(*****************************************************************************)
fun is_mlmutual (mlpair(x, defs)) =
      (x = mlmutual) andalso is_mlsexp_list defs
 |  is_mlmutual _  = false;

(*****************************************************************************)
(* Mutual destructor: (MUTUAL-RECURSION d1 ... dn) |--> [d1, ..., dn]        *)
(*****************************************************************************)
fun dest_mlmutual (mlpair(_, defs)) = dest_mlsexp_list defs
 |  dest_mlmutual _ = err "dest_mlmutual" "bad argument";

(*****************************************************************************)
(* Test for a encap: (ENCAP acl2sig events)                                  *)
(*****************************************************************************)
fun is_mlencap (mlpair(x, mlpair(acl2sig,events))) =
      (x = mlencap) andalso is_mlsexp_list acl2sig
                    andalso is_mlsexp_list events
 |  is_mlencap _  = false;

(*****************************************************************************)
(* Mutual destructor: (ENCAP (s1 ... sm) (e1 ... en))                        *)
(*                    |-->                                                   *)
(*                    ([s1, ..., sm],[e1,...,en])                            *)
(*****************************************************************************)
fun dest_mlencap (mlpair(_, mlpair(acl2sig,events))) =
     (dest_mlsexp_list acl2sig, dest_mlsexp_list events)
 |  dest_mlencap _ = err "dest_mlencap" "bad argument";

(*****************************************************************************)
(* Test for ``nat n`` where n is a numeral                                   *)
(*****************************************************************************)
fun is_nat tm =
 is_comb tm           andalso
 (rator tm = ``nat``) andalso
 is_numeral(rand tm);

(*****************************************************************************)
(* Convert ``nat n`` to "n"                                                  *)
(*****************************************************************************)
fun dest_nat tm = Arbnum.toString(dest_numeral(rand tm));

(*****************************************************************************)
(* Test for ``n`` where n is an integer numeral                              *)
(*****************************************************************************)
fun is_integer tm =
 is_comb tm andalso
 (if rator tm = ``int_of_num:num->int``       (* $& overloaded on int_of_num *)
   then is_numeral(rand tm) else
  if rator tm = ``int_neg:int->int``          (* $~ overloaded on int_neg    *)
   then is_integer(rand tm) else
  false);

(*****************************************************************************)
(* Test for ``int n`` where n is an integer numeral                          *)
(*****************************************************************************)
fun is_int tm =
 is_comb tm           andalso
 (rator tm = ``int``) andalso
 is_integer(rand tm);

(*****************************************************************************)
(* Convert an integer term numeral to a string:                              *)
(*                                                                           *)
(*  ``&d1d2...dn``   |-->  "d1d2...dn"                                       *)
(*  ``~& d1d2...dn`` |-->  "-d1d2...dn"                                      *)
(*****************************************************************************)
fun dest_integer tm =
 let val (opr,args) = strip_comb tm
 in
  if opr = ``int_of_num:num->int`` andalso (tl args = [])
   then (if is_numeral(hd args)
          then Arbnum.toString(dest_numeral(hd args))
          else (print_term tm;
                print " is not a non-negative integer numeral\n";
                err "dest_integer" "not a non-negative integer numeral"))
   else (if opr = ``int_neg:int->int`` andalso (tl args = [])
          then ("-" ^ dest_integer(hd args))
          else (print_term tm;
                print " is not an integer numeral\n";
                err "dest_integer" "not an integer numeral"))
 end;

(*****************************************************************************)
(* Convert ``int n`` to dest_integer ``n``                                   *)
(*****************************************************************************)
fun dest_int tm = dest_integer(rand tm);

(*****************************************************************************)
(* Replace initial "-" by "~" in a string (converts ACL2 representation of   *)
(* a negative integer to HOL representation).                                *)
(*****************************************************************************)
fun acl2_int_to_hol_int s =
 let val chars = explode s
  in
   if not(null chars) andalso hd chars = #"-"
    then implode(#"~" :: tl chars)
    else s
  end;

(*****************************************************************************)
(* Test whether a string is a natural number numeral                         *)
(*****************************************************************************)
fun is_num_string s = all Char.isDigit (explode s);


(*****************************************************************************)
(* Test whether a string is an integer numeral                               *)
(*****************************************************************************)
fun is_int_string s =
 let val sl = explode s
 in
  null sl
   orelse ((hd sl = #"-") andalso all Char.isDigit (tl sl))
   orelse all Char.isDigit sl
 end;

(*****************************************************************************)
(* Test for ``cpx a b c d``                                                  *)
(*****************************************************************************)
fun is_cpx tm =
 let val (opr,args) = strip_comb tm
 in
  (opr = ``cpx``)
    andalso (length args = 4)
    andalso is_int_string(dest_integer(el 1 args))
    andalso is_num_string(dest_integer(el 2 args))
    andalso is_int_string(dest_integer(el 3 args))
    andalso is_num_string(dest_integer(el 4 args))
 end;

(*****************************************************************************)
(* ``cpx an ad bn bd`` |--> ("an", "ad", "bn", "bd")                         *)
(*                                                                           *)
(* Negative numbers are represented with a prefixed "-" (e.g. "-3").         *)
(*****************************************************************************)
fun dest_cpx tm =
 if is_cpx tm          (* Probably redundant extra check included for safety *)
  then
  let val (_,args) = strip_comb tm
  in
   (dest_integer(el 1 args),
    dest_integer(el 2 args),
    dest_integer(el 3 args),
    dest_integer(el 4 args))
  end
 else (print_term tm;
       print " is not a complex numeral\n";
       err "dest_cpx" "not a complex numeral");

(*****************************************************************************)
(* mlsym(pkg,nam) |--> "pkg::nam"                                            *)
(*****************************************************************************)
fun mlsym_to_string (sym as mlsym(pkg,nam)) = (pkg^"::"^nam)
 |  mlsym_to_string _ = err "mlsym_to_string" "non sym argument";

(*****************************************************************************)
(* Association list of pairs of the form ("xyz", c), where c is a            *)
(* constant defined by |- c = "xyz". Used to avoid building terms with       *)
(* lots of string literals.                                                  *)
(*****************************************************************************)
val string_abbrevs = ref([]: (string * term)list);

(*****************************************************************************)
(* Check if an abbreviation already exists                                   *)
(*****************************************************************************)
fun has_abbrev s = can (assoc s) (!string_abbrevs);

(*****************************************************************************)
(* Function to add a list of string abbreviations to string_abbrevs          *)
(*****************************************************************************)
fun add_string_abbrevs tml = (string_abbrevs := (!string_abbrevs) @ tml);

(*****************************************************************************)
(* Declare constants ACL2_STRING_ABBREV_n, ACL2_STRING_ABBREV_n+1 etc to     *)
(* abbreviate strings in a supplied list. The starting point n is kept in    *)
(* the reference string_abbrev_count.                                        *)
(*                                                                           *)
(* If a string already has an abbreviation or is in a list !no_abbrev_list   *)
(* of strings that shouldn't be abbreviated, then it is ignored.             *)
(*****************************************************************************)
val string_abbrev_count = ref 0;
val no_abbrev_list      = ref(["NIL","QUOTE"]);

fun make_string_abbrevs [] = ()
 |  make_string_abbrevs (s::sl) =
     if has_abbrev s
      then (print "Warning: \""; print s; print "\" already abbreviated by ";
            print_term(assoc s (!string_abbrevs)); print "\n";
            make_string_abbrevs sl) else
     if mem s (!no_abbrev_list)
      then (print "Warning: \""; print s; print "\" is in !no_abbrev_list\n";
            make_string_abbrevs sl)
      else
       (add_string_abbrevs
         [(s, lhs
               (concl
                 (SPEC_ALL
                  (Define
                    `^(mk_var
                       (("ACL2_STRING_ABBREV_"
                         ^ Int.toString(!string_abbrev_count)),
                        ``:string``)) =
                     ^(fromMLstring s)`))))];
        (string_abbrev_count := (!string_abbrev_count)+1);
        make_string_abbrevs sl);

(*****************************************************************************)
(* Print !string_abbrevs to a string (used in adjoin_to_theory).             *)
(* There may be a better way of doing this!                                  *)
(*****************************************************************************)
local
fun string_abbrevs_to_string_aux [] = ""
 |  string_abbrevs_to_string_aux [(s,c)] =
    ("(\"" ^ s ^ "\",Parse.Term`" ^ fst(dest_const c) ^"`)")
 |  string_abbrevs_to_string_aux ((s,c)::pl) =
    ("(\"" ^ s ^ "\",Parse.Term`" ^ fst(dest_const c) ^"`)," ^
    string_abbrevs_to_string_aux pl)
in
fun string_abbrevs_to_string pl =
 ("[" ^ string_abbrevs_to_string_aux pl ^ "]")
end;

(*****************************************************************************)
(* Version of fromMLstring that looks up in string_abbrevs. Convert an ML    *)
(* string to a term: return constant from string_abbrevs if one is found,    *)
(* otherwise return a string literal.                                        *)
(*****************************************************************************)
fun abbrevMLstring s =
 assoc s (!string_abbrevs)
  handle HOL_ERR _ => fromMLstring s;

(*****************************************************************************)
(* Version of fromHOLstring that looks up in string_abbrevs.                 *)
(*****************************************************************************)
fun abbrevHOLstring c =
 rev_assoc c (!string_abbrevs)
  handle HOL_ERR _ => fromHOLstring c;

(*****************************************************************************)
(* Get the HOL name from ACL2 name.                                          *)
(* If there is no HOL name (e.g. an ACL2 variable) the ACL2 name is          *)
(* returned.                                                                 *)
(*****************************************************************************)
local
fun get_hol_name_from_acl2_name_aux [] sym =
     mlsym_to_string sym
 |  get_hol_name_from_acl2_name_aux ((hol,acl2) :: nl) sym =
     if acl2 = mlsym_to_string sym
      then hol
      else get_hol_name_from_acl2_name_aux nl sym
in
fun get_hol_name_from_acl2_name sym =
     get_hol_name_from_acl2_name_aux (!acl2_names) sym
end;

(*****************************************************************************)
(* Test that a type is ``:sexp`` or ``:sexp -> ... -> sexp``                 *)
(*****************************************************************************)
fun is_sexp_ty ty =
 let val (tyop,tyargs) = dest_type ty
 in
  (tyop = "sexp"
  orelse (tyop = "fun"
          andalso hd tyargs = ``:sexp``
          andalso is_sexp_ty(hd(tl tyargs))))
 end;

(*****************************************************************************)
(* Translate a term of type ``:sexp`` to an s-expression represented in ML   *)
(*****************************************************************************)
fun term_to_mlsexp tm =
 if is_var tm
  then string_to_mlsym(fst(dest_var tm)) else
 if is_const tm
  then
   (if is_sexp_ty(type_of tm)
     then string_to_mlsym(fst(dest_const tm))
     else (print_term tm;
           print " has type ``";
           print_type(type_of tm);
           print "`` so is not a first-order function on S-expressions\n";
           err "term_to_mlsexp" "constant has bad type")) else
 if is_string tm
  then string_to_mlsym(fromHOLstring tm) else
 if is_nat tm
  then mlnum(dest_nat tm, "1", "0", "1") else
 if is_int tm
  then mlnum(dest_int tm, "1", "0", "1") else
 if is_cpx tm
  then mlnum(dest_cpx tm) else
 if is_numeral tm
  then (print "Bad occurence of numeral ";
        print_term tm; print ". Use \"nat\", \"int\" or \"cpx\".\n";
        err "term_to_mlsexp" "bad occurrence of a numeral") else
 if is_integer tm
  then (print "Bad occurence of integer numeral ";
        print_term tm; print ". Use \"nat\", \"int\" or \"cpx\".\n";
        err "term_to_mlsexp" "bad occurrence of an integer numeral") else
 if is_let tm
  then
   let val (param_arg_tuples,bdy) = dest_anylet tm
       val (param_tuples,arg_tuples) = unzip param_arg_tuples
       val args = (flatten o map strip_pair) arg_tuples
       val params = (flatten o map strip_pair) param_tuples
   in
    if not(length params = length args)
     then (print_term tm; print "\n";
           print "different numbers of formal and actual parameters\n";
           err "term_to_mlsexp" "formal/actual mismatch")
     else mk_mlsexp_list
          (mk_mlsexp_list
            [mllambda,
             mk_mlsexp_list(map term_to_mlsexp params),
             term_to_mlsexp bdy]
           :: map term_to_mlsexp args)
   end else
 if is_comb tm
  then
   let val (opr,args) = strip_comb tm
   in
    if is_const opr
     then (case fst(dest_const opr)
           of "ACL2_SYMBOL"    => mk_mlquote
                                   (mlsym(abbrevHOLstring(hd args),
                                          abbrevHOLstring(hd(tl args))))
           |  "ACL2_STRING"    => mlstr(abbrevHOLstring(hd args))
           |  "ACL2_CHARACTER" => mlchr(fromHOLchar(hd args))
           |  "ACL2_NUMBER"    => (print_term tm; print "\n";
                                   print "term built with num not supported";
                                   print " -- use nat, int or cpx\n";
                                   err "term_to_mlsexp"
                                       "ACL2_NUMBER case unsupported")
           |  "cpx"            => (print_term tm; print "\n";
                                   print "bad use of cpx\n";
                                   err "term_to_mlsexp"
                                       "badly formed application of cpx")
           |  _                => mk_mlsexp_list
                                   (map term_to_mlsexp (opr::args))

          ) else
    if is_var opr
     then mk_mlsexp_list (map term_to_mlsexp (opr::args)) else
    if is_abs opr
     then
      let val (params,bdy) = strip_abs opr
      in
       if not(length params = length args)
        then (print_term tm; print "\n";
              print "different numbers of formal and actual parameters\n";
              err "term_to_mlsexp" "formal/actual mismatch")
        else mk_mlsexp_list
             (mk_mlsexp_list
               [mllambda,
                mk_mlsexp_list(map term_to_mlsexp params),
                term_to_mlsexp bdy]
              :: map term_to_mlsexp args)
      end else
    (print_term opr;
     print " is not allowed as a function\n";
     err "term_to_mlsexp" "bad function")
   end else
 (print_term tm; print "\n";
  print "bad argument to term_to_mlsexp\n";
  err "term_to_mlsexp" "bad argument");

(*****************************************************************************)
(* Print an ML s-expression s on an output stream out                        *)
(*****************************************************************************)
fun print_mlsexp (out:string->unit) (sym as mlsym(_,_))  =
     out(mlsym_to_string sym)
 | print_mlsexp (out:string->unit) (mlstr s) =
     (out "\""; out s; out "\"")
 | print_mlsexp (out:string->unit) (mlchr c) =
     (out "(code-char "; out(int_to_string(ord c)); out ")")
 | print_mlsexp (out:string->unit) (mlnum(an,ad,bn,bd)) =
    if (bn = "0") andalso (bd = "1")
     then (out an; out "/"; out ad)
     else (out "(COMMON-LISP::COMPLEX ";
           out an; out "/"; out ad;
           out " ";
           out bn; out "/"; out bd;
           out ")")
 | print_mlsexp (out:string->unit) (mlpair(p1,p2)) =
     (out "(";
      (if is_mlsexp_list p2
        then let val sl = dest_mlsexp_list p2
             in
              if null sl
               then print_mlsexp out p1
               else (print_mlsexp out p1;
                     map (fn p => (out " "; print_mlsexp out p)) sl;
                     ())
             end
        else (print_mlsexp out p1; out " . "; print_mlsexp out p2));
      out ")");

(*****************************************************************************)
(* Print an ML s-expression to the interactive session                       *)
(*****************************************************************************)
fun pr_mlsexp s = (print_mlsexp print s; print "\n");

(*****************************************************************************)
(* Print an s-expression term to the interactive session                     *)
(*****************************************************************************)
fun pr_sexp t = pr_mlsexp(term_to_mlsexp t);

(*****************************************************************************)
(* Extract the name of a constant or variable                                *)
(*****************************************************************************)
exception get_name_fail;
fun get_name tm =
 if is_const tm
  then fst(dest_const tm) else
 if is_var tm then fst(dest_var tm)
  else raise get_name_fail;

(*****************************************************************************)
(* ``f x1 ... xn = e`` --> (defun f (x1 ... xn) ^(term_to_mlsexp e))         *)
(*****************************************************************************)
fun deftm_to_mlsexp_defun tm =
 let val (l,r) = dest_eq(spec_all tm)
     val (opr, args) = strip_comb l
 in
  mk_mlsexp_list
   [mksym "COMMON-LISP" "DEFUN",
    string_to_mlsym(get_name opr),
    mk_mlsexp_list(map term_to_mlsexp args),
    term_to_mlsexp r]
 end;

(*****************************************************************************)
(* Translate a hol-acl2 definition                                           *)
(*                                                                           *)
(*   |- f x1 ... xn = e                                                      *)
(*                                                                           *)
(* to an ML s-expression representing                                        *)
(*                                                                           *)
(*  (defun f (x1 ... xn) ^(term_to_mlsexp e))                                *)
(*****************************************************************************)
fun def_to_mlsexp_defun th =
 let val (asl, concl) = dest_thm(SPEC_ALL th)
     val _ = if not(asl = [])
               then(print_thm th;
                    print "\n"; print"should not have any assumptions\n";
                    err "mk_mlsexp_defthm" "assumptions not allowed")
               else ()
 in
  deftm_to_mlsexp_defun concl
 end;

(*****************************************************************************)
(* Print a hol-acl2 definition                                               *)
(*                                                                           *)
(*   |- f x1 ... xn = e                                                      *)
(*                                                                           *)
(* as                                                                        *)
(*                                                                           *)
(*  (defun f (x1 ... xn) ^(term_to_mlsexp e))                                *)
(*****************************************************************************)
fun pr_mlsexp_defun th = pr_mlsexp(def_to_mlsexp_defun th);

(*****************************************************************************)
(* Code for processing ACL2 defuns slurped into HOL via Matt's a2ml tool     *)
(*****************************************************************************)

(*****************************************************************************)
(* Convert a string to integer numeral                                       *)
(*                                                                           *)
(*  string_to_int_term "37"  = ``37``                                        *)
(*  string_to_int_term "~37" = ``~37``                                       *)
(*  string_to_int_term "-37" = ``~37``                                       *)
(*****************************************************************************)
fun string_to_int_term s = intSyntax.term_of_int(Arbint.fromString s);

(*****************************************************************************)
(* There are two obvious ways to convert an mlsexp to a term:                *)
(*                                                                           *)
(*  1. recursively descend through it build up a term;                       *)
(*                                                                           *)
(*  2. convert it to a string s than then use Term[QUOTE s].                 *)
(*                                                                           *)
(* Method 1 allows more detailed checking and gives finer control over       *)
(* error messages.  Method 2 is a bit easier to implement, but may be        *)
(* less robust.                                                              *)
(*                                                                           *)
(* Initially we started to implement Method 2 as it was simpler, but then    *)
(* it became clear that it would not handle ACL2's non standard              *)
(* identifier names, so we switched to Method 1.                             *)
(*                                                                           *)
(* However, the unfinished partial implementation of Method 2                *)
(* (mlsexp_to_string) is useful for debugging, as it enables one to print    *)
(* compact representations of imported mlsexps.                              *)
(*                                                                           *)
(*****************************************************************************)

(*****************************************************************************)
(* Convert an ML s-expression (mlsexp) to a string that will parse to the    *)
(* corresponding HOL s-expression (sexp).                                    *)
(*****************************************************************************)
fun mlquote_to_string (mlsym(pkg,nam)) =
     ("(sym \"" ^ pkg ^ "\" \"" ^ nam ^"\")")
 |  mlquote_to_string (mlstr s) =
     ("(str " ^ "\"" ^ s ^ "\")")
 |  mlquote_to_string (mlchr c) =
     ("(chr " ^ "(CHR " ^ int_to_string(ord c) ^ "))")
 |  mlquote_to_string (mlnum(an,ad,bn,bd)) =
     ("(cpx " ^
         acl2_int_to_hol_int an ^ " " ^
         acl2_int_to_hol_int ad ^ " " ^
         acl2_int_to_hol_int bn ^ " " ^
         acl2_int_to_hol_int bd ^")")
 |  mlquote_to_string (mlpair(x,y)) =
     ("(cons " ^ mlquote_to_string x ^ " " ^ mlquote_to_string y ^ ")");

(*****************************************************************************)
(* Convert an ML s-expression (mlsexp) to a string that will parse to the    *)
(* corresponding HOL s-expression (sexp).                                    *)
(*****************************************************************************)
fun mlquote_to_string (mlsym(pkg,nam)) =
     ("(sym \"" ^ pkg ^ "\" \"" ^ nam ^"\")")
 |  mlquote_to_string (mlstr s) =
     ("(str " ^ "\"" ^ s ^ "\")")
 |  mlquote_to_string (mlchr c) =
     ("(chr " ^ "(CHR " ^ int_to_string(ord c) ^ "))")
 |  mlquote_to_string (mlnum(an,ad,bn,bd)) =
     ("(cpx " ^
         acl2_int_to_hol_int an ^ " " ^
         acl2_int_to_hol_int ad ^ " " ^
         acl2_int_to_hol_int bn ^ " " ^
         acl2_int_to_hol_int bd ^")")
 |  mlquote_to_string (mlpair(x,y)) =
     ("(cons " ^ mlquote_to_string x ^ " " ^ mlquote_to_string y ^ ")");

(*****************************************************************************)
(* Convert an ML s-expression (mlsexp) to the coresponding HOL               *)
(* s-expression (i.e. term of type sexp).                                    *)
(*****************************************************************************)
fun mlquote_to_term (sym as mlsym(pkg,nam)) =
     if sym = mlnil then ``nil`` else
     if sym = mlt   then ``t``   else
     ``sym ^(abbrevMLstring pkg) ^(abbrevMLstring nam)``
 |  mlquote_to_term (mlstr s) =
     ``str ^(abbrevMLstring s)``
 |  mlquote_to_term (mlchr c) =
     ``chr ^(fromMLchar c)``
 |  mlquote_to_term (mlnum(an,ad,bn,bd)) =
     ``cpx ^(string_to_int_term an)
           ^(string_to_int_term ad)
           ^(string_to_int_term bn)
           ^(string_to_int_term bd)``
 |  mlquote_to_term (mlpair(x,y)) =
     ``cons ^(mlquote_to_term x) ^(mlquote_to_term y)``;

(*****************************************************************************)
(* Convert an mlsexp representing a term to a string.                        *)
(*                                                                           *)
(* From: http://www.dina.kvl.dk/~sestoft/mosmllib/List.html                  *)
(*                                                                           *)
(*    [foldl op% e xs] evaluates xn % (x(n-1) % ( ... % (x2 % (x1 % e))))    *)
(*    where xs = [x1, x2, ..., x(n-1), xn], and % is taken to be infixed.    *)
(*                                                                           *)
(*****************************************************************************)
fun mlsexp_to_string (sym as mlsym(_,_)) =
     mlsym_to_string sym
 |  mlsexp_to_string (mlstr s) = ("(str " ^ "\"" ^ s ^ "\")")
 |  mlsexp_to_string (mlchr c) =
      ("(chr " ^ "(CHR " ^ int_to_string(ord c) ^ "))")
 |  mlsexp_to_string (mlnum(an,ad,bn,bd)) =
     ("(cpx " ^
         acl2_int_to_hol_int an ^ " " ^
         acl2_int_to_hol_int ad ^ " " ^
         acl2_int_to_hol_int bn ^ " " ^
         acl2_int_to_hol_int bd ^")")
 |  mlsexp_to_string (p as mlpair(x,y)) =
     if is_mlquote p
      then mlquote_to_string(dest_mlquote p)
      else ("(" ^
            (if is_mlsexp_list y
              then foldl
                    (fn (z,zs) => zs ^ " " ^ mlsexp_to_string z)
                    (mlsexp_to_string x)
                    (dest_mlsexp_list y)
              else (print "attempt to translate a non-list to a term\n";
                    err "mlsexp_to_string" "non-list")) ^
            ")");

(*****************************************************************************)
(* mlsym(pkg,nam) |--> mk_var("pkg::nam",``:sexp``)                          *)
(*****************************************************************************)
fun param_to_var (sym as mlsym(_,_)) =
      mk_var(mlsym_to_string sym,``:sexp``)
 |  param_to_var _ =
      (print "Not a mlsym\n";
       err "param_to_var" "parameter not an mlsym");

(*****************************************************************************)
(* mlsym(pkg,nam) ty |--> mk_var("pkg::nam",ty)                              *)
(*****************************************************************************)
fun name_to_var (sym as mlsym(_,_)) ty =
      mk_var(mlsym_to_string sym,ty)
 |  name_to_var _ _ =
      (print "Not a mlsym\n";
       err "name_to_var" "name not an mlsym");

(*****************************************************************************)
(* Look up the HOL name of an ACL2 name and return the corresponding         *)
(* term.  Return a variable with a supplied type if there is no HOL name.    *)
(*****************************************************************************)
val acl2_name_to_term_print_flag = ref false;

local
fun if_print s = if (!acl2_name_to_term_print_flag) then print s else ()
in
fun acl2_name_to_term sym ty =
 if sym = mlt
  then ``t`` else
 if sym = mlnil
  then ``nil`` else
 if sym = mlcons
  then ``ACL2_PAIR`` else
 let val sym_string = mlsym_to_string sym
     val sym_terms = Term.decls sym_string
     val sym_types = map (snd o dest_const) sym_terms
 in
  if mem ty sym_types
   then mk_const(sym_string,ty)
   else (if_print "Warning: \"";
         if_print sym_string;
         if_print "\" made a variable by acl2_name_to_term\n";
         mk_var(sym_string,ty))
 end
end;

(*****************************************************************************)
(* n |--> ``:sexp -> ... -> sexp`` (n arguments)                             *)
(*****************************************************************************)
fun mk_sexp_fun_ty n =
 if n = 0 then ``:sexp`` else ``:sexp -> ^(mk_sexp_fun_ty(n-1))``;

(*****************************************************************************)
(* list_mk_abs doesn't create an abstraction when the arg list is empty      *)
(*****************************************************************************)
val list_mk_fun = list_mk_abs;

(*****************************************************************************)
(* Convert an mlsexp representing a term to the term.                        *)
(*****************************************************************************)
fun mlsexp_to_term (sym as mlsym(_,_)) =
    acl2_name_to_term sym ``:sexp``
 |  mlsexp_to_term (mlstr s) = ``str ^(abbrevMLstring s)``
 |  mlsexp_to_term (mlchr c) = ``chr ^(fromMLchar c)``
 |  mlsexp_to_term (mlnum(an,ad,bn,bd)) =
     ``cpx ^(string_to_int_term an)
           ^(string_to_int_term ad)
           ^(string_to_int_term bn)
           ^(string_to_int_term bd)``
 |  mlsexp_to_term (p as mlpair(x,y)) =
     if is_mlquote p
      then mlquote_to_term(dest_mlquote p) else
     if is_mllambda p
      then let val (params,bdy,args) = dest_mllambda p
           in
            list_mk_comb
             (list_mk_fun(map param_to_var params, mlsexp_to_term bdy),
              map mlsexp_to_term args)
           end else
     if is_mlsexp_list y
      then let val args = map mlsexp_to_term (dest_mlsexp_list y)
               val opr = if is_mlsym x
                          then acl2_name_to_term
                                x
                                (mk_sexp_fun_ty(length args))
                          else mlsexp_to_term x
           in
            (list_mk_comb(opr,args)
             handle HOL_ERR _ =>
              (print "Can't make term\n";
               print(mlsexp_to_string p);
               print "\n";
               err "mlsexp_to_term" "bad mlsexp"))
            end else
     (print "attempt to translate a non-list to a term\n";
      err "mlsexp_to_term" "non-list");

(*****************************************************************************)
(* (defun d (x1 ... xm) b) |--> "d x1 ... xm = b"                            *)
(*****************************************************************************)
fun defun_to_string d =
 if is_mldefun d
  then let val (sym, params, bdy) = dest_mldefun d
       in
        foldl
         (fn (z,zs) => zs ^ " " ^ z)
         ("ACL2_" ^ mlsym_to_string sym)
         (map mlsym_to_string params)
        ^ " = " ^ mlsexp_to_string bdy
      end
  else (print "defun badly formed\n";
        err "defun_to_string" "bad defun");

(*****************************************************************************)
(* Test for a defun, defaxiom or defthm                                      *)
(*****************************************************************************)
fun is_mldef d =
 is_mldefun d orelse is_mldefun_sk d orelse is_mldefaxiom d orelse is_mldefthm d;

(*****************************************************************************)
(* ``f = \x1 ... xn. bdy`` --> ``f x1 ... xn = bdy``                         *)
(*****************************************************************************)
fun mk_def_eq tm =
 if is_eq tm
  then foldl
        (fn (v,t) => mk_eq(mk_comb(lhs t,v),beta_conv(mk_comb(rhs t,v))))
        tm
        (fst(strip_abs(rhs tm)))
  else tm;

(*****************************************************************************)
(* |- f = \x1 ... xn. bdy                                                    *)
(* ----------------------                                                    *)
(*  |- f x1 ... xn = bdy                                                     *)
(*****************************************************************************)
fun MK_DEF_EQ th =
 if is_eq(concl(SPEC_ALL th))
  then foldl
        (fn (v,th) => RIGHT_CONV_RULE BETA_CONV (AP_THM th v))
        th
        (fst(strip_abs(rhs(concl(SPEC_ALL th)))))
  else th;

(*****************************************************************************)
(* Conversion                                                                *)
(*                                                                           *)
(* ``(\x1 ... xn. t) y1 .. yn``                                              *)
(* -->                                                                       *)
(* |- (\x1 ... xn. t) y1 .. yn = let (x1,...,xn) = (y1,...,yn) in t          *)
(*                                                                           *)
(*****************************************************************************)
fun LET_INTRO_CONV tm =
 let val (opr, args) = strip_comb tm
     val (params,bdy) = strip_abs opr
     val param_arg_list = filter
                           (fn (v1,v2) => not(aconv v1 v2))
                           (zip params args)
     val let_tm = ``LET
                     ^(mk_pabs(list_mk_pair params,bdy))
                     ^(list_mk_pair args)``
     val th1 = DEPTH_CONV (REWR_CONV LET_THM) let_tm
     val th2 = DEPTH_CONV BETA_CONV tm
     val th3 = DEPTH_CONV PairRules.PBETA_CONV(rhs(concl th1))
 in
  GSYM(TRANS(TRANS th1 th3)(GSYM th2))
 end;

(*****************************************************************************)
(* Flag to determine whether to introduce lets                               *)
(*****************************************************************************)
val let_flag = ref true;

(*****************************************************************************)
(* Rule to introduce let throughout a term                                   *)
(*****************************************************************************)
fun LET_INTRO th =
 if !let_flag
  then CONV_RULE (TRY_CONV(RHS_CONV(TOP_DEPTH_CONV LET_INTRO_CONV))) th
  else th;

(******************************************************************************
The method of converting a full ACL2 name pkg::sym to a HOL-friendly
name is as follows (see definition of create_hol_name below).

 1. First see if the ACL2 name already has a HOL name, and if so
    return it.

 2. Convert sym to a HOL name, say hol_sym, using the ML function
    acl2_name_to_hol_name (this function is described below).

 3. If hol_sym starts with a digit, then use acl2_name_to_hol_name
    to convert pkg to hol_pkg, then lengthen the name to
    (hol_pkg ^ "_" ^ hol_sym).

 4. Check to see if sym_name (or the lengthened name) is already used.
    If not it is the result.

 5. If hol_sym is in use and doesn't start with a digit, then see if
    (hol_pkg ^ "_" ^ hol_sym) is used, and if not return it. If it is
    in use an error report is printed and an exception raised.

 6. Record any names generated by steps above in acl2_names so
    the original names can be recovered.

The function acl2_name_to_hol_name converts a string s to a
HOL-friendly name as follows.

 1. Convert s to a list of characters and convert all letters
    to lower-case.

 2. Replace "-" by "_".

 3. Replace special characters by strings of letter characters
    using acl2_to_hol_char_map (defined below). Add an underscore
    "_" to separate special characters from all other characters.

We think these simple rules should be sufficient in practice, and if
they are not it's better to reconsider carefully what to do rather
than to have ugly looking names generated by more complicated rules
(this might change if the sufficiency assumption is badly wrong).
******************************************************************************)


(*****************************************************************************)
(* Map from ACL2 characters in names to lists of HOL-friendly characters.    *)
(*****************************************************************************)
val acl2_to_hol_char_map =
 [(#"="  , explode "equal"),
  (#"<"  , explode "less"),
  (#">"  , explode "greater"),
  (#"/"  , explode "slash"),
  (#"\\" , explode "backslash"),
  (#"?"  , explode "question"),
  (#"$"  , explode "dollar"),
  (#"!"  , explode "exclaim"),
  (#"*"  , explode "star"),
  (#"+"  , explode "plus"),
  (#":"  , explode "colon"),
  (#" "  , explode "space")];

(*****************************************************************************)
(* Check is a character is in the domain of acl2_to_hol_char_map.            *)
(*****************************************************************************)
fun isSpecial c = can (assoc c) acl2_to_hol_char_map;

(*****************************************************************************)
(* Convert a character to a list of HOL-friendly characters by applying      *)
(* acl2_to_hol_char_map. If the character is not in the domain of            *)
(* acl2_to_hol_char_map, then if it is #"-" it is converted to #"_" else     *)
(* it is converted to lower case.                                            *)
(*****************************************************************************)
fun acl2_char_to_hol_chars c =
 if Char.isAlphaNum c
  then [Char.toLower c] else
 if c = #"-" then [#"_"]
  else assoc c acl2_to_hol_char_map handle HOL_ERR _ => [c];

fun acl2_chars_to_hol_chars [] = []
 |  acl2_chars_to_hol_chars [c] = acl2_char_to_hol_chars c
 |  acl2_chars_to_hol_chars (c1::(cl as (c2::_))) =
     if (isSpecial c1 orelse isSpecial c2)
        andalso not(c1 = #"-") andalso not(c2 = #"-")
      then acl2_char_to_hol_chars c1@(#"_"::acl2_chars_to_hol_chars cl)
      else acl2_char_to_hol_chars c1@acl2_chars_to_hol_chars cl;

(*****************************************************************************)
(* ACL2 to HOL name conversion function. Treats first character specially.   *)
(*****************************************************************************)
fun acl2_name_to_hol_name acl2_name =
 case assoc2 acl2_name (!acl2_names)
 of SOME (hol_name,_) => hol_name
 |  NONE              => implode(acl2_chars_to_hol_chars(explode acl2_name));

(*****************************************************************************)
(* Create a HOL-friendly name from a full ACL2 name and remember it in       *)
(* acl2_names. No effect on names unchanged by acl2_name_to_hol_name.        *)
(*                                                                           *)
(* The package name is eliminated unless it's needed to disambiguate HOL     *)
(* names (e.g. if the symbol symbol name occurs with two package names).     *)
(*****************************************************************************)
fun create_hol_name acl2_name =
 if acl2_name = acl2_name_to_hol_name acl2_name
  then acl2_name
  else
   let val (pkg_name,sym_name) = split_acl2_name acl2_name
       val hol_pkg_name = acl2_name_to_hol_name pkg_name
       val hol_sym_name = acl2_name_to_hol_name sym_name
       val long_hol_name = (hol_pkg_name ^ "_" ^ hol_sym_name)
       val fst_char = hd(explode hol_sym_name)
   in
   if Char.isDigit fst_char
    then
    (case (assoc1 long_hol_name (!acl2_names))
     of SOME(_,acl2_name')
        => if acl2_name = acl2_name'
            then long_hol_name
            else (print "\"";
                  print long_hol_name;
                  print "\" is the name of \"";
                  print acl2_name';
                  print "\"\nso can't use it to name \"";
                  print acl2_name; print "\"\n";
                  err "create_hol_name" "name already in use (case 1)")
     |  NONE
        => (acl2_names := (long_hol_name, acl2_name)::(!acl2_names);
            long_hol_name)
    )
    else
    (case (assoc1 hol_sym_name (!acl2_names))
     of SOME(_,acl2_name')
        => if acl2_name = acl2_name'
            then hol_sym_name
            else
            (case (assoc1 long_hol_name (!acl2_names))
               of SOME(_,acl2_name'')
                  => if acl2_name = acl2_name''
                      then long_hol_name
                      else (print "\"";
                            print hol_sym_name;
                            print "\" is the name of \"";
                            print acl2_name';
                            print "\"\nso can't use it to name \"";
                            print acl2_name; print "\"\n";
                            print "\"";
                            print long_hol_name;
                            print "\" is the name of \"";
                            print acl2_name'';
                            print "\"\nso can't use it to name \"";
                            print acl2_name; print "\"\n";
                            err "create_hol_name" "name already in use (case 2)")
               |  NONE
                  => (acl2_names := (long_hol_name, acl2_name)::(!acl2_names);
                      long_hol_name)
            )
     |  NONE
        => (acl2_names := (hol_sym_name, acl2_name)::(!acl2_names);
            hol_sym_name)
    )
   end;

(*****************************************************************************)
(* ML datatype to represent HOL tems and other data (e.g. names) of          *)
(* events imported from ACL2                                                 *)
(*                                                                           *)
(* A defun contains a defining equation: ``!x1 ... xn. f x1 ... xn = e``     *)
(* (the universal quantification may be partial or absent)                   *)
(*                                                                           *)
(* A defaxiom or defthm consists of a name and a term.                       *)
(*                                                                           *)
(* A mutual represents MUTUAL-RECURSION and is a defining term (normally a   *)
(* conjunction of universally quantified equations) suitable for processing  *)
(* by Define.                                                                *)
(*                                                                           *)
(* An encap represents ENCAPSULATE and is a pair comprising the list of      *)
(* names of the events specifying the functions being introduced and the     *)
(* defining term (normally an existential quantification) suitable for       *)
(* processing by new_specification.                                          *)
(*****************************************************************************)
datatype acl2def =
   defun    of term
 | defaxiom of string * term
 | defthm   of string * term
 | mutual   of term
 | encap    of (string list) * term;

(*****************************************************************************)
(* Strip ``|=`` from defthms and defaxioms                                   *)
(*****************************************************************************)
fun dest_ax_or_thm conc =
 let val (con,tm) = dest_comb conc
     val _ = if not(is_const con andalso (fst(dest_const con) = "|="))
               then(print_term conc;
                    print " should have form |= ...\n";
                    err "dest_ax_or_thm" "missing |=")
               else ()
 in
  tm
 end;

(*****************************************************************************)
(* "s1 s2 ... sn" |--> ["s1","s2",...,"sn"] (split at spaces)                *)
(*****************************************************************************)
val split_at_spaces = String.tokens (fn c => c = #" ");

(*****************************************************************************)
(* Convert a theorem obtained by slurping in ACL2 to an acl2def option.      *)
(* Used for reproving ACL2 imports inside HOL and for round-trip printing.   *)
(*****************************************************************************)
local
exception fail_for_mapfilter
in
fun dest_acl2_thm th =
 let val (asl, conc) = dest_thm(SPEC_ALL th)
     val _ = if not(asl = [])
               then(print_thm th;
                    print "\n"; print"should not have any assumptions\n";
                    err "dest_acl2_thm" "assumptions not allowed")
               else ()
     val tg = tag th
     val (tgl1,tgl2) = Tag.dest_tag tg
     val stgl = mapfilter
                 (fn s =>
                   let val (s1,s2) = split_tag s
                   in
                    if mem s1 ["DEFUN","DEFAXIOM","DEFTHM",
                               "MUTUAL-RECURSION","ENCAPSULATE"]
                     then (s1,s2)
                     else raise fail_for_mapfilter
                   end)
                 tgl1
 in
 if length stgl > 1
  then (print_thm th;
        print " has more than one ACL2 def tags!\n";
        err "dest_acl2_thm" "more than one ACL2 tag") else
  if null stgl
   then NONE
   else case (fst(hd stgl))
        of "DEFUN"
             => SOME(defun conc)
        |  "DEFAXIOM"
             => SOME(defaxiom(snd(hd stgl), dest_ax_or_thm conc))
        |  "DEFTHM"
             => SOME(defthm(snd(hd stgl), dest_ax_or_thm conc))
        |  "MUTUAL-RECURSION"
             => SOME(mutual conc)
        |  "ENCAPSULATE"
             => SOME(encap(split_at_spaces(snd(hd stgl)), conc))
        |  _ => NONE
 end
end;

(*****************************************************************************)
(* Convert a hol theorem to a defthm                                         *)
(*****************************************************************************)
fun thm_to_defthm(name,th) =
 defthm  (name, dest_ax_or_thm(concl(SPEC_ALL th)));

(*****************************************************************************)
(* Extraxt content from an option                                            *)
(*****************************************************************************)
fun dest_option (SOME x) = x
 |  dest_option NONE     = err "dest_option" "NONE";

(*****************************************************************************)
(* ``PKG::SYM`` |--> create_hol_name "PKG::SYM"                              *)
(*****************************************************************************)
fun clean_acl2_var tm =
 if is_var tm
  then let val (s,ty) = dest_var tm
           val hol_name = create_hol_name s
       in
        mk_var(hol_name, ty)
       end
  else tm;

(*****************************************************************************)
(* Clean all the free variables in a term                                    *)
(*****************************************************************************)
fun clean_acl2_term tm =
 subst (map (fn v => v |-> clean_acl2_var v) (free_vars tm)) tm;

(*****************************************************************************)
(* Clean all the free variables in a theorem                                 *)
(*****************************************************************************)
fun CLEAN_ACL2_FREES th =
 INST (map (fn v => v |-> clean_acl2_var v) (thm_frees th)) th;

(*****************************************************************************)
(* Conversion to clean a bound variable of an abstraction                    *)
(*****************************************************************************)
fun CLEAN_ACL2_ALPHA_CONV tm =
 let val (v,bdy) = dest_abs tm
     val (vname,vty) = dest_var v
     val hol_vname = create_hol_name vname
 in
  if hol_vname = vname
   then ALL_CONV tm
   else ALPHA_CONV (mk_var(hol_vname, vty)) tm
 end;

(*****************************************************************************)
(* Conversion to clean all bound variables in a term                         *)
(*****************************************************************************)
val CLEAN_ACL2_BOUND_CONV = DEPTH_CONV CLEAN_ACL2_ALPHA_CONV;

(*****************************************************************************)
(* Rule to clean all variables in a theorem                                  *)
(*****************************************************************************)
val CLEAN_ACL2_VARS =
 LET_INTRO o CLEAN_ACL2_FREES o CONV_RULE CLEAN_ACL2_BOUND_CONV;

(*****************************************************************************)
(*  deftm(defun tm)        = tm                                              *)
(*  deftm(defthm(_, tm))   = tm                                              *)
(*  deftm(defaxiom(_, tm)) = tm                                              *)
(*****************************************************************************)
fun deftm(defun tm)        = tm
 |  deftm(defthm(_, tm))   = tm
 |  deftm(defaxiom(_, tm)) = tm
 |  deftm _                = err "deftm" "bad arg";

(*****************************************************************************)
(* ``!v1...vn. f v1 ... vn = tm`` |--> f                                     *)
(*****************************************************************************)
fun get_defined tm = fst(strip_comb(lhs(spec_all tm)));

(*****************************************************************************)
(* defun ``!v1...vn. f v1 ... vn = tm`` |--> f                               *)
(* fails on non-defuns                                                       *)
(*****************************************************************************)
exception get_defun_fun_fail;
fun get_defun_fun (defun tm) = get_defined tm
 |  get_defun_fun _ = raise get_defun_fun_fail;

(*****************************************************************************)
(*  defname(defun ``!x1 ... xn. f x1 ... xn = t,``)  = f                     *)
(*  defname(defthm(nam, _))   = nam                                          *)
(*  defname(defaxiom(nam, _)) = nam                                          *)
(*****************************************************************************)
fun defname(defun tm)        = get_name(get_defined tm)
 |  defname(defthm(nam,_))   = nam
 |  defname(defaxiom(nam,_)) = nam
 |  defname _                = err "defname" "bad arg";

(*****************************************************************************)
(* mk_sexp_fun_ty n |--> ``:sexp -> ... -> sexp -> sexp`` (n arguments)      *)
(*****************************************************************************)
fun mk_sexp_fun_ty n =
 if n = 0 then ``:sexp`` else ``:sexp -> ^(mk_sexp_fun_ty(n-1))``;

(*****************************************************************************)
(* mk_closed_event vl tm |--> ``!v1 ... vn. tm``                             *)
(*                                                                           *)
(* where v1,...,vn are the free variables in tm not in vl                    *)
(*****************************************************************************)
fun mk_closed_event vl tm = list_mk_forall(subtract(free_vars tm)vl, tm);

(*****************************************************************************)
(* mk_acl2def converts an ML representation of an ACL2 event into an         *)
(* equivalent hol acl2def specification                                      *)
(*                                                                           *)
(* (defun nam (x1 ... xm) bdy)                                               *)
(* |-->                                                                      *)
(* defun("nam", ``!x1 ... xm. nam x1 ..., xm = bdy``)                        *)
(*                                                                           *)
(* (defthm nam bdy)                                                          *)
(* |-->                                                                      *)
(* defthm("nam", ``|= tm``)                                                  *)
(*                                                                           *)
(* (defaxiom nam bdy)                                                        *)
(* |-->                                                                      *)
(* defaxiom("nam", ``|= tm``)                                                *)
(*                                                                           *)
(* (mutual-recursion d1 ... dn)                                              *)
(* |-->                                                                      *)
(* mutual ``^(deftm(mk_acl2def d1)) /\ ... /\ ^(deftm(mk_acl2def dn))``      *)
(*                                                                           *)
(* (encapsulate ((v1 ... ) ... (vm ... )) e1 ... en)                         *)
(* |-->                                                                      *)
(* encap                                                                     *)
(*  ([``n1``,...,``nm``],                                                    *)
(*   ``?v1 ... vm.                                                           *)
(*      ^(deftm(mk_acl2def e1)) /\ ... /\ ^(deftm(mk_acl2def en))``)         *)
(*                                                                           *)
(* where n1,...,nm are the names of the events introducing v1,...,vm,        *)
(* respectively                                                              *)
(*****************************************************************************)
fun mk_acl2def d =
 if is_mldefun d
  then
   let val (nam,params,bdy) = dest_mldefun d
       val param_vars = map param_to_var params
       val bdy_tm = mlsexp_to_term bdy
       val tm = list_mk_fun(param_vars, bdy_tm)
       val ty = type_of tm
       val unbound_vars =
            subtract (free_vars bdy_tm) (name_to_var nam ty :: param_vars)
       val _ = if null unbound_vars
                then ()
                else print("Warning: "
                           ^ snd(dest_mlsym nam)
                           ^ " has unbound free variables\n")

       val sym_name = mlsym_to_string nam
       val newvar = mk_var(sym_name,ty)
       val defun_tm = list_mk_forall(param_vars, mk_def_eq(mk_eq(newvar,tm)))
   in
    defun(mk_closed_event [newvar] defun_tm)
   end else
 if is_mldefun_sk d
  then
   let val (nam,params,quant,qvars,bdy) = dest_mldefun_sk d
       val param_vars = map param_to_var params
       val quant_vars = map param_to_var qvars
       val quant_bdy =  ``|= ^(mlsexp_to_term bdy)``
       val quant_tm =
            if quant = ml_forall
             then list_mk_forall(quant_vars, quant_bdy) else
            if quant = ml_exists
             then list_mk_exists(quant_vars, quant_bdy)
             else err "mk_acl2def" (snd(dest_mlsym quant) ^ ": bad quantifier")
       val tm = list_mk_fun(param_vars, ``bool_to_sexp ^quant_tm``)
       val ty = type_of tm
       val unbound_vars =
            subtract (free_vars quant_tm) (name_to_var nam ty :: param_vars)
       val _ = if null unbound_vars
                then ()
                else print("Warning: "
                           ^ snd(dest_mlsym nam)
                           ^ " has unbound free variables\n")
       val sym_name = mlsym_to_string nam
       val newvar = mk_var(sym_name,ty)
       val defun_tm = list_mk_forall(param_vars, mk_def_eq(mk_eq(newvar,tm)))
   in
    defun(mk_closed_event [newvar] defun_tm)
   end else
 if is_mldefthm d
  then
   let val (nam,bdy) = dest_mldefthm d
       val tm = mlsexp_to_term bdy
       val ty = type_of tm
       val sym_name = mlsym_to_string nam
   in
    defthm(sym_name, gen_all ``|= ^tm``)
   end else
 if is_mldefaxiom d
  then
   let val (nam,bdy) = dest_mldefaxiom d
       val tm = mlsexp_to_term bdy
       val ty = type_of tm
       val sym_name = mlsym_to_string nam
   in
    defaxiom(sym_name, gen_all ``|= ^tm``)
   end else
 if is_mlmutual d
  then
   let val dl = dest_mlmutual d
       val names = map (mlsym_to_string o #1 o dest_mldefun) dl
   in
    mutual(gen_all(list_mk_conj(map (deftm o mk_acl2def) dl)))
   end else
 if is_mlencap d
  then
   let val (sigl,dl) = dest_mlencap d
       val sigll = map dest_mlsexp_list sigl
       val sig_vars =
            map
             (fn l =>
               mk_var
                (mlsym_to_string(hd l),
                 mk_sexp_fun_ty(length(dest_mlsexp_list(hd(tl l))))))
             sigll
       val eventl = map mk_acl2def dl
       val defunl = mapfilter get_defun_fun eventl
       val extended_sig_vars = union sig_vars defunl
       val names = map defname eventl
       val event_tms =
            map (mk_closed_event extended_sig_vars o spec_all o deftm) eventl
       val spec_body = list_mk_exists(extended_sig_vars,list_mk_conj event_tms)
   in
    encap(names,gen_all spec_body)
   end
  else err "mk_acl2def" "badly formed mldef";

(*****************************************************************************)
(* Convert a list of character code to a string.                             *)
(* Used in ML generated from ACL2 by a2ml.                                   *)
(*****************************************************************************)
val chars_to_string = implode o (map chr);

(*****************************************************************************)
(* ["s1","s2",...,"sn"] |--> "s1 s2 ... sn" (strings separated by spaces)    *)
(*****************************************************************************)
fun concat_with_spaces []      = ""
 |  concat_with_spaces [s]     = s
 |  concat_with_spaces (s::sl) = s ^ " " ^ concat_with_spaces sl;

(*****************************************************************************)
(* Get list of things being defined by a mutual recursion                    *)
(*****************************************************************************)
val get_defined_list = map get_defined o strip_conj o spec_all;

(*****************************************************************************)
(* Space-separated concatenation of names of defuns in a mutual-recursion    *)
(*****************************************************************************)
val mk_mutual_name = concat_with_spaces o map get_name o get_defined_list;

(*****************************************************************************)
(* Print an acl2def                                                          *)
(*****************************************************************************)
fun print_acl2def out (defun tm) =
     (out "; Defun:    "; out(get_name(get_defined tm)); out "\n";
      print_mlsexp out (deftm_to_mlsexp_defun(spec_all tm));
      out "\n\n")
 |  print_acl2def out (defaxiom(nam,tm)) =
     (out "; Defaxiom: "; out nam; out "\n";
      print_mlsexp out
       (mk_mlsexp_list
         [mldefaxiom,
          string_to_mlsym nam,
          term_to_mlsexp(spec_all tm)]);
      out "\n\n")
 |  print_acl2def out (defthm(nam,tm)) =
     (out "; Defthm:   "; out nam; out "\n";
      print_mlsexp out
       (mk_mlsexp_list
         [mldefthm,
          string_to_mlsym nam,
          term_to_mlsexp(spec_all tm)]);
      out "\n\n")
 |  print_acl2def out (mutual tm) =
     (out "; Mutual-Recursion "; out (mk_mutual_name tm); out "\n";
      out "(MUTUAL-RECURSION\n\n";
      map (print_acl2def out o defun) (strip_conj tm);
      out ")\n\n")
 |  print_acl2def out (encap(sl,tm)) = err "print_acl2def" "encap not yet supported";
(*
     (out "; Encapsulate\n";
      map (print_acl2def out o defthm) (strip_conj(snd(strip_exists tm)));
      out "\n");
*)

(*****************************************************************************)
(* Convert a preterm to a string (used for inputting ACL2)                   *)
(*****************************************************************************)
local
fun drop_until_close [] = []              (* drop chars until comment closes *)
 |  drop_until_close (#"*" :: #")" :: l) = l
 |  drop_until_close (c :: l) =  drop_until_close l
fun strip_comments [] = []                                (* remove comments *)
 |  strip_comments (#"(" :: #"*" :: l) = strip_comments(drop_until_close l)
 |  strip_comments (c :: l) =  c :: strip_comments l
fun strip_loc s = implode(strip_comments(explode s))
fun unQUOTE(QUOTE s) = s                                   (* QUOTE s |--> s *)
 |  unQUOTE _ = err "unQUOTE" "not applied to a QUOTE"
in
val preterm_to_string =
 foldr (fn(q,sl) => strip_loc(unQUOTE (q:term frag)) ^ "\n" ^ sl) ""
end;

(*****************************************************************************)
(* Absolute path of acl2 directory                                           *)
(*****************************************************************************)
val acl2_path = ref(Globals.HOLDIR ^ "/examples/acl2");

(*****************************************************************************)
(* Location of a2ml.csh tool for converting ACL2 files to ML files           *)
(*****************************************************************************)
val a2ml = ((!acl2_path) ^ "/lisp/a2ml.csh");

(*****************************************************************************)
(* Location of  pprint-file.csh. tool for pretty-printing ACL2 files         *)
(*****************************************************************************)
val pp = ((!acl2_path) ^ "/lisp/pprint-file.csh");

(*****************************************************************************)
(* Reference into which mlsexp generated by a2ml is put                      *)
(*****************************************************************************)
val acl2_list_ref = ref([] : mlsexp list);

(*****************************************************************************)
(* Wrapper around mk_oracle_thm.                                             *)
(* Saves strings used to create tags (now strings) in acl2_tags.             *)
(*****************************************************************************)
val acl2_tags = ref([]: (string*(string*string))list);

fun mk_acl2_thm defty acl2_name deftm =
 let val tg = defty ^ " " ^ acl2_name
 in
 (acl2_tags := (tg,(defty,acl2_name)) :: (!acl2_tags);
  mk_oracle_thm tg ([], deftm))
 end;

(*****************************************************************************)
(* Sequentially process, install and save the contents of acl2_list_ref:     *)
(*                                                                           *)
(* 1. declare constants in defuns, then make definition using mk_oracle_thm; *)
(*                                                                           *)
(* 2. declare HOL-friendly names (declare_names) using names generated       *)
(*    with create_hol_name.                                                  *)
(*                                                                           *)
(* 3. create theorems using mk_oracle_thm then save them with a HOL-friendly *)
(*    name with suffix "_defun", "_axiom", "_thm", "_mutual" or "_encap"     *)
(*****************************************************************************)
fun install(defun tm) =
     let val opr = get_defined tm
         val (opr_name,opr_ty) = dest_var opr
         val _ = if not(null(Term.decls opr_name))
                  then (print "\"";
                        print opr_name;
                        print "\" can only be defined once\n";
                        err "install" "repeated defun event")
                  else ()
         val (pkg_name,sym_name) = split_acl2_name opr_name
         val hol_name = create_hol_name opr_name
         val new_hol_name =
              (if null(Term.decls hol_name) then "" else "acl2_") ^ hol_name
         val _ = new_constant(opr_name,opr_ty)
         val _ = declare_names(opr_name,new_hol_name)
         val con = mk_const(opr_name,opr_ty)
         val newtm = subst[opr |-> con]tm
         val save_name = hol_name ^ "_defun"
         val defun_thm =
              save_thm
               (save_name, CLEAN_ACL2_VARS(mk_acl2_thm "DEFUN" opr_name newtm))
     in
      (save_name,defun_thm)
     end
 |  install(defaxiom(acl2_name, tm)) =
     let val (pkg_name,sym_name) = split_acl2_name acl2_name
         val hol_name = create_hol_name acl2_name
         val save_name = hol_name ^ "_axiom"
         val defaxiom_thm =
              save_thm
               (save_name, CLEAN_ACL2_VARS(mk_acl2_thm "DEFAXIOM" acl2_name tm))
     in
      (save_name,defaxiom_thm)
     end
 |  install(defthm(acl2_name, tm)) =
     let val (pkg_name,sym_name) = split_acl2_name acl2_name
         val hol_name = create_hol_name acl2_name
         val save_name = hol_name ^ "_thm"
         val defthm_thm =
              save_thm
               (save_name,
                CLEAN_ACL2_VARS(mk_acl2_thm "DEFTHM" acl2_name tm))
     in
      (save_name,defthm_thm)
     end
 | install(mutual tm) =
     let val tms = get_defined_list tm
         val opr_name_ty_list = map dest_var tms
         val acl2_name = mk_mutual_name tm
         val hol_names = map (create_hol_name o fst) opr_name_ty_list
         val new_hol_names =
              map
               (fn tm => (if null(Term.decls tm) then "" else "acl2_") ^ tm)
               hol_names
         val _ = map new_constant opr_name_ty_list
         val _ = map2
                  (fn (nam,ty) => fn new_nam => declare_names(nam,new_nam))
                  opr_name_ty_list
                  new_hol_names
         val con_list = map mk_const opr_name_ty_list
         val newtm =
              subst
               (map2 (fn opr => fn con => (opr |-> con)) tms con_list)
               (spec_all tm)
         val hol_name = create_hol_name acl2_name
         val save_name = hol_name ^ "_mutual"
         val defthm_thm =
              save_thm
               (save_name,
                CLEAN_ACL2_VARS (mk_acl2_thm "MUTUAL-RECURSION" acl2_name newtm))
     in
      (save_name,defthm_thm)
     end
 |  install(encap(sl,bdy)) =
     let val (tms,tm) = strip_exists bdy
         val opr_name_ty_list = map dest_var tms
         val acl2_name = concat_with_spaces(map get_name tms)
         val hol_names = map (create_hol_name o fst) opr_name_ty_list
         val new_hol_names =
              map
               (fn tm => (if null(Term.decls tm) then "" else "acl2_") ^ tm)
               hol_names
         val _ = map new_constant opr_name_ty_list
         val _ = map2
                  (fn (nam,ty) => fn new_nam => declare_names(nam,new_nam))
                  opr_name_ty_list
                  new_hol_names
         val con_list = map mk_const opr_name_ty_list
         val newtm =
              subst
               (map2 (fn opr => fn con => (opr |-> con)) tms con_list)
               tm
         val hol_name = create_hol_name acl2_name
         val save_name = hol_name ^ "_encap"
         val defthm_thm =
              save_thm
               (save_name,
                CLEAN_ACL2_VARS(mk_acl2_thm "ENCAPSULATE" acl2_name newtm))
     in
      (save_name,defthm_thm)
     end;

(*****************************************************************************)
(* Get kind of acl2def                                                       *)
(*****************************************************************************)
fun dest_acl2def (defun tm)      = ("DEFUN",get_name(get_defined tm))
 |  dest_acl2def (defaxiom(s,_)) = ("DEFAXIOM",s)
 |  dest_acl2def (defthm(s,_))   = ("DEFTHM",s)
 |  dest_acl2def (mutual tm)     = ("MUTUAL-RECURSION", mk_mutual_name tm)
 |  dest_acl2def (encap(sg,tm))  = ("ENCAPSULATE", concat_with_spaces sg);

(*****************************************************************************)
(* install plus a printing wrapper.                                          *)
(*****************************************************************************)
fun install_and_print a =
 let val (kind,name) = dest_acl2def a
     val _ = (print kind; print " "; print name; print "\n")
     val th = snd(install a)
     val _ = print_thm th
     val _ = print "\n\n"
 in
  th
 end;

(*****************************************************************************)
(* Union a list of lists                                                     *)
(*****************************************************************************)
fun union_flatten []      = []
 |  union_flatten (l::ll) = union l (union_flatten ll);;

(*****************************************************************************)
(* Gets the symbol names from an ML S-expression                             *)
(*****************************************************************************)
fun get_package_strings(mlsym(_,s)) = [s]
 |  get_package_strings(mlpair(p1,p2)) =
     union (get_package_strings p1) (get_package_strings p2)
 |  get_package_strings _  = [];

(*****************************************************************************)
(* Match a defun -- identity function if match succeeds                      *)
(*****************************************************************************)
fun match_defun full_acl2_name mlsexp =
 case mlsexp
 of (mlpair(mlsym("COMMON-LISP", "DEFUN"),
            mlpair(mlsym(pkg, sym), _)))
    => if (pkg, sym) = split_acl2_name full_acl2_name
        then mlsexp
        else raise err "match_defun"
                       ("bad match: (\"" ^ pkg ^ "\",\"" ^ sym ^ "\")")
 | _ => raise err "match_defun"
                  ("bad case match: " ^ full_acl2_name);

(*****************************************************************************)
(* Match a defaxiom -- identity function if match succeeds                   *)
(*****************************************************************************)
fun match_defaxiom full_acl2_name mlsexp =
 case mlsexp
 of (mlpair(mlsym("ACL2", "DEFAXIOM"),
            mlpair(mlsym(pkg, sym), _)))
    => if (pkg, sym) = split_acl2_name full_acl2_name
        then mlsexp
        else raise err "match_defaxiom"
                       ("bad match: (\"" ^ pkg ^ "\",\"" ^ sym ^ "\")")
 | _ => raise err "match_defaxiom"
                  ("bad case match: " ^ full_acl2_name);

(*****************************************************************************)
(* Match a defthm -- identity function if match succeeds                     *)
(*****************************************************************************)
fun match_defthm full_acl2_name mlsexp =
 case mlsexp
 of (mlpair(mlsym("ACL2", "DEFTHM"),
            mlpair(mlsym(pkg, sym), _)))
    => if (pkg, sym) = split_acl2_name full_acl2_name
        then mlsexp
        else raise err "match_defthm"
                       ("bad match: (\"" ^ pkg ^ "\",\"" ^ sym ^ "\")")
 | _ => raise err "match_defthm"
                  ("bad case match: " ^ full_acl2_name);

(*****************************************************************************)
(* Run a command returning true if it was successful.                        *)
(*    This is a nasty hack to ensure this file works in both MoscowML        *)
(*    and PolyML. My apologies.                                              *)
(*****************************************************************************)

fun run_with_test string =
    (Process.system (string ^ "&& touch success") ;
     can FileSys.remove "success");

(*****************************************************************************)
(* Print a list of ACL2 DEFUNs to a file defun-tmp.lisp,                     *)
(* then run a2ml to create defun-tmp.ml.                                     *)
(*****************************************************************************)

fun print_defuns_to_mlsexps ql =
 let val sl = map preterm_to_string ql
     val _ = print_lisp_file "defun-tmp" (fn pr => map pr sl)
in
  if not (run_with_test
         (a2ml ^ " defun-tmp.lisp defun-tmp.ml >& defun-tmp.log"))
   then (print "a2ml defun-tmp.lisp defun-tmp.ml: Failed\n";
         print "\n";
         err "print_defuns_to_mlsexs" "a2ml failed") else
   ()
 end;

(*****************************************************************************)
(* Create a script file for a theory named thy that contains ACL2 DEFUNs ql  *)
(* and hol names specified in an alist name_alist                            *)
(*****************************************************************************)
fun print_acl2_defun_script thy ql name_alist=
 let val outstr = TextIO.openOut("header-tmp.ml")
     fun out s = TextIO.output(outstr,s)
 in
  out("(* File created from HOL using print_acl2_defun_script on "
      ^ date() ^ " *)\n\n");
  out "open HolKernel Parse boolLib bossLib;\n";
  out "open stringLib complex_rationalTheory gcdTheory sexp sexpTheory;\n";
  out ("val _ = new_theory \"" ^ thy ^ "\";");
  out "\n\n";
  out "val name_alist = \n";
  out(string_pair_list_to_string name_alist);
  out ";\n\n";
  TextIO.flushOut outstr;
  TextIO.closeOut outstr;
  print_defuns_to_mlsexps ql;
  Process.system
   ("cat header-tmp.ml defun-tmp.ml end-boilerplate.ml > "
     ^ thy ^ "Script.sml")
 end;

(*****************************************************************************)
(* Read contents of acl2_list_ref (which should be set by slurping in        *)
(* ACL2 stuff), convert to tagged theorems and put the results in            *)
(* imported_acl2_theorems (an assignable variable).                          *)
(*                                                                           *)
(* The protocol for using this is:                                           *)
(*                                                                           *)
(*  use (Globals.HOLDIR ^ "/examples/acl2/...");                             *)
(*  load_imported_acl2_theorems();                                           *)
(*****************************************************************************)
val imported_acl2_theorems = ref([]:thm list);

fun load_imported_acl2_theorems () =
 let val acl2_package_strings =
      union_flatten
       (mapfilter
         (get_package_strings o match_defaxiom "ACL2::ACL2-PACKAGE")
         (!acl2_list_ref))
     val string_abbrev_count = length(!string_abbrevs)
 in
  print "Making string abbreviations ...\n";
  make_string_abbrevs acl2_package_strings;
  print(Int.toString(length(!string_abbrevs)-string_abbrev_count));
  print " new string abbreviations made\n";
  show_tags := true;
  print "read "; print(Int.toString(length(!acl2_list_ref))); print " defs\n";
  imported_acl2_theorems :=
   map (install_and_print o mk_acl2def) (!acl2_list_ref);
  print
   "Imported ACL2 stored in assignable variable imported_acl2_theorems.\n\n"
 end;

(*****************************************************************************)
(* Print imported imported_acl2_thms, assumed installed in theory named      *)
(* theory name, for round-trip test.                                         *)
(*****************************************************************************)
fun print_imported_acl2_theorems theory_name file_name =
 let val defs =
      mapfilter
       dest_option
       (map (dest_acl2_thm o snd) (theorems theory_name))
 in
  print_lisp_file
   file_name
   (fn out => map (print_acl2def out) defs)
 end;

fun print_thms_to_defthms name_thm_list file_name =
 let val defs = map thm_to_defthm name_thm_list
 in
  print_lisp_file
   file_name
   (fn out => map (print_acl2def out) defs)
 end;

(*****************************************************************************)
(* Add theory load time code to restore binding of acl2_simps in theory      *)
(*****************************************************************************)
fun save_acl2_simps () =
 adjoin_to_theory
 {sig_ps = NONE,
  struct_ps =
    SOME(fn ppstrm =>
          PP.add_string ppstrm
           ("val _ = (sexp.acl2_simps :="
            ^"  (!sexp.acl2_simps)@(Drule.CONJUNCTS ACL2_SIMPS));"))
 };

(*****************************************************************************)
(* Add theory load time code to restore binding of current_package in theory *)
(*****************************************************************************)
fun save_current_package() =
 adjoin_to_theory
 {sig_ps = NONE,
  struct_ps =
    SOME(fn ppstrm =>
          PP.add_string ppstrm
           ("val _ = sexp.set_current_package \""
            ^ (!current_package) ^ "\";"))
 };

(*****************************************************************************)
(* Add theory load time code to restore binding of acl2_names in theory.     *)
(*****************************************************************************)
fun save_acl2_names () =
 adjoin_to_theory
 {sig_ps = NONE,
  struct_ps =
    SOME(fn ppstrm =>
          PP.add_string ppstrm
           ("val _ = sexp.add_acl2_names " ^
            string_pair_list_to_string(!acl2_names) ^
            ";"))
 };


(*****************************************************************************)
(* Add theory load time code to restore binding of string_abbrevs in theory  *)
(*****************************************************************************)
fun save_string_abbrevs () =
 adjoin_to_theory
 {sig_ps = NONE,
  struct_ps =
    SOME(fn ppstrm =>
          PP.add_string ppstrm
           ("val _ = sexp.add_string_abbrevs " ^
            string_abbrevs_to_string(!string_abbrevs) ^
            ";\n\n"))
 };

(*****************************************************************************)
(* Save the acl2_simps, current_package, acl2_names, acl2_hol_names,         *)
(* string_abbrevs then export theory.                                        *)
(*****************************************************************************)
fun export_acl2_theory () =
 (save_thm("ACL2_SIMPS", LIST_CONJ(!acl2_simps));
  save_acl2_simps();
  save_current_package();
  save_acl2_names();
  save_string_abbrevs();
  export_theory());

(*****************************************************************************)
(* List of events processed. If two events with the same name occur,then the *)
(* second one is ignored.                                                    *)
(*****************************************************************************)
val event_names = ref([] : string list);

(*****************************************************************************)
(* Accumulate events and discard repeats                                     *)
(*****************************************************************************)
fun accumulate_discard_events [] = []
 |  accumulate_discard_events
     ((ev as (mlpair(_,mlpair(mlsym(_,ev_name),_)))) :: evl) =
      if mem ev_name (!event_names)
       then accumulate_discard_events evl
       else (event_names := ev_name :: (!event_names);
             ev :: accumulate_discard_events evl)
 | accumulate_discard_events (ev :: l) =
    err "accumulate_and_discard_events" "bad event";


end