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