1structure Manager :> Manager =
2struct
3
4open Feedback Lib History Abbrev;
5
6val ERR = mk_HOL_ERR "Manager";
7
8(*---------------------------------------------------------------------------*)
9(*  Add a notion of undo to the two kinds of proof manager                   *)
10(*---------------------------------------------------------------------------*)
11
12datatype proof = GOALSTACK of goalStack.gstk history
13               | GOALTREE of goalTree.gtree history;
14
15fun is_goalstack (GOALSTACK _) = true
16  | is_goalstack otherwise = false;
17
18fun is_goaltree (GOALTREE _) = true
19  | is_goaltree otherwise = false;
20
21(*---------------------------------------------------------------------------*)
22(* Lists of proof attempts.                                                  *)
23(*---------------------------------------------------------------------------*)
24
25datatype proofs = PRFS of proof list;
26
27exception NO_PROOFS;
28
29fun initial_proofs() = PRFS[];
30
31fun add p (PRFS L) = PRFS (p::L);
32
33fun drop (PRFS (_::rst)) = PRFS rst
34  | drop (PRFS []) = raise NO_PROOFS;
35
36fun current_proof (PRFS (p::_)) = p
37  | current_proof (PRFS []) = raise NO_PROOFS;
38
39fun rotl (a::rst) = rst@[a]
40  | rotl [] = raise ERR "rotl" "empty list"
41
42fun rotate_proofs i (PRFS []) = PRFS []
43  | rotate_proofs i (PRFS L) =
44      if i<0 then raise ERR "rotate_proofs" "negative rotation"
45      else if i > length L
46           then raise ERR "rotate_proofs" "more rotations than proofs"
47           else PRFS(funpow i rotl L);
48
49(*---------------------------------------------------------------------------*)
50(* Operations on PRFS.                                                       *)
51(*---------------------------------------------------------------------------*)
52
53fun hd_opr f (PRFS (p::t)) = PRFS(f p::t)
54  | hd_opr f otherwise = raise NO_PROOFS;
55
56fun hd_proj f (PRFS (p::_)) = f p
57  | hd_proj f otherwise = raise NO_PROOFS;
58
59
60(*---------------------------------------------------------------------------*)
61(* Common operations on managers.                                            *)
62(*---------------------------------------------------------------------------*)
63
64fun new_history_default obj = new_history{obj=obj, limit=15}
65fun new_goalstack g f = GOALSTACK(new_history_default (goalStack.new_goal g f));
66fun new_goaltree g  = GOALTREE(new_history_default (goalTree.new_gtree g));
67fun set_goal g = new_goalstack g Lib.I;  (* historical *)
68
69fun backup (GOALSTACK s) = GOALSTACK(undo s)
70  | backup (GOALTREE t) = GOALTREE(undo t);
71
72fun set_backup i (GOALSTACK s) = GOALSTACK(set_limit s i)
73  | set_backup i (GOALTREE t) = GOALTREE (set_limit t i);
74
75fun restore (GOALSTACK s) = GOALSTACK(History.restore s)
76  | restore (GOALTREE  t) = GOALTREE (History.restore t);
77
78fun save (GOALSTACK s) = GOALSTACK(History.save s)
79  | save (GOALTREE t) = GOALTREE(History.save t);
80
81fun forget_history (GOALSTACK s) = GOALSTACK(remove_past s)
82  | forget_history (GOALTREE t) = GOALTREE (remove_past t);
83
84fun expandf tac (GOALSTACK s) = GOALSTACK (apply (goalStack.expandf tac) s)
85  | expandf _ _ = raise ERR "expandf" "not implemented for goal trees";
86
87fun expand tac (GOALSTACK s) = GOALSTACK (apply (goalStack.expand tac) s)
88  | expand tac (GOALTREE t) = GOALTREE (apply (goalTree.expand("",tac)) t);
89
90fun expand_listf ltac (GOALSTACK s) =
91    GOALSTACK (apply (goalStack.expand_listf ltac) s)
92  | expand_listf _ _ =
93    raise ERR "expand_listf" "not implemented for goal trees";
94
95fun expand_list ltac (GOALSTACK s) =
96    GOALSTACK (apply (goalStack.expand_list ltac) s)
97  | expand_list _ _ =
98    raise ERR "expand_list" "not implemented for goal trees";
99
100fun expandv (s,tac) (GOALTREE t) =
101     GOALTREE (apply (goalTree.expand (s,tac)) t)
102   | expandv _ _ = raise ERR "expandv" "not implemented for goal stacks";
103
104fun top_thm (GOALSTACK s) = project goalStack.extract_thm s
105  | top_thm (GOALTREE _) = raise ERR "top_thm" "not implemented for goal trees";
106
107fun initial_goal (GOALSTACK s) = project goalStack.initial_goal s
108  | initial_goal (GOALTREE t) = goalTree.first_goal (History.initialValue t);
109
110fun finalizer (GOALSTACK s) = project goalStack.finalizer s
111  | finalizer gtree = raise ERR "finalizer" "not implemented for goal trees";
112
113fun top_goal (GOALSTACK s) = project goalStack.top_goal s
114  | top_goal (GOALTREE t) = project goalTree.first_goal t;
115
116fun top_goals (GOALSTACK s) = project goalStack.top_goals s
117  | top_goals (GOALTREE t) = project goalTree.all_goals t;
118
119fun rotate i (GOALSTACK s) = GOALSTACK(apply (C goalStack.rotate i) s)
120  | rotate i (GOALTREE t) = raise ERR "rotate"
121                               "not implemented for goal trees";
122
123fun flatn i (GOALSTACK s) = GOALSTACK(apply (C goalStack.flatn i) s)
124  | flatn i (GOALTREE t) = raise ERR "flatn"
125                               "not implemented for goal trees";
126
127fun restart (GOALSTACK s) = GOALSTACK (new_history_default (initialValue s))
128  | restart (GOALTREE t) = GOALTREE (new_history_default (initialValue t));
129
130(*---------------------------------------------------------------------------*)
131(* Prettyprinting of goalstacks and goaltrees.                               *)
132(*---------------------------------------------------------------------------*)
133
134fun pp_proof (GOALSTACK s) = project goalStack.pp_gstk s
135  | pp_proof (GOALTREE t) = project goalTree.pp_gtree t
136
137val set_goal_pp = goalStack.set_goal_pp;
138val std_goal_pp = goalStack.std_pp_goal;
139
140
141(*---------------------------------------------------------------------------
142 * Prettyprinting of proofs.
143 *---------------------------------------------------------------------------*)
144
145val enum = List.rev o Lib.enumerate 1;
146
147val inactive_stack = Lib.can goalStack.extract_thm
148val inactive_tree = null o goalTree.all_goals;
149
150val pp_proofs =
151   let open smpp
152       val pr_goal = lift goalStack.pp_goal
153       val pr_gtree = lift goalTree.pp_gtree
154       val pr_thm = lift Parse.pp_thm
155       fun pr1 ind (GOALSTACK x) =
156            if (project inactive_stack x)
157            then block Portable.CONSISTENT (2 + ind) (
158                   add_string"Completed goalstack:" >> add_break(1,0) >>
159                   pr_thm (project goalStack.extract_thm x)
160                 )
161            else
162              block Portable.CONSISTENT (2 + ind) (
163                   add_string"Incomplete goalstack:" >> add_break(1,0) >>
164                   block Portable.CONSISTENT 0 (
165                     add_string"Initial goal:" >> add_newline >>
166                     pr_goal (project goalStack.initial_goal x)
167                   ) >>
168                   (if (project goalStack.is_initial x) then nothing
169                    else
170                      add_newline >> add_newline >>
171                      add_string "Current goal:" >> add_break(1,0) >>
172                      pr_goal (project goalStack.top_goal x))
173              )
174         | pr1 ind (GOALTREE t) =
175            if (project inactive_tree t)
176            then
177              block Portable.CONSISTENT 2 (
178                   add_string"Completed goaltree:" >> add_break(1,0) >>
179                   project pr_gtree t
180              )
181            else
182              block Portable.CONSISTENT 2 (
183                  add_string"Incomplete goaltree:" >> add_break(1,0) >>
184                  add_string"Initial goal:" >> add_newline >>
185                  pr_gtree (History.initialValue t) >>
186                  add_newline >>
187                  add_string "Current goaltree:" >>
188                  add_break(1,0) >>
189                  project pr_gtree t
190              )
191
192       fun pr (PRFS extants) =
193          let
194            val len = length extants
195          in
196             if len = 0 then add_string"There are currently no proofs."
197             else
198               block Portable.CONSISTENT 2 (
199                 add_string("Proof manager status:") >> add_break(1,0) >>
200                 (case len of 1 => add_string "1 proof."
201                            | n => add_string(int_to_string n^" proofs."))
202               ) >> add_newline >>
203               pr_list
204                 (fn (i,x) =>
205                     let val num_s = Int.toString i ^ ". "
206                     in
207                       block Portable.CONSISTENT 0 (
208                         add_string num_s >> pr1 (size num_s) x
209                       )
210                     end
211                 ) (add_newline >> add_newline)
212                 (enum extants) >>
213               add_newline
214          end
215   in
216     fn pl => (block Portable.CONSISTENT 0 (pr pl))
217   end;
218
219val pp_proofs = Parse.mlower o pp_proofs
220
221end (* Manager *)
222