1(*---------------------------------------------------------------------------*) 2(* Goalstacks, with no idea of undo. *) 3(*---------------------------------------------------------------------------*) 4 5structure goalStack :> goalStack = 6struct 7 8open HolKernel Abbrev; 9 10infix 0 before; 11 12val ERR = mk_HOL_ERR "goalStack"; 13 14val show_nsubgoals = ref 10; 15val chatting = ref true; 16val show_stack_subgoal_count = ref true 17val print_fvs = ref false 18val print_goal_at_top = ref false; 19val reverse_assums = ref false; 20val print_number_assums = ref 1000000; 21val other_subgoals_pretty_limit = ref 100; 22 23val _ = register_trace ("Goalstack.howmany_printed_subgoals", show_nsubgoals, 24 10000); 25val _ = register_btrace("Goalstack.show_proved_subtheorems", chatting); 26val _ = register_btrace("Goalstack.show_stack_subgoal_count", 27 show_stack_subgoal_count); 28val _ = register_btrace("Goalstack.print_goal_fvs", print_fvs) 29val _ = register_btrace("Goalstack.print_goal_at_top", print_goal_at_top) 30val _ = register_btrace("Goalstack.print_assums_reversed", reverse_assums) 31val _ = register_trace ("Goalstack.howmany_printed_assums", 32 print_number_assums, 1000000) 33val _ = register_trace("Goalstack.other_subgoals_pretty_limit", 34 other_subgoals_pretty_limit, 100000) 35 36 37fun say s = if !chatting then Lib.say s else (); 38 39fun add_string_cr s = say (s^"\n") 40fun cr_add_string_cr s = say ("\n"^s^"\n") 41 42fun printthm th = if !chatting then say (Parse.thm_to_string th) else () 43 44fun rotl (a::rst) = rst@[a] 45 | rotl [] = raise ERR "rotl" "empty list" 46 47fun rotr lst = 48 let val (front,back) = Lib.front_last lst 49 in (back::front) 50 end 51 handle HOL_ERR _ => raise ERR "rotr" "empty list" 52 53fun goal_size (asl,t) = 54 List.foldl (fn (a,acc) => term_size a + acc) (term_size t) asl 55 56 57(* GOALSTACKS *) 58(*--------------------------------------------------------------------------- 59 * A goalstack is a stack of (goal list, validation_function) records. Each 60 * goal in the goal list is a (term list, term) pair. The validation 61 * function is a function from a list of theorems to a theorem. It must be 62 * that the number of goals in the goal list is equal to the number of 63 * formal parameters in the validation function. Unfortunately, the type 64 * system of ML is not strong enough to check that. 65 ---------------------------------------------------------------------------*) 66 67type tac_result = {goals : goal list, 68 validation : thm list -> thm} 69 70(*--------------------------------------------------------------------------- 71 Need both initial goal and final theorem in PROVED case, because 72 finalizer can take a theorem achieving the original goal and 73 transform it into a second theorem. Destructing that second theorem 74 wouldn't deliver the original goal. 75 ---------------------------------------------------------------------------*) 76 77datatype proposition = POSED of goal 78 | PROVED of thm * goal; 79 80datatype gstk = GSTK of {prop : proposition, 81 final : thm -> thm, 82 stack : tac_result list} 83 84 85fun depth(GSTK{stack,...}) = length stack; 86 87fun tac_result_size (tr : tac_result, acc) = 88 List.foldl (fn (g,acc) => goal_size g + acc) acc (#goals tr) 89 90fun gstk_size (GSTK{prop,stack,...}) = 91 case prop of 92 PROVED _ => 0 93 | POSED _ => List.foldl tac_result_size 0 stack 94 95fun is_initial(GSTK{prop=POSED g, stack=[], ...}) = true 96 | is_initial _ = false; 97 98fun top_goals(GSTK{prop=POSED g, stack=[], ...}) = [g] 99 | top_goals(GSTK{prop=POSED _, stack = ({goals,...}::_),...}) = goals 100 | top_goals(GSTK{prop=PROVED _, ...}) = raise ERR "top_goals" "no goals"; 101 102val top_goal = hd o top_goals; 103 104fun new_goal (g as (asl,w)) f = 105 if all (fn tm => type_of tm = bool) (w::asl) 106 then GSTK{prop=POSED g, stack=[], final=f} 107 else raise ERR "set_goal" "not a proposition; new goal not added"; 108 109fun finalizer(GSTK{final,...}) = final; 110 111fun initial_goal(GSTK{prop = POSED g,...}) = g 112 | initial_goal(GSTK{prop = PROVED (th,g),...}) = g; 113 114fun rotate(GSTK{prop=PROVED _, ...}) _ = 115 raise ERR "rotate" "goal has already been proved" 116 | rotate(GSTK{prop, stack, final}) n = 117 if n<0 then raise ERR"rotate" "negative rotations not allowed" 118 else 119 case stack 120 of [] => raise ERR"rotate" "No goals to rotate" 121 | {goals,validation}::rst => 122 if n > length goals 123 then raise ERR "rotate" 124 "More rotations than goals -- no rotation done" 125 else GSTK{prop=prop, final=final, 126 stack={goals=funpow n rotl goals, 127 validation=validation o funpow n rotr} :: rst}; 128 129local 130 fun imp_err s = 131 raise ERR "expandf or expand_listf" ("implementation error: "^s) 132 133 fun return(GSTK{stack={goals=[],validation}::rst, prop as POSED g,final}) = 134 let val th = validation [] 135 in case rst 136 of [] => 137 (let val thm = final th 138 in GSTK{prop=PROVED (thm,g), stack=[], final=final} 139 end 140 handle e as HOL_ERR _ 141 => (cr_add_string_cr "finalization failed"; raise e)) 142 | {goals = _::rst_o_goals, validation}::rst' => 143 ( cr_add_string_cr "Goal proved."; 144 printthm th; say "\n"; 145 return(GSTK{prop=prop, final=final, 146 stack={goals=rst_o_goals, 147 validation=fn thl => validation(th::thl)}::rst'}) 148 ) 149 | otherwise => imp_err (quote "return") 150 end 151 | return gstk = gstk 152 153 fun expand_msg dpth (GSTK{prop = PROVED _, ...}) = () 154 | expand_msg dpth (GSTK{prop, final, stack as {goals, ...}::_}) = 155 let val dpth' = length stack 156 in if dpth' > dpth 157 then if (dpth+1 = dpth') 158 then add_string_cr 159 (case (length goals) 160 of 0 => imp_err "1" 161 | 1 => "1 subgoal:" 162 | n => (int_to_string n)^" subgoals:") 163 else imp_err "2" 164 else cr_add_string_cr "Remaining subgoals:" 165 end 166 | expand_msg _ _ = imp_err "3" ; 167in 168fun expandf _ (GSTK{prop=PROVED _, ...}) = 169 raise ERR "expandf" "goal has already been proved" 170 | expandf tac (GSTK{prop as POSED g, stack,final}) = 171 let val arg = (case stack of [] => g | tr::_ => hd (#goals tr)) 172 val (glist,vf) = tac arg 173 val dpth = length stack 174 val gs = return(GSTK{prop=prop,final=final, 175 stack={goals=glist, validation=vf} :: stack}) 176 in expand_msg dpth gs ; gs end 177 178(* note - expand_listf, unlike expandf, replaces the top member of the stack *) 179fun expand_listf ltac (GSTK{prop=PROVED _, ...}) = 180 raise ERR "expand_listf" "goal has already been proved" 181 | expand_listf ltac (GSTK{prop as POSED g, stack = [], final}) = 182 expand_listf ltac (GSTK{prop = POSED g, 183 stack = [{goals = [g], validation = hd}], final = final}) 184 | expand_listf ltac (GSTK{prop, stack as {goals,validation}::rst, final}) = 185 let val (new_goals, new_vf) = ltac goals 186 val dpth = length stack - 1 (* because we don't augment the stack *) 187 val new_gs = return (GSTK{prop=prop, final=final, 188 stack={goals=new_goals, validation=validation o new_vf} :: rst}) 189 in expand_msg dpth new_gs ; new_gs end ; 190end ; 191 192fun expand tac gs = expandf (Tactical.VALID tac) gs; 193fun expand_list ltac gs = expand_listf (Tactical.VALID_LT ltac) gs; 194 195fun flat gstk = 196 case gstk of 197 GSTK{prop, 198 stack as {goals,validation} :: 199 {goals = g2 :: goals2, validation = validation2} :: 200 rst, 201 final} => 202 let 203 fun v thl = let 204 val (thl1, thl2) = Lib.split_after (length goals) thl 205 in 206 validation2 (validation thl1 :: thl2) 207 end 208 val newgv = {goals = goals @ goals2, validation = v} 209 in 210 GSTK {prop = prop, stack = newgv :: rst, final = final} 211 end 212 | _ => raise ERR "flat" "goalstack in wrong shape" 213 214fun flatn (GSTK{prop=PROVED _, ...}) n = 215 raise ERR "flatn" "goal has already been proved" 216 | flatn gstk 0 = gstk 217 | flatn (gstk as GSTK{prop, stack = [], final}) n = gstk 218 | flatn (gstk as GSTK{prop, stack as [_], final}) n = gstk 219 | flatn (gstk as GSTK{prop, stack, final}) n = flatn (flat gstk) (n-1) ; 220 221fun extract_thm (GSTK{prop=PROVED(th,_), ...}) = th 222 | extract_thm _ = raise ERR "extract_thm" "no theorem proved"; 223 224(* Prettyprinting *) 225 226local 227 228open Portable smpp 229fun ty2s ty = String.extract(Parse.type_to_string ty, 1, NONE) 230 231fun check_vars (g as (asl,w)) = 232 let 233 val fvs = FVL (w::asl) empty_tmset 234 fun foldthis (v,acc) = 235 let 236 val (nm,ty_s) = (I ## ty2s) (dest_var v) 237 in 238 case Binarymap.peek(acc, nm) of 239 NONE => Binarymap.insert(acc, nm, [ty_s]) 240 | SOME vs => Binarymap.insert(acc, nm, ty_s::vs) 241 end 242 val m = HOLset.foldl foldthis (Binarymap.mkDict String.compare) fvs 243 fun foldthis (nm,vtys,msg) = 244 if length vtys > 1 then 245 (" " ^ nm ^ " : " ^ String.concatWith ", " vtys) :: msg 246 else msg 247 val msg = Binarymap.foldl foldthis [] m 248 in 249 if null msg then nothing 250 else ( 251 add_newline >> add_newline >> 252 add_string ("WARNING: goal contains variables of same name \ 253 \but different types") >> 254 add_newline >> 255 List.foldl (fn (s,m) => m >> add_string s >> add_newline) 256 nothing 257 msg 258 ) 259 end 260val pr = lift Parse.pp_term 261fun min (a,b) = if a < b then a else b 262fun pr_numbered_assum (i,tm) = 263 let 264 val istr = StringCvt.padLeft #" " 2 (Int.toString i)^". " 265 in 266 block CONSISTENT 0 ( 267 add_string istr >> 268 block CONSISTENT (size istr) (pr tm) 269 ) 270 end 271fun pr_maybe_hidden_assum (SOME a) = pr_numbered_assum a 272 | pr_maybe_hidden_assum NONE = add_string "..." 273 274fun pr_assums asl = 275 let 276 val length_asl = length asl 277 val length_assums = min (length_asl, !print_number_assums) 278 val assums = List.rev (List.take (asl, length_assums)) 279 val l = Lib.enumerate (length_asl - length_assums) assums 280 val l = if !reverse_assums then List.rev l else l 281 val has = if !print_number_assums < length_asl then NONE :: map SOME l 282 else map SOME l 283 in 284 pr_list pr_maybe_hidden_assum add_newline has 285 end 286 287fun pr_v v = let 288 val (n, ty) = dest_var v 289in 290 block INCONSISTENT 2 ( 291 add_string n >> add_break(1,0) >> lift Parse.pp_type ty 292 ) 293end 294 295fun print_fvs0 fvs = 296 block CONSISTENT 0 ( 297 add_string "Free variables:" >> add_break(1,2) >> 298 block INCONSISTENT 0 (pr_list pr_v (add_break(3,0)) fvs) 299 ) 300fun print_goalfvs (asl,w) = 301 let 302 val fvs = free_varsl (w::asl) |> Listsort.sort Term.compare 303 in 304 if !print_fvs andalso not (null fvs) then 305 add_newline >> add_newline >> print_fvs0 fvs 306 else nothing 307 end 308 309val pr_goal = pr 310fun indent n p = add_string (CharVector.tabulate(n, fn _ => #" ")) >> 311 block CONSISTENT n p 312 313 314fun ppgoal_assums_first (g as (asl,w)) = 315 block CONSISTENT 0 ( 316 block CONSISTENT 0 (pr_assums asl) >> add_newline >> 317 add_string (!Globals.goal_line) >> add_newline >> 318 indent 5 (pr_goal w) >> 319 print_goalfvs g >> check_vars g 320 ) 321 322fun ppgoal_assums_last (g as (asl,w)) = 323 block CONSISTENT 0 ( 324 indent 5 (pr_goal w) >> add_newline >> 325 add_string (!Globals.goal_line) >> add_newline >> 326 block CONSISTENT 0 (pr_assums asl) >> 327 print_goalfvs g >> check_vars g 328 ) 329 330fun ppgoal (g as (asl,w)) = 331 if null asl then pr_goal w >> print_goalfvs g >> check_vars g 332 else 333 if !print_goal_at_top then ppgoal_assums_last g 334 else ppgoal_assums_first g 335 handle e => (Lib.say "\nError in attempting to print a goal!\n"; raise e); 336 337 val goal_printer = ref (Parse.mlower o ppgoal) 338in 339 val mppgoal = ppgoal 340 val std_pp_goal = Parse.mlower o ppgoal 341 val pp_goal = !goal_printer 342 fun set_goal_pp pp = !goal_printer before (goal_printer := pp) 343end; 344 345(* not clear that this function is used; certainly, default interactive system 346 uses Manager.sml's printer instead. *) 347fun pp_gstk gstk = 348 let open smpp 349 val pr_goal = mppgoal 350 fun pr (GSTK{prop = POSED g, stack = [], ...}) = 351 block Portable.CONSISTENT 0 ( 352 add_string"Initial goal:" >> add_newline >> add_newline >> 353 pr_goal g 354 ) 355 | pr (GSTK{prop = POSED _, stack = ({goals,...}::_), ...}) = 356 let val (ellipsis_action, goals_to_print) = 357 if length goals > !show_nsubgoals then 358 let val num_elided = length goals - !show_nsubgoals 359 in 360 (add_string ("..."^Int.toString num_elided ^ " subgoal"^ 361 (if num_elided = 1 then "" else "s") ^ 362 " elided...") >> 363 add_newline >> add_newline, 364 rev (List.take (goals, !show_nsubgoals))) 365 end 366 else 367 (add_newline, rev goals) 368 val (pfx,lastg) = front_last goals_to_print 369 fun start() = 370 (ellipsis_action >> 371 pr_list pr_goal (add_newline >> add_newline) pfx) 372 val size = List.foldl (fn (g,acc) => goal_size g + acc) 0 pfx 373 in 374 block Portable.CONSISTENT 0 ( 375 (if size > current_trace "Goalstack.other_subgoals_pretty_limit" 376 then 377 with_flag(Parse.current_backend, PPBackEnd.raw_terminal) 378 start() 379 else start()) >> 380 (if not (null pfx) then add_newline >> add_newline 381 else nothing) >> 382 pr_goal lastg >> 383 (if length goals > 1 andalso !show_stack_subgoal_count then 384 add_string ("\n\n" ^ Int.toString (length goals) ^ 385 " subgoals")>> 386 add_newline 387 else add_newline >> add_newline) 388 ) 389 end 390 | pr (GSTK{prop = PROVED (th,_), ...}) = 391 block Portable.CONSISTENT 0 ( 392 add_string "Initial goal proved." >> 393 add_newline >> 394 lift Parse.pp_thm th 395 ) 396 in 397 pr gstk 398 end 399 400val pp_gstk = Parse.mlower o pp_gstk 401 402fun print_tac pfx g = let 403in 404 print pfx; 405 HOLPP.prettyPrint(print,!Globals.linewidth) (pp_goal g); 406 Tactical.ALL_TAC g 407end 408 409end (* goalStack *) 410