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(**);