1 (* Title: Specify/solve-step.sml
3 (c) due to copyright terms
5 Code for the solve-phase in analogy to structure Specify_Step for the specify-phase.
10 val check: Tactic.input -> Calc.T -> Applicable.T
11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
15 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
19 structure Solve_Step(** ): SOLVE_STEP( **) =
24 check tactics (input by the user, mostly) for applicability
25 and determine as much of the result of the tactic as possible initially.
27 fun check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
29 val (msg, thy', isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
30 val f = Calc.current_formula cs;
34 case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
36 => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
37 | NONE => Applicable.No ("'calculate " ^ op_ ^ "' not applicable")
38 else Applicable.No msg
40 | check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*)
41 Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
42 | check (Tactic.Check_elementwise pred) cs =
44 val f = Calc.current_formula cs;
46 Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, [])))
48 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
49 | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve')
50 | check Tactic.Or_to_List cs =
52 val f = Calc.current_formula cs;
53 val ls = Prog_Expr.or2list f;
55 Applicable.Yes (Tactic.Or_to_List' (f, ls))
57 | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) =
59 val (msg, thy', ro, rls', _) = ApplicableOLD.from_pblobj_or_detail_thm thm p pt;
60 val thy = ThyC.get_theory thy';
61 val f = Calc.current_formula cs;
65 case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm) f of
66 SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
67 | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable")
68 else Applicable.No msg
70 | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) =
72 val pp = Ctree.par_pblobj pt p;
73 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
74 val thy = ThyC.get_theory thy';
75 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
76 val f = Calc.current_formula cs;
77 val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
79 case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm) f of
81 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
82 | NONE => Applicable.No (fst thm ^ " not applicable")
84 | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =
86 val pp = Ctree.par_pblobj pt p;
87 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
88 val f = Calc.current_formula cs;
90 case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
92 => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
93 | NONE => Applicable.No (rls ^ " not applicable")
95 | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, _))) =
97 val pp = Ctree.par_pblobj pt p;
98 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
99 val thy = ThyC.get_theory thy';
100 val f = Calc.current_formula cs;
101 val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
103 case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
105 => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
106 | NONE => Applicable.No (rls ^ " not applicable")
108 | check (Tactic.Subproblem (domID, pblID)) (_, _) =
109 Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
110 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
111 | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
113 val pp = Ctree.par_pblobj pt p
114 val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
115 val f = Calc.current_formula cs;
116 val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
117 val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
118 val subst = Subst.T_from_string_eqs thy sube
119 val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
121 if foldl and_ (true, map TermC.contains_Var subte)
123 let val f' = subst_atomic subst f
125 then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
126 else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
129 case Rewrite.rewrite_terms_ thy ro erls subte f of
130 SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
131 | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
133 | check (Tactic.Tac id) (cs as (pt, (p, _))) =
135 val pp = Ctree.par_pblobj pt p;
136 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
137 val thy = ThyC.get_theory thy';
138 val f = Calc.current_formula cs;
140 "subproblem_equation_dummy" =>
141 if TermC.is_expliceq f
142 then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
143 else Applicable.No "applicable only to equations made explicit"
144 | "solve_equation_dummy" =>
145 let val (id', f') = ApplicableOLD.split_dummy (UnparseC.term f);
147 if id' <> "subproblem_equation_dummy"
148 then Applicable.No "no subproblem"
149 else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
150 then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
151 else error ("Solve_Step.check: f= " ^ f')
153 | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
155 | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
156 | check (Tactic.Begin_Trans) cs =
157 Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs))
158 | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
160 then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
161 else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"
162 | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
163 | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);