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