1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 01 10:24:13 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 01 12:42:39 2020 +0200
1.3 @@ -9,15 +9,105 @@
1.4 *)
1.5 signature TACTIC =
1.6 sig
1.7 - datatype T = datatype Tactic_Def.T
1.8 + datatype T =
1.9 + Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
1.10 + | Add_Relation' of Rule.cterm' * Model.itm list
1.11 + | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
1.12 +
1.13 + | Begin_Sequ' | Begin_Trans' of term
1.14 + | Split_And' of term | Split_Or' of term | Split_Intersect' of term
1.15 + | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
1.16 + | End_Sequ' | End_Trans' of Selem.result
1.17 + | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.18 +
1.19 + | CAScmd' of term
1.20 + | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
1.21 + | Check_Postcond' of Celem.pblID * term
1.22 + | Check_elementwise' of term * Rule.cterm' * Selem.result
1.23 + | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.24 +
1.25 + | Derive' of Rule.rls
1.26 + | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.27 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
1.28 + | End_Detail' of Selem.result
1.29 +
1.30 + | Empty_Tac_
1.31 + | Free_Solve'
1.32 +
1.33 + | Init_Proof' of Rule.cterm' list * Celem.spec
1.34 + | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
1.35 + | Or_to_List' of term * term
1.36 + | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.37 + | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
1.38 +
1.39 + | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
1.40 + | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.41 + | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.42 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
1.43 +
1.44 + | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.45 + | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
1.46 + | Specify_Theory' of Rule.domID
1.47 + | Subproblem' of
1.48 + Celem.spec * Model.ori list *
1.49 + term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
1.50 + Selem.fmz_ * (* either input to root-probl. or derived from prog. in ??? *)
1.51 + (*Istate.T * ? *)
1.52 + Proof.context * (* derived from prog. in ??? *)
1.53 + term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
1.54 + | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
1.55 + | Tac_ of theory * string * string * string
1.56 + | Take' of term
1.57 val string_of: T -> string
1.58
1.59 - datatype input = datatype Tactic_Def.input
1.60 - val tac2str : input -> string
1.61 + datatype input =
1.62 + Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
1.63 + | Apply_Assumption of Rule.cterm' list
1.64 + | Apply_Method of Celem.metID
1.65 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.66 + | Begin_Sequ | Begin_Trans
1.67 + | Split_And | Split_Or | Split_Intersect
1.68 + | Conclude_And | Conclude_Or | Collect_Trues
1.69 + | End_Sequ | End_Trans
1.70 + | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
1.71 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.72 + | CAScmd of Rule.cterm'
1.73 + | Calculate of string
1.74 + | Check_Postcond of Celem.pblID
1.75 + | Check_elementwise of Rule.cterm'
1.76 + | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
1.77 +
1.78 + | Derive of Rule.rls'
1.79 + | Detail_Set of Rule.rls'
1.80 + | Detail_Set_Inst of Selem.subs * Rule.rls'
1.81 + | End_Detail
1.82 +
1.83 + | Empty_Tac
1.84 + | Free_Solve
1.85 +
1.86 + | Init_Proof of Rule.cterm' list * Celem.spec
1.87 + | Model_Problem
1.88 + | Or_to_List
1.89 + | Refine_Problem of Celem.pblID
1.90 + | Refine_Tacitly of Celem.pblID
1.91 +
1.92 + | Rewrite of Celem.thm''
1.93 + | Rewrite_Inst of Selem.subs * Celem.thm''
1.94 + | Rewrite_Set of Rule.rls'
1.95 + | Rewrite_Set_Inst of Selem.subs * Rule.rls'
1.96 +
1.97 + | Specify_Method of Celem.metID
1.98 + | Specify_Problem of Celem.pblID
1.99 + | Specify_Theory of Rule.domID
1.100 + | Subproblem of Rule.domID * Celem.pblID
1.101 +
1.102 + | Substitute of Selem.sube
1.103 + | Tac of string
1.104 + | Take of Rule.cterm' | Take_Inst of Rule.cterm'
1.105 + val input_to_string : input -> string
1.106 val tac2IDstr : input -> string
1.107 val is_empty : input -> bool
1.108
1.109 -(*//-------------------------------------------------------------- only AFTER ctree.sml required *)
1.110 val eq_tac : input * input -> bool
1.111 val is_rewtac : input -> bool
1.112 val is_rewset : input -> bool
1.113 @@ -45,11 +135,162 @@
1.114 struct
1.115 (**)
1.116
1.117 -datatype input = datatype Tactic_Def.input
1.118 +(* tactics for user at front-end.
1.119 + input propagates the construction of the calc-tree;
1.120 + there are
1.121 + (a) 'specsteps' for the specify-phase, and others for the solve-phase
1.122 + (b) those of the solve-phase are 'initac's and others;
1.123 + initacs start with a formula different from the preceding formula.
1.124 + see 'type tac_' for the internal representation of tactics
1.125 +*)
1.126 +datatype input =
1.127 + Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
1.128 + | Apply_Assumption of Rule.cterm' list
1.129 + | Apply_Method of Celem.metID
1.130 + (* creates an "istate" in PblObj.env; in case of "implicit_take"
1.131 + creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
1.132 + a "SOME istate" at fst of "loc".
1.133 + As each step (in the solve-phase) has a resulting formula (at the front-end)
1.134 + Apply_Method also does the 1st step in the script (an "initac") if there is no "implicit_take" *)
1.135 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.136 + | Begin_Sequ | Begin_Trans
1.137 + | Split_And | Split_Or | Split_Intersect
1.138 + | Conclude_And | Conclude_Or | Collect_Trues
1.139 + | End_Sequ | End_Trans
1.140 + | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
1.141 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.142 + | CAScmd of Rule.cterm'
1.143 + | Calculate of string
1.144 + | Check_Postcond of Celem.pblID
1.145 + | Check_elementwise of Rule.cterm'
1.146 + | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
1.147
1.148 -val tac2str = Tactic_Def.tac2str
1.149 -val tac2IDstr = Tactic_Def.tac2IDstr
1.150 -val is_empty = Tactic_Def.is_empty
1.151 + | Derive of Rule.rls' (* WN0509 drop *)
1.152 + | Detail_Set of Rule.rls' (* WN0509 drop *)
1.153 + | Detail_Set_Inst of Selem.subs * Rule.rls' (* WN0509 drop *)
1.154 + | End_Detail (* WN0509 drop *)
1.155 +
1.156 + | Empty_Tac
1.157 + | Free_Solve
1.158 +
1.159 + | Init_Proof of Rule.cterm' list * Celem.spec
1.160 + | Model_Problem
1.161 + | Or_to_List
1.162 + | Refine_Problem of Celem.pblID
1.163 + | Refine_Tacitly of Celem.pblID
1.164 +
1.165 + (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
1.166 + because there all the thms are present with both (thmID, thm)
1.167 + (where user-views can show both or only one of (thmID, thm)),
1.168 + and thm is created from ThmID by assoc_thm'' when entering isabisac *)
1.169 + | Rewrite of Celem.thm''
1.170 + | Rewrite_Inst of Selem.subs * Celem.thm''
1.171 + | Rewrite_Set of Rule.rls'
1.172 + | Rewrite_Set_Inst of Selem.subs * Rule.rls'
1.173 +
1.174 + | Specify_Method of Celem.metID
1.175 + | Specify_Problem of Celem.pblID
1.176 + | Specify_Theory of Rule.domID
1.177 + | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
1.178 +
1.179 + | Substitute of Selem.sube
1.180 + | Tac of string (* WN0509 drop *)
1.181 + | Take of Rule.cterm' | Take_Inst of Rule.cterm'
1.182 +
1.183 +fun input_to_string ma = case ma of
1.184 + Init_Proof (ppc, spec) =>
1.185 + "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec))
1.186 + | Model_Problem => "Model_Problem "
1.187 + | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
1.188 + | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
1.189 + | Add_Given cterm' => "Add_Given " ^ cterm'
1.190 + | Del_Given cterm' => "Del_Given " ^ cterm'
1.191 + | Add_Find cterm' => "Add_Find " ^ cterm'
1.192 + | Del_Find cterm' => "Del_Find " ^ cterm'
1.193 + | Add_Relation cterm' => "Add_Relation " ^ cterm'
1.194 + | Del_Relation cterm' => "Del_Relation " ^ cterm'
1.195 +
1.196 + | Specify_Theory domID => "Specify_Theory " ^ quote domID
1.197 + | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
1.198 + | Specify_Method metID => "Specify_Method " ^ strs2str metID
1.199 + | Apply_Method metID => "Apply_Method " ^ strs2str metID
1.200 + | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
1.201 + | Free_Solve => "Free_Solve"
1.202 +
1.203 + | Rewrite_Inst (subs, (id, thm)) =>
1.204 + "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str)))
1.205 + | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
1.206 + | Rewrite_Set_Inst (subs, rls) =>
1.207 + "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
1.208 + | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
1.209 + | Detail_Set rls => "Detail_Set " ^ quote rls
1.210 + | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
1.211 + | End_Detail => "End_Detail"
1.212 + | Derive rls' => "Derive " ^ rls'
1.213 + | Calculate op_ => "Calculate " ^ op_
1.214 + | Substitute sube => "Substitute " ^ Selem.sube2str sube
1.215 + | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
1.216 +
1.217 + | Take cterm' => "Take " ^ quote cterm'
1.218 + | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
1.219 + | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
1.220 + | End_Subproblem => "End_Subproblem"
1.221 + | CAScmd cterm' => "CAScmd " ^ quote cterm'
1.222 +
1.223 + | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
1.224 + | Or_to_List => "Or_to_List "
1.225 + | Collect_Trues => "Collect_Trues"
1.226 +
1.227 + | Empty_Tac => "Empty_Tac"
1.228 + | Tac string => "Tac " ^ string
1.229 + | End_Proof' => "input End_Proof'"
1.230 + | _ => "input_to_string not impl. for ?!";
1.231 +
1.232 +fun tac2IDstr ma = case ma of
1.233 + Model_Problem => "Model_Problem"
1.234 + | Refine_Tacitly _ => "Refine_Tacitly"
1.235 + | Refine_Problem _ => "Refine_Problem"
1.236 + | Add_Given _ => "Add_Given"
1.237 + | Del_Given _ => "Del_Given"
1.238 + | Add_Find _ => "Add_Find"
1.239 + | Del_Find _ => "Del_Find"
1.240 + | Add_Relation _ => "Add_Relation"
1.241 + | Del_Relation _ => "Del_Relation"
1.242 +
1.243 + | Specify_Theory _ => "Specify_Theory"
1.244 + | Specify_Problem _ => "Specify_Problem"
1.245 + | Specify_Method _ => "Specify_Method"
1.246 + | Apply_Method _ => "Apply_Method"
1.247 + | Check_Postcond _ => "Check_Postcond"
1.248 + | Free_Solve => "Free_Solve"
1.249 +
1.250 + | Rewrite_Inst _ => "Rewrite_Inst"
1.251 + | Rewrite _ => "Rewrite"
1.252 + | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
1.253 + | Rewrite_Set _ => "Rewrite_Set"
1.254 + | Detail_Set _ => "Detail_Set"
1.255 + | Detail_Set_Inst _ => "Detail_Set_Inst"
1.256 + | Derive _ => "Derive "
1.257 + | Calculate _ => "Calculate "
1.258 + | Substitute _ => "Substitute"
1.259 + | Apply_Assumption _ => "Apply_Assumption"
1.260 +
1.261 + | Take _ => "Take"
1.262 + | Take_Inst _ => "Take_Inst"
1.263 + | Subproblem _ => "Subproblem"
1.264 + | End_Subproblem => "End_Subproblem"
1.265 + | CAScmd _ => "CAScmd"
1.266 +
1.267 + | Check_elementwise _ => "Check_elementwise"
1.268 + | Or_to_List => "Or_to_List "
1.269 + | Collect_Trues => "Collect_Trues"
1.270 +
1.271 + | Empty_Tac => "Empty_Tac"
1.272 + | Tac _ => "Tac "
1.273 + | End_Proof' => "End_Proof'"
1.274 + | _ => "input_to_string not impl. for ?!";
1.275 +
1.276 +fun is_empty input = case input of Empty_Tac => true | _ => false
1.277
1.278 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
1.279 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
1.280 @@ -68,7 +309,7 @@
1.281
1.282 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
1.283 | rls_of (Rewrite_Set rls) = rls
1.284 - | rls_of input = error ("rls_of: called with input \"" ^ Tactic_Def.tac2IDstr input ^ "\"");
1.285 + | rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
1.286
1.287 fun rule2tac thy _ (Rule.Num_Calc (opID, _)) = Calculate (assoc_calc thy opID)
1.288 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
1.289 @@ -80,9 +321,139 @@
1.290 | rule2tac _ _ rule =
1.291 error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
1.292
1.293 - datatype T = datatype Tactic_Def.T
1.294 +(* tactics for for internal use, compare "input" for user at the front-end.
1.295 + tac_ contains results from check in 'fun applicable_in'.
1.296 + This is useful for costly results, e.g. from rewriting;
1.297 + however, these results might be changed by Scripts like
1.298 + " eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
1.299 + " eq = (Rewrite_Set equival_trans False) eq;" ^
1.300 + TODO.WN120106 ANALOGOUSLY TO Substitute':
1.301 + So tac_ contains the term t the result was calculated from
1.302 + in order to compare t with t' possibly changed by "Expr "
1.303 + and re-calculate result if t<>t'
1.304 + TODO.WN161219: replace *every* cterm' by term
1.305 +*)
1.306 + datatype T =
1.307 + Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
1.308 + | Add_Relation' of Rule.cterm' * Model.itm list
1.309 + | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
1.310 + * tactic Apply_Method metID
1.311 + * formula term *)
1.312 + Celem.metID * (* key for KEStore *)
1.313 + term option * (* the first formula of Calc.T. TODO: rm option *)
1.314 + Istate_Def.T * (* for the newly started program *)
1.315 + Proof.context (* for the newly started program *)
1.316 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.317 + | Begin_Sequ' | Begin_Trans' of term
1.318 + | Split_And' of term | Split_Or' of term | Split_Intersect' of term
1.319 + | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
1.320 + | End_Sequ' | End_Trans' of Selem.result
1.321 + | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.322 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.323 + | CAScmd' of term
1.324 + | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
1.325 + | Check_Postcond' of Celem.pblID *
1.326 + term (* returnvalue of program in solve *)
1.327 + | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
1.328 + term * (* (1) the current formula: [x=1,x=...] *)
1.329 + string * (* (2) the pred from Check_elementwise *)
1.330 + Selem.result (* (3) composed from (1) and (2): {x. pred} *)
1.331 + | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.332
1.333 -val string_of = Tactic_Def.string_of
1.334 + | Derive' of Rule.rls
1.335 + | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.336 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
1.337 + | End_Detail' of Selem.result
1.338 +
1.339 + | Empty_Tac_
1.340 + | Free_Solve'
1.341 +
1.342 + | Init_Proof' of Rule.cterm' list * Celem.spec
1.343 + | Model_Problem' of (* first step in specifying *)
1.344 + Celem.pblID * (* key into KEStore *)
1.345 + Model.itm list * (* the 'untouched' pbl *)
1.346 + Model.itm list (* the casually completed met *)
1.347 + | Or_to_List' of term * term
1.348 + | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.349 + | Refine_Tacitly' of
1.350 + Celem.pblID * (* input *)
1.351 + Celem.pblID * (* the refined from applicable_in *)
1.352 + Rule.domID * (* from new pbt?! filled in specify *)
1.353 + Celem.metID * (* from new pbt?! filled in specify *)
1.354 + Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.355 + | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
1.356 + | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.357 + | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.358 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
1.359 +
1.360 + | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.361 + | Specify_Problem' of Celem.pblID *
1.362 + (bool * (* matches *)
1.363 + (Model.itm list * (* ppc *)
1.364 + (bool * term) list)) (* preconditions marked true/false *)
1.365 + | Specify_Theory' of Rule.domID
1.366 + | Subproblem' of
1.367 + Celem.spec *
1.368 + (Model.ori list) * (* filled in associate Subproblem' *)
1.369 + term * (* filled -"-, headline of calc-head *)
1.370 + Selem.fmz_ * (* string list from arguments *)
1.371 + Proof.context * (* for specify-phase *)
1.372 + term (* Subproblem (thyID, pbl) OR cascmd *)
1.373 + | Substitute' of
1.374 + Rule.rew_ord_ * (* for re-calculation *)
1.375 + Rule.rls * (* for re-calculation *)
1.376 + Selem.subte * (* the 'substitution': terms of type bool *)
1.377 + term * (* to be substituted into *)
1.378 + term (* resulting from the substitution *)
1.379 + | Tac_ of theory * string * string * string
1.380 + | Take' of term
1.381 +
1.382 +fun string_of ma = case ma of
1.383 + Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
1.384 + | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
1.385 + | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
1.386 + strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
1.387 + | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
1.388 + | Add_Given' _ => "Add_Given' "(*^cterm'*)
1.389 + | Del_Given' _ => "Del_Given' "(*^cterm'*)
1.390 + | Add_Find' _ => "Add_Find' "(*^cterm'*)
1.391 + | Del_Find' _ => "Del_Find' "(*^cterm'*)
1.392 + | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
1.393 + | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
1.394 +
1.395 + | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
1.396 + | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
1.397 + spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
1.398 + | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
1.399 + Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
1.400 +
1.401 + | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
1.402 + | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
1.403 + (spair2str (strs2str pblID, Rule.term2str scval))
1.404 +
1.405 + | Free_Solve' => "Free_Solve'"
1.406 +
1.407 + | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
1.408 + | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
1.409 + | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
1.410 + | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
1.411 + "," ^ Rule.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
1.412 + | End_Detail' _ => "End_Detail' xxx"
1.413 + | Detail_Set' _ => "Detail_Set' xxx"
1.414 + | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
1.415 +
1.416 + | Derive' rls => "Derive' " ^ Rule.id_rls rls
1.417 + | Calculate' _ => "Calculate' "
1.418 + | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
1.419 +
1.420 + | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
1.421 + | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
1.422 + "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
1.423 + | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
1.424 +
1.425 + | Empty_Tac_ => "Empty_Tac_"
1.426 + | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
1.427 + | _ => "string_of not impl. for arg";
1.428
1.429 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
1.430 | input_from_T (Model_Problem' (_, _, _)) = Model_Problem
1.431 @@ -116,7 +487,7 @@
1.432 | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
1.433 | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
1.434 | input_from_T Empty_Tac_ = Empty_Tac
1.435 - | input_from_T m = raise ERROR (": not impl. for "^(Tactic_Def.string_of m));
1.436 + | input_from_T m = raise ERROR (": not impl. for "^(string_of m));
1.437
1.438 fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
1.439 | res (Rewrite' (_, _, _, _, _, _, res)) = res
1.440 @@ -128,7 +499,7 @@
1.441 | res (Take' t) = (t, [])
1.442 | res (Substitute' (_, _, _, _, t)) = (t, [])
1.443 | res (Or_to_List' (_, t)) = (t, [])
1.444 - | res m = raise ERROR ("result: not impl.for " ^ Tactic_Def.string_of m)
1.445 + | res m = raise ERROR ("result: not impl.for " ^ string_of m)
1.446
1.447 (*fun result m = (fst o res) m; TODO*)
1.448 fun result tac = (fst o res) tac;