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