1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 10 12:28:47 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 10 14:46:55 2020 +0200
1.3 @@ -10,8 +10,8 @@
1.4 signature TACTIC =
1.5 sig
1.6 datatype T =
1.7 - Add_Find' of UnparseC.cterm' * Model.itm list | Add_Given' of UnparseC.cterm' * Model.itm list
1.8 - | Add_Relation' of UnparseC.cterm' * Model.itm list
1.9 + Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
1.10 + | Add_Relation' of TermC.as_string * Model.itm list
1.11 | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
1.12
1.13 | Begin_Sequ' | Begin_Trans' of term
1.14 @@ -21,10 +21,10 @@
1.15 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.16
1.17 | CAScmd' of term
1.18 - | Calculate' of ThyC.theory' * string * term * (term * ThmC.thm')
1.19 + | Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.thm')
1.20 | Check_Postcond' of Celem.pblID * term
1.21 - | Check_elementwise' of term * UnparseC.cterm' * Selem.result
1.22 - | Del_Find' of UnparseC.cterm' | Del_Given' of UnparseC.cterm' | Del_Relation' of UnparseC.cterm'
1.23 + | Check_elementwise' of term * TermC.as_string * Selem.result
1.24 + | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.25
1.26 | Derive' of Rule_Set.T
1.27 | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.28 @@ -34,14 +34,14 @@
1.29 | Empty_Tac_
1.30 | Free_Solve'
1.31
1.32 - | Init_Proof' of UnparseC.cterm' list * Celem.spec
1.33 + | Init_Proof' of TermC.as_string list * Celem.spec
1.34 | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
1.35 | Or_to_List' of term * term
1.36 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.37 | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.domID * Celem.metID * Model.itm list
1.38
1.39 - | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.thm'' * term * Selem.result
1.40 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.thm'' * term * Selem.result
1.41 + | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC_Def.thm'' * term * Selem.result
1.42 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC_Def.thm'' * term * Selem.result
1.43 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.44 | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
1.45
1.46 @@ -61,8 +61,8 @@
1.47 val string_of: T -> string
1.48
1.49 datatype input =
1.50 - Add_Find of UnparseC.cterm' | Add_Given of UnparseC.cterm' | Add_Relation of UnparseC.cterm'
1.51 - | Apply_Assumption of UnparseC.cterm' list
1.52 + Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
1.53 + | Apply_Assumption of TermC.as_string list
1.54 | Apply_Method of Celem.metID
1.55 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.56 | Begin_Sequ | Begin_Trans
1.57 @@ -71,11 +71,11 @@
1.58 | End_Sequ | End_Trans
1.59 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
1.60 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.61 - | CAScmd of UnparseC.cterm'
1.62 + | CAScmd of TermC.as_string
1.63 | Calculate of string
1.64 | Check_Postcond of Celem.pblID
1.65 - | Check_elementwise of UnparseC.cterm'
1.66 - | Del_Find of UnparseC.cterm' | Del_Given of UnparseC.cterm' | Del_Relation of UnparseC.cterm'
1.67 + | Check_elementwise of TermC.as_string
1.68 + | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
1.69
1.70 | Derive of Rule_Set.identifier
1.71 | Detail_Set of Rule_Set.identifier
1.72 @@ -85,14 +85,14 @@
1.73 | Empty_Tac
1.74 | Free_Solve
1.75
1.76 - | Init_Proof of UnparseC.cterm' list * Celem.spec
1.77 + | Init_Proof of TermC.as_string list * Celem.spec
1.78 | Model_Problem
1.79 | Or_to_List
1.80 | Refine_Problem of Celem.pblID
1.81 | Refine_Tacitly of Celem.pblID
1.82
1.83 - | Rewrite of ThmC.thm''
1.84 - | Rewrite_Inst of Selem.subs * ThmC.thm''
1.85 + | Rewrite of ThmC_Def.thm''
1.86 + | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
1.87 | Rewrite_Set of Rule_Set.identifier
1.88 | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
1.89
1.90 @@ -103,7 +103,7 @@
1.91
1.92 | Substitute of Selem.sube
1.93 | Tac of string
1.94 - | Take of UnparseC.cterm' | Take_Inst of UnparseC.cterm'
1.95 + | Take of TermC.as_string | Take_Inst of TermC.as_string
1.96 val input_to_string : input -> string
1.97 val tac2IDstr : input -> string
1.98 val is_empty : input -> bool
1.99 @@ -144,8 +144,8 @@
1.100 see 'type tac_' for the internal representation of tactics
1.101 *)
1.102 datatype input =
1.103 - Add_Find of UnparseC.cterm' | Add_Given of UnparseC.cterm' | Add_Relation of UnparseC.cterm'
1.104 - | Apply_Assumption of UnparseC.cterm' list
1.105 + Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
1.106 + | Apply_Assumption of TermC.as_string list
1.107 | Apply_Method of Celem.metID
1.108 (* creates an "istate" in PblObj.env; in case of "implicit_take"
1.109 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
1.110 @@ -159,11 +159,11 @@
1.111 | End_Sequ | End_Trans
1.112 | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
1.113 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.114 - | CAScmd of UnparseC.cterm'
1.115 + | CAScmd of TermC.as_string
1.116 | Calculate of string
1.117 | Check_Postcond of Celem.pblID
1.118 - | Check_elementwise of UnparseC.cterm'
1.119 - | Del_Find of UnparseC.cterm' | Del_Given of UnparseC.cterm' | Del_Relation of UnparseC.cterm'
1.120 + | Check_elementwise of TermC.as_string
1.121 + | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
1.122
1.123 | Derive of Rule_Set.identifier (* WN0509 drop *)
1.124 | Detail_Set of Rule_Set.identifier (* WN0509 drop *)
1.125 @@ -173,7 +173,7 @@
1.126 | Empty_Tac
1.127 | Free_Solve
1.128
1.129 - | Init_Proof of UnparseC.cterm' list * Celem.spec
1.130 + | Init_Proof of TermC.as_string list * Celem.spec
1.131 | Model_Problem
1.132 | Or_to_List
1.133 | Refine_Problem of Celem.pblID
1.134 @@ -183,8 +183,8 @@
1.135 because there all the thms are present with both (thmID, thm)
1.136 (where user-views can show both or only one of (thmID, thm)),
1.137 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
1.138 - | Rewrite of ThmC.thm''
1.139 - | Rewrite_Inst of Selem.subs * ThmC.thm''
1.140 + | Rewrite of ThmC_Def.thm''
1.141 + | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
1.142 | Rewrite_Set of Rule_Set.identifier
1.143 | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
1.144
1.145 @@ -195,7 +195,7 @@
1.146
1.147 | Substitute of Selem.sube
1.148 | Tac of string (* WN0509 drop *)
1.149 - | Take of UnparseC.cterm' | Take_Inst of UnparseC.cterm'
1.150 + | Take of TermC.as_string | Take_Inst of TermC.as_string
1.151
1.152 fun input_to_string ma = case ma of
1.153 Init_Proof (ppc, spec) =>
1.154 @@ -334,8 +334,8 @@
1.155 TODO.WN161219: replace *every* cterm' by term
1.156 *)
1.157 datatype T =
1.158 - Add_Find' of UnparseC.cterm' * Model.itm list | Add_Given' of UnparseC.cterm' * Model.itm list
1.159 - | Add_Relation' of UnparseC.cterm' * Model.itm list
1.160 + Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
1.161 + | Add_Relation' of TermC.as_string * Model.itm list
1.162 | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
1.163 * tactic Apply_Method metID
1.164 * formula term *)
1.165 @@ -351,14 +351,14 @@
1.166 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.167 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.168 | CAScmd' of term
1.169 - | Calculate' of ThyC.theory' * string * term * (term * ThmC.thm')
1.170 + | Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.thm')
1.171 | Check_Postcond' of Celem.pblID *
1.172 term (* returnvalue of program in solve *)
1.173 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
1.174 term * (* (1) the current formula: [x=1,x=...] *)
1.175 string * (* (2) the pred from Check_elementwise *)
1.176 Selem.result (* (3) composed from (1) and (2): {x. pred} *)
1.177 - | Del_Find' of UnparseC.cterm' | Del_Given' of UnparseC.cterm' | Del_Relation' of UnparseC.cterm'
1.178 + | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.179
1.180 | Derive' of Rule_Set.T
1.181 | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.182 @@ -368,7 +368,7 @@
1.183 | Empty_Tac_
1.184 | Free_Solve'
1.185
1.186 - | Init_Proof' of UnparseC.cterm' list * Celem.spec
1.187 + | Init_Proof' of TermC.as_string list * Celem.spec
1.188 | Model_Problem' of (* first step in specifying *)
1.189 Celem.pblID * (* key into KEStore *)
1.190 Model.itm list * (* the 'untouched' pbl *)
1.191 @@ -381,8 +381,8 @@
1.192 ThyC.domID * (* from new pbt?! filled in specify *)
1.193 Celem.metID * (* from new pbt?! filled in specify *)
1.194 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.195 - | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.thm'' * term * Selem.result
1.196 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.thm'' * term * Selem.result
1.197 + | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC_Def.thm'' * term * Selem.result
1.198 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC_Def.thm'' * term * Selem.result
1.199 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.200 | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
1.201