1.1 --- a/src/Tools/isac/Interpret/solve-step.sml Wed Apr 29 12:30:51 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Fri May 01 15:28:40 2020 +0200
1.3 @@ -7,7 +7,12 @@
1.4
1.5 signature SOLVE_STEP =
1.6 sig
1.7 - val check_appl: Pos.pos' -> CTbasic.ctree -> Tactic.input -> Applicable.T
1.8 + val check: Tactic.input -> Calc.T -> Applicable.T
1.9 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.10 + (*NONE*)
1.11 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.12 + (*NONE*)
1.13 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.14 end
1.15
1.16 (**)
1.17 @@ -16,6 +21,285 @@
1.18 (**)
1.19
1.20 (*-----^^^^^- specify -----vvvvv- solve --------------------------------------------------------*)
1.21 +fun check (Tactic.Check_Postcond pI) (_, (p, p_)) =
1.22 + if member op = [Pos.Pbl, Pos.Met] p_
1.23 + then Applicable.No ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.24 + else Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
1.25 + | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
1.26 + | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve') (* always applicable *)
1.27 + | check (m as Tactic.Rewrite_Inst (subs, thm'')) (pt, (p, p_)) =
1.28 + if member op = [Pos.Pbl, Pos.Met] p_
1.29 + then Applicable.No ((Tactic.input_to_string m)^" not for pos " ^ Pos.pos'2str (p, p_))
1.30 + else
1.31 + let
1.32 + val pp = Ctree.par_pblobj pt p;
1.33 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.34 + val thy = ThyC.get_theory thy';
1.35 + val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
1.36 + val (f, _) = case p_ of (*p 12.4.00 unnecessary*)
1.37 + Frm => (Ctree.get_obj Ctree.g_form pt p, p)
1.38 + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
1.39 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.40 + in
1.41 + let
1.42 + val subst = Subst.T_from_input thy subs;
1.43 + in
1.44 + case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of
1.45 + SOME (f',asm) =>
1.46 + Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
1.47 + | NONE => Applicable.No ((fst thm'')^" not applicable")
1.48 + end
1.49 + handle _ => Applicable.No ("syntax error in "^(subs2str subs))
1.50 + end
1.51 + | check (m as Tactic.Rewrite thm'') (pt, (p, p_)) =
1.52 + if member op = [Pos.Pbl, Pos.Met] p_
1.53 + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
1.54 + else
1.55 + let
1.56 + val (msg, thy', ro, rls', _)= ApplicableOLD.from_pblobj_or_detail_thm thm'' p pt;
1.57 + val thy = ThyC.get_theory thy';
1.58 + val f = case p_ of
1.59 + Frm => Ctree.get_obj Ctree.g_form pt p
1.60 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.61 + | _ => error ("Solve_Step.check Rewrite: call by " ^ Pos.pos'2str (p, p_));
1.62 + in
1.63 + if msg = "OK"
1.64 + then
1.65 + case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of
1.66 + SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
1.67 + | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable")
1.68 + else Applicable.No msg
1.69 + end
1.70 + | check (m as Tactic.Detail_Set_Inst (subs, rls)) (pt, (p, p_)) =
1.71 + if member op = [Pos.Pbl, Pos.Met] p_
1.72 + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
1.73 + else
1.74 + let
1.75 + val pp = Ctree.par_pblobj pt p;
1.76 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.77 + val thy = ThyC.get_theory thy';
1.78 + val f = case p_ of Frm => Ctree.get_obj Ctree.g_form pt p
1.79 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.80 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.81 + val subst = Subst.T_from_input thy subs
1.82 + in
1.83 + case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
1.84 + SOME (f', asm)
1.85 + => Applicable.Yes (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
1.86 + | NONE => Applicable.No (rls ^ " not applicable")
1.87 + handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
1.88 + end
1.89 + | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (pt, (p, p_)) =
1.90 + if member op = [Pos.Pbl, Pos.Met] p_
1.91 + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
1.92 + else
1.93 + let
1.94 + val pp = Ctree.par_pblobj pt p;
1.95 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.96 + val thy = ThyC.get_theory thy';
1.97 + val (f, _) = case p_ of
1.98 + Frm => (Ctree.get_obj Ctree.g_form pt p, p)
1.99 + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
1.100 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.101 + val subst = Subst.T_from_input thy subs;
1.102 + in
1.103 + case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
1.104 + SOME (f',asm)
1.105 + => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
1.106 + | NONE => Applicable.No (rls ^ " not applicable")
1.107 + handle _ => Applicable.No ("syntax error in " ^(subs2str subs))
1.108 + end
1.109 + | check (m as Tactic.Rewrite_Set rls) (pt, (p, p_)) =
1.110 + if member op = [Pos.Pbl, Pos.Met] p_
1.111 + then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.112 + else
1.113 + let
1.114 + val pp = Ctree.par_pblobj pt p;
1.115 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.116 + val (f, _) = case p_ of
1.117 + Frm => (Ctree.get_obj Ctree.g_form pt p, p)
1.118 + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
1.119 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.120 + in
1.121 + case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
1.122 + SOME (f', asm)
1.123 + => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
1.124 + | NONE => Applicable.No (rls ^ " not applicable")
1.125 + end
1.126 + | check (m as Tactic.Detail_Set rls) (pt, (p, p_)) =
1.127 + if member op = [Pos.Pbl, Pos.Met] p_
1.128 + then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.129 + else
1.130 + let
1.131 + val pp = Ctree.par_pblobj pt p
1.132 + val thy' = Ctree.get_obj Ctree.g_domID pt pp
1.133 + val f = case p_ of
1.134 + Frm => Ctree.get_obj Ctree.g_form pt p
1.135 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) 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) => Applicable.Yes (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
1.140 + | NONE => Applicable.No (rls^" not applicable")
1.141 + end
1.142 + | check Tactic.End_Ruleset _ = raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset)
1.143 + | check (m as Tactic.Calculate op_) (pt, (p, p_)) =
1.144 + if member op = [Pos.Pbl, Pos.Met] p_
1.145 + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
1.146 + else
1.147 + let
1.148 + val (msg,thy',isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
1.149 + val f = case p_ of
1.150 + Frm => Ctree.get_obj Ctree.g_form pt p
1.151 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.152 + | _ => raise ERROR ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.153 + in
1.154 + if msg = "OK"
1.155 + then
1.156 + case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
1.157 + SOME (f', (id, thm))
1.158 + => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
1.159 + | NONE => Applicable.No ("'calculate "^op_^"' not applicable")
1.160 + else Applicable.No msg
1.161 + end
1.162 + (*Substitute combines two different kind of "substitution":
1.163 + (1) subst_atomic: for ?a..?z
1.164 + (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
1.165 + | check (m as Tactic.Substitute sube) (pt, (p, p_)) =
1.166 + if member op = [Pos.Pbl, Pos.Met] p_
1.167 + then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.168 + else
1.169 + let
1.170 + val pp = Ctree.par_pblobj pt p
1.171 + val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
1.172 + val f = case p_ of
1.173 + Frm => Ctree.get_obj Ctree.g_form pt p
1.174 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.175 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.176 + val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
1.177 + val subte = Subst.input_to_terms sube
1.178 + val subst = Subst.T_from_string_eqs thy sube
1.179 + val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
1.180 + in
1.181 + if foldl and_ (true, map TermC.contains_Var subte)
1.182 + then (*1*)
1.183 + let val f' = subst_atomic subst f
1.184 + in if f = f'
1.185 + then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
1.186 + else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
1.187 + end
1.188 + else (*2*)
1.189 + case Rewrite.rewrite_terms_ thy ro erls subte f of
1.190 + SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
1.191 + | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
1.192 + end
1.193 + | check (Tactic.Apply_Assumption cts') _ =
1.194 + raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
1.195 + (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)
1.196 + | check (Tactic.Take_Inst ct') _ =
1.197 + raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct'))
1.198 + | check (m as Tactic.Subproblem (domID, pblID)) (_, (p, p_)) =
1.199 + if Pos.on_specification p_
1.200 + then
1.201 + Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.202 + else (*some fields filled later in LI*)
1.203 + Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
1.204 + TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
1.205 + | check (Tactic.End_Subproblem) _ =
1.206 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)
1.207 + | check (Tactic.CAScmd ct') _ =
1.208 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct'))
1.209 + | check (Tactic.Split_And) _ =
1.210 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_And)
1.211 + | check (Tactic.Conclude_And) _ =
1.212 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And)
1.213 + | check (Tactic.Split_Or) _ =
1.214 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or)
1.215 + | check (Tactic.Conclude_Or) _ =
1.216 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or)
1.217 + | check (Tactic.Begin_Trans) (pt, (p, p_)) =
1.218 + let
1.219 + val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
1.220 + Pos.Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p)
1.221 + | 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.222 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.223 + in (Applicable.Yes (Tactic.Begin_Trans' f))
1.224 + handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'")
1.225 + end
1.226 + | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
1.227 + if p_ = Pos.Res
1.228 + then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
1.229 + else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"
1.230 + | check (Tactic.Begin_Sequ) _ =
1.231 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ))
1.232 + | check (Tactic.End_Sequ) _ =
1.233 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ))
1.234 + | check (Tactic.Split_Intersect) _ =
1.235 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect))
1.236 + | check (Tactic.End_Intersect) _ =
1.237 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect))
1.238 + | check (m as Tactic.Check_elementwise pred) (pt, (p, p_)) =
1.239 + if member op = [Pos.Pbl, Pos.Met] p_
1.240 + then Applicable.No ((Tactic.input_to_string m) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.241 + else
1.242 + let
1.243 + val pp = Ctree.par_pblobj pt p;
1.244 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.245 + val thy = ThyC.get_theory thy'
1.246 + val metID = (Ctree.get_obj Ctree.g_metID pt pp)
1.247 + val {crls, ...} = Specify.get_met metID
1.248 + val (f, asm) = case p_ of
1.249 + Frm => (Ctree.get_obj Ctree.g_form pt p , [])
1.250 + | Pos.Res => Ctree.get_obj Ctree.g_result pt p
1.251 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.252 + val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> ApplicableOLD.mk_set thy pt p f;
1.253 + in
1.254 + Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm)))
1.255 + end
1.256 + | check Tactic.Or_to_List (pt, (p, p_)) =
1.257 + if member op = [Pos.Pbl, Pos.Met] p_
1.258 + then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_)))
1.259 + else
1.260 + let
1.261 + val f = case p_ of
1.262 + Frm => Ctree.get_obj Ctree.g_form pt p
1.263 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.264 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.265 + in (let val ls = Prog_Expr.or2list f
1.266 + in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end)
1.267 + handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f)
1.268 + end
1.269 + | check Tactic.Collect_Trues _ =
1.270 + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues)
1.271 + | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
1.272 + | check (Tactic.Tac id) (pt, (p, p_)) =
1.273 + let
1.274 + val pp = Ctree.par_pblobj pt p;
1.275 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
1.276 + val thy = ThyC.get_theory thy';
1.277 + val f = case p_ of
1.278 + Frm => Ctree.get_obj Ctree.g_form pt p
1.279 + | Pos.Pbl => error "Solve_Step.check (p,Pos.Pbl) pt (Tac id): not at Pos.Pbl"
1.280 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.281 + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.282 + in case id of
1.283 + "subproblem_equation_dummy" =>
1.284 + if TermC.is_expliceq f
1.285 + then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
1.286 + else Applicable.No "applicable only to equations made explicit"
1.287 + | "solve_equation_dummy" =>
1.288 + let val (id', f') = ApplicableOLD.split_dummy (UnparseC.term f);
1.289 + in
1.290 + if id' <> "subproblem_equation_dummy"
1.291 + then Applicable.No "no subproblem"
1.292 + else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
1.293 + then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
1.294 + else error ("Solve_Step.check: f= " ^ f')
1.295 + end
1.296 + | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
1.297 + end
1.298 + | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
1.299 + | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
1.300 (*-----^^^^^- solve ---------------------------------------------------------------------------*)
1.301
1.302