1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 22 11:23:30 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 22 14:36:27 2020 +0200
1.3 @@ -12,7 +12,7 @@
1.4 datatype T =
1.5 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
1.6 | Add_Relation' of TermC.as_string * Model.itm list
1.7 - | Apply_Method' of Spec.metID * term option * Istate_Def.T * Proof.context
1.8 + | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
1.9
1.10 | Begin_Sequ' | Begin_Trans' of term
1.11 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
1.12 @@ -22,7 +22,7 @@
1.13
1.14 | CAScmd' of term
1.15 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.16 - | Check_Postcond' of Spec.pblID * term
1.17 + | Check_Postcond' of Problem.id * term
1.18 | Check_elementwise' of term * TermC.as_string * Selem.result
1.19 | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.20
1.21 @@ -34,22 +34,22 @@
1.22 | Empty_Tac_
1.23 | Free_Solve'
1.24
1.25 - | Init_Proof' of TermC.as_string list * Spec.spec
1.26 - | Model_Problem' of Spec.pblID * Model.itm list * Model.itm list
1.27 + | Init_Proof' of TermC.as_string list * Spec.T
1.28 + | Model_Problem' of Problem.id * Model.itm list * Model.itm list
1.29 | Or_to_List' of term * term
1.30 - | Refine_Problem' of Spec.pblID * (Model.itm list * (bool * term) list)
1.31 - | Refine_Tacitly' of Spec.pblID * Spec.pblID * ThyC.id * Spec.metID * Model.itm list
1.32 + | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
1.33 + | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
1.34
1.35 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
1.36 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
1.37 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.38 | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
1.39
1.40 - | Specify_Method' of Spec.metID * Model.ori list * Model.itm list
1.41 - | Specify_Problem' of Spec.pblID * (bool * (Model.itm list * (bool * term) list))
1.42 + | Specify_Method' of Method.id * Model.ori list * Model.itm list
1.43 + | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
1.44 | Specify_Theory' of ThyC.id
1.45 | Subproblem' of
1.46 - Spec.spec * Model.ori list *
1.47 + Spec.T * Model.ori list *
1.48 term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
1.49 Selem.fmz_ * (* either input to root-probl. or derived from prog. in ??? *)
1.50 (*Istate.T * ? *)
1.51 @@ -63,7 +63,7 @@
1.52 datatype input =
1.53 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
1.54 | Apply_Assumption of TermC.as_string list
1.55 - | Apply_Method of Spec.metID
1.56 + | Apply_Method of Method.id
1.57 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.58 | Begin_Sequ | Begin_Trans
1.59 | Split_And | Split_Or | Split_Intersect
1.60 @@ -73,7 +73,7 @@
1.61 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.62 | CAScmd of TermC.as_string
1.63 | Calculate of string
1.64 - | Check_Postcond of Spec.pblID
1.65 + | Check_Postcond of Problem.id
1.66 | Check_elementwise of TermC.as_string
1.67 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
1.68
1.69 @@ -85,21 +85,21 @@
1.70 | Empty_Tac
1.71 | Free_Solve
1.72
1.73 - | Init_Proof of TermC.as_string list * Spec.spec
1.74 + | Init_Proof of TermC.as_string list * Spec.T
1.75 | Model_Problem
1.76 | Or_to_List
1.77 - | Refine_Problem of Spec.pblID
1.78 - | Refine_Tacitly of Spec.pblID
1.79 + | Refine_Problem of Problem.id
1.80 + | Refine_Tacitly of Problem.id
1.81
1.82 | Rewrite of ThmC.T
1.83 | Rewrite_Inst of Selem.subs * ThmC.T
1.84 | Rewrite_Set of Rule_Set.id
1.85 | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
1.86
1.87 - | Specify_Method of Spec.metID
1.88 - | Specify_Problem of Spec.pblID
1.89 + | Specify_Method of Method.id
1.90 + | Specify_Problem of Problem.id
1.91 | Specify_Theory of ThyC.id
1.92 - | Subproblem of ThyC.id * Spec.pblID
1.93 + | Subproblem of ThyC.id * Problem.id
1.94
1.95 | Substitute of Selem.sube
1.96 | Tac of string
1.97 @@ -146,7 +146,7 @@
1.98 datatype input =
1.99 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
1.100 | Apply_Assumption of TermC.as_string list
1.101 - | Apply_Method of Spec.metID
1.102 + | Apply_Method of Method.id
1.103 (* creates an "istate" in PblObj.env; in case of "implicit_take"
1.104 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
1.105 a "SOME istate" at fst of "loc".
1.106 @@ -161,7 +161,7 @@
1.107 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.108 | CAScmd of TermC.as_string
1.109 | Calculate of string
1.110 - | Check_Postcond of Spec.pblID
1.111 + | Check_Postcond of Problem.id
1.112 | Check_elementwise of TermC.as_string
1.113 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
1.114
1.115 @@ -173,11 +173,11 @@
1.116 | Empty_Tac
1.117 | Free_Solve
1.118
1.119 - | Init_Proof of TermC.as_string list * Spec.spec
1.120 + | Init_Proof of TermC.as_string list * Spec.T
1.121 | Model_Problem
1.122 | Or_to_List
1.123 - | Refine_Problem of Spec.pblID
1.124 - | Refine_Tacitly of Spec.pblID
1.125 + | Refine_Problem of Problem.id
1.126 + | Refine_Tacitly of Problem.id
1.127
1.128 (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
1.129 because there all the thms are present with both (thmID, thm)
1.130 @@ -188,10 +188,10 @@
1.131 | Rewrite_Set of Rule_Set.id
1.132 | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
1.133
1.134 - | Specify_Method of Spec.metID
1.135 - | Specify_Problem of Spec.pblID
1.136 + | Specify_Method of Method.id
1.137 + | Specify_Problem of Problem.id
1.138 | Specify_Theory of ThyC.id
1.139 - | Subproblem of ThyC.id * Spec.pblID (* WN0509 drop *)
1.140 + | Subproblem of ThyC.id * Problem.id (* WN0509 drop *)
1.141
1.142 | Substitute of Selem.sube
1.143 | Tac of string (* WN0509 drop *)
1.144 @@ -339,7 +339,7 @@
1.145 | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
1.146 * tactic Apply_Method metID
1.147 * formula term *)
1.148 - Spec.metID * (* key for Know_Store *)
1.149 + Method.id * (* key for Know_Store *)
1.150 term option * (* the first formula of Calc.T. TODO: rm option *)
1.151 Istate_Def.T * (* for the newly started program *)
1.152 Proof.context (* for the newly started program *)
1.153 @@ -352,7 +352,7 @@
1.154 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.155 | CAScmd' of term
1.156 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.157 - | Check_Postcond' of Spec.pblID *
1.158 + | Check_Postcond' of Problem.id *
1.159 term (* returnvalue of program in solve *)
1.160 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
1.161 term * (* (1) the current formula: [x=1,x=...] *)
1.162 @@ -368,32 +368,32 @@
1.163 | Empty_Tac_
1.164 | Free_Solve'
1.165
1.166 - | Init_Proof' of TermC.as_string list * Spec.spec
1.167 + | Init_Proof' of TermC.as_string list * Spec.T
1.168 | Model_Problem' of (* first step in specifying *)
1.169 - Spec.pblID * (* key into Know_Store *)
1.170 + Problem.id * (* key into Know_Store *)
1.171 Model.itm list * (* the 'untouched' pbl *)
1.172 Model.itm list (* the casually completed met *)
1.173 | Or_to_List' of term * term
1.174 - | Refine_Problem' of Spec.pblID * (Model.itm list * (bool * term) list)
1.175 + | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
1.176 | Refine_Tacitly' of
1.177 - Spec.pblID * (* input *)
1.178 - Spec.pblID * (* the refined from applicable_in *)
1.179 + Problem.id * (* input *)
1.180 + Problem.id * (* the refined from applicable_in *)
1.181 ThyC.id * (* from new pbt?! filled in specify *)
1.182 - Spec.metID * (* from new pbt?! filled in specify *)
1.183 + Method.id * (* from new pbt?! filled in specify *)
1.184 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.185 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
1.186 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
1.187 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.188 | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
1.189
1.190 - | Specify_Method' of Spec.metID * Model.ori list * Model.itm list
1.191 - | Specify_Problem' of Spec.pblID *
1.192 + | Specify_Method' of Method.id * Model.ori list * Model.itm list
1.193 + | Specify_Problem' of Problem.id *
1.194 (bool * (* matches *)
1.195 (Model.itm list * (* ppc *)
1.196 (bool * term) list)) (* preconditions marked true/false *)
1.197 | Specify_Theory' of ThyC.id
1.198 | Subproblem' of
1.199 - Spec.spec *
1.200 + Spec.T *
1.201 (Model.ori list) * (* filled in associate Subproblem' *)
1.202 term * (* filled -"-, headline of calc-head *)
1.203 Selem.fmz_ * (* string list from arguments *)
1.204 @@ -425,7 +425,7 @@
1.205 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
1.206 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
1.207 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
1.208 - Spec.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
1.209 + Method.id_to_string pI ^ ", " ^ Model.oris2str oris ^ ", )"
1.210
1.211 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
1.212 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^