1.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Dec 17 16:35:29 2019 +0100
1.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Dec 17 17:19:34 2019 +0100
1.3 @@ -12,12 +12,13 @@
1.4 ML_file mstools.sml
1.5 ML_file "specification-elems.sml"
1.6 ML_file "istate-def.sml"
1.7 - ML_file tactic.sml
1.8 + ML_file "tactic-def.sml"
1.9 ML_file position.sml
1.10 ML_file "ctree-basic.sml"
1.11 ML_file "ctree-access.sml"
1.12 ML_file "ctree-navi.sml"
1.13 ML_file ctree.sml
1.14 + ML_file tactic.sml
1.15
1.16 ML \<open>
1.17 \<close> ML \<open>
2.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Tue Dec 17 16:35:29 2019 +0100
2.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Tue Dec 17 17:19:34 2019 +0100
2.3 @@ -19,7 +19,7 @@
2.4 val update_oris : CTbasic.ctree -> CTbasic.pos -> Model.ori list -> CTbasic.ctree
2.5 val update_orispec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree
2.6 val update_spec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree
2.7 - val update_tac : CTbasic.ctree -> CTbasic.pos -> Tactic.input -> CTbasic.ctree
2.8 + val update_tac : CTbasic.ctree -> CTbasic.pos -> Tactic_Def.input -> CTbasic.ctree
2.9
2.10 val upd_istate_ctxt : CTbasic.state -> Istate_Def.T * Proof.context -> CTbasic.ctree
2.11 val upd_istate : CTbasic.state -> Istate_Def.T -> CTbasic.ctree
2.12 @@ -32,13 +32,13 @@
2.13 val append_result : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context ->
2.14 Selem.result -> CTbasic.ostate -> CTbasic.ctree * 'a list
2.15 val append_atomic : (* for solve.sml *)
2.16 - CTbasic.pos -> Istate_Def.T * Proof.context -> term -> Tactic.input -> Selem.result ->
2.17 + CTbasic.pos -> Istate_Def.T * Proof.context -> term -> Tactic_Def.input -> Selem.result ->
2.18 CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree
2.19 val cappend_atomic : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> term ->
2.20 - Tactic.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * CTbasic.pos' list
2.21 + Tactic_Def.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * CTbasic.pos' list
2.22 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.23 val cappend_parent : CTbasic.ctree -> int list -> Istate_Def.T * Proof.context -> term ->
2.24 - Tactic.input -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list
2.25 + Tactic_Def.input -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list
2.26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.27 val update_loc' : CTbasic.ctree -> CTbasic.pos ->
2.28 (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option -> CTbasic.ctree
2.29 @@ -208,7 +208,7 @@
2.30
2.31 (* called by Take *)
2.32 fun append_form p l f pt =
2.33 - insert_pt (PrfObj {cell = NONE, form = f, tac = Tactic.Empty_Tac, loc = (SOME l, NONE),
2.34 + insert_pt (PrfObj {cell = NONE, form = f, tac = Tactic_Def.Empty_Tac, loc = (SOME l, NONE),
2.35 branch = NoBranch, result = (Rule.e_term, []), ostate = Incomplete}) pt p;
2.36 fun cappend_form pt p loc f =
2.37 let
2.38 @@ -232,7 +232,7 @@
2.39 fun append_parent p l f r b pt =
2.40 let
2.41 val (ll, f) =
2.42 - if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)
2.43 + if existpt p pt andalso Tactic_Def.is_empty_tac (get_obj g_tac pt p)
2.44 then ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p)
2.45 else ((SOME l, NONE), f)
2.46 in insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = ll,
2.47 @@ -244,7 +244,7 @@
2.48 fun append_atomic p l f r f' s pt =
2.49 let
2.50 val (iss, f) =
2.51 - if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)
2.52 + if existpt p pt andalso Tactic_Def.is_empty_tac (get_obj g_tac pt p)
2.53 then (*after Take*) ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p)
2.54 else ((NONE, SOME l), f)
2.55 in
2.56 @@ -257,7 +257,7 @@
2.57 cut decided in applicable_in !?!
2.58 *)
2.59 fun cappend_atomic pt p ist_res f r f' s =
2.60 - if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)
2.61 + if existpt p pt andalso Tactic_Def.is_empty_tac (get_obj g_tac pt p)
2.62 then (*after Take: transfer Frm and respective istate*)
2.63 let
2.64 val (ist_form, f) =
3.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Dec 17 16:35:29 2019 +0100
3.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Dec 17 17:19:34 2019 +0100
3.3 @@ -42,7 +42,7 @@
3.4 result: Selem.result,
3.5
3.6 form: term,
3.7 - tac: Tactic.input}
3.8 + tac: Tactic_Def.input}
3.9 datatype ctree = EmptyPtree | Nd of ppobj * ctree list
3.10
3.11 (** basic functions **)
3.12 @@ -68,7 +68,7 @@
3.13 val g_met : ppobj -> Model.itm list
3.14 val g_metID : ppobj -> Celem.metID
3.15 val g_result : ppobj -> Selem.result
3.16 - val g_tac : ppobj -> Tactic.input
3.17 + val g_tac : ppobj -> Tactic_Def.input
3.18 val g_domID : ppobj -> Rule.domID (* for appl.sml TODO: replace by thyID *)
3.19 val g_env : ppobj -> (Istate_Def.T * Proof.context) option (* for appl.sml *)
3.20
3.21 @@ -173,7 +173,7 @@
3.22 used for continuing eval script + for generate *)
3.23 type ets =
3.24 (Celem.path *(* of tactic in scr, tactic (weakly) associated with tac_ *)
3.25 - (Tactic.T * (* (for generate) *)
3.26 + (Tactic_Def.T * (* (for generate) *)
3.27 Env.T * (* with 'tactic=result' as rule, tactic ev. _not_ ready for 'parallel let' *)
3.28 Env.T * (* with results of (ready) tacs *)
3.29 term * (* itr_arg of tactic, for upd. env at Repeat, Try *)
3.30 @@ -182,7 +182,7 @@
3.31 list;
3.32
3.33 fun ets2s (l,(m,eno,env,iar,res,s)) =
3.34 - "\n(" ^ Celem.path2str l ^ ",(" ^ Tactic.string_of m ^
3.35 + "\n(" ^ Celem.path2str l ^ ",(" ^ Tactic_Def.string_of m ^
3.36 ",\n ens= " ^ Env.subst2str eno ^
3.37 ",\n env= " ^ Env.subst2str env ^
3.38 ",\n iar= " ^ Rule.term2str iar ^
3.39 @@ -200,7 +200,7 @@
3.40 PrfObj of
3.41 {cell : Celem.lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *)
3.42 form : term, (* where tac is applied to *)
3.43 - tac : Tactic.input, (* also in istate *)
3.44 + tac : Tactic_Def.input, (* also in istate *)
3.45 loc : (Istate_Def.T * (* script interpreter state *)
3.46 Proof.context) (* context for provers, type inference *)
3.47 option * (* both for interpreter location on Frm, Pbl, Met *)
3.48 @@ -333,7 +333,7 @@
3.49 | g_loc (PrfObj {loc = l, ...}) = l;
3.50 fun g_branch (PblObj {branch = b, ...}) = b
3.51 | g_branch (PrfObj {branch = b, ...}) = b;
3.52 -fun g_tac (PblObj {spec = (_, _, m),...}) = Tactic.Apply_Method m
3.53 +fun g_tac (PblObj {spec = (_, _, m),...}) = Tactic_Def.Apply_Method m
3.54 | g_tac (PrfObj {tac = m, ...}) = m;
3.55 fun g_result (PblObj {result = r, ...}) = r
3.56 | g_result (PrfObj {result = r, ...}) = r;
3.57 @@ -415,8 +415,8 @@
3.58 if is_pblobj (get_obj I pt p)
3.59 then (true, p, Rule.Erls)
3.60 else case get_obj g_tac pt p of
3.61 - Tactic.Rewrite_Set rls' => (false, p, assoc_rls rls')
3.62 - | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, assoc_rls rls')
3.63 + Tactic_Def.Rewrite_Set rls' => (false, p, assoc_rls rls')
3.64 + | Tactic_Def.Rewrite_Set_Inst (_, rls') => (false, p, assoc_rls rls')
3.65 | _ => par pt (lev_up p)
3.66 in par pt (lev_up p) end;
3.67
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/isac/MathEngBasic/tactic-def.sml Tue Dec 17 17:19:34 2019 +0100
4.3 @@ -0,0 +1,363 @@
4.4 +(* Title: Tactics; tac_ for interaction with frontend, input for internal use.
4.5 + Author: Walther Neuper 170121
4.6 + (c) due to copyright terms
4.7 +
4.8 +regular expression for search:
4.9 +
4.10 +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
4.11 +
4.12 +*)
4.13 +signature TACTIC_DEF =
4.14 +sig
4.15 + datatype T =
4.16 + Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
4.17 + | Add_Relation' of Rule.cterm' * Model.itm list
4.18 + | Apply_Assumption' of term list * term
4.19 + | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
4.20 +
4.21 + | Begin_Sequ' | Begin_Trans' of term
4.22 + | Split_And' of term | Split_Or' of term | Split_Intersect' of term
4.23 + | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
4.24 + | End_Sequ' | End_Trans' of Selem.result
4.25 + | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
4.26 +
4.27 + | CAScmd' of term
4.28 + | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
4.29 + | Check_Postcond' of Celem.pblID * Selem.result
4.30 + | Check_elementwise' of term * Rule.cterm' * Selem.result
4.31 + | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
4.32 +
4.33 + | Derive' of Rule.rls
4.34 + | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
4.35 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
4.36 + | End_Detail' of Selem.result
4.37 +
4.38 + | Empty_Tac_
4.39 + | Free_Solve'
4.40 +
4.41 + | Init_Proof' of Rule.cterm' list * Celem.spec
4.42 + | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
4.43 + | Or_to_List' of term * term
4.44 + | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
4.45 + | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
4.46 +
4.47 + | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
4.48 + | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
4.49 + | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
4.50 + | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
4.51 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
4.52 +
4.53 + | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
4.54 + | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
4.55 + | Specify_Theory' of Rule.domID
4.56 + | Subproblem' of Celem.spec * Model.ori list * term * Selem.fmz_ * Proof.context * term
4.57 + | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
4.58 + | Tac_ of theory * string * string * string
4.59 + | Take' of term | Take_Inst' of term
4.60 + val string_of : T -> string
4.61 +
4.62 + datatype input =
4.63 + Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
4.64 + | Apply_Assumption of Rule.cterm' list
4.65 + | Apply_Method of Celem.metID
4.66 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
4.67 + | Begin_Sequ | Begin_Trans
4.68 + | Split_And | Split_Or | Split_Intersect
4.69 + | Conclude_And | Conclude_Or | Collect_Trues
4.70 + | End_Sequ | End_Trans
4.71 + | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
4.72 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
4.73 + | CAScmd of Rule.cterm'
4.74 + | Calculate of string
4.75 + | Check_Postcond of Celem.pblID
4.76 + | Check_elementwise of Rule.cterm'
4.77 + | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
4.78 +
4.79 + | Derive of Rule.rls'
4.80 + | Detail_Set of Rule.rls'
4.81 + | Detail_Set_Inst of Selem.subs * Rule.rls'
4.82 + | End_Detail
4.83 +
4.84 + | Empty_Tac
4.85 + | Free_Solve
4.86 +
4.87 + | Init_Proof of Rule.cterm' list * Celem.spec
4.88 + | Model_Problem
4.89 + | Or_to_List
4.90 + | Refine_Problem of Celem.pblID
4.91 + | Refine_Tacitly of Celem.pblID
4.92 +
4.93 + | Rewrite of Celem.thm''
4.94 + | Rewrite_Asm of Celem.thm''
4.95 + | Rewrite_Inst of Selem.subs * Celem.thm''
4.96 + | Rewrite_Set of Rule.rls'
4.97 + | Rewrite_Set_Inst of Selem.subs * Rule.rls'
4.98 +
4.99 + | Specify_Method of Celem.metID
4.100 + | Specify_Problem of Celem.pblID
4.101 + | Specify_Theory of Rule.domID
4.102 + | Subproblem of Rule.domID * Celem.pblID
4.103 +
4.104 + | Substitute of Selem.sube
4.105 + | Tac of string
4.106 + | Take of Rule.cterm' | Take_Inst of Rule.cterm'
4.107 + val tac2str : input -> string
4.108 +
4.109 + val is_empty_tac : input -> bool
4.110 +end
4.111 +
4.112 +(**)
4.113 +structure Tactic_Def(**): TACTIC_DEF(**) =
4.114 +struct
4.115 +(**)
4.116 +
4.117 +(* tactics for user at front-end.
4.118 + input propagates the construction of the calc-tree;
4.119 + there are
4.120 + (a) 'specsteps' for the specify-phase, and others for the solve-phase
4.121 + (b) those of the solve-phase are 'initac's and others;
4.122 + initacs start with a formula different from the preceding formula.
4.123 + see 'type tac_' for the internal representation of tactics
4.124 +*)
4.125 +datatype input =
4.126 + Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
4.127 + | Apply_Assumption of Rule.cterm' list
4.128 + | Apply_Method of Celem.metID
4.129 + (* creates an "istate" in PblObj.env; in case of "init_form"
4.130 + creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
4.131 + a "SOME istate" at fst of "loc".
4.132 + As each step (in the solve-phase) has a resulting formula (at the front-end)
4.133 + Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *)
4.134 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
4.135 + | Begin_Sequ | Begin_Trans
4.136 + | Split_And | Split_Or | Split_Intersect
4.137 + | Conclude_And | Conclude_Or | Collect_Trues
4.138 + | End_Sequ | End_Trans
4.139 + | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
4.140 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
4.141 + | CAScmd of Rule.cterm'
4.142 + | Calculate of string
4.143 + | Check_Postcond of Celem.pblID
4.144 + | Check_elementwise of Rule.cterm'
4.145 + | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
4.146 +
4.147 + | Derive of Rule.rls' (* WN0509 drop *)
4.148 + | Detail_Set of Rule.rls' (* WN0509 drop *)
4.149 + | Detail_Set_Inst of Selem.subs * Rule.rls' (* WN0509 drop *)
4.150 + | End_Detail (* WN0509 drop *)
4.151 +
4.152 + | Empty_Tac
4.153 + | Free_Solve
4.154 +
4.155 + | Init_Proof of Rule.cterm' list * Celem.spec
4.156 + | Model_Problem
4.157 + | Or_to_List
4.158 + | Refine_Problem of Celem.pblID
4.159 + | Refine_Tacitly of Celem.pblID
4.160 +
4.161 + (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
4.162 + because there all the thms are present with both (thmID, thm)
4.163 + (where user-views can show both or only one of (thmID, thm)),
4.164 + and thm is created from ThmID by assoc_thm'' when entering isabisac *)
4.165 + | Rewrite of Celem.thm''
4.166 + | Rewrite_Asm of Celem.thm''
4.167 + | Rewrite_Inst of Selem.subs * Celem.thm''
4.168 + | Rewrite_Set of Rule.rls'
4.169 + | Rewrite_Set_Inst of Selem.subs * Rule.rls'
4.170 +
4.171 + | Specify_Method of Celem.metID
4.172 + | Specify_Problem of Celem.pblID
4.173 + | Specify_Theory of Rule.domID
4.174 + | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
4.175 +
4.176 + | Substitute of Selem.sube
4.177 + | Tac of string (* WN0509 drop *)
4.178 + | Take of Rule.cterm' | Take_Inst of Rule.cterm'
4.179 +
4.180 +fun tac2str ma = case ma of
4.181 + Init_Proof (ppc, spec) =>
4.182 + "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec))
4.183 + | Model_Problem => "Model_Problem "
4.184 + | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
4.185 + | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
4.186 + | Add_Given cterm' => "Add_Given " ^ cterm'
4.187 + | Del_Given cterm' => "Del_Given " ^ cterm'
4.188 + | Add_Find cterm' => "Add_Find " ^ cterm'
4.189 + | Del_Find cterm' => "Del_Find " ^ cterm'
4.190 + | Add_Relation cterm' => "Add_Relation " ^ cterm'
4.191 + | Del_Relation cterm' => "Del_Relation " ^ cterm'
4.192 +
4.193 + | Specify_Theory domID => "Specify_Theory " ^ quote domID
4.194 + | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
4.195 + | Specify_Method metID => "Specify_Method " ^ strs2str metID
4.196 + | Apply_Method metID => "Apply_Method " ^ strs2str metID
4.197 + | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
4.198 + | Free_Solve => "Free_Solve"
4.199 +
4.200 + | Rewrite_Inst (subs, (id, thm)) =>
4.201 + "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str)))
4.202 + | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
4.203 + | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
4.204 + | Rewrite_Set_Inst (subs, rls) =>
4.205 + "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
4.206 + | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
4.207 + | Detail_Set rls => "Detail_Set " ^ quote rls
4.208 + | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
4.209 + | End_Detail => "End_Detail"
4.210 + | Derive rls' => "Derive " ^ rls'
4.211 + | Calculate op_ => "Calculate " ^ op_
4.212 + | Substitute sube => "Substitute " ^ Selem.sube2str sube
4.213 + | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
4.214 +
4.215 + | Take cterm' => "Take " ^ quote cterm'
4.216 + | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
4.217 + | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
4.218 + | End_Subproblem => "End_Subproblem"
4.219 + | CAScmd cterm' => "CAScmd " ^ quote cterm'
4.220 +
4.221 + | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
4.222 + | Or_to_List => "Or_to_List "
4.223 + | Collect_Trues => "Collect_Trues"
4.224 +
4.225 + | Empty_Tac => "Empty_Tac"
4.226 + | Tac string => "Tac " ^ string
4.227 + | End_Proof' => "input End_Proof'"
4.228 + | _ => "tac2str not impl. for ?!";
4.229 +
4.230 +fun is_empty_tac input = case input of Empty_Tac => true | _ => false
4.231 +
4.232 +(* tactics for for internal use, compare "input" for user at the front-end.
4.233 + tac_ contains results from check in 'fun applicable_in'.
4.234 + This is useful for costly results, e.g. from rewriting;
4.235 + however, these results might be changed by Scripts like
4.236 + " eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
4.237 + " eq = (Rewrite_Set equival_trans False) eq;" ^
4.238 + TODO.WN120106 ANALOGOUSLY TO Substitute':
4.239 + So tac_ contains the term t the result was calculated from
4.240 + in order to compare t with t' possibly changed by "Expr "
4.241 + and re-calculate result if t<>t'
4.242 + TODO.WN161219: replace *every* cterm' by term
4.243 +*)
4.244 + datatype T =
4.245 + Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
4.246 + | Add_Relation' of Rule.cterm' * Model.itm list
4.247 + | Apply_Assumption' of term list * term
4.248 + | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
4.249 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
4.250 + | Begin_Sequ' | Begin_Trans' of term
4.251 + | Split_And' of term | Split_Or' of term | Split_Intersect' of term
4.252 + | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
4.253 + | End_Sequ' | End_Trans' of Selem.result
4.254 + | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
4.255 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
4.256 + | CAScmd' of term
4.257 + | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
4.258 + | Check_Postcond' of Celem.pblID *
4.259 + Selem.result (* returnvalue of script in solve *)
4.260 + | Check_elementwise' of (*special case:*)
4.261 + term * (* (1) the current formula: [x=1,x=...] *)
4.262 + string * (* (2) the pred from Check_elementwise *)
4.263 + Selem.result (* (3) composed from (1) and (2): {x. pred} *)
4.264 + | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
4.265 +
4.266 + | Derive' of Rule.rls
4.267 + | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
4.268 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
4.269 + | End_Detail' of Selem.result
4.270 +
4.271 + | Empty_Tac_
4.272 + | Free_Solve'
4.273 +
4.274 + | Init_Proof' of Rule.cterm' list * Celem.spec
4.275 + | Model_Problem' of Celem.pblID *
4.276 + Model.itm list * (* the 'untouched' pbl *)
4.277 + Model.itm list (* the casually completed met *)
4.278 + | Or_to_List' of term * term
4.279 + | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
4.280 + | Refine_Tacitly' of
4.281 + Celem.pblID * (* input*)
4.282 + Celem.pblID * (* the refined from applicable_in *)
4.283 + Rule.domID * (* from new pbt?! filled in specify *)
4.284 + Celem.metID * (* from new pbt?! filled in specify *)
4.285 + Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
4.286 + | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
4.287 + | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
4.288 + | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
4.289 + | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
4.290 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
4.291 +
4.292 + | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
4.293 + | Specify_Problem' of Celem.pblID *
4.294 + (bool * (* matches *)
4.295 + (Model.itm list * (* ppc *)
4.296 + (bool * term) list)) (* preconditions *)
4.297 + | Specify_Theory' of Rule.domID
4.298 + | Subproblem' of
4.299 + Celem.spec *
4.300 + (Model.ori list) * (* filled in associate Subproblem' *)
4.301 + term * (* filled -"-, headline of calc-head *)
4.302 + Selem.fmz_ *
4.303 + Proof.context * (* DEPRECATED shifted into loc for all ppobj *)
4.304 + term (* Subproblem (thyID, pbl) OR cascmd *)
4.305 + | Substitute' of
4.306 + Rule.rew_ord_ * (* for re-calculation *)
4.307 + Rule.rls * (* for re-calculation *)
4.308 + Selem.subte * (* the 'substitution': terms of type bool *)
4.309 + term * (* to be substituted into *)
4.310 + term (* resulting from the substitution *)
4.311 + | Tac_ of theory * string * string * string
4.312 + | Take' of term | Take_Inst' of term
4.313 +
4.314 +fun string_of ma = case ma of
4.315 + Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
4.316 + | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
4.317 + | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
4.318 + strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
4.319 + | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
4.320 + | Add_Given' _ => "Add_Given' "(*^cterm'*)
4.321 + | Del_Given' _ => "Del_Given' "(*^cterm'*)
4.322 + | Add_Find' _ => "Add_Find' "(*^cterm'*)
4.323 + | Del_Find' _ => "Del_Find' "(*^cterm'*)
4.324 + | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
4.325 + | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
4.326 +
4.327 + | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
4.328 + | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
4.329 + spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
4.330 + | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
4.331 + Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
4.332 +
4.333 + | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
4.334 + | Check_Postcond' (pblID, (scval, asm)) => "Check_Postcond' " ^
4.335 + (spair2str (strs2str pblID, spair2str (Rule.term2str scval, Rule.terms2str asm)))
4.336 +
4.337 + | Free_Solve' => "Free_Solve'"
4.338 +
4.339 + | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
4.340 + | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
4.341 + | Rewrite_Asm' _(*thm'*) => "Rewrite_Asm' "(*^(spair2str thm')*)
4.342 + | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
4.343 + | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
4.344 + "," ^ Rule.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
4.345 + | End_Detail' _ => "End_Detail' xxx"
4.346 + | Detail_Set' _ => "Detail_Set' xxx"
4.347 + | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
4.348 +
4.349 + | Derive' rls => "Derive' " ^ Rule.id_rls rls
4.350 + | Calculate' _ => "Calculate' "
4.351 + | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
4.352 + | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*)
4.353 +
4.354 + | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
4.355 + | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*)
4.356 + | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
4.357 + "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
4.358 + | End_Subproblem' _ => "End_Subproblem'"
4.359 + | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
4.360 +
4.361 + | Empty_Tac_ => "Empty_Tac_"
4.362 + | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
4.363 + | _ => "string_of not impl. for arg";
4.364 +
4.365 +
4.366 +(**)end(**)
5.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Tue Dec 17 16:35:29 2019 +0100
5.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Tue Dec 17 17:19:34 2019 +0100
5.3 @@ -9,98 +9,10 @@
5.4 *)
5.5 signature TACTIC =
5.6 sig
5.7 - datatype T =
5.8 - Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
5.9 - | Add_Relation' of Rule.cterm' * Model.itm list
5.10 - | Apply_Assumption' of term list * term
5.11 - | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
5.12 -
5.13 - | Begin_Sequ' | Begin_Trans' of term
5.14 - | Split_And' of term | Split_Or' of term | Split_Intersect' of term
5.15 - | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
5.16 - | End_Sequ' | End_Trans' of Selem.result
5.17 - | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
5.18 -
5.19 - | CAScmd' of term
5.20 - | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
5.21 - | Check_Postcond' of Celem.pblID * Selem.result
5.22 - | Check_elementwise' of term * Rule.cterm' * Selem.result
5.23 - | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
5.24 -
5.25 - | Derive' of Rule.rls
5.26 - | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
5.27 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
5.28 - | End_Detail' of Selem.result
5.29 -
5.30 - | Empty_Tac_
5.31 - | Free_Solve'
5.32 -
5.33 - | Init_Proof' of Rule.cterm' list * Celem.spec
5.34 - | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
5.35 - | Or_to_List' of term * term
5.36 - | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
5.37 - | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
5.38 -
5.39 - | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
5.40 - | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
5.41 - | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
5.42 - | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
5.43 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
5.44 -
5.45 - | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
5.46 - | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
5.47 - | Specify_Theory' of Rule.domID
5.48 - | Subproblem' of Celem.spec * Model.ori list * term * Selem.fmz_ * Proof.context * term
5.49 - | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
5.50 - | Tac_ of theory * string * string * string
5.51 - | Take' of term | Take_Inst' of term
5.52 + datatype T = datatype Tactic_Def.T
5.53 val string_of : T -> string
5.54
5.55 - datatype input =
5.56 - Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
5.57 - | Apply_Assumption of Rule.cterm' list
5.58 - | Apply_Method of Celem.metID
5.59 - (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
5.60 - | Begin_Sequ | Begin_Trans
5.61 - | Split_And | Split_Or | Split_Intersect
5.62 - | Conclude_And | Conclude_Or | Collect_Trues
5.63 - | End_Sequ | End_Trans
5.64 - | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
5.65 - (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
5.66 - | CAScmd of Rule.cterm'
5.67 - | Calculate of string
5.68 - | Check_Postcond of Celem.pblID
5.69 - | Check_elementwise of Rule.cterm'
5.70 - | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
5.71 -
5.72 - | Derive of Rule.rls'
5.73 - | Detail_Set of Rule.rls'
5.74 - | Detail_Set_Inst of Selem.subs * Rule.rls'
5.75 - | End_Detail
5.76 -
5.77 - | Empty_Tac
5.78 - | Free_Solve
5.79 -
5.80 - | Init_Proof of Rule.cterm' list * Celem.spec
5.81 - | Model_Problem
5.82 - | Or_to_List
5.83 - | Refine_Problem of Celem.pblID
5.84 - | Refine_Tacitly of Celem.pblID
5.85 -
5.86 - | Rewrite of Celem.thm''
5.87 - | Rewrite_Asm of Celem.thm''
5.88 - | Rewrite_Inst of Selem.subs * Celem.thm''
5.89 - | Rewrite_Set of Rule.rls'
5.90 - | Rewrite_Set_Inst of Selem.subs * Rule.rls'
5.91 -
5.92 - | Specify_Method of Celem.metID
5.93 - | Specify_Problem of Celem.pblID
5.94 - | Specify_Theory of Rule.domID
5.95 - | Subproblem of Rule.domID * Celem.pblID
5.96 -
5.97 - | Substitute of Selem.sube
5.98 - | Tac of string
5.99 - | Take of Rule.cterm' | Take_Inst of Rule.cterm'
5.100 + datatype input = datatype Tactic_Def.input
5.101 val tac2str : input -> string
5.102
5.103 val eq_tac : input * input -> bool
5.104 @@ -138,112 +50,11 @@
5.105 initacs start with a formula different from the preceding formula.
5.106 see 'type tac_' for the internal representation of tactics
5.107 *)
5.108 -datatype input =
5.109 - Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
5.110 - | Apply_Assumption of Rule.cterm' list
5.111 - | Apply_Method of Celem.metID
5.112 - (* creates an "istate" in PblObj.env; in case of "init_form"
5.113 - creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
5.114 - a "SOME istate" at fst of "loc".
5.115 - As each step (in the solve-phase) has a resulting formula (at the front-end)
5.116 - Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *)
5.117 - (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
5.118 - | Begin_Sequ | Begin_Trans
5.119 - | Split_And | Split_Or | Split_Intersect
5.120 - | Conclude_And | Conclude_Or | Collect_Trues
5.121 - | End_Sequ | End_Trans
5.122 - | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
5.123 - (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
5.124 - | CAScmd of Rule.cterm'
5.125 - | Calculate of string
5.126 - | Check_Postcond of Celem.pblID
5.127 - | Check_elementwise of Rule.cterm'
5.128 - | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
5.129 +datatype input = datatype Tactic_Def.input
5.130
5.131 - | Derive of Rule.rls' (* WN0509 drop *)
5.132 - | Detail_Set of Rule.rls' (* WN0509 drop *)
5.133 - | Detail_Set_Inst of Selem.subs * Rule.rls' (* WN0509 drop *)
5.134 - | End_Detail (* WN0509 drop *)
5.135 +val tac2str = Tactic_Def.tac2str
5.136
5.137 - | Empty_Tac
5.138 - | Free_Solve
5.139 -
5.140 - | Init_Proof of Rule.cterm' list * Celem.spec
5.141 - | Model_Problem
5.142 - | Or_to_List
5.143 - | Refine_Problem of Celem.pblID
5.144 - | Refine_Tacitly of Celem.pblID
5.145 -
5.146 - (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
5.147 - because there all the thms are present with both (thmID, thm)
5.148 - (where user-views can show both or only one of (thmID, thm)),
5.149 - and thm is created from ThmID by assoc_thm'' when entering isabisac *)
5.150 - | Rewrite of Celem.thm''
5.151 - | Rewrite_Asm of Celem.thm''
5.152 - | Rewrite_Inst of Selem.subs * Celem.thm''
5.153 - | Rewrite_Set of Rule.rls'
5.154 - | Rewrite_Set_Inst of Selem.subs * Rule.rls'
5.155 -
5.156 - | Specify_Method of Celem.metID
5.157 - | Specify_Problem of Celem.pblID
5.158 - | Specify_Theory of Rule.domID
5.159 - | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
5.160 -
5.161 - | Substitute of Selem.sube
5.162 - | Tac of string (* WN0509 drop *)
5.163 - | Take of Rule.cterm' | Take_Inst of Rule.cterm'
5.164 -
5.165 -fun tac2str ma = case ma of
5.166 - Init_Proof (ppc, spec) =>
5.167 - "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec))
5.168 - | Model_Problem => "Model_Problem "
5.169 - | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
5.170 - | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
5.171 - | Add_Given cterm' => "Add_Given " ^ cterm'
5.172 - | Del_Given cterm' => "Del_Given " ^ cterm'
5.173 - | Add_Find cterm' => "Add_Find " ^ cterm'
5.174 - | Del_Find cterm' => "Del_Find " ^ cterm'
5.175 - | Add_Relation cterm' => "Add_Relation " ^ cterm'
5.176 - | Del_Relation cterm' => "Del_Relation " ^ cterm'
5.177 -
5.178 - | Specify_Theory domID => "Specify_Theory " ^ quote domID
5.179 - | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
5.180 - | Specify_Method metID => "Specify_Method " ^ strs2str metID
5.181 - | Apply_Method metID => "Apply_Method " ^ strs2str metID
5.182 - | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
5.183 - | Free_Solve => "Free_Solve"
5.184 -
5.185 - | Rewrite_Inst (subs, (id, thm)) =>
5.186 - "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str)))
5.187 - | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
5.188 - | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
5.189 - | Rewrite_Set_Inst (subs, rls) =>
5.190 - "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
5.191 - | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
5.192 - | Detail_Set rls => "Detail_Set " ^ quote rls
5.193 - | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
5.194 - | End_Detail => "End_Detail"
5.195 - | Derive rls' => "Derive " ^ rls'
5.196 - | Calculate op_ => "Calculate " ^ op_
5.197 - | Substitute sube => "Substitute " ^ Selem.sube2str sube
5.198 - | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
5.199 -
5.200 - | Take cterm' => "Take " ^ quote cterm'
5.201 - | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
5.202 - | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
5.203 - | End_Subproblem => "End_Subproblem"
5.204 - | CAScmd cterm' => "CAScmd " ^ quote cterm'
5.205 -
5.206 - | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
5.207 - | Or_to_List => "Or_to_List "
5.208 - | Collect_Trues => "Collect_Trues"
5.209 -
5.210 - | Empty_Tac => "Empty_Tac"
5.211 - | Tac string => "Tac " ^ string
5.212 - | End_Proof' => "input End_Proof'"
5.213 - | _ => "tac2str not impl. for ?!";
5.214 -
5.215 -fun is_empty_tac input = case input of Empty_Tac => true | _ => false
5.216 +val is_empty_tac = Tactic_Def.is_empty_tac
5.217
5.218 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
5.219 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
5.220 @@ -331,126 +142,9 @@
5.221 and re-calculate result if t<>t'
5.222 TODO.WN161219: replace *every* cterm' by term
5.223 *)
5.224 - datatype T =
5.225 - Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
5.226 - | Add_Relation' of Rule.cterm' * Model.itm list
5.227 - | Apply_Assumption' of term list * term
5.228 - | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
5.229 - (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
5.230 - | Begin_Sequ' | Begin_Trans' of term
5.231 - | Split_And' of term | Split_Or' of term | Split_Intersect' of term
5.232 - | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
5.233 - | End_Sequ' | End_Trans' of Selem.result
5.234 - | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
5.235 - (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
5.236 - | CAScmd' of term
5.237 - | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
5.238 - | Check_Postcond' of Celem.pblID *
5.239 - Selem.result (* returnvalue of script in solve *)
5.240 - | Check_elementwise' of (*special case:*)
5.241 - term * (* (1) the current formula: [x=1,x=...] *)
5.242 - string * (* (2) the pred from Check_elementwise *)
5.243 - Selem.result (* (3) composed from (1) and (2): {x. pred} *)
5.244 - | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
5.245 + datatype T = datatype Tactic_Def.T
5.246
5.247 - | Derive' of Rule.rls
5.248 - | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
5.249 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
5.250 - | End_Detail' of Selem.result
5.251 -
5.252 - | Empty_Tac_
5.253 - | Free_Solve'
5.254 -
5.255 - | Init_Proof' of Rule.cterm' list * Celem.spec
5.256 - | Model_Problem' of Celem.pblID *
5.257 - Model.itm list * (* the 'untouched' pbl *)
5.258 - Model.itm list (* the casually completed met *)
5.259 - | Or_to_List' of term * term
5.260 - | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
5.261 - | Refine_Tacitly' of
5.262 - Celem.pblID * (* input*)
5.263 - Celem.pblID * (* the refined from applicable_in *)
5.264 - Rule.domID * (* from new pbt?! filled in specify *)
5.265 - Celem.metID * (* from new pbt?! filled in specify *)
5.266 - Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
5.267 - | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
5.268 - | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
5.269 - | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
5.270 - | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
5.271 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
5.272 -
5.273 - | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
5.274 - | Specify_Problem' of Celem.pblID *
5.275 - (bool * (* matches *)
5.276 - (Model.itm list * (* ppc *)
5.277 - (bool * term) list)) (* preconditions *)
5.278 - | Specify_Theory' of Rule.domID
5.279 - | Subproblem' of
5.280 - Celem.spec *
5.281 - (Model.ori list) * (* filled in associate Subproblem' *)
5.282 - term * (* filled -"-, headline of calc-head *)
5.283 - Selem.fmz_ *
5.284 - Proof.context * (* DEPRECATED shifted into loc for all ppobj *)
5.285 - term (* Subproblem (thyID, pbl) OR cascmd *)
5.286 - | Substitute' of
5.287 - Rule.rew_ord_ * (* for re-calculation *)
5.288 - Rule.rls * (* for re-calculation *)
5.289 - Selem.subte * (* the 'substitution': terms of type bool *)
5.290 - term * (* to be substituted into *)
5.291 - term (* resulting from the substitution *)
5.292 - | Tac_ of theory * string * string * string
5.293 - | Take' of term | Take_Inst' of term
5.294 -
5.295 -fun string_of ma = case ma of
5.296 - Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
5.297 - | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
5.298 - | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
5.299 - strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
5.300 - | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
5.301 - | Add_Given' _ => "Add_Given' "(*^cterm'*)
5.302 - | Del_Given' _ => "Del_Given' "(*^cterm'*)
5.303 - | Add_Find' _ => "Add_Find' "(*^cterm'*)
5.304 - | Del_Find' _ => "Del_Find' "(*^cterm'*)
5.305 - | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
5.306 - | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
5.307 -
5.308 - | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
5.309 - | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
5.310 - spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
5.311 - | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
5.312 - Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
5.313 -
5.314 - | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
5.315 - | Check_Postcond' (pblID, (scval, asm)) => "Check_Postcond' " ^
5.316 - (spair2str (strs2str pblID, spair2str (Rule.term2str scval, Rule.terms2str asm)))
5.317 -
5.318 - | Free_Solve' => "Free_Solve'"
5.319 -
5.320 - | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
5.321 - | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
5.322 - | Rewrite_Asm' _(*thm'*) => "Rewrite_Asm' "(*^(spair2str thm')*)
5.323 - | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
5.324 - | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
5.325 - "," ^ Rule.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
5.326 - | End_Detail' _ => "End_Detail' xxx"
5.327 - | Detail_Set' _ => "Detail_Set' xxx"
5.328 - | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
5.329 -
5.330 - | Derive' rls => "Derive' " ^ Rule.id_rls rls
5.331 - | Calculate' _ => "Calculate' "
5.332 - | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
5.333 - | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*)
5.334 -
5.335 - | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
5.336 - | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*)
5.337 - | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
5.338 - "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
5.339 - | End_Subproblem' _ => "End_Subproblem'"
5.340 - | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
5.341 -
5.342 - | Empty_Tac_ => "Empty_Tac_"
5.343 - | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
5.344 - | _ => "string_of not impl. for arg";
5.345 +val string_of = Tactic_Def.string_of
5.346
5.347 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
5.348 | input_from_T (Model_Problem' (_, _, _)) = Model_Problem