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: wneuper@59304: Add_Find|Add_Given|Add_Relation|Apply_Assumption|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|Collect_Trues|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|CAScmd|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_Asm|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@59741: datatype T = walther@59741: Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list walther@59741: | Add_Relation' of Rule.cterm' * Model.itm list walther@59741: | Apply_Assumption' of term list * term walther@59741: | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context walther@59741: walther@59741: | Begin_Sequ' | Begin_Trans' of term walther@59741: | Split_And' of term | Split_Or' of term | Split_Intersect' of term walther@59741: | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term walther@59741: | End_Sequ' | End_Trans' of Selem.result walther@59741: | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof'' walther@59741: walther@59741: | CAScmd' of term walther@59741: | Calculate' of Rule.theory' * string * term * (term * Celem.thm') walther@59741: | Check_Postcond' of Celem.pblID * Selem.result walther@59741: | Check_elementwise' of term * Rule.cterm' * Selem.result walther@59741: | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm' walther@59741: walther@59741: | Derive' of Rule.rls walther@59741: | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result walther@59741: | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result walther@59741: | End_Detail' of Selem.result walther@59741: walther@59741: | Empty_Tac_ walther@59741: | Free_Solve' walther@59741: walther@59741: | Init_Proof' of Rule.cterm' list * Celem.spec walther@59741: | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list walther@59741: | Or_to_List' of term * term walther@59741: | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list) walther@59741: | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list walther@59741: walther@59741: | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result walther@59741: | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result walther@59741: | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result walther@59741: | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result walther@59741: | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result walther@59741: walther@59741: | Specify_Method' of Celem.metID * Model.ori list * Model.itm list walther@59741: | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list)) walther@59741: | Specify_Theory' of Rule.domID walther@59741: | Subproblem' of Celem.spec * Model.ori list * term * Selem.fmz_ * Proof.context * term walther@59741: | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term walther@59741: | Tac_ of theory * string * string * string walther@59741: | Take' of term | Take_Inst' of term walther@59728: val string_of : T -> string wneuper@59302: walther@59741: datatype input = walther@59741: Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm' walther@59741: | Apply_Assumption of Rule.cterm' list walther@59741: | Apply_Method of Celem.metID walther@59741: (*/--- TODO: re-design ? -----------------------------------------------------------------\*) walther@59741: | Begin_Sequ | Begin_Trans walther@59741: | Split_And | Split_Or | Split_Intersect walther@59741: | Conclude_And | Conclude_Or | Collect_Trues walther@59741: | End_Sequ | End_Trans walther@59741: | End_Ruleset | End_Subproblem | End_Intersect | End_Proof' walther@59741: (*\--- TODO: re-design ? -----------------------------------------------------------------/*) walther@59741: | CAScmd of Rule.cterm' walther@59741: | Calculate of string walther@59741: | Check_Postcond of Celem.pblID walther@59741: | Check_elementwise of Rule.cterm' walther@59741: | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm' walther@59741: walther@59741: | Derive of Rule.rls' walther@59741: | Detail_Set of Rule.rls' walther@59741: | Detail_Set_Inst of Selem.subs * Rule.rls' walther@59741: | End_Detail walther@59741: walther@59741: | Empty_Tac walther@59741: | Free_Solve walther@59741: walther@59741: | Init_Proof of Rule.cterm' list * Celem.spec walther@59741: | Model_Problem walther@59741: | Or_to_List walther@59741: | Refine_Problem of Celem.pblID walther@59741: | Refine_Tacitly of Celem.pblID walther@59741: walther@59741: | Rewrite of Celem.thm'' walther@59741: | Rewrite_Asm of Celem.thm'' walther@59741: | Rewrite_Inst of Selem.subs * Celem.thm'' walther@59741: | Rewrite_Set of Rule.rls' walther@59741: | Rewrite_Set_Inst of Selem.subs * Rule.rls' walther@59741: walther@59741: | Specify_Method of Celem.metID walther@59741: | Specify_Problem of Celem.pblID walther@59741: | Specify_Theory of Rule.domID walther@59741: | Subproblem of Rule.domID * Celem.pblID walther@59741: walther@59741: | Substitute of Selem.sube walther@59741: | Tac of string walther@59741: | Take of Rule.cterm' | Take_Inst of Rule.cterm' wneuper@59571: val tac2str : input -> string wneuper@59302: walther@59728: val eq_tac : input * input -> bool walther@59728: val is_empty_tac : input -> bool walther@59728: val is_rewtac : input -> bool walther@59728: val is_rewset : input -> bool walther@59728: val rls_of : input -> Rule.rls' wneuper@59571: val tac2IDstr : input -> string walther@59728: val rule2tac : theory -> (term * term) list -> Rule.rule -> input 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: input -> bool walther@59749: val for_specify': T -> bool walther@59735: wneuper@59310: (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) wneuper@59310: (* NONE *) walther@59702: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) wneuper@59310: (* NONE *) walther@59702: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59298: wneuper@59310: (*----- unused code, kept as hints to design ideas ---------------------------------------------*) wneuper@59310: (* NONE *) wneuper@59298: end wneuper@59298: walther@59728: (**) wneuper@59571: structure Tactic(**): TACTIC(**) = wneuper@59298: struct walther@59728: (**) wneuper@59298: wneuper@59302: (* tactics for user at front-end. wneuper@59571: input propagates the construction of the calc-tree; wneuper@59302: there are wneuper@59302: (a) 'specsteps' for the specify-phase, and others for the solve-phase wneuper@59302: (b) those of the solve-phase are 'initac's and others; wneuper@59302: initacs start with a formula different from the preceding formula. wneuper@59302: see 'type tac_' for the internal representation of tactics wneuper@59302: *) walther@59741: datatype input = walther@59741: Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm' walther@59741: | Apply_Assumption of Rule.cterm' list walther@59741: | Apply_Method of Celem.metID walther@59741: (* creates an "istate" in PblObj.env; in case of "init_form" walther@59741: creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc" walther@59741: a "SOME istate" at fst of "loc". walther@59741: As each step (in the solve-phase) has a resulting formula (at the front-end) walther@59741: Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *) walther@59741: (*/--- TODO: re-design ? -----------------------------------------------------------------\*) walther@59741: | Begin_Sequ | Begin_Trans walther@59741: | Split_And | Split_Or | Split_Intersect walther@59741: | Conclude_And | Conclude_Or | Collect_Trues walther@59741: | End_Sequ | End_Trans walther@59741: | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof' walther@59741: (*\--- TODO: re-design ? -----------------------------------------------------------------/*) walther@59741: | CAScmd of Rule.cterm' walther@59741: | Calculate of string walther@59741: | Check_Postcond of Celem.pblID walther@59741: | Check_elementwise of Rule.cterm' walther@59741: | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm' wneuper@59302: walther@59741: | Derive of Rule.rls' (* WN0509 drop *) walther@59741: | Detail_Set of Rule.rls' (* WN0509 drop *) walther@59741: | Detail_Set_Inst of Selem.subs * Rule.rls' (* WN0509 drop *) walther@59741: | End_Detail (* WN0509 drop *) wneuper@59302: walther@59741: | Empty_Tac walther@59741: | Free_Solve walther@59741: walther@59741: | Init_Proof of Rule.cterm' list * Celem.spec walther@59741: | Model_Problem walther@59741: | Or_to_List walther@59741: | Refine_Problem of Celem.pblID walther@59741: | Refine_Tacitly of Celem.pblID walther@59741: walther@59741: (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end walther@59741: because there all the thms are present with both (thmID, thm) walther@59741: (where user-views can show both or only one of (thmID, thm)), walther@59741: and thm is created from ThmID by assoc_thm'' when entering isabisac *) walther@59741: | Rewrite of Celem.thm'' walther@59741: | Rewrite_Asm of Celem.thm'' walther@59741: | Rewrite_Inst of Selem.subs * Celem.thm'' walther@59741: | Rewrite_Set of Rule.rls' walther@59741: | Rewrite_Set_Inst of Selem.subs * Rule.rls' walther@59741: walther@59741: | Specify_Method of Celem.metID walther@59741: | Specify_Problem of Celem.pblID walther@59741: | Specify_Theory of Rule.domID walther@59741: | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *) walther@59741: walther@59741: | Substitute of Selem.sube walther@59741: | Tac of string (* WN0509 drop *) walther@59741: | Take of Rule.cterm' | Take_Inst of Rule.cterm' walther@59741: walther@59741: fun tac2str ma = case ma of walther@59741: Init_Proof (ppc, spec) => walther@59741: "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec)) walther@59741: | Model_Problem => "Model_Problem " walther@59741: | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID walther@59741: | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID walther@59741: | Add_Given cterm' => "Add_Given " ^ cterm' walther@59741: | Del_Given cterm' => "Del_Given " ^ cterm' walther@59741: | Add_Find cterm' => "Add_Find " ^ cterm' walther@59741: | Del_Find cterm' => "Del_Find " ^ cterm' walther@59741: | Add_Relation cterm' => "Add_Relation " ^ cterm' walther@59741: | Del_Relation cterm' => "Del_Relation " ^ cterm' walther@59741: walther@59741: | Specify_Theory domID => "Specify_Theory " ^ quote domID walther@59741: | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID walther@59741: | Specify_Method metID => "Specify_Method " ^ strs2str metID walther@59741: | Apply_Method metID => "Apply_Method " ^ strs2str metID walther@59741: | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID walther@59741: | Free_Solve => "Free_Solve" walther@59741: walther@59741: | Rewrite_Inst (subs, (id, thm)) => walther@59741: "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str))) walther@59741: | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str) walther@59741: | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str) walther@59741: | Rewrite_Set_Inst (subs, rls) => walther@59741: "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls) walther@59741: | Rewrite_Set rls => "Rewrite_Set " ^ quote rls walther@59741: | Detail_Set rls => "Detail_Set " ^ quote rls walther@59741: | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls) walther@59741: | End_Detail => "End_Detail" walther@59741: | Derive rls' => "Derive " ^ rls' walther@59741: | Calculate op_ => "Calculate " ^ op_ walther@59741: | Substitute sube => "Substitute " ^ Selem.sube2str sube walther@59741: | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's walther@59741: walther@59741: | Take cterm' => "Take " ^ quote cterm' walther@59741: | Take_Inst cterm' => "Take_Inst " ^ quote cterm' walther@59741: | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID) walther@59741: | End_Subproblem => "End_Subproblem" walther@59741: | CAScmd cterm' => "CAScmd " ^ quote cterm' walther@59741: walther@59741: | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm' walther@59741: | Or_to_List => "Or_to_List " walther@59741: | Collect_Trues => "Collect_Trues" walther@59741: walther@59741: | Empty_Tac => "Empty_Tac" walther@59741: | Tac string => "Tac " ^ string walther@59741: | End_Proof' => "input End_Proof'" walther@59741: | _ => "tac2str not impl. for ?!"; walther@59741: walther@59741: fun is_empty_tac 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@59302: | is_rewtac (Rewrite_Asm _) = true wneuper@59571: | is_rewtac input = is_rewset input; wneuper@59302: wneuper@59302: fun tac2IDstr ma = case ma of wneuper@59302: Model_Problem => "Model_Problem" wneuper@59302: | Refine_Tacitly _ => "Refine_Tacitly" wneuper@59302: | Refine_Problem _ => "Refine_Problem" wneuper@59302: | Add_Given _ => "Add_Given" wneuper@59302: | Del_Given _ => "Del_Given" wneuper@59302: | Add_Find _ => "Add_Find" wneuper@59302: | Del_Find _ => "Del_Find" wneuper@59302: | Add_Relation _ => "Add_Relation" wneuper@59302: | Del_Relation _ => "Del_Relation" wneuper@59302: wneuper@59302: | Specify_Theory _ => "Specify_Theory" wneuper@59302: | Specify_Problem _ => "Specify_Problem" wneuper@59302: | Specify_Method _ => "Specify_Method" wneuper@59302: | Apply_Method _ => "Apply_Method" wneuper@59302: | Check_Postcond _ => "Check_Postcond" wneuper@59302: | Free_Solve => "Free_Solve" wneuper@59302: wneuper@59302: | Rewrite_Inst _ => "Rewrite_Inst" wneuper@59302: | Rewrite _ => "Rewrite" wneuper@59302: | Rewrite_Asm _ => "Rewrite_Asm" wneuper@59302: | Rewrite_Set_Inst _ => "Rewrite_Set_Inst" wneuper@59302: | Rewrite_Set _ => "Rewrite_Set" wneuper@59302: | Detail_Set _ => "Detail_Set" wneuper@59302: | Detail_Set_Inst _ => "Detail_Set_Inst" wneuper@59302: | Derive _ => "Derive " wneuper@59302: | Calculate _ => "Calculate " wneuper@59302: | Substitute _ => "Substitute" wneuper@59302: | Apply_Assumption _ => "Apply_Assumption" wneuper@59302: wneuper@59302: | Take _ => "Take" wneuper@59302: | Take_Inst _ => "Take_Inst" wneuper@59302: | Subproblem _ => "Subproblem" wneuper@59302: | End_Subproblem => "End_Subproblem" wneuper@59302: | CAScmd _ => "CAScmd" wneuper@59302: wneuper@59302: | Check_elementwise _ => "Check_elementwise" wneuper@59302: | Or_to_List => "Or_to_List " wneuper@59302: | Collect_Trues => "Collect_Trues" wneuper@59302: wneuper@59302: | Empty_Tac => "Empty_Tac" wneuper@59302: | Tac _ => "Tac " wneuper@59302: | End_Proof' => "End_Proof'" wneuper@59302: | _ => "tac2str not impl. for ?!"; wneuper@59302: wneuper@59302: fun rls_of (Rewrite_Set_Inst (_, rls)) = rls wneuper@59302: | rls_of (Rewrite_Set rls) = rls wneuper@59571: | rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\""); wneuper@59302: wneuper@59416: fun rule2tac thy _ (Rule.Calc (opID, _)) = Calculate (assoc_calc thy opID) wneuper@59416: | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm'' wneuper@59416: | rule2tac _ subst (Rule.Thm thm'') = wneuper@59302: Rewrite_Inst (Selem.subst2subs subst, thm'') wneuper@59416: | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule.id_rls rls) wneuper@59416: | rule2tac _ subst (Rule.Rls_ rls) = wneuper@59416: Rewrite_Set_Inst (Selem.subst2subs subst, (Rule.id_rls rls)) wneuper@59302: | rule2tac _ _ rule = wneuper@59416: error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\""); wneuper@59302: wneuper@59571: (* tactics for for internal use, compare "input" for user at the front-end. wneuper@59302: tac_ contains results from check in 'fun applicable_in'. wneuper@59302: This is useful for costly results, e.g. from rewriting; wneuper@59302: however, these results might be changed by Scripts like wneuper@59499: " eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^ wneuper@59302: " eq = (Rewrite_Set equival_trans False) eq;" ^ wneuper@59302: TODO.WN120106 ANALOGOUSLY TO Substitute': wneuper@59302: So tac_ contains the term t the result was calculated from wneuper@59302: in order to compare t with t' possibly changed by "Expr " wneuper@59302: and re-calculate result if t<>t' wneuper@59302: TODO.WN161219: replace *every* cterm' by term wneuper@59302: *) walther@59741: datatype T = walther@59741: Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list walther@59741: | Add_Relation' of Rule.cterm' * Model.itm list walther@59741: | Apply_Assumption' of term list * term walther@59741: | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context walther@59741: (*/--- TODO: re-design ? -----------------------------------------------------------------\*) walther@59741: | Begin_Sequ' | Begin_Trans' of term walther@59741: | Split_And' of term | Split_Or' of term | Split_Intersect' of term walther@59741: | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term walther@59741: | End_Sequ' | End_Trans' of Selem.result walther@59741: | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof'' walther@59741: (*\--- TODO: re-design ? -----------------------------------------------------------------/*) walther@59741: | CAScmd' of term walther@59741: | Calculate' of Rule.theory' * string * term * (term * Celem.thm') walther@59741: | Check_Postcond' of Celem.pblID * walther@59741: Selem.result (* returnvalue of script in solve *) walther@59741: | Check_elementwise' of (*special case:*) walther@59741: term * (* (1) the current formula: [x=1,x=...] *) walther@59741: string * (* (2) the pred from Check_elementwise *) walther@59741: Selem.result (* (3) composed from (1) and (2): {x. pred} *) walther@59741: | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm' wneuper@59302: walther@59741: | Derive' of Rule.rls walther@59741: | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result walther@59741: | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result walther@59741: | End_Detail' of Selem.result walther@59741: walther@59741: | Empty_Tac_ walther@59741: | Free_Solve' walther@59741: walther@59741: | Init_Proof' of Rule.cterm' list * Celem.spec walther@59741: | Model_Problem' of Celem.pblID * walther@59741: Model.itm list * (* the 'untouched' pbl *) walther@59741: Model.itm list (* the casually completed met *) walther@59741: | Or_to_List' of term * term walther@59741: | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list) walther@59741: | Refine_Tacitly' of walther@59741: Celem.pblID * (* input*) walther@59741: Celem.pblID * (* the refined from applicable_in *) walther@59741: Rule.domID * (* from new pbt?! filled in specify *) walther@59741: Celem.metID * (* from new pbt?! filled in specify *) walther@59741: Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *) walther@59741: | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result walther@59741: | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result walther@59741: | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result walther@59741: | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result walther@59741: | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result walther@59741: walther@59741: | Specify_Method' of Celem.metID * Model.ori list * Model.itm list walther@59741: | Specify_Problem' of Celem.pblID * walther@59741: (bool * (* matches *) walther@59741: (Model.itm list * (* ppc *) walther@59741: (bool * term) list)) (* preconditions *) walther@59741: | Specify_Theory' of Rule.domID walther@59741: | Subproblem' of walther@59741: Celem.spec * walther@59741: (Model.ori list) * (* filled in associate Subproblem' *) walther@59741: term * (* filled -"-, headline of calc-head *) walther@59741: Selem.fmz_ * walther@59741: Proof.context * (* DEPRECATED shifted into loc for all ppobj *) walther@59741: term (* Subproblem (thyID, pbl) OR cascmd *) walther@59741: | Substitute' of walther@59741: Rule.rew_ord_ * (* for re-calculation *) walther@59741: Rule.rls * (* for re-calculation *) walther@59741: Selem.subte * (* the 'substitution': terms of type bool *) walther@59741: term * (* to be substituted into *) walther@59741: term (* resulting from the substitution *) walther@59741: | Tac_ of theory * string * string * string walther@59741: | Take' of term | Take_Inst' of term walther@59741: walther@59741: fun string_of ma = case ma of walther@59741: Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec) walther@59741: | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID walther@59741: | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^ walther@59741: strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)" walther@59741: | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")" walther@59741: | Add_Given' _ => "Add_Given' "(*^cterm'*) walther@59741: | Del_Given' _ => "Del_Given' "(*^cterm'*) walther@59741: | Add_Find' _ => "Add_Find' "(*^cterm'*) walther@59741: | Del_Find' _ => "Del_Find' "(*^cterm'*) walther@59741: | Add_Relation' _ => "Add_Relation' "(*^cterm'*) walther@59741: | Del_Relation' _ => "Del_Relation' "(*^cterm'*) walther@59741: walther@59741: | Specify_Theory' domID => "Specify_Theory' " ^ quote domID walther@59741: | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^ walther@59741: spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre"))) walther@59741: | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^ walther@59741: Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )" walther@59741: walther@59741: | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID walther@59741: | Check_Postcond' (pblID, (scval, asm)) => "Check_Postcond' " ^ walther@59741: (spair2str (strs2str pblID, spair2str (Rule.term2str scval, Rule.terms2str asm))) walther@59741: walther@59741: | Free_Solve' => "Free_Solve'" walther@59741: walther@59741: | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*) walther@59741: | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*) walther@59741: | Rewrite_Asm' _(*thm'*) => "Rewrite_Asm' "(*^(spair2str thm')*) walther@59741: | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*) walther@59741: | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^ walther@59741: "," ^ Rule.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))" walther@59741: | End_Detail' _ => "End_Detail' xxx" walther@59741: | Detail_Set' _ => "Detail_Set' xxx" walther@59741: | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx" walther@59741: walther@59741: | Derive' rls => "Derive' " ^ Rule.id_rls rls walther@59741: | Calculate' _ => "Calculate' " walther@59741: | Substitute' _ => "Substitute' "(*^(subs2str subs)*) walther@59741: | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*) walther@59741: walther@59741: | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*) walther@59741: | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*) walther@59741: | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) => walther@59741: "Subproblem' "(*^(pair2str (domID, strs2str ,))*) walther@59741: | End_Subproblem' _ => "End_Subproblem'" walther@59741: | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*) walther@59741: walther@59741: | Empty_Tac_ => "Empty_Tac_" walther@59741: | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")" walther@59741: | _ => "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@59704: | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm) walther@59704: walther@59704: | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule.id_rls rls) walther@59704: | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule.id_rls rls) walther@59704: walther@59704: | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) = walther@59704: Rewrite_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls) walther@59704: | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) = walther@59704: Detail_Set_Inst (Selem.subst2subs sub, Rule.id_rls 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@59704: | input_from_T (Take' term) = Take (Rule.term2str term) walther@59704: | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Selem.subte2sube 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@59728: | input_from_T m = 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@59728: | 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@59749: fun for_specify (Init_Proof _) = true walther@59749: | for_specify Model_Problem = true walther@59749: | for_specify (Refine_Tacitly _) = true walther@59749: | for_specify (Refine_Problem _) = true walther@59749: | for_specify (Add_Given _) = true walther@59749: | for_specify (Del_Given _) = true walther@59749: | for_specify (Add_Find _) = true walther@59749: | for_specify (Del_Find _) = true walther@59749: | for_specify (Add_Relation _) = true walther@59749: | for_specify (Del_Relation _) = true walther@59749: | for_specify (Specify_Theory _) = true walther@59749: | for_specify (Specify_Problem _) = true walther@59749: | for_specify (Specify_Method _) = true walther@59749: | for_specify _ = false walther@59749: fun for_specify' (Init_Proof' _) = true walther@59749: | for_specify' (Model_Problem' _) = true walther@59749: | for_specify' (Refine_Tacitly' _) = true walther@59749: | for_specify' (Refine_Problem' _) = true walther@59749: | for_specify' (Add_Given' _) = true walther@59749: | for_specify' (Del_Given' _) = true walther@59749: | for_specify' (Add_Find' _) = true walther@59749: | for_specify' (Del_Find' _) = true walther@59749: | for_specify' (Add_Relation' _) = true walther@59749: | for_specify' (Del_Relation' _) = true walther@59749: | for_specify' (Specify_Theory' _) = true walther@59749: | for_specify' (Specify_Problem' _) = true walther@59749: | for_specify' (Specify_Method' _) = true walther@59749: | for_specify' _ = false walther@59749: walther@59728: (**)end(**)