1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Feb 03 15:21:12 2021 +0100
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Feb 03 16:39:44 2021 +0100
1.3 @@ -15,12 +15,12 @@
1.4 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.5 | Model_Problem' of Problem.id * Model_Def.i_model * Model_Def.i_model
1.6 | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)
1.7 - | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model_Def.i_model
1.8 - | Specify_Method' of Method.id * Model_Def.o_model * Model_Def.i_model
1.9 + | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * MethodC.id * Model_Def.i_model
1.10 + | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model
1.11 | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model * Pre_Conds_Def.T))
1.12 | Specify_Theory' of ThyC.id
1.13 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.14 - | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
1.15 + | Apply_Method' of MethodC.id * term option * Istate_Def.T * Proof.context
1.16 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.17 | Check_Postcond' of Problem.id * term
1.18 | Check_elementwise' of term * TermC.as_string * Celem.result
1.19 @@ -49,11 +49,11 @@
1.20 | Model_Problem
1.21 | Refine_Problem of Problem.id
1.22 | Refine_Tacitly of Problem.id
1.23 - | Specify_Method of Method.id
1.24 + | Specify_Method of MethodC.id
1.25 | Specify_Problem of Problem.id
1.26 | Specify_Theory of ThyC.id
1.27 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.28 - | Apply_Method of Method.id
1.29 + | Apply_Method of MethodC.id
1.30 | Calculate of string
1.31 | Check_Postcond of Problem.id
1.32 | Check_elementwise of TermC.as_string
1.33 @@ -114,11 +114,11 @@
1.34 | Model_Problem
1.35 | Refine_Problem of Problem.id
1.36 | Refine_Tacitly of Problem.id
1.37 - | Specify_Method of Method.id
1.38 + | Specify_Method of MethodC.id
1.39 | Specify_Problem of Problem.id
1.40 | Specify_Theory of ThyC.id
1.41 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.42 - | Apply_Method of Method.id
1.43 + | Apply_Method of MethodC.id
1.44 | Calculate of string
1.45 | Check_Postcond of Problem.id
1.46 | Check_elementwise of TermC.as_string
1.47 @@ -307,9 +307,9 @@
1.48 Problem.id * (* the original id in the Know_Store *)
1.49 Problem.id * (* the id of the refined Problem *)
1.50 ThyC.id * (* the id of the refined theory *)
1.51 - Method.id * (* the id of the refined Method *)
1.52 + MethodC.id * (* the id of the refined MethodC *)
1.53 Model_Def.i_model (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
1.54 - | Specify_Method' of Method.id * Model_Def.o_model * Model_Def.i_model
1.55 + | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model
1.56 | Specify_Problem' of Problem.id *
1.57 (bool * (* all preconditions evaluate to True *)
1.58 (Model_Def.i_model * (* the model checked for the input id *)
1.59 @@ -317,7 +317,7 @@
1.60 | Specify_Theory' of ThyC.id
1.61 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.62 | Apply_Method' of (* last step in specifu-phse, switch to solve-phase *)
1.63 - Method.id * (* id in the Know_Store *)
1.64 + MethodC.id * (* id in the Know_Store *)
1.65 term option * (* first formula in the (sub-)Problem TODO: rm option *)
1.66 Istate_Def.T * (* for starting the Program *)
1.67 Proof.context (* for starting the Program *)
1.68 @@ -373,7 +373,7 @@
1.69 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
1.70 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
1.71 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
1.72 - Method.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string oris ^ ", )"
1.73 + MethodC.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string oris ^ ", )"
1.74
1.75 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
1.76 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^