wneuper@59562
|
1 |
(* Title: Interpret/lucas-interpreter.sml
|
wneuper@59554
|
2 |
Author: Walther Neuper 2019
|
wneuper@59554
|
3 |
(c) due to copyright terms
|
wneuper@59554
|
4 |
*)
|
wneuper@59554
|
5 |
|
wneuper@59554
|
6 |
signature LUCAS_INTERPRETER =
|
wneuper@59554
|
7 |
sig
|
walther@59776
|
8 |
datatype next_step_result =
|
walther@59776
|
9 |
Next_Step of Istate.T * Proof.context * Tactic.T
|
walther@59776
|
10 |
| Helpless | End_Program of Istate.T (*TODO ?needed when..*)* Tactic.T
|
walther@59776
|
11 |
val find_next_step: Program.T -> Calc.T -> Istate.T -> Proof.context
|
walther@59776
|
12 |
-> next_step_result
|
walther@59776
|
13 |
|
walther@59747
|
14 |
datatype input_tactic_result =
|
walther@59747
|
15 |
Safe_Step of Istate.T * Proof.context * Tactic.T
|
walther@59655
|
16 |
| Unsafe_Step of Istate.T * Proof.context * Tactic.T
|
walther@59776
|
17 |
| Not_Locatable (*TODO rm..*) of string
|
walther@59776
|
18 |
val locate_input_tactic: Program.T -> Calc.T -> Istate.T -> Proof.context
|
walther@59776
|
19 |
-> Tactic.T -> input_tactic_result
|
wneuper@59557
|
20 |
|
walther@59796
|
21 |
datatype input_term_result = Found_Step of Calc.T | Not_Derivable (**)
|
walther@59796
|
22 |
val locate_input_term: Calc.T -> term -> input_term_result (**)
|
walther@59749
|
23 |
|
walther@59749
|
24 |
(* must reside here:
|
walther@59772
|
25 |
find_next_step calls do_next and is called by by_tactic;
|
walther@59779
|
26 |
by_tactic and do_next are mutually recursive via by_tactic..Apply_Method'
|
walther@59749
|
27 |
*)
|
walther@59981
|
28 |
val by_tactic: Tactic.T -> Istate.T * Proof.context -> Calc.T -> string * Calc.state_post
|
walther@59981
|
29 |
val do_next: Calc.T -> string * Calc.state_post
|
wneuper@59569
|
30 |
|
wneuper@59557
|
31 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59712
|
32 |
datatype expr_val1 =
|
walther@59718
|
33 |
Accept_Tac1 of Istate.pstate * Proof.context * Tactic.T
|
walther@59712
|
34 |
| Reject_Tac1 of Istate.pstate * Proof.context * Tactic.T
|
walther@59713
|
35 |
| Term_Val1 of term;
|
walther@59734
|
36 |
val assoc2str: expr_val1 -> string
|
walther@59796
|
37 |
(* ---- for Doc/Lucas-Interpreter ------------------------------------------------------------- *)
|
walther@59767
|
38 |
val check_Seq_up: Istate.pstate -> term -> term
|
walther@59770
|
39 |
datatype expr_val = Accept_Tac of Tactic.T * Istate.pstate * Proof.context
|
walther@59770
|
40 |
| Reject_Tac | Term_Val of term
|
walther@59767
|
41 |
|
walther@59775
|
42 |
val scan_dn: Calc.T * Proof.context -> Istate.pstate -> term -> expr_val
|
walther@59775
|
43 |
val scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> term -> expr_val
|
walther@59775
|
44 |
val go_scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> expr_val
|
walther@59775
|
45 |
val scan_to_tactic: term * (Calc.T * Proof.context) -> Istate.T -> expr_val
|
walther@59799
|
46 |
val check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option -> expr_val
|
walther@59886
|
47 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59734
|
48 |
val check_Let_up: Istate.pstate -> term -> term * term
|
walther@59981
|
49 |
val compare_step: State_Steps.T * Pos.pos' list * Calc.T -> term -> string * Calc.state_post
|
walther@59686
|
50 |
|
walther@59775
|
51 |
val scan_dn1: (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1
|
walther@59775
|
52 |
val scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
|
walther@59775
|
53 |
val go_scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
|
walther@59775
|
54 |
val scan_to_tactic1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.T -> expr_val1
|
walther@59767
|
55 |
|
walther@59799
|
56 |
val check_tac1: Calc.T * Proof.context * Tactic.T -> Istate.pstate -> term * term option -> expr_val1
|
walther@59886
|
57 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59554
|
58 |
end
|
wneuper@59554
|
59 |
|
walther@59684
|
60 |
(**)
|
walther@59791
|
61 |
structure LI(**): LUCAS_INTERPRETER(**) =
|
wneuper@59554
|
62 |
struct
|
walther@59684
|
63 |
(**)
|
wneuper@59554
|
64 |
open Ctree
|
walther@59695
|
65 |
open Pos
|
walther@59767
|
66 |
open TermC
|
walther@59661
|
67 |
open Istate
|
wneuper@59554
|
68 |
|
walther@59701
|
69 |
(*** auxiliary functions ***)
|
wneuper@59567
|
70 |
|
walther@59767
|
71 |
fun at_location [] t = t
|
walther@59767
|
72 |
| at_location (D :: p) (Abs(_, _, body)) = at_location (p : TermC.path) body
|
walther@59767
|
73 |
| at_location (L :: p) (t1 $ _) = at_location p t1
|
walther@59767
|
74 |
| at_location (R :: p) (_ $ t2) = at_location p t2
|
walther@59962
|
75 |
| at_location l _ = raise ERROR ("at_location: no " ^ TermC.string_of_path l);
|
wneuper@59554
|
76 |
|
walther@59685
|
77 |
fun check_Let_up ({path, ...}: pstate) prog =
|
walther@59767
|
78 |
case at_location (drop_last path) prog of
|
walther@59664
|
79 |
Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (TermC.mk_Free (i, T), body)
|
walther@59868
|
80 |
| t => raise ERROR ("scan_up1..\"HOL.Let $ _\" with: \"" ^ UnparseC.term t ^ "\"")
|
walther@59685
|
81 |
fun check_Seq_up ({path, ...}: pstate) prog =
|
walther@59767
|
82 |
case at_location (drop_last path) prog of
|
walther@59688
|
83 |
Const ("Tactical.Chain",_) $ _ $ e2=> e2
|
walther@59868
|
84 |
| t => raise ERROR ("scan_up1..\"Tactical.Chain $ _\" with: \"" ^ UnparseC.term t ^ "\"")
|
walther@59691
|
85 |
|
walther@59701
|
86 |
|
walther@59796
|
87 |
(*** determine a next tactic within a program ***)
|
walther@59796
|
88 |
|
walther@59796
|
89 |
datatype next_step_result = Next_Step of Istate.T * Proof.context * Tactic.T
|
walther@59796
|
90 |
| Helpless | End_Program of Istate.T * Tactic.T (*contains prog_result, without asms*)
|
walther@59796
|
91 |
|
walther@59796
|
92 |
(** scan to a Prog_Tac **)
|
walther@59796
|
93 |
|
walther@59796
|
94 |
datatype expr_val = (* "ExprVal" in the sense of denotational semantics *)
|
walther@59796
|
95 |
Reject_Tac (* tactic is found but NOT acknowledged, scan is continued *)
|
walther@59796
|
96 |
| Accept_Tac of (* tactic is found and acknowledged, scan is stalled *)
|
walther@59796
|
97 |
Tactic.T * (* Prog_Tac is applicable_in cstate *)
|
walther@59796
|
98 |
Istate.pstate * (* created by application of Tactic.T, for resuming execution *)
|
walther@59796
|
99 |
Proof.context (* created by application of Tactic.T *)
|
walther@59796
|
100 |
| Term_Val of (* Prog_Expr is found and evaluated, scan is continued *)
|
walther@59796
|
101 |
term; (* value of Prog_Expr, for updating environment *)
|
walther@59796
|
102 |
|
walther@59796
|
103 |
(* check if a prog_tac found in a program is applicable_in *)
|
walther@59799
|
104 |
fun check_tac ((pt, p), ctxt) ist (prog_tac, form_arg) =
|
walther@59796
|
105 |
let
|
walther@59825
|
106 |
val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
|
walther@59796
|
107 |
in
|
walther@59824
|
108 |
case m of
|
walther@59825
|
109 |
Tactic.Subproblem _ => (*might involve problem refinement etc*)
|
walther@59825
|
110 |
let
|
walther@59825
|
111 |
val m' = snd (Sub_Problem.tac_from_prog pt prog_tac)
|
walther@59825
|
112 |
in
|
walther@59825
|
113 |
Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'), ctxt)
|
walther@59825
|
114 |
end
|
walther@59796
|
115 |
| _ =>
|
walther@59921
|
116 |
(case Solve_Step.check m (pt, p) of
|
walther@59920
|
117 |
Applicable.Yes m' =>
|
walther@59825
|
118 |
Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'),
|
walther@59824
|
119 |
Tactic.insert_assumptions m' ctxt)
|
walther@59796
|
120 |
| _ => Reject_Tac)
|
walther@59796
|
121 |
end
|
walther@59824
|
122 |
|
walther@59796
|
123 |
|
walther@59796
|
124 |
(*
|
walther@59796
|
125 |
scan_dn, go_scan_up, scan_up scan for find_next_step.
|
walther@59796
|
126 |
(1) scan_dn is recursive descent depth first strictly from L to R;
|
walther@59796
|
127 |
(2) go_scan_up goes to the parent node and calls (3);
|
walther@59796
|
128 |
(3) scan_up resumes according to the interpreter-state.
|
walther@59796
|
129 |
Call of (2) means that there was an applicable Prog_Tac below = before.
|
walther@59796
|
130 |
*)
|
walther@59796
|
131 |
fun scan_dn cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*1*), _) $ e $ a) =
|
walther@59796
|
132 |
(case scan_dn cc (ist|> path_down_form ([L, R], a)) e of
|
walther@59796
|
133 |
Reject_Tac => Term_Val act_arg
|
walther@59796
|
134 |
| (*Accept_Tac*) goback => goback)
|
walther@59796
|
135 |
| scan_dn cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*2*), _) $ e) =
|
walther@59796
|
136 |
(case scan_dn cc (ist |> path_down [R]) e of
|
walther@59796
|
137 |
Reject_Tac => Term_Val act_arg
|
walther@59796
|
138 |
| (*Accept_Tac*) goback => goback)
|
walther@59796
|
139 |
|
walther@59796
|
140 |
| scan_dn cc ist (Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
|
walther@59796
|
141 |
scan_dn cc (ist |> path_down_form ([L, R], a)) e
|
walther@59796
|
142 |
| scan_dn cc ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
|
walther@59796
|
143 |
scan_dn cc (ist |> path_down [R]) e
|
walther@59796
|
144 |
|
walther@59796
|
145 |
| scan_dn cc ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
|
walther@59796
|
146 |
(case scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 of
|
walther@59796
|
147 |
Term_Val v => scan_dn cc (ist |> path_down_form ([L, R], a) |> set_act v) e2
|
walther@59796
|
148 |
| (*Accept_Tac*) goback => goback)
|
walther@59796
|
149 |
| scan_dn cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =
|
walther@59796
|
150 |
(case scan_dn cc (ist |> path_down [L, R]) e1 of
|
walther@59796
|
151 |
Term_Val v => scan_dn cc (ist |> path_down [R] |> set_act v) e2
|
walther@59796
|
152 |
| (*Accept_Tac*) goback => goback)
|
walther@59796
|
153 |
|
walther@59796
|
154 |
| scan_dn cc ist (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b))) =
|
walther@59796
|
155 |
(case scan_dn cc (ist |> path_down [L, R]) e of
|
walther@59796
|
156 |
Term_Val res => scan_dn cc (ist |> path_down [R, D] |> upd_env'' (Free (i, T), res)) b
|
walther@59796
|
157 |
| (*Accept_Tac*) goback => goback)
|
walther@59796
|
158 |
|
walther@59796
|
159 |
| scan_dn (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
|
walther@59799
|
160 |
if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
|
walther@59796
|
161 |
then scan_dn cc (ist |> path_down_form ([L, R], a)) e
|
walther@59796
|
162 |
else Term_Val act_arg
|
walther@59796
|
163 |
| scan_dn (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
|
walther@59799
|
164 |
if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
|
walther@59796
|
165 |
then scan_dn cc (ist |> path_down [R]) e
|
walther@59796
|
166 |
else Term_Val act_arg
|
walther@59796
|
167 |
|
walther@59796
|
168 |
|scan_dn cc ist (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
|
walther@59796
|
169 |
(case scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 of
|
walther@59796
|
170 |
Accept_Tac lme => Accept_Tac lme
|
walther@59796
|
171 |
| _ => scan_dn cc (ist |> path_down_form ([L, R], a)) e2)
|
walther@59796
|
172 |
| scan_dn cc ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
|
walther@59796
|
173 |
(case scan_dn cc (ist |> path_down [L, R]) e1 of
|
walther@59796
|
174 |
Accept_Tac lme => Accept_Tac lme
|
walther@59796
|
175 |
| _ => scan_dn cc (ist |> path_down [R]) e2)
|
walther@59796
|
176 |
|
walther@59796
|
177 |
| scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.If"(*1*), _) $ c $ e1 $ e2) =
|
walther@59799
|
178 |
if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
|
walther@59796
|
179 |
then scan_dn cc (ist |> path_down [L, R]) e1
|
walther@59796
|
180 |
else scan_dn cc (ist |> path_down [R]) e2
|
walther@59796
|
181 |
|
walther@59796
|
182 |
| scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t =
|
walther@59796
|
183 |
if Tactical.contained_in t
|
walther@59796
|
184 |
then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t])
|
walther@59796
|
185 |
else
|
walther@59796
|
186 |
case LItool.check_leaf "next " ctxt eval (get_subst ist) t of
|
walther@59796
|
187 |
(Program.Expr s, _) => Term_Val s (*TODO?: include set_found here and drop those after call*)
|
walther@59796
|
188 |
| (Program.Tac prog_tac, form_arg) =>
|
walther@59799
|
189 |
check_tac cc ist (prog_tac, form_arg)
|
walther@59796
|
190 |
|
walther@59796
|
191 |
fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) =
|
walther@59848
|
192 |
if path = [R] (*root of the program body*) then
|
walther@59848
|
193 |
if found_accept then
|
walther@59848
|
194 |
Term_Val act_arg
|
walther@59796
|
195 |
else raise ERROR "LItool.find_next_step without result"
|
walther@59796
|
196 |
else scan_up pcc (ist |> path_up) (go_up path sc)
|
walther@59796
|
197 |
(* scan is strictly to R, because at L there was an \<open>expr_val\<close> *)
|
walther@59796
|
198 |
and scan_up pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up pcc ist
|
walther@59796
|
199 |
| scan_up pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up pcc ist
|
walther@59796
|
200 |
|
walther@59796
|
201 |
| scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =
|
walther@59796
|
202 |
(case scan_dn cc (ist |> path_down [L, R]) e of
|
walther@59796
|
203 |
Accept_Tac ict => Accept_Tac ict
|
walther@59796
|
204 |
| Reject_Tac => go_scan_up pcc ist
|
walther@59796
|
205 |
| Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))
|
walther@59796
|
206 |
| scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
|
walther@59796
|
207 |
(case scan_dn cc (ist |> path_down [R]) e of
|
walther@59796
|
208 |
Accept_Tac ict => Accept_Tac ict
|
walther@59796
|
209 |
| Reject_Tac => go_scan_up pcc ist
|
walther@59796
|
210 |
| Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))
|
walther@59796
|
211 |
|
walther@59796
|
212 |
| scan_up pcc ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
|
walther@59796
|
213 |
| scan_up pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up pcc ist
|
walther@59796
|
214 |
| scan_up (pcc as (sc, cc)) ist (Const ("Tactical.Chain"(*3*), _) $ _) =
|
walther@59796
|
215 |
let
|
walther@59796
|
216 |
val e2 = check_Seq_up ist sc
|
walther@59796
|
217 |
in
|
walther@59796
|
218 |
case scan_dn cc (ist |> path_up_down [R]) e2 of
|
walther@59796
|
219 |
Accept_Tac ict => Accept_Tac ict
|
walther@59796
|
220 |
| Reject_Tac => go_scan_up pcc (ist |> path_up)
|
walther@59796
|
221 |
| Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> set_found)
|
walther@59796
|
222 |
end
|
walther@59796
|
223 |
|
walther@59796
|
224 |
| scan_up (pcc as (sc, cc)) ist (Const ("HOL.Let"(*1*), _) $ _) =
|
walther@59796
|
225 |
let
|
walther@59796
|
226 |
val (i, body) = check_Let_up ist sc
|
walther@59796
|
227 |
in
|
walther@59796
|
228 |
case scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body of
|
walther@59796
|
229 |
Accept_Tac ict => Accept_Tac ict
|
walther@59796
|
230 |
| Reject_Tac => go_scan_up pcc (ist |> path_up)
|
walther@59796
|
231 |
| Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> set_found)
|
walther@59796
|
232 |
end
|
walther@59796
|
233 |
| scan_up pcc ist (Abs _(*2*)) = go_scan_up pcc ist
|
walther@59796
|
234 |
| scan_up pcc ist (Const ("HOL.Let"(*3*), _) $ _ $ (Abs _)) = go_scan_up pcc ist
|
walther@59796
|
235 |
|
walther@59796
|
236 |
| scan_up (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...})
|
walther@59796
|
237 |
(Const ("Tactical.While"(*1*), _) $ c $ e $ _) =
|
walther@59799
|
238 |
if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
|
walther@59796
|
239 |
then
|
walther@59796
|
240 |
case scan_dn cc (ist |> path_down [L, R]) e of
|
walther@59796
|
241 |
Accept_Tac ict => Accept_Tac ict
|
walther@59796
|
242 |
| Reject_Tac => go_scan_up pcc ist
|
walther@59796
|
243 |
| Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found)
|
walther@59796
|
244 |
else
|
walther@59796
|
245 |
go_scan_up pcc (ist (*|> set_found*))
|
walther@59796
|
246 |
| scan_up (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...})
|
walther@59796
|
247 |
(Const ("Tactical.While"(*2*), _) $ c $ e) =
|
walther@59799
|
248 |
if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
|
walther@59796
|
249 |
then
|
walther@59796
|
250 |
case scan_dn cc (ist |> path_down [R]) e of
|
walther@59796
|
251 |
Accept_Tac ict => Accept_Tac ict
|
walther@59796
|
252 |
| Reject_Tac => go_scan_up pcc ist
|
walther@59796
|
253 |
| Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found)
|
walther@59796
|
254 |
else
|
walther@59796
|
255 |
go_scan_up pcc ist
|
walther@59796
|
256 |
|
walther@59796
|
257 |
| scan_up pcc ist (Const ("Tactical.Or"(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
|
walther@59796
|
258 |
| scan_up pcc ist (Const ("Tactical.Or"(*2*), _) $ _ $ _) = go_scan_up pcc ist
|
walther@59796
|
259 |
| scan_up pcc ist (Const ("Tactical.Or"(*3*), _) $ _ ) = go_scan_up pcc ist
|
walther@59796
|
260 |
|
walther@59796
|
261 |
| scan_up pcc ist (Const ("Tactical.If"(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
|
walther@59796
|
262 |
|
walther@59962
|
263 |
| scan_up _ _ t = raise ERROR ("scan_up not impl for " ^ UnparseC.term t)
|
walther@59796
|
264 |
|
walther@59796
|
265 |
(* scan program until an applicable tactic is found *)
|
walther@59796
|
266 |
fun scan_to_tactic (prog, cc) (Pstate (ist as {path, ...})) =
|
walther@59848
|
267 |
if path = [] then
|
walther@59848
|
268 |
scan_dn cc (trans_scan_dn ist) (Program.body_of prog)
|
walther@59796
|
269 |
else go_scan_up (prog, cc) (trans_scan_up ist)
|
walther@59796
|
270 |
| scan_to_tactic _ _ = raise ERROR "scan_to_tactic: uncovered pattern";
|
walther@59796
|
271 |
|
walther@59796
|
272 |
(* find the next applicable Prog_Tac in a prog *)
|
walther@59796
|
273 |
fun find_next_step (Rule.Prog prog) (ptp as(pt, (p, _))) (Pstate ist) ctxt =
|
walther@59796
|
274 |
(case scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) of
|
walther@59796
|
275 |
Accept_Tac (tac, ist, ctxt) =>
|
walther@59796
|
276 |
Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac)
|
walther@59796
|
277 |
| Term_Val prog_result =>
|
walther@59838
|
278 |
(case parent_node pt p of
|
walther@59796
|
279 |
(true, p', _) =>
|
walther@59796
|
280 |
let
|
walther@59796
|
281 |
val (_, pblID, _) = get_obj g_spec pt p';
|
walther@59796
|
282 |
in
|
walther@59843
|
283 |
End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
|
walther@59796
|
284 |
end
|
walther@59861
|
285 |
| _ => End_Program (Pstate ist, Tactic.End_Detail' (TermC.empty,[])))
|
walther@59796
|
286 |
| Reject_Tac => Helpless)
|
walther@59796
|
287 |
| find_next_step _ _ ist _ =
|
walther@59844
|
288 |
raise ERROR ("find_next_step: not impl for " ^ Istate.string_of ist);
|
walther@59796
|
289 |
|
walther@59796
|
290 |
|
walther@59701
|
291 |
(*** locate an input tactic within a program ***)
|
walther@59691
|
292 |
|
walther@59691
|
293 |
datatype input_tactic_result =
|
walther@59691
|
294 |
Safe_Step of Istate.T * Proof.context * Tactic.T
|
walther@59691
|
295 |
| Unsafe_Step of Istate.T * Proof.context * Tactic.T
|
walther@59691
|
296 |
| Not_Locatable of string
|
walther@59691
|
297 |
|
walther@59796
|
298 |
(*all functions ending with "1" are supposed to be replaced by those without "1"*)
|
walther@59712
|
299 |
datatype expr_val1 = (* "ExprVal" in the sense of denotational semantics *)
|
walther@59712
|
300 |
Reject_Tac1 of (* tactic is found but NOT acknowledged, scan is continued *)
|
walther@59770
|
301 |
Istate.pstate * Proof.context * Tactic.T (*TODO: revise Pstate {or,...},no args as Reject_Tac*)
|
walther@59796
|
302 |
| Accept_Tac1 of (* tactic is found and acknowledged, scan is stalled *)
|
walther@59712
|
303 |
Istate.pstate * (* the current state, returned for resuming execution *)
|
walther@59712
|
304 |
Proof.context * (* updated according to evaluation of Prog_Tac *)
|
walther@59712
|
305 |
Tactic.T (* Prog_Tac is associated to Tactic.input *)
|
walther@59712
|
306 |
| Term_Val1 of (* Prog_Expr is found and evaluated, scan is continued *)
|
walther@59712
|
307 |
term (* value of Prog_Expr, for updating environment *)
|
walther@59718
|
308 |
fun assoc2str (Accept_Tac1 _) = "Accept_Tac1"
|
walther@59712
|
309 |
| assoc2str (Term_Val1 _) = "Term_Val1"
|
walther@59712
|
310 |
| assoc2str (Reject_Tac1 _) = "Reject_Tac1";
|
walther@59691
|
311 |
|
walther@59701
|
312 |
|
walther@59796
|
313 |
(** check a Prog_Tac: is it associated to Tactic ? **)
|
walther@59718
|
314 |
|
walther@59799
|
315 |
fun check_tac1 ((pt, p), ctxt, tac) (ist as {act_arg, or, ...}) (prog_tac, form_arg) =
|
walther@59790
|
316 |
case LItool.associate pt ctxt (tac, prog_tac) of
|
walther@59844
|
317 |
LItool.Associated (m, v', ctxt)
|
walther@59787
|
318 |
=> Accept_Tac1 (ist |> set_subst_true (form_arg, v') |> set_found, ctxt, m)
|
walther@59790
|
319 |
| LItool.Ass_Weak (m, v', ctxt) (*the ONLY ones in locate_tac ^v^v^v^v^ *)
|
walther@59787
|
320 |
=> Accept_Tac1 (ist |> set_subst_false (form_arg, v') |> set_found, ctxt, m)
|
walther@59844
|
321 |
| LItool.Not_Associated =>
|
walther@59718
|
322 |
(case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
|
walther@59718
|
323 |
AssOnly => Term_Val1 act_arg
|
walther@59718
|
324 |
| _(*ORundef*) =>
|
walther@59921
|
325 |
case Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) of
|
walther@59920
|
326 |
Applicable.Yes m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
|
walther@59920
|
327 |
| Applicable.No _ => Term_Val1 act_arg)
|
walther@59718
|
328 |
|
walther@59701
|
329 |
(** scan to a Prog_Tac **)
|
walther@59701
|
330 |
|
walther@59779
|
331 |
(* scan is strictly first L, then R; tacticals have 2 args at maximum *)
|
walther@59700
|
332 |
fun scan_dn1 cct ist (Const ("Tactical.Try"(*1*), _) $ e $ a) =
|
walther@59701
|
333 |
(case scan_dn1 cct (ist |> path_down_form ([L, R], a)) e of goback => goback)
|
walther@59700
|
334 |
| scan_dn1 cct ist (Const ("Tactical.Try"(*2*), _) $ e) =
|
walther@59701
|
335 |
(case scan_dn1 cct (ist |> path_down [R]) e of goback => goback)
|
walther@59691
|
336 |
|
walther@59700
|
337 |
| scan_dn1 cct ist (Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
|
walther@59701
|
338 |
scan_dn1 cct (ist |> path_down_form ([L, R], a)) e
|
walther@59700
|
339 |
| scan_dn1 cct ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
|
walther@59700
|
340 |
scan_dn1 cct (ist |> path_down [R]) e
|
walther@59691
|
341 |
|
walther@59709
|
342 |
| scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
|
walther@59700
|
343 |
(case scan_dn1 cct (ist |> path_down_form ([L, L, R], a)) e1 of
|
walther@59712
|
344 |
Term_Val1 v => scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v)) e2
|
walther@59712
|
345 |
| Reject_Tac1 (ist', ctxt', tac') => scan_dn1 (cstate, ctxt', tac') (ist
|
walther@59712
|
346 |
|> path_down_form ([L, R], a) |> trans_env_act ist') e2
|
walther@59701
|
347 |
| goback => goback)
|
walther@59709
|
348 |
| scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*2*), _) $e1 $ e2) =
|
walther@59700
|
349 |
(case scan_dn1 cct (ist |> path_down [L, R]) e1 of
|
walther@59712
|
350 |
Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
|
walther@59712
|
351 |
| Reject_Tac1 (ist', ctxt', tac') =>
|
walther@59712
|
352 |
scan_dn1 (cstate, ctxt', tac') (ist |> path_down [R] |> trans_env_act ist') e2
|
walther@59701
|
353 |
| goback => goback)
|
walther@59691
|
354 |
|
walther@59709
|
355 |
| scan_dn1 cct ist (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))) =
|
walther@59700
|
356 |
(case scan_dn1 cct (ist |> path_down [L, R]) e of
|
walther@59712
|
357 |
Reject_Tac1 (ist', _, _) =>
|
walther@59700
|
358 |
scan_dn1 cct (ist' |> path_down [R, D] |> upd_env (TermC.mk_Free (id, T)) |> trans_ass ist) b
|
walther@59712
|
359 |
| Term_Val1 v =>
|
walther@59709
|
360 |
scan_dn1 cct (ist |> path_down [R, D] |> upd_env'' (TermC.mk_Free (id, T), v)) b
|
walther@59703
|
361 |
| goback => goback)
|
walther@59691
|
362 |
|
walther@59722
|
363 |
| scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, act_arg, ...})
|
walther@59722
|
364 |
(Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
|
walther@59799
|
365 |
if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
|
walther@59703
|
366 |
then scan_dn1 cct (ist |> path_down_form ([L, R], a)) e
|
walther@59712
|
367 |
else Term_Val1 act_arg
|
walther@59722
|
368 |
| scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, act_arg, ...})
|
walther@59722
|
369 |
(Const ("Tactical.While"(*2*),_) $ c $ e) =
|
walther@59799
|
370 |
if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
|
walther@59700
|
371 |
then scan_dn1 cct (ist |> path_down [R]) e
|
walther@59712
|
372 |
else Term_Val1 act_arg
|
walther@59691
|
373 |
|
walther@59718
|
374 |
| scan_dn1 cct (ist as {or = ORundef, ...}) (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
|
walther@59700
|
375 |
(case scan_dn1 cct (ist |> path_down_form ([L, L, R], a) |> set_or AssOnly) e1 of
|
walther@59712
|
376 |
Term_Val1 v =>
|
walther@59709
|
377 |
(case scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v) |> set_or AssOnly) e2 of
|
walther@59712
|
378 |
Term_Val1 v =>
|
walther@59709
|
379 |
(case scan_dn1 cct (ist |> path_down [L, L, R] |> upd_env'' (a, v) |> set_or AssGen) e1 of
|
walther@59712
|
380 |
Term_Val1 v =>
|
walther@59709
|
381 |
scan_dn1 cct (ist |> path_down [L, R] |> upd_env'' (a, v) |> set_or AssGen) e2
|
walther@59703
|
382 |
| goback => goback)
|
walther@59703
|
383 |
| goback => goback)
|
walther@59712
|
384 |
| Reject_Tac1 _ => raise ERROR ("scan_dn1 Tactical.Or(*1*): must not return Reject_Tac1")
|
walther@59703
|
385 |
| goback => goback)
|
walther@59710
|
386 |
| scan_dn1 cct ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
|
walther@59700
|
387 |
(case scan_dn1 cct (ist |> path_down [L, R]) e1 of
|
walther@59712
|
388 |
Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
|
walther@59703
|
389 |
| goback => goback)
|
walther@59691
|
390 |
|
walther@59722
|
391 |
| scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, ...}) (Const ("Tactical.If", _) $ c $ e1 $ e2) =
|
walther@59799
|
392 |
if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
|
walther@59700
|
393 |
then scan_dn1 cct (ist |> path_down [L, R]) e1
|
walther@59700
|
394 |
else scan_dn1 cct (ist |> path_down [R]) e2
|
walther@59691
|
395 |
|
walther@59719
|
396 |
| scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, ...}) t =
|
walther@59716
|
397 |
if Tactical.contained_in t then raise TERM ("scan_dn1 expects Prog_Tac or Prog_Expr", [t])
|
walther@59717
|
398 |
else
|
walther@59790
|
399 |
case LItool.check_leaf "locate" ctxt eval (get_subst ist) t of
|
walther@59731
|
400 |
(Program.Expr _, form_arg) =>
|
walther@59731
|
401 |
Term_Val1 (Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) eval
|
walther@59731
|
402 |
(subst_atomic (Env.update_opt'' (get_act_env ist, form_arg)) t))
|
walther@59731
|
403 |
| (Program.Tac prog_tac, form_arg) =>
|
walther@59799
|
404 |
check_tac1 cct ist (prog_tac, form_arg)
|
walther@59691
|
405 |
|
walther@59720
|
406 |
fun go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
|
walther@59848
|
407 |
if 1 < length path then
|
walther@59848
|
408 |
scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog)
|
walther@59720
|
409 |
else Term_Val1 act_arg
|
walther@59779
|
410 |
(* scan is strictly to R, because at L there was a expr_val *)
|
walther@59720
|
411 |
and scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
|
walther@59700
|
412 |
| scan_up1 pcct ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up1 pcct ist
|
walther@59691
|
413 |
|
walther@59709
|
414 |
| scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
|
walther@59718
|
415 |
(case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
|
walther@59712
|
416 |
Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
|
walther@59712
|
417 |
| Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
|
walther@59703
|
418 |
| goback => goback)
|
walther@59710
|
419 |
| scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*2*), _) $ e) =
|
walther@59718
|
420 |
(case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
|
walther@59712
|
421 |
Term_Val1 v' => go_scan_up1 pcct (ist |> set_act v')
|
walther@59712
|
422 |
| Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
|
walther@59703
|
423 |
| goback => goback)
|
walther@59691
|
424 |
|
walther@59703
|
425 |
(*all has been done in (*2*) below*)
|
walther@59700
|
426 |
| scan_up1 pcct ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
|
walther@59718
|
427 |
| scan_up1 pcct ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist (*comes from e2*)
|
walther@59709
|
428 |
| scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const ("Tactical.Chain"(*3*), _) $ _ ) =
|
walther@59691
|
429 |
let
|
walther@59718
|
430 |
val e2 = check_Seq_up ist prog (*comes from e1, goes to e2*)
|
walther@59691
|
431 |
in
|
walther@59718
|
432 |
case scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 of
|
walther@59712
|
433 |
Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
|
walther@59712
|
434 |
| Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
|
walther@59703
|
435 |
| goback => goback
|
walther@59691
|
436 |
end
|
walther@59691
|
437 |
|
walther@59709
|
438 |
| scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const ("HOL.Let"(*1*), _) $ _) =
|
walther@59691
|
439 |
let
|
walther@59692
|
440 |
val (i, body) = check_Let_up ist prog
|
walther@59718
|
441 |
in case scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body of
|
walther@59718
|
442 |
Accept_Tac1 iss => Accept_Tac1 iss
|
walther@59712
|
443 |
| Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
|
walther@59712
|
444 |
| Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
|
walther@59691
|
445 |
end
|
walther@59700
|
446 |
| scan_up1 pcct ist (Abs(*2*) _) = go_scan_up1 pcct ist
|
walther@59700
|
447 |
| scan_up1 pcct ist (Const ("HOL.Let"(*3*), _) $ _ $ (Abs _)) = go_scan_up1 pcct ist
|
walther@59691
|
448 |
|
walther@59722
|
449 |
| scan_up1 (pcct as (prog, cct as (cstate, ctxt, _))) (ist as {eval, ...})
|
walther@59703
|
450 |
(t as Const ("Tactical.While"(*1*),_) $ c $ e $ a) =
|
walther@59722
|
451 |
if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update' a (get_act_env ist)) c)
|
walther@59691
|
452 |
then
|
walther@59718
|
453 |
case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
|
walther@59712
|
454 |
Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
|
walther@59691
|
455 |
|
walther@59712
|
456 |
| Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
|
walther@59703
|
457 |
| goback => goback
|
walther@59700
|
458 |
else go_scan_up1 pcct (ist |> set_form a)
|
walther@59722
|
459 |
| scan_up1 (pcct as (prog, cct as (cstate, ctxt, _))) (ist as {eval, ...})
|
walther@59703
|
460 |
(t as Const ("Tactical.While"(*2*), _) $ c $ e) =
|
walther@59722
|
461 |
if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
|
walther@59691
|
462 |
then
|
walther@59718
|
463 |
case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
|
walther@59712
|
464 |
Term_Val1 v => go_scan_up1 pcct (ist |> set_act v)
|
walther@59712
|
465 |
| Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
|
walther@59703
|
466 |
| goback => goback
|
walther@59700
|
467 |
else go_scan_up1 pcct ist
|
walther@59691
|
468 |
|
walther@59700
|
469 |
| scan_up1 pcct ist (Const ("If", _) $ _ $ _ $ _) = go_scan_up1 pcct ist
|
walther@59691
|
470 |
|
walther@59700
|
471 |
| scan_up1 pcct ist (Const ("Tactical.Or"(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
|
walther@59700
|
472 |
| scan_up1 pcct ist (Const ("Tactical.Or"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist
|
walther@59700
|
473 |
| scan_up1 pcct ist (Const ("Tactical.Or"(*3*), _) $ _ ) = go_scan_up1 pcct (ist |> path_up)
|
walther@59691
|
474 |
|
walther@59700
|
475 |
| scan_up1 pcct ist (Const ("Tactical.If",_) $ _ $ _ $ _) = go_scan_up1 pcct ist
|
walther@59691
|
476 |
|
walther@59962
|
477 |
| scan_up1 _ _ t = raise ERROR ("scan_up1 not impl for t= " ^ UnparseC.term t)
|
walther@59691
|
478 |
|
walther@59774
|
479 |
fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Pstate (ist as {path, ...})) =
|
walther@59772
|
480 |
if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH find_next_step IN solve*)p
|
walther@59718
|
481 |
then scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog)
|
walther@59692
|
482 |
else go_scan_up1 (prog, cctt) ist
|
walther@59691
|
483 |
| scan_to_tactic1 _ _ = raise ERROR "scan_to_tactic1: uncovered pattern in fun.def"
|
walther@59691
|
484 |
|
walther@59701
|
485 |
(*locate an input tactic within a program*)
|
walther@59699
|
486 |
fun locate_input_tactic (Rule.Prog prog) cstate istate ctxt tac =
|
walther@59699
|
487 |
(case scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate of
|
walther@59718
|
488 |
Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac') =>
|
walther@59848
|
489 |
if assoc then
|
walther@59848
|
490 |
Safe_Step (Pstate ist, ctxt, tac')
|
walther@59774
|
491 |
else Unsafe_Step (Pstate ist, ctxt, tac')
|
walther@59728
|
492 |
| Reject_Tac1 _ => Not_Locatable (Tactic.string_of tac ^ " not locatable")
|
walther@59845
|
493 |
| err => raise ERROR ("not-found-in-program: NotLocatable from " ^ @{make_string} err))
|
walther@59691
|
494 |
| locate_input_tactic _ _ _ _ _ = raise ERROR "locate_input_tactic: uncovered case in definition"
|
walther@59691
|
495 |
|
walther@59837
|
496 |
|
walther@59796
|
497 |
(*** locate an input formula within a program ***)
|
wneuper@59569
|
498 |
|
walther@59795
|
499 |
datatype input_term_result = Found_Step of Calc.T | Not_Derivable
|
wneuper@59562
|
500 |
|
walther@59751
|
501 |
fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
|
walther@59848
|
502 |
let
|
walther@59848
|
503 |
val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
|
walther@59848
|
504 |
PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
|
walther@59962
|
505 |
| _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
|
walther@59970
|
506 |
val {ppc, ...} = Method.from_store mI;
|
walther@59988
|
507 |
val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
|
walther@59975
|
508 |
val itms = Step_Specify.hack_until_review_Specify_1 mI itms
|
walther@59848
|
509 |
val srls = LItool.get_simplifier (pt, pos)
|
walther@59848
|
510 |
val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
|
walther@59848
|
511 |
(is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
|
walther@59962
|
512 |
| _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
|
walther@59848
|
513 |
val ini = LItool.implicit_take prog env;
|
walther@59848
|
514 |
val pos = start_new_level pos
|
walther@59848
|
515 |
in
|
walther@59848
|
516 |
case ini of
|
walther@59848
|
517 |
SOME t =>
|
walther@59848
|
518 |
let (* implicit Take *)
|
walther@59848
|
519 |
val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
|
walther@59932
|
520 |
val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos)
|
walther@59848
|
521 |
in
|
walther@59848
|
522 |
("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
|
walther@59848
|
523 |
end
|
walther@59848
|
524 |
| NONE =>
|
walther@59848
|
525 |
let
|
walther@59848
|
526 |
val (tac', ist', ctxt') =
|
walther@59848
|
527 |
case find_next_step prog (pt, (lev_dn p, Res)) is ctxt of
|
walther@59848
|
528 |
Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
|
walther@59848
|
529 |
| _ => raise ERROR ("LI.by_tactic..Apply_Method find_next_step \<rightarrow> " ^ strs2str' mI)
|
walther@59848
|
530 |
in
|
walther@59848
|
531 |
case tac' of
|
walther@59848
|
532 |
Tactic.Take' t =>
|
walther@59848
|
533 |
let (* explicit Take *)
|
walther@59848
|
534 |
val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');
|
walther@59932
|
535 |
val (pos, c, _, pt) = Solve_Step.add show_add (ist', ctxt') (pt, pos)
|
walther@59848
|
536 |
in
|
walther@59848
|
537 |
("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
|
walther@59848
|
538 |
end
|
walther@59848
|
539 |
| add as Tactic.Subproblem' (_, _, headline, _, _, _) =>
|
walther@59848
|
540 |
let (* Subproblem *)
|
walther@59848
|
541 |
val show = Tactic.Apply_Method' (mI, SOME headline, ist', ctxt');
|
walther@59932
|
542 |
val (pos, c, _, pt) = Solve_Step.add add (ist', ctxt') (pt, pos)
|
walther@59848
|
543 |
in
|
walther@59848
|
544 |
("ok", ([(Tactic.Apply_Method mI, show, (pos, (ist', ctxt')))], c, (pt, pos)))
|
walther@59848
|
545 |
end
|
walther@59848
|
546 |
| tac =>
|
walther@59848
|
547 |
raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of tac)
|
walther@59848
|
548 |
end
|
walther@59848
|
549 |
end
|
walther@59842
|
550 |
| by_tactic (Tactic.Check_Postcond' (pI, _)) (sub_ist, sub_ctxt) (pt, pos as (p, _)) =
|
walther@59848
|
551 |
let
|
walther@59848
|
552 |
val parent_pos = par_pblobj pt p
|
walther@59970
|
553 |
val {scr, ...} = Method.from_store (get_obj g_metID pt parent_pos);
|
walther@59848
|
554 |
val prog_res =
|
walther@59848
|
555 |
case find_next_step scr (pt, pos) sub_ist sub_ctxt of
|
walther@59848
|
556 |
(*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
|
walther@59848
|
557 |
|(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
|
walther@59848
|
558 |
| _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
|
walther@59848
|
559 |
in
|
walther@59848
|
560 |
if parent_pos = [] then
|
walther@59848
|
561 |
let
|
walther@59848
|
562 |
val tac = Tactic.Check_Postcond' (pI, prog_res)
|
walther@59848
|
563 |
val is = Pstate (sub_ist |> the_pstate |> set_act prog_res |> set_found)
|
walther@59932
|
564 |
val ((p, p_), ps, _, pt) = Solve_Step.add_general tac (is, sub_ctxt) (pt, (parent_pos, Res))
|
walther@59848
|
565 |
in
|
walther@59848
|
566 |
("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is, sub_ctxt)))], ps, (pt, (p, p_))))
|
walther@59848
|
567 |
end
|
walther@59848
|
568 |
else
|
walther@59848
|
569 |
let (*resume program of parent PblObj, transfer result of Subproblem-program*)
|
walther@59848
|
570 |
val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
|
walther@59848
|
571 |
(Pstate i, c) => (i, c)
|
walther@59962
|
572 |
| _ => raise ERROR "LI.by_tactic Check_Postcond': uncovered case get_loc"
|
walther@59848
|
573 |
val (prog_res', ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent
|
walther@59848
|
574 |
val tac = Tactic.Check_Postcond' (pI, prog_res')
|
walther@59848
|
575 |
val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
|
walther@59932
|
576 |
val ((p, p_), ps, _, pt) = Solve_Step.add_general tac (ist', ctxt') (pt, (parent_pos, Res))
|
walther@59848
|
577 |
in
|
walther@59848
|
578 |
("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))
|
walther@59848
|
579 |
end
|
walther@59848
|
580 |
end
|
walther@59762
|
581 |
| by_tactic (Tactic.End_Proof'') _ ptp = ("end-of-calculation", ([], [], ptp))
|
walther@59837
|
582 |
| by_tactic tac_ ic (pt, pos) =
|
wneuper@59555
|
583 |
let
|
walther@59759
|
584 |
val pos = next_in_prog' pos
|
walther@59932
|
585 |
val (pos', c, _, pt) = Solve_Step.add_general tac_ ic (pt, pos);
|
wneuper@59555
|
586 |
in
|
walther@59837
|
587 |
("ok", ([(Tactic.input_from_T tac_, tac_, (pos, ic))], c, (pt, pos')))
|
wneuper@59555
|
588 |
end
|
walther@59772
|
589 |
(*find_next_step from program, by_tactic will update Ctree*)
|
walther@59760
|
590 |
and do_next (ptp as (pt, pos as (p, p_))) =
|
walther@59903
|
591 |
if Method.id_empty = get_obj g_metID pt (par_pblobj pt p) then
|
walther@59848
|
592 |
("helpless", ([], [], (pt, (p, p_))))
|
wneuper@59555
|
593 |
else
|
wneuper@59555
|
594 |
let
|
wneuper@59555
|
595 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@59831
|
596 |
val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
|
walther@59745
|
597 |
in
|
walther@59772
|
598 |
case find_next_step sc (pt, pos) ist ctxt of
|
walther@59745
|
599 |
Next_Step (ist, ctxt, tac) =>
|
walther@59751
|
600 |
by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp
|
walther@59842
|
601 |
| End_Program (ist, tac) => (*TODO RM ..*)
|
walther@59745
|
602 |
(case tac of
|
walther@59745
|
603 |
Tactic.End_Detail' res =>
|
walther@59762
|
604 |
("ok", ([(Tactic.End_Detail,
|
walther@59762
|
605 |
Tactic.End_Detail' res, (pos, (ist, ctxt)))], [], ptp))
|
walther@59842
|
606 |
| _ => (*.. RM*) by_tactic tac (ist, ctxt) ptp
|
walther@59762
|
607 |
)
|
walther@59981
|
608 |
| Helpless => ("helpless", Calc.state_empty_post)
|
walther@59745
|
609 |
end;
|
walther@59686
|
610 |
|
walther@59701
|
611 |
(*
|
walther@59701
|
612 |
compare inform with ctree.form at current pos by nrls;
|
walther@59701
|
613 |
if found, embed the derivation generated during comparison
|
walther@59934
|
614 |
if not, let the mat-engine compute the next Calc.result
|
walther@59701
|
615 |
|
walther@59934
|
616 |
TODO: find code in common with complete_solve
|
walther@59701
|
617 |
*)
|
walther@59848
|
618 |
fun compare_step (tacis, c, ptp as (pt, pos as (p, _))) ifo =
|
wneuper@59555
|
619 |
let
|
walther@59928
|
620 |
val fo = Calc.current_formula ptp
|
walther@59970
|
621 |
val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
|
walther@59852
|
622 |
val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
|
walther@59907
|
623 |
val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
|
wneuper@59555
|
624 |
in
|
wneuper@59555
|
625 |
if found
|
wneuper@59555
|
626 |
then
|
wneuper@59555
|
627 |
let
|
walther@59908
|
628 |
val tacis' = map (State_Steps.make_single rew_ord erls) der;
|
walther@59932
|
629 |
val (c', ptp) = Derive.embed tacis' ptp;
|
wneuper@59555
|
630 |
in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
|
wneuper@59555
|
631 |
else
|
walther@59694
|
632 |
if pos = ([], Pos.Res) (*TODO: we should stop earlier with trying subproblems *)
|
walther@59981
|
633 |
then ("no derivation found", (tacis, c, ptp): Calc.state_post)
|
wneuper@59555
|
634 |
else
|
wneuper@59555
|
635 |
let
|
walther@59762
|
636 |
val msg_cs' as (_, (tacis, c', ptp)) = do_next ptp; (*<---------------------*)
|
walther@59762
|
637 |
val (_, (tacis, c'', ptp)) = case tacis of
|
walther@59820
|
638 |
((Tactic.Subproblem _, _, _) :: _) =>
|
wneuper@59555
|
639 |
let
|
walther@59977
|
640 |
val ptp as (pt, (p, _)) = Specification.all_modspec ptp (*<--------------------*)
|
wneuper@59555
|
641 |
val mI = Ctree.get_obj Ctree.g_metID pt p
|
wneuper@59555
|
642 |
in
|
walther@59846
|
643 |
by_tactic (Tactic.Apply_Method' (mI, NONE, empty, ContextC.empty))
|
walther@59846
|
644 |
(empty, ContextC.empty) ptp
|
wneuper@59555
|
645 |
end
|
walther@59762
|
646 |
| _ => msg_cs';
|
wneuper@59555
|
647 |
in compare_step (tacis, c @ c' @ c'', ptp) ifo end
|
wneuper@59555
|
648 |
end
|
wneuper@59555
|
649 |
|
walther@59848
|
650 |
(* Locate a step in a program, which has been determined by input of a term *)
|
walther@59795
|
651 |
fun locate_input_term (pt, pos) tm =
|
walther@59658
|
652 |
let
|
walther@59757
|
653 |
val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
|
walther@59658
|
654 |
val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred)
|
walther@59658
|
655 |
in
|
walther@59658
|
656 |
case compare_step ([], [], (pt, pos_pred)) tm of
|
walther@59848
|
657 |
("no derivation found", _) => Not_Derivable
|
walther@59796
|
658 |
| ("ok", (_, _, cstate)) =>
|
walther@59795
|
659 |
Found_Step cstate
|
walther@59658
|
660 |
| _ => raise ERROR "compare_step: uncovered case"
|
walther@59658
|
661 |
end
|
wneuper@59556
|
662 |
|
walther@59684
|
663 |
(**)end(**)
|