1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Thu Apr 09 17:16:48 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Thu Apr 09 18:21:09 2020 +0200
1.3 @@ -10,8 +10,8 @@
1.4 signature TACTIC =
1.5 sig
1.6 datatype T =
1.7 - Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
1.8 - | Add_Relation' of Rule.cterm' * Model.itm list
1.9 + Add_Find' of UnparseC.cterm' * Model.itm list | Add_Given' of UnparseC.cterm' * Model.itm list
1.10 + | Add_Relation' of UnparseC.cterm' * 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 @@ -23,27 +23,27 @@
1.15 | CAScmd' of term
1.16 | Calculate' of ThyC.theory' * string * term * (term * ThmC.thm')
1.17 | Check_Postcond' of Celem.pblID * term
1.18 - | Check_elementwise' of term * Rule.cterm' * Selem.result
1.19 - | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.20 + | Check_elementwise' of term * UnparseC.cterm' * Selem.result
1.21 + | Del_Find' of UnparseC.cterm' | Del_Given' of UnparseC.cterm' | Del_Relation' of UnparseC.cterm'
1.22
1.23 | Derive' of Rule_Set.T
1.24 | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.25 - | Detail_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.26 + | Detail_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
1.27 | End_Detail' of Selem.result
1.28
1.29 | Empty_Tac_
1.30 | Free_Solve'
1.31
1.32 - | Init_Proof' of Rule.cterm' list * Celem.spec
1.33 + | Init_Proof' of UnparseC.cterm' 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 * Rule.subst * ThmC.thm'' * term * Selem.result
1.41 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.thm'' * term * Selem.result
1.42 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.43 - | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * 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 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.47 | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
1.48 @@ -61,8 +61,8 @@
1.49 val string_of: T -> string
1.50
1.51 datatype input =
1.52 - Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
1.53 - | Apply_Assumption of Rule.cterm' list
1.54 + Add_Find of UnparseC.cterm' | Add_Given of UnparseC.cterm' | Add_Relation of UnparseC.cterm'
1.55 + | Apply_Assumption of UnparseC.cterm' list
1.56 | Apply_Method of Celem.metID
1.57 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.58 | Begin_Sequ | Begin_Trans
1.59 @@ -71,11 +71,11 @@
1.60 | End_Sequ | End_Trans
1.61 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
1.62 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.63 - | CAScmd of Rule.cterm'
1.64 + | CAScmd of UnparseC.cterm'
1.65 | Calculate of string
1.66 | Check_Postcond of Celem.pblID
1.67 - | Check_elementwise of Rule.cterm'
1.68 - | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
1.69 + | Check_elementwise of UnparseC.cterm'
1.70 + | Del_Find of UnparseC.cterm' | Del_Given of UnparseC.cterm' | Del_Relation of UnparseC.cterm'
1.71
1.72 | Derive of Rule_Set.identifier
1.73 | Detail_Set of Rule_Set.identifier
1.74 @@ -85,7 +85,7 @@
1.75 | Empty_Tac
1.76 | Free_Solve
1.77
1.78 - | Init_Proof of Rule.cterm' list * Celem.spec
1.79 + | Init_Proof of UnparseC.cterm' list * Celem.spec
1.80 | Model_Problem
1.81 | Or_to_List
1.82 | Refine_Problem of Celem.pblID
1.83 @@ -103,7 +103,7 @@
1.84
1.85 | Substitute of Selem.sube
1.86 | Tac of string
1.87 - | Take of Rule.cterm' | Take_Inst of Rule.cterm'
1.88 + | Take of UnparseC.cterm' | Take_Inst of UnparseC.cterm'
1.89 val input_to_string : input -> string
1.90 val tac2IDstr : input -> string
1.91 val is_empty : input -> bool
1.92 @@ -144,8 +144,8 @@
1.93 see 'type tac_' for the internal representation of tactics
1.94 *)
1.95 datatype input =
1.96 - Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
1.97 - | Apply_Assumption of Rule.cterm' list
1.98 + Add_Find of UnparseC.cterm' | Add_Given of UnparseC.cterm' | Add_Relation of UnparseC.cterm'
1.99 + | Apply_Assumption of UnparseC.cterm' list
1.100 | Apply_Method of Celem.metID
1.101 (* creates an "istate" in PblObj.env; in case of "implicit_take"
1.102 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
1.103 @@ -159,11 +159,11 @@
1.104 | End_Sequ | End_Trans
1.105 | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
1.106 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.107 - | CAScmd of Rule.cterm'
1.108 + | CAScmd of UnparseC.cterm'
1.109 | Calculate of string
1.110 | Check_Postcond of Celem.pblID
1.111 - | Check_elementwise of Rule.cterm'
1.112 - | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
1.113 + | Check_elementwise of UnparseC.cterm'
1.114 + | Del_Find of UnparseC.cterm' | Del_Given of UnparseC.cterm' | Del_Relation of UnparseC.cterm'
1.115
1.116 | Derive of Rule_Set.identifier (* WN0509 drop *)
1.117 | Detail_Set of Rule_Set.identifier (* WN0509 drop *)
1.118 @@ -173,7 +173,7 @@
1.119 | Empty_Tac
1.120 | Free_Solve
1.121
1.122 - | Init_Proof of Rule.cterm' list * Celem.spec
1.123 + | Init_Proof of UnparseC.cterm' list * Celem.spec
1.124 | Model_Problem
1.125 | Or_to_List
1.126 | Refine_Problem of Celem.pblID
1.127 @@ -195,7 +195,7 @@
1.128
1.129 | Substitute of Selem.sube
1.130 | Tac of string (* WN0509 drop *)
1.131 - | Take of Rule.cterm' | Take_Inst of Rule.cterm'
1.132 + | Take of UnparseC.cterm' | Take_Inst of UnparseC.cterm'
1.133
1.134 fun input_to_string ma = case ma of
1.135 Init_Proof (ppc, spec) =>
1.136 @@ -315,9 +315,9 @@
1.137 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
1.138 | rule2tac _ subst (Rule.Thm thm'') =
1.139 Rewrite_Inst (Selem.subst2subs subst, thm'')
1.140 - | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id_rls rls)
1.141 + | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.rls2str rls)
1.142 | rule2tac _ subst (Rule.Rls_ rls) =
1.143 - Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.id_rls rls))
1.144 + Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.rls2str rls))
1.145 | rule2tac _ _ rule =
1.146 error ("rule2tac: called with \"" ^ Rule_Set.rule2str rule ^ "\"");
1.147
1.148 @@ -334,8 +334,8 @@
1.149 TODO.WN161219: replace *every* cterm' by term
1.150 *)
1.151 datatype T =
1.152 - Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
1.153 - | Add_Relation' of Rule.cterm' * Model.itm list
1.154 + Add_Find' of UnparseC.cterm' * Model.itm list | Add_Given' of UnparseC.cterm' * Model.itm list
1.155 + | Add_Relation' of UnparseC.cterm' * Model.itm list
1.156 | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
1.157 * tactic Apply_Method metID
1.158 * formula term *)
1.159 @@ -358,17 +358,17 @@
1.160 term * (* (1) the current formula: [x=1,x=...] *)
1.161 string * (* (2) the pred from Check_elementwise *)
1.162 Selem.result (* (3) composed from (1) and (2): {x. pred} *)
1.163 - | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.164 + | Del_Find' of UnparseC.cterm' | Del_Given' of UnparseC.cterm' | Del_Relation' of UnparseC.cterm'
1.165
1.166 | Derive' of Rule_Set.T
1.167 | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.168 - | Detail_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.169 + | Detail_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
1.170 | End_Detail' of Selem.result
1.171
1.172 | Empty_Tac_
1.173 | Free_Solve'
1.174
1.175 - | Init_Proof' of Rule.cterm' list * Celem.spec
1.176 + | Init_Proof' of UnparseC.cterm' list * Celem.spec
1.177 | Model_Problem' of (* first step in specifying *)
1.178 Celem.pblID * (* key into KEStore *)
1.179 Model.itm list * (* the 'untouched' pbl *)
1.180 @@ -382,9 +382,9 @@
1.181 Celem.metID * (* from new pbt?! filled in specify *)
1.182 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.183 | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.thm'' * term * Selem.result
1.184 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Rule.subst * ThmC.thm'' * term * Selem.result
1.185 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.thm'' * term * Selem.result
1.186 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.187 - | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.188 + | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
1.189
1.190 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.191 | Specify_Problem' of Celem.pblID *
1.192 @@ -437,12 +437,12 @@
1.193 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
1.194 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
1.195 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
1.196 - "," ^ Rule_Set.id_rls rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
1.197 + "," ^ Rule_Set.rls2str rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
1.198 | End_Detail' _ => "End_Detail' xxx"
1.199 | Detail_Set' _ => "Detail_Set' xxx"
1.200 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
1.201
1.202 - | Derive' rls => "Derive' " ^ Rule_Set.id_rls rls
1.203 + | Derive' rls => "Derive' " ^ Rule_Set.rls2str rls
1.204 | Calculate' _ => "Calculate' "
1.205 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
1.206
1.207 @@ -468,13 +468,13 @@
1.208 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
1.209 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
1.210
1.211 - | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id_rls rls)
1.212 - | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id_rls rls)
1.213 + | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.rls2str rls)
1.214 + | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.rls2str rls)
1.215
1.216 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
1.217 - Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.id_rls rls)
1.218 + Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.rls2str rls)
1.219 | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
1.220 - Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.id_rls rls)
1.221 + Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.rls2str rls)
1.222
1.223 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
1.224 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred