# HG changeset patch # User desharna # Date 1743079233 -3600 # Node ID 0b5f1364606c985c24868b330bf7d2c8da72dfe8 # Parent 6a09257afd061d7cddf16fea5d1de6c0c4898890 tuned signature diff -r 6a09257afd06 -r 0b5f1364606c src/HOL/Tools/try0_util.ML --- a/src/HOL/Tools/try0_util.ML Thu Mar 27 13:30:16 2025 +0100 +++ b/src/HOL/Tools/try0_util.ML Thu Mar 27 13:40:33 2025 +0100 @@ -10,6 +10,8 @@ sig val silence_methods : bool -> Proof.context -> Proof.context val string_of_xref : Try0.xref -> string + val apply_raw_named_method : string -> bool -> (Try0.modifier * string) list -> + Time.time option -> Try0.tagged_xref list -> Proof.state -> Try0.result option end structure Try0_Util : TRY0_UTIL = struct @@ -32,4 +34,87 @@ Facts.string_of_ref xref) ^ implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args) +local + +fun add_attr_text (tagged : Try0.tagged_xref list) (tag, src) s = + let + val fs = tagged + |> map_filter (fn (xref, tags) => + if member (op =) tags tag then + SOME (string_of_xref xref) + else + NONE) + in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end + +fun attrs_text tags (tagged : Try0.tagged_xref list) = + "" |> fold (add_attr_text tagged) tags + +fun parse_method ctxt s = + enclose "(" ")" s + |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start + |> filter Token.is_proper + |> Scan.read Token.stopper Method.parse + |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source") + +fun run_tac timeout_opt tac st = + let val with_timeout = + (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I) + in with_timeout (Seq.pull o tac) st |> Option.map fst end + +val num_goals = Thm.nprems_of o #goal o Proof.goal + +fun apply_recursive recurse elapsed0 timeout_opt apply st = + (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of + ({elapsed, ...}, SOME st') => + if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then + let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt) + in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end + else (elapsed0 + elapsed, st') + |_ => (elapsed0, st)) + +in + +fun apply_raw_named_method (name : string) all_goals attrs timeout_opt + (tagged : Try0.tagged_xref list) (st : Proof.state) : Try0.result option = + let + val st = Proof.map_contexts (silence_methods false) st + val unused = + tagged + |> filter + (fn (_, tags) => not (null tags) andalso null (inter (op =) tags (attrs |> map fst))) + |> map fst + + val attrs = attrs_text attrs tagged + + val ctxt = Proof.context_of st + + val text = + name ^ attrs + |> parse_method ctxt + |> Method.method_cmd ctxt + |> Method.Basic + |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) + + val apply = + Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)] + #> Proof.refine text #> Seq.filter_results + val num_before = num_goals st + val multiple_goals = all_goals andalso num_before > 1 + val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st + val num_after = num_goals st' + val select = "[" ^ string_of_int (num_before - num_after) ^ "]" + val unused = implode_space (unused |> map string_of_xref) + val command = + (if unused <> "" then "using " ^ unused ^ " " else "") ^ + (if num_after = 0 then "by " else "apply ") ^ + (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^ + (if multiple_goals andalso num_after > 0 then select else "") + in + if num_before > num_after then + SOME {name = name, command = command, time = time, state = st'} + else NONE + end + +end + end \ No newline at end of file diff -r 6a09257afd06 -r 0b5f1364606c src/HOL/Try0_HOL.thy --- a/src/HOL/Try0_HOL.thy Thu Mar 27 13:30:16 2025 +0100 +++ b/src/HOL/Try0_HOL.thy Thu Mar 27 13:40:33 2025 +0100 @@ -20,38 +20,6 @@ ML \ local -fun add_attr_text (tagged : Try0.tagged_xref list) (tag, src) s = - let - val fs = tagged - |> map_filter (fn (xref, tags) => if member (op =) tags tag then SOME (Try0_Util.string_of_xref xref) else NONE) - in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end - -fun attrs_text tags (tagged : Try0.tagged_xref list) = - "" |> fold (add_attr_text tagged) tags - -fun parse_method ctxt s = - enclose "(" ")" s - |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start - |> filter Token.is_proper - |> Scan.read Token.stopper Method.parse - |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source") - -fun run_tac timeout_opt tac st = - let val with_timeout = - (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I) - in with_timeout (Seq.pull o tac) st |> Option.map fst end - -val num_goals = Thm.nprems_of o #goal o Proof.goal - -fun apply_recursive recurse elapsed0 timeout_opt apply st = - (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of - ({elapsed, ...}, SOME st') => - if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then - let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt) - in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end - else (elapsed0 + elapsed, st') - |_ => (elapsed0, st)) - val full_attrs = [(Try0.Simp, "simp"), (Try0.Intro, "intro"), (Try0.Elim, "elim"), (Try0.Dest, "dest")] val clas_attrs = [(Try0.Intro, "intro"), (Try0.Elim, "elim"), (Try0.Dest, "dest")] val simp_attrs = [(Try0.Simp, "add")] @@ -75,52 +43,11 @@ ("satx", (false, (false, no_attrs))), ("order", (true, (false, no_attrs)))] -fun apply_raw_named_method name (all_goals, attrs) timeout_opt tagged st : - Try0.result option = - let - val st = Proof.map_contexts (Try0_Util.silence_methods false) st - val unused = - tagged - |> filter - (fn (_, tags) => not (null tags) andalso null (inter (op =) tags (attrs |> map fst))) - |> map fst - - val attrs = attrs_text attrs tagged - - val ctxt = Proof.context_of st - - val text = - name ^ attrs - |> parse_method ctxt - |> Method.method_cmd ctxt - |> Method.Basic - |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) - - val apply = - Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)] - #> Proof.refine text #> Seq.filter_results - val num_before = num_goals st - val multiple_goals = all_goals andalso num_before > 1 - val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st - val num_after = num_goals st' - val select = "[" ^ string_of_int (num_before - num_after) ^ "]" - val unused = implode_space (unused |> map Try0_Util.string_of_xref) - val command = - (if unused <> "" then "using " ^ unused ^ " " else "") ^ - (if num_after = 0 then "by " else "apply ") ^ - (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^ - (if multiple_goals andalso num_after > 0 then select else "") - in - if num_before > num_after then - SOME {name = name, command = command, time = time, state = st'} - else NONE - end - in val () = raw_named_methods - |> List.app (fn (name, (run_if_auto_try, raw_method)) => - let val meth : Try0.proof_method = apply_raw_named_method name raw_method in + |> List.app (fn (name, (run_if_auto_try, (all_goals, tags))) => + let val meth : Try0.proof_method = Try0_Util.apply_raw_named_method name all_goals tags in Try0.register_proof_method name {run_if_auto_try = run_if_auto_try} meth handle Symtab.DUP _ => () end)