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