1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Tue Apr 21 12:26:08 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Tue Apr 21 15:42:50 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 Celem.metID * term option * Istate_Def.T * Proof.context
1.8 + | Apply_Method' of Spec.metID * 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 Celem.pblID * term
1.17 + | Check_Postcond' of Spec.pblID * 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 * Celem.spec
1.26 - | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
1.27 + | Init_Proof' of TermC.as_string list * Spec.spec
1.28 + | Model_Problem' of Spec.pblID * Model.itm list * Model.itm list
1.29 | Or_to_List' of term * term
1.30 - | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.31 - | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.id * Celem.metID * Model.itm list
1.32 + | Refine_Problem' of Spec.pblID * (Model.itm list * (bool * term) list)
1.33 + | Refine_Tacitly' of Spec.pblID * Spec.pblID * ThyC.id * Spec.metID * 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 Celem.metID * Model.ori list * Model.itm list
1.41 - | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
1.42 + | Specify_Method' of Spec.metID * Model.ori list * Model.itm list
1.43 + | Specify_Problem' of Spec.pblID * (bool * (Model.itm list * (bool * term) list))
1.44 | Specify_Theory' of ThyC.id
1.45 | Subproblem' of
1.46 - Celem.spec * Model.ori list *
1.47 + Spec.spec * 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 Celem.metID
1.56 + | Apply_Method of Spec.metID
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 Celem.pblID
1.65 + | Check_Postcond of Spec.pblID
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 * Celem.spec
1.74 + | Init_Proof of TermC.as_string list * Spec.spec
1.75 | Model_Problem
1.76 | Or_to_List
1.77 - | Refine_Problem of Celem.pblID
1.78 - | Refine_Tacitly of Celem.pblID
1.79 + | Refine_Problem of Spec.pblID
1.80 + | Refine_Tacitly of Spec.pblID
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 Celem.metID
1.88 - | Specify_Problem of Celem.pblID
1.89 + | Specify_Method of Spec.metID
1.90 + | Specify_Problem of Spec.pblID
1.91 | Specify_Theory of ThyC.id
1.92 - | Subproblem of ThyC.id * Celem.pblID
1.93 + | Subproblem of ThyC.id * Spec.pblID
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 Celem.metID
1.102 + | Apply_Method of Spec.metID
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 Celem.pblID
1.111 + | Check_Postcond of Spec.pblID
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 * Celem.spec
1.120 + | Init_Proof of TermC.as_string list * Spec.spec
1.121 | Model_Problem
1.122 | Or_to_List
1.123 - | Refine_Problem of Celem.pblID
1.124 - | Refine_Tacitly of Celem.pblID
1.125 + | Refine_Problem of Spec.pblID
1.126 + | Refine_Tacitly of Spec.pblID
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 Celem.metID
1.135 - | Specify_Problem of Celem.pblID
1.136 + | Specify_Method of Spec.metID
1.137 + | Specify_Problem of Spec.pblID
1.138 | Specify_Theory of ThyC.id
1.139 - | Subproblem of ThyC.id * Celem.pblID (* WN0509 drop *)
1.140 + | Subproblem of ThyC.id * Spec.pblID (* WN0509 drop *)
1.141
1.142 | Substitute of Selem.sube
1.143 | Tac of string (* WN0509 drop *)
1.144 @@ -199,7 +199,7 @@
1.145
1.146 fun input_to_string ma = case ma of
1.147 Init_Proof (ppc, spec) =>
1.148 - "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec))
1.149 + "Init_Proof "^(pair2str (strs2str ppc, Spec.spec2str spec))
1.150 | Model_Problem => "Model_Problem "
1.151 | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
1.152 | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
1.153 @@ -339,7 +339,7 @@
1.154 | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
1.155 * tactic Apply_Method metID
1.156 * formula term *)
1.157 - Celem.metID * (* key for Know_Store *)
1.158 + Spec.metID * (* key for Know_Store *)
1.159 term option * (* the first formula of Calc.T. TODO: rm option *)
1.160 Istate_Def.T * (* for the newly started program *)
1.161 Proof.context (* for the newly started program *)
1.162 @@ -352,7 +352,7 @@
1.163 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.164 | CAScmd' of term
1.165 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.166 - | Check_Postcond' of Celem.pblID *
1.167 + | Check_Postcond' of Spec.pblID *
1.168 term (* returnvalue of program in solve *)
1.169 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
1.170 term * (* (1) the current formula: [x=1,x=...] *)
1.171 @@ -368,32 +368,32 @@
1.172 | Empty_Tac_
1.173 | Free_Solve'
1.174
1.175 - | Init_Proof' of TermC.as_string list * Celem.spec
1.176 + | Init_Proof' of TermC.as_string list * Spec.spec
1.177 | Model_Problem' of (* first step in specifying *)
1.178 - Celem.pblID * (* key into Know_Store *)
1.179 + Spec.pblID * (* key into Know_Store *)
1.180 Model.itm list * (* the 'untouched' pbl *)
1.181 Model.itm list (* the casually completed met *)
1.182 | Or_to_List' of term * term
1.183 - | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.184 + | Refine_Problem' of Spec.pblID * (Model.itm list * (bool * term) list)
1.185 | Refine_Tacitly' of
1.186 - Celem.pblID * (* input *)
1.187 - Celem.pblID * (* the refined from applicable_in *)
1.188 + Spec.pblID * (* input *)
1.189 + Spec.pblID * (* the refined from applicable_in *)
1.190 ThyC.id * (* from new pbt?! filled in specify *)
1.191 - Celem.metID * (* from new pbt?! filled in specify *)
1.192 + Spec.metID * (* from new pbt?! filled in specify *)
1.193 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.194 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
1.195 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
1.196 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.197 | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
1.198
1.199 - | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.200 - | Specify_Problem' of Celem.pblID *
1.201 + | Specify_Method' of Spec.metID * Model.ori list * Model.itm list
1.202 + | Specify_Problem' of Spec.pblID *
1.203 (bool * (* matches *)
1.204 (Model.itm list * (* ppc *)
1.205 (bool * term) list)) (* preconditions marked true/false *)
1.206 | Specify_Theory' of ThyC.id
1.207 | Subproblem' of
1.208 - Celem.spec *
1.209 + Spec.spec *
1.210 (Model.ori list) * (* filled in associate Subproblem' *)
1.211 term * (* filled -"-, headline of calc-head *)
1.212 Selem.fmz_ * (* string list from arguments *)
1.213 @@ -409,7 +409,7 @@
1.214 | Take' of term
1.215
1.216 fun string_of ma = case ma of
1.217 - Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
1.218 + Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.spec2str spec)
1.219 | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
1.220 | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
1.221 strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
1.222 @@ -425,7 +425,7 @@
1.223 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
1.224 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
1.225 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
1.226 - Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
1.227 + Spec.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
1.228
1.229 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
1.230 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^