walther@59920
|
1 |
(* Title: Specify/solve-step.sml
|
walther@59920
|
2 |
Author: Walther Neuper
|
walther@59920
|
3 |
(c) due to copyright terms
|
walther@59920
|
4 |
|
walther@59920
|
5 |
Code for the solve-phase in analogy to structure Specify_Step for the specify-phase.
|
walther@59920
|
6 |
*)
|
walther@59920
|
7 |
|
walther@59920
|
8 |
signature SOLVE_STEP =
|
walther@59920
|
9 |
sig
|
walther@59921
|
10 |
val check: Tactic.input -> Calc.T -> Applicable.T
|
walther@59921
|
11 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59921
|
12 |
(*NONE*)
|
walther@59921
|
13 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59921
|
14 |
(*NONE*)
|
walther@59921
|
15 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59920
|
16 |
end
|
walther@59920
|
17 |
|
walther@59920
|
18 |
(**)
|
walther@59920
|
19 |
structure Solve_Step(** ): SOLVE_STEP( **) =
|
walther@59920
|
20 |
struct
|
walther@59920
|
21 |
(**)
|
walther@59920
|
22 |
|
walther@59922
|
23 |
(*
|
walther@59922
|
24 |
check tactics (input by the user, mostly) for applicability
|
walther@59922
|
25 |
and determine as much of the result of the tactic as possible initially.
|
walther@59922
|
26 |
*)
|
walther@59928
|
27 |
fun check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
|
walther@59923
|
28 |
let
|
walther@59928
|
29 |
val (msg, thy', isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
|
walther@59928
|
30 |
val f = Calc.current_formula cs;
|
walther@59923
|
31 |
in
|
walther@59923
|
32 |
if msg = "OK"
|
walther@59923
|
33 |
then
|
walther@59923
|
34 |
case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
|
walther@59923
|
35 |
SOME (f', (id, thm))
|
walther@59923
|
36 |
=> Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
|
walther@59923
|
37 |
| NONE => Applicable.No ("'calculate "^op_^"' not applicable")
|
walther@59923
|
38 |
else Applicable.No msg
|
walther@59923
|
39 |
end
|
walther@59928
|
40 |
| check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*)
|
walther@59928
|
41 |
Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
|
walther@59928
|
42 |
| check (Tactic.Check_elementwise pred) cs =
|
walther@59923
|
43 |
let
|
walther@59928
|
44 |
val f = Calc.current_formula cs;
|
walther@59923
|
45 |
in
|
walther@59928
|
46 |
Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, [])))
|
walther@59923
|
47 |
end
|
walther@59923
|
48 |
| check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
|
walther@59921
|
49 |
| check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve') (* always applicable *)
|
walther@59923
|
50 |
| check Tactic.Or_to_List (pt, (p, p_)) =
|
walther@59928
|
51 |
let
|
walther@59923
|
52 |
val f = case p_ of
|
walther@59927
|
53 |
Pos.Frm => Ctree.get_obj Ctree.g_form pt p
|
walther@59923
|
54 |
| Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
|
walther@59923
|
55 |
| _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
|
walther@59923
|
56 |
in (let val ls = Prog_Expr.or2list f
|
walther@59923
|
57 |
in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end)
|
walther@59923
|
58 |
handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f)
|
walther@59923
|
59 |
end
|
walther@59928
|
60 |
| check (Tactic.Rewrite thm'') (cs as (pt, (p, _))) =
|
walther@59923
|
61 |
let
|
walther@59923
|
62 |
val (msg, thy', ro, rls', _)= ApplicableOLD.from_pblobj_or_detail_thm thm'' p pt;
|
walther@59923
|
63 |
val thy = ThyC.get_theory thy';
|
walther@59928
|
64 |
val f = Calc.current_formula cs;
|
walther@59923
|
65 |
in
|
walther@59923
|
66 |
if msg = "OK"
|
walther@59923
|
67 |
then
|
walther@59923
|
68 |
case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of
|
walther@59923
|
69 |
SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
|
walther@59923
|
70 |
| NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable")
|
walther@59923
|
71 |
else Applicable.No msg
|
walther@59923
|
72 |
end
|
walther@59928
|
73 |
| check (Tactic.Rewrite_Inst (subs, thm'')) (cs as (pt, (p, _))) =
|
walther@59921
|
74 |
let
|
walther@59921
|
75 |
val pp = Ctree.par_pblobj pt p;
|
walther@59921
|
76 |
val thy' = Ctree.get_obj Ctree.g_domID pt pp;
|
walther@59921
|
77 |
val thy = ThyC.get_theory thy';
|
walther@59921
|
78 |
val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
|
walther@59928
|
79 |
val f = Calc.current_formula cs;
|
walther@59921
|
80 |
in
|
walther@59921
|
81 |
let
|
walther@59921
|
82 |
val subst = Subst.T_from_input thy subs;
|
walther@59921
|
83 |
in
|
walther@59921
|
84 |
case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of
|
walther@59921
|
85 |
SOME (f',asm) =>
|
walther@59921
|
86 |
Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
|
walther@59921
|
87 |
| NONE => Applicable.No ((fst thm'')^" not applicable")
|
walther@59921
|
88 |
end
|
walther@59928
|
89 |
handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
|
walther@59921
|
90 |
end
|
walther@59928
|
91 |
| check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =
|
walther@59921
|
92 |
let
|
walther@59923
|
93 |
val pp = Ctree.par_pblobj pt p;
|
walther@59921
|
94 |
val thy' = Ctree.get_obj Ctree.g_domID pt pp;
|
walther@59928
|
95 |
val f = Calc.current_formula cs;
|
walther@59923
|
96 |
in
|
walther@59923
|
97 |
case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
|
walther@59921
|
98 |
SOME (f', asm)
|
walther@59923
|
99 |
=> Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
|
walther@59923
|
100 |
| NONE => Applicable.No (rls ^ " not applicable")
|
walther@59921
|
101 |
end
|
walther@59928
|
102 |
| check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, p_))) =
|
walther@59921
|
103 |
if member op = [Pos.Pbl, Pos.Met] p_
|
walther@59921
|
104 |
then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
|
walther@59921
|
105 |
else
|
walther@59921
|
106 |
let
|
walther@59921
|
107 |
val pp = Ctree.par_pblobj pt p;
|
walther@59921
|
108 |
val thy' = Ctree.get_obj Ctree.g_domID pt pp;
|
walther@59921
|
109 |
val thy = ThyC.get_theory thy';
|
walther@59928
|
110 |
val f = Calc.current_formula cs;
|
walther@59921
|
111 |
val subst = Subst.T_from_input thy subs;
|
walther@59921
|
112 |
in
|
walther@59928
|
113 |
case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
|
walther@59928
|
114 |
SOME (f', asm)
|
walther@59921
|
115 |
=> Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
|
walther@59921
|
116 |
| NONE => Applicable.No (rls ^ " not applicable")
|
walther@59921
|
117 |
handle _ => Applicable.No ("syntax error in " ^(subs2str subs))
|
walther@59921
|
118 |
end
|
walther@59928
|
119 |
| check (Tactic.Subproblem (domID, pblID)) (_, _) =
|
walther@59928
|
120 |
Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
|
walther@59928
|
121 |
TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
|
walther@59928
|
122 |
|
walther@59928
|
123 |
(*Substitute combines two different kind of "substitution":
|
walther@59921
|
124 |
(1) subst_atomic: for ?a..?z
|
walther@59921
|
125 |
(2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
|
walther@59928
|
126 |
| check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
|
walther@59928
|
127 |
let
|
walther@59928
|
128 |
val pp = Ctree.par_pblobj pt p
|
walther@59928
|
129 |
val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
|
walther@59928
|
130 |
val f = Calc.current_formula cs;
|
walther@59928
|
131 |
val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
|
walther@59928
|
132 |
val subte = Subst.input_to_terms sube
|
walther@59928
|
133 |
val subst = Subst.T_from_string_eqs thy sube
|
walther@59928
|
134 |
val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
|
walther@59928
|
135 |
in
|
walther@59928
|
136 |
if foldl and_ (true, map TermC.contains_Var subte)
|
walther@59928
|
137 |
then (*1*)
|
walther@59928
|
138 |
let val f' = subst_atomic subst f
|
walther@59928
|
139 |
in if f = f'
|
walther@59928
|
140 |
then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
|
walther@59928
|
141 |
else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
|
walther@59928
|
142 |
end
|
walther@59928
|
143 |
else (*2*)
|
walther@59928
|
144 |
case Rewrite.rewrite_terms_ thy ro erls subte f of
|
walther@59928
|
145 |
SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
|
walther@59928
|
146 |
| NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
|
walther@59928
|
147 |
end
|
walther@59928
|
148 |
| check (Tactic.Tac id) (cs as (pt, (p, _))) =
|
walther@59921
|
149 |
let
|
walther@59921
|
150 |
val pp = Ctree.par_pblobj pt p;
|
walther@59921
|
151 |
val thy' = Ctree.get_obj Ctree.g_domID pt pp;
|
walther@59921
|
152 |
val thy = ThyC.get_theory thy';
|
walther@59928
|
153 |
val f = Calc.current_formula cs;
|
walther@59921
|
154 |
in case id of
|
walther@59921
|
155 |
"subproblem_equation_dummy" =>
|
walther@59921
|
156 |
if TermC.is_expliceq f
|
walther@59921
|
157 |
then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
|
walther@59921
|
158 |
else Applicable.No "applicable only to equations made explicit"
|
walther@59921
|
159 |
| "solve_equation_dummy" =>
|
walther@59921
|
160 |
let val (id', f') = ApplicableOLD.split_dummy (UnparseC.term f);
|
walther@59921
|
161 |
in
|
walther@59921
|
162 |
if id' <> "subproblem_equation_dummy"
|
walther@59921
|
163 |
then Applicable.No "no subproblem"
|
walther@59921
|
164 |
else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
|
walther@59921
|
165 |
then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
|
walther@59921
|
166 |
else error ("Solve_Step.check: f= " ^ f')
|
walther@59921
|
167 |
end
|
walther@59921
|
168 |
| _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
|
walther@59921
|
169 |
end
|
walther@59923
|
170 |
| check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
|
walther@59923
|
171 |
| check (Tactic.Begin_Trans) (pt, (p, p_)) =
|
walther@59923
|
172 |
let
|
walther@59923
|
173 |
val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
|
walther@59923
|
174 |
Pos.Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p)
|
walther@59923
|
175 |
| Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, (Pos.lev_on o Pos.lev_dn o Pos.lev_on) p)
|
walther@59923
|
176 |
| _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
|
walther@59923
|
177 |
in (Applicable.Yes (Tactic.Begin_Trans' f))
|
walther@59923
|
178 |
handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'")
|
walther@59923
|
179 |
end
|
walther@59923
|
180 |
| check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
|
walther@59923
|
181 |
if p_ = Pos.Res
|
walther@59923
|
182 |
then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
|
walther@59923
|
183 |
else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"
|
walther@59921
|
184 |
| check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
|
walther@59921
|
185 |
| check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
|
walther@59920
|
186 |
|
walther@59920
|
187 |
(**)end(**);
|