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 expandf tac =
76   (say "OK..\n";
77    the_proofs := Manager.hd_opr (Manager.expandf tac) (proofs());
78    top_proof())
79  handle e => Raise e;
80
81fun expand tac =
82   (say "OK..\n";
83    the_proofs := Manager.hd_opr (Manager.expand tac) (proofs());
84    top_proof())
85  handle e => Raise e;
86
87fun expand_listf ltac =
88   (say "OK..\n";
89    the_proofs := Manager.hd_opr (Manager.expand_listf ltac) (proofs());
90    top_proof())
91  handle e => Raise e;
92
93fun expand_list ltac =
94   (say "OK..\n";
95    the_proofs := Manager.hd_opr (Manager.expand_list ltac) (proofs());
96    top_proof())
97  handle e => Raise e;
98
99fun expandv (s,tac) =
100   (say "OK..\n";
101    the_proofs := Manager.hd_opr (Manager.expandv (s,tac)) (proofs());
102    top_proof())
103  handle e => Raise e;
104
105val elt = expand_list ;
106fun eall tac = expand_list (Tactical.ALLGOALS tac) ;
107fun eta tac = expand_list (Tactical.TRYALL tac) ;
108fun enth tac i = expand_list (Tactical.NTH_GOAL tac i) ;
109val e = expand;
110val et = expandv;
111
112val top_thm      = Manager.hd_proj Manager.top_thm o proofs;
113val initial_goal = Manager.hd_proj Manager.initial_goal o proofs;
114val top_goal     = Manager.hd_proj Manager.top_goal o proofs;
115val top_goals    = Manager.hd_proj Manager.top_goals o proofs;
116
117fun p () = Manager.hd_proj I (proofs())
118        handle Manager.NO_PROOFS =>
119         (say "No goalstack is currently being managed.\n";
120          raise mk_HOL_ERR "proofManagerLib" "p" "")
121
122val status = proofs;
123
124fun flatn i =
125  (the_proofs := Manager.hd_opr (Manager.flatn i) (proofs());
126   top_proof());
127
128fun rotate i =
129  (the_proofs := Manager.hd_opr (Manager.rotate i) (proofs());
130   top_proof());
131
132val r = rotate;
133
134fun rotate_proofs i =
135   (the_proofs := Manager.rotate_proofs i (proofs());
136    proofs());
137
138val R = rotate_proofs;
139
140val set_goal_pp  = Manager.set_goal_pp
141val std_goal_pp  = Manager.std_goal_pp
142
143val pp_proof = Manager.pp_proof
144val pp_proofs = Manager.pp_proofs
145
146end (* proofManagerLib *)
147