1(*****************************************************************************) 2(* Various ML tools to support ACL2 in HOL including: *) 3(* *) 4(* 1. A printer from HOL to ACL2. *) 5(* *) 6(* 2. A converter from the ML representation of ACL2 defuns, *) 7(* defaxioms and defthms generated by Matt's tool a2ml.csh *) 8(* to HOL term. *) 9(*****************************************************************************) 10 11(*****************************************************************************) 12(* Ignore everything up to "END BOILERPLATE" *) 13(*****************************************************************************) 14 15(*****************************************************************************) 16(* START BOILERPLATE NEEDED FOR COMPILATION *) 17(*****************************************************************************) 18 19(****************************************************************************** 20* Load theories 21******************************************************************************) 22(* The commented out stuff below should be loaded in interactive sessions 23quietdec := true; 24map 25 load 26 ["intSyntax","pairSyntax","listSyntax","stringLib","stringSimps", 27 "rich_listTheory","pred_setLib"]; 28open pairSyntax listSyntax stringLib numLib stringSimps 29 rich_listTheory pred_setLib Defn; 30printDepth := 1000; 31printLength := 1000; 32Globals.checking_const_names := false; 33quietdec := false; 34*) 35 36structure sexp = 37struct 38 39(****************************************************************************** 40* Boilerplate needed for compilation: open HOL4 systems modules 41******************************************************************************) 42open HolKernel Parse boolLib bossLib; 43 44(****************************************************************************** 45* Open theories 46******************************************************************************) 47open intSyntax pairSyntax listSyntax stringLib numLib; 48 49(*****************************************************************************) 50(* END BOILERPLATE *) 51(*****************************************************************************) 52 53(*****************************************************************************) 54(* Print utility from Michael Norrish (may not end up being used): *) 55(* *) 56(* > Is there a way of redirecting output from print_term to a file? *) 57(* *) 58(* You need to turn an outstream (the thing you get back from a call to *) 59(* TextIO.openOut) into a ppstream. You could do this with *) 60(* *) 61(* fun mk_pp_from_out outstream = *) 62(* PP.mk_ppstream { consumer = (fn s => TextIO.output(outstream,s)), *) 63(* linewidth = 80, *) 64(* flush = (fn () => TextIO.flushOut outstream) } *) 65(* *) 66(* where I have chosen the linewidth arbitrarily. Then you would use the *) 67(* ppstream based pretty-printer Parse.pp_term. So a complete solution *) 68(* for outputting a single term to a given file would be *) 69(*****************************************************************************) 70fun mk_pp_from_out outstream = 71 PP.mk_ppstream { consumer = (fn s => TextIO.output(outstream,s)), 72 linewidth = 80, 73 flush = (fn () => TextIO.flushOut outstream) }; 74 75fun print_term_to_file fname term = let 76 val outstr = TextIO.openOut fname 77 val pps = mk_pp_from_out outstr 78in 79 Parse.pp_term pps term; 80 PP.flush_ppstream pps; 81 TextIO.closeOut outstr 82end; 83 84 85(*****************************************************************************) 86(* Swich off warning messages when defining types and constants with *) 87(* non-standard names (e.g. names originating from ACL2). *) 88(*****************************************************************************) 89val _ = (Globals.checking_const_names := false); 90 91(*****************************************************************************) 92(* Flag to determine if HOL_ERR exceptions are printed *) 93(*****************************************************************************) 94val print_err = ref false; 95 96(*****************************************************************************) 97(* Error reporting function (uses some HOL boilerplate I don't understand) *) 98(*****************************************************************************) 99fun err fn_name msg = 100 if !print_err 101 then Raise(mk_HOL_ERR "sexp" fn_name msg) 102 else raise(mk_HOL_ERR "sexp" fn_name msg); 103 104(*****************************************************************************) 105(* Global variable holding current package name. Initially "ACL2". *) 106(*****************************************************************************) 107val current_package = ref "ACL2"; 108 109(*****************************************************************************) 110(* Set value of current package *) 111(*****************************************************************************) 112fun set_current_package pname = 113 (current_package := pname); 114 115(*****************************************************************************) 116(* Global updateable list of ACL2 simplification theorems *) 117(*****************************************************************************) 118val acl2_simps = ref([]:thm list); 119 120(*****************************************************************************) 121(* Function to add a list of theorems to acl2_simps *) 122(*****************************************************************************) 123fun add_acl2_simps thl = (acl2_simps := (!acl2_simps) @ thl); 124 125(*****************************************************************************) 126(* |- ("T" = "NIL") = F -- shouldn't need to have to prove this explicitly! *) 127(*****************************************************************************) 128val T_NIL = EVAL ``"T" = "NIL"``; 129 130val _ = add_acl2_simps[T_NIL]; 131 132(*****************************************************************************) 133(* Tactics that simplifies with acl2_simps and other theorems supplied *) 134(* explicitly by the user *) 135(*****************************************************************************) 136fun ACL2_SIMP_TAC thl = RW_TAC list_ss ((!acl2_simps) @ thl) 137and ACL2_FULL_SIMP_TAC thl = FULL_SIMP_TAC list_ss ((!acl2_simps) @ thl); 138 139(*****************************************************************************) 140(* Global association list of pairs (hol_name, acl2_name). *) 141(*****************************************************************************) 142val acl2_names = 143 ref([("ACL2_PAIR", "COMMON-LISP::CONS")]:(string*string)list); 144 145(*****************************************************************************) 146(* Test if a name is already used *) 147(*****************************************************************************) 148fun is_acl2_name s = can (assoc s) (!acl2_names); 149 150(*****************************************************************************) 151(* Add a pair (hol_name, acl2_name) to acl2_names after checking that *) 152(* hol_name is not already used. *) 153(*****************************************************************************) 154fun add_acl2_name (hol_name, acl2_name) = 155 let val res = assoc1 hol_name (!acl2_names) 156 in 157 case res 158 of SOME(_,acl2_name') 159 => if acl2_name = acl2_name' 160 then () 161 else (print "\""; 162 print hol_name; 163 print "\" is the name of \""; 164 print acl2_name'; 165 print "\n\" so can't use it to name \""; 166 print acl2_name; print "\"\n"; 167 err "add_acl2_name" "name already in use") 168 | NONE 169 => (acl2_names := (hol_name, acl2_name) :: (!acl2_names)) 170 end; 171 172(*****************************************************************************) 173(* Function to add an entry to acl2_names *) 174(*****************************************************************************) 175fun add_acl2_names [] = () 176 | add_acl2_names (p::pl) = (add_acl2_name p; add_acl2_names pl); 177 178(*****************************************************************************) 179(* Print !acl2_names to a string (used in adjoin_to_theory). *) 180(* There may be a better way of doing this! *) 181(*****************************************************************************) 182local 183fun string_pair_list_to_string_aux [] = "" 184 | string_pair_list_to_string_aux [(hol,acl2)] = 185 ("(\"" ^ hol ^ "\",\"" ^ acl2 ^"\")") 186 | string_pair_list_to_string_aux ((hol,acl2)::pl) = 187 ("(\"" ^ hol ^ "\",\"" ^ acl2 ^"\")," ^ 188 string_pair_list_to_string_aux pl) 189in 190fun string_pair_list_to_string pl = 191 ("[" ^ string_pair_list_to_string_aux pl ^ "]") 192end; 193 194(*****************************************************************************) 195(* declare_names("acl2_name","hol_name") *) 196(* *) 197(* 1. Checks "acl2_name" is the name of exactly one constant. *) 198(* *) 199(* 2. Checks "hol_name" isn't an existing abbreviation. *) 200(* *) 201(* 3. Uses the HOL overloading mechanism to introduce "hol_name" *) 202(* as an alternative name for "acl2_name" ("hol_name" should be *) 203(* a valid HOL identifier name). *) 204(*****************************************************************************) 205fun declare_names (acl2_name,hol_name) = 206 let val hol_tml = Term.decls hol_name 207 val acl2_tml = Term.decls acl2_name 208 in 209 if null acl2_tml 210 then (print "no constant named: "; 211 print acl2_name; 212 print "\n"; 213 err "declare_names" "no term with acl2 name") else 214 if not(length acl2_tml = 1) 215 then (print "Warning -- there is more than one constant named: "; 216 print acl2_name; 217 print "\n") else 218 if not(length hol_tml = 0) 219 then (print "Warning -- there is already a constant named: "; 220 print hol_name; 221 print "\n") 222 else (add_acl2_names[(hol_name,acl2_name)]; 223 overload_on(hol_name,hd acl2_tml)) 224 end; 225 226(*****************************************************************************) 227(* ``!x1 ... xn. tm`` |--> tm *) 228(*****************************************************************************) 229val spec_all = snd o strip_forall; 230 231(*****************************************************************************) 232(* Three functions from KXS (modified by MJCG) to support non-standard names *) 233(*****************************************************************************) 234fun dest_hd_eqn eqs = 235 let val hd_eqn = if is_conj eqs then fst(dest_conj eqs) else eqs 236 val (lhs,rhs) = dest_eq (spec_all hd_eqn) 237 in (strip_comb lhs, rhs) 238 end; 239 240(* Version that raises an exception if type variables occur 241fun non_standard_name_defn name q = 242 let val absyn0 = Parse.Absyn q 243 val (qtm,_) = Defn.parse_absyn absyn0 244 val tyvars = type_vars_in_term qtm 245 val ((f,args),rhs) = dest_hd_eqn qtm 246 val (fname,fty) = dest_var f 247 val _ = if null tyvars 248 then () 249 else (print "Type variables in definition "; 250 print name; 251 print " of ``"; 252 print fname; print "`` "; 253 map (fn ty => (print_type ty; print " ")) tyvars; 254 print "\n"; 255 err "non_standard_name_defn" "type variables not allowed") 256 val qtm' = subst [f |-> mk_var(name,fty)] qtm 257 in 258 (fname, Defn.mk_defn fname qtm') 259 end; 260*) 261 262(* Automatically instantiate all type variables to ``:sexp`` *) 263fun non_standard_name_defn name q = 264 let val absyn0 = Parse.Absyn q 265 val (qtm,_) = Defn.parse_absyn absyn0 266 val ((f,args),rhs) = dest_hd_eqn qtm 267 val (fname,fty) = dest_var f 268 val qtm' = subst [f |-> mk_var(name,fty)] qtm 269 val tyvars = type_vars_in_term qtm' 270 val qtm'' = inst (map (fn ty => ty |-> ``:sexp``) tyvars) qtm' 271 in 272 (fname, Defn.mk_defn fname qtm'') 273 end; 274 275fun non_standard_nameDefine name q = 276 let val (hol_name,def) = non_standard_name_defn name q 277 in 278 ((hol_name, #1(TotalDefn.primDefine def)) 279 handle e => raise wrap_exn "ACL2 support" "xxDefine" e) 280 end; 281 282(*****************************************************************************) 283(* acl2Define "acl2_name" `(foo ... = ...) /\ ... ` does the following: *) 284(* *) 285(* 1. non_standard_nameDefine "acl2_name" `(foo ... = ...) /\ ... ` *) 286(* *) 287(* 2. adds the theorem resulting from the definition to acl2_simps *) 288(* *) 289(* 3. declare_names("acl2_name","hol_name") ("hol_name" is name of hol) *) 290(* *) 291(* 4. the definition theorem is returned *) 292(* *) 293(* Example: *) 294(* *) 295(* val stringp_def = *) 296(* acl2Define "COMMON-LISP::STRINGP" *) 297(* `(stringp(str x) = t) /\ (stringp _ = nil)`; *) 298(* *) 299(*****************************************************************************) 300fun acl2Define acl2_name q = 301 let val (hol_name,th) = non_standard_nameDefine acl2_name q 302 in 303 acl2_simps := (!acl2_simps) @ [th]; 304 declare_names(acl2_name,hol_name); 305 (print"\""; 306 print acl2_name; 307 print "\" defined with HOL name \""; 308 print hol_name; print "\"\n"); 309 th 310 end; 311 312(*****************************************************************************) 313(* Wrapper around mk_oracle_thm. *) 314(* Saves strings used to create tags (now strings) in acl2_tags. *) 315(*****************************************************************************) 316val acl2_tags = ref([]: (string*(string*string))list); 317 318fun mk_acl2_thm defty acl2_name deftm = 319 let val tg = defty ^ " " ^ acl2_name 320 in 321 (acl2_tags := (tg,(defty,acl2_name)) :: (!acl2_tags); 322 mk_oracle_thm tg ([], deftm)) 323 end; 324 325(*****************************************************************************) 326(* Create an axiomatic definition with tag ("acl2AxiomDefine" ^ acl2_name) *) 327(*****************************************************************************) 328fun acl2AxiomDefine acl2_name q = 329 let val absyn0 = Parse.Absyn q 330 val (qtm,_) = Defn.parse_absyn absyn0 331 val tyvars = type_vars_in_term qtm 332 val qtm' = inst (map (fn ty => ty |-> ``:sexp``) tyvars) qtm 333 val ((f,args),rhs) = dest_hd_eqn qtm' 334 val (hol_name,fty) = dest_var f 335 val _ = new_constant(acl2_name,fty) 336 val _ = declare_names(acl2_name,hol_name); 337 val qtm'' = subst [f |-> mk_const(acl2_name,fty)] qtm' 338 val dth = mk_acl2_thm "acl2AxiomDefine" acl2_name qtm'' 339 val _ = (acl2_simps := (!acl2_simps) @ [dth]) 340 in 341 print "Axiomatic definition has been stored under \""; 342 print (hol_name ^ "_def\".\n"); 343 print "\""; 344 print acl2_name; 345 print "\" axiomatically defined with HOL name \""; 346 print hol_name; print "\"\n"; 347 save_thm((hol_name ^ "_def"),dth) 348 end; 349 350(* 351val expt_def = 352 acl2AxiomDefine "COMMON-LISP::EXPT" 353 `expt r i = 354 itel 355 [(zip i,nat 1); (common_lisp_equal (fix r) (nat 0),nat 0); 356 (less (nat 0) i,mult r (expt r (add i (int ~1))))] 357 (mult (reciprocal r) (expt r (add i (nat 1))))`; 358 359val expt1_def = 360 acl2AxiomDefine "COMMON-LISP::EXPT1" 361 `expt1 r i = nil`; 362*) 363 364(*****************************************************************************) 365(* acl2_tgoal "acl2_name" `(foo ... = ...) /\ ... ` creates a termination *) 366(* goal for the recursive definition with acl2_name replacing foo. Example: *) 367(* *) 368(* acl2_tgoal "ACL2::TRUE-LISTP" *) 369(* `true_listp x = ite (consp x) (true_listp (cdr x)) (eq x nil)` *) 370(* *) 371(* *) 372(*****************************************************************************) 373fun acl2_tgoal acl2_name q = 374 let val (hol_name,def) = non_standard_name_defn acl2_name q 375 in 376 (print "Creating termination goal for "; 377 print acl2_name; 378 print " ("; print hol_name; print ")\n"; 379 Defn.tgoal def 380 handle e => Raise(wrap_exn "ACL2 support" "Hol_defn" e)) 381 end; 382 383(*****************************************************************************) 384(* acl2_defn "acl2_name" (`(foo ... = ...) /\ ... `, tac) uses tac to *) 385(* solve the termination goal for the recursive definition with acl2_name *) 386(* replacing foo. Makes the definition of acl2_name and then overloads foo *) 387(* on acl2_name. Example: *) 388(* *) 389(* val (true_listp_def,true_listp_ind) = *) 390(* acl2_defn "ACL2::TRUE-LISTP" *) 391(* (`true_listp x = ite (consp x) (true_listp (cdr x)) (eq x nil)`, *) 392(* WF_REL_TAC `measure sexp_size` *) 393(* THEN RW_TAC arith_ss [sexp_size_cdr]); *) 394(*****************************************************************************) 395fun acl2_defn acl2_name (q,tac) = 396 let val (hol_name,def) = non_standard_name_defn acl2_name q 397 val (def_th,ind_th) = 398 (Defn.tprove(def,tac) 399 handle e => Raise(wrap_exn "ACL2 support" "Defn.tgoal" e)) 400 in 401(*acl2_simps := (!acl2_simps) @ [def_th];*) 402 declare_names(acl2_name,hol_name); 403 save_thm((hol_name ^ "_def"),def_th); 404 save_thm((hol_name ^ "_ind"),ind_th); 405 (print"\""; 406 print acl2_name; 407 print "\" defined with HOL name \""; 408 print hol_name; print "\"\n"; 409 (def_th,ind_th)) 410 end; 411 412(*****************************************************************************) 413(* Generate date and time for making file timestamps *) 414(*****************************************************************************) 415fun date() = Date.fmt "%c" (Date.fromTimeLocal (Time.now ())); 416 417(*****************************************************************************) 418(* Create a output stream to a file called file_name.lisp, apply a printer *) 419(* to it and then flush and close the stream. *) 420(*****************************************************************************) 421fun print_lisp_file file_name printer = 422 let val outstr = TextIO.openOut(file_name ^ ".lisp") 423 fun out s = TextIO.output(outstr,s) 424 in 425 (out("; File created from HOL using print_lisp_file on " ^ date() ^ "\n\n"); 426 (* Add time stamp *) 427 (* out("(IN-PACKAGE \"ACL2\")\n\n"); *) 428 (* ACL2 initialisation (currently commented out at Matt's suggestion) *) 429 printer out; 430 TextIO.flushOut outstr; 431 TextIO.closeOut outstr) 432 end; 433 434(*****************************************************************************) 435(* Representation of s-expressions in ML *) 436(* *) 437(* Complex rational a/b + (p/q)i is constructed by mlnum("a","b","p","q"). *) 438(* Must use strings, as ML numerals are 32-bit! *) 439(* *) 440(* con mlchr = fn : char -> mlsexp *) 441(* con mlnum = fn : string * string * string * string -> mlsexp *) 442(* con mlpair = fn : mlsexp * mlsexp -> mlsexp *) 443(* con mlstr = fn : string -> mlsexp *) 444(* con mlsym = fn : string * string -> mlsexp *) 445(* *) 446(* Negative numbers are represented by prefixing the numerator with "-", *) 447(* so denominators b and q should be natural number numerals (0,1,2,...), *) 448(* and numerators a and p should be natural number numerals, possibly with *) 449(* a "-" prefix. Thus mlnum("1","-1","0","1") is invalid. *) 450(*****************************************************************************) 451datatype mlsexp = 452 mlsym of string * string 453 | mlstr of string 454 | mlchr of char 455 | mlnum of string * string * string * string 456 | mlpair of mlsexp * mlsexp; 457 458val mksym = curry mlsym 459and mkstr = mlstr 460and mkchr = mlchr o chr 461and mknum = fn numerator_x => 462 fn denominator_x => 463 fn numerator_y => 464 fn denominator_y => 465 mlnum(numerator_x,denominator_x,numerator_y,denominator_y) 466and mkpair = fn x => 467 fn y => 468 mlpair(x,y); 469 470(*****************************************************************************) 471(* Test and destructor for mlsym *) 472(*****************************************************************************) 473fun is_mlsym (mlsym(_,_)) = true 474 | is_mlsym _ = false; 475 476fun dest_mlsym (mlsym(sym_pac,sym_name)) = (sym_pac,sym_name) 477 | dest_mlsym _ = err "dest_mlsym" "not a sym"; 478 479(*****************************************************************************) 480(* Alternative name for mlstr used to indicate string originates from a *) 481(* list of characters sent from ACL2. *) 482(*****************************************************************************) 483val mk_chars_str = mlstr; 484 485(*****************************************************************************) 486(* Abbreviation for some symbols. *) 487(*****************************************************************************) 488val mlnil = mksym "COMMON-LISP" "NIL" 489val mlt = mksym "COMMON-LISP" "T" 490and mlquote = mksym "COMMON-LISP" "QUOTE" 491and mlcons = mksym "COMMON-LISP" "CONS" 492and mllambda = mksym "COMMON-LISP" "LAMBDA" 493and mldefun = mksym "COMMON-LISP" "DEFUN" 494and mldefun_sk = mksym "ACL2" "DEFUN-SK" 495and ml_forall = mksym "ACL2" "FORALL" 496and ml_exists = mksym "ACL2" "EXISTS" 497and mlinclude = mksym "ACL2" "INCLUDE-BOOK" 498and mlmutual = mksym "ACL2" "MUTUAL-RECURSION" 499and mlencap = mksym "ACL2" "ENCAP" 500and mldefaxiom = mksym "ACL2" "DEFAXIOM" 501and mldefthm = mksym "ACL2" "DEFTHM"; 502 503(*****************************************************************************) 504(* "tag_ty nam" |--> ("tag_ty","nam") *) 505(*****************************************************************************) 506val split_tag = 507 let 508 fun split_tag_chars acc [] = ([],rev acc) 509 | split_tag_chars acc (#" " :: l) = (rev acc,l) 510 | split_tag_chars acc (c :: l) = split_tag_chars (c :: acc) l 511 in 512 (implode ## implode) o split_tag_chars [] o explode 513end; 514 515(*****************************************************************************) 516(* "pkg::nam" |--> ("pkg","nam") *) 517(*****************************************************************************) 518val split_acl2_name = 519 let 520 fun split_acl2_name_chars acc [] = ([],rev acc) 521 | split_acl2_name_chars acc (#":" :: #":" :: l) = (rev acc,l) 522 | split_acl2_name_chars acc (c :: l) = split_acl2_name_chars (c :: acc) l 523 in 524 (implode ## implode) o split_acl2_name_chars [] o explode 525end; 526 527(*****************************************************************************) 528(* Lookup a string in acl2_names. If it corresponds to a full ACL2 name *) 529(* (with package and symbol name separated by "::") then return the ACL2 *) 530(* name. If it corresponds to an ACL2 name without a package name (which *) 531(* shouldn't happen), then add the current_package as package name. If *) 532(* the string isn't in acl2_names and is "ACL2_PAIR" then return *) 533(* mlsym("COMMON-LISP", "CONS"), otherwise split at "::" (or using *) 534(* current_package if no "::") and then use mlsym. *) 535(*****************************************************************************) 536fun string_to_mlsym s = 537 case assoc1 s (!acl2_names) 538 of SOME(_,acl2_name) 539 => let val (pkg,nam) = split_acl2_name acl2_name 540 in 541 mlsym(if pkg = "" then (!current_package) else pkg, nam) 542 end 543 | NONE 544 => if s = "ACL2_PAIR" 545 then mlcons 546 else let val (pkg,nam) = split_acl2_name s 547 in 548 mlsym(if pkg = "" then (!current_package) else pkg, nam) 549 end; 550 551(*****************************************************************************) 552(* Test for a proper list: (x1 . (x2 . ... . (xn . nil) ...)) *) 553(*****************************************************************************) 554fun is_mlsexp_proper_list (sym as mlsym(_,_)) = 555 (sym = mlnil) 556 | is_mlsexp_proper_list (mlpair(_,p)) = 557 is_mlsexp_proper_list p 558 | is_mlsexp_proper_list _ = false; 559 560(*****************************************************************************) 561(* Test for a proper list or an atom *) 562(*****************************************************************************) 563fun is_mlsexp_list (p as mlpair(_,_)) = is_mlsexp_proper_list p 564 | is_mlsexp_list _ = true; 565 566(*****************************************************************************) 567(* Destruct an ML s-expression list: *) 568(* (x1 . (x2 . ... (xn . nil) ...)) |--> [x1,x2,...,xn] *) 569(*****************************************************************************) 570fun dest_mlsexp_list (sym as mlsym(_,_)) = 571 if (sym = mlnil) then [] else [sym] 572 | dest_mlsexp_list (mlpair(p1,p2)) = 573 p1 :: dest_mlsexp_list p2 574 | dest_mlsexp_list p = [p]; 575 576(*****************************************************************************) 577(* [x1,...,xn] --> (mkpair x1 ... (mkpair xn mlnil) ... )) *) 578(*****************************************************************************) 579fun mk_mlsexp_list [] = mlnil 580 | mk_mlsexp_list (x::xl) = mlpair(x, mk_mlsexp_list xl); 581 582(*****************************************************************************) 583(* Test for a quote: (QUOTE x) *) 584(*****************************************************************************) 585fun is_mlquote (mlpair(x,mlpair(_,n))) = (x = mlquote) andalso (n = mlnil) 586 | is_mlquote _ = false; 587 588(*****************************************************************************) 589(* Extract body of a quote: (QUOTE x) |--> x *) 590(*****************************************************************************) 591fun dest_mlquote (mlpair(_,mlpair(x,_))) = x 592 | dest_mlquote _ = err "dest_mlquote" "bad argument"; 593 594(*****************************************************************************) 595(* Make an ML quote x |--> (QUOTE x) *) 596(*****************************************************************************) 597fun mk_mlquote x = mk_mlsexp_list[mlquote,x]; 598 599(*****************************************************************************) 600(* Test for a lambda: ((LAMBDA (x1 ... xm) bdy) (a1 ... an)) *) 601(*****************************************************************************) 602fun is_mllambda (mlpair(mlpair(x,mlpair(params,mlpair(bdy,n))),args)) = 603 (x = mllambda) andalso 604 is_mlsexp_list params andalso 605 is_mlsexp_list args andalso 606 is_mlsexp_list bdy andalso 607 (n = mlnil) 608 | is_mllambda _ = false; 609 610(*****************************************************************************) 611(* Lambda destructor: *) 612(* ((LAMBDA (x1 ... xm) bdy) (a1 ... an)) *) 613(* |--> *) 614(* ([x1, ..., xm], bdy, [a1, ..., an]) *) 615(* *) 616(*****************************************************************************) 617fun dest_mllambda (mlpair(mlpair(_,mlpair(params,mlpair(bdy,_))),args)) = 618 (dest_mlsexp_list params, bdy, dest_mlsexp_list args) 619 | dest_mllambda _ = 620 err "dest_mllambda" "bad argument"; 621 622(*****************************************************************************) 623(* Test for an include-book: (INCLUDE_BOOK book) *) 624(*****************************************************************************) 625fun is_mlinclude 626 (mlpair(x,mlpair(mlstr book,n))) = (x = mlinclude) 627 | is_mlinclude _ = false; 628 629(*****************************************************************************) 630(* Include-book destructor: (INCLUDE-BOOK book) |--> book *) 631(*****************************************************************************) 632fun dest_mlinclude b = 633 if is_mlinclude b 634 then case dest_mlsexp_list b 635 of [_,mlstr book] => book 636 | _ => err "dest_mlinclude" "bad case match" 637 else err "dest_mlinclude" "not an include-book"; 638 639(*****************************************************************************) 640(* Include-book Constructor: book |--> (INCLUDE-BOOK book) *) 641(*****************************************************************************) 642fun mk_mlinclude book = 643 mk_mlsexp_list [mlinclude, mlstr book]; 644 645(*****************************************************************************) 646(* Test for a defun: (DEFUN nam (x1 ... xn) bdy) *) 647(*****************************************************************************) 648fun is_mldefun 649 (mlpair(x,mlpair(mlsym(_,_),mlpair(params,mlpair(bdy,n))))) = 650 (x = mldefun) andalso 651 is_mlsexp_list params andalso 652 is_mlsexp_list bdy andalso 653 (n = mlnil) 654 | is_mldefun _ = false; 655 656(*****************************************************************************) 657(* Defun destructor: (DEFUN nam (x1 ... xn) bdy) |-->(nam,[x1,...,xn],bdy) *) 658(*****************************************************************************) 659fun dest_mldefun d = 660 if is_mldefun d 661 then case dest_mlsexp_list d 662 of [_,nam,params,bdy] 663 => (nam, dest_mlsexp_list params, bdy) 664 | _ 665 => err "dest_mldefun" "bad case match" 666 else err "dest_mldefun" "not a defun"; 667 668(*****************************************************************************) 669(* Defun Constructor: (nam,[x1,...,xn],bdy) |--> (DEFUN nam (x1 ... xn) bdy) *) 670(*****************************************************************************) 671fun mk_mldefun (nam, params, bdy) = 672 mk_mlsexp_list [mldefun, nam, mk_mlsexp_list params, bdy]; 673 674(*****************************************************************************) 675(* Test for a defun_sk: (DEFUN-SK nam (x1 ... xn) (QUANT (v1 ... vm) bdy)) *) 676(*****************************************************************************) 677fun is_mldefun_sk 678 (mlpair 679 (x, 680 mlpair 681 (mlsym(_,_), 682 mlpair 683 (params, 684 mlpair 685 (mlpair(quant, mlpair(qvars, mlpair(bdy,n1))), 686 n2))))) = 687 (x = mldefun_sk) andalso 688 is_mlsexp_list params andalso 689 (mem quant [ml_forall,ml_exists]) andalso 690 is_mlsexp_list qvars andalso 691 is_mlsexp_list bdy andalso 692 (n1 = mlnil) andalso 693 (n2 = mlnil) 694 | is_mldefun_sk _ = false; 695 696(*****************************************************************************) 697(* Defun destructor: *) 698(* (DEFUN-SK nam (x1 ... xn) (QUANT (v1 ... vm) bdy)) *) 699(* |--> *) 700(* (nam, [x1,...,xn], quant, qvars, bdy) *) 701(*****************************************************************************) 702fun dest_mldefun_sk d = 703 if is_mldefun_sk d 704 then case dest_mlsexp_list d 705 of [_,nam,params,quant_bdy] 706 => (case dest_mlsexp_list quant_bdy 707 of [quant,qvars,bdy] 708 => (nam, dest_mlsexp_list params, 709 quant, dest_mlsexp_list qvars, bdy) 710 | _ 711 => err "dest_mldefun_sk" "bad quant case match") 712 | _ 713 => err "dest_mldefun_sk" "bad case match" 714 else err "dest_mldefun" "not a defun"; 715 716(*****************************************************************************) 717(* Defun Constructor: *) 718(* (nam,[x1,...,xn],quant,qvars,bdy) *) 719(* |--> *) 720(* (DEFUN-SK nam (x1 ... xn) (quant qvars bdy)) *) 721(*****************************************************************************) 722fun mk_mldefun_sk (nam, params, quant, qvars, bdy) = 723 mk_mlsexp_list 724 [mldefun_sk, nam, mk_mlsexp_list params, 725 mk_mlsexp_list [quant, mk_mlsexp_list qvars, bdy]]; 726 727(*****************************************************************************) 728(* Test for a defaxiom: (DEFAXIOM nam bdy) *) 729(*****************************************************************************) 730fun is_mldefaxiom 731 (mlpair(x,mlpair(mlsym(_,_),mlpair(bdy,n)))) = 732 (x = mldefaxiom) andalso 733 is_mlsexp_list bdy andalso 734 (n = mlnil) 735 | is_mldefaxiom _ = false; 736 737(*****************************************************************************) 738(* Defaxiom destructor: (DEFAXIOM nam bdy) |--> (nam,bdy) *) 739(*****************************************************************************) 740fun dest_mldefaxiom 741 (mlpair(_,mlpair(nam,mlpair(bdy,_)))) = (nam, bdy) 742 | dest_mldefaxiom _ = err "dest_mldefaxiom" "bad argument"; 743 744(*****************************************************************************) 745(* Defaxiom constructor: (nam,bdy) |--> (DEFAXIOM nam bdy) *) 746(*****************************************************************************) 747fun mk_mldefaxiom(nam,bdy) = 748 mk_mlsexp_list [mldefaxiom, nam, bdy]; 749 750(*****************************************************************************) 751(* Test for a defthm: (DEFTHM nam bdy) *) 752(*****************************************************************************) 753fun is_mldefthm 754 (mlpair(x,mlpair(mlsym(_,_),mlpair(bdy,n)))) = 755 (x = mldefthm) andalso 756 is_mlsexp_list bdy andalso 757 (n = mlnil) 758 | is_mldefthm _ = false; 759 760(*****************************************************************************) 761(* Defthm destructor: (DEFTHM nam bdy) |--> (nam,bdy) *) 762(*****************************************************************************) 763fun dest_mldefthm 764 (mlpair(_,mlpair(nam,mlpair(bdy,_)))) = (nam, bdy) 765 | dest_mldefthm _ = err "dest_mldefthm" "bad argument"; 766 767(*****************************************************************************) 768(* Defthm constructor: (nam,bdy) |--> (DEFTHM nam bdy) *) 769(*****************************************************************************) 770fun mk_mldefthm(nam,bdy) = 771 mk_mlsexp_list [mldefthm, nam, bdy]; 772 773(*****************************************************************************) 774(* Test for a mutual: (MUTUAL-RECURSION d1 ... dn) *) 775(*****************************************************************************) 776fun is_mlmutual (mlpair(x, defs)) = (x = mlmutual) andalso is_mlsexp_list defs 777 | is_mlmutual _ = false; 778 779(*****************************************************************************) 780(* Mutual destructor: (MUTUAL-RECURSION d1 ... dn) |--> [d1, ..., dn] *) 781(*****************************************************************************) 782fun dest_mlmutual (mlpair(_, defs)) = dest_mlsexp_list defs 783 | dest_mlmutual _ = err "dest_mlmutual" "bad argument"; 784 785(*****************************************************************************) 786(* Test for a encap: (ENCAP acl2sig events) *) 787(*****************************************************************************) 788fun is_mlencap (mlpair(x, mlpair(acl2sig,events))) = 789 (x = mlencap) andalso is_mlsexp_list acl2sig 790 andalso is_mlsexp_list events 791 | is_mlencap _ = false; 792 793(*****************************************************************************) 794(* Mutual destructor: (ENCAP (s1 ... sm) (e1 ... en)) *) 795(* |--> *) 796(* ([s1, ..., sm],[e1,...,en]) *) 797(*****************************************************************************) 798fun dest_mlencap (mlpair(_, mlpair(acl2sig,events))) = 799 (dest_mlsexp_list acl2sig, dest_mlsexp_list events) 800 | dest_mlencap _ = err "dest_mlencap" "bad argument"; 801 802(*****************************************************************************) 803(* Test for ``nat n`` where n is a numeral *) 804(*****************************************************************************) 805fun is_nat tm = 806 is_comb tm andalso 807 (rator tm = ``nat``) andalso 808 is_numeral(rand tm); 809 810(*****************************************************************************) 811(* Convert ``nat n`` to "n" *) 812(*****************************************************************************) 813fun dest_nat tm = Arbnum.toString(dest_numeral(rand tm)); 814 815(*****************************************************************************) 816(* Test for ``n`` where n is an integer numeral *) 817(*****************************************************************************) 818fun is_integer tm = 819 is_comb tm andalso 820 (if rator tm = ``int_of_num:num->int`` (* $& overloaded on int_of_num *) 821 then is_numeral(rand tm) else 822 if rator tm = ``int_neg:int->int`` (* $~ overloaded on int_neg *) 823 then is_integer(rand tm) else 824 false); 825 826(*****************************************************************************) 827(* Test for ``int n`` where n is an integer numeral *) 828(*****************************************************************************) 829fun is_int tm = 830 is_comb tm andalso 831 (rator tm = ``int``) andalso 832 is_integer(rand tm); 833 834(*****************************************************************************) 835(* Convert an integer term numeral to a string: *) 836(* *) 837(* ``&d1d2...dn`` |--> "d1d2...dn" *) 838(* ``~& d1d2...dn`` |--> "-d1d2...dn" *) 839(*****************************************************************************) 840fun dest_integer tm = 841 let val (opr,args) = strip_comb tm 842 in 843 if opr = ``int_of_num:num->int`` andalso (tl args = []) 844 then (if is_numeral(hd args) 845 then Arbnum.toString(dest_numeral(hd args)) 846 else (print_term tm; 847 print " is not a non-negative integer numeral\n"; 848 err "dest_integer" "not a non-negative integer numeral")) 849 else (if opr = ``int_neg:int->int`` andalso (tl args = []) 850 then ("-" ^ dest_integer(hd args)) 851 else (print_term tm; 852 print " is not an integer numeral\n"; 853 err "dest_integer" "not an integer numeral")) 854 end; 855 856(*****************************************************************************) 857(* Convert ``int n`` to dest_integer ``n`` *) 858(*****************************************************************************) 859fun dest_int tm = dest_integer(rand tm); 860 861(*****************************************************************************) 862(* Replace initial "-" by "~" in a string (converts ACL2 representation of *) 863(* a negative integer to HOL representation). *) 864(*****************************************************************************) 865fun acl2_int_to_hol_int s = 866 let val chars = explode s 867 in 868 if not(null chars) andalso hd chars = #"-" 869 then implode(#"~" :: tl chars) 870 else s 871 end; 872 873(*****************************************************************************) 874(* Test whether a string is a natural number numeral *) 875(*****************************************************************************) 876fun is_num_string s = all Char.isDigit (explode s); 877 878 879(*****************************************************************************) 880(* Test whether a string is an integer numeral *) 881(*****************************************************************************) 882fun is_int_string s = 883 let val sl = explode s 884 in 885 null sl 886 orelse ((hd sl = #"-") andalso all Char.isDigit (tl sl)) 887 orelse all Char.isDigit sl 888 end; 889 890(*****************************************************************************) 891(* Test for ``cpx a b c d`` *) 892(*****************************************************************************) 893fun is_cpx tm = 894 let val (opr,args) = strip_comb tm 895 in 896 (opr = ``cpx``) 897 andalso (length args = 4) 898 andalso is_int_string(dest_integer(el 1 args)) 899 andalso is_num_string(dest_integer(el 2 args)) 900 andalso is_int_string(dest_integer(el 3 args)) 901 andalso is_num_string(dest_integer(el 4 args)) 902 end; 903 904(*****************************************************************************) 905(* ``cpx an ad bn bd`` |--> ("an", "ad", "bn", "bd") *) 906(* *) 907(* Negative numbers are represented with a prefixed "-" (e.g. "-3"). *) 908(*****************************************************************************) 909fun dest_cpx tm = 910 if is_cpx tm (* Probably redundant extra check included for safety *) 911 then 912 let val (_,args) = strip_comb tm 913 in 914 (dest_integer(el 1 args), 915 dest_integer(el 2 args), 916 dest_integer(el 3 args), 917 dest_integer(el 4 args)) 918 end 919 else (print_term tm; 920 print " is not a complex numeral\n"; 921 err "dest_cpx" "not a complex numeral"); 922 923(*****************************************************************************) 924(* mlsym(pkg,nam) |--> "pkg::nam" *) 925(*****************************************************************************) 926fun mlsym_to_string (sym as mlsym(pkg,nam)) = (pkg^"::"^nam) 927 | mlsym_to_string _ = err "mlsym_to_string" "non sym argument"; 928 929(*****************************************************************************) 930(* Association list of pairs of the form ("xyz", c), where c is a *) 931(* constant defined by |- c = "xyz". Used to avoid building terms with *) 932(* lots of string literals. *) 933(*****************************************************************************) 934val string_abbrevs = ref([]: (string * term)list); 935 936(*****************************************************************************) 937(* Check if an abbreviation already exists *) 938(*****************************************************************************) 939fun has_abbrev s = can (assoc s) (!string_abbrevs); 940 941(*****************************************************************************) 942(* Function to add a list of string abbreviations to string_abbrevs *) 943(*****************************************************************************) 944fun add_string_abbrevs tml = (string_abbrevs := (!string_abbrevs) @ tml); 945 946(*****************************************************************************) 947(* Declare constants ACL2_STRING_ABBREV_n, ACL2_STRING_ABBREV_n+1 etc to *) 948(* abbreviate strings in a supplied list. The starting point n is kept in *) 949(* the reference string_abbrev_count. *) 950(* *) 951(* If a string already has an abbreviation or is in a list !no_abbrev_list *) 952(* of strings that shouldn't be abbreviated, then it is ignored. *) 953(*****************************************************************************) 954val string_abbrev_count = ref 0; 955val no_abbrev_list = ref(["NIL","QUOTE"]); 956 957fun make_string_abbrevs [] = () 958 | make_string_abbrevs (s::sl) = 959 if has_abbrev s 960 then (print "Warning: \""; print s; print "\" already abbreviated by "; 961 print_term(assoc s (!string_abbrevs)); print "\n"; 962 make_string_abbrevs sl) else 963 if mem s (!no_abbrev_list) 964 then (print "Warning: \""; print s; print "\" is in !no_abbrev_list\n"; 965 make_string_abbrevs sl) 966 else 967 (add_string_abbrevs 968 [(s, lhs 969 (concl 970 (SPEC_ALL 971 (Define 972 `^(mk_var 973 (("ACL2_STRING_ABBREV_" 974 ^ Int.toString(!string_abbrev_count)), 975 ``:string``)) = 976 ^(fromMLstring s)`))))]; 977 (string_abbrev_count := (!string_abbrev_count)+1); 978 make_string_abbrevs sl); 979 980(*****************************************************************************) 981(* Print !string_abbrevs to a string (used in adjoin_to_theory). *) 982(* There may be a better way of doing this! *) 983(*****************************************************************************) 984local 985fun string_abbrevs_to_string_aux [] = "" 986 | string_abbrevs_to_string_aux [(s,c)] = 987 ("(\"" ^ s ^ "\",Parse.Term`" ^ fst(dest_const c) ^"`)") 988 | string_abbrevs_to_string_aux ((s,c)::pl) = 989 ("(\"" ^ s ^ "\",Parse.Term`" ^ fst(dest_const c) ^"`)," ^ 990 string_abbrevs_to_string_aux pl) 991in 992fun string_abbrevs_to_string pl = 993 ("[" ^ string_abbrevs_to_string_aux pl ^ "]") 994end; 995 996(*****************************************************************************) 997(* Version of fromMLstring that looks up in string_abbrevs. Convert an ML *) 998(* string to a term: return constant from string_abbrevs if one is found, *) 999(* otherwise return a string literal. *) 1000(*****************************************************************************) 1001fun abbrevMLstring s = 1002 assoc s (!string_abbrevs) 1003 handle HOL_ERR _ => fromMLstring s; 1004 1005(*****************************************************************************) 1006(* Version of fromHOLstring that looks up in string_abbrevs. *) 1007(*****************************************************************************) 1008fun abbrevHOLstring c = 1009 rev_assoc c (!string_abbrevs) 1010 handle HOL_ERR _ => fromHOLstring c; 1011 1012(*****************************************************************************) 1013(* Get the HOL name from ACL2 name. *) 1014(* If there is no HOL name (e.g. an ACL2 variable) the ACL2 name is *) 1015(* returned. *) 1016(*****************************************************************************) 1017local 1018fun get_hol_name_from_acl2_name_aux [] sym = 1019 mlsym_to_string sym 1020 | get_hol_name_from_acl2_name_aux ((hol,acl2) :: nl) sym = 1021 if acl2 = mlsym_to_string sym 1022 then hol 1023 else get_hol_name_from_acl2_name_aux nl sym 1024in 1025fun get_hol_name_from_acl2_name sym = 1026 get_hol_name_from_acl2_name_aux (!acl2_names) sym 1027end; 1028 1029(*****************************************************************************) 1030(* Test that a type is ``:sexp`` or ``:sexp -> ... -> sexp`` *) 1031(*****************************************************************************) 1032fun is_sexp_ty ty = 1033 let val (tyop,tyargs) = dest_type ty 1034 in 1035 (tyop = "sexp" 1036 orelse (tyop = "fun" 1037 andalso hd tyargs = ``:sexp`` 1038 andalso is_sexp_ty(hd(tl tyargs)))) 1039 end; 1040 1041(*****************************************************************************) 1042(* Translate a term of type ``:sexp`` to an s-expression represented in ML *) 1043(*****************************************************************************) 1044fun term_to_mlsexp tm = 1045 if is_var tm 1046 then string_to_mlsym(fst(dest_var tm)) else 1047 if is_const tm 1048 then 1049 (if is_sexp_ty(type_of tm) 1050 then string_to_mlsym(fst(dest_const tm)) 1051 else (print_term tm; 1052 print " has type ``"; 1053 print_type(type_of tm); 1054 print "`` so is not a first-order function on S-expressions\n"; 1055 err "term_to_mlsexp" "constant has bad type")) else 1056 if is_string tm 1057 then string_to_mlsym(fromHOLstring tm) else 1058 if is_nat tm 1059 then mlnum(dest_nat tm, "1", "0", "1") else 1060 if is_int tm 1061 then mlnum(dest_int tm, "1", "0", "1") else 1062 if is_cpx tm 1063 then mlnum(dest_cpx tm) else 1064 if is_numeral tm 1065 then (print "Bad occurence of numeral "; 1066 print_term tm; print ". Use \"nat\", \"int\" or \"cpx\".\n"; 1067 err "term_to_mlsexp" "bad occurrence of a numeral") else 1068 if is_integer tm 1069 then (print "Bad occurence of integer numeral "; 1070 print_term tm; print ". Use \"nat\", \"int\" or \"cpx\".\n"; 1071 err "term_to_mlsexp" "bad occurrence of an integer numeral") else 1072 if is_let tm 1073 then 1074 let val (param_arg_tuples,bdy) = dest_anylet tm 1075 val (param_tuples,arg_tuples) = unzip param_arg_tuples 1076 val args = (flatten o map strip_pair) arg_tuples 1077 val params = (flatten o map strip_pair) param_tuples 1078 in 1079 if not(length params = length args) 1080 then (print_term tm; print "\n"; 1081 print "different numbers of formal and actual parameters\n"; 1082 err "term_to_mlsexp" "formal/actual mismatch") 1083 else mk_mlsexp_list 1084 (mk_mlsexp_list 1085 [mllambda, 1086 mk_mlsexp_list(map term_to_mlsexp params), 1087 term_to_mlsexp bdy] 1088 :: map term_to_mlsexp args) 1089 end else 1090 if is_comb tm 1091 then 1092 let val (opr,args) = strip_comb tm 1093 in 1094 if is_const opr 1095 then (case fst(dest_const opr) 1096 of "ACL2_SYMBOL" => mk_mlquote 1097 (mlsym(abbrevHOLstring(hd args), 1098 abbrevHOLstring(hd(tl args)))) 1099 | "ACL2_STRING" => mlstr(abbrevHOLstring(hd args)) 1100 | "ACL2_CHARACTER" => mlchr(fromHOLchar(hd args)) 1101 | "ACL2_NUMBER" => (print_term tm; print "\n"; 1102 print "term built with num not supported"; 1103 print " -- use nat, int or cpx\n"; 1104 err "term_to_mlsexp" 1105 "ACL2_NUMBER case unsupported") 1106 | "cpx" => (print_term tm; print "\n"; 1107 print "bad use of cpx\n"; 1108 err "term_to_mlsexp" 1109 "badly formed application of cpx") 1110 | _ => mk_mlsexp_list 1111 (map term_to_mlsexp (opr::args)) 1112 1113 ) else 1114 if is_var opr 1115 then mk_mlsexp_list (map term_to_mlsexp (opr::args)) else 1116 if is_abs opr 1117 then 1118 let val (params,bdy) = strip_abs opr 1119 in 1120 if not(length params = length args) 1121 then (print_term tm; print "\n"; 1122 print "different numbers of formal and actual parameters\n"; 1123 err "term_to_mlsexp" "formal/actual mismatch") 1124 else mk_mlsexp_list 1125 (mk_mlsexp_list 1126 [mllambda, 1127 mk_mlsexp_list(map term_to_mlsexp params), 1128 term_to_mlsexp bdy] 1129 :: map term_to_mlsexp args) 1130 end else 1131 (print_term opr; 1132 print " is not allowed as a function\n"; 1133 err "term_to_mlsexp" "bad function") 1134 end else 1135 (print_term tm; print "\n"; 1136 print "bad argument to term_to_mlsexp\n"; 1137 err "term_to_mlsexp" "bad argument"); 1138 1139(*****************************************************************************) 1140(* Print an ML s-expression s on an output stream out *) 1141(*****************************************************************************) 1142fun print_mlsexp (out:string->unit) (sym as mlsym(_,_)) = 1143 out(mlsym_to_string sym) 1144 | print_mlsexp (out:string->unit) (mlstr s) = 1145 (out "\""; out s; out "\"") 1146 | print_mlsexp (out:string->unit) (mlchr c) = 1147 (out "(code-char "; out(int_to_string(ord c)); out ")") 1148 | print_mlsexp (out:string->unit) (mlnum(an,ad,bn,bd)) = 1149 if (bn = "0") andalso (bd = "1") 1150 then (out an; out "/"; out ad) 1151 else (out "(COMMON-LISP::COMPLEX "; 1152 out an; out "/"; out ad; 1153 out " "; 1154 out bn; out "/"; out bd; 1155 out ")") 1156 | print_mlsexp (out:string->unit) (mlpair(p1,p2)) = 1157 (out "("; 1158 (if is_mlsexp_list p2 1159 then let val sl = dest_mlsexp_list p2 1160 in 1161 if null sl 1162 then print_mlsexp out p1 1163 else (print_mlsexp out p1; 1164 map (fn p => (out " "; print_mlsexp out p)) sl; 1165 ()) 1166 end 1167 else (print_mlsexp out p1; out " . "; print_mlsexp out p2)); 1168 out ")"); 1169 1170(*****************************************************************************) 1171(* Print an ML s-expression to the interactive session *) 1172(*****************************************************************************) 1173fun pr_mlsexp s = (print_mlsexp print s; print "\n"); 1174 1175(*****************************************************************************) 1176(* Print an s-expression term to the interactive session *) 1177(*****************************************************************************) 1178fun pr_sexp t = pr_mlsexp(term_to_mlsexp t); 1179 1180(*****************************************************************************) 1181(* Extract the name of a constant or variable *) 1182(*****************************************************************************) 1183exception get_name_fail; 1184fun get_name tm = 1185 if is_const tm 1186 then fst(dest_const tm) else 1187 if is_var tm then fst(dest_var tm) 1188 else raise get_name_fail; 1189 1190(*****************************************************************************) 1191(* ``f x1 ... xn = e`` --> (defun f (x1 ... xn) ^(term_to_mlsexp e)) *) 1192(*****************************************************************************) 1193fun deftm_to_mlsexp_defun tm = 1194 let val (l,r) = dest_eq(spec_all tm) 1195 val (opr, args) = strip_comb l 1196 in 1197 mk_mlsexp_list 1198 [mksym "COMMON-LISP" "DEFUN", 1199 string_to_mlsym(get_name opr), 1200 mk_mlsexp_list(map term_to_mlsexp args), 1201 term_to_mlsexp r] 1202 end; 1203 1204(*****************************************************************************) 1205(* Translate a hol-acl2 definition *) 1206(* *) 1207(* |- f x1 ... xn = e *) 1208(* *) 1209(* to an ML s-expression representing *) 1210(* *) 1211(* (defun f (x1 ... xn) ^(term_to_mlsexp e)) *) 1212(*****************************************************************************) 1213fun def_to_mlsexp_defun th = 1214 let val (asl, concl) = dest_thm(SPEC_ALL th) 1215 val _ = if not(asl = []) 1216 then(print_thm th; 1217 print "\n"; print"should not have any assumptions\n"; 1218 err "mk_mlsexp_defthm" "assumptions not allowed") 1219 else () 1220 in 1221 deftm_to_mlsexp_defun concl 1222 end; 1223 1224(*****************************************************************************) 1225(* Print a hol-acl2 definition *) 1226(* *) 1227(* |- f x1 ... xn = e *) 1228(* *) 1229(* as *) 1230(* *) 1231(* (defun f (x1 ... xn) ^(term_to_mlsexp e)) *) 1232(*****************************************************************************) 1233fun pr_mlsexp_defun th = pr_mlsexp(def_to_mlsexp_defun th); 1234 1235(*****************************************************************************) 1236(* Code for processing ACL2 defuns slurped into HOL via Matt's a2ml tool *) 1237(*****************************************************************************) 1238 1239(*****************************************************************************) 1240(* Convert a string to integer numeral *) 1241(* *) 1242(* string_to_int_term "37" = ``37`` *) 1243(* string_to_int_term "~37" = ``~37`` *) 1244(* string_to_int_term "-37" = ``~37`` *) 1245(*****************************************************************************) 1246fun string_to_int_term s = intSyntax.term_of_int(Arbint.fromString s); 1247 1248(*****************************************************************************) 1249(* There are two obvious ways to convert an mlsexp to a term: *) 1250(* *) 1251(* 1. recursively descend through it build up a term; *) 1252(* *) 1253(* 2. convert it to a string s than then use Term[QUOTE s]. *) 1254(* *) 1255(* Method 1 allows more detailed checking and gives finer control over *) 1256(* error messages. Method 2 is a bit easier to implement, but may be *) 1257(* less robust. *) 1258(* *) 1259(* Initially we started to implement Method 2 as it was simpler, but then *) 1260(* it became clear that it would not handle ACL2's non standard *) 1261(* identifier names, so we switched to Method 1. *) 1262(* *) 1263(* However, the unfinished partial implementation of Method 2 *) 1264(* (mlsexp_to_string) is useful for debugging, as it enables one to print *) 1265(* compact representations of imported mlsexps. *) 1266(* *) 1267(*****************************************************************************) 1268 1269(*****************************************************************************) 1270(* Convert an ML s-expression (mlsexp) to a string that will parse to the *) 1271(* corresponding HOL s-expression (sexp). *) 1272(*****************************************************************************) 1273fun mlquote_to_string (mlsym(pkg,nam)) = 1274 ("(sym \"" ^ pkg ^ "\" \"" ^ nam ^"\")") 1275 | mlquote_to_string (mlstr s) = 1276 ("(str " ^ "\"" ^ s ^ "\")") 1277 | mlquote_to_string (mlchr c) = 1278 ("(chr " ^ "(CHR " ^ int_to_string(ord c) ^ "))") 1279 | mlquote_to_string (mlnum(an,ad,bn,bd)) = 1280 ("(cpx " ^ 1281 acl2_int_to_hol_int an ^ " " ^ 1282 acl2_int_to_hol_int ad ^ " " ^ 1283 acl2_int_to_hol_int bn ^ " " ^ 1284 acl2_int_to_hol_int bd ^")") 1285 | mlquote_to_string (mlpair(x,y)) = 1286 ("(cons " ^ mlquote_to_string x ^ " " ^ mlquote_to_string y ^ ")"); 1287 1288(*****************************************************************************) 1289(* Convert an ML s-expression (mlsexp) to a string that will parse to the *) 1290(* corresponding HOL s-expression (sexp). *) 1291(*****************************************************************************) 1292fun mlquote_to_string (mlsym(pkg,nam)) = 1293 ("(sym \"" ^ pkg ^ "\" \"" ^ nam ^"\")") 1294 | mlquote_to_string (mlstr s) = 1295 ("(str " ^ "\"" ^ s ^ "\")") 1296 | mlquote_to_string (mlchr c) = 1297 ("(chr " ^ "(CHR " ^ int_to_string(ord c) ^ "))") 1298 | mlquote_to_string (mlnum(an,ad,bn,bd)) = 1299 ("(cpx " ^ 1300 acl2_int_to_hol_int an ^ " " ^ 1301 acl2_int_to_hol_int ad ^ " " ^ 1302 acl2_int_to_hol_int bn ^ " " ^ 1303 acl2_int_to_hol_int bd ^")") 1304 | mlquote_to_string (mlpair(x,y)) = 1305 ("(cons " ^ mlquote_to_string x ^ " " ^ mlquote_to_string y ^ ")"); 1306 1307(*****************************************************************************) 1308(* Convert an ML s-expression (mlsexp) to the coresponding HOL *) 1309(* s-expression (i.e. term of type sexp). *) 1310(*****************************************************************************) 1311fun mlquote_to_term (sym as mlsym(pkg,nam)) = 1312 if sym = mlnil then ``nil`` else 1313 if sym = mlt then ``t`` else 1314 ``sym ^(abbrevMLstring pkg) ^(abbrevMLstring nam)`` 1315 | mlquote_to_term (mlstr s) = 1316 ``str ^(abbrevMLstring s)`` 1317 | mlquote_to_term (mlchr c) = 1318 ``chr ^(fromMLchar c)`` 1319 | mlquote_to_term (mlnum(an,ad,bn,bd)) = 1320 ``cpx ^(string_to_int_term an) 1321 ^(string_to_int_term ad) 1322 ^(string_to_int_term bn) 1323 ^(string_to_int_term bd)`` 1324 | mlquote_to_term (mlpair(x,y)) = 1325 ``cons ^(mlquote_to_term x) ^(mlquote_to_term y)``; 1326 1327(*****************************************************************************) 1328(* Convert an mlsexp representing a term to a string. *) 1329(* *) 1330(* From: http://www.dina.kvl.dk/~sestoft/mosmllib/List.html *) 1331(* *) 1332(* [foldl op% e xs] evaluates xn % (x(n-1) % ( ... % (x2 % (x1 % e)))) *) 1333(* where xs = [x1, x2, ..., x(n-1), xn], and % is taken to be infixed. *) 1334(* *) 1335(*****************************************************************************) 1336fun mlsexp_to_string (sym as mlsym(_,_)) = 1337 mlsym_to_string sym 1338 | mlsexp_to_string (mlstr s) = ("(str " ^ "\"" ^ s ^ "\")") 1339 | mlsexp_to_string (mlchr c) = 1340 ("(chr " ^ "(CHR " ^ int_to_string(ord c) ^ "))") 1341 | mlsexp_to_string (mlnum(an,ad,bn,bd)) = 1342 ("(cpx " ^ 1343 acl2_int_to_hol_int an ^ " " ^ 1344 acl2_int_to_hol_int ad ^ " " ^ 1345 acl2_int_to_hol_int bn ^ " " ^ 1346 acl2_int_to_hol_int bd ^")") 1347 | mlsexp_to_string (p as mlpair(x,y)) = 1348 if is_mlquote p 1349 then mlquote_to_string(dest_mlquote p) 1350 else ("(" ^ 1351 (if is_mlsexp_list y 1352 then foldl 1353 (fn (z,zs) => zs ^ " " ^ mlsexp_to_string z) 1354 (mlsexp_to_string x) 1355 (dest_mlsexp_list y) 1356 else (print "attempt to translate a non-list to a term\n"; 1357 err "mlsexp_to_string" "non-list")) ^ 1358 ")"); 1359 1360(*****************************************************************************) 1361(* mlsym(pkg,nam) |--> mk_var("pkg::nam",``:sexp``) *) 1362(*****************************************************************************) 1363fun param_to_var (sym as mlsym(_,_)) = 1364 mk_var(mlsym_to_string sym,``:sexp``) 1365 | param_to_var _ = 1366 (print "Not a mlsym\n"; 1367 err "param_to_var" "parameter not an mlsym"); 1368 1369(*****************************************************************************) 1370(* mlsym(pkg,nam) ty |--> mk_var("pkg::nam",ty) *) 1371(*****************************************************************************) 1372fun name_to_var (sym as mlsym(_,_)) ty = 1373 mk_var(mlsym_to_string sym,ty) 1374 | name_to_var _ _ = 1375 (print "Not a mlsym\n"; 1376 err "name_to_var" "name not an mlsym"); 1377 1378(*****************************************************************************) 1379(* Look up the HOL name of an ACL2 name and return the corresponding *) 1380(* term. Return a variable with a supplied type if there is no HOL name. *) 1381(*****************************************************************************) 1382val acl2_name_to_term_print_flag = ref false; 1383 1384local 1385fun if_print s = if (!acl2_name_to_term_print_flag) then print s else () 1386in 1387fun acl2_name_to_term sym ty = 1388 if sym = mlt 1389 then ``t`` else 1390 if sym = mlnil 1391 then ``nil`` else 1392 if sym = mlcons 1393 then ``ACL2_PAIR`` else 1394 let val sym_string = mlsym_to_string sym 1395 val sym_terms = Term.decls sym_string 1396 val sym_types = map (snd o dest_const) sym_terms 1397 in 1398 if mem ty sym_types 1399 then mk_const(sym_string,ty) 1400 else (if_print "Warning: \""; 1401 if_print sym_string; 1402 if_print "\" made a variable by acl2_name_to_term\n"; 1403 mk_var(sym_string,ty)) 1404 end 1405end; 1406 1407(*****************************************************************************) 1408(* n |--> ``:sexp -> ... -> sexp`` (n arguments) *) 1409(*****************************************************************************) 1410fun mk_sexp_fun_ty n = 1411 if n = 0 then ``:sexp`` else ``:sexp -> ^(mk_sexp_fun_ty(n-1))``; 1412 1413(*****************************************************************************) 1414(* list_mk_abs doesn't create an abstraction when the arg list is empty *) 1415(*****************************************************************************) 1416val list_mk_fun = list_mk_abs; 1417 1418(*****************************************************************************) 1419(* Convert an mlsexp representing a term to the term. *) 1420(*****************************************************************************) 1421fun mlsexp_to_term (sym as mlsym(_,_)) = 1422 acl2_name_to_term sym ``:sexp`` 1423 | mlsexp_to_term (mlstr s) = ``str ^(abbrevMLstring s)`` 1424 | mlsexp_to_term (mlchr c) = ``chr ^(fromMLchar c)`` 1425 | mlsexp_to_term (mlnum(an,ad,bn,bd)) = 1426 ``cpx ^(string_to_int_term an) 1427 ^(string_to_int_term ad) 1428 ^(string_to_int_term bn) 1429 ^(string_to_int_term bd)`` 1430 | mlsexp_to_term (p as mlpair(x,y)) = 1431 if is_mlquote p 1432 then mlquote_to_term(dest_mlquote p) else 1433 if is_mllambda p 1434 then let val (params,bdy,args) = dest_mllambda p 1435 in 1436 list_mk_comb 1437 (list_mk_fun(map param_to_var params, mlsexp_to_term bdy), 1438 map mlsexp_to_term args) 1439 end else 1440 if is_mlsexp_list y 1441 then let val args = map mlsexp_to_term (dest_mlsexp_list y) 1442 val opr = if is_mlsym x 1443 then acl2_name_to_term 1444 x 1445 (mk_sexp_fun_ty(length args)) 1446 else mlsexp_to_term x 1447 in 1448 (list_mk_comb(opr,args) 1449 handle HOL_ERR _ => 1450 (print "Can't make term\n"; 1451 print(mlsexp_to_string p); 1452 print "\n"; 1453 err "mlsexp_to_term" "bad mlsexp")) 1454 end else 1455 (print "attempt to translate a non-list to a term\n"; 1456 err "mlsexp_to_term" "non-list"); 1457 1458(*****************************************************************************) 1459(* (defun d (x1 ... xm) b) |--> "d x1 ... xm = b" *) 1460(*****************************************************************************) 1461fun defun_to_string d = 1462 if is_mldefun d 1463 then let val (sym, params, bdy) = dest_mldefun d 1464 in 1465 foldl 1466 (fn (z,zs) => zs ^ " " ^ z) 1467 ("ACL2_" ^ mlsym_to_string sym) 1468 (map mlsym_to_string params) 1469 ^ " = " ^ mlsexp_to_string bdy 1470 end 1471 else (print "defun badly formed\n"; 1472 err "defun_to_string" "bad defun"); 1473 1474(*****************************************************************************) 1475(* Test for a defun, defaxiom or defthm *) 1476(*****************************************************************************) 1477fun is_mldef d = 1478 is_mldefun d orelse is_mldefun_sk d orelse is_mldefaxiom d orelse is_mldefthm d; 1479 1480(*****************************************************************************) 1481(* ``f = \x1 ... xn. bdy`` --> ``f x1 ... xn = bdy`` *) 1482(*****************************************************************************) 1483fun mk_def_eq tm = 1484 if is_eq tm 1485 then foldl 1486 (fn (v,t) => mk_eq(mk_comb(lhs t,v),beta_conv(mk_comb(rhs t,v)))) 1487 tm 1488 (fst(strip_abs(rhs tm))) 1489 else tm; 1490 1491(*****************************************************************************) 1492(* |- f = \x1 ... xn. bdy *) 1493(* ---------------------- *) 1494(* |- f x1 ... xn = bdy *) 1495(*****************************************************************************) 1496fun MK_DEF_EQ th = 1497 if is_eq(concl(SPEC_ALL th)) 1498 then foldl 1499 (fn (v,th) => RIGHT_CONV_RULE BETA_CONV (AP_THM th v)) 1500 th 1501 (fst(strip_abs(rhs(concl(SPEC_ALL th))))) 1502 else th; 1503 1504(*****************************************************************************) 1505(* Conversion *) 1506(* *) 1507(* ``(\x1 ... xn. t) y1 .. yn`` *) 1508(* --> *) 1509(* |- (\x1 ... xn. t) y1 .. yn = let (x1,...,xn) = (y1,...,yn) in t *) 1510(* *) 1511(*****************************************************************************) 1512fun LET_INTRO_CONV tm = 1513 let val (opr, args) = strip_comb tm 1514 val (params,bdy) = strip_abs opr 1515 val param_arg_list = filter 1516 (fn (v1,v2) => not(aconv v1 v2)) 1517 (zip params args) 1518 val let_tm = ``LET 1519 ^(mk_pabs(list_mk_pair params,bdy)) 1520 ^(list_mk_pair args)`` 1521 val th1 = DEPTH_CONV (REWR_CONV LET_THM) let_tm 1522 val th2 = DEPTH_CONV BETA_CONV tm 1523 val th3 = DEPTH_CONV PairRules.PBETA_CONV(rhs(concl th1)) 1524 in 1525 GSYM(TRANS(TRANS th1 th3)(GSYM th2)) 1526 end; 1527 1528(*****************************************************************************) 1529(* Flag to determine whether to introduce lets *) 1530(*****************************************************************************) 1531val let_flag = ref true; 1532 1533(*****************************************************************************) 1534(* Rule to introduce let throughout a term *) 1535(*****************************************************************************) 1536fun LET_INTRO th = 1537 if !let_flag 1538 then CONV_RULE (TRY_CONV(RHS_CONV(TOP_DEPTH_CONV LET_INTRO_CONV))) th 1539 else th; 1540 1541(****************************************************************************** 1542The method of converting a full ACL2 name pkg::sym to a HOL-friendly 1543name is as follows (see definition of create_hol_name below). 1544 1545 1. First see if the ACL2 name already has a HOL name, and if so 1546 return it. 1547 1548 2. Convert sym to a HOL name, say hol_sym, using the ML function 1549 acl2_name_to_hol_name (this function is described below). 1550 1551 3. If hol_sym starts with a digit, then use acl2_name_to_hol_name 1552 to convert pkg to hol_pkg, then lengthen the name to 1553 (hol_pkg ^ "_" ^ hol_sym). 1554 1555 4. Check to see if sym_name (or the lengthened name) is already used. 1556 If not it is the result. 1557 1558 5. If hol_sym is in use and doesn't start with a digit, then see if 1559 (hol_pkg ^ "_" ^ hol_sym) is used, and if not return it. If it is 1560 in use an error report is printed and an exception raised. 1561 1562 6. Record any names generated by steps above in acl2_names so 1563 the original names can be recovered. 1564 1565The function acl2_name_to_hol_name converts a string s to a 1566HOL-friendly name as follows. 1567 1568 1. Convert s to a list of characters and convert all letters 1569 to lower-case. 1570 1571 2. Replace "-" by "_". 1572 1573 3. Replace special characters by strings of letter characters 1574 using acl2_to_hol_char_map (defined below). Add an underscore 1575 "_" to separate special characters from all other characters. 1576 1577We think these simple rules should be sufficient in practice, and if 1578they are not it's better to reconsider carefully what to do rather 1579than to have ugly looking names generated by more complicated rules 1580(this might change if the sufficiency assumption is badly wrong). 1581******************************************************************************) 1582 1583 1584(*****************************************************************************) 1585(* Map from ACL2 characters in names to lists of HOL-friendly characters. *) 1586(*****************************************************************************) 1587val acl2_to_hol_char_map = 1588 [(#"=" , explode "equal"), 1589 (#"<" , explode "less"), 1590 (#">" , explode "greater"), 1591 (#"/" , explode "slash"), 1592 (#"\\" , explode "backslash"), 1593 (#"?" , explode "question"), 1594 (#"$" , explode "dollar"), 1595 (#"!" , explode "exclaim"), 1596 (#"*" , explode "star"), 1597 (#"+" , explode "plus"), 1598 (#":" , explode "colon"), 1599 (#" " , explode "space")]; 1600 1601(*****************************************************************************) 1602(* Check is a character is in the domain of acl2_to_hol_char_map. *) 1603(*****************************************************************************) 1604fun isSpecial c = can (assoc c) acl2_to_hol_char_map; 1605 1606(*****************************************************************************) 1607(* Convert a character to a list of HOL-friendly characters by applying *) 1608(* acl2_to_hol_char_map. If the character is not in the domain of *) 1609(* acl2_to_hol_char_map, then if it is #"-" it is converted to #"_" else *) 1610(* it is converted to lower case. *) 1611(*****************************************************************************) 1612fun acl2_char_to_hol_chars c = 1613 if Char.isAlphaNum c 1614 then [Char.toLower c] else 1615 if c = #"-" then [#"_"] 1616 else assoc c acl2_to_hol_char_map handle HOL_ERR _ => [c]; 1617 1618fun acl2_chars_to_hol_chars [] = [] 1619 | acl2_chars_to_hol_chars [c] = acl2_char_to_hol_chars c 1620 | acl2_chars_to_hol_chars (c1::(cl as (c2::_))) = 1621 if (isSpecial c1 orelse isSpecial c2) 1622 andalso not(c1 = #"-") andalso not(c2 = #"-") 1623 then acl2_char_to_hol_chars c1@(#"_"::acl2_chars_to_hol_chars cl) 1624 else acl2_char_to_hol_chars c1@acl2_chars_to_hol_chars cl; 1625 1626(*****************************************************************************) 1627(* ACL2 to HOL name conversion function. Treats first character specially. *) 1628(*****************************************************************************) 1629fun acl2_name_to_hol_name acl2_name = 1630 case assoc2 acl2_name (!acl2_names) 1631 of SOME (hol_name,_) => hol_name 1632 | NONE => implode(acl2_chars_to_hol_chars(explode acl2_name)); 1633 1634(*****************************************************************************) 1635(* Create a HOL-friendly name from a full ACL2 name and remember it in *) 1636(* acl2_names. No effect on names unchanged by acl2_name_to_hol_name. *) 1637(* *) 1638(* The package name is eliminated unless it's needed to disambiguate HOL *) 1639(* names (e.g. if the symbol symbol name occurs with two package names). *) 1640(*****************************************************************************) 1641fun create_hol_name acl2_name = 1642 if acl2_name = acl2_name_to_hol_name acl2_name 1643 then acl2_name 1644 else 1645 let val (pkg_name,sym_name) = split_acl2_name acl2_name 1646 val hol_pkg_name = acl2_name_to_hol_name pkg_name 1647 val hol_sym_name = acl2_name_to_hol_name sym_name 1648 val long_hol_name = (hol_pkg_name ^ "_" ^ hol_sym_name) 1649 val fst_char = hd(explode hol_sym_name) 1650 in 1651 if Char.isDigit fst_char 1652 then 1653 (case (assoc1 long_hol_name (!acl2_names)) 1654 of SOME(_,acl2_name') 1655 => if acl2_name = acl2_name' 1656 then long_hol_name 1657 else (print "\""; 1658 print long_hol_name; 1659 print "\" is the name of \""; 1660 print acl2_name'; 1661 print "\"\nso can't use it to name \""; 1662 print acl2_name; print "\"\n"; 1663 err "create_hol_name" "name already in use (case 1)") 1664 | NONE 1665 => (acl2_names := (long_hol_name, acl2_name)::(!acl2_names); 1666 long_hol_name) 1667 ) 1668 else 1669 (case (assoc1 hol_sym_name (!acl2_names)) 1670 of SOME(_,acl2_name') 1671 => if acl2_name = acl2_name' 1672 then hol_sym_name 1673 else 1674 (case (assoc1 long_hol_name (!acl2_names)) 1675 of SOME(_,acl2_name'') 1676 => if acl2_name = acl2_name'' 1677 then long_hol_name 1678 else (print "\""; 1679 print hol_sym_name; 1680 print "\" is the name of \""; 1681 print acl2_name'; 1682 print "\"\nso can't use it to name \""; 1683 print acl2_name; print "\"\n"; 1684 print "\""; 1685 print long_hol_name; 1686 print "\" is the name of \""; 1687 print acl2_name''; 1688 print "\"\nso can't use it to name \""; 1689 print acl2_name; print "\"\n"; 1690 err "create_hol_name" "name already in use (case 2)") 1691 | NONE 1692 => (acl2_names := (long_hol_name, acl2_name)::(!acl2_names); 1693 long_hol_name) 1694 ) 1695 | NONE 1696 => (acl2_names := (hol_sym_name, acl2_name)::(!acl2_names); 1697 hol_sym_name) 1698 ) 1699 end; 1700 1701(*****************************************************************************) 1702(* ML datatype to represent HOL tems and other data (e.g. names) of *) 1703(* events imported from ACL2 *) 1704(* *) 1705(* A defun contains a defining equation: ``!x1 ... xn. f x1 ... xn = e`` *) 1706(* (the universal quantification may be partial or absent) *) 1707(* *) 1708(* A defaxiom or defthm consists of a name and a term. *) 1709(* *) 1710(* A mutual represents MUTUAL-RECURSION and is a defining term (normally a *) 1711(* conjunction of universally quantified equations) suitable for processing *) 1712(* by Define. *) 1713(* *) 1714(* An encap represents ENCAPSULATE and is a pair comprising the list of *) 1715(* names of the events specifying the functions being introduced and the *) 1716(* defining term (normally an existential quantification) suitable for *) 1717(* processing by new_specification. *) 1718(*****************************************************************************) 1719datatype acl2def = 1720 defun of term 1721 | defaxiom of string * term 1722 | defthm of string * term 1723 | mutual of term 1724 | encap of (string list) * term; 1725 1726(*****************************************************************************) 1727(* Strip ``|=`` from defthms and defaxioms *) 1728(*****************************************************************************) 1729fun dest_ax_or_thm conc = 1730 let val (con,tm) = dest_comb conc 1731 val _ = if not(is_const con andalso (fst(dest_const con) = "|=")) 1732 then(print_term conc; 1733 print " should have form |= ...\n"; 1734 err "dest_ax_or_thm" "missing |=") 1735 else () 1736 in 1737 tm 1738 end; 1739 1740(*****************************************************************************) 1741(* "s1 s2 ... sn" |--> ["s1","s2",...,"sn"] (split at spaces) *) 1742(*****************************************************************************) 1743val split_at_spaces = String.tokens (fn c => c = #" "); 1744 1745(*****************************************************************************) 1746(* Convert a theorem obtained by slurping in ACL2 to an acl2def option. *) 1747(* Used for reproving ACL2 imports inside HOL and for round-trip printing. *) 1748(*****************************************************************************) 1749local 1750exception fail_for_mapfilter 1751in 1752fun dest_acl2_thm th = 1753 let val (asl, conc) = dest_thm(SPEC_ALL th) 1754 val _ = if not(asl = []) 1755 then(print_thm th; 1756 print "\n"; print"should not have any assumptions\n"; 1757 err "dest_acl2_thm" "assumptions not allowed") 1758 else () 1759 val tg = tag th 1760 val (tgl1,tgl2) = Tag.dest_tag tg 1761 val stgl = mapfilter 1762 (fn s => 1763 let val (s1,s2) = split_tag s 1764 in 1765 if mem s1 ["DEFUN","DEFAXIOM","DEFTHM", 1766 "MUTUAL-RECURSION","ENCAPSULATE"] 1767 then (s1,s2) 1768 else raise fail_for_mapfilter 1769 end) 1770 tgl1 1771 in 1772 if length stgl > 1 1773 then (print_thm th; 1774 print " has more than one ACL2 def tags!\n"; 1775 err "dest_acl2_thm" "more than one ACL2 tag") else 1776 if null stgl 1777 then NONE 1778 else case (fst(hd stgl)) 1779 of "DEFUN" 1780 => SOME(defun conc) 1781 | "DEFAXIOM" 1782 => SOME(defaxiom(snd(hd stgl), dest_ax_or_thm conc)) 1783 | "DEFTHM" 1784 => SOME(defthm(snd(hd stgl), dest_ax_or_thm conc)) 1785 | "MUTUAL-RECURSION" 1786 => SOME(mutual conc) 1787 | "ENCAPSULATE" 1788 => SOME(encap(split_at_spaces(snd(hd stgl)), conc)) 1789 | _ => NONE 1790 end 1791end; 1792 1793(*****************************************************************************) 1794(* Convert a hol theorem to a defthm *) 1795(*****************************************************************************) 1796fun thm_to_defthm(name,th) = 1797 defthm (name, dest_ax_or_thm(concl(SPEC_ALL th))); 1798 1799(*****************************************************************************) 1800(* Extraxt content from an option *) 1801(*****************************************************************************) 1802fun dest_option (SOME x) = x 1803 | dest_option NONE = err "dest_option" "NONE"; 1804 1805(*****************************************************************************) 1806(* ``PKG::SYM`` |--> create_hol_name "PKG::SYM" *) 1807(*****************************************************************************) 1808fun clean_acl2_var tm = 1809 if is_var tm 1810 then let val (s,ty) = dest_var tm 1811 val hol_name = create_hol_name s 1812 in 1813 mk_var(hol_name, ty) 1814 end 1815 else tm; 1816 1817(*****************************************************************************) 1818(* Clean all the free variables in a term *) 1819(*****************************************************************************) 1820fun clean_acl2_term tm = 1821 subst (map (fn v => v |-> clean_acl2_var v) (free_vars tm)) tm; 1822 1823(*****************************************************************************) 1824(* Clean all the free variables in a theorem *) 1825(*****************************************************************************) 1826fun CLEAN_ACL2_FREES th = 1827 INST (map (fn v => v |-> clean_acl2_var v) (thm_frees th)) th; 1828 1829(*****************************************************************************) 1830(* Conversion to clean a bound variable of an abstraction *) 1831(*****************************************************************************) 1832fun CLEAN_ACL2_ALPHA_CONV tm = 1833 let val (v,bdy) = dest_abs tm 1834 val (vname,vty) = dest_var v 1835 val hol_vname = create_hol_name vname 1836 in 1837 if hol_vname = vname 1838 then ALL_CONV tm 1839 else ALPHA_CONV (mk_var(hol_vname, vty)) tm 1840 end; 1841 1842(*****************************************************************************) 1843(* Conversion to clean all bound variables in a term *) 1844(*****************************************************************************) 1845val CLEAN_ACL2_BOUND_CONV = DEPTH_CONV CLEAN_ACL2_ALPHA_CONV; 1846 1847(*****************************************************************************) 1848(* Rule to clean all variables in a theorem *) 1849(*****************************************************************************) 1850val CLEAN_ACL2_VARS = 1851 LET_INTRO o CLEAN_ACL2_FREES o CONV_RULE CLEAN_ACL2_BOUND_CONV; 1852 1853(*****************************************************************************) 1854(* deftm(defun tm) = tm *) 1855(* deftm(defthm(_, tm)) = tm *) 1856(* deftm(defaxiom(_, tm)) = tm *) 1857(*****************************************************************************) 1858fun deftm(defun tm) = tm 1859 | deftm(defthm(_, tm)) = tm 1860 | deftm(defaxiom(_, tm)) = tm 1861 | deftm _ = err "deftm" "bad arg"; 1862 1863(*****************************************************************************) 1864(* ``!v1...vn. f v1 ... vn = tm`` |--> f *) 1865(*****************************************************************************) 1866fun get_defined tm = fst(strip_comb(lhs(spec_all tm))); 1867 1868(*****************************************************************************) 1869(* defun ``!v1...vn. f v1 ... vn = tm`` |--> f *) 1870(* fails on non-defuns *) 1871(*****************************************************************************) 1872exception get_defun_fun_fail; 1873fun get_defun_fun (defun tm) = get_defined tm 1874 | get_defun_fun _ = raise get_defun_fun_fail; 1875 1876(*****************************************************************************) 1877(* defname(defun ``!x1 ... xn. f x1 ... xn = t,``) = f *) 1878(* defname(defthm(nam, _)) = nam *) 1879(* defname(defaxiom(nam, _)) = nam *) 1880(*****************************************************************************) 1881fun defname(defun tm) = get_name(get_defined tm) 1882 | defname(defthm(nam,_)) = nam 1883 | defname(defaxiom(nam,_)) = nam 1884 | defname _ = err "defname" "bad arg"; 1885 1886(*****************************************************************************) 1887(* mk_sexp_fun_ty n |--> ``:sexp -> ... -> sexp -> sexp`` (n arguments) *) 1888(*****************************************************************************) 1889fun mk_sexp_fun_ty n = 1890 if n = 0 then ``:sexp`` else ``:sexp -> ^(mk_sexp_fun_ty(n-1))``; 1891 1892(*****************************************************************************) 1893(* mk_closed_event vl tm |--> ``!v1 ... vn. tm`` *) 1894(* *) 1895(* where v1,...,vn are the free variables in tm not in vl *) 1896(*****************************************************************************) 1897fun mk_closed_event vl tm = list_mk_forall(subtract(free_vars tm)vl, tm); 1898 1899(*****************************************************************************) 1900(* mk_acl2def converts an ML representation of an ACL2 event into an *) 1901(* equivalent hol acl2def specification *) 1902(* *) 1903(* (defun nam (x1 ... xm) bdy) *) 1904(* |--> *) 1905(* defun("nam", ``!x1 ... xm. nam x1 ..., xm = bdy``) *) 1906(* *) 1907(* (defthm nam bdy) *) 1908(* |--> *) 1909(* defthm("nam", ``|= tm``) *) 1910(* *) 1911(* (defaxiom nam bdy) *) 1912(* |--> *) 1913(* defaxiom("nam", ``|= tm``) *) 1914(* *) 1915(* (mutual-recursion d1 ... dn) *) 1916(* |--> *) 1917(* mutual ``^(deftm(mk_acl2def d1)) /\ ... /\ ^(deftm(mk_acl2def dn))`` *) 1918(* *) 1919(* (encapsulate ((v1 ... ) ... (vm ... )) e1 ... en) *) 1920(* |--> *) 1921(* encap *) 1922(* ([``n1``,...,``nm``], *) 1923(* ``?v1 ... vm. *) 1924(* ^(deftm(mk_acl2def e1)) /\ ... /\ ^(deftm(mk_acl2def en))``) *) 1925(* *) 1926(* where n1,...,nm are the names of the events introducing v1,...,vm, *) 1927(* respectively *) 1928(*****************************************************************************) 1929fun mk_acl2def d = 1930 if is_mldefun d 1931 then 1932 let val (nam,params,bdy) = dest_mldefun d 1933 val param_vars = map param_to_var params 1934 val bdy_tm = mlsexp_to_term bdy 1935 val tm = list_mk_fun(param_vars, bdy_tm) 1936 val ty = type_of tm 1937 val unbound_vars = 1938 subtract (free_vars bdy_tm) (name_to_var nam ty :: param_vars) 1939 val _ = if null unbound_vars 1940 then () 1941 else (print("Mutual recursion? " 1942 ^ snd(dest_mlsym nam) 1943 ^ " has unbound free variables: "); 1944 map (fn tm => (print_term tm; print " ")) unbound_vars; 1945 print"\n") 1946 1947 val sym_name = mlsym_to_string nam 1948 val newvar = mk_var(sym_name,ty) 1949 val defun_tm = list_mk_forall(param_vars, mk_def_eq(mk_eq(newvar,tm))) 1950 in 1951 defun(mk_closed_event [newvar] defun_tm) 1952 end else 1953 if is_mldefun_sk d 1954 then 1955 let val (nam,params,quant,qvars,bdy) = dest_mldefun_sk d 1956 val param_vars = map param_to_var params 1957 val quant_vars = map param_to_var qvars 1958 val quant_bdy = ``|= ^(mlsexp_to_term bdy)`` 1959 val quant_tm = 1960 if quant = ml_forall 1961 then list_mk_forall(quant_vars, quant_bdy) else 1962 if quant = ml_exists 1963 then list_mk_exists(quant_vars, quant_bdy) 1964 else err "mk_acl2def" (snd(dest_mlsym quant) ^ ": bad quantifier") 1965 val tm = list_mk_fun(param_vars, ``bool_to_sexp ^quant_tm``) 1966 val ty = type_of tm 1967 val unbound_vars = 1968 subtract (free_vars quant_tm) (name_to_var nam ty :: param_vars) 1969 val _ = if null unbound_vars 1970 then () 1971 else (print("Mutual recursion?" 1972 ^ snd(dest_mlsym nam) 1973 ^ " has unbound free variables: "); 1974 map (fn tm => (print_term tm; print " ")) unbound_vars; 1975 print"\n") 1976 val sym_name = mlsym_to_string nam 1977 val newvar = mk_var(sym_name,ty) 1978 val defun_tm = list_mk_forall(param_vars, mk_def_eq(mk_eq(newvar,tm))) 1979 in 1980 defun(mk_closed_event [newvar] defun_tm) 1981 end else 1982 if is_mldefthm d 1983 then 1984 let val (nam,bdy) = dest_mldefthm d 1985 val tm = mlsexp_to_term bdy 1986 val ty = type_of tm 1987 val sym_name = mlsym_to_string nam 1988 in 1989 defthm(sym_name, gen_all ``|= ^tm``) 1990 end else 1991 if is_mldefaxiom d 1992 then 1993 let val (nam,bdy) = dest_mldefaxiom d 1994 val tm = mlsexp_to_term bdy 1995 val ty = type_of tm 1996 val sym_name = mlsym_to_string nam 1997 in 1998 defaxiom(sym_name, gen_all ``|= ^tm``) 1999 end else 2000 if is_mlmutual d 2001 then 2002 let val dl = dest_mlmutual d 2003 val names = map (mlsym_to_string o #1 o dest_mldefun) dl 2004 in 2005 mutual(gen_all(list_mk_conj(map (deftm o mk_acl2def) dl))) (* WRONG! *) 2006 end else 2007 if is_mlencap d 2008 then 2009 let val (sigl,dl) = dest_mlencap d 2010 val sigll = map dest_mlsexp_list sigl 2011 val sig_vars = 2012 map 2013 (fn l => 2014 mk_var 2015 (mlsym_to_string(hd l), 2016 mk_sexp_fun_ty(length(dest_mlsexp_list(hd(tl l)))))) 2017 sigll 2018 val eventl = map mk_acl2def dl 2019 val defunl = mapfilter get_defun_fun eventl 2020 val extended_sig_vars = union sig_vars defunl 2021 val names = map defname eventl 2022 val event_tms = 2023 map (mk_closed_event extended_sig_vars o spec_all o deftm) eventl 2024 val spec_body = list_mk_exists(extended_sig_vars,list_mk_conj event_tms) 2025 in 2026 encap(names,gen_all spec_body) 2027 end 2028 else err "mk_acl2def" "badly formed mldef"; 2029 2030(*****************************************************************************) 2031(* Convert a list of character code to a string. *) 2032(* Used in ML generated from ACL2 by a2ml. *) 2033(*****************************************************************************) 2034val chars_to_string = implode o (map chr); 2035 2036(*****************************************************************************) 2037(* ["s1","s2",...,"sn"] |--> "s1 s2 ... sn" (strings separated by spaces) *) 2038(*****************************************************************************) 2039fun concat_with_spaces [] = "" 2040 | concat_with_spaces [s] = s 2041 | concat_with_spaces (s::sl) = s ^ " " ^ concat_with_spaces sl; 2042 2043(*****************************************************************************) 2044(* Get list of things being defined by a mutual recursion *) 2045(*****************************************************************************) 2046val get_defined_list = map get_defined o strip_conj o spec_all; 2047 2048(*****************************************************************************) 2049(* Space-separated concatenation of names of defuns in a mutual-recursion *) 2050(*****************************************************************************) 2051val mk_mutual_name = concat_with_spaces o map get_name o get_defined_list; 2052 2053(*****************************************************************************) 2054(* Print an acl2def *) 2055(*****************************************************************************) 2056fun print_acl2def out (defun tm) = 2057 (out "; Defun: "; out(get_name(get_defined tm)); out "\n"; 2058 print_mlsexp out (deftm_to_mlsexp_defun(spec_all tm)); 2059 out "\n\n") 2060 | print_acl2def out (defaxiom(nam,tm)) = 2061 (out "; Defaxiom: "; out nam; out "\n"; 2062 print_mlsexp out 2063 (mk_mlsexp_list 2064 [mldefaxiom, 2065 string_to_mlsym nam, 2066 term_to_mlsexp(spec_all tm)]); 2067 out "\n\n") 2068 | print_acl2def out (defthm(nam,tm)) = 2069 (out "; Defthm: "; out nam; out "\n"; 2070 print_mlsexp out 2071 (mk_mlsexp_list 2072 [mldefthm, 2073 string_to_mlsym nam, 2074 term_to_mlsexp(spec_all tm)]); 2075 out "\n\n") 2076 | print_acl2def out (mutual tm) = 2077 (out "; Mutual-Recursion "; out (mk_mutual_name tm); out "\n"; 2078 out "(MUTUAL-RECURSION\n\n"; 2079 map (print_acl2def out o defun) (strip_conj tm); 2080 out ")\n\n") 2081 | print_acl2def out (encap(sl,tm)) = err "print_acl2def" "encap not yet supported"; 2082(* 2083 (out "; Encapsulate\n"; 2084 map (print_acl2def out o defthm) (strip_conj(snd(strip_exists tm))); 2085 out "\n"); 2086*) 2087 2088(*****************************************************************************) 2089(* Convert a preterm to a string (used for inputting ACL2) *) 2090(*****************************************************************************) 2091local 2092fun drop_until_close [] = [] (* drop chars until comment closes *) 2093 | drop_until_close (#"*" :: #")" :: l) = l 2094 | drop_until_close (c :: l) = drop_until_close l 2095fun strip_comments [] = [] (* remove comments *) 2096 | strip_comments (#"(" :: #"*" :: l) = strip_comments(drop_until_close l) 2097 | strip_comments (c :: l) = c :: strip_comments l 2098fun strip_loc s = implode(strip_comments(explode s)) 2099fun unQUOTE(QUOTE s) = s (* QUOTE s |--> s *) 2100 | unQUOTE _ = err "unQUOTE" "not applied to a QUOTE" 2101in 2102val preterm_to_string = 2103 foldr (fn(q,sl) => strip_loc(unQUOTE (q:term frag)) ^ "\n" ^ sl) "" 2104end; 2105 2106(*****************************************************************************) 2107(* Absolute path of acl2 directory *) 2108(*****************************************************************************) 2109val acl2_path = ref(Globals.HOLDIR ^ "/examples/acl2"); 2110 2111(*****************************************************************************) 2112(* Location of a2ml.csh tool for converting ACL2 files to ML files *) 2113(*****************************************************************************) 2114val a2ml = ((!acl2_path) ^ "/lisp/a2ml.csh"); 2115 2116(*****************************************************************************) 2117(* Location of pprint-file.csh. tool for pretty-printing ACL2 files *) 2118(*****************************************************************************) 2119val pp = ((!acl2_path) ^ "/lisp/pprint-file.csh"); 2120 2121(*****************************************************************************) 2122(* Reference into which mlsexp generated by a2ml is put *) 2123(*****************************************************************************) 2124val acl2_list_ref = ref([] : mlsexp list); 2125 2126(*****************************************************************************) 2127(* Sequentially process, install and save the contents of acl2_list_ref: *) 2128(* *) 2129(* 1. declare constants in defuns, then make definition using mk_oracle_thm; *) 2130(* *) 2131(* 2. declare HOL-friendly names (declare_names) using names generated *) 2132(* with create_hol_name. *) 2133(* *) 2134(* 3. create theorems using mk_oracle_thm then save them with a HOL-friendly *) 2135(* name with suffix "_defun", "_axiom", "_thm", "_mutual" or "_encap" *) 2136(*****************************************************************************) 2137val mutual_ref = ref[]; (* For debugging *) 2138fun install(defun tm) = 2139 let val opr = get_defined tm 2140 val (opr_name,opr_ty) = dest_var opr 2141 val _ = if not(null(Term.decls opr_name)) 2142 then (print "\""; 2143 print opr_name; 2144 print "\" can only be defined once\n"; 2145 err "install" "repeated defun event") 2146 else () 2147 val (pkg_name,sym_name) = split_acl2_name opr_name 2148 val hol_name = create_hol_name opr_name 2149 val new_hol_name = 2150 (if null(Term.decls hol_name) then "" else "acl2_") ^ hol_name 2151 val _ = new_constant(opr_name,opr_ty) 2152 val _ = declare_names(opr_name,new_hol_name) 2153 val con = mk_const(opr_name,opr_ty) 2154 val newtm = subst[opr |-> con]tm 2155 val save_name = hol_name ^ "_defun" 2156 val defun_thm = 2157 save_thm 2158 (save_name, CLEAN_ACL2_VARS(mk_acl2_thm "DEFUN" opr_name newtm)) 2159 in 2160 (save_name,defun_thm) 2161 end 2162 | install(defaxiom(acl2_name, tm)) = 2163 let val (pkg_name,sym_name) = split_acl2_name acl2_name 2164 val hol_name = create_hol_name acl2_name 2165 val save_name = hol_name ^ "_axiom" 2166 val defaxiom_thm = 2167 save_thm 2168 (save_name, CLEAN_ACL2_VARS(mk_acl2_thm "DEFAXIOM" acl2_name tm)) 2169 in 2170 (save_name,defaxiom_thm) 2171 end 2172 | install(defthm(acl2_name, tm)) = 2173 let val (pkg_name,sym_name) = split_acl2_name acl2_name 2174 val hol_name = create_hol_name acl2_name 2175 val save_name = hol_name ^ "_thm" 2176 val defthm_thm = 2177 save_thm 2178 (save_name, 2179 CLEAN_ACL2_VARS(mk_acl2_thm "DEFTHM" acl2_name tm)) 2180 in 2181 (save_name,defthm_thm) 2182 end 2183 | install(mutual tm) = 2184 let val _ = (mutual_ref := tm:: (!mutual_ref)) 2185 val tms = get_defined_list tm 2186 val opr_name_ty_list = map dest_var tms 2187 val acl2_name = mk_mutual_name tm 2188 val hol_names = map (create_hol_name o fst) opr_name_ty_list 2189 val new_hol_names = 2190 map 2191 (fn tm => (if null(Term.decls tm) then "" else "acl2_") ^ tm) 2192 hol_names 2193 val _ = map new_constant opr_name_ty_list 2194 val _ = map2 2195 (fn (nam,ty) => fn new_nam => declare_names(nam,new_nam)) 2196 opr_name_ty_list 2197 new_hol_names 2198 val con_list = map mk_const opr_name_ty_list 2199(* Old bad version 2200 val newtm = 2201 subst 2202 (map2 (fn opr => fn con => (opr |-> con)) tms con_list) 2203 (spec_all tm) 2204*) 2205 val newtm = 2206 list_mk_conj 2207 (map 2208 (gen_all 2209 o (subst(map2 (fn opr => fn con => (opr |-> con)) tms con_list)) 2210 o spec_all) 2211 (strip_conj(spec_all tm))) 2212 val hol_name = create_hol_name acl2_name 2213 val save_name = hol_name ^ "_mutual" 2214 val defthm_thm = 2215 save_thm 2216 (save_name, 2217 CLEAN_ACL2_VARS (mk_acl2_thm "MUTUAL-RECURSION" acl2_name newtm)) 2218 in 2219 (save_name,defthm_thm) 2220 end 2221 | install(encap(sl,bdy)) = 2222 let val (tms,tm) = strip_exists bdy 2223 val opr_name_ty_list = map dest_var tms 2224 val acl2_name = concat_with_spaces(map get_name tms) 2225 val hol_names = map (create_hol_name o fst) opr_name_ty_list 2226 val new_hol_names = 2227 map 2228 (fn tm => (if null(Term.decls tm) then "" else "acl2_") ^ tm) 2229 hol_names 2230 val _ = map new_constant opr_name_ty_list 2231 val _ = map2 2232 (fn (nam,ty) => fn new_nam => declare_names(nam,new_nam)) 2233 opr_name_ty_list 2234 new_hol_names 2235 val con_list = map mk_const opr_name_ty_list 2236 val newtm = 2237 subst 2238 (map2 (fn opr => fn con => (opr |-> con)) tms con_list) 2239 tm 2240 val hol_name = create_hol_name acl2_name 2241 val save_name = hol_name ^ "_encap" 2242 val defthm_thm = 2243 save_thm 2244 (save_name, 2245 CLEAN_ACL2_VARS(mk_acl2_thm "ENCAPSULATE" acl2_name newtm)) 2246 in 2247 (save_name,defthm_thm) 2248 end; 2249 2250(*****************************************************************************) 2251(* Get kind of acl2def *) 2252(*****************************************************************************) 2253fun dest_acl2def (defun tm) = ("DEFUN",get_name(get_defined tm)) 2254 | dest_acl2def (defaxiom(s,_)) = ("DEFAXIOM",s) 2255 | dest_acl2def (defthm(s,_)) = ("DEFTHM",s) 2256 | dest_acl2def (mutual tm) = ("MUTUAL-RECURSION", mk_mutual_name tm) 2257 | dest_acl2def (encap(sg,tm)) = ("ENCAPSULATE", concat_with_spaces sg); 2258 2259(*****************************************************************************) 2260(* install plus a printing wrapper. *) 2261(*****************************************************************************) 2262fun install_and_print a = 2263 let val (kind,name) = dest_acl2def a 2264 val _ = (print kind; print " "; print name; print "\n") 2265 val th = snd(install a) 2266 val _ = print_thm th 2267 val _ = print "\n\n" 2268 in 2269 th 2270 end; 2271 2272(*****************************************************************************) 2273(* Union a list of lists *) 2274(*****************************************************************************) 2275fun union_flatten [] = [] 2276 | union_flatten (l::ll) = union l (union_flatten ll);; 2277 2278(*****************************************************************************) 2279(* Gets the symbol names from an ML S-expression *) 2280(*****************************************************************************) 2281fun get_package_strings(mlsym(_,s)) = [s] 2282 | get_package_strings(mlpair(p1,p2)) = 2283 union (get_package_strings p1) (get_package_strings p2) 2284 | get_package_strings _ = []; 2285 2286(*****************************************************************************) 2287(* Match a defun -- identity function if match succeeds *) 2288(*****************************************************************************) 2289fun match_defun full_acl2_name mlsexp = 2290 case mlsexp 2291 of (mlpair(mlsym("COMMON-LISP", "DEFUN"), 2292 mlpair(mlsym(pkg, sym), _))) 2293 => if (pkg, sym) = split_acl2_name full_acl2_name 2294 then mlsexp 2295 else raise err "match_defun" 2296 ("bad match: (\"" ^ pkg ^ "\",\"" ^ sym ^ "\")") 2297 | _ => raise err "match_defun" 2298 ("bad case match: " ^ full_acl2_name); 2299 2300(*****************************************************************************) 2301(* Match a defaxiom -- identity function if match succeeds *) 2302(*****************************************************************************) 2303fun match_defaxiom full_acl2_name mlsexp = 2304 case mlsexp 2305 of (mlpair(mlsym("ACL2", "DEFAXIOM"), 2306 mlpair(mlsym(pkg, sym), _))) 2307 => if (pkg, sym) = split_acl2_name full_acl2_name 2308 then mlsexp 2309 else raise err "match_defaxiom" 2310 ("bad match: (\"" ^ pkg ^ "\",\"" ^ sym ^ "\")") 2311 | _ => raise err "match_defaxiom" 2312 ("bad case match: " ^ full_acl2_name); 2313 2314(*****************************************************************************) 2315(* Match a defthm -- identity function if match succeeds *) 2316(*****************************************************************************) 2317fun match_defthm full_acl2_name mlsexp = 2318 case mlsexp 2319 of (mlpair(mlsym("ACL2", "DEFTHM"), 2320 mlpair(mlsym(pkg, sym), _))) 2321 => if (pkg, sym) = split_acl2_name full_acl2_name 2322 then mlsexp 2323 else raise err "match_defthm" 2324 ("bad match: (\"" ^ pkg ^ "\",\"" ^ sym ^ "\")") 2325 | _ => raise err "match_defthm" 2326 ("bad case match: " ^ full_acl2_name); 2327 2328(*****************************************************************************) 2329(* Run a command returning true if it was successful. *) 2330(* This is a nasty hack to ensure this file works in both MoscowML *) 2331(* and PolyML. My apologies. *) 2332(*****************************************************************************) 2333 2334fun run_with_test string = 2335 (Process.system (string ^ "&& touch success") ; 2336 can FileSys.remove "success"); 2337 2338(*****************************************************************************) 2339(* Print a list of ACL2 DEFUNs to a file defun-tmp.lisp, *) 2340(* then run a2ml to create defun-tmp.ml. *) 2341(*****************************************************************************) 2342 2343fun print_defuns_to_mlsexps ql = 2344 let val sl = map preterm_to_string ql 2345 val _ = print_lisp_file "defun-tmp" (fn pr => map pr sl) 2346in 2347 if not (run_with_test 2348 (a2ml ^ " defun-tmp.lisp defun-tmp.ml >& defun-tmp.log")) 2349 then (print "a2ml defun-tmp.lisp defun-tmp.ml: Failed\n"; 2350 print "\n"; 2351 err "print_defuns_to_mlsexs" "a2ml failed") else 2352 () 2353 end; 2354 2355(*****************************************************************************) 2356(* Create a script file for a theory named thy that contains ACL2 DEFUNs ql *) 2357(* and hol names specified in an alist name_alist *) 2358(*****************************************************************************) 2359fun print_acl2_defun_script thy ql name_alist= 2360 let val outstr = TextIO.openOut("header-tmp.ml") 2361 fun out s = TextIO.output(outstr,s) 2362 in 2363 out("(* File created from HOL using print_acl2_defun_script on " 2364 ^ date() ^ " *)\n\n"); 2365 out "open HolKernel Parse boolLib bossLib;\n"; 2366 out "open stringLib complex_rationalTheory gcdTheory sexp sexpTheory;\n"; 2367 out ("val _ = new_theory \"" ^ thy ^ "\";"); 2368 out "\n\n"; 2369 out "val name_alist = \n"; 2370 out(string_pair_list_to_string name_alist); 2371 out ";\n\n"; 2372 TextIO.flushOut outstr; 2373 TextIO.closeOut outstr; 2374 print_defuns_to_mlsexps ql; 2375 Process.system 2376 ("cat header-tmp.ml defun-tmp.ml end-boilerplate.ml > " 2377 ^ thy ^ "Script.sml") 2378 end; 2379 2380(*****************************************************************************) 2381(* Read contents of acl2_list_ref (which should be set by slurping in *) 2382(* ACL2 stuff), convert to tagged theorems and put the results in *) 2383(* imported_acl2_theorems (an assignable variable). *) 2384(* *) 2385(* The protocol for using this is: *) 2386(* *) 2387(* use (Globals.HOLDIR ^ "/examples/acl2/..."); *) 2388(* load_imported_acl2_theorems(); *) 2389(*****************************************************************************) 2390val imported_acl2_theorems = ref([]:thm list); 2391 2392fun load_imported_acl2_theorems () = 2393 let val acl2_package_strings = 2394 union_flatten 2395 (mapfilter 2396 (get_package_strings o match_defaxiom "ACL2::ACL2-PACKAGE") 2397 (!acl2_list_ref)) 2398 val string_abbrev_count = length(!string_abbrevs) 2399 in 2400 print "Making string abbreviations ...\n"; 2401 make_string_abbrevs acl2_package_strings; 2402 print(Int.toString(length(!string_abbrevs)-string_abbrev_count)); 2403 print " new string abbreviations made\n"; 2404 show_tags := true; 2405 print "read "; print(Int.toString(length(!acl2_list_ref))); print " defs\n"; 2406 imported_acl2_theorems := 2407 map (install_and_print o mk_acl2def) (!acl2_list_ref); 2408 print 2409 "Imported ACL2 stored in assignable variable imported_acl2_theorems.\n\n" 2410 end; 2411 2412(*****************************************************************************) 2413(* Print imported imported_acl2_thms, assumed installed in theory named *) 2414(* theory name, for round-trip test. *) 2415(*****************************************************************************) 2416fun print_imported_acl2_theorems theory_name file_name = 2417 let val defs = 2418 mapfilter 2419 dest_option 2420 (map (dest_acl2_thm o snd) (theorems theory_name)) 2421 in 2422 print_lisp_file 2423 file_name 2424 (fn out => map (print_acl2def out) defs) 2425 end; 2426 2427fun print_thms_to_defthms name_thm_list file_name = 2428 let val defs = map thm_to_defthm name_thm_list 2429 in 2430 print_lisp_file 2431 file_name 2432 (fn out => map (print_acl2def out) defs) 2433 end; 2434 2435(*****************************************************************************) 2436(* Add theory load time code to restore binding of acl2_simps in theory *) 2437(*****************************************************************************) 2438fun save_acl2_simps () = 2439 adjoin_to_theory 2440 {sig_ps = NONE, 2441 struct_ps = 2442 SOME(fn ppstrm => 2443 PP.add_string ppstrm 2444 ("val _ = (sexp.acl2_simps :=" 2445 ^" (!sexp.acl2_simps)@(Drule.CONJUNCTS ACL2_SIMPS));")) 2446 }; 2447 2448(*****************************************************************************) 2449(* Add theory load time code to restore binding of current_package in theory *) 2450(*****************************************************************************) 2451fun save_current_package() = 2452 adjoin_to_theory 2453 {sig_ps = NONE, 2454 struct_ps = 2455 SOME(fn ppstrm => 2456 PP.add_string ppstrm 2457 ("val _ = sexp.set_current_package \"" 2458 ^ (!current_package) ^ "\";")) 2459 }; 2460 2461(*****************************************************************************) 2462(* Add theory load time code to restore binding of acl2_names in theory. *) 2463(*****************************************************************************) 2464fun save_acl2_names () = 2465 adjoin_to_theory 2466 {sig_ps = NONE, 2467 struct_ps = 2468 SOME(fn ppstrm => 2469 PP.add_string ppstrm 2470 ("val _ = sexp.add_acl2_names " ^ 2471 string_pair_list_to_string(!acl2_names) ^ 2472 ";")) 2473 }; 2474 2475 2476(*****************************************************************************) 2477(* Add theory load time code to restore binding of string_abbrevs in theory *) 2478(*****************************************************************************) 2479fun save_string_abbrevs () = 2480 adjoin_to_theory 2481 {sig_ps = NONE, 2482 struct_ps = 2483 SOME(fn ppstrm => 2484 PP.add_string ppstrm 2485 ("val _ = sexp.add_string_abbrevs " ^ 2486 string_abbrevs_to_string(!string_abbrevs) ^ 2487 ";\n\n")) 2488 }; 2489 2490(*****************************************************************************) 2491(* Save the acl2_simps, current_package, acl2_names, acl2_hol_names, *) 2492(* string_abbrevs then export theory. *) 2493(*****************************************************************************) 2494fun export_acl2_theory () = 2495 (save_thm("ACL2_SIMPS", LIST_CONJ(!acl2_simps)); 2496 save_acl2_simps(); 2497 save_current_package(); 2498 save_acl2_names(); 2499 save_string_abbrevs(); 2500 export_theory()); 2501 2502(*****************************************************************************) 2503(* List of events processed. If two events with the same name occur then the *) 2504(* second one is ignored. *) 2505(*****************************************************************************) 2506 2507(*****************************************************************************) 2508(* Accumulate events and discard repeats *) 2509(*****************************************************************************) 2510(* Old version 2511val event_names = ref([] : string list); 2512 2513fun accumulate_discard_events [] = [] 2514 | accumulate_discard_events 2515 ((ev as (mlpair(_,mlpair(mlsym(_,ev_name),_)))) :: evl) = 2516 if mem ev_name (!event_names) 2517 then accumulate_discard_events evl 2518 else (event_names := ev_name :: (!event_names); 2519 ev :: accumulate_discard_events evl) 2520 | accumulate_discard_events (ev :: l) = 2521 (pr_mlsexp ev; 2522 err "accumulate_and_discard_events" "bad event"); 2523 2524fun accumulate_discard_events [] = [] 2525 | accumulate_discard_events (ev :: evl) = 2526 if is_mldefun ev 2527 then 2528 let val (ev_sym,vs,bdy) = dest_mldefun ev 2529 val (pkg,ev_name) = dest_mlsym ev_sym 2530 in if mem ev_name (!event_names) 2531 then accumulate_discard_events evl 2532 else (event_names := ev_name :: (!event_names); 2533 ev :: accumulate_discard_events evl) 2534 end else 2535 if is_mlmutual ev (* WRONG! *) 2536 then ev :: accumulate_discard_events evl else 2537 if is_mldefthm ev 2538 then 2539 let val (ev_sym,bdy) = dest_mldefthm ev 2540 val (pkg,ev_name) = dest_mlsym ev_sym 2541 in if mem ev_name (!event_names) 2542 then accumulate_discard_events evl 2543 else (event_names := ev_name :: (!event_names); 2544 ev :: accumulate_discard_events evl) 2545 end else 2546 if is_mlinclude ev 2547 then (print "accumulate_and_discard_events shouldn't encounter "; 2548 print "INCLUDE-BOOK events, but it encountered:\n"; 2549 pr_mlsexp ev; 2550 err "accumulate_and_discard_events" "bad event (INCLUDE-BOOK)") 2551 else 2552 (print "Bad event:\n"; pr_mlsexp ev; 2553 err "accumulate_and_discard_events" "bad event"); 2554*) 2555 2556 2557(*****************************************************************************) 2558(* Test if a list xl contains an element eq_fun to x *) 2559(*****************************************************************************) 2560fun remove_duplicates eq_fn [] = [] 2561 | remove_duplicates eq_fn (x :: xl) = 2562 x :: remove_duplicates eq_fn (op_set_diff eq_fn xl [x]); 2563 2564(* 2565remove_duplicates (fn x => fn y => (fst x = fst y)) [(1,1),(2,2),(1,3),(4,4)]; 2566*) 2567 2568(*****************************************************************************) 2569(* Test equality of events *) 2570(*****************************************************************************) 2571fun event_name ev = 2572 if is_mldefun ev 2573 then #1(dest_mldefun ev) else 2574 if is_mldefun_sk ev 2575 then #1(dest_mldefun_sk ev) else 2576 if is_mldefaxiom ev 2577 then #1(dest_mldefaxiom ev) else 2578 if is_mlmutual ev 2579 then event_name(hd(dest_mlmutual ev)) else 2580 if is_mldefthm ev 2581 then #1(dest_mldefthm ev) else 2582 if is_mlinclude ev 2583 then mlsym((!current_package), dest_mlinclude ev) else 2584 (print "Unhandled arg to event_name\n"; 2585 pr_mlsexp ev; print "\n"; 2586 err "event_name" "unhandled arg"); 2587 2588(*****************************************************************************) 2589(* Test equality of events *) 2590(*****************************************************************************) 2591(* Old version 2592fun event_eq ev ev' = 2593 if is_mldefun ev 2594 then is_mldefun ev' andalso 2595 (#1(dest_mldefun ev) = #1(dest_mldefun ev')) else 2596 if is_mldefun_sk ev 2597 then is_mldefun_sk ev' andalso 2598 (#1(dest_mldefun_sk ev) = #1(dest_mldefun_sk ev')) else 2599 if is_mldefaxiom ev 2600 then is_mldefaxiom ev' andalso 2601 (#1(dest_mldefaxiom ev) = #1(dest_mldefaxiom ev')) else 2602 if is_mlmutual ev 2603 then is_mlmutual ev' andalso 2604 null(op_set_diff event_eq (dest_mlmutual ev) (dest_mlmutual ev')) andalso 2605 null(op_set_diff event_eq (dest_mlmutual ev') (dest_mlmutual ev)) else 2606 if is_mldefthm ev 2607 then is_mldefthm ev' andalso 2608 (#1(dest_mldefthm ev) = #1(dest_mldefthm ev')) else 2609 if is_mlinclude ev 2610 then is_mlinclude ev' andalso 2611 (dest_mlinclude ev = dest_mlinclude ev') 2612 else 2613 (print "Unhandled args to event_eq:\n"; 2614 pr_mlsexp ev; print "\n"; 2615 pr_mlsexp ev'; 2616 err "event_eq" "unhandled args"); 2617*) 2618 2619fun discard_duplicate_events evl = 2620(print "Discarding duplicated events.\n"; 2621 remove_duplicates (fn ev => fn ev' => event_name ev = event_name ev') evl); 2622 2623end