1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Tue Dec 17 17:19:34 2019 +0100
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Tue Dec 17 17:52:48 2019 +0100
1.3 @@ -9,10 +9,98 @@
1.4 *)
1.5 signature TACTIC =
1.6 sig
1.7 - datatype T = datatype Tactic_Def.T
1.8 + datatype T =
1.9 + Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
1.10 + | Add_Relation' of Rule.cterm' * Model.itm list
1.11 + | Apply_Assumption' of term list * term
1.12 + | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
1.13 +
1.14 + | Begin_Sequ' | Begin_Trans' of term
1.15 + | Split_And' of term | Split_Or' of term | Split_Intersect' of term
1.16 + | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
1.17 + | End_Sequ' | End_Trans' of Selem.result
1.18 + | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
1.19 +
1.20 + | CAScmd' of term
1.21 + | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
1.22 + | Check_Postcond' of Celem.pblID * Selem.result
1.23 + | Check_elementwise' of term * Rule.cterm' * Selem.result
1.24 + | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.25 +
1.26 + | Derive' of Rule.rls
1.27 + | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.28 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
1.29 + | End_Detail' of Selem.result
1.30 +
1.31 + | Empty_Tac_
1.32 + | Free_Solve'
1.33 +
1.34 + | Init_Proof' of Rule.cterm' list * Celem.spec
1.35 + | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
1.36 + | Or_to_List' of term * term
1.37 + | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.38 + | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
1.39 +
1.40 + | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
1.41 + | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
1.42 + | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.43 + | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.44 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * 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 + | Specify_Theory' of Rule.domID
1.49 + | Subproblem' of Celem.spec * Model.ori list * term * Selem.fmz_ * Proof.context * term
1.50 + | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
1.51 + | Tac_ of theory * string * string * string
1.52 + | Take' of term | Take_Inst' of term
1.53 val string_of : T -> string
1.54
1.55 - datatype input = datatype Tactic_Def.input
1.56 + datatype input =
1.57 + Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
1.58 + | Apply_Assumption of Rule.cterm' list
1.59 + | Apply_Method of Celem.metID
1.60 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.61 + | Begin_Sequ | Begin_Trans
1.62 + | Split_And | Split_Or | Split_Intersect
1.63 + | Conclude_And | Conclude_Or | Collect_Trues
1.64 + | End_Sequ | End_Trans
1.65 + | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
1.66 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.67 + | CAScmd of Rule.cterm'
1.68 + | Calculate of string
1.69 + | Check_Postcond of Celem.pblID
1.70 + | Check_elementwise of Rule.cterm'
1.71 + | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
1.72 +
1.73 + | Derive of Rule.rls'
1.74 + | Detail_Set of Rule.rls'
1.75 + | Detail_Set_Inst of Selem.subs * Rule.rls'
1.76 + | End_Detail
1.77 +
1.78 + | Empty_Tac
1.79 + | Free_Solve
1.80 +
1.81 + | Init_Proof of Rule.cterm' list * Celem.spec
1.82 + | Model_Problem
1.83 + | Or_to_List
1.84 + | Refine_Problem of Celem.pblID
1.85 + | Refine_Tacitly of Celem.pblID
1.86 +
1.87 + | Rewrite of Celem.thm''
1.88 + | Rewrite_Asm of Celem.thm''
1.89 + | Rewrite_Inst of Selem.subs * Celem.thm''
1.90 + | Rewrite_Set of Rule.rls'
1.91 + | Rewrite_Set_Inst of Selem.subs * Rule.rls'
1.92 +
1.93 + | Specify_Method of Celem.metID
1.94 + | Specify_Problem of Celem.pblID
1.95 + | Specify_Theory of Rule.domID
1.96 + | Subproblem of Rule.domID * Celem.pblID
1.97 +
1.98 + | Substitute of Selem.sube
1.99 + | Tac of string
1.100 + | Take of Rule.cterm' | Take_Inst of Rule.cterm'
1.101 val tac2str : input -> string
1.102
1.103 val eq_tac : input * input -> bool
1.104 @@ -50,11 +138,112 @@
1.105 initacs start with a formula different from the preceding formula.
1.106 see 'type tac_' for the internal representation of tactics
1.107 *)
1.108 -datatype input = datatype Tactic_Def.input
1.109 +datatype input =
1.110 + Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
1.111 + | Apply_Assumption of Rule.cterm' list
1.112 + | Apply_Method of Celem.metID
1.113 + (* creates an "istate" in PblObj.env; in case of "init_form"
1.114 + creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
1.115 + a "SOME istate" at fst of "loc".
1.116 + As each step (in the solve-phase) has a resulting formula (at the front-end)
1.117 + Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *)
1.118 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.119 + | Begin_Sequ | Begin_Trans
1.120 + | Split_And | Split_Or | Split_Intersect
1.121 + | Conclude_And | Conclude_Or | Collect_Trues
1.122 + | End_Sequ | End_Trans
1.123 + | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
1.124 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.125 + | CAScmd of Rule.cterm'
1.126 + | Calculate of string
1.127 + | Check_Postcond of Celem.pblID
1.128 + | Check_elementwise of Rule.cterm'
1.129 + | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
1.130
1.131 -val tac2str = Tactic_Def.tac2str
1.132 + | Derive of Rule.rls' (* WN0509 drop *)
1.133 + | Detail_Set of Rule.rls' (* WN0509 drop *)
1.134 + | Detail_Set_Inst of Selem.subs * Rule.rls' (* WN0509 drop *)
1.135 + | End_Detail (* WN0509 drop *)
1.136
1.137 -val is_empty_tac = Tactic_Def.is_empty_tac
1.138 + | Empty_Tac
1.139 + | Free_Solve
1.140 +
1.141 + | Init_Proof of Rule.cterm' list * Celem.spec
1.142 + | Model_Problem
1.143 + | Or_to_List
1.144 + | Refine_Problem of Celem.pblID
1.145 + | Refine_Tacitly of Celem.pblID
1.146 +
1.147 + (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
1.148 + because there all the thms are present with both (thmID, thm)
1.149 + (where user-views can show both or only one of (thmID, thm)),
1.150 + and thm is created from ThmID by assoc_thm'' when entering isabisac *)
1.151 + | Rewrite of Celem.thm''
1.152 + | Rewrite_Asm of Celem.thm''
1.153 + | Rewrite_Inst of Selem.subs * Celem.thm''
1.154 + | Rewrite_Set of Rule.rls'
1.155 + | Rewrite_Set_Inst of Selem.subs * Rule.rls'
1.156 +
1.157 + | Specify_Method of Celem.metID
1.158 + | Specify_Problem of Celem.pblID
1.159 + | Specify_Theory of Rule.domID
1.160 + | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
1.161 +
1.162 + | Substitute of Selem.sube
1.163 + | Tac of string (* WN0509 drop *)
1.164 + | Take of Rule.cterm' | Take_Inst of Rule.cterm'
1.165 +
1.166 +fun tac2str ma = case ma of
1.167 + Init_Proof (ppc, spec) =>
1.168 + "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec))
1.169 + | Model_Problem => "Model_Problem "
1.170 + | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
1.171 + | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
1.172 + | Add_Given cterm' => "Add_Given " ^ cterm'
1.173 + | Del_Given cterm' => "Del_Given " ^ cterm'
1.174 + | Add_Find cterm' => "Add_Find " ^ cterm'
1.175 + | Del_Find cterm' => "Del_Find " ^ cterm'
1.176 + | Add_Relation cterm' => "Add_Relation " ^ cterm'
1.177 + | Del_Relation cterm' => "Del_Relation " ^ cterm'
1.178 +
1.179 + | Specify_Theory domID => "Specify_Theory " ^ quote domID
1.180 + | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
1.181 + | Specify_Method metID => "Specify_Method " ^ strs2str metID
1.182 + | Apply_Method metID => "Apply_Method " ^ strs2str metID
1.183 + | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
1.184 + | Free_Solve => "Free_Solve"
1.185 +
1.186 + | Rewrite_Inst (subs, (id, thm)) =>
1.187 + "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str)))
1.188 + | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
1.189 + | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
1.190 + | Rewrite_Set_Inst (subs, rls) =>
1.191 + "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
1.192 + | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
1.193 + | Detail_Set rls => "Detail_Set " ^ quote rls
1.194 + | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
1.195 + | End_Detail => "End_Detail"
1.196 + | Derive rls' => "Derive " ^ rls'
1.197 + | Calculate op_ => "Calculate " ^ op_
1.198 + | Substitute sube => "Substitute " ^ Selem.sube2str sube
1.199 + | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
1.200 +
1.201 + | Take cterm' => "Take " ^ quote cterm'
1.202 + | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
1.203 + | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
1.204 + | End_Subproblem => "End_Subproblem"
1.205 + | CAScmd cterm' => "CAScmd " ^ quote cterm'
1.206 +
1.207 + | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
1.208 + | Or_to_List => "Or_to_List "
1.209 + | Collect_Trues => "Collect_Trues"
1.210 +
1.211 + | Empty_Tac => "Empty_Tac"
1.212 + | Tac string => "Tac " ^ string
1.213 + | End_Proof' => "input End_Proof'"
1.214 + | _ => "tac2str not impl. for ?!";
1.215 +
1.216 +fun is_empty_tac input = case input of Empty_Tac => true | _ => false
1.217
1.218 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
1.219 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
1.220 @@ -142,9 +331,126 @@
1.221 and re-calculate result if t<>t'
1.222 TODO.WN161219: replace *every* cterm' by term
1.223 *)
1.224 - datatype T = datatype Tactic_Def.T
1.225 + datatype T =
1.226 + Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
1.227 + | Add_Relation' of Rule.cterm' * Model.itm list
1.228 + | Apply_Assumption' of term list * term
1.229 + | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
1.230 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.231 + | Begin_Sequ' | Begin_Trans' of term
1.232 + | Split_And' of term | Split_Or' of term | Split_Intersect' of term
1.233 + | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
1.234 + | End_Sequ' | End_Trans' of Selem.result
1.235 + | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
1.236 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.237 + | CAScmd' of term
1.238 + | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
1.239 + | Check_Postcond' of Celem.pblID *
1.240 + Selem.result (* returnvalue of script in solve *)
1.241 + | Check_elementwise' of (*special case:*)
1.242 + term * (* (1) the current formula: [x=1,x=...] *)
1.243 + string * (* (2) the pred from Check_elementwise *)
1.244 + Selem.result (* (3) composed from (1) and (2): {x. pred} *)
1.245 + | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.246
1.247 -val string_of = Tactic_Def.string_of
1.248 + | Derive' of Rule.rls
1.249 + | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.250 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
1.251 + | End_Detail' of Selem.result
1.252 +
1.253 + | Empty_Tac_
1.254 + | Free_Solve'
1.255 +
1.256 + | Init_Proof' of Rule.cterm' list * Celem.spec
1.257 + | Model_Problem' of Celem.pblID *
1.258 + Model.itm list * (* the 'untouched' pbl *)
1.259 + Model.itm list (* the casually completed met *)
1.260 + | Or_to_List' of term * term
1.261 + | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.262 + | Refine_Tacitly' of
1.263 + Celem.pblID * (* input*)
1.264 + Celem.pblID * (* the refined from applicable_in *)
1.265 + Rule.domID * (* from new pbt?! filled in specify *)
1.266 + Celem.metID * (* from new pbt?! filled in specify *)
1.267 + Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.268 + | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
1.269 + | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
1.270 + | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.271 + | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.272 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
1.273 +
1.274 + | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.275 + | Specify_Problem' of Celem.pblID *
1.276 + (bool * (* matches *)
1.277 + (Model.itm list * (* ppc *)
1.278 + (bool * term) list)) (* preconditions *)
1.279 + | Specify_Theory' of Rule.domID
1.280 + | Subproblem' of
1.281 + Celem.spec *
1.282 + (Model.ori list) * (* filled in associate Subproblem' *)
1.283 + term * (* filled -"-, headline of calc-head *)
1.284 + Selem.fmz_ *
1.285 + Proof.context * (* DEPRECATED shifted into loc for all ppobj *)
1.286 + term (* Subproblem (thyID, pbl) OR cascmd *)
1.287 + | Substitute' of
1.288 + Rule.rew_ord_ * (* for re-calculation *)
1.289 + Rule.rls * (* for re-calculation *)
1.290 + Selem.subte * (* the 'substitution': terms of type bool *)
1.291 + term * (* to be substituted into *)
1.292 + term (* resulting from the substitution *)
1.293 + | Tac_ of theory * string * string * string
1.294 + | Take' of term | Take_Inst' of term
1.295 +
1.296 +fun string_of ma = case ma of
1.297 + Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
1.298 + | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
1.299 + | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
1.300 + strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
1.301 + | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
1.302 + | Add_Given' _ => "Add_Given' "(*^cterm'*)
1.303 + | Del_Given' _ => "Del_Given' "(*^cterm'*)
1.304 + | Add_Find' _ => "Add_Find' "(*^cterm'*)
1.305 + | Del_Find' _ => "Del_Find' "(*^cterm'*)
1.306 + | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
1.307 + | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
1.308 +
1.309 + | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
1.310 + | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
1.311 + spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
1.312 + | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
1.313 + Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
1.314 +
1.315 + | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
1.316 + | Check_Postcond' (pblID, (scval, asm)) => "Check_Postcond' " ^
1.317 + (spair2str (strs2str pblID, spair2str (Rule.term2str scval, Rule.terms2str asm)))
1.318 +
1.319 + | Free_Solve' => "Free_Solve'"
1.320 +
1.321 + | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
1.322 + | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
1.323 + | Rewrite_Asm' _(*thm'*) => "Rewrite_Asm' "(*^(spair2str thm')*)
1.324 + | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
1.325 + | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
1.326 + "," ^ Rule.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
1.327 + | End_Detail' _ => "End_Detail' xxx"
1.328 + | Detail_Set' _ => "Detail_Set' xxx"
1.329 + | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
1.330 +
1.331 + | Derive' rls => "Derive' " ^ Rule.id_rls rls
1.332 + | Calculate' _ => "Calculate' "
1.333 + | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
1.334 + | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*)
1.335 +
1.336 + | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
1.337 + | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*)
1.338 + | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
1.339 + "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
1.340 + | End_Subproblem' _ => "End_Subproblem'"
1.341 + | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
1.342 +
1.343 + | Empty_Tac_ => "Empty_Tac_"
1.344 + | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
1.345 + | _ => "string_of not impl. for arg";
1.346
1.347 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
1.348 | input_from_T (Model_Problem' (_, _, _)) = Model_Problem