1.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Dec 17 17:19:34 2019 +0100
1.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Dec 17 17:52:48 2019 +0100
1.3 @@ -12,13 +12,12 @@
1.4 ML_file mstools.sml
1.5 ML_file "specification-elems.sml"
1.6 ML_file "istate-def.sml"
1.7 - ML_file "tactic-def.sml"
1.8 + ML_file tactic.sml
1.9 ML_file position.sml
1.10 ML_file "ctree-basic.sml"
1.11 ML_file "ctree-access.sml"
1.12 ML_file "ctree-navi.sml"
1.13 ML_file ctree.sml
1.14 - ML_file tactic.sml
1.15
1.16 ML \<open>
1.17 \<close> ML \<open>
2.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Tue Dec 17 17:19:34 2019 +0100
2.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Tue Dec 17 17:52:48 2019 +0100
2.3 @@ -19,7 +19,7 @@
2.4 val update_oris : CTbasic.ctree -> CTbasic.pos -> Model.ori list -> CTbasic.ctree
2.5 val update_orispec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree
2.6 val update_spec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree
2.7 - val update_tac : CTbasic.ctree -> CTbasic.pos -> Tactic_Def.input -> CTbasic.ctree
2.8 + val update_tac : CTbasic.ctree -> CTbasic.pos -> Tactic.input -> CTbasic.ctree
2.9
2.10 val upd_istate_ctxt : CTbasic.state -> Istate_Def.T * Proof.context -> CTbasic.ctree
2.11 val upd_istate : CTbasic.state -> Istate_Def.T -> CTbasic.ctree
2.12 @@ -32,13 +32,13 @@
2.13 val append_result : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context ->
2.14 Selem.result -> CTbasic.ostate -> CTbasic.ctree * 'a list
2.15 val append_atomic : (* for solve.sml *)
2.16 - CTbasic.pos -> Istate_Def.T * Proof.context -> term -> Tactic_Def.input -> Selem.result ->
2.17 + CTbasic.pos -> Istate_Def.T * Proof.context -> term -> Tactic.input -> Selem.result ->
2.18 CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree
2.19 val cappend_atomic : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> term ->
2.20 - Tactic_Def.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * CTbasic.pos' list
2.21 + Tactic.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * CTbasic.pos' list
2.22 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.23 val cappend_parent : CTbasic.ctree -> int list -> Istate_Def.T * Proof.context -> term ->
2.24 - Tactic_Def.input -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list
2.25 + Tactic.input -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list
2.26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.27 val update_loc' : CTbasic.ctree -> CTbasic.pos ->
2.28 (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option -> CTbasic.ctree
2.29 @@ -208,7 +208,7 @@
2.30
2.31 (* called by Take *)
2.32 fun append_form p l f pt =
2.33 - insert_pt (PrfObj {cell = NONE, form = f, tac = Tactic_Def.Empty_Tac, loc = (SOME l, NONE),
2.34 + insert_pt (PrfObj {cell = NONE, form = f, tac = Tactic.Empty_Tac, loc = (SOME l, NONE),
2.35 branch = NoBranch, result = (Rule.e_term, []), ostate = Incomplete}) pt p;
2.36 fun cappend_form pt p loc f =
2.37 let
2.38 @@ -232,7 +232,7 @@
2.39 fun append_parent p l f r b pt =
2.40 let
2.41 val (ll, f) =
2.42 - if existpt p pt andalso Tactic_Def.is_empty_tac (get_obj g_tac pt p)
2.43 + if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)
2.44 then ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p)
2.45 else ((SOME l, NONE), f)
2.46 in insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = ll,
2.47 @@ -244,7 +244,7 @@
2.48 fun append_atomic p l f r f' s pt =
2.49 let
2.50 val (iss, f) =
2.51 - if existpt p pt andalso Tactic_Def.is_empty_tac (get_obj g_tac pt p)
2.52 + if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)
2.53 then (*after Take*) ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p)
2.54 else ((NONE, SOME l), f)
2.55 in
2.56 @@ -257,7 +257,7 @@
2.57 cut decided in applicable_in !?!
2.58 *)
2.59 fun cappend_atomic pt p ist_res f r f' s =
2.60 - if existpt p pt andalso Tactic_Def.is_empty_tac (get_obj g_tac pt p)
2.61 + if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)
2.62 then (*after Take: transfer Frm and respective istate*)
2.63 let
2.64 val (ist_form, f) =
3.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Dec 17 17:19:34 2019 +0100
3.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Dec 17 17:52:48 2019 +0100
3.3 @@ -42,7 +42,7 @@
3.4 result: Selem.result,
3.5
3.6 form: term,
3.7 - tac: Tactic_Def.input}
3.8 + tac: Tactic.input}
3.9 datatype ctree = EmptyPtree | Nd of ppobj * ctree list
3.10
3.11 (** basic functions **)
3.12 @@ -68,7 +68,7 @@
3.13 val g_met : ppobj -> Model.itm list
3.14 val g_metID : ppobj -> Celem.metID
3.15 val g_result : ppobj -> Selem.result
3.16 - val g_tac : ppobj -> Tactic_Def.input
3.17 + val g_tac : ppobj -> Tactic.input
3.18 val g_domID : ppobj -> Rule.domID (* for appl.sml TODO: replace by thyID *)
3.19 val g_env : ppobj -> (Istate_Def.T * Proof.context) option (* for appl.sml *)
3.20
3.21 @@ -173,7 +173,7 @@
3.22 used for continuing eval script + for generate *)
3.23 type ets =
3.24 (Celem.path *(* of tactic in scr, tactic (weakly) associated with tac_ *)
3.25 - (Tactic_Def.T * (* (for generate) *)
3.26 + (Tactic.T * (* (for generate) *)
3.27 Env.T * (* with 'tactic=result' as rule, tactic ev. _not_ ready for 'parallel let' *)
3.28 Env.T * (* with results of (ready) tacs *)
3.29 term * (* itr_arg of tactic, for upd. env at Repeat, Try *)
3.30 @@ -182,7 +182,7 @@
3.31 list;
3.32
3.33 fun ets2s (l,(m,eno,env,iar,res,s)) =
3.34 - "\n(" ^ Celem.path2str l ^ ",(" ^ Tactic_Def.string_of m ^
3.35 + "\n(" ^ Celem.path2str l ^ ",(" ^ Tactic.string_of m ^
3.36 ",\n ens= " ^ Env.subst2str eno ^
3.37 ",\n env= " ^ Env.subst2str env ^
3.38 ",\n iar= " ^ Rule.term2str iar ^
3.39 @@ -200,7 +200,7 @@
3.40 PrfObj of
3.41 {cell : Celem.lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *)
3.42 form : term, (* where tac is applied to *)
3.43 - tac : Tactic_Def.input, (* also in istate *)
3.44 + tac : Tactic.input, (* also in istate *)
3.45 loc : (Istate_Def.T * (* script interpreter state *)
3.46 Proof.context) (* context for provers, type inference *)
3.47 option * (* both for interpreter location on Frm, Pbl, Met *)
3.48 @@ -333,7 +333,7 @@
3.49 | g_loc (PrfObj {loc = l, ...}) = l;
3.50 fun g_branch (PblObj {branch = b, ...}) = b
3.51 | g_branch (PrfObj {branch = b, ...}) = b;
3.52 -fun g_tac (PblObj {spec = (_, _, m),...}) = Tactic_Def.Apply_Method m
3.53 +fun g_tac (PblObj {spec = (_, _, m),...}) = Tactic.Apply_Method m
3.54 | g_tac (PrfObj {tac = m, ...}) = m;
3.55 fun g_result (PblObj {result = r, ...}) = r
3.56 | g_result (PrfObj {result = r, ...}) = r;
3.57 @@ -415,8 +415,8 @@
3.58 if is_pblobj (get_obj I pt p)
3.59 then (true, p, Rule.Erls)
3.60 else case get_obj g_tac pt p of
3.61 - Tactic_Def.Rewrite_Set rls' => (false, p, assoc_rls rls')
3.62 - | Tactic_Def.Rewrite_Set_Inst (_, rls') => (false, p, assoc_rls rls')
3.63 + Tactic.Rewrite_Set rls' => (false, p, assoc_rls rls')
3.64 + | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, assoc_rls rls')
3.65 | _ => par pt (lev_up p)
3.66 in par pt (lev_up p) end;
3.67
4.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Tue Dec 17 17:19:34 2019 +0100
4.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Tue Dec 17 17:52:48 2019 +0100
4.3 @@ -9,10 +9,98 @@
4.4 *)
4.5 signature TACTIC =
4.6 sig
4.7 - datatype T = datatype Tactic_Def.T
4.8 + datatype T =
4.9 + Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
4.10 + | Add_Relation' of Rule.cterm' * Model.itm list
4.11 + | Apply_Assumption' of term list * term
4.12 + | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
4.13 +
4.14 + | Begin_Sequ' | Begin_Trans' of term
4.15 + | Split_And' of term | Split_Or' of term | Split_Intersect' of term
4.16 + | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
4.17 + | End_Sequ' | End_Trans' of Selem.result
4.18 + | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
4.19 +
4.20 + | CAScmd' of term
4.21 + | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
4.22 + | Check_Postcond' of Celem.pblID * Selem.result
4.23 + | Check_elementwise' of term * Rule.cterm' * Selem.result
4.24 + | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
4.25 +
4.26 + | Derive' of Rule.rls
4.27 + | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
4.28 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
4.29 + | End_Detail' of Selem.result
4.30 +
4.31 + | Empty_Tac_
4.32 + | Free_Solve'
4.33 +
4.34 + | Init_Proof' of Rule.cterm' list * Celem.spec
4.35 + | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
4.36 + | Or_to_List' of term * term
4.37 + | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
4.38 + | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
4.39 +
4.40 + | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
4.41 + | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
4.42 + | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
4.43 + | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
4.44 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
4.45 +
4.46 + | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
4.47 + | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
4.48 + | Specify_Theory' of Rule.domID
4.49 + | Subproblem' of Celem.spec * Model.ori list * term * Selem.fmz_ * Proof.context * term
4.50 + | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
4.51 + | Tac_ of theory * string * string * string
4.52 + | Take' of term | Take_Inst' of term
4.53 val string_of : T -> string
4.54
4.55 - datatype input = datatype Tactic_Def.input
4.56 + datatype input =
4.57 + Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
4.58 + | Apply_Assumption of Rule.cterm' list
4.59 + | Apply_Method of Celem.metID
4.60 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
4.61 + | Begin_Sequ | Begin_Trans
4.62 + | Split_And | Split_Or | Split_Intersect
4.63 + | Conclude_And | Conclude_Or | Collect_Trues
4.64 + | End_Sequ | End_Trans
4.65 + | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
4.66 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
4.67 + | CAScmd of Rule.cterm'
4.68 + | Calculate of string
4.69 + | Check_Postcond of Celem.pblID
4.70 + | Check_elementwise of Rule.cterm'
4.71 + | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
4.72 +
4.73 + | Derive of Rule.rls'
4.74 + | Detail_Set of Rule.rls'
4.75 + | Detail_Set_Inst of Selem.subs * Rule.rls'
4.76 + | End_Detail
4.77 +
4.78 + | Empty_Tac
4.79 + | Free_Solve
4.80 +
4.81 + | Init_Proof of Rule.cterm' list * Celem.spec
4.82 + | Model_Problem
4.83 + | Or_to_List
4.84 + | Refine_Problem of Celem.pblID
4.85 + | Refine_Tacitly of Celem.pblID
4.86 +
4.87 + | Rewrite of Celem.thm''
4.88 + | Rewrite_Asm of Celem.thm''
4.89 + | Rewrite_Inst of Selem.subs * Celem.thm''
4.90 + | Rewrite_Set of Rule.rls'
4.91 + | Rewrite_Set_Inst of Selem.subs * Rule.rls'
4.92 +
4.93 + | Specify_Method of Celem.metID
4.94 + | Specify_Problem of Celem.pblID
4.95 + | Specify_Theory of Rule.domID
4.96 + | Subproblem of Rule.domID * Celem.pblID
4.97 +
4.98 + | Substitute of Selem.sube
4.99 + | Tac of string
4.100 + | Take of Rule.cterm' | Take_Inst of Rule.cterm'
4.101 val tac2str : input -> string
4.102
4.103 val eq_tac : input * input -> bool
4.104 @@ -50,11 +138,112 @@
4.105 initacs start with a formula different from the preceding formula.
4.106 see 'type tac_' for the internal representation of tactics
4.107 *)
4.108 -datatype input = datatype Tactic_Def.input
4.109 +datatype input =
4.110 + Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
4.111 + | Apply_Assumption of Rule.cterm' list
4.112 + | Apply_Method of Celem.metID
4.113 + (* creates an "istate" in PblObj.env; in case of "init_form"
4.114 + creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
4.115 + a "SOME istate" at fst of "loc".
4.116 + As each step (in the solve-phase) has a resulting formula (at the front-end)
4.117 + Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *)
4.118 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
4.119 + | Begin_Sequ | Begin_Trans
4.120 + | Split_And | Split_Or | Split_Intersect
4.121 + | Conclude_And | Conclude_Or | Collect_Trues
4.122 + | End_Sequ | End_Trans
4.123 + | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
4.124 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
4.125 + | CAScmd of Rule.cterm'
4.126 + | Calculate of string
4.127 + | Check_Postcond of Celem.pblID
4.128 + | Check_elementwise of Rule.cterm'
4.129 + | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
4.130
4.131 -val tac2str = Tactic_Def.tac2str
4.132 + | Derive of Rule.rls' (* WN0509 drop *)
4.133 + | Detail_Set of Rule.rls' (* WN0509 drop *)
4.134 + | Detail_Set_Inst of Selem.subs * Rule.rls' (* WN0509 drop *)
4.135 + | End_Detail (* WN0509 drop *)
4.136
4.137 -val is_empty_tac = Tactic_Def.is_empty_tac
4.138 + | Empty_Tac
4.139 + | Free_Solve
4.140 +
4.141 + | Init_Proof of Rule.cterm' list * Celem.spec
4.142 + | Model_Problem
4.143 + | Or_to_List
4.144 + | Refine_Problem of Celem.pblID
4.145 + | Refine_Tacitly of Celem.pblID
4.146 +
4.147 + (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
4.148 + because there all the thms are present with both (thmID, thm)
4.149 + (where user-views can show both or only one of (thmID, thm)),
4.150 + and thm is created from ThmID by assoc_thm'' when entering isabisac *)
4.151 + | Rewrite of Celem.thm''
4.152 + | Rewrite_Asm of Celem.thm''
4.153 + | Rewrite_Inst of Selem.subs * Celem.thm''
4.154 + | Rewrite_Set of Rule.rls'
4.155 + | Rewrite_Set_Inst of Selem.subs * Rule.rls'
4.156 +
4.157 + | Specify_Method of Celem.metID
4.158 + | Specify_Problem of Celem.pblID
4.159 + | Specify_Theory of Rule.domID
4.160 + | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
4.161 +
4.162 + | Substitute of Selem.sube
4.163 + | Tac of string (* WN0509 drop *)
4.164 + | Take of Rule.cterm' | Take_Inst of Rule.cterm'
4.165 +
4.166 +fun tac2str ma = case ma of
4.167 + Init_Proof (ppc, spec) =>
4.168 + "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec))
4.169 + | Model_Problem => "Model_Problem "
4.170 + | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
4.171 + | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
4.172 + | Add_Given cterm' => "Add_Given " ^ cterm'
4.173 + | Del_Given cterm' => "Del_Given " ^ cterm'
4.174 + | Add_Find cterm' => "Add_Find " ^ cterm'
4.175 + | Del_Find cterm' => "Del_Find " ^ cterm'
4.176 + | Add_Relation cterm' => "Add_Relation " ^ cterm'
4.177 + | Del_Relation cterm' => "Del_Relation " ^ cterm'
4.178 +
4.179 + | Specify_Theory domID => "Specify_Theory " ^ quote domID
4.180 + | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
4.181 + | Specify_Method metID => "Specify_Method " ^ strs2str metID
4.182 + | Apply_Method metID => "Apply_Method " ^ strs2str metID
4.183 + | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
4.184 + | Free_Solve => "Free_Solve"
4.185 +
4.186 + | Rewrite_Inst (subs, (id, thm)) =>
4.187 + "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str)))
4.188 + | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
4.189 + | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
4.190 + | Rewrite_Set_Inst (subs, rls) =>
4.191 + "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
4.192 + | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
4.193 + | Detail_Set rls => "Detail_Set " ^ quote rls
4.194 + | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
4.195 + | End_Detail => "End_Detail"
4.196 + | Derive rls' => "Derive " ^ rls'
4.197 + | Calculate op_ => "Calculate " ^ op_
4.198 + | Substitute sube => "Substitute " ^ Selem.sube2str sube
4.199 + | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
4.200 +
4.201 + | Take cterm' => "Take " ^ quote cterm'
4.202 + | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
4.203 + | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
4.204 + | End_Subproblem => "End_Subproblem"
4.205 + | CAScmd cterm' => "CAScmd " ^ quote cterm'
4.206 +
4.207 + | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
4.208 + | Or_to_List => "Or_to_List "
4.209 + | Collect_Trues => "Collect_Trues"
4.210 +
4.211 + | Empty_Tac => "Empty_Tac"
4.212 + | Tac string => "Tac " ^ string
4.213 + | End_Proof' => "input End_Proof'"
4.214 + | _ => "tac2str not impl. for ?!";
4.215 +
4.216 +fun is_empty_tac input = case input of Empty_Tac => true | _ => false
4.217
4.218 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
4.219 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
4.220 @@ -142,9 +331,126 @@
4.221 and re-calculate result if t<>t'
4.222 TODO.WN161219: replace *every* cterm' by term
4.223 *)
4.224 - datatype T = datatype Tactic_Def.T
4.225 + datatype T =
4.226 + Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
4.227 + | Add_Relation' of Rule.cterm' * Model.itm list
4.228 + | Apply_Assumption' of term list * term
4.229 + | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
4.230 + (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
4.231 + | Begin_Sequ' | Begin_Trans' of term
4.232 + | Split_And' of term | Split_Or' of term | Split_Intersect' of term
4.233 + | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
4.234 + | End_Sequ' | End_Trans' of Selem.result
4.235 + | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
4.236 + (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
4.237 + | CAScmd' of term
4.238 + | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
4.239 + | Check_Postcond' of Celem.pblID *
4.240 + Selem.result (* returnvalue of script in solve *)
4.241 + | Check_elementwise' of (*special case:*)
4.242 + term * (* (1) the current formula: [x=1,x=...] *)
4.243 + string * (* (2) the pred from Check_elementwise *)
4.244 + Selem.result (* (3) composed from (1) and (2): {x. pred} *)
4.245 + | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
4.246
4.247 -val string_of = Tactic_Def.string_of
4.248 + | Derive' of Rule.rls
4.249 + | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
4.250 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
4.251 + | End_Detail' of Selem.result
4.252 +
4.253 + | Empty_Tac_
4.254 + | Free_Solve'
4.255 +
4.256 + | Init_Proof' of Rule.cterm' list * Celem.spec
4.257 + | Model_Problem' of Celem.pblID *
4.258 + Model.itm list * (* the 'untouched' pbl *)
4.259 + Model.itm list (* the casually completed met *)
4.260 + | Or_to_List' of term * term
4.261 + | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
4.262 + | Refine_Tacitly' of
4.263 + Celem.pblID * (* input*)
4.264 + Celem.pblID * (* the refined from applicable_in *)
4.265 + Rule.domID * (* from new pbt?! filled in specify *)
4.266 + Celem.metID * (* from new pbt?! filled in specify *)
4.267 + Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
4.268 + | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
4.269 + | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
4.270 + | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
4.271 + | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
4.272 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
4.273 +
4.274 + | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
4.275 + | Specify_Problem' of Celem.pblID *
4.276 + (bool * (* matches *)
4.277 + (Model.itm list * (* ppc *)
4.278 + (bool * term) list)) (* preconditions *)
4.279 + | Specify_Theory' of Rule.domID
4.280 + | Subproblem' of
4.281 + Celem.spec *
4.282 + (Model.ori list) * (* filled in associate Subproblem' *)
4.283 + term * (* filled -"-, headline of calc-head *)
4.284 + Selem.fmz_ *
4.285 + Proof.context * (* DEPRECATED shifted into loc for all ppobj *)
4.286 + term (* Subproblem (thyID, pbl) OR cascmd *)
4.287 + | Substitute' of
4.288 + Rule.rew_ord_ * (* for re-calculation *)
4.289 + Rule.rls * (* for re-calculation *)
4.290 + Selem.subte * (* the 'substitution': terms of type bool *)
4.291 + term * (* to be substituted into *)
4.292 + term (* resulting from the substitution *)
4.293 + | Tac_ of theory * string * string * string
4.294 + | Take' of term | Take_Inst' of term
4.295 +
4.296 +fun string_of ma = case ma of
4.297 + Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
4.298 + | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
4.299 + | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
4.300 + strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
4.301 + | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
4.302 + | Add_Given' _ => "Add_Given' "(*^cterm'*)
4.303 + | Del_Given' _ => "Del_Given' "(*^cterm'*)
4.304 + | Add_Find' _ => "Add_Find' "(*^cterm'*)
4.305 + | Del_Find' _ => "Del_Find' "(*^cterm'*)
4.306 + | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
4.307 + | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
4.308 +
4.309 + | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
4.310 + | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
4.311 + spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
4.312 + | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
4.313 + Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
4.314 +
4.315 + | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
4.316 + | Check_Postcond' (pblID, (scval, asm)) => "Check_Postcond' " ^
4.317 + (spair2str (strs2str pblID, spair2str (Rule.term2str scval, Rule.terms2str asm)))
4.318 +
4.319 + | Free_Solve' => "Free_Solve'"
4.320 +
4.321 + | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
4.322 + | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
4.323 + | Rewrite_Asm' _(*thm'*) => "Rewrite_Asm' "(*^(spair2str thm')*)
4.324 + | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
4.325 + | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
4.326 + "," ^ Rule.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
4.327 + | End_Detail' _ => "End_Detail' xxx"
4.328 + | Detail_Set' _ => "Detail_Set' xxx"
4.329 + | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
4.330 +
4.331 + | Derive' rls => "Derive' " ^ Rule.id_rls rls
4.332 + | Calculate' _ => "Calculate' "
4.333 + | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
4.334 + | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*)
4.335 +
4.336 + | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
4.337 + | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*)
4.338 + | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
4.339 + "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
4.340 + | End_Subproblem' _ => "End_Subproblem'"
4.341 + | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
4.342 +
4.343 + | Empty_Tac_ => "Empty_Tac_"
4.344 + | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
4.345 + | _ => "string_of not impl. for arg";
4.346
4.347 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
4.348 | input_from_T (Model_Problem' (_, _, _)) = Model_Problem
5.1 --- a/src/Tools/isac/TODO.thy Tue Dec 17 17:19:34 2019 +0100
5.2 +++ b/src/Tools/isac/TODO.thy Tue Dec 17 17:52:48 2019 +0100
5.3 @@ -78,10 +78,9 @@
5.4 \item xxx
5.5 \item re-organise code for Interpret
5.6 \begin{itemize}
5.7 - \item Applicable.applicable_in --> ?Step?.applicable
5.8 - TRIED: Applicable.applicable_in --> Tactic.applicable, stopped because
5.9 - Tactic.T --> Ctree_Basic.tactic would separated !long! def. from code
5.10 - (tactic.sml evaluated BEFPRE ctree)
5.11 + \item Applicable.applicable_in --> ?Step_Specify?.applicable
5.12 + TRIED: separated tactic.sml | tactic-def.sml, shifted tactic.sml after ctree
5.13 + copy appl.sml into tactic.sml shows: need much of Specify
5.14 \item istate
5.15 \begin{itemize}
5.16 \item Istate.init with Specify.hack_until_reorg