File ‹Dynamic_Tactic_Generation.ML›
signature DYNAMIC_TACTIC_GENERATOR_SEED =
sig
type modifier;
type modifiers = modifier list;
val get_all_modifiers : Proof.state -> modifiers;
val mods_to_string : modifiers -> string;
val reordered_mods : modifiers -> modifiers list;
end;
signature DYNAMIC_TACTIC_GENERATOR =
sig
include DYNAMIC_TACTIC_GENERATOR_SEED;
val meth_name_n_modifiers_to_nontac_on_state: string -> modifiers -> Proof.state Dynamic_Utils.nontac;
val meth_name_n_modifiers_to_logtac_on_state: string -> modifiers -> Proof.state Dynamic_Utils.logtac;
val meth_name_n_modifiers_to_stttac_on_state: string -> modifiers -> Proof.state Dynamic_Utils.stttac;
end;
functor mk_Dynamic_Tactic_Generator (Seed:DYNAMIC_TACTIC_GENERATOR_SEED) : DYNAMIC_TACTIC_GENERATOR =
struct
open Seed;
structure DG = Dynamic_Utils;
fun general_case (meth_name:string) (mods:modifiers) =
let
val method_str_w_attr = "(" ^ meth_name ^ mods_to_string mods ^ ")";
fun nontac_on_state st = (Utils.try_with (K Seq.empty) DG.string_to_nontac_on_pstate method_str_w_attr
|> Isabelle_Utils.TIMEOUT_in 0.3) st;
val trace_node = DG.Apply {using = [], methN = method_str_w_attr, back = 0};
val logtac_on_state = DG.nontac_to_logtac trace_node nontac_on_state;
val stttac_on_state = DG.logtac_to_stttac logtac_on_state;
in
(nontac_on_state, logtac_on_state, stttac_on_state)
end;
val meth_name_n_modifiers_to_nontac_on_state = #1 oo general_case;
val meth_name_n_modifiers_to_logtac_on_state = #2 oo general_case;
val meth_name_n_modifiers_to_stttac_on_state = #3 oo general_case;
end;
signature DYNAMIC_TACTIC =
sig
val get_state_stttacs : Proof.state -> Proof.state Dynamic_Utils.stttac Seq.seq;
end;
signature DYNAMIC_TACTIC_GENERATION =
sig
type get_stttacs = Proof.state -> Proof.state Dynamic_Utils.stttac Seq.seq;
val rule : get_stttacs;
val erule : get_stttacs;
val simp : get_stttacs;
val induct : get_stttacs;
val induct_tac : get_stttacs;
val coinduction : get_stttacs;
val cases : get_stttacs;
val case_tac : get_stttacs;
val clarsimp : get_stttacs;
val blast : get_stttacs;
val fastforce : get_stttacs;
val auto : get_stttacs;
end;
structure Dynamic_Tactic_Generation =
struct
structure Rule_Seed_Base =
struct
datatype modifier = Rule of string;
type modifiers = modifier list;
fun order (mods:modifiers) = mods;
fun get_name (Rule name) = name;
val get_names = map get_name;
fun mods_to_string (mods:modifiers) =
mods |> order |> (fn rules => get_names rules) |> Dynamic_Utils.get_meth_nm "";
val reordered_mods = single o I;
end;
structure Dynamic_Rule : DYNAMIC_TACTIC =
struct
structure Rule_Seed : DYNAMIC_TACTIC_GENERATOR_SEED =
struct
open Rule_Seed_Base;
fun get_all_modifiers (state:Proof.state) =
let
val {context: Proof.context, goal: thm,...} = Proof.goal state;
val intros = map Rule (Find_Theorems2.get_intro_rule_names context goal);
in
intros : modifiers
end;
end;
structure RTG : DYNAMIC_TACTIC_GENERATOR = mk_Dynamic_Tactic_Generator (Rule_Seed);
fun get_state_stttacs (state:Proof.state) =
let
val rule = "HOL.rule";
val all_modifiers = RTG.get_all_modifiers state : RTG.modifiers;
val all_modifierss = map single all_modifiers |> Seq.of_list : RTG.modifiers Seq.seq;
val stttacs = Seq.map (RTG.meth_name_n_modifiers_to_stttac_on_state rule) all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
stttacs : Proof.state stttac Seq.seq
end;
end;
structure Dynamic_Erule : DYNAMIC_TACTIC =
struct
structure Erule_Seed : DYNAMIC_TACTIC_GENERATOR_SEED =
struct
open Rule_Seed_Base;
fun get_all_modifiers (state:Proof.state) =
let
val {context: Proof.context, goal: thm,...} = Proof.goal state;
val intros = map Rule (Find_Theorems2.get_elim_rule_names context goal);
in
intros : modifiers
end;
end;
structure ETG : DYNAMIC_TACTIC_GENERATOR = mk_Dynamic_Tactic_Generator (Erule_Seed);
fun get_state_stttacs (state:Proof.state) =
let
val rule = "HOL.erule";
val all_modifiers = ETG.get_all_modifiers state : ETG.modifiers;
val all_modifierss = map single all_modifiers |> Seq.of_list : ETG.modifiers Seq.seq;
val stttacs = Seq.map (ETG.meth_name_n_modifiers_to_stttac_on_state rule) all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
stttacs : Proof.state stttac Seq.seq
end;
end;
structure Dynamic_Simp : DYNAMIC_TACTIC =
struct
structure Simp_Seed : DYNAMIC_TACTIC_GENERATOR_SEED =
struct
datatype modifier = Add of string;
type modifiers = modifier list;
fun get_adds (consts:string list) = map Add consts;
fun order (mods:modifiers) = mods;
fun get_name (Add name) = name;
val get_names = map get_name;
fun mods_to_string (mods:modifiers) = mods |> order
|> (fn adds => ["add:"] @ get_names adds)
|> Dynamic_Utils.get_meth_nm "";
fun get_all_modifiers (state:Proof.state) =
let
val {context: Proof.context, goal: thm,...} = Proof.goal state;
val simp_rule_names = Find_Theorems2.get_simp_rule_names context goal;
val standard_rules = ["arith", "algebra", "ac_simps", "field_simps", "algebra_simps", "divide_simps"]
val all_simp_mods = get_adds (standard_rules @ simp_rule_names);
in
all_simp_mods : modifiers
end;
val reordered_mods = single o I;
end;
structure STG : DYNAMIC_TACTIC_GENERATOR =
mk_Dynamic_Tactic_Generator (Simp_Seed) : DYNAMIC_TACTIC_GENERATOR;
fun get_state_stttacs (state:Proof.state) =
let
val simp = "simp ";
val all_modifiers = STG.get_all_modifiers state : STG.modifiers;
val all_modifierss = map single all_modifiers |> Seq.of_list : STG.modifiers Seq.seq;
val ssstacs = Seq.map (STG.meth_name_n_modifiers_to_stttac_on_state simp) all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
ssstacs : Proof.state stttac Seq.seq
end;
end;
structure Dynamic_Induct : DYNAMIC_TACTIC =
struct
structure Induct_Seed : DYNAMIC_TACTIC_GENERATOR_SEED =
struct
datatype modifier =
On of string
| Arbitrary of string
| Rule of string;
type modifiers = modifier list;
fun get_ons (fvars:string list) = map On fvars;
fun get_arbs (fvars:string list) = map Arbitrary fvars;
fun get_rules (rules:string list) = map Rule rules;
fun order' ordered [] = ordered
| order' (ons, arbs, rules) (On var :: mods) = order' (On var::ons, arbs, rules) mods
| order' (ons, arbs, rules) (Arbitrary var :: mods) = order' (ons, Arbitrary var::arbs, rules) mods
| order' (ons, arbs, rules) (Rule rule :: mods) = order' (ons, arbs, Rule rule::rules) mods;
fun order (mods:modifiers) =
order' ([],[],[]) mods : (modifiers * modifiers * modifiers)
fun get_name (On name) = name
| get_name (Arbitrary name) = name
| get_name (Rule name) = name;
val get_names = map get_name;
fun mods_to_string (mods:modifiers) =
let
val prefix_if_nonnil = Utils.prefix_if_nonempty;
in
mods |> order |> (fn (ons, arbs, rules) =>
get_names ons
@ prefix_if_nonnil "arbitrary:" (get_names arbs)
@ prefix_if_nonnil "rule:" (get_names rules))
|> Dynamic_Utils.get_meth_nm ""
end;
fun get_all_modifiers (state:Proof.state) =
let
val {context: Proof.context, goal: thm,...} = Proof.goal state;
val free_var_names = Isabelle_Utils.get_free_var_names_in_1st_subg goal;
val induct_rules = Find_Theorems2.get_induct_rule_names context goal : string list;
val all_induct_mods = get_ons free_var_names @ get_arbs free_var_names @ get_rules induct_rules;
in
all_induct_mods : modifiers
end;
val pick_vars = filter (fn modi => case modi of On _ => true | _ => false);
val dump_vars = filter_out (fn modi => case modi of On _ => true | _ => false);
fun reordered_mods (mods:modifiers)=
let
val vars = pick_vars mods : modifiers;
val varss = Nitpick_Util.all_permutations vars : modifiers list;
val others = dump_vars mods : modifiers;
val combs = map (fn vs => vs @ others) varss;
in
combs:modifiers list
end;
end;
structure ITG : DYNAMIC_TACTIC_GENERATOR = mk_Dynamic_Tactic_Generator (Induct_Seed);
open Induct_Seed;
fun get_state_stttacs (state:Proof.state) =
let
val induct = "induct";
val all_modifiers = ITG.get_all_modifiers state : ITG.modifiers;
val all_modifierss = Seq2.powerset (Seq.of_list all_modifiers)
|> Seq.map Seq.list_of
|> Seq.map reordered_mods
|> Seq.map Seq.of_list
|> Seq.flat: ITG.modifiers Seq.seq;
val stttacs = Seq.map (ITG.meth_name_n_modifiers_to_stttac_on_state induct) all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
stttacs : Proof.state stttac Seq.seq
end;
end;
structure Dynamic_Induct_Tac : DYNAMIC_TACTIC =
struct
structure Induct_Tac_Seed : DYNAMIC_TACTIC_GENERATOR_SEED =
struct
datatype modifier =
On of string
| Rule of string;
type modifiers = modifier list;
fun get_ons (fvars:string list) = map On fvars;
fun get_rules (rules:string list) = map Rule rules;
fun order' ordered [] = ordered
| order' (ons, rules) (On var :: mods) = order' (On var::ons, rules) mods
| order' (ons, rules) (Rule rule :: mods) = order' (ons, Rule rule::rules) mods;
fun order (mods:modifiers) =
order' ([],[]) mods : (modifiers * modifiers)
fun get_name (On name) = name
| get_name (Rule name) = name;
val get_names = map get_name;
fun mods_to_string (mods:modifiers) =
let
val prefix_if_nonnil = Utils.prefix_if_nonempty;
in
mods |> order |> (fn (ons, rules) =>
get_names ons
@ prefix_if_nonnil "rule:" (get_names rules))
|> Dynamic_Utils.get_meth_nm ""
end;
fun get_all_modifiers (state:Proof.state) =
let
val {context: Proof.context, goal: thm,...} = Proof.goal state;
val all_var_names = Isabelle_Utils.get_all_var_names_in_1st_subg goal;
val induct_rules = Find_Theorems2.get_induct_rule_names context goal : string list;
val all_induct_mods = get_ons all_var_names @ get_rules induct_rules;
in
all_induct_mods : modifiers
end;
val reordered_mods = single o I;
end;
structure ITTG : DYNAMIC_TACTIC_GENERATOR =
mk_Dynamic_Tactic_Generator (Induct_Tac_Seed);
fun get_state_stttacs (state:Proof.state) =
let
val induct = "induct_tac";
val all_modifiers = ITTG.get_all_modifiers state : ITTG.modifiers;
val all_modifierss = Seq2.powerset (Seq.of_list all_modifiers)
|> Seq.map Seq.list_of: ITTG.modifiers Seq.seq;
val stttacs = Seq.map (ITTG.meth_name_n_modifiers_to_stttac_on_state induct) all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
stttacs : Proof.state stttac Seq.seq
end;
end;
structure Dynamic_Coinduction : DYNAMIC_TACTIC =
struct
structure Coinduction_Seed : DYNAMIC_TACTIC_GENERATOR_SEED =
struct
datatype modifier =
On of string
| Arbitrary of string
| Rule of string;
type modifiers = modifier list;
fun get_ons (fvars:string list) = map On fvars;
fun get_arbs (fvars:string list) = map Arbitrary fvars;
fun get_rules (rules:string list) = map Rule rules;
fun order' ordered [] = ordered
| order' (ons, arbs, rules) (On var :: mods) = order' (On var::ons, arbs, rules) mods
| order' (ons, arbs, rules) (Arbitrary var :: mods) = order' (ons, Arbitrary var::arbs, rules) mods
| order' (ons, arbs, rules) (Rule rule :: mods) = order' (ons, arbs, Rule rule::rules) mods;
fun order (mods:modifiers) =
order' ([],[],[]) mods : (modifiers * modifiers * modifiers)
fun get_name (On name) = name
| get_name (Arbitrary name) = name
| get_name (Rule name) = name;
val get_names = map get_name;
fun mods_to_string (mods:modifiers) =
let
val prefix_if_nonnil = Utils.prefix_if_nonempty;
in
mods |> order |> (fn (ons, arbs, rules) =>
get_names ons
@ prefix_if_nonnil "arbitrary:" (get_names arbs)
@ prefix_if_nonnil "rule:" (get_names rules))
|> Dynamic_Utils.get_meth_nm ""
end;
fun get_all_modifiers (state:Proof.state) =
let
val {context:Proof.context, goal: thm,...} = Proof.goal state;
val free_var_names = Isabelle_Utils.get_free_var_names_in_1st_subg goal;
val induct_rules = Find_Theorems2.get_coinduction_rule_names context goal : string list;
val all_induct_mods = get_ons free_var_names @ get_arbs free_var_names @ get_rules induct_rules;
in
all_induct_mods : modifiers
end;
val reordered_mods = single o I;
end;
structure CITG : DYNAMIC_TACTIC_GENERATOR = mk_Dynamic_Tactic_Generator (Coinduction_Seed);
fun get_state_stttacs (state:Proof.state) =
let
val coinduction = "coinduction";
val all_modifiers = CITG.get_all_modifiers state : CITG.modifiers;
val all_modifierss = Seq2.powerset (Seq.of_list all_modifiers)
|> Seq.map Seq.list_of: CITG.modifiers Seq.seq;
val stttacs = Seq.map (CITG.meth_name_n_modifiers_to_stttac_on_state coinduction) all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
stttacs : Proof.state stttac Seq.seq
end;
end;
structure Dynamic_Cases : DYNAMIC_TACTIC =
struct
structure Cases_Seed : DYNAMIC_TACTIC_GENERATOR_SEED =
struct
datatype modifier = On of string;
type modifiers = modifier list;
fun get_ons (fvars:string list) = map On fvars;
fun order (mods:modifiers) = mods;
fun get_name (On name) = name;
val get_names = map get_name;
fun mods_to_string (mods:modifiers) =
mods |> order |> (fn ons => get_names ons |> Dynamic_Utils.get_meth_nm "");
fun get_all_modifiers (state:Proof.state) =
let
val {goal: thm,...} = Proof.goal state;
val free_var_names = Isabelle_Utils.get_free_var_names_in_1st_subg goal;
val all_cases_mods = get_ons free_var_names;
in
all_cases_mods : modifiers
end;
val reordered_mods = single o I;
end;
structure CTG : DYNAMIC_TACTIC_GENERATOR = mk_Dynamic_Tactic_Generator (Cases_Seed);
fun get_state_stttacs (state:Proof.state) =
let
val induct = "cases";
val all_modifiers = CTG.get_all_modifiers state : CTG.modifiers;
val all_modifierss = map single all_modifiers |> Seq.of_list : CTG.modifiers Seq.seq;
val stttacs = Seq.map (CTG.meth_name_n_modifiers_to_stttac_on_state induct) all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
stttacs : Proof.state stttac Seq.seq
end;
end;
structure Dynamic_Case_Tac : DYNAMIC_TACTIC =
struct
structure Case_Tac_Seed : DYNAMIC_TACTIC_GENERATOR_SEED =
struct
datatype modifier = On of string;
type modifiers = modifier list;
fun get_ons (all_vars:string list) = map On all_vars;
fun order (mods:modifiers) = mods;
fun get_name (On name) = name;
val get_names = map get_name;
fun mods_to_string (mods:modifiers) =
mods |> order |> (fn ons => get_names ons |> Dynamic_Utils.get_meth_nm "");
fun get_all_modifiers (state:Proof.state) =
let
val {goal: thm,...} = Proof.goal state;
val all_var_names = Isabelle_Utils.get_all_var_names_in_1st_subg goal;
val all_cases_mods = get_ons all_var_names;
in
all_cases_mods : modifiers
end;
val reordered_mods = single o I;
end;
structure CTTG : DYNAMIC_TACTIC_GENERATOR = mk_Dynamic_Tactic_Generator (Case_Tac_Seed);
fun get_state_stttacs (state:Proof.state) =
let
val induct = "case_tac";
val all_modifiers = CTTG.get_all_modifiers state : CTTG.modifiers;
val all_modifierss = map single all_modifiers |> Seq.of_list : CTTG.modifiers Seq.seq;
val stttacs = Seq.map (CTTG.meth_name_n_modifiers_to_stttac_on_state induct) all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
stttacs : Proof.state stttac Seq.seq
end;
end;
structure Classical_Seed : DYNAMIC_TACTIC_GENERATOR_SEED =
struct
datatype modifier =
Simp of string
| Split of string
| Dest of string
| Elim of string
| Intro of string;
type modifiers = modifier list;
fun order' ordered [] = ordered
| order' (simps, splits, dests, elims, intros) (Simp rule ::params) = order' (Simp rule::simps, splits, dests, elims, intros) params
| order' (simps, splits, dests, elims, intros) (Split rule ::params) = order' (simps, Split rule::splits, dests, elims, intros) params
| order' (simps, splits, dests, elims, intros) (Dest rule ::params) = order' (simps, splits, Dest rule::dests, elims, intros) params
| order' (simps, splits, dests, elims, intros) (Elim rule ::params) = order' (simps, splits, dests, Elim rule::elims, intros) params
| order' (simps, splits, dests, elims, intros) (Intro rule ::params) = order' (simps, splits, dests, elims, Intro rule::intros) params
fun order (mods:modifiers) =
order' ([],[],[],[],[]) mods : (modifiers * modifiers * modifiers * modifiers * modifiers)
fun get_name (Simp name) = name
| get_name (Split name) = name
| get_name (Dest name) = name
| get_name (Elim name) = name
| get_name (Intro name) = name;
val get_names = map get_name;
fun mods_to_string (mods:modifiers) =
let
val prefix_if_nonnil = Utils.prefix_if_nonempty;
in
mods |> order |> (fn (simps, splits, dests, elims, intros) =>
prefix_if_nonnil "simp:" (get_names simps)
@ prefix_if_nonnil "split:" (get_names splits)
@ prefix_if_nonnil "dest:" (get_names dests)
@ prefix_if_nonnil "elim:" (get_names elims)
@ prefix_if_nonnil "intro:" (get_names intros))
|> Dynamic_Utils.get_meth_nm ""
end;
structure FT2 = Find_Theorems2;
fun get_all_modifiers (state:Proof.state) =
let
val {context: Proof.context, goal: thm,...} = Proof.goal state;
val split_names = FT2.get_split_rule_names context goal;
val elim_names = FT2.get_elim_rule_names context goal;
val intro_names = FT2.get_intro_rule_names context goal;
val dest_names = FT2.get_dest_rule_names context goal;
fun to_bool EQUAL = true
| to_bool _ = false;
fun are_same (x, y) = (to_bool o String.compare) (x, y);
val simps = subtract are_same (split_names @ elim_names @ intro_names @ dest_names)
(FT2.get_fact_names_mesh state) |> map Simp;
val splits = map Split split_names;
val elims = map Elim elim_names;
val intros = map Intro intro_names;
val dest = map Dest dest_names;
val modifiers = simps @ splits @ elims @ intros @ dest;
in
modifiers : modifiers
end;
val reordered_mods = single o I;
end;
local
structure CTG : DYNAMIC_TACTIC_GENERATOR = mk_Dynamic_Tactic_Generator (Classical_Seed);
in
structure Dynamic_Clarsimp : DYNAMIC_TACTIC =
struct
fun get_state_stttacs (state:Proof.state) =
let
val all_modifiers = CTG.get_all_modifiers state : CTG.modifiers;
val all_modifierss = map single all_modifiers |> Seq.of_list : CTG.modifiers Seq.seq;
val stttacs = Seq.map (CTG.meth_name_n_modifiers_to_stttac_on_state "clarsimp") all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
stttacs : Proof.state stttac Seq.seq
end;
end;
structure Dynamic_Fastforce : DYNAMIC_TACTIC =
struct
fun get_state_stttacs (state:Proof.state) =
let
val all_modifiers = CTG.get_all_modifiers state : CTG.modifiers;
val all_modifierss = map single all_modifiers |> Seq.of_list : CTG.modifiers Seq.seq;
val stttacs = Seq.map (CTG.meth_name_n_modifiers_to_stttac_on_state "fastforce") all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
stttacs : Proof.state stttac Seq.seq
end;
end;
structure Dynamic_Blast : DYNAMIC_TACTIC =
struct
fun get_state_stttacs (state:Proof.state) =
let
val all_modifiers = CTG.get_all_modifiers state : CTG.modifiers;
val all_modifierss = map single all_modifiers |> Seq.of_list : CTG.modifiers Seq.seq;
val stttacs = Seq.map (CTG.meth_name_n_modifiers_to_stttac_on_state "blast") all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
stttacs : Proof.state stttac Seq.seq
end;
end;
structure Dynamic_Auto : DYNAMIC_TACTIC =
struct
type mods = CTG.modifiers;
type pstate = Proof.state;
fun get_state_stttacs (state:Proof.state) =
let
val all_modifiers = CTG.get_all_modifiers state : CTG.modifiers;
val all_modifierss = map single all_modifiers |> Seq.of_list : CTG.modifiers Seq.seq;
val stttacs = Seq.map (CTG.meth_name_n_modifiers_to_stttac_on_state "auto") all_modifierss;
type 'a stttac = 'a Dynamic_Utils.stttac;
in
stttacs : Proof.state stttac Seq.seq
end;
end;
end;
type get_stttacs = Proof.state -> Proof.state Dynamic_Utils.stttac Seq.seq;
val rule = Dynamic_Rule.get_state_stttacs;
val erule = Dynamic_Erule.get_state_stttacs;
val simp = Dynamic_Simp.get_state_stttacs;
val induct = Dynamic_Induct.get_state_stttacs;
val induct_tac = Dynamic_Induct_Tac.get_state_stttacs;
val coinduction = Dynamic_Coinduction.get_state_stttacs;
val cases = Dynamic_Cases.get_state_stttacs;
val case_tac = Dynamic_Case_Tac.get_state_stttacs;
val clarsimp = Dynamic_Clarsimp.get_state_stttacs;
val blast = Dynamic_Blast.get_state_stttacs;
val fastforce = Dynamic_Fastforce.get_state_stttacs;
val auto = Dynamic_Auto.get_state_stttacs;
end;