haftmann@39644
|
1 |
(* Title: Tools/Code/code_runtime.ML
|
haftmann@28054
|
2 |
Author: Florian Haftmann, TU Muenchen
|
haftmann@28054
|
3 |
|
haftmann@34026
|
4 |
Runtime services building on code generation into implementation language SML.
|
haftmann@28054
|
5 |
*)
|
haftmann@28054
|
6 |
|
haftmann@39644
|
7 |
signature CODE_RUNTIME =
|
haftmann@28054
|
8 |
sig
|
haftmann@34026
|
9 |
val target: string
|
haftmann@40093
|
10 |
val value: Proof.context ->
|
haftmann@40093
|
11 |
(Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
|
haftmann@40093
|
12 |
string * string -> 'a
|
haftmann@39713
|
13 |
type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
|
haftmann@39713
|
14 |
val dynamic_value: 'a cookie -> theory -> string option
|
haftmann@39713
|
15 |
-> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option
|
haftmann@39713
|
16 |
val dynamic_value_strict: 'a cookie -> theory -> string option
|
haftmann@39713
|
17 |
-> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a
|
haftmann@39713
|
18 |
val dynamic_value_exn: 'a cookie -> theory -> string option
|
haftmann@39713
|
19 |
-> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
|
haftmann@39713
|
20 |
val static_value: 'a cookie -> theory -> string option
|
haftmann@39713
|
21 |
-> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a option
|
haftmann@39713
|
22 |
val static_value_strict: 'a cookie -> theory -> string option
|
haftmann@39713
|
23 |
-> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a
|
haftmann@39713
|
24 |
val static_value_exn: 'a cookie -> theory -> string option
|
haftmann@39713
|
25 |
-> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result
|
haftmann@41488
|
26 |
val dynamic_holds_conv: theory -> conv
|
haftmann@39713
|
27 |
val static_holds_conv: theory -> string list -> conv
|
haftmann@40648
|
28 |
val code_reflect: (string * string list option) list -> string list -> string
|
haftmann@40648
|
29 |
-> string option -> theory -> theory
|
haftmann@39713
|
30 |
datatype truth = Holds
|
haftmann@39713
|
31 |
val put_truth: (unit -> truth) -> Proof.context -> Proof.context
|
haftmann@40390
|
32 |
val trace: bool Unsynchronized.ref
|
haftmann@40058
|
33 |
val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
|
haftmann@28054
|
34 |
end;
|
haftmann@28054
|
35 |
|
haftmann@39644
|
36 |
structure Code_Runtime : CODE_RUNTIME =
|
haftmann@28054
|
37 |
struct
|
haftmann@28054
|
38 |
|
haftmann@39713
|
39 |
open Basic_Code_Thingol;
|
haftmann@39713
|
40 |
|
haftmann@39647
|
41 |
(** evaluation **)
|
haftmann@33989
|
42 |
|
haftmann@39713
|
43 |
(* technical prerequisites *)
|
haftmann@39713
|
44 |
|
haftmann@39713
|
45 |
val this = "Code_Runtime";
|
haftmann@39713
|
46 |
val s_truth = Long_Name.append this "truth";
|
haftmann@39713
|
47 |
val s_Holds = Long_Name.append this "Holds";
|
haftmann@39713
|
48 |
|
haftmann@34026
|
49 |
val target = "Eval";
|
haftmann@45529
|
50 |
val structure_generated = "Generated_Code";
|
haftmann@28054
|
51 |
|
haftmann@39713
|
52 |
datatype truth = Holds;
|
haftmann@39668
|
53 |
|
haftmann@39713
|
54 |
val _ = Context.>> (Context.map_theory
|
haftmann@39713
|
55 |
(Code_Target.extend_target (target, (Code_ML.target_SML, K I))
|
haftmann@39725
|
56 |
#> Code_Target.add_tyco_syntax target @{type_name prop}
|
haftmann@39725
|
57 |
(SOME (0, (K o K o K) (Code_Printer.str s_truth)))
|
haftmann@39725
|
58 |
#> Code_Target.add_const_syntax target @{const_name Code_Generator.holds}
|
haftmann@39725
|
59 |
(SOME (Code_Printer.plain_const_syntax s_Holds))
|
haftmann@39713
|
60 |
#> Code_Target.add_reserved target this
|
haftmann@39725
|
61 |
#> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
|
haftmann@39725
|
62 |
(*avoid further pervasive infix names*)
|
haftmann@39713
|
63 |
|
haftmann@40390
|
64 |
val trace = Unsynchronized.ref false;
|
haftmann@40390
|
65 |
|
haftmann@40093
|
66 |
fun exec verbose code =
|
haftmann@40390
|
67 |
(if ! trace then tracing code else ();
|
haftmann@40500
|
68 |
ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code));
|
haftmann@40093
|
69 |
|
haftmann@40093
|
70 |
fun value ctxt (get, put, put_ml) (prelude, value) =
|
haftmann@40093
|
71 |
let
|
haftmann@40093
|
72 |
val code = (prelude
|
haftmann@40093
|
73 |
^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
|
haftmann@40093
|
74 |
^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
|
haftmann@40093
|
75 |
val ctxt' = ctxt
|
haftmann@40093
|
76 |
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
|
haftmann@40093
|
77 |
|> Context.proof_map (exec false code);
|
haftmann@40093
|
78 |
in get ctxt' () end;
|
haftmann@40093
|
79 |
|
haftmann@39713
|
80 |
|
haftmann@39713
|
81 |
(* evaluation into target language values *)
|
haftmann@39713
|
82 |
|
haftmann@39713
|
83 |
type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
|
haftmann@39713
|
84 |
|
haftmann@39829
|
85 |
fun reject_vars thy t =
|
haftmann@39829
|
86 |
let
|
wenzelm@43232
|
87 |
val ctxt = Proof_Context.init_global thy;
|
haftmann@39829
|
88 |
in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
|
haftmann@39829
|
89 |
|
haftmann@41597
|
90 |
fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target);
|
haftmann@39725
|
91 |
|
haftmann@41595
|
92 |
fun evaluation cookie thy evaluator vs_t args =
|
haftmann@39647
|
93 |
let
|
wenzelm@43232
|
94 |
val ctxt = Proof_Context.init_global thy;
|
haftmann@41595
|
95 |
val (program_code, value_name) = evaluator vs_t;
|
haftmann@39713
|
96 |
val value_code = space_implode " "
|
haftmann@41595
|
97 |
(value_name :: "()" :: map (enclose "(" ")") args);
|
wenzelm@40491
|
98 |
in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
|
haftmann@39713
|
99 |
|
haftmann@39713
|
100 |
fun partiality_as_none e = SOME (Exn.release e)
|
haftmann@39713
|
101 |
handle General.Match => NONE
|
haftmann@39713
|
102 |
| General.Bind => NONE
|
haftmann@39713
|
103 |
| General.Fail _ => NONE;
|
haftmann@39713
|
104 |
|
haftmann@39713
|
105 |
fun dynamic_value_exn cookie thy some_target postproc t args =
|
haftmann@39713
|
106 |
let
|
haftmann@39829
|
107 |
val _ = reject_vars thy t;
|
haftmann@41347
|
108 |
val _ = if ! trace
|
haftmann@41347
|
109 |
then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
|
haftmann@41347
|
110 |
else ()
|
haftmann@39722
|
111 |
fun evaluator naming program ((_, vs_ty), t) deps =
|
haftmann@41595
|
112 |
evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args;
|
haftmann@41432
|
113 |
in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
|
haftmann@39713
|
114 |
|
haftmann@39713
|
115 |
fun dynamic_value_strict cookie thy some_target postproc t args =
|
haftmann@39713
|
116 |
Exn.release (dynamic_value_exn cookie thy some_target postproc t args);
|
haftmann@39713
|
117 |
|
haftmann@39713
|
118 |
fun dynamic_value cookie thy some_target postproc t args =
|
haftmann@39713
|
119 |
partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
|
haftmann@39713
|
120 |
|
haftmann@41595
|
121 |
fun static_evaluator cookie thy some_target naming program consts' =
|
haftmann@41595
|
122 |
let
|
haftmann@41595
|
123 |
val evaluator = obtain_evaluator thy some_target naming program consts'
|
haftmann@41595
|
124 |
in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
|
haftmann@41595
|
125 |
|
haftmann@39713
|
126 |
fun static_value_exn cookie thy some_target postproc consts =
|
haftmann@41595
|
127 |
Code_Thingol.static_value thy (Exn.map_result o postproc) consts
|
haftmann@41595
|
128 |
(static_evaluator cookie thy some_target) o reject_vars thy;
|
haftmann@39713
|
129 |
|
haftmann@41595
|
130 |
fun static_value_strict cookie thy some_target postproc consts =
|
haftmann@41595
|
131 |
Exn.release o static_value_exn cookie thy some_target postproc consts;
|
haftmann@39713
|
132 |
|
haftmann@41595
|
133 |
fun static_value cookie thy some_target postproc consts =
|
haftmann@41595
|
134 |
partiality_as_none o static_value_exn cookie thy some_target postproc consts;
|
haftmann@39713
|
135 |
|
haftmann@39713
|
136 |
|
haftmann@39713
|
137 |
(* evaluation for truth or nothing *)
|
haftmann@39713
|
138 |
|
wenzelm@40066
|
139 |
structure Truth_Result = Proof_Data
|
wenzelm@40066
|
140 |
(
|
haftmann@39713
|
141 |
type T = unit -> truth
|
wenzelm@41720
|
142 |
(* FIXME avoid user error with non-user text *)
|
haftmann@39713
|
143 |
fun init _ () = error "Truth_Result"
|
haftmann@39713
|
144 |
);
|
haftmann@39713
|
145 |
val put_truth = Truth_Result.put;
|
haftmann@39713
|
146 |
val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
|
haftmann@39713
|
147 |
|
haftmann@39829
|
148 |
val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of);
|
haftmann@39829
|
149 |
|
haftmann@41597
|
150 |
local
|
haftmann@41597
|
151 |
|
haftmann@41597
|
152 |
fun check_holds thy evaluator vs_t deps ct =
|
haftmann@39713
|
153 |
let
|
haftmann@39713
|
154 |
val t = Thm.term_of ct;
|
haftmann@39713
|
155 |
val _ = if fastype_of t <> propT
|
haftmann@39713
|
156 |
then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
|
haftmann@39713
|
157 |
else ();
|
haftmann@39713
|
158 |
val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
|
haftmann@41597
|
159 |
val result = case partiality_as_none (evaluation truth_cookie thy evaluator vs_t [])
|
haftmann@39713
|
160 |
of SOME Holds => true
|
haftmann@39713
|
161 |
| _ => false;
|
haftmann@39713
|
162 |
in
|
haftmann@39713
|
163 |
Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct)
|
haftmann@39713
|
164 |
end;
|
haftmann@39713
|
165 |
|
haftmann@39713
|
166 |
val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
|
wenzelm@44500
|
167 |
(Thm.add_oracle (@{binding holds_by_evaluation},
|
haftmann@41597
|
168 |
fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct)));
|
haftmann@39713
|
169 |
|
haftmann@41597
|
170 |
fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
|
haftmann@41597
|
171 |
raw_check_holds_oracle (thy, evaluator, (vs_ty, t), deps, ct);
|
haftmann@41597
|
172 |
|
haftmann@41597
|
173 |
in
|
haftmann@39713
|
174 |
|
haftmann@41488
|
175 |
fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
|
haftmann@41597
|
176 |
(fn naming => fn program => fn vs_t => fn deps =>
|
haftmann@41597
|
177 |
check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps)
|
haftmann@41597
|
178 |
o reject_vars thy;
|
haftmann@39713
|
179 |
|
haftmann@41597
|
180 |
fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
|
haftmann@41597
|
181 |
(fn naming => fn program => fn consts' =>
|
haftmann@41597
|
182 |
check_holds_oracle thy (obtain_evaluator thy NONE naming program consts'))
|
haftmann@41597
|
183 |
o reject_vars thy;
|
haftmann@41597
|
184 |
|
haftmann@41597
|
185 |
end; (*local*)
|
haftmann@39647
|
186 |
|
haftmann@39647
|
187 |
|
haftmann@39647
|
188 |
(** instrumentalization **)
|
haftmann@39647
|
189 |
|
haftmann@39156
|
190 |
fun evaluation_code thy module_name tycos consts =
|
haftmann@33989
|
191 |
let
|
wenzelm@43232
|
192 |
val ctxt = Proof_Context.init_global thy;
|
haftmann@36271
|
193 |
val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
|
haftmann@34026
|
194 |
val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
|
wenzelm@43230
|
195 |
val (ml_code, target_names) =
|
wenzelm@43230
|
196 |
Code_Target.produce_code_for thy
|
wenzelm@43230
|
197 |
target NONE module_name [] naming program (consts' @ tycos');
|
haftmann@34026
|
198 |
val (consts'', tycos'') = chop (length consts') target_names;
|
wenzelm@43230
|
199 |
val consts_map = map2 (fn const =>
|
wenzelm@43230
|
200 |
fn NONE =>
|
wenzelm@43230
|
201 |
error ("Constant " ^ (quote o Code.string_of_const thy) const ^
|
wenzelm@43230
|
202 |
"\nhas a user-defined serialization")
|
wenzelm@43230
|
203 |
| SOME const'' => (const, const'')) consts consts''
|
wenzelm@43230
|
204 |
val tycos_map = map2 (fn tyco =>
|
wenzelm@43230
|
205 |
fn NONE =>
|
wenzelm@43232
|
206 |
error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^
|
wenzelm@43230
|
207 |
"\nhas a user-defined serialization")
|
wenzelm@43230
|
208 |
| SOME tyco'' => (tyco, tyco'')) tycos tycos'';
|
haftmann@34026
|
209 |
in (ml_code, (tycos_map, consts_map)) end;
|
haftmann@28054
|
210 |
|
haftmann@28054
|
211 |
|
haftmann@39647
|
212 |
(* by antiquotation *)
|
haftmann@28054
|
213 |
|
haftmann@28054
|
214 |
local
|
haftmann@28054
|
215 |
|
haftmann@39156
|
216 |
structure Code_Antiq_Data = Proof_Data
|
haftmann@28054
|
217 |
(
|
haftmann@39156
|
218 |
type T = (string list * string list) * (bool
|
haftmann@40648
|
219 |
* (string * (string * string) list) lazy);
|
haftmann@40648
|
220 |
fun init _ = (([], []), (true, (Lazy.value ("", []))));
|
haftmann@28054
|
221 |
);
|
haftmann@28054
|
222 |
|
haftmann@39156
|
223 |
val is_first_occ = fst o snd o Code_Antiq_Data.get;
|
haftmann@28054
|
224 |
|
haftmann@30962
|
225 |
fun register_code new_tycos new_consts ctxt =
|
haftmann@28054
|
226 |
let
|
haftmann@39156
|
227 |
val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
|
haftmann@30962
|
228 |
val tycos' = fold (insert (op =)) new_tycos tycos;
|
haftmann@30962
|
229 |
val consts' = fold (insert (op =)) new_consts consts;
|
haftmann@39156
|
230 |
val acc_code = Lazy.lazy (fn () =>
|
haftmann@45529
|
231 |
evaluation_code (Proof_Context.theory_of ctxt) structure_generated tycos' consts'
|
haftmann@40649
|
232 |
|> apsnd snd);
|
haftmann@39156
|
233 |
in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
|
haftmann@28054
|
234 |
|
haftmann@30962
|
235 |
fun register_const const = register_code [] [const];
|
haftmann@30962
|
236 |
|
haftmann@40648
|
237 |
fun print_code is_first const ctxt =
|
haftmann@30962
|
238 |
let
|
haftmann@39156
|
239 |
val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
|
haftmann@40648
|
240 |
val (ml_code, consts_map) = Lazy.force acc_code;
|
haftmann@40649
|
241 |
val ml_code = if is_first then ml_code else "";
|
wenzelm@41734
|
242 |
val body = "Isabelle." ^ the (AList.lookup (op =) consts_map const);
|
wenzelm@41625
|
243 |
in (ml_code, body) end;
|
haftmann@28054
|
244 |
|
haftmann@28054
|
245 |
in
|
haftmann@28054
|
246 |
|
wenzelm@35019
|
247 |
fun ml_code_antiq raw_const background =
|
haftmann@28054
|
248 |
let
|
wenzelm@43232
|
249 |
val const = Code.check_const (Proof_Context.theory_of background) raw_const;
|
haftmann@28054
|
250 |
val is_first = is_first_occ background;
|
haftmann@28054
|
251 |
val background' = register_const const background;
|
haftmann@40648
|
252 |
in (print_code is_first const, background') end;
|
haftmann@30962
|
253 |
|
haftmann@28054
|
254 |
end; (*local*)
|
haftmann@28054
|
255 |
|
haftmann@28054
|
256 |
|
haftmann@39647
|
257 |
(* reflection support *)
|
haftmann@36466
|
258 |
|
haftmann@40648
|
259 |
fun check_datatype thy tyco some_consts =
|
haftmann@36466
|
260 |
let
|
haftmann@40969
|
261 |
val constrs = (map fst o snd o fst o Code.get_type thy) tyco;
|
haftmann@40648
|
262 |
val _ = case some_consts
|
haftmann@40648
|
263 |
of SOME consts =>
|
haftmann@40648
|
264 |
let
|
haftmann@40648
|
265 |
val missing_constrs = subtract (op =) consts constrs;
|
haftmann@40648
|
266 |
val _ = if null missing_constrs then []
|
wenzelm@46301
|
267 |
else error ("Missing constructor(s) " ^ commas_quote missing_constrs
|
haftmann@40648
|
268 |
^ " for datatype " ^ quote tyco);
|
haftmann@40648
|
269 |
val false_constrs = subtract (op =) constrs consts;
|
haftmann@40648
|
270 |
val _ = if null false_constrs then []
|
wenzelm@46301
|
271 |
else error ("Non-constructor(s) " ^ commas_quote false_constrs
|
haftmann@40648
|
272 |
^ " for datatype " ^ quote tyco)
|
haftmann@40648
|
273 |
in () end
|
haftmann@40648
|
274 |
| NONE => ();
|
haftmann@40648
|
275 |
in (tyco, constrs) end;
|
haftmann@36466
|
276 |
|
haftmann@36466
|
277 |
fun add_eval_tyco (tyco, tyco') thy =
|
haftmann@36466
|
278 |
let
|
haftmann@36466
|
279 |
val k = Sign.arity_number thy tyco;
|
haftmann@40648
|
280 |
fun pr pr' _ [] = tyco'
|
haftmann@40648
|
281 |
| pr pr' _ [ty] =
|
haftmann@36466
|
282 |
Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
|
haftmann@40648
|
283 |
| pr pr' _ tys =
|
haftmann@36466
|
284 |
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
|
haftmann@36466
|
285 |
in
|
haftmann@36466
|
286 |
thy
|
haftmann@39149
|
287 |
|> Code_Target.add_tyco_syntax target tyco (SOME (k, pr))
|
haftmann@36466
|
288 |
end;
|
haftmann@36466
|
289 |
|
haftmann@36507
|
290 |
fun add_eval_constr (const, const') thy =
|
haftmann@36507
|
291 |
let
|
haftmann@36507
|
292 |
val k = Code.args_number thy const;
|
haftmann@36507
|
293 |
fun pr pr' fxy ts = Code_Printer.brackify fxy
|
haftmann@39148
|
294 |
(const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
|
haftmann@36507
|
295 |
in
|
haftmann@36507
|
296 |
thy
|
haftmann@39149
|
297 |
|> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
|
haftmann@36507
|
298 |
end;
|
haftmann@36507
|
299 |
|
haftmann@39149
|
300 |
fun add_eval_const (const, const') = Code_Target.add_const_syntax target
|
haftmann@36466
|
301 |
const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
|
haftmann@36466
|
302 |
|
haftmann@40093
|
303 |
fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
|
haftmann@39161
|
304 |
thy
|
haftmann@39161
|
305 |
|> Code_Target.add_reserved target module_name
|
haftmann@40093
|
306 |
|> Context.theory_map (exec true code)
|
haftmann@39161
|
307 |
|> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
|
haftmann@39161
|
308 |
|> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
|
haftmann@39161
|
309 |
|> fold (add_eval_const o apsnd Code_Printer.str) const_map
|
haftmann@40093
|
310 |
| process_reflection (code, _) _ (SOME file_name) thy =
|
haftmann@36466
|
311 |
let
|
wenzelm@38213
|
312 |
val preamble =
|
wenzelm@47612
|
313 |
"(* Generated from " ^
|
wenzelm@47612
|
314 |
Path.implode (Thy_Load.thy_path (Path.basic (Context.theory_name thy))) ^
|
wenzelm@47612
|
315 |
"; DO NOT EDIT! *)";
|
haftmann@40093
|
316 |
val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code);
|
haftmann@36466
|
317 |
in
|
haftmann@36466
|
318 |
thy
|
haftmann@36466
|
319 |
end;
|
haftmann@36466
|
320 |
|
haftmann@36466
|
321 |
fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy =
|
haftmann@36466
|
322 |
let
|
haftmann@36466
|
323 |
val datatypes = map (fn (raw_tyco, raw_cos) =>
|
haftmann@40648
|
324 |
(prep_type thy raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
|
haftmann@40648
|
325 |
val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes
|
haftmann@40648
|
326 |
|> apsnd flat;
|
haftmann@36466
|
327 |
val functions = map (prep_const thy) raw_functions;
|
haftmann@36507
|
328 |
val result = evaluation_code thy module_name tycos (constrs @ functions)
|
haftmann@36507
|
329 |
|> (apsnd o apsnd) (chop (length constrs));
|
haftmann@36466
|
330 |
in
|
haftmann@36466
|
331 |
thy
|
haftmann@39725
|
332 |
|> process_reflection result module_name some_file
|
haftmann@36466
|
333 |
end;
|
haftmann@36466
|
334 |
|
haftmann@39668
|
335 |
val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I);
|
haftmann@36466
|
336 |
val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const;
|
haftmann@36466
|
337 |
|
haftmann@36466
|
338 |
|
haftmann@28054
|
339 |
(** Isar setup **)
|
haftmann@28054
|
340 |
|
wenzelm@44446
|
341 |
val _ =
|
wenzelm@44446
|
342 |
Context.>> (Context.map_theory
|
wenzelm@44500
|
343 |
(ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq)));
|
haftmann@28054
|
344 |
|
haftmann@36466
|
345 |
local
|
haftmann@36466
|
346 |
|
wenzelm@36970
|
347 |
val parse_datatype =
|
wenzelm@47823
|
348 |
Parse.name --| @{keyword "="} --
|
haftmann@40959
|
349 |
(((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
|
wenzelm@47823
|
350 |
|| ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME));
|
haftmann@36466
|
351 |
|
haftmann@36466
|
352 |
in
|
haftmann@36466
|
353 |
|
haftmann@36466
|
354 |
val _ =
|
wenzelm@36970
|
355 |
Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
|
wenzelm@47823
|
356 |
Keyword.thy_decl (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype
|
wenzelm@47823
|
357 |
::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
|
wenzelm@47823
|
358 |
-- Scan.optional (@{keyword "functions"} |-- Scan.repeat1 Parse.name) []
|
wenzelm@47823
|
359 |
-- Scan.option (@{keyword "file"} |-- Parse.name)
|
haftmann@36534
|
360 |
>> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
|
haftmann@36466
|
361 |
(code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
|
haftmann@36466
|
362 |
|
haftmann@36466
|
363 |
end; (*local*)
|
haftmann@36466
|
364 |
|
haftmann@40058
|
365 |
|
haftmann@40058
|
366 |
(** using external SML files as substitute for proper definitions -- only for polyml! **)
|
haftmann@40058
|
367 |
|
haftmann@40058
|
368 |
local
|
haftmann@40058
|
369 |
|
wenzelm@40066
|
370 |
structure Loaded_Values = Theory_Data
|
wenzelm@40066
|
371 |
(
|
haftmann@40058
|
372 |
type T = string list
|
haftmann@40058
|
373 |
val empty = []
|
wenzelm@41720
|
374 |
val extend = I
|
wenzelm@40066
|
375 |
fun merge data : T = Library.merge (op =) data
|
haftmann@40058
|
376 |
);
|
haftmann@40058
|
377 |
|
haftmann@40058
|
378 |
fun notify_val (string, value) =
|
haftmann@40058
|
379 |
let
|
haftmann@40058
|
380 |
val _ = #enterVal ML_Env.name_space (string, value);
|
haftmann@40058
|
381 |
val _ = Context.>> ((Context.map_theory o Loaded_Values.map) (insert (op =) string));
|
haftmann@40058
|
382 |
in () end;
|
haftmann@40058
|
383 |
|
haftmann@40058
|
384 |
fun abort _ = error "Only value bindings allowed.";
|
haftmann@40058
|
385 |
|
haftmann@40058
|
386 |
val notifying_context : use_context =
|
haftmann@40058
|
387 |
{tune_source = #tune_source ML_Env.local_context,
|
haftmann@40058
|
388 |
name_space =
|
haftmann@40058
|
389 |
{lookupVal = #lookupVal ML_Env.name_space,
|
haftmann@40058
|
390 |
lookupType = #lookupType ML_Env.name_space,
|
haftmann@40058
|
391 |
lookupFix = #lookupFix ML_Env.name_space,
|
haftmann@40058
|
392 |
lookupStruct = #lookupStruct ML_Env.name_space,
|
haftmann@40058
|
393 |
lookupSig = #lookupSig ML_Env.name_space,
|
haftmann@40058
|
394 |
lookupFunct = #lookupFunct ML_Env.name_space,
|
haftmann@40058
|
395 |
enterVal = notify_val,
|
haftmann@40058
|
396 |
enterType = abort,
|
haftmann@40058
|
397 |
enterFix = abort,
|
haftmann@40058
|
398 |
enterStruct = abort,
|
haftmann@40058
|
399 |
enterSig = abort,
|
haftmann@40058
|
400 |
enterFunct = abort,
|
haftmann@40058
|
401 |
allVal = #allVal ML_Env.name_space,
|
haftmann@40058
|
402 |
allType = #allType ML_Env.name_space,
|
haftmann@40058
|
403 |
allFix = #allFix ML_Env.name_space,
|
haftmann@40058
|
404 |
allStruct = #allStruct ML_Env.name_space,
|
haftmann@40058
|
405 |
allSig = #allSig ML_Env.name_space,
|
haftmann@40058
|
406 |
allFunct = #allFunct ML_Env.name_space},
|
haftmann@40058
|
407 |
str_of_pos = #str_of_pos ML_Env.local_context,
|
haftmann@40058
|
408 |
print = #print ML_Env.local_context,
|
haftmann@40058
|
409 |
error = #error ML_Env.local_context};
|
haftmann@40058
|
410 |
|
haftmann@40058
|
411 |
in
|
haftmann@40058
|
412 |
|
haftmann@40058
|
413 |
fun use_file filepath thy =
|
haftmann@40058
|
414 |
let
|
haftmann@40058
|
415 |
val thy' = Loaded_Values.put [] thy;
|
haftmann@40058
|
416 |
val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
|
haftmann@40058
|
417 |
val _ = Secure.use_text notifying_context
|
haftmann@40058
|
418 |
(0, Path.implode filepath) false (File.read filepath);
|
wenzelm@46139
|
419 |
val thy'' = Context.the_theory (Context.the_thread_data ());
|
haftmann@40093
|
420 |
val names = Loaded_Values.get thy'';
|
haftmann@40558
|
421 |
in (names, thy'') end;
|
haftmann@40058
|
422 |
|
haftmann@40058
|
423 |
end;
|
haftmann@40058
|
424 |
|
haftmann@40058
|
425 |
fun add_definiendum (ml_name, (b, T)) thy =
|
haftmann@40058
|
426 |
thy
|
haftmann@40058
|
427 |
|> Code_Target.add_reserved target ml_name
|
haftmann@40058
|
428 |
|> Specification.axiomatization [(b, SOME T, NoSyn)] []
|
haftmann@40058
|
429 |
|-> (fn ([Const (const, _)], _) =>
|
haftmann@40058
|
430 |
Code_Target.add_const_syntax target const
|
haftmann@40093
|
431 |
(SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))
|
haftmann@45529
|
432 |
#> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
|
haftmann@40058
|
433 |
|
haftmann@40058
|
434 |
fun process_file filepath (definienda, thy) =
|
haftmann@40058
|
435 |
let
|
haftmann@40058
|
436 |
val (ml_names, thy') = use_file filepath thy;
|
haftmann@40058
|
437 |
val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names;
|
haftmann@40058
|
438 |
val _ = if null superfluous then ()
|
haftmann@40058
|
439 |
else error ("Value binding(s) " ^ commas_quote superfluous
|
wenzelm@42815
|
440 |
^ " found in external file " ^ Path.print filepath
|
haftmann@40058
|
441 |
^ " not present among the given contants binding(s).");
|
haftmann@40058
|
442 |
val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names;
|
haftmann@40058
|
443 |
val thy'' = fold add_definiendum these_definienda thy';
|
haftmann@40058
|
444 |
val definienda' = fold (AList.delete (op =)) ml_names definienda;
|
haftmann@40058
|
445 |
in (definienda', thy'') end;
|
haftmann@40058
|
446 |
|
haftmann@40058
|
447 |
fun polyml_as_definition bTs filepaths thy =
|
haftmann@40058
|
448 |
let
|
haftmann@40058
|
449 |
val definienda = map (fn bT => ((Binding.name_of o fst) bT, bT)) bTs;
|
haftmann@40058
|
450 |
val (remaining, thy') = fold process_file filepaths (definienda, thy);
|
haftmann@40058
|
451 |
val _ = if null remaining then ()
|
haftmann@40058
|
452 |
else error ("Constant binding(s) " ^ commas_quote (map fst remaining)
|
haftmann@40058
|
453 |
^ " not present in external file(s).");
|
haftmann@40058
|
454 |
in thy' end;
|
haftmann@40058
|
455 |
|
haftmann@28054
|
456 |
end; (*struct*)
|