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