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@59931
|
11 |
val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
|
walther@59935
|
12 |
|
walther@59932
|
13 |
val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
|
walther@59932
|
14 |
val s_add_general: State_Steps.T ->
|
walther@59932
|
15 |
Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
|
walther@59933
|
16 |
val add_hard:
|
walther@59933
|
17 |
theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Generate.test_out
|
walther@59932
|
18 |
|
walther@59935
|
19 |
val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
|
walther@59935
|
20 |
string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
|
walther@59935
|
21 |
val get_eval: string -> Pos.pos ->Ctree.ctree ->
|
walther@59935
|
22 |
string * ThyC.id * (string * Rule_Def.eval_fn)
|
walther@59935
|
23 |
|
walther@59921
|
24 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59921
|
25 |
(*NONE*)
|
walther@59921
|
26 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59935
|
27 |
val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list
|
walther@59921
|
28 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59920
|
29 |
end
|
walther@59920
|
30 |
|
walther@59920
|
31 |
(**)
|
walther@59920
|
32 |
structure Solve_Step(** ): SOLVE_STEP( **) =
|
walther@59920
|
33 |
struct
|
walther@59920
|
34 |
(**)
|
walther@59920
|
35 |
|
walther@59935
|
36 |
(** get data from Calc.T **)
|
walther@59935
|
37 |
|
walther@59935
|
38 |
(* the source is the parent node, either a problem or a Rule_Set (with inter_steps) *)
|
walther@59935
|
39 |
fun rew_info (Rule_Def.Repeat {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
|
walther@59935
|
40 |
(rew_ord', erls, ca)
|
walther@59935
|
41 |
| rew_info (Rule_Set.Sequence {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
|
walther@59935
|
42 |
(rew_ord', erls, ca)
|
walther@59935
|
43 |
| rew_info (Rule_Set.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
|
walther@59935
|
44 |
(rew_ord', erls, ca)
|
walther@59935
|
45 |
| rew_info rls = error ("rew_info called with '" ^ Rule_Set.id rls ^ "'");
|
walther@59935
|
46 |
|
walther@59935
|
47 |
fun get_ruleset _ p pt =
|
walther@59935
|
48 |
let
|
walther@59935
|
49 |
val (pbl, p', rls') = Ctree.parent_node pt p
|
walther@59935
|
50 |
in
|
walther@59935
|
51 |
if pbl
|
walther@59935
|
52 |
then
|
walther@59935
|
53 |
let
|
walther@59935
|
54 |
val thy' = Ctree.get_obj Ctree.g_domID pt p'
|
walther@59935
|
55 |
val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
|
walther@59935
|
56 |
in ("OK", thy', rew_ord', erls, false) end
|
walther@59935
|
57 |
else
|
walther@59935
|
58 |
let
|
walther@59935
|
59 |
val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p)
|
walther@59935
|
60 |
val (rew_ord', erls, _) = rew_info rls'
|
walther@59935
|
61 |
in ("OK", thy', rew_ord', erls, false) end
|
walther@59935
|
62 |
end;
|
walther@59935
|
63 |
|
walther@59935
|
64 |
fun get_eval scrop p pt =
|
walther@59935
|
65 |
let
|
walther@59935
|
66 |
val (pbl, p', rls') = Ctree.parent_node pt p
|
walther@59935
|
67 |
in
|
walther@59935
|
68 |
if pbl
|
walther@59935
|
69 |
then
|
walther@59935
|
70 |
let
|
walther@59935
|
71 |
val thy' = Ctree.get_obj Ctree.g_domID pt p'
|
walther@59935
|
72 |
val {calc = scr_isa_fns, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
|
walther@59935
|
73 |
val opt = assoc (scr_isa_fns, scrop)
|
walther@59935
|
74 |
in
|
walther@59935
|
75 |
case opt of
|
walther@59935
|
76 |
SOME isa_fn => ("OK", thy', isa_fn)
|
walther@59935
|
77 |
| NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
|
walther@59935
|
78 |
end
|
walther@59935
|
79 |
else
|
walther@59935
|
80 |
let
|
walther@59935
|
81 |
val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p);
|
walther@59935
|
82 |
val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
|
walther@59935
|
83 |
in
|
walther@59935
|
84 |
case assoc (scr_isa_fns, scrop) of
|
walther@59935
|
85 |
SOME isa_fn => ("OK",thy',isa_fn)
|
walther@59935
|
86 |
| NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
|
walther@59935
|
87 |
end
|
walther@59935
|
88 |
end;
|
walther@59935
|
89 |
|
walther@59935
|
90 |
(** Solve_Step.check **)
|
walther@59935
|
91 |
|
walther@59922
|
92 |
(*
|
walther@59922
|
93 |
check tactics (input by the user, mostly) for applicability
|
walther@59922
|
94 |
and determine as much of the result of the tactic as possible initially.
|
walther@59922
|
95 |
*)
|
walther@59932
|
96 |
fun check (Tactic.Apply_Method mI) (pt, (p, _)) =
|
walther@59932
|
97 |
let
|
walther@59932
|
98 |
val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
|
walther@59932
|
99 |
Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
|
walther@59932
|
100 |
| _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
|
walther@59932
|
101 |
val {where_, ...} = Specify.get_pbt pI
|
walther@59943
|
102 |
val pres = map (I_Model.mk_env probl |> subst_atomic) where_
|
walther@59932
|
103 |
val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
|
walther@59932
|
104 |
then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
|
walther@59932
|
105 |
else ctxt
|
walther@59932
|
106 |
in
|
walther@59932
|
107 |
Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))
|
walther@59932
|
108 |
end
|
walther@59932
|
109 |
| check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
|
walther@59923
|
110 |
let
|
walther@59935
|
111 |
val (msg, thy', isa_fn) = get_eval op_ p pt;
|
walther@59928
|
112 |
val f = Calc.current_formula cs;
|
walther@59923
|
113 |
in
|
walther@59923
|
114 |
if msg = "OK"
|
walther@59923
|
115 |
then
|
walther@59923
|
116 |
case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
|
walther@59923
|
117 |
SOME (f', (id, thm))
|
walther@59923
|
118 |
=> Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
|
walther@59929
|
119 |
| NONE => Applicable.No ("'calculate " ^ op_ ^ "' not applicable")
|
walther@59923
|
120 |
else Applicable.No msg
|
walther@59923
|
121 |
end
|
walther@59928
|
122 |
| check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*)
|
walther@59928
|
123 |
Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
|
walther@59928
|
124 |
| check (Tactic.Check_elementwise pred) cs =
|
walther@59923
|
125 |
let
|
walther@59928
|
126 |
val f = Calc.current_formula cs;
|
walther@59923
|
127 |
in
|
walther@59928
|
128 |
Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, [])))
|
walther@59923
|
129 |
end
|
walther@59923
|
130 |
| check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
|
walther@59929
|
131 |
| check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve')
|
walther@59929
|
132 |
| check Tactic.Or_to_List cs =
|
walther@59928
|
133 |
let
|
walther@59929
|
134 |
val f = Calc.current_formula cs;
|
walther@59929
|
135 |
val ls = Prog_Expr.or2list f;
|
walther@59929
|
136 |
in
|
walther@59929
|
137 |
Applicable.Yes (Tactic.Or_to_List' (f, ls))
|
walther@59923
|
138 |
end
|
walther@59929
|
139 |
| check (Tactic.Rewrite thm) (cs as (pt, (p, _))) =
|
walther@59923
|
140 |
let
|
walther@59935
|
141 |
val (msg, thy', ro, rls', _) = get_ruleset thm p pt;
|
walther@59923
|
142 |
val thy = ThyC.get_theory thy';
|
walther@59928
|
143 |
val f = Calc.current_formula cs;
|
walther@59923
|
144 |
in
|
walther@59923
|
145 |
if msg = "OK"
|
walther@59923
|
146 |
then
|
walther@59929
|
147 |
case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm) f of
|
walther@59929
|
148 |
SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
|
walther@59929
|
149 |
| NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable")
|
walther@59923
|
150 |
else Applicable.No msg
|
walther@59923
|
151 |
end
|
walther@59929
|
152 |
| check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) =
|
walther@59921
|
153 |
let
|
walther@59921
|
154 |
val pp = Ctree.par_pblobj pt p;
|
walther@59921
|
155 |
val thy' = Ctree.get_obj Ctree.g_domID pt pp;
|
walther@59921
|
156 |
val thy = ThyC.get_theory thy';
|
walther@59921
|
157 |
val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
|
walther@59928
|
158 |
val f = Calc.current_formula cs;
|
walther@59929
|
159 |
val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
|
walther@59921
|
160 |
in
|
walther@59929
|
161 |
case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm) f of
|
walther@59929
|
162 |
SOME (f', asm) =>
|
walther@59929
|
163 |
Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
|
walther@59929
|
164 |
| NONE => Applicable.No (fst thm ^ " not applicable")
|
walther@59921
|
165 |
end
|
walther@59928
|
166 |
| check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =
|
walther@59921
|
167 |
let
|
walther@59923
|
168 |
val pp = Ctree.par_pblobj pt p;
|
walther@59921
|
169 |
val thy' = Ctree.get_obj Ctree.g_domID pt pp;
|
walther@59928
|
170 |
val f = Calc.current_formula cs;
|
walther@59923
|
171 |
in
|
walther@59923
|
172 |
case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
|
walther@59921
|
173 |
SOME (f', asm)
|
walther@59923
|
174 |
=> Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
|
walther@59923
|
175 |
| NONE => Applicable.No (rls ^ " not applicable")
|
walther@59921
|
176 |
end
|
walther@59929
|
177 |
| check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, _))) =
|
walther@59921
|
178 |
let
|
walther@59921
|
179 |
val pp = Ctree.par_pblobj pt p;
|
walther@59921
|
180 |
val thy' = Ctree.get_obj Ctree.g_domID pt pp;
|
walther@59921
|
181 |
val thy = ThyC.get_theory thy';
|
walther@59928
|
182 |
val f = Calc.current_formula cs;
|
walther@59929
|
183 |
val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
|
walther@59921
|
184 |
in
|
walther@59928
|
185 |
case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
|
walther@59928
|
186 |
SOME (f', asm)
|
walther@59921
|
187 |
=> Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
|
walther@59921
|
188 |
| NONE => Applicable.No (rls ^ " not applicable")
|
walther@59921
|
189 |
end
|
walther@59928
|
190 |
| check (Tactic.Subproblem (domID, pblID)) (_, _) =
|
walther@59928
|
191 |
Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
|
walther@59928
|
192 |
TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
|
walther@59936
|
193 |
| check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
|
walther@59928
|
194 |
let
|
walther@59928
|
195 |
val pp = Ctree.par_pblobj pt p
|
walther@59928
|
196 |
val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
|
walther@59928
|
197 |
val f = Calc.current_formula cs;
|
walther@59928
|
198 |
val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
|
walther@59929
|
199 |
val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
|
walther@59928
|
200 |
val subst = Subst.T_from_string_eqs thy sube
|
walther@59928
|
201 |
val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
|
walther@59928
|
202 |
in
|
walther@59928
|
203 |
if foldl and_ (true, map TermC.contains_Var subte)
|
walther@59928
|
204 |
then (*1*)
|
walther@59928
|
205 |
let val f' = subst_atomic subst f
|
walther@59928
|
206 |
in if f = f'
|
walther@59928
|
207 |
then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
|
walther@59928
|
208 |
else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
|
walther@59928
|
209 |
end
|
walther@59928
|
210 |
else (*2*)
|
walther@59928
|
211 |
case Rewrite.rewrite_terms_ thy ro erls subte f of
|
walther@59928
|
212 |
SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
|
walther@59928
|
213 |
| NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
|
walther@59928
|
214 |
end
|
walther@59928
|
215 |
| check (Tactic.Tac id) (cs as (pt, (p, _))) =
|
walther@59929
|
216 |
let
|
walther@59929
|
217 |
val pp = Ctree.par_pblobj pt p;
|
walther@59929
|
218 |
val thy' = Ctree.get_obj Ctree.g_domID pt pp;
|
walther@59929
|
219 |
val thy = ThyC.get_theory thy';
|
walther@59929
|
220 |
val f = Calc.current_formula cs;
|
walther@59936
|
221 |
in
|
walther@59936
|
222 |
Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
|
walther@59921
|
223 |
end
|
walther@59923
|
224 |
| check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
|
walther@59929
|
225 |
| check (Tactic.Begin_Trans) cs =
|
walther@59929
|
226 |
Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs))
|
walther@59923
|
227 |
| check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
|
walther@59923
|
228 |
if p_ = Pos.Res
|
walther@59923
|
229 |
then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
|
walther@59923
|
230 |
else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"
|
walther@59921
|
231 |
| check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
|
walther@59921
|
232 |
| check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
|
walther@59920
|
233 |
|
walther@59935
|
234 |
|
walther@59935
|
235 |
(** Solve_Step.add **)
|
walther@59935
|
236 |
|
walther@59932
|
237 |
fun add (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) =
|
walther@59932
|
238 |
(case topt of
|
walther@59932
|
239 |
SOME t =>
|
walther@59932
|
240 |
let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t
|
walther@59932
|
241 |
in (pos, c, Generate.EmptyMout, pt) end
|
walther@59932
|
242 |
| NONE => (pos, [], Generate.EmptyMout, pt))
|
walther@59932
|
243 |
| add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
|
walther@59931
|
244 |
let
|
walther@59931
|
245 |
val p =
|
walther@59931
|
246 |
let val (ps, p') = split_last p (* no connex to prev.ppobj *)
|
walther@59931
|
247 |
in if p' = 0 then ps @ [1] else p end
|
walther@59931
|
248 |
val (pt, c) = Ctree.cappend_form pt p l t
|
walther@59931
|
249 |
in
|
walther@59931
|
250 |
((p, Pos.Frm), c, Generate.FormKF (UnparseC.term t), pt)
|
walther@59931
|
251 |
end
|
walther@59931
|
252 |
| add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Frm)) =
|
walther@59931
|
253 |
let
|
walther@59931
|
254 |
val (pt, c) = Ctree.cappend_form pt p l t
|
walther@59931
|
255 |
val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*)
|
walther@59931
|
256 |
(* replace the old PrfOjb ~~~~~ *)
|
walther@59931
|
257 |
val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
|
walther@59931
|
258 |
val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)
|
walther@59931
|
259 |
in
|
walther@59931
|
260 |
((p, Pos.Frm), c @ c', Generate.FormKF (UnparseC.term t), pt)
|
walther@59931
|
261 |
end
|
walther@59931
|
262 |
| add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) =
|
walther@59931
|
263 |
(*append after existing PrfObj vvvvvvvvvvvvv*)
|
walther@59931
|
264 |
add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm))
|
walther@59931
|
265 |
| add (Tactic.End_Trans' tasm) l (pt, (p, _)) =
|
walther@59931
|
266 |
let
|
walther@59931
|
267 |
val p' = Pos.lev_up p
|
walther@59931
|
268 |
val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
|
walther@59931
|
269 |
in
|
walther@59931
|
270 |
((p', Pos.Res), c, Generate.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
|
walther@59931
|
271 |
end
|
walther@59931
|
272 |
| add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
|
walther@59931
|
273 |
let
|
walther@59931
|
274 |
val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
|
walther@59931
|
275 |
(Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete;
|
walther@59931
|
276 |
val pt = Ctree.update_branch pt p Ctree.TransitiveB
|
walther@59931
|
277 |
in
|
walther@59931
|
278 |
((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
|
walther@59931
|
279 |
end
|
walther@59931
|
280 |
| add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
|
walther@59931
|
281 |
let
|
walther@59931
|
282 |
val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete
|
walther@59931
|
283 |
val pt = Ctree.update_branch pt p Ctree.TransitiveB
|
walther@59931
|
284 |
in
|
walther@59931
|
285 |
((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
|
walther@59931
|
286 |
end
|
walther@59931
|
287 |
| add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
|
walther@59931
|
288 |
let
|
walther@59931
|
289 |
val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
|
walther@59931
|
290 |
(Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete
|
walther@59931
|
291 |
val pt = Ctree.update_branch pt p Ctree.TransitiveB
|
walther@59931
|
292 |
in
|
walther@59931
|
293 |
((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
|
walther@59931
|
294 |
end
|
walther@59931
|
295 |
| add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
|
walther@59931
|
296 |
let
|
walther@59931
|
297 |
val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
|
walther@59931
|
298 |
(Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
|
walther@59931
|
299 |
val pt = Ctree.update_branch pt p Ctree.TransitiveB
|
walther@59931
|
300 |
in
|
walther@59931
|
301 |
((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
|
walther@59931
|
302 |
end
|
walther@59931
|
303 |
| add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =
|
walther@59931
|
304 |
let
|
walther@59931
|
305 |
val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete
|
walther@59931
|
306 |
in
|
walther@59931
|
307 |
((p, Pos.Res), c, Generate.FormKF (UnparseC.term scval), pt)
|
walther@59931
|
308 |
end
|
walther@59931
|
309 |
| add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) =
|
walther@59931
|
310 |
let
|
walther@59931
|
311 |
val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete
|
walther@59931
|
312 |
in
|
walther@59931
|
313 |
((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
|
walther@59931
|
314 |
end
|
walther@59931
|
315 |
| add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) =
|
walther@59931
|
316 |
let
|
walther@59931
|
317 |
val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete
|
walther@59931
|
318 |
in
|
walther@59931
|
319 |
((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
|
walther@59931
|
320 |
end
|
walther@59931
|
321 |
| add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) =
|
walther@59931
|
322 |
let
|
walther@59931
|
323 |
val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete
|
walther@59931
|
324 |
in
|
walther@59931
|
325 |
((p, Pos.Res), c, Generate.FormKF (UnparseC.term list), pt)
|
walther@59931
|
326 |
end
|
walther@59931
|
327 |
| add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =
|
walther@59931
|
328 |
let
|
walther@59931
|
329 |
val (pt,c) =
|
walther@59931
|
330 |
Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete
|
walther@59931
|
331 |
in ((p, Pos.Res), c, Generate.FormKF (UnparseC.term t'), pt)
|
walther@59931
|
332 |
end
|
walther@59931
|
333 |
| add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =
|
walther@59931
|
334 |
let
|
walther@59931
|
335 |
val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete
|
walther@59931
|
336 |
in
|
walther@59931
|
337 |
((p,Pos.Res), c, Generate.FormKF f', pt)
|
walther@59931
|
338 |
end
|
walther@59931
|
339 |
| add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))
|
walther@59931
|
340 |
(l as (_, ctxt)) (pt, (p, _)) =
|
walther@59932
|
341 |
let
|
walther@59932
|
342 |
val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
|
walther@59932
|
343 |
(oris, (domID, pblID, metID), hdl, ctxt_specify)
|
walther@59932
|
344 |
val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
|
walther@59932
|
345 |
in
|
walther@59932
|
346 |
((p, Pos.Pbl), c, Generate.FormKF f, pt)
|
walther@59932
|
347 |
end
|
walther@59932
|
348 |
| add m' _ (_, pos) =
|
walther@59932
|
349 |
raise ERROR ("Solve_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)
|
walther@59932
|
350 |
|
walther@59932
|
351 |
(* LI switches between solve-phase and specify-phase *)
|
walther@59932
|
352 |
fun add_general tac ic cs =
|
walther@59932
|
353 |
if Tactic.for_specify' tac
|
walther@59933
|
354 |
then Specify_Step.add tac ic cs
|
walther@59932
|
355 |
else add tac ic cs
|
walther@59932
|
356 |
|
walther@59933
|
357 |
(* the order of State_Steps is reversed: insert last element first *)
|
walther@59932
|
358 |
fun s_add_general [] ptp = ptp
|
walther@59932
|
359 |
| s_add_general tacis (pt, c, _) =
|
walther@59931
|
360 |
let
|
walther@59932
|
361 |
val (tacis', (_, tac_, (p, is))) = split_last tacis
|
walther@59933
|
362 |
val (p', c', _, pt') = add_general tac_ is (pt, p)
|
walther@59931
|
363 |
in
|
walther@59932
|
364 |
s_add_general tacis' (pt', c@c', p')
|
walther@59931
|
365 |
end
|
walther@59932
|
366 |
|
walther@59933
|
367 |
(* a still undeveloped concept: do a calculation without LI *)
|
walther@59933
|
368 |
fun add_hard _(*thy*) m' (p, p_) pt =
|
walther@59933
|
369 |
let
|
walther@59933
|
370 |
val p = case p_ of
|
walther@59933
|
371 |
Pos.Frm => p | Pos.Res => Pos.lev_on p
|
walther@59933
|
372 |
| _ => error ("generate_hard: call by " ^ Pos.pos'2str (p,p_))
|
walther@59933
|
373 |
in
|
walther@59933
|
374 |
add_general m' (Istate_Def.empty, ContextC.empty) (pt, (p, p_))
|
walther@59933
|
375 |
end
|
walther@59931
|
376 |
|
walther@59920
|
377 |
(**)end(**);
|