1.1 --- a/src/Tools/isac/Interpret/solve-step.sml Sat May 02 12:13:20 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Sat May 02 15:41:27 2020 +0200
1.3 @@ -24,18 +24,10 @@
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.CAScmd ct') _ =
1.8 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct'))
1.9 - | check (m as Tactic.Calculate op_) (pt, (p, p_)) =
1.10 - if member op = [Pos.Pbl, Pos.Met] p_
1.11 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
1.12 - else
1.13 +fun check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
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 + val (msg, thy', isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
1.21 + val f = Calc.current_formula cs;
1.22 in
1.23 if msg = "OK"
1.24 then
1.25 @@ -45,35 +37,18 @@
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 (m as Tactic.Check_elementwise pred) (pt, (p, p_)) =
1.34 - if member op = [Pos.Pbl, Pos.Met] p_
1.35 - then Applicable.No ((Tactic.input_to_string m) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.36 - else
1.37 + | check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*)
1.38 + Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
1.39 + | check (Tactic.Check_elementwise pred) cs =
1.40 let
1.41 - val pp = Ctree.par_pblobj pt p;
1.42 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.43 - val thy = ThyC.get_theory thy'
1.44 - val metID = (Ctree.get_obj Ctree.g_metID pt pp)
1.45 - val {crls, ...} = Specify.get_met metID
1.46 - val (f, asm) = case p_ of
1.47 - Frm => (Ctree.get_obj Ctree.g_form pt p , [])
1.48 - | Pos.Res => Ctree.get_obj Ctree.g_result pt p
1.49 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.50 - val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> ApplicableOLD.mk_set thy pt p f;
1.51 + val f = Calc.current_formula cs;
1.52 in
1.53 - Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm)))
1.54 + Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, [])))
1.55 end
1.56 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
1.57 | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve') (* always applicable *)
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 + let
1.64 val f = case p_ of
1.65 Pos.Frm => Ctree.get_obj Ctree.g_form pt p
1.66 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.67 @@ -82,17 +57,11 @@
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 + | check (Tactic.Rewrite thm'') (cs as (pt, (p, _))) =
1.76 let
1.77 val (msg, thy', ro, rls', _)= ApplicableOLD.from_pblobj_or_detail_thm thm'' p pt;
1.78 val thy = ThyC.get_theory thy';
1.79 - val f = case p_ of
1.80 - Frm => Ctree.get_obj Ctree.g_form pt p
1.81 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.82 - | _ => error ("Solve_Step.check Rewrite: call by " ^ Pos.pos'2str (p, p_));
1.83 + val f = Calc.current_formula cs;
1.84 in
1.85 if msg = "OK"
1.86 then
1.87 @@ -101,19 +70,13 @@
1.88 | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable")
1.89 else Applicable.No msg
1.90 end
1.91 - | check (m as Tactic.Rewrite_Inst (subs, thm'')) (pt, (p, p_)) =
1.92 - if member op = [Pos.Pbl, Pos.Met] p_
1.93 - then Applicable.No ((Tactic.input_to_string m)^" not for pos " ^ Pos.pos'2str (p, p_))
1.94 - else
1.95 + | check (Tactic.Rewrite_Inst (subs, thm'')) (cs as (pt, (p, _))) =
1.96 let
1.97 val pp = Ctree.par_pblobj pt p;
1.98 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.99 val thy = ThyC.get_theory thy';
1.100 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
1.101 - val (f, _) = case p_ of (*p 12.4.00 unnecessary*)
1.102 - Frm => (Ctree.get_obj Ctree.g_form pt p, p)
1.103 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
1.104 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.105 + val f = Calc.current_formula cs;
1.106 in
1.107 let
1.108 val subst = Subst.T_from_input thy subs;
1.109 @@ -123,26 +86,20 @@
1.110 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
1.111 | NONE => Applicable.No ((fst thm'')^" not applicable")
1.112 end
1.113 - handle _ => Applicable.No ("syntax error in "^(subs2str subs))
1.114 + handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
1.115 end
1.116 - | check (m as Tactic.Rewrite_Set rls) (pt, (p, p_)) =
1.117 - if member op = [Pos.Pbl, Pos.Met] p_
1.118 - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.119 - else
1.120 + | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =
1.121 let
1.122 val pp = Ctree.par_pblobj pt p;
1.123 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.124 - val (f, _) = case p_ of
1.125 - Frm => (Ctree.get_obj Ctree.g_form pt p, p)
1.126 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
1.127 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.128 + val f = Calc.current_formula cs;
1.129 in
1.130 case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
1.131 SOME (f', asm)
1.132 => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
1.133 | NONE => Applicable.No (rls ^ " not applicable")
1.134 end
1.135 - | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (pt, (p, p_)) =
1.136 + | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, p_))) =
1.137 if member op = [Pos.Pbl, Pos.Met] p_
1.138 then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
1.139 else
1.140 @@ -150,66 +107,50 @@
1.141 val pp = Ctree.par_pblobj pt p;
1.142 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.143 val thy = ThyC.get_theory thy';
1.144 - val (f, _) = case p_ of
1.145 - Frm => (Ctree.get_obj Ctree.g_form pt p, p)
1.146 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
1.147 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.148 + val f = Calc.current_formula cs;
1.149 val subst = Subst.T_from_input thy subs;
1.150 in
1.151 - case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
1.152 - SOME (f',asm)
1.153 + case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
1.154 + SOME (f', asm)
1.155 => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
1.156 | NONE => Applicable.No (rls ^ " not applicable")
1.157 handle _ => Applicable.No ("syntax error in " ^(subs2str subs))
1.158 end
1.159 - | check (m as Tactic.Subproblem (domID, pblID)) (_, (p, p_)) =
1.160 - if Pos.on_specification p_
1.161 - then
1.162 - Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.163 - else (*some fields filled later in LI*)
1.164 - Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
1.165 - TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
1.166 - (*Substitute combines two different kind of "substitution":
1.167 + | check (Tactic.Subproblem (domID, pblID)) (_, _) =
1.168 + Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
1.169 + TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
1.170 +
1.171 + (*Substitute combines two different kind of "substitution":
1.172 (1) subst_atomic: for ?a..?z
1.173 (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
1.174 - | check (m as Tactic.Substitute sube) (pt, (p, p_)) =
1.175 - if member op = [Pos.Pbl, Pos.Met] p_
1.176 - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.177 - else
1.178 - let
1.179 - val pp = Ctree.par_pblobj pt p
1.180 - val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
1.181 - val f = case p_ of
1.182 - Frm => Ctree.get_obj Ctree.g_form pt p
1.183 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.184 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.185 - val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
1.186 - val subte = Subst.input_to_terms sube
1.187 - val subst = Subst.T_from_string_eqs thy sube
1.188 - val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
1.189 - in
1.190 - if foldl and_ (true, map TermC.contains_Var subte)
1.191 - then (*1*)
1.192 - let val f' = subst_atomic subst f
1.193 - in if f = f'
1.194 - then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
1.195 - else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
1.196 - end
1.197 - else (*2*)
1.198 - case Rewrite.rewrite_terms_ thy ro erls subte f of
1.199 - SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
1.200 - | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
1.201 - end
1.202 - | check (Tactic.Tac id) (pt, (p, p_)) =
1.203 + | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
1.204 + let
1.205 + val pp = Ctree.par_pblobj pt p
1.206 + val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
1.207 + val f = Calc.current_formula cs;
1.208 + val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
1.209 + val subte = Subst.input_to_terms sube
1.210 + val subst = Subst.T_from_string_eqs thy sube
1.211 + val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
1.212 + in
1.213 + if foldl and_ (true, map TermC.contains_Var subte)
1.214 + then (*1*)
1.215 + let val f' = subst_atomic subst f
1.216 + in if f = f'
1.217 + then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
1.218 + else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
1.219 + end
1.220 + else (*2*)
1.221 + case Rewrite.rewrite_terms_ thy ro erls subte f of
1.222 + SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
1.223 + | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
1.224 + end
1.225 + | check (Tactic.Tac id) (cs as (pt, (p, _))) =
1.226 let
1.227 val pp = Ctree.par_pblobj pt p;
1.228 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.229 val thy = ThyC.get_theory thy';
1.230 - val f = case p_ of
1.231 - Frm => Ctree.get_obj Ctree.g_form pt p
1.232 - | Pos.Pbl => error "Solve_Step.check (p,Pos.Pbl) pt (Tac id): not at Pos.Pbl"
1.233 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.234 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.235 + val f = Calc.current_formula cs;
1.236 in case id of
1.237 "subproblem_equation_dummy" =>
1.238 if TermC.is_expliceq f