1 2(* Commands when run interactively: 3quietdec := true; 4loadPath := (Globals.HOLDIR ^ "/examples/acl2/ml") :: !loadPath; 5map load ["sexp","sexpTheory","hol_defaxiomsTheory"]; 6open fracTheory ratTheory complex_rationalTheory 7 sexp sexpTheory hol_defaxiomsTheory; 8 9printDepth := 10000; 10printLength := 10000; 11 12quietdec := false; 13*) 14 15structure load_book :> load_book = 16struct 17 18 19 20(*****************************************************************************) 21(* Boilerplate needed for compilation *) 22(*****************************************************************************) 23 24open HolKernel Parse boolLib bossLib pred_setTheory pred_setLib; 25 26open fracTheory ratTheory sexp complex_rationalTheory sexpTheory 27 hol_defaxiomsTheory; 28 29(*****************************************************************************) 30(* END BOILERPLATE *) 31(*****************************************************************************) 32 33val load_simp_fn = 34 SIMP_RULE 35 list_ss 36 ([let_simp,andl_fold,itel_fold,itel_append, 37 forall2_thm,exists2_thm,forall_fold,exists_fold, 38 implies,andl_simp,not_simp,t_nil] 39 @ 40 (map GSYM [int_def,nat_def,List_def,asym_def,csym_def,ksym_def,osym_def])); 41 42fun get_acl2_thm s = load_simp_fn(DB.fetch "imported_acl2" (s ^ "_thm")); 43 44(*****************************************************************************) 45(* load a book after recursively loading included books *) 46(*****************************************************************************) 47fun load_book (load_fn:string->unit) (simp_fn:thm->thm) book_name = 48 let val _ = load_fn(book_name ^ ".ml") 49 val acl2_list = !acl2_list_ref 50 val install_fn = (I ## simp_fn) o install o mk_acl2def 51 in 52 if is_mlinclude(hd acl2_list) 53 then let val thll = 54 load_book load_fn simp_fn (dest_mlinclude(hd acl2_list)) 55 val thl = 56 map install_fn (accumulate_discard_events(tl acl2_list)) 57 in 58 thll @ [thl] 59 end 60 else [map install_fn (accumulate_discard_events acl2_list) 61 handle e => Raise e] 62 end; 63 64end 65