diff -r 33913fe24685 -r 0766dade4a78 src/Tools/isac/Interpret/solve-step.sml --- a/src/Tools/isac/Interpret/solve-step.sml Wed Apr 29 12:30:51 2020 +0200 +++ b/src/Tools/isac/Interpret/solve-step.sml Fri May 01 15:28:40 2020 +0200 @@ -7,7 +7,12 @@ signature SOLVE_STEP = sig - val check_appl: Pos.pos' -> CTbasic.ctree -> Tactic.input -> Applicable.T + val check: Tactic.input -> Calc.T -> Applicable.T +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) + (*NONE*) +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) + (*NONE*) +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) end (**) @@ -16,6 +21,285 @@ (**) (*-----^^^^^- specify -----vvvvv- solve --------------------------------------------------------*) +fun check (Tactic.Check_Postcond pI) (_, (p, p_)) = + if member op = [Pos.Pbl, Pos.Met] p_ + then Applicable.No ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_)) + else Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty)) + | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*) + | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve') (* always applicable *) + | check (m as Tactic.Rewrite_Inst (subs, thm'')) (pt, (p, p_)) = + if member op = [Pos.Pbl, Pos.Met] p_ + then Applicable.No ((Tactic.input_to_string m)^" not for pos " ^ Pos.pos'2str (p, p_)) + else + let + val pp = Ctree.par_pblobj pt p; + val thy' = Ctree.get_obj Ctree.g_domID pt pp; + val thy = ThyC.get_theory thy'; + val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp); + val (f, _) = case p_ of (*p 12.4.00 unnecessary*) + Frm => (Ctree.get_obj Ctree.g_form pt p, p) + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p) + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + in + let + val subst = Subst.T_from_input thy subs; + in + case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of + SOME (f',asm) => + Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm))) + | NONE => Applicable.No ((fst thm'')^" not applicable") + end + handle _ => Applicable.No ("syntax error in "^(subs2str subs)) + end + | check (m as Tactic.Rewrite thm'') (pt, (p, p_)) = + if member op = [Pos.Pbl, Pos.Met] p_ + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_))) + else + let + val (msg, thy', ro, rls', _)= ApplicableOLD.from_pblobj_or_detail_thm thm'' p pt; + val thy = ThyC.get_theory thy'; + val f = case p_ of + Frm => Ctree.get_obj Ctree.g_form pt p + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p + | _ => error ("Solve_Step.check Rewrite: call by " ^ Pos.pos'2str (p, p_)); + in + if msg = "OK" + then + case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of + SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm))) + | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable") + else Applicable.No msg + end + | check (m as Tactic.Detail_Set_Inst (subs, rls)) (pt, (p, p_)) = + if member op = [Pos.Pbl, Pos.Met] p_ + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_))) + else + let + val pp = Ctree.par_pblobj pt p; + val thy' = Ctree.get_obj Ctree.g_domID pt pp; + val thy = ThyC.get_theory thy'; + val f = case p_ of Frm => Ctree.get_obj Ctree.g_form pt p + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + val subst = Subst.T_from_input thy subs + in + case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of + SOME (f', asm) + => Applicable.Yes (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm))) + | NONE => Applicable.No (rls ^ " not applicable") + handle _ => Applicable.No ("syntax error in " ^ subs2str subs) + end + | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (pt, (p, p_)) = + if member op = [Pos.Pbl, Pos.Met] p_ + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_))) + else + let + val pp = Ctree.par_pblobj pt p; + val thy' = Ctree.get_obj Ctree.g_domID pt pp; + val thy = ThyC.get_theory thy'; + val (f, _) = case p_ of + Frm => (Ctree.get_obj Ctree.g_form pt p, p) + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p) + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + val subst = Subst.T_from_input thy subs; + in + case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of + SOME (f',asm) + => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm))) + | NONE => Applicable.No (rls ^ " not applicable") + handle _ => Applicable.No ("syntax error in " ^(subs2str subs)) + end + | check (m as Tactic.Rewrite_Set rls) (pt, (p, p_)) = + if member op = [Pos.Pbl, Pos.Met] p_ + then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_)) + else + let + val pp = Ctree.par_pblobj pt p; + val thy' = Ctree.get_obj Ctree.g_domID pt pp; + val (f, _) = case p_ of + Frm => (Ctree.get_obj Ctree.g_form pt p, p) + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p) + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + in + case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of + SOME (f', asm) + => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm))) + | NONE => Applicable.No (rls ^ " not applicable") + end + | check (m as Tactic.Detail_Set rls) (pt, (p, p_)) = + if member op = [Pos.Pbl, Pos.Met] p_ + then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_)) + else + let + val pp = Ctree.par_pblobj pt p + val thy' = Ctree.get_obj Ctree.g_domID pt pp + val f = case p_ of + Frm => Ctree.get_obj Ctree.g_form pt p + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + in + case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of + SOME (f',asm) => Applicable.Yes (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm))) + | NONE => Applicable.No (rls^" not applicable") + end + | check Tactic.End_Ruleset _ = raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset) + | check (m as Tactic.Calculate op_) (pt, (p, p_)) = + if member op = [Pos.Pbl, Pos.Met] p_ + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_))) + else + let + val (msg,thy',isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt; + val f = case p_ of + Frm => Ctree.get_obj Ctree.g_form pt p + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p + | _ => raise ERROR ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + in + if msg = "OK" + then + case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of + SOME (f', (id, thm)) + => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm)))) + | NONE => Applicable.No ("'calculate "^op_^"' not applicable") + else Applicable.No msg + end + (*Substitute combines two different kind of "substitution": + (1) subst_atomic: for ?a..?z + (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*) + | check (m as Tactic.Substitute sube) (pt, (p, p_)) = + if member op = [Pos.Pbl, Pos.Met] p_ + then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_)) + else + let + val pp = Ctree.par_pblobj pt p + val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp) + val f = case p_ of + Frm => Ctree.get_obj Ctree.g_form pt p + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) + val subte = Subst.input_to_terms sube + val subst = Subst.T_from_string_eqs thy sube + val ro = Rewrite_Ord.assoc_rew_ord rew_ord' + in + if foldl and_ (true, map TermC.contains_Var subte) + then (*1*) + let val f' = subst_atomic subst f + in if f = f' + then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") + else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) + end + else (*2*) + case Rewrite.rewrite_terms_ thy ro erls subte f of + SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) + | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") + end + | check (Tactic.Apply_Assumption cts') _ = + raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts')) + (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *) + | check (Tactic.Take_Inst ct') _ = + raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct')) + | check (m as Tactic.Subproblem (domID, pblID)) (_, (p, p_)) = + if Pos.on_specification p_ + then + Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_)) + else (*some fields filled later in LI*) + Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [], + TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID)) + | check (Tactic.End_Subproblem) _ = + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem) + | check (Tactic.CAScmd ct') _ = + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct')) + | check (Tactic.Split_And) _ = + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_And) + | check (Tactic.Conclude_And) _ = + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And) + | check (Tactic.Split_Or) _ = + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or) + | check (Tactic.Conclude_Or) _ = + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or) + | check (Tactic.Begin_Trans) (pt, (p, p_)) = + let + val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*) + Pos.Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p) + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, (Pos.lev_on o Pos.lev_dn o Pos.lev_on) p) + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + in (Applicable.Yes (Tactic.Begin_Trans' f)) + handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'") + end + | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*) + if p_ = Pos.Res + then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p)) + else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence" + | check (Tactic.Begin_Sequ) _ = + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ)) + | check (Tactic.End_Sequ) _ = + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ)) + | check (Tactic.Split_Intersect) _ = + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect)) + | check (Tactic.End_Intersect) _ = + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect)) + | check (m as Tactic.Check_elementwise pred) (pt, (p, p_)) = + if member op = [Pos.Pbl, Pos.Met] p_ + then Applicable.No ((Tactic.input_to_string m) ^ " not for pos " ^ Pos.pos'2str (p, p_)) + else + let + val pp = Ctree.par_pblobj pt p; + val thy' = Ctree.get_obj Ctree.g_domID pt pp; + val thy = ThyC.get_theory thy' + val metID = (Ctree.get_obj Ctree.g_metID pt pp) + val {crls, ...} = Specify.get_met metID + val (f, asm) = case p_ of + Frm => (Ctree.get_obj Ctree.g_form pt p , []) + | Pos.Res => Ctree.get_obj Ctree.g_result pt p + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> ApplicableOLD.mk_set thy pt p f; + in + Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm))) + end + | check Tactic.Or_to_List (pt, (p, p_)) = + if member op = [Pos.Pbl, Pos.Met] p_ + then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_))) + else + let + val f = case p_ of + Frm => Ctree.get_obj Ctree.g_form pt p + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + in (let val ls = Prog_Expr.or2list f + in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end) + handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f) + end + | check Tactic.Collect_Trues _ = + error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues) + | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable" + | check (Tactic.Tac id) (pt, (p, p_)) = + let + val pp = Ctree.par_pblobj pt p; + val thy' = Ctree.get_obj Ctree.g_domID pt pp; + val thy = ThyC.get_theory thy'; + val f = case p_ of + Frm => Ctree.get_obj Ctree.g_form pt p + | Pos.Pbl => error "Solve_Step.check (p,Pos.Pbl) pt (Tac id): not at Pos.Pbl" + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p + | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + in case id of + "subproblem_equation_dummy" => + if TermC.is_expliceq f + then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")")) + else Applicable.No "applicable only to equations made explicit" + | "solve_equation_dummy" => + let val (id', f') = ApplicableOLD.split_dummy (UnparseC.term f); + in + if id' <> "subproblem_equation_dummy" + then Applicable.No "no subproblem" + else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq + then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]")) + else error ("Solve_Step.check: f= " ^ f') + end + | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f)) + end + | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof'' + | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m); (*-----^^^^^- solve ---------------------------------------------------------------------------*)