5 *) |
5 *) |
6 |
6 |
7 signature CODE_RUNTIME = |
7 signature CODE_RUNTIME = |
8 sig |
8 sig |
9 val target: string |
9 val target: string |
10 val eval: string option |
10 val value: string option |
11 -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string |
11 -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string |
12 -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a |
12 -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a |
13 val setup: theory -> theory |
13 val setup: theory -> theory |
14 end; |
14 end; |
15 |
15 |
16 structure Code_Runtime : CODE_RUNTIME = |
16 structure Code_Runtime : CODE_RUNTIME = |
17 struct |
17 struct |
18 |
18 |
19 (** generic **) |
19 (** evaluation **) |
20 |
20 |
21 val target = "Eval"; |
21 val target = "Eval"; |
22 |
22 |
23 fun evaluation_code thy module_name tycos consts = |
23 fun value some_target cookie postproc thy t args = |
24 let |
|
25 val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts; |
|
26 val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; |
|
27 val (ml_code, target_names) = Code_Target.produce_code_for thy |
|
28 target NONE module_name [] naming program (consts' @ tycos'); |
|
29 val (consts'', tycos'') = chop (length consts') target_names; |
|
30 val consts_map = map2 (fn const => fn NONE => |
|
31 error ("Constant " ^ (quote o Code.string_of_const thy) const |
|
32 ^ "\nhas a user-defined serialization") |
|
33 | SOME const'' => (const, const'')) consts consts'' |
|
34 val tycos_map = map2 (fn tyco => fn NONE => |
|
35 error ("Type " ^ (quote o Sign.extern_type thy) tyco |
|
36 ^ "\nhas a user-defined serialization") |
|
37 | SOME tyco'' => (tyco, tyco'')) tycos tycos''; |
|
38 in (ml_code, (tycos_map, consts_map)) end; |
|
39 |
|
40 |
|
41 (** evaluation **) |
|
42 |
|
43 fun eval some_target cookie postproc thy t args = |
|
44 let |
24 let |
45 val ctxt = ProofContext.init_global thy; |
25 val ctxt = ProofContext.init_global thy; |
46 fun evaluator naming program ((_, (_, ty)), t) deps = |
26 fun evaluator naming program ((_, (_, ty)), t) deps = |
47 let |
27 let |
48 val _ = if Code_Thingol.contains_dictvar t then |
28 val _ = if Code_Thingol.contains_dictvar t then |
58 (value_name' :: map (enclose "(" ")") args); |
38 (value_name' :: map (enclose "(" ")") args); |
59 in ML_Context.value ctxt cookie (program_code, value_code) end; |
39 in ML_Context.value ctxt cookie (program_code, value_code) end; |
60 in Code_Thingol.dynamic_eval_value thy postproc evaluator t end; |
40 in Code_Thingol.dynamic_eval_value thy postproc evaluator t end; |
61 |
41 |
62 |
42 |
63 (** instrumentalization by antiquotation **) |
43 (** instrumentalization **) |
|
44 |
|
45 fun evaluation_code thy module_name tycos consts = |
|
46 let |
|
47 val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts; |
|
48 val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; |
|
49 val (ml_code, target_names) = Code_Target.produce_code_for thy |
|
50 target NONE module_name [] naming program (consts' @ tycos'); |
|
51 val (consts'', tycos'') = chop (length consts') target_names; |
|
52 val consts_map = map2 (fn const => fn NONE => |
|
53 error ("Constant " ^ (quote o Code.string_of_const thy) const |
|
54 ^ "\nhas a user-defined serialization") |
|
55 | SOME const'' => (const, const'')) consts consts'' |
|
56 val tycos_map = map2 (fn tyco => fn NONE => |
|
57 error ("Type " ^ (quote o Sign.extern_type thy) tyco |
|
58 ^ "\nhas a user-defined serialization") |
|
59 | SOME tyco'' => (tyco, tyco'')) tycos tycos''; |
|
60 in (ml_code, (tycos_map, consts_map)) end; |
|
61 |
|
62 |
|
63 (* by antiquotation *) |
64 |
64 |
65 local |
65 local |
66 |
66 |
67 structure Code_Antiq_Data = Proof_Data |
67 structure Code_Antiq_Data = Proof_Data |
68 ( |
68 ( |
108 in (print_code is_first (print_const const), background') end; |
108 in (print_code is_first (print_const const), background') end; |
109 |
109 |
110 end; (*local*) |
110 end; (*local*) |
111 |
111 |
112 |
112 |
113 (** reflection support **) |
113 (* reflection support *) |
114 |
114 |
115 fun check_datatype thy tyco consts = |
115 fun check_datatype thy tyco consts = |
116 let |
116 let |
117 val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco; |
117 val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco; |
118 val missing_constrs = subtract (op =) consts constrs; |
118 val missing_constrs = subtract (op =) consts constrs; |