walther@59845
|
1 |
(* Title: Interpret/li-tool.sml
|
walther@59790
|
2 |
Author: Walther Neuper 2000
|
walther@59790
|
3 |
(c) due to copyright terms
|
walther@59845
|
4 |
|
walther@59845
|
5 |
Tools for Lucas_Interpreter
|
walther@59790
|
6 |
*)
|
walther@59790
|
7 |
|
walther@59790
|
8 |
signature LUCAS_INTERPRETER_TOOL =
|
walther@59790
|
9 |
sig
|
walther@59790
|
10 |
datatype ass =
|
walther@59906
|
11 |
Associated of Tactic.T * term (*..result*) * Proof.context
|
walther@59906
|
12 |
| Ass_Weak of Tactic.T * term (*..result*) * Proof.context
|
walther@59844
|
13 |
| Not_Associated;
|
Walther@60609
|
14 |
val associate: Ctree.state -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
|
walther@59790
|
15 |
|
Walther@60559
|
16 |
val parent_node: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T * Proof.context
|
Walther@60710
|
17 |
val init_pstate: Proof.context -> I_Model.T_TEST -> MethodC.id ->
|
Walther@60710
|
18 |
Istate.T * Proof.context * Program.T
|
Walther@60559
|
19 |
val resume_prog: Pos.pos' -> Ctree.ctree ->
|
walther@59831
|
20 |
(Istate.T * Proof.context) * Program.T
|
walther@59824
|
21 |
|
walther@59906
|
22 |
val check_leaf: string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term ->
|
walther@59790
|
23 |
Program.leaf * term option
|
walther@59901
|
24 |
|
Walther@60673
|
25 |
val implicit_take: Proof.context -> Program.T -> Env.T -> term option
|
walther@59906
|
26 |
val get_simplifier: Calc.T -> Rule_Set.T
|
Walther@60640
|
27 |
val tac_from_prog: Ctree.state -> term -> Tactic.input
|
Walther@60744
|
28 |
|
Walther@60578
|
29 |
(*from isac_test for Minisubpbl*)
|
Walther@60578
|
30 |
val arguments_from_model : Proof.context -> MethodC.id -> I_Model.T -> term list
|
Walther@60710
|
31 |
val errmsg: string
|
Walther@60710
|
32 |
val error_msg_2: Proof.context -> term -> I_Model.T -> string
|
Walther@60710
|
33 |
val error_msg_2_TEST: Proof.context -> term -> I_Model.T_TEST -> string
|
Walther@60710
|
34 |
val error_msg_1: string
|
Walther@60710
|
35 |
val relate_args: Env.T -> term list -> term list -> Proof.context -> Program.term ->
|
Walther@60710
|
36 |
MethodC.id -> term list -> term list -> (term * term) list
|
walther@59906
|
37 |
|
wenzelm@60223
|
38 |
\<^isac_test>\<open>
|
Walther@60758
|
39 |
val trace_init: Proof.context -> string list -> unit
|
Walther@60758
|
40 |
|
Walther@60578
|
41 |
(**)
|
wenzelm@60223
|
42 |
\<close>
|
walther@59790
|
43 |
end
|
walther@59790
|
44 |
|
Walther@60598
|
45 |
(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step *)
|
Walther@60598
|
46 |
val LI_trace = Attrib.setup_config_bool \<^binding>\<open>LI_trace\<close> (K false);
|
Walther@60598
|
47 |
|
walther@59790
|
48 |
(**)
|
walther@59790
|
49 |
structure LItool(**): LUCAS_INTERPRETER_TOOL(**) =
|
walther@59790
|
50 |
struct
|
walther@59790
|
51 |
(**)
|
walther@59790
|
52 |
open Ctree
|
walther@59790
|
53 |
open Pos
|
walther@59790
|
54 |
|
walther@59848
|
55 |
(* find the formal argument of a tactic in case there is only one (e.g. in simplification) *)
|
Walther@60712
|
56 |
fun implicit_take _ (Rule.Prog prog) env =
|
walther@60372
|
57 |
Option.map (subst_atomic env) (Prog_Tac.get_first_argument prog)
|
Walther@60673
|
58 |
| implicit_take _ _ _ = raise ERROR "implicit_take: no match";
|
walther@59790
|
59 |
|
Walther@60586
|
60 |
val error_msg_1 = "ERROR: the guard is missing (#model in 'type met' added in prep_met)."
|
Walther@60611
|
61 |
fun error_msg_2 ctxt d itms =
|
Walther@60675
|
62 |
("arguments_from_model: '" ^ UnparseC.term ctxt d ^ "' not in itms:\n" ^
|
walther@59942
|
63 |
"itms:\n" ^ I_Model.to_string @{context} itms)
|
Walther@60710
|
64 |
fun error_msg_2_TEST ctxt d itms =
|
Walther@60710
|
65 |
("arguments_from_model: '" ^ UnparseC.term ctxt d ^ "' not in itms:\n" ^
|
Walther@60710
|
66 |
"itms:\n" ^ I_Model.to_string_TEST @{context} itms)
|
walther@60152
|
67 |
(* turn Model-items into arguments for a program *)
|
Walther@60557
|
68 |
fun arguments_from_model ctxt mI itms =
|
walther@59790
|
69 |
let
|
Walther@60705
|
70 |
val mvat = Pre_Conds.max_variant itms
|
walther@59790
|
71 |
fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
|
walther@59790
|
72 |
val itms = filter (okv mvat) itms
|
Walther@60739
|
73 |
fun itm2arg _ (_, (_, _)) = [](*this limits errors to init_pstate,
|
Walther@60710
|
74 |
while changing I_Model.penvval_in triggers much more errors*)
|
Walther@60586
|
75 |
val pats = (#model o MethodC.from_store ctxt) mI
|
walther@59848
|
76 |
val _ = if pats = [] then raise ERROR error_msg_1 else ()
|
walther@59790
|
77 |
in (flat o (map (itm2arg itms))) pats end;
|
walther@59790
|
78 |
|
Walther@60611
|
79 |
(*
|
Walther@60640
|
80 |
convert a Prog_Tac to Tactic.input;
|
Walther@60611
|
81 |
argument Ctree.state is specifically for "Prog_Tac.SubProblem" (requires Pos),
|
Walther@60611
|
82 |
*)
|
Walther@60640
|
83 |
fun tac_from_prog (pt, pos) intac =
|
Walther@60640
|
84 |
let
|
Walther@60640
|
85 |
val pos = Pos.back_from_new pos
|
Walther@60640
|
86 |
val ctxt = Ctree.get_ctxt pt pos
|
Walther@60640
|
87 |
val thy = Proof_Context.theory_of ctxt
|
Walther@60640
|
88 |
in
|
Walther@60640
|
89 |
case intac of
|
Walther@60640
|
90 |
(Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>, _) $ thmID $ _) =>
|
Walther@60640
|
91 |
let
|
Walther@60640
|
92 |
val tid = HOLogic.dest_string thmID
|
Walther@60640
|
93 |
in (Tactic.Rewrite (tid, ThmC.thm_from_thy thy tid)) end
|
Walther@60640
|
94 |
| (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) =>
|
Walther@60640
|
95 |
let
|
Walther@60640
|
96 |
val tid = HOLogic.dest_string thmID
|
Walther@60640
|
97 |
val sub' = Subst.program_to_input ctxt sub
|
Walther@60640
|
98 |
in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end
|
Walther@60640
|
99 |
| (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) =>
|
Walther@60640
|
100 |
(Tactic.Rewrite_Set (HOLogic.dest_string rls))
|
Walther@60640
|
101 |
| (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =>
|
Walther@60640
|
102 |
let
|
Walther@60640
|
103 |
val sub' = Subst.program_to_input ctxt sub
|
Walther@60640
|
104 |
in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end
|
Walther@60640
|
105 |
| (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>, _) $ op_ $ _) =>
|
Walther@60640
|
106 |
(Tactic.Calculate (HOLogic.dest_string op_))
|
Walther@60640
|
107 |
| (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ t) =>
|
Walther@60675
|
108 |
(Tactic.Take (UnparseC.term ctxt t))
|
Walther@60640
|
109 |
| (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ isasub $ _) =>
|
Walther@60640
|
110 |
Tactic.Substitute (Prog_Tac.Substitute_adapt_to_type thy isasub)
|
Walther@60640
|
111 |
| (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>, _) $ _ $
|
Walther@60640
|
112 |
(Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, pred))) =>
|
Walther@60675
|
113 |
(Tactic.Check_elementwise (UnparseC.term ctxt pred))
|
Walther@60640
|
114 |
| (Const (\<^const_name>\<open>Prog_Tac.Or_to_List\<close>, _) $ _ ) => Tactic.Or_to_List
|
Walther@60640
|
115 |
| (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _) =>
|
Walther@60640
|
116 |
fst (Sub_Problem.tac_from_prog (pt, pos) ptac) (*might involve problem refinement etc*)
|
Walther@60640
|
117 |
| t =>
|
Walther@60675
|
118 |
raise ERROR ("stac2tac_ TODO: no match for " ^ UnparseC.term ctxt t)
|
Walther@60640
|
119 |
end
|
walther@59790
|
120 |
|
walther@59790
|
121 |
datatype ass =
|
walther@59844
|
122 |
Associated of
|
walther@59848
|
123 |
Tactic.T (* Subproblem' gets args instantiated in associate *)
|
walther@59848
|
124 |
* term (* resulting from application of Tactic.T *)
|
walther@59848
|
125 |
* Proof.context (* updated by assumptioons from Rewrite* *)
|
walther@59790
|
126 |
| Ass_Weak of Tactic.T * term * Proof.context
|
walther@59844
|
127 |
| Not_Associated;
|
walther@59790
|
128 |
|
walther@59906
|
129 |
(*
|
walther@59906
|
130 |
associate is the ONLY code within by_tactic, which handles Tactic.T individually;
|
walther@59906
|
131 |
thus it does ContextC.insert_assumptions in case of Rewrite*.
|
walther@59906
|
132 |
The argument Ctree.ctree is required only for Subproblem'.
|
walther@59906
|
133 |
*)
|
Walther@60503
|
134 |
fun trace_msg_3 ctxt tac =
|
Walther@60503
|
135 |
if Config.get ctxt LI_trace then
|
walther@59848
|
136 |
tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n" ^
|
Walther@60655
|
137 |
"@@@ tac_ = \"" ^ Tactic.string_of ctxt tac ^ "\"")
|
walther@59848
|
138 |
else ();
|
walther@59790
|
139 |
fun associate _ ctxt (m as Tactic.Rewrite_Inst'
|
walther@59848
|
140 |
(_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
|
walther@59848
|
141 |
(case stac of
|
walther@60335
|
142 |
(Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ _ $ thmID_ $ f_) =>
|
walther@59848
|
143 |
if thmID = HOLogic.dest_string thmID_ then
|
walther@59848
|
144 |
if f = f_ then
|
walther@59848
|
145 |
Associated (m, f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
146 |
else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
147 |
else Not_Associated
|
walther@60335
|
148 |
| (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ rls_ $ f_) =>
|
Walther@60543
|
149 |
if Rule_Set.contains (Rule.Thm thm'') (get_rls ctxt (HOLogic.dest_string rls_)) then
|
walther@59848
|
150 |
if f = f_ then
|
walther@59848
|
151 |
Associated (m, f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
152 |
else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
153 |
else Not_Associated
|
walther@59848
|
154 |
| _ => Not_Associated)
|
walther@59790
|
155 |
| associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
|
walther@59848
|
156 |
(case stac of
|
walther@60335
|
157 |
(Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>, _) $ thmID_ $ f_) =>
|
walther@59848
|
158 |
if thmID = HOLogic.dest_string thmID_ then
|
walther@59848
|
159 |
if f = f_ then
|
walther@59848
|
160 |
Associated (m, f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
161 |
else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
162 |
else Not_Associated
|
walther@60335
|
163 |
| (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>, _) $ rls_ $ f_) =>
|
Walther@60543
|
164 |
if Rule_Set.contains (Rule.Thm thm'') (get_rls ctxt (HOLogic.dest_string rls_)) then
|
walther@59848
|
165 |
if f = f_ then
|
walther@59848
|
166 |
Associated (m, f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
167 |
else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
168 |
else Not_Associated
|
walther@59848
|
169 |
| _ => Not_Associated)
|
walther@59790
|
170 |
| associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
|
walther@60335
|
171 |
(Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ _ $ rls_ $ f_)) =
|
walther@59867
|
172 |
if Rule_Set.id rls = HOLogic.dest_string rls_ then
|
walther@59848
|
173 |
if f = f_ then
|
walther@59848
|
174 |
Associated (m, f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
175 |
else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
176 |
else Not_Associated
|
walther@59790
|
177 |
| associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
|
walther@60335
|
178 |
(Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>, _) $ rls_ $ f_)) =
|
walther@59867
|
179 |
if Rule_Set.id rls = HOLogic.dest_string rls_ then
|
walther@59848
|
180 |
if f = f_ then
|
walther@59848
|
181 |
Associated (m, f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
182 |
else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
|
walther@59848
|
183 |
else Not_Associated
|
walther@59790
|
184 |
| associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
|
walther@59848
|
185 |
(case stac of
|
walther@60335
|
186 |
(Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ op__ $ f_) =>
|
walther@59848
|
187 |
if op_ = HOLogic.dest_string op__ then
|
walther@59848
|
188 |
if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
|
walther@59848
|
189 |
else Not_Associated
|
walther@60335
|
190 |
| (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ _ $ rls_ $ f_) =>
|
Walther@60550
|
191 |
if Rule_Set.contains (Rule.Eval (get_calc ctxt
|
Walther@60543
|
192 |
op_ |> snd)) (get_rls ctxt (HOLogic.dest_string rls_)) then
|
walther@59848
|
193 |
if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
|
walther@59844
|
194 |
else Not_Associated
|
walther@60335
|
195 |
| (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls_ $ f_) =>
|
Walther@60550
|
196 |
if Rule_Set.contains (Rule.Eval (get_calc ctxt
|
Walther@60543
|
197 |
op_ |> snd)) (get_rls ctxt (HOLogic.dest_string rls_)) then
|
walther@59848
|
198 |
if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
|
walther@59844
|
199 |
else Not_Associated
|
walther@59848
|
200 |
| _ => Not_Associated)
|
walther@59790
|
201 |
| associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
|
walther@60335
|
202 |
(Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>,_) $ consts' $ _)) =
|
walther@59848
|
203 |
if consts = consts' then Associated (m, consts_chkd, ctxt) else Not_Associated
|
walther@60335
|
204 |
| associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const (\<^const_name>\<open>Prog_Tac.Or_to_List\<close>, _) $ _)) =
|
walther@59848
|
205 |
Associated (m, list, ctxt)
|
walther@60335
|
206 |
| associate _ ctxt (m as Tactic.Take' term, (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)) =
|
walther@59848
|
207 |
Associated (m, term, ctxt)
|
Walther@60586
|
208 |
| associate _ ctxt (m as Tactic.Substitute' (ro, asm_rls, subte, f, f'),
|
walther@60335
|
209 |
(Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ _ $ t)) =
|
walther@59848
|
210 |
if f = t then
|
walther@59848
|
211 |
Associated (m, f', ctxt)
|
walther@59848
|
212 |
else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
|
walther@59848
|
213 |
if foldl and_ (true, map TermC.contains_Var subte) then
|
walther@59848
|
214 |
let
|
walther@59848
|
215 |
val t' = subst_atomic (map HOLogic.dest_eq subte) t
|
walther@59848
|
216 |
in
|
walther@59962
|
217 |
if t = t' then raise ERROR "associate: Substitute' not applicable to val of Expr"
|
Walther@60586
|
218 |
else Associated (Tactic.Substitute' (ro, asm_rls, subte, t, t'), t', ctxt)
|
walther@59848
|
219 |
end
|
walther@59848
|
220 |
else
|
Walther@60676
|
221 |
(case Rewrite.rewrite_terms_ ctxt ro asm_rls subte t of
|
Walther@60586
|
222 |
SOME (t', _) => Associated (Tactic.Substitute' (ro, asm_rls, subte, t, t'), t', ctxt)
|
walther@59962
|
223 |
| NONE => raise ERROR "associate: Substitute' not applicable to val of Expr")
|
walther@59817
|
224 |
| associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
|
walther@60335
|
225 |
(stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =
|
walther@59848
|
226 |
(case Sub_Problem.tac_from_prog pt stac of
|
walther@59848
|
227 |
(_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) =>
|
walther@59848
|
228 |
if domID = dI andalso pblID = pI then Associated (tac, f, ctxt) else Not_Associated
|
walther@59848
|
229 |
| _ => raise ERROR ("associate: uncovered case"))
|
Walther@60503
|
230 |
| associate _ ctxt (tac, _) =
|
Walther@60503
|
231 |
(trace_msg_3 ctxt tac; Not_Associated);
|
walther@59790
|
232 |
|
Walther@60631
|
233 |
(* in detail step find the next parent, which is either a PblObj xor a PrfObj *)
|
Walther@60559
|
234 |
fun parent_node _ ([], _) = (true, [], Rule_Set.Empty, ContextC.empty)
|
Walther@60559
|
235 |
| parent_node pt (pos as (p, _)) =
|
Walther@60544
|
236 |
let
|
Walther@60557
|
237 |
fun par _ [] = (true, [], Rule_Set.Empty, ContextC.empty)
|
Walther@60544
|
238 |
| par pt p =
|
Walther@60544
|
239 |
if Ctree.is_pblobj (Ctree.get_obj I pt p)
|
Walther@60557
|
240 |
then (true, p, Rule_Set.Empty, ContextC.empty)
|
Walther@60544
|
241 |
else
|
Walther@60544
|
242 |
let
|
Walther@60544
|
243 |
val ctxt = Ctree.get_ctxt pt pos
|
Walther@60544
|
244 |
in
|
Walther@60544
|
245 |
case Ctree.get_obj Ctree.g_tac pt p of
|
Walther@60557
|
246 |
Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls', ctxt)
|
Walther@60557
|
247 |
| Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls', ctxt)
|
Walther@60544
|
248 |
| _ => par pt (Pos.lev_up p)
|
Walther@60544
|
249 |
end
|
Walther@60544
|
250 |
in par pt (Pos.lev_up p) end;
|
Walther@60544
|
251 |
|
walther@59790
|
252 |
(* create the initial interpreter state
|
walther@59848
|
253 |
from the items of the guard and the formal arguments of the program.
|
walther@59790
|
254 |
Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
|
walther@59790
|
255 |
(a) fmz is given by a math author
|
Walther@60710
|
256 |
(b) fmz_ is transformed to O_Model.T as a prerequisite for efficient interactive modelling
|
Walther@60710
|
257 |
(c) modelling creates an I_Model.T from O_Model.T + possible user input
|
Walther@60710
|
258 |
(d) specifying a theory might add some items to I_Model.T and create a guard for the program
|
walther@59848
|
259 |
(e) fun relate_args creates an environment for evaluating the program.
|
walther@59848
|
260 |
Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the program:
|
walther@60125
|
261 |
* Since the arguments of the partial_function have no description (see Input_Descript.thy),
|
walther@59790
|
262 |
(e) depends on the sequence in fmz_ and on the types of the formal arguments.
|
walther@59790
|
263 |
* pairing formal arguments with itm's follows the sequence
|
walther@59790
|
264 |
* Thus the resulting sequence-relation can be ambiguous.
|
walther@59790
|
265 |
* Ambiguities are done by rearranging fmz_ or the formal arguments.
|
walther@59848
|
266 |
* The latter is easier, albeit not optimal: a fmz_ can be used by different programs.
|
Walther@60710
|
267 |
*)
|
walther@59790
|
268 |
val errmsg = "ERROR: found no actual arguments for prog. of "
|
Walther@60710
|
269 |
(** )local( ** ) open for tests*)
|
Walther@60578
|
270 |
fun msg_miss ctxt sc metID caller f formals actuals =
|
walther@59790
|
271 |
"ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
|
walther@60154
|
272 |
"and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
|
Walther@60675
|
273 |
"formal arg \"" ^ UnparseC.term ctxt f ^ "\" doesn't match any actual arg.\n" ^
|
walther@59790
|
274 |
"with:\n" ^
|
Walther@60675
|
275 |
(string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
|
Walther@60675
|
276 |
(string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals
|
Walther@60578
|
277 |
fun msg_miss_type ctxt sc metID f formals actuals =
|
walther@59790
|
278 |
"ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
|
walther@60154
|
279 |
"and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
|
Walther@60675
|
280 |
"formal arg \"" ^ UnparseC.term ctxt f ^ "\" of type \"" ^ UnparseC.typ ctxt (type_of f) ^
|
Walther@60578
|
281 |
"\" doesn't mach any actual arg.\nwith:\n" ^
|
Walther@60675
|
282 |
(string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
|
Walther@60675
|
283 |
(string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals ^ "\n" ^
|
Walther@60675
|
284 |
" with types: " ^ (strs2str o (map ((UnparseC.typ ctxt) o type_of))) actuals
|
Walther@60578
|
285 |
fun msg_ambiguous ctxt sc metID f aas formals actuals =
|
walther@59790
|
286 |
"AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
|
walther@60154
|
287 |
"and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
|
Walther@60675
|
288 |
"formal arg. \"" ^ UnparseC.term ctxt f ^ "\" type-matches with several..." ^
|
Walther@60675
|
289 |
"actual args. \"" ^ UnparseC.terms ctxt aas ^ "\"\n" ^
|
Walther@60675
|
290 |
"selected \"" ^ UnparseC.term ctxt (hd aas) ^ "\"\n" ^
|
walther@59790
|
291 |
"with\n" ^
|
Walther@60675
|
292 |
"formals: " ^ UnparseC.terms ctxt formals ^ "\n" ^
|
Walther@60675
|
293 |
"actuals: " ^ UnparseC.terms ctxt actuals
|
Walther@60758
|
294 |
|
Walther@60758
|
295 |
(*for isac_test*)
|
Walther@60503
|
296 |
fun trace_init ctxt metID =
|
Walther@60503
|
297 |
if Config.get ctxt LI_trace
|
walther@59846
|
298 |
then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
|
walther@59790
|
299 |
else ();
|
Walther@60710
|
300 |
fun assoc_by_type ctxt f aa prog met_id formals actuals =
|
Walther@60710
|
301 |
case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
|
Walther@60710
|
302 |
[] => raise ERROR (msg_miss_type ctxt prog met_id f formals actuals)
|
Walther@60710
|
303 |
| [a] => (f, a)
|
Walther@60710
|
304 |
| aas as (a :: _) => (writeln (msg_ambiguous ctxt prog met_id f aas formals actuals); (f, a));
|
Walther@60735
|
305 |
|
Walther@60760
|
306 |
(*
|
Walther@60760
|
307 |
The sequence of \<open>formals\<close> and \<open>actuals\<close> must be the same:
|
Walther@60760
|
308 |
the sequence of \<open>formals\<close> is given by the program,
|
Walther@60760
|
309 |
the sequence of \<open>actuals\<close> is given by the by theMethodC#model
|
Walther@60760
|
310 |
|
Walther@60760
|
311 |
In case of equal sequence the \<open>fun relate\<close> could be simpler ...
|
Walther@60760
|
312 |
*)
|
Walther@60710
|
313 |
fun relate_args _ (f::_) [] ctxt prog met_id formals actuals =
|
Walther@60710
|
314 |
raise ERROR (msg_miss ctxt prog met_id "relate_args" f formals actuals)
|
Walther@60710
|
315 |
| relate_args env [] _ _ _ _ _ _ = env (*may drop Find?*)
|
Walther@60710
|
316 |
| relate_args env (f::ff) (aas as (a::aa)) ctxt prog met_id formals actuals =
|
Walther@60710
|
317 |
if type_of f = type_of a
|
Walther@60735
|
318 |
then
|
Walther@60735
|
319 |
relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals
|
Walther@60710
|
320 |
else
|
Walther@60735
|
321 |
let
|
Walther@60735
|
322 |
val (f, a) = assoc_by_type ctxt f aas prog met_id formals actuals
|
Walther@60735
|
323 |
in
|
Walther@60735
|
324 |
relate_args (env @ [(f, a)]) ff (remove op = a aas) ctxt prog met_id formals actuals
|
Walther@60735
|
325 |
end
|
Walther@60710
|
326 |
(** )in( **)
|
Walther@60710
|
327 |
fun init_pstate ctxt i_model met_id =
|
walther@59790
|
328 |
let
|
Walther@60710
|
329 |
val (model_patt, program, prog, prog_rls, where_, where_rls) =
|
Walther@60710
|
330 |
case MethodC.from_store ctxt met_id of
|
Walther@60760
|
331 |
{model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>
|
Walther@60710
|
332 |
(model_patt, program, prog, prog_rls, where_, where_rls)
|
Walther@60710
|
333 |
| _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)
|
Walther@60758
|
334 |
val (env_model, (env_subst, env_eval)) = Pre_Conds.make_environments model_patt i_model;
|
Walther@60760
|
335 |
|
Walther@60726
|
336 |
val actuals = map snd env_model
|
Walther@60726
|
337 |
val formals = Program.formal_args prog
|
Walther@60741
|
338 |
val preconds = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))
|
Walther@60710
|
339 |
val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
|
walther@59790
|
340 |
val ist = Istate.e_pstate
|
Walther@60586
|
341 |
|> Istate.set_eval prog_rls
|
Walther@60710
|
342 |
|> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)
|
walther@59790
|
343 |
in
|
Walther@60586
|
344 |
(Istate.Pstate ist, ctxt, program)
|
Walther@60710
|
345 |
end
|
Walther@60710
|
346 |
(** )end( ** )local*)
|
walther@59790
|
347 |
|
Walther@60712
|
348 |
(*DEL single call +tests, get the simplifier of the current method *)
|
Walther@60557
|
349 |
fun get_simplifier (pt, pos as (p, _)) =
|
walther@59790
|
350 |
let
|
walther@59790
|
351 |
val p' = Ctree.par_pblobj pt p
|
walther@59790
|
352 |
val metID = Ctree.get_obj Ctree.g_metID pt p'
|
Walther@60557
|
353 |
val ctxt = Ctree.get_ctxt pt pos
|
Walther@60586
|
354 |
val {prog_rls, ...} = MethodC.from_store ctxt metID
|
Walther@60586
|
355 |
in prog_rls end
|
walther@59790
|
356 |
|
walther@59848
|
357 |
(* resume program interpretation at the beginning of a step *)
|
Walther@60559
|
358 |
fun resume_prog pos pt =
|
walther@59838
|
359 |
let
|
Walther@60559
|
360 |
val (is_problem, p', rls', ctxt) = parent_node pt pos (*is Ctree.PrfObj in case of detail step*)
|
walther@59838
|
361 |
in
|
walther@59848
|
362 |
if is_problem then
|
walther@59838
|
363 |
let
|
walther@59838
|
364 |
val metID = get_obj g_metID pt p'
|
Walther@60586
|
365 |
val {prog_rls, ...} = MethodC.from_store ctxt metID
|
walther@59838
|
366 |
val (is, ctxt) =
|
Walther@60557
|
367 |
case get_loc pt pos of
|
Walther@60586
|
368 |
(Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval prog_rls ist), ctxt)
|
walther@59838
|
369 |
| _ => raise ERROR "resume_prog: unexpected result from get_loc"
|
walther@59848
|
370 |
in
|
Walther@60586
|
371 |
((is, ctxt), (#program o MethodC.from_store ctxt) metID)
|
walther@59848
|
372 |
end
|
walther@59848
|
373 |
else
|
Walther@60557
|
374 |
(get_loc pt pos,
|
Walther@60557
|
375 |
Rule.Prog (Auto_Prog.gen (Proof_Context.theory_of ctxt) (get_last_formula (pt, pos)) rls'))
|
walther@59838
|
376 |
end
|
walther@59790
|
377 |
|
Walther@60503
|
378 |
fun trace_msg_1 ctxt call t stac =
|
Walther@60503
|
379 |
if Config.get ctxt LI_trace then
|
Walther@60675
|
380 |
tracing ("@@@ " ^ call ^ " leaf \"" ^ UnparseC.term ctxt t ^ "\" \<longrightarrow> Tac \"" ^
|
Walther@60675
|
381 |
UnparseC.term ctxt stac ^ "\"")
|
walther@59845
|
382 |
else ();
|
Walther@60503
|
383 |
fun trace_msg_2 ctxt call t lexpr' =
|
Walther@60503
|
384 |
if Config.get ctxt LI_trace then
|
Walther@60675
|
385 |
tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term ctxt t ^ "' \<longrightarrow> Expr \"" ^
|
Walther@60675
|
386 |
UnparseC.term ctxt lexpr' ^ "\"")
|
walther@59845
|
387 |
else ();
|
walther@59848
|
388 |
(*
|
walther@59848
|
389 |
check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
|
Walther@60567
|
390 |
snd of return value are the formal arguments in case of currying.
|
walther@59848
|
391 |
*)
|
Walther@60586
|
392 |
fun check_leaf call ctxt prog_rls (E, (a, v)) t =
|
walther@59790
|
393 |
case Prog_Tac.eval_leaf E a v t of
|
walther@59790
|
394 |
(Program.Tac stac, a') =>
|
walther@59848
|
395 |
let
|
Walther@60586
|
396 |
val stac' = Rewrite.eval_prog_expr ctxt prog_rls
|
walther@59801
|
397 |
(subst_atomic (Env.update_opt E (a, v)) stac)
|
walther@59790
|
398 |
in
|
Walther@60503
|
399 |
(trace_msg_1 ctxt call t stac; (Program.Tac stac', a'))
|
walther@59790
|
400 |
end
|
walther@59790
|
401 |
| (Program.Expr lexpr, a') =>
|
walther@59848
|
402 |
let
|
Walther@60586
|
403 |
val lexpr' = Rewrite.eval_prog_expr ctxt prog_rls
|
walther@59801
|
404 |
(subst_atomic (Env.update_opt E (a, v)) lexpr)
|
walther@59790
|
405 |
in
|
Walther@60503
|
406 |
(trace_msg_2 ctxt call t lexpr'; (Program.Expr lexpr', a'))
|
walther@59790
|
407 |
end;
|
walther@59790
|
408 |
|
walther@59790
|
409 |
(**)end(**)
|