1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 17:39:04 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon May 04 09:25:51 2020 +0200
1.3 @@ -12,7 +12,6 @@
1.4 datatype T =
1.5 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
1.6 | Add_Relation' of TermC.as_string * Model.itm list
1.7 - | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
1.8 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.9 | Model_Problem' of Problem.id * Model.itm list * Model.itm list
1.10 | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
1.11 @@ -21,6 +20,7 @@
1.12 | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
1.13 | Specify_Theory' of ThyC.id
1.14 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.15 + | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
1.16 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.17 | Check_Postcond' of Problem.id * term
1.18 | Check_elementwise' of term * TermC.as_string * Selem.result
1.19 @@ -45,7 +45,6 @@
1.20 datatype input =
1.21 Add_Find of TermC.as_string | Add_Given of TermC.as_string
1.22 | Add_Relation of TermC.as_string
1.23 - | Apply_Method of Method.id
1.24 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
1.25 | Model_Problem
1.26 | Refine_Problem of Problem.id
1.27 @@ -54,6 +53,7 @@
1.28 | Specify_Problem of Problem.id
1.29 | Specify_Theory of ThyC.id
1.30 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.31 + | Apply_Method of Method.id
1.32 | Calculate of string
1.33 | Check_Postcond of Problem.id
1.34 | Check_elementwise of TermC.as_string
1.35 @@ -110,7 +110,6 @@
1.36
1.37 datatype input =
1.38 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
1.39 - | Apply_Method of Method.id
1.40 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
1.41 | Model_Problem
1.42 | Refine_Problem of Problem.id
1.43 @@ -119,6 +118,7 @@
1.44 | Specify_Problem of Problem.id
1.45 | Specify_Theory of ThyC.id
1.46 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.47 + | Apply_Method of Method.id
1.48 | Calculate of string
1.49 | Check_Postcond of Problem.id
1.50 | Check_elementwise of TermC.as_string
1.51 @@ -162,6 +162,8 @@
1.52 | Rewrite_Set_Inst (subs, rls) =>
1.53 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
1.54 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
1.55 + | Begin_Trans => "Begin_Trans"
1.56 + | End_Trans => "End_Trans"
1.57 | End_Detail => "End_Detail"
1.58 | Derive rls' => "Derive " ^ rls'
1.59 | Calculate op_ => "Calculate " ^ op_
1.60 @@ -295,11 +297,6 @@
1.61 datatype T =
1.62 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
1.63 | Add_Relation' of TermC.as_string * Model.itm list (* for Step.do_next *)
1.64 - | Apply_Method' of (* last step in specifu-phse, switch to solve-phase *)
1.65 - Method.id * (* id in the Know_Store *)
1.66 - term option * (* first formula in the (sub-)Problem TODO: rm option *)
1.67 - Istate_Def.T * (* for starting the Program *)
1.68 - Proof.context (* for starting the Program *)
1.69 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.70 | Model_Problem' of (* first step in specify-phase *)
1.71 Problem.id * (* id in the Know_Store *)
1.72 @@ -319,6 +316,11 @@
1.73 (bool * term) list)) (* individual preconditions marked true/false *)
1.74 | Specify_Theory' of ThyC.id
1.75 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.76 + | Apply_Method' of (* last step in specifu-phse, switch to solve-phase *)
1.77 + Method.id * (* id in the Know_Store *)
1.78 + term option * (* first formula in the (sub-)Problem TODO: rm option *)
1.79 + Istate_Def.T * (* for starting the Program *)
1.80 + Proof.context (* for starting the Program *)
1.81 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.82 | Check_Postcond' of (* last step in solving a (sub-)Problem *)
1.83 Problem.id * (* id of the Problem to be checked *)
1.84 @@ -450,31 +452,32 @@
1.85
1.86 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt
1.87
1.88 -fun for_specify Model_Problem = true
1.89 +fun for_specify (Add_Find _) = true
1.90 + | for_specify (Add_Given _) = true
1.91 + | for_specify (Add_Relation _) = true
1.92 + | for_specify (Del_Find _) = true
1.93 + | for_specify (Del_Given _) = true
1.94 + | for_specify (Del_Relation _) = true
1.95 + | for_specify Model_Problem = true
1.96 + | for_specify (Refine_Problem _) = true
1.97 | for_specify (Refine_Tacitly _) = true
1.98 - | for_specify (Refine_Problem _) = true
1.99 - | for_specify (Add_Given _) = true
1.100 - | for_specify (Del_Given _) = true
1.101 - | for_specify (Add_Find _) = true
1.102 - | for_specify (Del_Find _) = true
1.103 - | for_specify (Add_Relation _) = true
1.104 - | for_specify (Del_Relation _) = true
1.105 + | for_specify (Specify_Method _) = true
1.106 + | for_specify (Specify_Problem _) = true
1.107 | for_specify (Specify_Theory _) = true
1.108 - | for_specify (Specify_Problem _) = true
1.109 - | for_specify (Specify_Method _) = true
1.110 | for_specify _ = false
1.111 -fun for_specify' (Model_Problem' _) = true
1.112 +
1.113 +fun for_specify' (Add_Find' _) = true
1.114 + | for_specify' (Add_Given' _) = true
1.115 + | for_specify' (Add_Relation' _) = true
1.116 + | for_specify' (Del_Find' _) = true
1.117 + | for_specify' (Del_Given' _) = true
1.118 + | for_specify' (Del_Relation' _) = true
1.119 + | for_specify' (Model_Problem' _) = true
1.120 + | for_specify' (Refine_Problem' _) = true
1.121 | for_specify' (Refine_Tacitly' _) = true
1.122 - | for_specify' (Refine_Problem' _) = true
1.123 - | for_specify' (Add_Given' _) = true
1.124 - | for_specify' (Del_Given' _) = true
1.125 - | for_specify' (Add_Find' _) = true
1.126 - | for_specify' (Del_Find' _) = true
1.127 - | for_specify' (Add_Relation' _) = true
1.128 - | for_specify' (Del_Relation' _) = true
1.129 + | for_specify' (Specify_Method' _) = true
1.130 + | for_specify' (Specify_Problem' _) = true
1.131 | for_specify' (Specify_Theory' _) = true
1.132 - | for_specify' (Specify_Problem' _) = true
1.133 - | for_specify' (Specify_Method' _) = true
1.134 | for_specify' _ = false
1.135
1.136 (**)end(**)