adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: improve wp tracing 

When tracing wp can now print the instantiated version of the rules being used.
It also says which set each used rule is from.
This commit is contained in:
Corey Lewis 2019-11-05 13:46:02 +11:00
parent 7107f9abaf
commit 5120e351b3
7 changed files with 127 additions and 67 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

88
lib/Monad_WP/wp/WP-method.ML
View File

@ -221,46 +221,65 @@ fun debug_get ctxt = WPData.get (Context.Proof ctxt);
fun get_rules ctxt extras = fold_rev add_rule extras (debug_get ctxt);
fun append_used_thm thm used_thms = used_thms := !used_thms @ [thm]
fun resolve_ruleset_tac' ctxt rs used_thms_ref n t =
let fun append_thm used_thm thm =
Seq.map (fn thm => (append_used_thm used_thm used_thms_ref; thm)) thm;
fun resolve_ruleset_tac' trace ctxt rs used_thms_ref n t =
let
val rtac = WP_Pre.rtac ctxt
fun trace_rtac tag rule = WP_Pre.trace_rule trace ctxt used_thms_ref tag rtac rule
in case
Thm.cprem_of t n |> Thm.term_of |> snd (#trips rs) (Thm.theory_of_thm t)
|> Envir.beta_eta_contract |> Logic.strip_assums_concl
handle THM _ => @{const True}
of Const (@{const_name Trueprop}, _) $
(Const (@{const_name triple_judgement}, _) $ _ $ f $ _) => let
val ts = Net.unify_term (#1 (#rules rs)) f |> order_list |> rev;
val combapps = Seq.maps (fn combapp => Seq.map
(fn combapp' => (combapp, combapp')) (resolve_tac ctxt [combapp] n t))
(Seq.of_list (#combs rs)) |> Seq.list_of |> Seq.of_list;
fun per_rule_tac t = (fn thm => append_thm t (resolve_tac ctxt [t] n thm)) ORELSE
(fn _ => Seq.maps (fn combapp => append_thm t
(append_thm (#1 combapp) (resolve_tac ctxt [t] n (#2 combapp)))) combapps);
in FIRST (map per_rule_tac ts) ORELSE
FIRST (map (fn split => fn thm => append_thm split (resolve_tac ctxt [split] n thm)) (#splits rs)) end t
| _ => FIRST (map (fn rule => fn thm => append_thm rule (resolve_tac ctxt [rule] n thm))
(map snd (#3 (#rules rs)) @ #splits rs)) t end;
(Const (@{const_name triple_judgement}, _) $ _ $ f $ _) =>
let
val rules = Net.unify_term (#1 (#rules rs)) f |> order_list |> rev;
fun per_rule_combapp_tac rule combapp =
let val insts_ref = Unsynchronized.ref (Trace_Schematic_Insts.empty_instantiations)
in WP_Pre.trace_rule' trace ctxt
(fn rule_insts => fn _ => insts_ref := rule_insts)
rtac combapp
THEN'
WP_Pre.trace_rule' trace ctxt
(fn rule_insts => fn _ =>
(WP_Pre.append_used_rule ctxt used_thms_ref "wp_comb" combapp (!insts_ref);
WP_Pre.append_used_rule ctxt used_thms_ref "wp" rule rule_insts))
rtac rule
end
fun per_rule_tac rule =
trace_rtac "wp" rule ORELSE'
FIRST' (map (per_rule_combapp_tac rule) (#combs rs))
in (FIRST' (map per_rule_tac rules) ORELSE'
FIRST' (map (trace_rtac "wp_split") (#splits rs))) n t
end
| _ => FIRST' (map (trace_rtac "wp") (map snd (#3 (#rules rs))) @
map (trace_rtac "wp_split") (#splits rs)) n t
end;
fun resolve_ruleset_tac ctxt rs used_thms_ref n =
(Apply_Debug.break ctxt (SOME "wp")) THEN (resolve_ruleset_tac' ctxt rs used_thms_ref n)
fun resolve_ruleset_tac trace ctxt rs used_thms_ref n =
(Apply_Debug.break ctxt (SOME "wp")) THEN (resolve_ruleset_tac' trace ctxt rs used_thms_ref n)
val wp_trace = Attrib.setup_config_bool @{binding wp_trace} (K false);
fun trace_used_thm ctxt (name, tag, prop) =
let val adjusted_name = ThmExtras.adjust_thm_name ctxt (name, NONE) prop
in Pretty.block
(ThmExtras.pretty_adjusted_name ctxt adjusted_name ::
[Pretty.str ("[" ^ tag ^ "]:"),Pretty.brk 1, Syntax.unparse_term ctxt prop])
end
fun trace_used_thms trace used_thms_ref ctxt =
if trace orelse Config.get ctxt wp_trace
then Pretty.big_list "Theorems used by wp:" (map (ThmExtras.pretty_thm false ctxt) (!used_thms_ref))
fun trace_used_thms trace ctxt used_thms_ref =
if trace
then Pretty.big_list "Theorems used by wp:"
(map (trace_used_thm ctxt) (!used_thms_ref))
|> Pretty.writeln
handle Size => warning ("WP tracing information was too large to print.")
else ();
fun warn_unsafe_rules unsafe_rules n ctxt t =
let val used_thms_dummy = Unsynchronized.ref [] : thm list Unsynchronized.ref;
let val used_thms_dummy = Unsynchronized.ref [] : (string * string * term) list Unsynchronized.ref;
val ctxt' = Config.put WP_Pre.wp_trace false ctxt
val useful_unsafe_rules =
filter (fn rule =>
(is_some o SINGLE (
resolve_ruleset_tac ctxt (get_rules ctxt [rule]) used_thms_dummy n)) t)
resolve_ruleset_tac false ctxt' (get_rules ctxt [rule]) used_thms_dummy n)) t)
unsafe_rules
in if not (null useful_unsafe_rules)
then Pretty.list "Unsafe theorems that could be used: \n" ""
@ -270,18 +289,19 @@ fun warn_unsafe_rules unsafe_rules n ctxt t =
fun apply_rules_tac_n trace ctxt extras n =
let
val rules = get_rules ctxt extras;
val used_thms_ref = Unsynchronized.ref [] : thm list Unsynchronized.ref
val wp_pre_tac = TRY (WP_Pre.tac (SOME used_thms_ref) ctxt 1)
val trace' = trace orelse Config.get ctxt WP_Pre.wp_trace
val used_thms_ref = Unsynchronized.ref [] : (string * string * term) list Unsynchronized.ref
val rules = get_rules ctxt extras
val wp_pre_tac = TRY (WP_Pre.tac trace' used_thms_ref ctxt 1)
val wp_fix_tac = TRY (WPFix.both_tac ctxt 1)
val cleanup_tac = TRY (REPEAT
(resolve_tac ctxt [@{thm TrueI}, @{thm conj_TrueI}, @{thm conj_TrueI2}] 1
ORELSE assume_tac ctxt 1))
val steps_tac = (CHANGED (REPEAT_DETERM (resolve_ruleset_tac ctxt rules used_thms_ref 1)))
val steps_tac = (CHANGED (REPEAT_DETERM (resolve_ruleset_tac trace' ctxt rules used_thms_ref 1)))
THEN cleanup_tac
in
SELECT_GOAL (
(fn t => Seq.map (fn thm => (trace_used_thms trace used_thms_ref ctxt;
(fn t => Seq.map (fn thm => (trace_used_thms trace' ctxt used_thms_ref;
used_thms_ref := []; thm))
((wp_pre_tac THEN wp_fix_tac THEN steps_tac) t))
THEN_ELSE
@ -293,9 +313,11 @@ fun apply_rules_tac trace ctxt extras = apply_rules_tac_n trace ctxt extras 1;
fun apply_once_tac trace ctxt extras t =
let
val used_thms_ref = Unsynchronized.ref [] : thm list Unsynchronized.ref;
in Seq.map (fn thm => (trace_used_thms trace used_thms_ref ctxt; thm))
(SELECT_GOAL (resolve_ruleset_tac ctxt (get_rules ctxt extras) used_thms_ref 1) 1 t)
val trace' = trace orelse Config.get ctxt WP_Pre.wp_trace
val used_thms_ref = Unsynchronized.ref [] : (string * string * term) list Unsynchronized.ref
val rules = get_rules ctxt extras
in Seq.map (fn thm => (trace_used_thms trace' ctxt used_thms_ref; thm))
(SELECT_GOAL (resolve_ruleset_tac trace' ctxt rules used_thms_ref 1) 1 t)
end
fun clear_rules ({combs, rules, trips, splits, unsafe_rules}) =

2
lib/Monad_WP/wp/WP.thy
View File

@ -37,7 +37,7 @@ lemma conj_TrueI2: "P \<Longrightarrow> P \<and> True" by simp
ML_file "WP-method.ML"
declare [[wp_trace = false]]
declare [[wp_trace = false, wp_trace_instantiation = false]]
setup WeakestPre.setup

47
lib/Monad_WP/wp/WP_Pre.thy
View File

@ -11,6 +11,7 @@
theory WP_Pre
imports
Main
"../../Trace_Schematic_Insts"
"HOL-Eisbach.Eisbach_Tools"
begin
@ -19,14 +20,33 @@ named_theorems wp_pre
ML \<open>
structure WP_Pre = struct
fun append_used_thm thm used_thms = used_thms := !used_thms @ [thm]
val wp_trace = Attrib.setup_config_bool @{binding wp_trace} (K false);
val wp_trace_instantiation =
Attrib.setup_config_bool @{binding wp_trace_instantiation} (K false);
fun pre_tac ctxt pre_rules used_ref_option i t = let
fun append_thm used_thm thm =
if Option.isSome used_ref_option
then Seq.map (fn thm => (append_used_thm used_thm (Option.valOf used_ref_option); thm)) thm
else thm;
fun apply_rule t thm = append_thm t (resolve_tac ctxt [t] i thm)
fun append_used_rule ctxt used_thms_ref tag used_thm insts =
let
val name = Thm.get_name_hint used_thm
val inst_term =
if Config.get ctxt wp_trace_instantiation
then Trace_Schematic_Insts.instantiate_thm ctxt used_thm insts
else Thm.prop_of used_thm
in used_thms_ref := !used_thms_ref @ [(name, tag, inst_term)] end
fun trace_rule' trace ctxt callback tac rule =
if trace
then Trace_Schematic_Insts.trace_schematic_insts_tac ctxt callback tac rule
else tac rule;
fun trace_rule trace ctxt used_thms_ref tag tac rule =
trace_rule' trace ctxt
(fn rule_insts => fn _ => append_used_rule ctxt used_thms_ref tag rule rule_insts)
tac rule;
fun rtac ctxt rule = resolve_tac ctxt [rule]
fun pre_tac trace ctxt pre_rules used_thms_ref i t = let
fun apply_rule t = trace_rule trace ctxt used_thms_ref "wp_pre" (rtac ctxt) t i
val t2 = FIRST (map apply_rule pre_rules) t |> Seq.hd
val etac = TRY o eresolve_tac ctxt [@{thm FalseE}]
fun dummy_t2 _ _ = Seq.single t2
@ -35,12 +55,17 @@ fun pre_tac ctxt pre_rules used_ref_option i t = let
then Seq.empty else Seq.single t2 end
handle Option => Seq.empty
fun tac used_ref_option ctxt = let
fun tac trace used_thms_ref ctxt = let
val pres = Named_Theorems.get ctxt @{named_theorems wp_pre}
in pre_tac ctxt pres used_ref_option end
in pre_tac trace ctxt pres used_thms_ref end
val method
= Args.context >> (fn _ => fn ctxt => Method.SIMPLE_METHOD' (tac NONE ctxt));
val method =
let
val used_thms_ref = Unsynchronized.ref [] : (string * string * term) list Unsynchronized.ref
in
Args.context >> (fn _ => fn ctxt =>
Method.SIMPLE_METHOD' (tac (Config.get ctxt wp_trace) used_thms_ref ctxt))
end
end
\<close>

4
lib/NICTATools.thy
View File

@ -87,4 +87,8 @@ val _ = Try.tool_setup ("unused_meta_forall",
lemma test_unused_meta_forall: "\<And>x. y \<or> \<not> y"
oops
(* Hide rules used by Trace_Schematic_Insts from apply_trace. *)
lemmas [no_trace] =
data_stash.elim data_stash.proof_state_add data_stash.proof_state_remove data_stash.rule_add
end

3
lib/crunch-cmd.ML
View File

@ -599,8 +599,7 @@ val mism_term_trace = Unsynchronized.ref []
fun seq_try_apply f x = Seq.map_filter (try f) (Seq.single x)
fun wp ctxt rules =
WeakestPre.apply_rules_tac_n false ctxt rules
fun wp ctxt rules = WeakestPre.apply_rules_tac_n false ctxt rules
fun wpsimp ctxt wp_rules simp_rules =
let val ctxt' = Config.put Method.old_section_parser true ctxt

47
lib/ml-helpers/ThmExtras.ML
View File

@ -18,6 +18,8 @@ sig
val adjust_found_thm : adjusted_name -> thm -> adjusted_name
val fact_ref_to_name : Facts.ref * thm -> adjusted_name
val adjust_thm_name : Proof.context -> string * int option -> term -> adjusted_name
val pretty_adjusted_name : Proof.context -> adjusted_name -> Pretty.T
val pretty_adjusted_fact : Proof.context -> adjusted_name -> Pretty.T
val pretty_fact : bool -> Proof.context -> adjusted_name -> Pretty.T
val pretty_thm : bool -> Proof.context -> thm -> Pretty.T
@ -36,8 +38,8 @@ fun adjust_found_thm (FoundName (name, _)) thm = FoundName (name, thm)
| adjust_found_thm adjusted_name _ = adjusted_name
fun fact_ref_to_name ((Facts.Named ((nm,_), (SOME [Facts.Single i]))),thm) = FoundName ((nm,SOME i),thm)
| fact_ref_to_name ((Facts.Named ((nm,_), (NONE))),thm) = FoundName ((nm,NONE),thm)
| fact_ref_to_name (_,thm) = UnknownName ("",Thm.prop_of thm)
| fact_ref_to_name ((Facts.Named ((nm,_), (NONE))),thm) = FoundName ((nm,NONE),thm)
| fact_ref_to_name (_,thm) = UnknownName ("",Thm.prop_of thm)
(* Parse the index of a theorem name in the form "x_1". *)
fun parse_thm_index name =
@ -78,31 +80,40 @@ in
| _ => UnknownName (name, term)
end
fun pretty_adjusted_name ctxt (FoundName ((name, idx), _)) =
Pretty.block
[Pretty.mark_str (Facts.markup_extern ctxt (Proof_Context.facts_of ctxt) name),
case idx of
SOME n => Pretty.str ("(" ^ string_of_int (n + 1) ^ ")")
| NONE => Pretty.str ""]
| pretty_adjusted_name _ (UnknownName (name, _)) =
Pretty.block [Pretty.str name, Pretty.str "(?)"]
fun pretty_adjusted_fact ctxt (FoundName (_, thm)) =
Thm.pretty_thm ctxt thm
| pretty_adjusted_fact ctxt (UnknownName (_, prop)) =
Syntax.unparse_term ctxt prop
(* Render the given fact, using the given adjusted name. *)
fun pretty_fact only_names ctxt (FoundName ((name, idx), thm)) =
fun pretty_fact only_names ctxt adjusted_name =
Pretty.block
([Pretty.mark_str (Facts.markup_extern ctxt (Proof_Context.facts_of ctxt) name),
case idx of
SOME n => Pretty.str ("(" ^ string_of_int (n + 1) ^ ")")
| NONE => Pretty.str ""] @
(pretty_adjusted_name ctxt adjusted_name ::
(if only_names then []
else [Pretty.str ":",Pretty.brk 1, Thm.pretty_thm ctxt thm]))
| pretty_fact _ ctxt (UnknownName (name, prop)) =
Pretty.block
[Pretty.str name, Pretty.str "(?) :", Pretty.brk 1,
Syntax.unparse_term ctxt prop]
else [Pretty.str ":",Pretty.brk 1, pretty_adjusted_fact ctxt adjusted_name]))
(* Render the given fact. *)
fun pretty_thm only_names ctxt thm =
let
val name = Thm.get_name_hint thm
val adjusted_name = adjust_thm_name ctxt (name, NONE) (Thm.prop_of thm)
in pretty_fact only_names ctxt adjusted_name end
let
val name = Thm.get_name_hint thm
val adjusted_name = adjust_thm_name ctxt (name, NONE) (Thm.prop_of thm)
in pretty_fact only_names ctxt adjusted_name
end
(* Render the given fact, using the given name. The name and fact do not have to match. *)
fun pretty_specific_thm ctxt name thm =
let val adjusted_name = adjust_thm_name ctxt (name, NONE) (Thm.prop_of thm)
in pretty_fact false ctxt (adjust_found_thm adjusted_name thm) end
let val adjusted_name = adjust_thm_name ctxt (name, NONE) (Thm.prop_of thm)
in pretty_fact false ctxt (adjust_found_thm adjusted_name thm)
end
(* Render the given name, with markup if it matches a known fact. *)
fun pretty_fact_name ctxt name =

3
tools/autocorres/tests/examples/SchorrWaite.thy
View File

@ -342,8 +342,7 @@ lemma the_equality': "\<And>P a. \<lbrakk>P a; \<And>x. \<lbrakk> P a; P x \<rbr
ML \<open>
fun wp_all_tac ctxt = let fun f n thm =
if n > Thm.nprems_of thm then Seq.single thm else
let val thms = WeakestPre.apply_rules_tac_n false
ctxt [] n thm
let val thms = WeakestPre.apply_rules_tac_n false ctxt [] n thm
|> Seq.list_of
in if null thms then f (n+1) thm else f n (hd thms) end
in f 0 end