1(*---------------------------------------------------------------------------*)
2(* The programs here maintain a reference to an element of the proofs type.  *)
3(* For purely functional operations, i.e., where no hidden state is being    *)
4(* maintained, see the Manager structure.                                    *)
5(*---------------------------------------------------------------------------*)
6
7structure proofManagerLib :> proofManagerLib =
8struct
9
10open HolKernel Abbrev;
11
12type proof = Manager.proof
13type proofs = Manager.proofs
14
15val chatting = goalStack.chatting;
16fun say s = if !chatting then Lib.say s else ();
17
18val the_proofs = ref (Manager.initial_proofs());
19
20fun proofs() = !the_proofs;
21fun top_proof() = Manager.current_proof(proofs());
22
23
24fun new_goalstack g f =
25   (the_proofs := Manager.add (Manager.new_goalstack g f) (proofs());
26    proofs());
27
28fun new_goaltree g =
29   (the_proofs := Manager.add (Manager.new_goaltree g) (proofs());
30    proofs());
31
32fun set_goal g = new_goalstack g Lib.I;
33fun set_goaltree g = new_goaltree g;
34
35fun g q = set_goal([],Parse.Term q);
36fun gt q = set_goaltree([],Parse.Term q);
37
38fun add g = (say"Adding new proof..\n";
39             the_proofs := Manager.add g (proofs());
40             proofs());
41
42fun backup () =
43   (the_proofs := Manager.hd_opr Manager.backup (proofs());
44    top_proof());
45
46fun restore () =
47   (the_proofs := Manager.hd_opr Manager.restore (proofs());
48    top_proof());
49
50fun save () =
51   (the_proofs := Manager.hd_opr Manager.save (proofs());
52    top_proof());
53
54val b = backup;
55
56fun set_backup i =
57  (the_proofs := Manager.hd_opr (Manager.set_backup i) (proofs()));
58
59fun forget_history () =
60  (the_proofs := Manager.hd_opr (Manager.forget_history) (proofs()));
61
62fun restart() =
63   (the_proofs := Manager.hd_opr Manager.restart (proofs());
64    top_proof());
65
66local fun primdrop() = (the_proofs := Manager.drop (proofs()));
67in
68fun drop() = (primdrop(); say"OK..\n"; proofs())
69        handle Manager.NO_PROOFS => proofs()
70fun dropn i =
71   if i<1 then (say"OK..\n"; proofs()) else (primdrop(); dropn (i-1))
72   handle Manager.NO_PROOFS => proofs()
73end;
74
75fun drop_all () =
76    (the_proofs := Manager.initial_proofs(); !the_proofs)
77
78fun expandf tac =
79   (say "OK..\n";
80    the_proofs := Manager.hd_opr (Manager.expandf tac) (proofs());
81    top_proof())
82  handle e => Raise e;
83
84fun expand tac =
85   (say "OK..\n";
86    the_proofs := Manager.hd_opr (Manager.expand tac) (proofs());
87    top_proof())
88  handle e => Raise e;
89
90fun expand_listf ltac =
91   (say "OK..\n";
92    the_proofs := Manager.hd_opr (Manager.expand_listf ltac) (proofs());
93    top_proof())
94  handle e => Raise e;
95
96fun expand_list ltac =
97   (say "OK..\n";
98    the_proofs := Manager.hd_opr (Manager.expand_list ltac) (proofs());
99    top_proof())
100  handle e => Raise e;
101
102fun expandv (s,tac) =
103   (say "OK..\n";
104    the_proofs := Manager.hd_opr (Manager.expandv (s,tac)) (proofs());
105    top_proof())
106  handle e => Raise e;
107
108val elt = expand_list ;
109fun eall tac = expand_list (Tactical.ALLGOALS tac) ;
110fun eta tac = expand_list (Tactical.TRYALL tac) ;
111fun enth tac i = expand_list (Tactical.NTH_GOAL tac i) ;
112val e = expand;
113val et = expandv;
114
115val top_thm      = Manager.hd_proj Manager.top_thm o proofs;
116val initial_goal = Manager.hd_proj Manager.initial_goal o proofs;
117val top_goal     = Manager.hd_proj Manager.top_goal o proofs;
118val top_goals    = Manager.hd_proj Manager.top_goals o proofs;
119
120fun p () = Manager.hd_proj I (proofs())
121        handle Manager.NO_PROOFS =>
122         (say "No goalstack is currently being managed.\n";
123          raise mk_HOL_ERR "proofManagerLib" "p" "")
124
125val status = proofs;
126
127fun flatn i =
128  (the_proofs := Manager.hd_opr (Manager.flatn i) (proofs());
129   top_proof());
130
131fun rotate i =
132  (the_proofs := Manager.hd_opr (Manager.rotate i) (proofs());
133   top_proof());
134
135val r = rotate;
136
137fun rotate_proofs i =
138   (the_proofs := Manager.rotate_proofs i (proofs());
139    proofs());
140
141val R = rotate_proofs;
142
143val set_goal_pp  = Manager.set_goal_pp
144val std_goal_pp  = Manager.std_goal_pp
145
146val pp_proof = Manager.pp_proof
147val pp_proofs = Manager.pp_proofs
148
149end (* proofManagerLib *)
150