equal
deleted
inserted
replaced
38 val is_chain: state -> bool |
38 val is_chain: state -> bool |
39 val assert_forward: state -> state |
39 val assert_forward: state -> state |
40 val assert_forward_or_chain: state -> state |
40 val assert_forward_or_chain: state -> state |
41 val assert_backward: state -> state |
41 val assert_backward: state -> state |
42 val assert_no_chain: state -> state |
42 val assert_no_chain: state -> state |
43 val atp_hook: (ProofContext.context * Thm.thm -> unit) ref |
43 val atp_hook: (context * thm -> unit) ref |
44 val enter_forward: state -> state |
44 val enter_forward: state -> state |
|
45 val show_main_goal: bool ref |
45 val verbose: bool ref |
46 val verbose: bool ref |
46 val show_main_goal: bool ref |
47 val depth_of: state -> int |
47 val pretty_state: int -> state -> Pretty.T list |
48 val pretty_state: int -> state -> Pretty.T list |
48 val pretty_goals: bool -> state -> Pretty.T list |
49 val pretty_goals: bool -> state -> Pretty.T list |
49 val level: state -> int |
50 val level: state -> int |
50 type method |
51 type method |
51 val method: (thm list -> tactic) -> method |
52 val method: (thm list -> tactic) -> method |
380 |
381 |
381 |
382 |
382 (** pretty_state **) |
383 (** pretty_state **) |
383 |
384 |
384 val show_main_goal = ref false; |
385 val show_main_goal = ref false; |
385 |
|
386 val verbose = ProofContext.verbose; |
386 val verbose = ProofContext.verbose; |
|
387 |
|
388 |
|
389 fun depth_of (State (_, nodes)) = length nodes div 2 - 1; |
387 |
390 |
388 val pretty_goals_local = Display.pretty_goals_aux o ProofContext.pp; |
391 val pretty_goals_local = Display.pretty_goals_aux o ProofContext.pp; |
389 |
392 |
390 fun pretty_facts _ _ NONE = [] |
393 fun pretty_facts _ _ NONE = [] |
391 | pretty_facts s ctxt (SOME ths) = |
394 | pretty_facts s ctxt (SOME ths) = |
392 [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""]; |
395 [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""]; |
393 |
396 |
394 fun pretty_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, nodes)) = |
397 fun pretty_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, _)) = |
395 let |
398 let |
396 val ref (_, _, begin_goal) = Display.current_goals_markers; |
399 val ref (_, _, begin_goal) = Display.current_goals_markers; |
397 |
400 |
398 fun levels_up 0 = "" |
401 fun levels_up 0 = "" |
399 | levels_up 1 = ", 1 level up" |
402 | levels_up 1 = ", 1 level up" |
420 else if mode = Backward then ProofContext.pretty_asms ctxt |
423 else if mode = Backward then ProofContext.pretty_asms ctxt |
421 else []; |
424 else []; |
422 |
425 |
423 val prts = |
426 val prts = |
424 [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ |
427 [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ |
425 (if ! verbose then ", depth " ^ string_of_int (length nodes div 2 - 1) |
428 (if ! verbose then ", depth " ^ string_of_int (depth_of state) |
426 else "")), Pretty.str ""] @ |
429 else "")), Pretty.str ""] @ |
427 (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @ |
430 (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @ |
428 (if ! verbose orelse mode = Forward then |
431 (if ! verbose orelse mode = Forward then |
429 (pretty_facts "" ctxt facts @ prt_goal (find_goal state)) |
432 (pretty_facts "" ctxt facts @ prt_goal (find_goal state)) |
430 else if mode = ForwardChain then pretty_facts "picking " ctxt facts |
433 else if mode = ForwardChain then pretty_facts "picking " ctxt facts |