1.1 --- a/src/Tools/isac/Interpret/solve-step.sml Fri May 01 16:06:59 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Fri May 01 17:17:41 2020 +0200
1.3 @@ -24,12 +24,87 @@
1.4 check tactics (input by the user, mostly) for applicability
1.5 and determine as much of the result of the tactic as possible initially.
1.6 *)
1.7 -fun check (Tactic.Check_Postcond pI) (_, (p, p_)) =
1.8 +fun check (Tactic.CAScmd ct') _ =
1.9 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct'))
1.10 + | check (m as Tactic.Calculate op_) (pt, (p, p_)) =
1.11 + if member op = [Pos.Pbl, Pos.Met] p_
1.12 + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
1.13 + else
1.14 + let
1.15 + val (msg,thy',isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
1.16 + val f = case p_ of
1.17 + Frm => Ctree.get_obj Ctree.g_form pt p
1.18 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.19 + | _ => raise ERROR ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.20 + in
1.21 + if msg = "OK"
1.22 + then
1.23 + case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
1.24 + SOME (f', (id, thm))
1.25 + => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
1.26 + | NONE => Applicable.No ("'calculate "^op_^"' not applicable")
1.27 + else Applicable.No msg
1.28 + end
1.29 + | check (Tactic.Check_Postcond pI) (_, (p, p_)) =
1.30 if member op = [Pos.Pbl, Pos.Met] p_
1.31 then Applicable.No ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.32 else Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
1.33 - | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
1.34 + | check (m as Tactic.Check_elementwise pred) (pt, (p, p_)) =
1.35 + if member op = [Pos.Pbl, Pos.Met] p_
1.36 + then Applicable.No ((Tactic.input_to_string m) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.37 + else
1.38 + let
1.39 + val pp = Ctree.par_pblobj pt p;
1.40 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.41 + val thy = ThyC.get_theory thy'
1.42 + val metID = (Ctree.get_obj Ctree.g_metID pt pp)
1.43 + val {crls, ...} = Specify.get_met metID
1.44 + val (f, asm) = case p_ of
1.45 + Frm => (Ctree.get_obj Ctree.g_form pt p , [])
1.46 + | Pos.Res => Ctree.get_obj Ctree.g_result pt p
1.47 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.48 + val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> ApplicableOLD.mk_set thy pt p f;
1.49 + in
1.50 + Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm)))
1.51 + end
1.52 +(*RM* )| Derive of Rule_Set.id( *RM*)
1.53 + | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
1.54 | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve') (* always applicable *)
1.55 + | check (Tactic.Apply_Assumption cts') _ =
1.56 + raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
1.57 + (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)
1.58 + | check Tactic.Or_to_List (pt, (p, p_)) =
1.59 + if member op = [Pos.Pbl, Pos.Met] p_
1.60 + then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_)))
1.61 + else
1.62 + let
1.63 + val f = case p_ of
1.64 + Frm => Ctree.get_obj Ctree.g_form pt p
1.65 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.66 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.67 + in (let val ls = Prog_Expr.or2list f
1.68 + in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end)
1.69 + handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f)
1.70 + end
1.71 + | check (m as Tactic.Rewrite thm'') (pt, (p, p_)) =
1.72 + if member op = [Pos.Pbl, Pos.Met] p_
1.73 + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
1.74 + else
1.75 + let
1.76 + val (msg, thy', ro, rls', _)= ApplicableOLD.from_pblobj_or_detail_thm thm'' p pt;
1.77 + val thy = ThyC.get_theory thy';
1.78 + val f = case p_ of
1.79 + Frm => Ctree.get_obj Ctree.g_form pt p
1.80 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.81 + | _ => error ("Solve_Step.check Rewrite: call by " ^ Pos.pos'2str (p, p_));
1.82 + in
1.83 + if msg = "OK"
1.84 + then
1.85 + case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of
1.86 + SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
1.87 + | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable")
1.88 + else Applicable.No msg
1.89 + end
1.90 | check (m as Tactic.Rewrite_Inst (subs, thm'')) (pt, (p, p_)) =
1.91 if member op = [Pos.Pbl, Pos.Met] p_
1.92 then Applicable.No ((Tactic.input_to_string m)^" not for pos " ^ Pos.pos'2str (p, p_))
1.93 @@ -54,43 +129,22 @@
1.94 end
1.95 handle _ => Applicable.No ("syntax error in "^(subs2str subs))
1.96 end
1.97 - | check (m as Tactic.Rewrite thm'') (pt, (p, p_)) =
1.98 + | check (m as Tactic.Rewrite_Set rls) (pt, (p, p_)) =
1.99 if member op = [Pos.Pbl, Pos.Met] p_
1.100 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
1.101 - else
1.102 - let
1.103 - val (msg, thy', ro, rls', _)= ApplicableOLD.from_pblobj_or_detail_thm thm'' p pt;
1.104 - val thy = ThyC.get_theory thy';
1.105 - val f = case p_ of
1.106 - Frm => Ctree.get_obj Ctree.g_form pt p
1.107 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.108 - | _ => error ("Solve_Step.check Rewrite: call by " ^ Pos.pos'2str (p, p_));
1.109 - in
1.110 - if msg = "OK"
1.111 - then
1.112 - case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of
1.113 - SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
1.114 - | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable")
1.115 - else Applicable.No msg
1.116 - end
1.117 - | check (m as Tactic.Detail_Set_Inst (subs, rls)) (pt, (p, p_)) =
1.118 - if member op = [Pos.Pbl, Pos.Met] p_
1.119 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
1.120 + then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.121 else
1.122 let
1.123 - val pp = Ctree.par_pblobj pt p;
1.124 + val pp = Ctree.par_pblobj pt p;
1.125 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.126 - val thy = ThyC.get_theory thy';
1.127 - val f = case p_ of Frm => Ctree.get_obj Ctree.g_form pt p
1.128 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.129 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.130 - val subst = Subst.T_from_input thy subs
1.131 - in
1.132 - case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
1.133 + val (f, _) = case p_ of
1.134 + Frm => (Ctree.get_obj Ctree.g_form pt p, p)
1.135 + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
1.136 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.137 + in
1.138 + case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
1.139 SOME (f', asm)
1.140 - => Applicable.Yes (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
1.141 - | NONE => Applicable.No (rls ^ " not applicable")
1.142 - handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
1.143 + => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
1.144 + | NONE => Applicable.No (rls ^ " not applicable")
1.145 end
1.146 | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (pt, (p, p_)) =
1.147 if member op = [Pos.Pbl, Pos.Met] p_
1.148 @@ -112,59 +166,13 @@
1.149 | NONE => Applicable.No (rls ^ " not applicable")
1.150 handle _ => Applicable.No ("syntax error in " ^(subs2str subs))
1.151 end
1.152 - | check (m as Tactic.Rewrite_Set rls) (pt, (p, p_)) =
1.153 - if member op = [Pos.Pbl, Pos.Met] p_
1.154 - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.155 - else
1.156 - let
1.157 - val pp = Ctree.par_pblobj pt p;
1.158 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.159 - val (f, _) = case p_ of
1.160 - Frm => (Ctree.get_obj Ctree.g_form pt p, p)
1.161 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
1.162 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.163 - in
1.164 - case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
1.165 - SOME (f', asm)
1.166 - => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
1.167 - | NONE => Applicable.No (rls ^ " not applicable")
1.168 - end
1.169 - | check (m as Tactic.Detail_Set rls) (pt, (p, p_)) =
1.170 - if member op = [Pos.Pbl, Pos.Met] p_
1.171 - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.172 - else
1.173 - let
1.174 - val pp = Ctree.par_pblobj pt p
1.175 - val thy' = Ctree.get_obj Ctree.g_domID pt pp
1.176 - val f = case p_ of
1.177 - Frm => Ctree.get_obj Ctree.g_form pt p
1.178 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.179 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.180 - in
1.181 - case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
1.182 - SOME (f',asm) => Applicable.Yes (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
1.183 - | NONE => Applicable.No (rls^" not applicable")
1.184 - end
1.185 - | check Tactic.End_Ruleset _ = raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset)
1.186 - | check (m as Tactic.Calculate op_) (pt, (p, p_)) =
1.187 - if member op = [Pos.Pbl, Pos.Met] p_
1.188 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
1.189 - else
1.190 - let
1.191 - val (msg,thy',isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
1.192 - val f = case p_ of
1.193 - Frm => Ctree.get_obj Ctree.g_form pt p
1.194 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.195 - | _ => raise ERROR ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.196 - in
1.197 - if msg = "OK"
1.198 - then
1.199 - case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
1.200 - SOME (f', (id, thm))
1.201 - => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
1.202 - | NONE => Applicable.No ("'calculate "^op_^"' not applicable")
1.203 - else Applicable.No msg
1.204 - end
1.205 + | check (m as Tactic.Subproblem (domID, pblID)) (_, (p, p_)) =
1.206 + if Pos.on_specification p_
1.207 + then
1.208 + Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.209 + else (*some fields filled later in LI*)
1.210 + Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
1.211 + TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
1.212 (*Substitute combines two different kind of "substitution":
1.213 (1) subst_atomic: for ?a..?z
1.214 (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
1.215 @@ -196,85 +204,6 @@
1.216 SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
1.217 | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
1.218 end
1.219 - | check (Tactic.Apply_Assumption cts') _ =
1.220 - raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
1.221 - (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)
1.222 - | check (Tactic.Take_Inst ct') _ =
1.223 - raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct'))
1.224 - | check (m as Tactic.Subproblem (domID, pblID)) (_, (p, p_)) =
1.225 - if Pos.on_specification p_
1.226 - then
1.227 - Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.228 - else (*some fields filled later in LI*)
1.229 - Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
1.230 - TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
1.231 - | check (Tactic.End_Subproblem) _ =
1.232 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)
1.233 - | check (Tactic.CAScmd ct') _ =
1.234 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct'))
1.235 - | check (Tactic.Split_And) _ =
1.236 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_And)
1.237 - | check (Tactic.Conclude_And) _ =
1.238 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And)
1.239 - | check (Tactic.Split_Or) _ =
1.240 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or)
1.241 - | check (Tactic.Conclude_Or) _ =
1.242 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or)
1.243 - | check (Tactic.Begin_Trans) (pt, (p, p_)) =
1.244 - let
1.245 - val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
1.246 - Pos.Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p)
1.247 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, (Pos.lev_on o Pos.lev_dn o Pos.lev_on) p)
1.248 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.249 - in (Applicable.Yes (Tactic.Begin_Trans' f))
1.250 - handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'")
1.251 - end
1.252 - | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
1.253 - if p_ = Pos.Res
1.254 - then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
1.255 - else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"
1.256 - | check (Tactic.Begin_Sequ) _ =
1.257 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ))
1.258 - | check (Tactic.End_Sequ) _ =
1.259 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ))
1.260 - | check (Tactic.Split_Intersect) _ =
1.261 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect))
1.262 - | check (Tactic.End_Intersect) _ =
1.263 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect))
1.264 - | check (m as Tactic.Check_elementwise pred) (pt, (p, p_)) =
1.265 - if member op = [Pos.Pbl, Pos.Met] p_
1.266 - then Applicable.No ((Tactic.input_to_string m) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.267 - else
1.268 - let
1.269 - val pp = Ctree.par_pblobj pt p;
1.270 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.271 - val thy = ThyC.get_theory thy'
1.272 - val metID = (Ctree.get_obj Ctree.g_metID pt pp)
1.273 - val {crls, ...} = Specify.get_met metID
1.274 - val (f, asm) = case p_ of
1.275 - Frm => (Ctree.get_obj Ctree.g_form pt p , [])
1.276 - | Pos.Res => Ctree.get_obj Ctree.g_result pt p
1.277 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.278 - val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> ApplicableOLD.mk_set thy pt p f;
1.279 - in
1.280 - Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm)))
1.281 - end
1.282 - | check Tactic.Or_to_List (pt, (p, p_)) =
1.283 - if member op = [Pos.Pbl, Pos.Met] p_
1.284 - then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_)))
1.285 - else
1.286 - let
1.287 - val f = case p_ of
1.288 - Frm => Ctree.get_obj Ctree.g_form pt p
1.289 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.290 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.291 - in (let val ls = Prog_Expr.or2list f
1.292 - in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end)
1.293 - handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f)
1.294 - end
1.295 - | check Tactic.Collect_Trues _ =
1.296 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues)
1.297 - | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
1.298 | check (Tactic.Tac id) (pt, (p, p_)) =
1.299 let
1.300 val pp = Ctree.par_pblobj pt p;
1.301 @@ -301,10 +230,80 @@
1.302 end
1.303 | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
1.304 end
1.305 + | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
1.306 +(*RM*)| check (Tactic.Take_Inst ct') _ =
1.307 + raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct'))
1.308 +(*RM*)| check (Tactic.Begin_Sequ) _ =
1.309 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ))
1.310 + | check (Tactic.Begin_Trans) (pt, (p, p_)) =
1.311 + let
1.312 + val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
1.313 + Pos.Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p)
1.314 + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, (Pos.lev_on o Pos.lev_dn o Pos.lev_on) p)
1.315 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.316 + in (Applicable.Yes (Tactic.Begin_Trans' f))
1.317 + handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'")
1.318 + end
1.319 + | check (Tactic.Split_And) _ =
1.320 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_And)
1.321 + | check (Tactic.Split_Or) _ =
1.322 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or)
1.323 + | check (Tactic.Split_Intersect) _ =
1.324 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect))
1.325 + | check (Tactic.Conclude_And) _ =
1.326 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And)
1.327 + | check (Tactic.Conclude_Or) _ =
1.328 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or)
1.329 + | check Tactic.Collect_Trues _ =
1.330 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues)
1.331 + | check (Tactic.End_Sequ) _ =
1.332 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ))
1.333 + | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
1.334 + if p_ = Pos.Res
1.335 + then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
1.336 + else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"
1.337 + | check Tactic.End_Ruleset _ = raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset)
1.338 + | check (Tactic.End_Subproblem) _ =
1.339 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)
1.340 + | check (Tactic.End_Intersect) _ =
1.341 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect))
1.342 + | check (m as Tactic.Detail_Set rls) (pt, (p, p_)) =
1.343 + if member op = [Pos.Pbl, Pos.Met] p_
1.344 + then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.345 + else
1.346 + let
1.347 + val pp = Ctree.par_pblobj pt p
1.348 + val thy' = Ctree.get_obj Ctree.g_domID pt pp
1.349 + val f = case p_ of
1.350 + Frm => Ctree.get_obj Ctree.g_form pt p
1.351 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.352 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.353 + in
1.354 + case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
1.355 + SOME (f',asm) => Applicable.Yes (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
1.356 + | NONE => Applicable.No (rls^" not applicable")
1.357 + end
1.358 + | check (m as Tactic.Detail_Set_Inst (subs, rls)) (pt, (p, p_)) =
1.359 + if member op = [Pos.Pbl, Pos.Met] p_
1.360 + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
1.361 + else
1.362 + let
1.363 + val pp = Ctree.par_pblobj pt p;
1.364 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.365 + val thy = ThyC.get_theory thy';
1.366 + val f = case p_ of Frm => Ctree.get_obj Ctree.g_form pt p
1.367 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.368 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.369 + val subst = Subst.T_from_input thy subs
1.370 + in
1.371 + case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
1.372 + SOME (f', asm)
1.373 + => Applicable.Yes (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
1.374 + | NONE => Applicable.No (rls ^ " not applicable")
1.375 + handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
1.376 + end
1.377 +(*RM* )| End_Detail( *RM*)
1.378 | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
1.379 | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
1.380 -(*-----^^^^^- solve ---------------------------------------------------------------------------*)
1.381 -
1.382 -
1.383
1.384 (**)end(**);
2.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Fri May 01 16:06:59 2020 +0200
2.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Fri May 01 17:17:41 2020 +0200
2.3 @@ -13,41 +13,28 @@
2.4 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
2.5 | Add_Relation' of TermC.as_string * Model.itm list
2.6 | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
2.7 -
2.8 - | Begin_Sequ' | Begin_Trans' of term
2.9 - | Split_And' of term | Split_Or' of term | Split_Intersect' of term
2.10 - | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
2.11 - | End_Sequ' | End_Trans' of Selem.result
2.12 - | End_Ruleset' of term | End_Intersect' of term | End_Proof''
2.13 -
2.14 + | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
2.15 + | Init_Proof' of TermC.as_string list * Spec.T
2.16 + | Model_Problem' of Problem.id * Model.itm list * Model.itm list
2.17 + | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
2.18 + | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
2.19 + | Specify_Method' of Method.id * Model.ori list * Model.itm list
2.20 + | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
2.21 + | Specify_Theory' of ThyC.id
2.22 + (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
2.23 | CAScmd' of term
2.24 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
2.25 | Check_Postcond' of Problem.id * term
2.26 | Check_elementwise' of term * TermC.as_string * Selem.result
2.27 - | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
2.28 -
2.29 - | Derive' of Rule_Set.T
2.30 - | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
2.31 - | Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
2.32 - | End_Detail' of Selem.result
2.33 -
2.34 +(*RM*)| Derive' of Rule_Set.T
2.35 | Empty_Tac_
2.36 | Free_Solve'
2.37 -
2.38 - | Init_Proof' of TermC.as_string list * Spec.T
2.39 - | Model_Problem' of Problem.id * Model.itm list * Model.itm list
2.40 +(*RM* )| Apply_Assumption of TermC.as_string list( *RM*)
2.41 | Or_to_List' of term * term
2.42 - | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
2.43 - | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
2.44 -
2.45 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
2.46 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
2.47 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
2.48 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
2.49 -
2.50 - | Specify_Method' of Method.id * Model.ori list * Model.itm list
2.51 - | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
2.52 - | Specify_Theory' of ThyC.id
2.53 | Subproblem' of
2.54 Spec.T * Model.ori list *
2.55 term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
2.56 @@ -56,54 +43,61 @@
2.57 Proof.context * (* derived from prog. in ??? *)
2.58 term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
2.59 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
2.60 - | Tac_ of theory * string * string * string
2.61 +(*RM*)| Tac_ of theory * string * string * string
2.62 | Take' of term
2.63 +(*RM* )| Take_Inst of TermC.as_string( *RM*)
2.64 +(*RM*)| Begin_Sequ' | Begin_Trans' of term
2.65 +(*RM*)| Split_And' of term | Split_Or' of term | Split_Intersect' of term
2.66 +(*RM*)| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
2.67 +(*RM*)| End_Sequ' | End_Trans' of Selem.result
2.68 +(*RM*)| End_Ruleset' of term | End_Intersect' of term | End_Proof''
2.69 +(*RM*)| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
2.70 +(*RM*)| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
2.71 +(*RM*)| End_Detail' of Selem.result;
2.72 +
2.73 val string_of: T -> string
2.74
2.75 datatype input =
2.76 - Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
2.77 - | Apply_Assumption of TermC.as_string list
2.78 + Add_Find of TermC.as_string | Add_Given of TermC.as_string
2.79 + | Add_Relation of TermC.as_string
2.80 | Apply_Method of Method.id
2.81 - (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
2.82 - | Begin_Sequ | Begin_Trans
2.83 - | Split_And | Split_Or | Split_Intersect
2.84 - | Conclude_And | Conclude_Or | Collect_Trues
2.85 - | End_Sequ | End_Trans
2.86 - | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
2.87 - (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
2.88 + | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
2.89 + | Init_Proof of TermC.as_string list * Spec.T
2.90 + | Model_Problem
2.91 + | Refine_Problem of Problem.id
2.92 + | Refine_Tacitly of Problem.id
2.93 + | Specify_Method of Method.id
2.94 + | Specify_Problem of Problem.id
2.95 + | Specify_Theory of ThyC.id
2.96 + (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
2.97 | CAScmd of TermC.as_string
2.98 | Calculate of string
2.99 | Check_Postcond of Problem.id
2.100 | Check_elementwise of TermC.as_string
2.101 - | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
2.102 -
2.103 - | Derive of Rule_Set.id
2.104 - | Detail_Set of Rule_Set.id
2.105 - | Detail_Set_Inst of Subst.input * Rule_Set.id
2.106 - | End_Detail
2.107 -
2.108 +(*RM*)| Derive of Rule_Set.id(*RM*)
2.109 | Empty_Tac
2.110 - | Free_Solve
2.111 -
2.112 - | Init_Proof of TermC.as_string list * Spec.T
2.113 - | Model_Problem
2.114 +(*RM*)| Free_Solve
2.115 +(*RM*)| Apply_Assumption of TermC.as_string list
2.116 | Or_to_List
2.117 - | Refine_Problem of Problem.id
2.118 - | Refine_Tacitly of Problem.id
2.119 -
2.120 | Rewrite of ThmC.T
2.121 | Rewrite_Inst of Subst.input * ThmC.T
2.122 | Rewrite_Set of Rule_Set.id
2.123 | Rewrite_Set_Inst of Subst.input * Rule_Set.id
2.124 + | Subproblem of ThyC.id * Problem.id
2.125 + | Substitute of Subst.input
2.126 +(*RM*)| Tac of string
2.127 + | Take of TermC.as_string
2.128 +(*RM*)| Take_Inst of TermC.as_string
2.129 +(*RM*)| Begin_Sequ | Begin_Trans
2.130 +(*RM*)| Split_And | Split_Or | Split_Intersect
2.131 +(*RM*)| Conclude_And | Conclude_Or | Collect_Trues
2.132 +(*RM*)| End_Sequ | End_Trans
2.133 +(*RM*)| End_Ruleset | End_Subproblem | End_Intersect
2.134 +(*RM*)| Detail_Set of Rule_Set.id
2.135 +(*RM*)| Detail_Set_Inst of Subst.input * Rule_Set.id
2.136 +(*RM*)| End_Detail
2.137 + | End_Proof';
2.138
2.139 - | Specify_Method of Method.id
2.140 - | Specify_Problem of Problem.id
2.141 - | Specify_Theory of ThyC.id
2.142 - | Subproblem of ThyC.id * Problem.id
2.143 -
2.144 - | Substitute of Subst.input
2.145 - | Tac of string
2.146 - | Take of TermC.as_string | Take_Inst of TermC.as_string
2.147 val input_to_string : input -> string
2.148 val tac2IDstr : input -> string
2.149 val is_empty : input -> bool
3.1 --- a/src/Tools/isac/Specify/specify-step.sml Fri May 01 16:06:59 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/specify-step.sml Fri May 01 17:17:41 2020 +0200
3.3 @@ -1,7 +1,7 @@
3.4 (* Title: Specify/specify-step.sml
3.5 Author: Walther Neuper
3.6 (c) due to copyright terms
3.7 -
3.8 +
3.9 Code for the specify-phase in analogy to structure Solve_Step for the solve-phase.
3.10 *)
3.11
3.12 @@ -24,101 +24,20 @@
3.13 check tactics (input by the user, mostly) for applicability
3.14 and determine as much of the result of the tactic as possible initially.
3.15 *)
3.16 -fun check (Tactic.Init_Proof (ct', spec)) _ = Applicable.Yes (Tactic.Init_Proof' (ct', spec))
3.17 - | check Tactic.Model_Problem (pt, (p, p_)) =
3.18 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res then
3.19 - Applicable.No ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.20 - else
3.21 - let
3.22 - val pI' = case Ctree.get_obj I pt p of
3.23 - Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
3.24 - | _ => error "Specify_Step.check Init_Proof: uncovered case Ctree.get_obj"
3.25 - val {ppc, ...} = Specify.get_pbt pI'
3.26 - val pbl = Generate.init_pbl ppc
3.27 - in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
3.28 - | check (Tactic.Refine_Tacitly pI) (pt, (p, p_)) =
3.29 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.30 - then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.31 - else
3.32 - let
3.33 - val oris = case Ctree.get_obj I pt p of
3.34 - Ctree.PblObj {origin = (oris, _, _), ...} => oris
3.35 - | _ => error "Specify_Step.check Refine_Tacitly: uncovered case Ctree.get_obj"
3.36 - in
3.37 - case Specify.refine_ori oris pI of
3.38 - SOME pblID =>
3.39 - Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [](*filled in specify*)))
3.40 - | NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
3.41 - end
3.42 - | check (Tactic.Refine_Problem pI) (pt, (p, p_)) =
3.43 +fun check (Tactic.Add_Find ct') (pt, (p, p_)) =
3.44 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.45 - then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not for pos "^(Pos.pos'2str (p, p_)))
3.46 - else
3.47 - let
3.48 - val (dI, dI', itms) = case Ctree.get_obj I pt p of
3.49 - Ctree.PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
3.50 - => (dI, dI', itms)
3.51 - | _ => error "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
3.52 - val thy = if dI' = ThyC.id_empty then dI else dI';
3.53 - in
3.54 - case Specify.refine_pbl (ThyC.get_theory thy) pI itms of
3.55 - NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
3.56 - | SOME (rf as (pI', _)) =>
3.57 - if pI' = pI
3.58 - then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
3.59 - else Applicable.Yes (Tactic.Refine_Problem' rf)
3.60 - end
3.61 + then Applicable.No ((Tactic.input_to_string (Tactic.Add_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.62 + else Applicable.Yes (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
3.63 (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*)
3.64 | check (Tactic.Add_Given ct') (pt, (p, p_)) =
3.65 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.66 then Applicable.No ((Tactic.input_to_string (Tactic.Add_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.67 else Applicable.Yes (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))
3.68 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
3.69 - | check (Tactic.Del_Given ct') (pt, (p, p_)) =
3.70 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.71 - then Applicable.No ((Tactic.input_to_string (Tactic.Del_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.72 - else Applicable.Yes (Tactic.Del_Given' ct')
3.73 - | check (Tactic.Add_Find ct') (pt, (p, p_)) =
3.74 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.75 - then Applicable.No ((Tactic.input_to_string (Tactic.Add_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.76 - else Applicable.Yes (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
3.77 - | check (Tactic.Del_Find ct') (pt, (p, p_)) =
3.78 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.79 - then Applicable.No ((Tactic.input_to_string (Tactic.Del_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.80 - else Applicable.Yes (Tactic.Del_Find' ct')
3.81 | check (Tactic.Add_Relation ct') (pt, (p, p_)) =
3.82 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.83 then Applicable.No ((Tactic.input_to_string (Tactic.Add_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.84 else Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))
3.85 - | check (Tactic.Del_Relation ct') (pt, (p, p_)) =
3.86 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.87 - then Applicable.No ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.88 - else Applicable.Yes (Tactic.Del_Relation' ct')
3.89 - | check (Tactic.Specify_Theory dI) (pt, (p, p_)) =
3.90 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.91 - then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Theory dI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.92 - else Applicable.Yes (Tactic.Specify_Theory' dI)
3.93 - | check (Tactic.Specify_Problem pID) (pt, (p, p_)) =
3.94 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.95 - then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Problem pID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.96 - else
3.97 - let
3.98 - val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
3.99 - Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
3.100 - => (oris, dI, pI, dI', pI', itms)
3.101 - | _ => error "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
3.102 - val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
3.103 - val {ppc, where_, prls, ...} = Specify.get_pbt pID;
3.104 - val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
3.105 - then (false, (Generate.init_pbl ppc, []))
3.106 - else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
3.107 - in
3.108 - Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
3.109 - end
3.110 - | check (Tactic.Specify_Method mID) (pt, (p, p_)) =
3.111 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.112 - then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Method mID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.113 - else Applicable.Yes (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
3.114 | check (Tactic.Apply_Method mI) (pt, (p, p_)) =
3.115 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.116 then Applicable.No ((Tactic.input_to_string (Tactic.Apply_Method mI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.117 @@ -140,6 +59,87 @@
3.118 Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled in solve*), ctxt))
3.119 end
3.120 (*required for corner cases, e.g. test setup in inssort.sml*)
3.121 + | check (Tactic.Del_Find ct') (pt, (p, p_)) =
3.122 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.123 + then Applicable.No ((Tactic.input_to_string (Tactic.Del_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.124 + else Applicable.Yes (Tactic.Del_Find' ct')
3.125 + | check (Tactic.Del_Given ct') (pt, (p, p_)) =
3.126 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.127 + then Applicable.No ((Tactic.input_to_string (Tactic.Del_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.128 + else Applicable.Yes (Tactic.Del_Given' ct')
3.129 + | check (Tactic.Del_Relation ct') (pt, (p, p_)) =
3.130 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.131 + then Applicable.No ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.132 + else Applicable.Yes (Tactic.Del_Relation' ct')
3.133 + | check (Tactic.Init_Proof (ct', spec)) _ = Applicable.Yes (Tactic.Init_Proof' (ct', spec))
3.134 + | check Tactic.Model_Problem (pt, (p, p_)) =
3.135 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res then
3.136 + Applicable.No ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.137 + else
3.138 + let
3.139 + val pI' = case Ctree.get_obj I pt p of
3.140 + Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
3.141 + | _ => error "Specify_Step.check Init_Proof: uncovered case Ctree.get_obj"
3.142 + val {ppc, ...} = Specify.get_pbt pI'
3.143 + val pbl = Generate.init_pbl ppc
3.144 + in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
3.145 + | check (Tactic.Refine_Problem pI) (pt, (p, p_)) =
3.146 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.147 + then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not for pos "^(Pos.pos'2str (p, p_)))
3.148 + else
3.149 + let
3.150 + val (dI, dI', itms) = case Ctree.get_obj I pt p of
3.151 + Ctree.PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
3.152 + => (dI, dI', itms)
3.153 + | _ => error "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
3.154 + val thy = if dI' = ThyC.id_empty then dI else dI';
3.155 + in
3.156 + case Specify.refine_pbl (ThyC.get_theory thy) pI itms of
3.157 + NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
3.158 + | SOME (rf as (pI', _)) =>
3.159 + if pI' = pI
3.160 + then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
3.161 + else Applicable.Yes (Tactic.Refine_Problem' rf)
3.162 + end
3.163 + | check (Tactic.Refine_Tacitly pI) (pt, (p, p_)) =
3.164 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.165 + then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.166 + else
3.167 + let
3.168 + val oris = case Ctree.get_obj I pt p of
3.169 + Ctree.PblObj {origin = (oris, _, _), ...} => oris
3.170 + | _ => error "Specify_Step.check Refine_Tacitly: uncovered case Ctree.get_obj"
3.171 + in
3.172 + case Specify.refine_ori oris pI of
3.173 + SOME pblID =>
3.174 + Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [](*filled in specify*)))
3.175 + | NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
3.176 + end
3.177 + | check (Tactic.Specify_Method mID) (pt, (p, p_)) =
3.178 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.179 + then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Method mID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.180 + else Applicable.Yes (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
3.181 + | check (Tactic.Specify_Problem pID) (pt, (p, p_)) =
3.182 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.183 + then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Problem pID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.184 + else
3.185 + let
3.186 + val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
3.187 + Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
3.188 + => (oris, dI, pI, dI', pI', itms)
3.189 + | _ => error "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
3.190 + val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
3.191 + val {ppc, where_, prls, ...} = Specify.get_pbt pID;
3.192 + val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
3.193 + then (false, (Generate.init_pbl ppc, []))
3.194 + else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
3.195 + in
3.196 + Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
3.197 + end
3.198 + | check (Tactic.Specify_Theory dI) (pt, (p, p_)) =
3.199 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.200 + then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Theory dI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.201 + else Applicable.Yes (Tactic.Specify_Theory' dI)
3.202 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
3.203 | check tac (_, pos) =
3.204 raise ERROR ("Specify_Step.check called for " ^ Tactic.input_to_string tac ^ " at" ^ Pos.pos'2str pos);
4.1 --- a/src/Tools/isac/TODO.thy Fri May 01 16:06:59 2020 +0200
4.2 +++ b/src/Tools/isac/TODO.thy Fri May 01 17:17:41 2020 +0200
4.3 @@ -29,9 +29,9 @@
4.4 \item ML_file "rule-set.sml" Know_Store -> MathEngBasic (=ThmC, Rewrite)
4.5 probably first review calcelems.sml
4.6 \item xxx
4.7 - \item replace src/ Erls Rule_Set.Empty
4.8 + \item rename/relocate: Selem.result -> Calc.result ?OR? (NEW..)Formula.result
4.9 \item xxx
4.10 - \item xxx
4.11 + \item replace src/ Erls by Rule_Set.Empty
4.12 \item xxx
4.13 \item rename ptyps.sml -> specify-etc.sml
4.14 rename Specify -> Specify_Etc