wneuper@59571: (* Title: Tactics; tac_ for interaction with frontend, input for internal use. wneuper@59304: Author: Walther Neuper 170121 wneuper@59304: (c) due to copyright terms wneuper@59304: wneuper@59304: regular expression for search: wneuper@59304: walther@59928: Add_Find|Add_Given|Add_Relation|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst wneuper@59304: wneuper@59304: *) wneuper@59298: signature TACTIC = wneuper@59298: sig walther@59846: datatype T = walther@59940: Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model walther@59940: | Add_Relation' of TermC.as_string * Model_Def.i_model walther@59924: (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string walther@59940: | Model_Problem' of Problem.id * Model_Def.i_model * Model_Def.i_model walther@59963: | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T) walther@60154: | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * MethodC.id * Model_Def.i_model walther@60154: | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model walther@59963: | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model * Pre_Conds_Def.T)) walther@59923: | Specify_Theory' of ThyC.id walther@59923: (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*) walther@60154: | Apply_Method' of MethodC.id * term option * Istate_Def.T * Proof.context walther@59879: | Calculate' of ThyC.id * string * term * (term * ThmC.T) walther@59903: | Check_Postcond' of Problem.id * term walther@59937: | Check_elementwise' of term * TermC.as_string * Celem.result walther@59927: | Derive' of Rule_Set.T walther@59846: | Empty_Tac_ walther@59846: | Free_Solve' walther@59846: | Or_to_List' of term * term Walther@60509: | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result Walther@60509: | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result walther@59937: | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result walther@59937: | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result walther@59985: | Subproblem' of References_Def.T * Model_Def.o_model * term * Model_Def.form_model * Proof.context * term Walther@60509: | Substitute' of Rewrite_Ord.function * Rule_Set.T * Subst.as_eqs * term * term walther@59923: (*RM*)| Tac_ of theory * string * string * string walther@59846: | Take' of term walther@59937: | End_Detail' of Celem.result walther@59937: | Begin_Trans' of term | End_Trans' of Celem.result walther@59925: | End_Proof'' walther@59923: walther@59812: val string_of: T -> string walther@59741: walther@59846: datatype input = walther@59923: Add_Find of TermC.as_string | Add_Given of TermC.as_string walther@59923: | Add_Relation of TermC.as_string walther@59923: | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string walther@59923: | Model_Problem walther@59923: | Refine_Problem of Problem.id walther@59923: | Refine_Tacitly of Problem.id walther@60154: | Specify_Method of MethodC.id walther@59923: | Specify_Problem of Problem.id walther@59923: | Specify_Theory of ThyC.id walther@59923: (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*) walther@60154: | Apply_Method of MethodC.id walther@59846: | Calculate of string walther@59903: | Check_Postcond of Problem.id walther@59865: | Check_elementwise of TermC.as_string walther@59927: | Derive of Rule_Set.id walther@59846: | Empty_Tac walther@59927: | Free_Solve walther@59846: | Or_to_List walther@59874: | Rewrite of ThmC.T walther@59911: | Rewrite_Inst of Subst.input * ThmC.T walther@59867: | Rewrite_Set of Rule_Set.id walther@59911: | Rewrite_Set_Inst of Subst.input * Rule_Set.id walther@59923: | Subproblem of ThyC.id * Problem.id walther@59923: | Substitute of Subst.input walther@59923: (*RM*)| Tac of string walther@59923: | Take of TermC.as_string walther@59925: | End_Detail walther@59925: | Begin_Trans | End_Trans walther@59923: | End_Proof'; walther@59846: walther@59846: val input_to_string : input -> string walther@59812: val tac2IDstr : input -> string walther@59844: val is_empty : input -> bool wneuper@59302: walther@59728: val eq_tac : input * input -> bool walther@59728: val is_rewtac : input -> bool walther@59728: val is_rewset : input -> bool walther@59867: val rls_of : input -> Rule_Set.id Walther@60500: val rule2tac : Proof.context -> Env.T -> Rule.rule -> input Walther@60500: val applicable : Proof.context -> string -> Rule_Set.T -> term -> input ->input list walther@59914: val for_specify: input -> bool walther@59914: walther@59704: val input_from_T : T -> input walther@59728: val result : T -> term walther@59728: val creates_assms: T -> term list walther@59728: val insert_assumptions: T -> Proof.context -> Proof.context walther@59749: val for_specify': T -> bool wneuper@59298: end wneuper@59298: walther@59728: (**) wneuper@59571: structure Tactic(**): TACTIC(**) = wneuper@59298: struct walther@59728: (**) wneuper@59298: walther@59914: (** tactics for user at front-end **) walther@59914: walther@59846: datatype input = walther@59865: Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string walther@59924: | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string walther@59924: | Model_Problem walther@59924: | Refine_Problem of Problem.id walther@59924: | Refine_Tacitly of Problem.id walther@60154: | Specify_Method of MethodC.id walther@59924: | Specify_Problem of Problem.id walther@59924: | Specify_Theory of ThyC.id walther@59924: (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*) walther@60154: | Apply_Method of MethodC.id walther@59846: | Calculate of string walther@59903: | Check_Postcond of Problem.id walther@59865: | Check_elementwise of TermC.as_string walther@59927: | Derive of Rule_Set.id walther@59846: | Empty_Tac walther@59927: | Free_Solve walther@59846: | Or_to_List walther@59874: | Rewrite of ThmC.T walther@59911: | Rewrite_Inst of Subst.input * ThmC.T walther@59867: | Rewrite_Set of Rule_Set.id walther@59911: | Rewrite_Set_Inst of Subst.input * Rule_Set.id walther@59924: | Subproblem of ThyC.id * Problem.id walther@59912: | Substitute of Subst.input walther@59924: (*RM*)| Tac of string walther@59924: | Take of TermC.as_string walther@59925: | End_Detail walther@59925: | Begin_Trans | End_Trans walther@59924: | End_Proof'; walther@59846: walther@59846: fun input_to_string ma = case ma of walther@59926: Model_Problem => "Model_Problem " walther@59846: | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID walther@59846: | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID walther@59846: | Add_Given cterm' => "Add_Given " ^ cterm' walther@59846: | Del_Given cterm' => "Del_Given " ^ cterm' walther@59846: | Add_Find cterm' => "Add_Find " ^ cterm' walther@59846: | Del_Find cterm' => "Del_Find " ^ cterm' walther@59846: | Add_Relation cterm' => "Add_Relation " ^ cterm' walther@59846: | Del_Relation cterm' => "Del_Relation " ^ cterm' walther@59846: walther@59846: | Specify_Theory domID => "Specify_Theory " ^ quote domID walther@59846: | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID walther@59846: | Specify_Method metID => "Specify_Method " ^ strs2str metID walther@59846: | Apply_Method metID => "Apply_Method " ^ strs2str metID walther@59846: | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID walther@59846: | Free_Solve => "Free_Solve" walther@59846: walther@59846: | Rewrite_Inst (subs, (id, thm)) => walther@59868: "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> UnparseC.term))) walther@59868: | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> UnparseC.term) walther@59846: | Rewrite_Set_Inst (subs, rls) => walther@59846: "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls) walther@59846: | Rewrite_Set rls => "Rewrite_Set " ^ quote rls walther@59932: | Begin_Trans => "Begin_Trans" walther@59932: | End_Trans => "End_Trans" walther@59846: | End_Detail => "End_Detail" walther@59927: | Derive rls' => "Derive " ^ rls' walther@59911: | Calculate op_ => "Calculate " ^ op_ walther@59912: | Substitute sube => "Substitute " ^ Subst.string_eqs_to_string sube walther@59846: walther@59846: | Take cterm' => "Take " ^ quote cterm' walther@59846: | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID) walther@59846: walther@59846: | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm' walther@59846: | Or_to_List => "Or_to_List " walther@59846: walther@59846: | Empty_Tac => "Empty_Tac" walther@59927: (*RM*)| Tac string => "Tac " ^ string(*RM*) walther@60268: | End_Proof' => "input End_Proof'"; walther@59846: walther@59846: fun tac2IDstr ma = case ma of walther@59846: Model_Problem => "Model_Problem" walther@59846: | Refine_Tacitly _ => "Refine_Tacitly" walther@59846: | Refine_Problem _ => "Refine_Problem" walther@59846: | Add_Given _ => "Add_Given" walther@59846: | Del_Given _ => "Del_Given" walther@59846: | Add_Find _ => "Add_Find" walther@59846: | Del_Find _ => "Del_Find" walther@59846: | Add_Relation _ => "Add_Relation" walther@59846: | Del_Relation _ => "Del_Relation" walther@59846: walther@59846: | Specify_Theory _ => "Specify_Theory" walther@59846: | Specify_Problem _ => "Specify_Problem" walther@59846: | Specify_Method _ => "Specify_Method" walther@59846: | Apply_Method _ => "Apply_Method" walther@59846: | Check_Postcond _ => "Check_Postcond" walther@59846: | Free_Solve => "Free_Solve" walther@59846: walther@59846: | Rewrite_Inst _ => "Rewrite_Inst" walther@59846: | Rewrite _ => "Rewrite" walther@59846: | Rewrite_Set_Inst _ => "Rewrite_Set_Inst" walther@59846: | Rewrite_Set _ => "Rewrite_Set" walther@59846: | Derive _ => "Derive " walther@59846: | Calculate _ => "Calculate " walther@59846: | Substitute _ => "Substitute" walther@59846: walther@59846: | Take _ => "Take" walther@59846: | Subproblem _ => "Subproblem" walther@59846: walther@59846: | Check_elementwise _ => "Check_elementwise" walther@59846: | Or_to_List => "Or_to_List " walther@59846: walther@59846: | Empty_Tac => "Empty_Tac" walther@59846: | Tac _ => "Tac " walther@59846: | End_Proof' => "End_Proof'" walther@59846: | _ => "input_to_string not impl. for ?!"; walther@59846: walther@59846: fun is_empty input = case input of Empty_Tac => true | _ => false wneuper@59302: wneuper@59302: fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2 wneuper@59302: | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2 wneuper@59302: | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2 wneuper@59302: | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2 wneuper@59302: | eq_tac (Calculate id1, Calculate id2) = id1 = id2 wneuper@59302: | eq_tac _ = false wneuper@59302: wneuper@59302: fun is_rewset (Rewrite_Set_Inst _) = true wneuper@59302: | is_rewset (Rewrite_Set _) = true wneuper@59302: | is_rewset _ = false; wneuper@59302: fun is_rewtac (Rewrite _) = true wneuper@59302: | is_rewtac (Rewrite_Inst _) = true wneuper@59571: | is_rewtac input = is_rewset input; wneuper@59302: wneuper@59302: wneuper@59302: fun rls_of (Rewrite_Set_Inst (_, rls)) = rls wneuper@59302: | rls_of (Rewrite_Set rls) = rls walther@59962: | rls_of input = raise ERROR ("rls_of: called with input \"" ^ tac2IDstr input ^ "\""); wneuper@59302: Walther@60500: fun rule2tac ctxt _ (Rule.Eval (opID, _)) = Calculate (assoc_calc (Proof_Context.theory_of ctxt) opID) wneuper@59416: | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm'' wneuper@59416: | rule2tac _ subst (Rule.Thm thm'') = walther@59911: Rewrite_Inst (Subst.T_to_input subst, thm'') walther@59867: | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls) wneuper@59416: | rule2tac _ subst (Rule.Rls_ rls) = walther@59911: Rewrite_Set_Inst (Subst.T_to_input subst, (Rule_Set.id rls)) wneuper@59302: | rule2tac _ _ rule = walther@59962: raise ERROR ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\""); wneuper@59302: walther@59914: (* try if a rewrite-rule is applicable to a given formula; walther@59914: in case of rule-sets (recursivley) collect all _atomic_ rewrites *) Walther@60509: fun try_rew ctxt ((_, ro) : Rewrite_Ord.T) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) = walther@59914: if Auto_Prog.contains_bdv thm Walther@60500: then case Rewrite.rewrite_inst_ ctxt ro erls false subst thm f of Walther@60500: SOME _ => [rule2tac ctxt subst thm'] walther@59914: | NONE => [] Walther@60500: else (case Rewrite.rewrite_ ctxt ro erls false thm f of Walther@60500: SOME _ => [rule2tac ctxt [] thm'] walther@59914: | NONE => []) Walther@60500: | try_rew ctxt _ _ _ f (cal as Rule.Eval c) = Walther@60500: (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of Walther@60500: SOME _ => [rule2tac ctxt [] cal] walther@59914: | NONE => []) Walther@60500: | try_rew ctxt _ _ _ f (cal as Rule.Cal1 c) = Walther@60500: (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of Walther@60500: SOME _ => [rule2tac ctxt [] cal] walther@59914: | NONE => []) walther@59914: | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls walther@59962: | try_rew _ _ _ _ _ _ = raise ERROR "try_rew: uncovered case" walther@59914: and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) = walther@60017: distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules)) walther@59914: | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) = walther@60017: distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules)) walther@59914: | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = [] walther@59962: | filter_appl_rews _ _ _ _ = raise ERROR "filter_appl_rews: uncovered case" walther@59914: walther@59914: (* decide if a tactic is applicable to a given formula; walther@59914: in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *) Walther@60500: fun applicable ctxt _ _ f (Calculate scrID) = Walther@60509: try_rew ctxt Rewrite_Ord.empty Rule_Set.empty [] f Walther@60500: (Rule.Eval (assoc_calc' (Proof_Context.theory_of ctxt) scrID |> snd)) Walther@60500: | applicable ctxt ro erls f (Rewrite thm'') = Walther@60506: try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls [] f (Rule.Thm thm'') Walther@60500: | applicable ctxt ro erls f (Rewrite_Inst (subs, thm'')) = Walther@60506: try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls Walther@60506: (Subst.T_from_input ctxt subs) f (Rule.Thm thm'') walther@59914: walther@59914: | applicable thy _ _ f (Rewrite_Set rls') = walther@59914: filter_appl_rews thy [] f (assoc_rls rls') walther@59914: | applicable thy _ _ f (Rewrite_Set_Inst (subs, rls')) = walther@59914: filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls') walther@59914: | applicable _ _ _ _ tac = walther@59914: (tracing ("### applicable: not impl. for tac = '" ^ input_to_string tac ^ "'"); []); walther@59914: walther@59914: walther@59914: (** tactics for internal use **) walther@59914: walther@59846: datatype T = walther@59940: Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model walther@59940: | Add_Relation' of TermC.as_string * Model_Def.i_model (* for Step.do_next *) walther@59924: (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string walther@59924: | Model_Problem' of (* first step in specify-phase *) walther@59924: Problem.id * (* id in the Know_Store *) walther@59940: Model_Def.i_model * (* the model for the Problem *) walther@59940: Model_Def.i_model (* the model for the method *) walther@59963: | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T) walther@59924: | Refine_Tacitly' of walther@59924: Problem.id * (* the original id in the Know_Store *) walther@59924: Problem.id * (* the id of the refined Problem *) walther@59924: ThyC.id * (* the id of the refined theory *) walther@60154: MethodC.id * (* the id of the refined MethodC *) walther@59940: Model_Def.i_model (* RM 9.03: remains [] for Model_Problem recognizing its activation *) walther@60154: | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model walther@59924: | Specify_Problem' of Problem.id * walther@59924: (bool * (* all preconditions evaluate to True *) walther@59940: (Model_Def.i_model * (* the model checked for the input id *) walther@59963: Pre_Conds_Def.T)) (* individual preconditions marked true/false *) walther@59924: | Specify_Theory' of ThyC.id walther@59924: (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*) walther@59932: | Apply_Method' of (* last step in specifu-phse, switch to solve-phase *) walther@60154: MethodC.id * (* id in the Know_Store *) walther@59932: term option * (* first formula in the (sub-)Problem TODO: rm option *) walther@59932: Istate_Def.T * (* for starting the Program *) walther@59932: Proof.context (* for starting the Program *) walther@59879: | Calculate' of ThyC.id * string * term * (term * ThmC.T) walther@59924: | Check_Postcond' of (* last step in solving a (sub-)Problem *) walther@59924: Problem.id * (* id of the Problem to be checked *) walther@59924: term (* return value of the program *) walther@59924: | Check_elementwise' of(* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *) walther@59924: term * (* the current formula: [x=1,x=...] *) walther@59924: string * (* the pred from Check_elementwise *) walther@59937: Celem.result (* composed from (1) and (2): {x. pred} *) walther@59959: | Derive' of Rule_Set.T(* for Test_Out.embed_deriv *) walther@59846: | Empty_Tac_ walther@59846: | Free_Solve' walther@59846: | Or_to_List' of term * term Walther@60509: | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result Walther@60509: | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result walther@59937: | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result walther@59937: | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result walther@59924: | Subproblem' of (* switch from solve-phase to specify-phase *) walther@59985: References_Def.T * (* specification of the SubProblem *) walther@59940: (Model_Def.o_model) * (* original model, filled in associate Subproblem' *) walther@59924: term * (* headline of calc-head, filled -"- *) walther@59941: Model_Def.form_model * (* string list from arguments of the calling Program*) walther@59924: Proof.context * (* for the specify-phase *) walther@59924: term (* Subproblem (thyID, pbl) OR CAS_Cmd *) walther@59924: | Substitute' of (* substitute variables (TODO: from the context) *) Walther@60509: Rewrite_Ord.function *(* for re-calculation *) walther@59924: Rule_Set.T * (* for re-calculation *) walther@59924: Subst.as_eqs * (* the substitution: terms of type bool *) walther@59924: term * (* to be substituted into *) walther@59924: term (* resulting from the substitution *) walther@59924: (*RM*)| Tac_ of theory * string * string * string walther@59846: | Take' of term walther@59937: | End_Detail' of Celem.result (* for intermediate steps into Rewrite_Set *) walther@59927: | Begin_Trans' of term (* for intermediate steps into Rewrite_Set *) walther@59937: | End_Trans' of Celem.result (* for intermediate steps into Rewrite_Set *) walther@59925: | End_Proof'' walther@59846: walther@59846: fun string_of ma = case ma of walther@59926: Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID walther@59846: | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^ walther@59846: strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)" walther@59846: | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")" walther@59846: | Add_Given' _ => "Add_Given' "(*^cterm'*) walther@59846: | Del_Given' _ => "Del_Given' "(*^cterm'*) walther@59846: | Add_Find' _ => "Add_Find' "(*^cterm'*) walther@59846: | Del_Find' _ => "Del_Find' "(*^cterm'*) walther@59846: | Add_Relation' _ => "Add_Relation' "(*^cterm'*) walther@59846: | Del_Relation' _ => "Del_Relation' "(*^cterm'*) walther@59846: walther@59846: | Specify_Theory' domID => "Specify_Theory' " ^ quote domID walther@59846: | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^ walther@59846: spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre"))) walther@59846: | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^ walther@60154: MethodC.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string oris ^ ", )" walther@59846: walther@59846: | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID walther@59846: | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^ walther@59868: (spair2str (strs2str pblID, UnparseC.term scval)) walther@59846: walther@59846: | Free_Solve' => "Free_Solve'" walther@59846: walther@59846: | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*) walther@59846: | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*) walther@59846: | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*) walther@59997: | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ ", " ^ bool2str pasm ^ walther@59997: ", " ^ Rule_Set.id rls' ^ ", " ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ ", " ^ UnparseC.terms asm ^ "))" walther@59846: | End_Detail' _ => "End_Detail' xxx" walther@59846: walther@59867: | Derive' rls => "Derive' " ^ Rule_Set.id rls walther@59846: | Calculate' _ => "Calculate' " walther@59846: | Substitute' _ => "Substitute' "(*^(subs2str subs)*) walther@59846: walther@59846: | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*) walther@59846: | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) => walther@59846: "Subproblem' "(*^(pair2str (domID, strs2str ,))*) walther@59846: walther@59846: | Empty_Tac_ => "Empty_Tac_" walther@59997: | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ ", " ^ id ^ ", " ^ result ^ ")" walther@59925: walther@59925: | Begin_Trans' _ => "Begin_Trans' xxx" walther@59925: | End_Trans' _ => "End_Trans' xxx" walther@59925: | End_Proof'' => "End_Trans' xxx" walther@59846: | _ => "string_of not impl. for arg"; wneuper@59302: walther@59704: fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI walther@59704: | input_from_T (Model_Problem' (_, _, _)) = Model_Problem walther@59704: | input_from_T (Add_Given' (t, _)) = Add_Given t walther@59704: | input_from_T (Add_Find' (t, _)) = Add_Find t walther@59704: | input_from_T (Add_Relation' (t, _)) = Add_Relation t walther@59704: walther@59704: | input_from_T (Specify_Theory' dI) = Specify_Theory dI walther@59704: | input_from_T (Specify_Problem' (dI, _)) = Specify_Problem dI walther@59704: | input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI walther@59704: walther@59704: | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm walther@59911: | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Subst.T_to_input sub, thm) walther@59704: walther@59867: | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls) walther@59704: | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) = walther@59911: Rewrite_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls) walther@59704: walther@59704: | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_) walther@59704: | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred walther@59704: walther@59704: | input_from_T (Or_to_List' _) = Or_to_List walther@59868: | input_from_T (Take' term) = Take (UnparseC.term term) walther@59912: | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_input subte) walther@59704: | input_from_T (Tac_ (_, _, id, _)) = Tac id walther@59704: walther@59704: | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID) walther@59704: | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID walther@59704: | input_from_T Empty_Tac_ = Empty_Tac walther@59846: | input_from_T m = raise ERROR (": not impl. for "^(string_of m)); walther@59704: walther@59728: fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res walther@59728: | res (Rewrite' (_, _, _, _, _, _, res)) = res walther@59728: | res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res walther@59728: | res (Rewrite_Set' (_, _, _, _, res)) = res walther@59728: | res (Calculate' (_, _, _, (t, _))) = (t, []) walther@59728: | res (Check_elementwise' (_, _, res)) = res walther@59728: | res (Subproblem' (_, _, _, _, _, t)) = (t, []) walther@59728: | res (Take' t) = (t, []) walther@59728: | res (Substitute' (_, _, _, _, t)) = (t, []) walther@59728: | res (Or_to_List' (_, t)) = (t, []) walther@59846: | res m = raise ERROR ("result: not impl.for " ^ string_of m) walther@59728: walther@59728: (*fun result m = (fst o res) m; TODO*) walther@59728: fun result tac = (fst o res) tac; walther@59728: fun creates_assms tac = (snd o res) tac; walther@59728: walther@59728: fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt walther@59728: walther@59932: fun for_specify (Add_Find _) = true walther@59932: | for_specify (Add_Given _) = true walther@59932: | for_specify (Add_Relation _) = true walther@59932: | for_specify (Del_Find _) = true walther@59932: | for_specify (Del_Given _) = true walther@59932: | for_specify (Del_Relation _) = true walther@59932: | for_specify Model_Problem = true walther@59932: | for_specify (Refine_Problem _) = true walther@59749: | for_specify (Refine_Tacitly _) = true walther@59932: | for_specify (Specify_Method _) = true walther@59932: | for_specify (Specify_Problem _) = true walther@59749: | for_specify (Specify_Theory _) = true walther@59749: | for_specify _ = false walther@59932: walther@59932: fun for_specify' (Add_Find' _) = true walther@59932: | for_specify' (Add_Given' _) = true walther@59932: | for_specify' (Add_Relation' _) = true walther@59932: | for_specify' (Del_Find' _) = true walther@59932: | for_specify' (Del_Given' _) = true walther@59932: | for_specify' (Del_Relation' _) = true walther@59932: | for_specify' (Model_Problem' _) = true walther@59932: | for_specify' (Refine_Problem' _) = true walther@59749: | for_specify' (Refine_Tacitly' _) = true walther@59932: | for_specify' (Specify_Method' _) = true walther@59932: | for_specify' (Specify_Problem' _) = true walther@59749: | for_specify' (Specify_Theory' _) = true walther@59749: | for_specify' _ = false walther@59749: walther@59728: (**)end(**)