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