1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Fri May 01 17:17:41 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 09:15:39 2020 +0200
1.3 @@ -13,8 +13,8 @@
1.4 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
1.5 | Add_Relation' of TermC.as_string * Model.itm list
1.6 | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
1.7 - | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.8 - | Init_Proof' of TermC.as_string list * Spec.T
1.9 +(*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.10 +(*RM*)| Init_Proof' of TermC.as_string list * Spec.T
1.11 | Model_Problem' of Problem.id * Model.itm list * Model.itm list
1.12 | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
1.13 | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
1.14 @@ -35,13 +35,7 @@
1.15 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
1.16 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.17 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
1.18 - | Subproblem' of
1.19 - Spec.T * Model.ori list *
1.20 - term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
1.21 - Selem.fmz_ * (* either input to root-probl. or derived from prog. in ??? *)
1.22 - (*Istate.T * ? *)
1.23 - Proof.context * (* derived from prog. in ??? *)
1.24 - term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
1.25 + | Subproblem' of Spec.T * Model.ori list * term * Selem.fmz_ * Proof.context * term
1.26 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
1.27 (*RM*)| Tac_ of theory * string * string * string
1.28 | Take' of term
1.29 @@ -133,67 +127,45 @@
1.30
1.31 (** tactics for user at front-end **)
1.32
1.33 -(* tactics for user at front-end.
1.34 - input propagates the construction of the calc-tree;
1.35 - there are
1.36 - (a) 'specsteps' for the specify-phase, and others for the solve-phase
1.37 - (b) those of the solve-phase are 'initac's and others;
1.38 - initacs start with a formula different from the preceding formula.
1.39 - see 'type tac_' for the internal representation of tactics
1.40 -*)
1.41 datatype input =
1.42 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
1.43 - | Apply_Assumption of TermC.as_string list
1.44 | Apply_Method of Method.id
1.45 - (* creates an "istate" in PblObj.env; in case of "implicit_take"
1.46 - creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
1.47 - a "SOME istate" at fst of "loc".
1.48 - As each step (in the solve-phase) has a resulting formula (at the front-end)
1.49 - Apply_Method also does the 1st step in the script (an "initac") if there is no "implicit_take" *)
1.50 - (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.51 - | Begin_Sequ | Begin_Trans
1.52 - | Split_And | Split_Or | Split_Intersect
1.53 - | Conclude_And | Conclude_Or | Collect_Trues
1.54 - | End_Sequ | End_Trans
1.55 - | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
1.56 - (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.57 + | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
1.58 + | Init_Proof of TermC.as_string list * Spec.T
1.59 + | Model_Problem
1.60 + | Refine_Problem of Problem.id
1.61 + | Refine_Tacitly of Problem.id
1.62 + | Specify_Method of Method.id
1.63 + | Specify_Problem of Problem.id
1.64 + | Specify_Theory of ThyC.id
1.65 + (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.66 | CAScmd of TermC.as_string
1.67 | Calculate of string
1.68 | Check_Postcond of Problem.id
1.69 | Check_elementwise of TermC.as_string
1.70 - | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
1.71 -
1.72 - | Derive of Rule_Set.id (* WN0509 drop *)
1.73 - | Detail_Set of Rule_Set.id (* WN0509 drop *)
1.74 - | Detail_Set_Inst of Subst.input * Rule_Set.id (* WN0509 drop *)
1.75 - | End_Detail (* WN0509 drop *)
1.76 -
1.77 +(*RM*)| Derive of Rule_Set.id
1.78 | Empty_Tac
1.79 - | Free_Solve
1.80 -
1.81 - | Init_Proof of TermC.as_string list * Spec.T
1.82 - | Model_Problem
1.83 +(*RM*)| Free_Solve
1.84 +(*RM*)| Apply_Assumption of TermC.as_string list
1.85 | Or_to_List
1.86 - | Refine_Problem of Problem.id
1.87 - | Refine_Tacitly of Problem.id
1.88 -
1.89 - (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
1.90 - because there all the thms are present with both (thmID, thm)
1.91 - (where user-views can show both or only one of (thmID, thm)),
1.92 - and thm is created from ThmID by assoc_thm'' when entering isabisac *)
1.93 | Rewrite of ThmC.T
1.94 | Rewrite_Inst of Subst.input * ThmC.T
1.95 | Rewrite_Set of Rule_Set.id
1.96 | Rewrite_Set_Inst of Subst.input * Rule_Set.id
1.97 -
1.98 - | Specify_Method of Method.id
1.99 - | Specify_Problem of Problem.id
1.100 - | Specify_Theory of ThyC.id
1.101 - | Subproblem of ThyC.id * Problem.id (* WN0509 drop *)
1.102 -
1.103 + | Subproblem of ThyC.id * Problem.id
1.104 | Substitute of Subst.input
1.105 - | Tac of string (* WN0509 drop *)
1.106 - | Take of TermC.as_string | Take_Inst of TermC.as_string
1.107 +(*RM*)| Tac of string
1.108 + | Take of TermC.as_string
1.109 +(*RM*)| Take_Inst of TermC.as_string
1.110 +(*RM*)| Begin_Sequ | Begin_Trans
1.111 +(*RM*)| Split_And | Split_Or | Split_Intersect
1.112 +(*RM*)| Conclude_And | Conclude_Or | Collect_Trues
1.113 +(*RM*)| End_Sequ | End_Trans
1.114 +(*RM*)| End_Ruleset | End_Subproblem | End_Intersect
1.115 +(*RM*)| Detail_Set of Rule_Set.id
1.116 +(*RM*)| Detail_Set_Inst of Subst.input * Rule_Set.id
1.117 +(*RM*)| End_Detail
1.118 + | End_Proof';
1.119
1.120 fun input_to_string ma = case ma of
1.121 Init_Proof (ppc, spec) =>
1.122 @@ -365,92 +337,75 @@
1.123
1.124 (** tactics for internal use **)
1.125
1.126 -(* tactics for for internal use, compare "input" for user at the front-end.
1.127 - tac_ contains results from check in 'fun applicable_in'.
1.128 - This is useful for costly results, e.g. from rewriting;
1.129 - however, these results might be changed by Scripts like
1.130 - " eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
1.131 - " eq = (Rewrite_Set equival_trans False) eq;" ^
1.132 - TODO.WN120106 ANALOGOUSLY TO Substitute':
1.133 - So tac_ contains the term t the result was calculated from
1.134 - in order to compare t with t' possibly changed by "Expr "
1.135 - and re-calculate result if t<>t'
1.136 - TODO.WN161219: replace *every* cterm' by term
1.137 -*)
1.138 datatype T =
1.139 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
1.140 - | Add_Relation' of TermC.as_string * Model.itm list
1.141 - | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
1.142 - * tactic Apply_Method metID
1.143 - * formula term *)
1.144 - Method.id * (* key for Know_Store *)
1.145 - term option * (* the first formula of Calc.T. TODO: rm option *)
1.146 - Istate_Def.T * (* for the newly started program *)
1.147 - Proof.context (* for the newly started program *)
1.148 - (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.149 - | Begin_Sequ' | Begin_Trans' of term
1.150 - | Split_And' of term | Split_Or' of term | Split_Intersect' of term
1.151 - | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
1.152 - | End_Sequ' | End_Trans' of Selem.result
1.153 - | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.154 - (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.155 + | Add_Relation' of TermC.as_string * Model.itm list (* for Step.do_next *)
1.156 + | Apply_Method' of (* last step in specifu-phse, switch to solve-phase *)
1.157 + Method.id * (* id in the Know_Store *)
1.158 + term option * (* first formula in the (sub-)Problem TODO: rm option *)
1.159 + Istate_Def.T * (* for starting the Program *)
1.160 + Proof.context (* for starting the Program *)
1.161 +(*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.162 +(*RM*)| Init_Proof' of TermC.as_string list * Spec.T
1.163 + | Model_Problem' of (* first step in specify-phase *)
1.164 + Problem.id * (* id in the Know_Store *)
1.165 + Model.itm list * (* the model for the Problem *)
1.166 + Model.itm list (* the model for the method *)
1.167 + | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
1.168 + | Refine_Tacitly' of
1.169 + Problem.id * (* the original id in the Know_Store *)
1.170 + Problem.id * (* the id of the refined Problem *)
1.171 + ThyC.id * (* the id of the refined theory *)
1.172 + Method.id * (* the id of the refined Method *)
1.173 + Model.itm list (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
1.174 + | Specify_Method' of Method.id * Model.ori list * Model.itm list
1.175 + | Specify_Problem' of Problem.id *
1.176 + (bool * (* all preconditions evaluate to True *)
1.177 + (Model.itm list * (* the model checked for the input id *)
1.178 + (bool * term) list)) (* individual preconditions marked true/false *)
1.179 + | Specify_Theory' of ThyC.id
1.180 + (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.181 | CAScmd' of term
1.182 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.183 - | Check_Postcond' of Problem.id *
1.184 - term (* returnvalue of program in solve *)
1.185 - | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
1.186 - term * (* (1) the current formula: [x=1,x=...] *)
1.187 - string * (* (2) the pred from Check_elementwise *)
1.188 - Selem.result (* (3) composed from (1) and (2): {x. pred} *)
1.189 - | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.190 -
1.191 - | Derive' of Rule_Set.T
1.192 - | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.193 - | Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
1.194 - | End_Detail' of Selem.result
1.195 -
1.196 + | Check_Postcond' of (* last step in solving a (sub-)Problem *)
1.197 + Problem.id * (* id of the Problem to be checked *)
1.198 + term (* return value of the program *)
1.199 + | Check_elementwise' of(* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
1.200 + term * (* the current formula: [x=1,x=...] *)
1.201 + string * (* the pred from Check_elementwise *)
1.202 + Selem.result (* composed from (1) and (2): {x. pred} *)
1.203 +(*RM*)| Derive' of Rule_Set.T
1.204 | Empty_Tac_
1.205 | Free_Solve'
1.206 -
1.207 - | Init_Proof' of TermC.as_string list * Spec.T
1.208 - | Model_Problem' of (* first step in specifying *)
1.209 - Problem.id * (* key into Know_Store *)
1.210 - Model.itm list * (* the 'untouched' pbl *)
1.211 - Model.itm list (* the casually completed met *)
1.212 +(*RM* )| Apply_Assumption of TermC.as_string list( *RM*)
1.213 | Or_to_List' of term * term
1.214 - | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
1.215 - | Refine_Tacitly' of
1.216 - Problem.id * (* input *)
1.217 - Problem.id * (* the refined from applicable_in *)
1.218 - ThyC.id * (* from new pbt?! filled in specify *)
1.219 - Method.id * (* from new pbt?! filled in specify *)
1.220 - Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.221 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
1.222 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
1.223 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.224 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
1.225 -
1.226 - | Specify_Method' of Method.id * Model.ori list * Model.itm list
1.227 - | Specify_Problem' of Problem.id *
1.228 - (bool * (* matches *)
1.229 - (Model.itm list * (* ppc *)
1.230 - (bool * term) list)) (* preconditions marked true/false *)
1.231 - | Specify_Theory' of ThyC.id
1.232 - | Subproblem' of
1.233 - Spec.T *
1.234 - (Model.ori list) * (* filled in associate Subproblem' *)
1.235 - term * (* filled -"-, headline of calc-head *)
1.236 - Selem.fmz_ * (* string list from arguments *)
1.237 - Proof.context * (* for specify-phase *)
1.238 - term (* Subproblem (thyID, pbl) OR cascmd *)
1.239 - | Substitute' of
1.240 - Rule_Def.rew_ord_ * (* for re-calculation *)
1.241 - Rule_Set.T * (* for re-calculation *)
1.242 - Subst.as_eqs * (* the 'substitution': terms of type bool *)
1.243 - term * (* to be substituted into *)
1.244 - term (* resulting from the substitution *)
1.245 - | Tac_ of theory * string * string * string
1.246 + | Subproblem' of (* switch from solve-phase to specify-phase *)
1.247 + Spec.T * (* specification of the SubProblem *)
1.248 + (Model.ori list) * (* original model, filled in associate Subproblem' *)
1.249 + term * (* headline of calc-head, filled -"- *)
1.250 + Selem.fmz_ * (* string list from arguments of the calling Program*)
1.251 + Proof.context * (* for the specify-phase *)
1.252 + term (* Subproblem (thyID, pbl) OR CAS_Cmd *)
1.253 + | Substitute' of (* substitute variables (TODO: from the context) *)
1.254 + Rule_Def.rew_ord_ *(* for re-calculation *)
1.255 + Rule_Set.T * (* for re-calculation *)
1.256 + Subst.as_eqs * (* the substitution: terms of type bool *)
1.257 + term * (* to be substituted into *)
1.258 + term (* resulting from the substitution *)
1.259 +(*RM*)| Tac_ of theory * string * string * string
1.260 | Take' of term
1.261 +(*RM*)| Begin_Sequ' | Begin_Trans' of term
1.262 +(*RM*)| Split_And' of term | Split_Or' of term | Split_Intersect' of term
1.263 +(*RM*)| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
1.264 +(*RM*)| End_Sequ' | End_Trans' of Selem.result
1.265 +(*RM*)| End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.266 +(*RM*)| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.267 +(*RM*)| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
1.268 +(*RM*)| End_Detail' of Selem.result;
1.269
1.270 fun string_of ma = case ma of
1.271 Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec)