1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Mon May 04 13:27:45 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon May 04 16:25:14 2020 +0200
1.3 @@ -10,34 +10,34 @@
1.4 signature TACTIC =
1.5 sig
1.6 datatype T =
1.7 - Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
1.8 - | Add_Relation' of TermC.as_string * Model.itm list
1.9 + Add_Find' of TermC.as_string * Model_Def.itm list | Add_Given' of TermC.as_string * Model_Def.itm list
1.10 + | Add_Relation' of TermC.as_string * Model_Def.itm list
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.itm list * Model.itm list
1.13 - | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
1.14 - | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
1.15 - | Specify_Method' of Method.id * Model.ori list * Model.itm list
1.16 - | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
1.17 + | Model_Problem' of Problem.id * Model_Def.itm list * Model_Def.itm list
1.18 + | Refine_Problem' of Problem.id * (Model_Def.itm list * (bool * term) list)
1.19 + | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model_Def.itm list
1.20 + | Specify_Method' of Method.id * Model_Def.ori list * Model_Def.itm list
1.21 + | Specify_Problem' of Problem.id * (bool * (Model_Def.itm list * (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 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.26 | Check_Postcond' of Problem.id * term
1.27 - | Check_elementwise' of term * TermC.as_string * Selem.result
1.28 + | Check_elementwise' of term * TermC.as_string * Celem.result
1.29 | Derive' of Rule_Set.T
1.30 | Empty_Tac_
1.31 | Free_Solve'
1.32 | Or_to_List' of term * term
1.33 - | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
1.34 - | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
1.35 - | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.36 - | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
1.37 - | Subproblem' of Spec.T * Model.ori list * term * Selem.fmz_ * Proof.context * term
1.38 + | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
1.39 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
1.40 + | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
1.41 + | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
1.42 + | Subproblem' of Spec.T * Model_Def.ori list * term * Celem.fmz_ * Proof.context * term
1.43 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
1.44 (*RM*)| Tac_ of theory * string * string * string
1.45 | Take' of term
1.46 - | End_Detail' of Selem.result
1.47 - | Begin_Trans' of term | End_Trans' of Selem.result
1.48 + | End_Detail' of Celem.result
1.49 + | Begin_Trans' of term | End_Trans' of Celem.result
1.50 | End_Proof''
1.51
1.52 val string_of: T -> string
1.53 @@ -295,24 +295,24 @@
1.54 (** tactics for internal use **)
1.55
1.56 datatype T =
1.57 - Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
1.58 - | Add_Relation' of TermC.as_string * Model.itm list (* for Step.do_next *)
1.59 + Add_Find' of TermC.as_string * Model_Def.itm list | Add_Given' of TermC.as_string * Model_Def.itm list
1.60 + | Add_Relation' of TermC.as_string * Model_Def.itm list (* for Step.do_next *)
1.61 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.62 | Model_Problem' of (* first step in specify-phase *)
1.63 Problem.id * (* id in the Know_Store *)
1.64 - Model.itm list * (* the model for the Problem *)
1.65 - Model.itm list (* the model for the method *)
1.66 - | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
1.67 + Model_Def.itm list * (* the model for the Problem *)
1.68 + Model_Def.itm list (* the model for the method *)
1.69 + | Refine_Problem' of Problem.id * (Model_Def.itm list * (bool * term) list)
1.70 | Refine_Tacitly' of
1.71 Problem.id * (* the original id in the Know_Store *)
1.72 Problem.id * (* the id of the refined Problem *)
1.73 ThyC.id * (* the id of the refined theory *)
1.74 Method.id * (* the id of the refined Method *)
1.75 - Model.itm list (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
1.76 - | Specify_Method' of Method.id * Model.ori list * Model.itm list
1.77 + Model_Def.itm list (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
1.78 + | Specify_Method' of Method.id * Model_Def.ori list * Model_Def.itm list
1.79 | Specify_Problem' of Problem.id *
1.80 (bool * (* all preconditions evaluate to True *)
1.81 - (Model.itm list * (* the model checked for the input id *)
1.82 + (Model_Def.itm list * (* the model checked for the input id *)
1.83 (bool * term) list)) (* individual preconditions marked true/false *)
1.84 | Specify_Theory' of ThyC.id
1.85 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.86 @@ -328,20 +328,20 @@
1.87 | Check_elementwise' of(* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
1.88 term * (* the current formula: [x=1,x=...] *)
1.89 string * (* the pred from Check_elementwise *)
1.90 - Selem.result (* composed from (1) and (2): {x. pred} *)
1.91 + Celem.result (* composed from (1) and (2): {x. pred} *)
1.92 | Derive' of Rule_Set.T(* for Generate.embed_deriv *)
1.93 | Empty_Tac_
1.94 | Free_Solve'
1.95 | Or_to_List' of term * term
1.96 - | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
1.97 - | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
1.98 - | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.99 - | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
1.100 + | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
1.101 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
1.102 + | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
1.103 + | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
1.104 | Subproblem' of (* switch from solve-phase to specify-phase *)
1.105 Spec.T * (* specification of the SubProblem *)
1.106 - (Model.ori list) * (* original model, filled in associate Subproblem' *)
1.107 + (Model_Def.ori list) * (* original model, filled in associate Subproblem' *)
1.108 term * (* headline of calc-head, filled -"- *)
1.109 - Selem.fmz_ * (* string list from arguments of the calling Program*)
1.110 + Celem.fmz_ * (* string list from arguments of the calling Program*)
1.111 Proof.context * (* for the specify-phase *)
1.112 term (* Subproblem (thyID, pbl) OR CAS_Cmd *)
1.113 | Substitute' of (* substitute variables (TODO: from the context) *)
1.114 @@ -352,9 +352,9 @@
1.115 term (* resulting from the substitution *)
1.116 (*RM*)| Tac_ of theory * string * string * string
1.117 | Take' of term
1.118 - | End_Detail' of Selem.result (* for intermediate steps into Rewrite_Set *)
1.119 + | End_Detail' of Celem.result (* for intermediate steps into Rewrite_Set *)
1.120 | Begin_Trans' of term (* for intermediate steps into Rewrite_Set *)
1.121 - | End_Trans' of Selem.result (* for intermediate steps into Rewrite_Set *)
1.122 + | End_Trans' of Celem.result (* for intermediate steps into Rewrite_Set *)
1.123 | End_Proof''
1.124
1.125 fun string_of ma = case ma of
1.126 @@ -373,7 +373,7 @@
1.127 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
1.128 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
1.129 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
1.130 - Method.id_to_string pI ^ ", " ^ Model.oris2str oris ^ ", )"
1.131 + Method.id_to_string pI ^ ", " ^ Model_Def.oris2str oris ^ ", )"
1.132
1.133 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
1.134 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^