1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Mon May 04 17:08:32 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon May 04 18:47:27 2020 +0200
1.3 @@ -10,14 +10,14 @@
1.4 signature TACTIC =
1.5 sig
1.6 datatype T =
1.7 - Add_Find' of TermC.as_string * Model_Def.itm list | Add_Given' of TermC.as_string * Model_Def.itm list
1.8 - | Add_Relation' of TermC.as_string * Model_Def.itm list
1.9 + Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model
1.10 + | Add_Relation' of TermC.as_string * Model_Def.i_model
1.11 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.12 - | Model_Problem' of Problem.id * Model_Def.itm list * Model_Def.itm list
1.13 - | Refine_Problem' of Problem.id * (Model_Def.itm list * (bool * term) list)
1.14 - | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model_Def.itm list
1.15 - | Specify_Method' of Method.id * Model_Def.ori list * Model_Def.itm list
1.16 - | Specify_Problem' of Problem.id * (bool * (Model_Def.itm list * (bool * term) list))
1.17 + | Model_Problem' of Problem.id * Model_Def.i_model * Model_Def.i_model
1.18 + | Refine_Problem' of Problem.id * (Model_Def.i_model * (bool * term) list)
1.19 + | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model_Def.i_model
1.20 + | Specify_Method' of Method.id * Model_Def.o_model * Model_Def.i_model
1.21 + | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model * (bool * term) list))
1.22 | Specify_Theory' of ThyC.id
1.23 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.24 | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
1.25 @@ -32,7 +32,7 @@
1.26 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
1.27 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
1.28 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
1.29 - | Subproblem' of Spec.T * Model_Def.ori list * term * Celem.fmz_ * Proof.context * term
1.30 + | Subproblem' of Spec.T * Model_Def.o_model * term * Celem.fmz_ * Proof.context * term
1.31 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
1.32 (*RM*)| Tac_ of theory * string * string * string
1.33 | Take' of term
1.34 @@ -295,24 +295,24 @@
1.35 (** tactics for internal use **)
1.36
1.37 datatype T =
1.38 - Add_Find' of TermC.as_string * Model_Def.itm list | Add_Given' of TermC.as_string * Model_Def.itm list
1.39 - | Add_Relation' of TermC.as_string * Model_Def.itm list (* for Step.do_next *)
1.40 + Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model
1.41 + | Add_Relation' of TermC.as_string * Model_Def.i_model (* for Step.do_next *)
1.42 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.43 | Model_Problem' of (* first step in specify-phase *)
1.44 Problem.id * (* id in the Know_Store *)
1.45 - Model_Def.itm list * (* the model for the Problem *)
1.46 - Model_Def.itm list (* the model for the method *)
1.47 - | Refine_Problem' of Problem.id * (Model_Def.itm list * (bool * term) list)
1.48 + Model_Def.i_model * (* the model for the Problem *)
1.49 + Model_Def.i_model (* the model for the method *)
1.50 + | Refine_Problem' of Problem.id * (Model_Def.i_model * (bool * term) list)
1.51 | Refine_Tacitly' of
1.52 Problem.id * (* the original id in the Know_Store *)
1.53 Problem.id * (* the id of the refined Problem *)
1.54 ThyC.id * (* the id of the refined theory *)
1.55 Method.id * (* the id of the refined Method *)
1.56 - Model_Def.itm list (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
1.57 - | Specify_Method' of Method.id * Model_Def.ori list * Model_Def.itm list
1.58 + Model_Def.i_model (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
1.59 + | Specify_Method' of Method.id * Model_Def.o_model * Model_Def.i_model
1.60 | Specify_Problem' of Problem.id *
1.61 (bool * (* all preconditions evaluate to True *)
1.62 - (Model_Def.itm list * (* the model checked for the input id *)
1.63 + (Model_Def.i_model * (* the model checked for the input id *)
1.64 (bool * term) list)) (* individual preconditions marked true/false *)
1.65 | Specify_Theory' of ThyC.id
1.66 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.67 @@ -339,7 +339,7 @@
1.68 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
1.69 | Subproblem' of (* switch from solve-phase to specify-phase *)
1.70 Spec.T * (* specification of the SubProblem *)
1.71 - (Model_Def.ori list) * (* original model, filled in associate Subproblem' *)
1.72 + (Model_Def.o_model) * (* original model, filled in associate Subproblem' *)
1.73 term * (* headline of calc-head, filled -"- *)
1.74 Celem.fmz_ * (* string list from arguments of the calling Program*)
1.75 Proof.context * (* for the specify-phase *)
1.76 @@ -373,7 +373,7 @@
1.77 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
1.78 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
1.79 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
1.80 - Method.id_to_string pI ^ ", " ^ Model_Def.oris2str oris ^ ", )"
1.81 + Method.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string oris ^ ", )"
1.82
1.83 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
1.84 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^