1 (* Title: Tools/Code/code_eval.ML |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 |
|
4 Runtime services building on code generation into implementation language SML. |
|
5 *) |
|
6 |
|
7 signature CODE_EVAL = |
|
8 sig |
|
9 val target: string |
|
10 val eval: string option |
|
11 -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string |
|
12 -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a |
|
13 val setup: theory -> theory |
|
14 end; |
|
15 |
|
16 structure Code_Eval : CODE_EVAL = |
|
17 struct |
|
18 |
|
19 (** generic **) |
|
20 |
|
21 val target = "Eval"; |
|
22 |
|
23 fun evaluation_code thy module_name tycos consts = |
|
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 |
|
45 val ctxt = ProofContext.init_global thy; |
|
46 fun evaluator naming program ((_, (_, ty)), t) deps = |
|
47 let |
|
48 val _ = if Code_Thingol.contains_dictvar t then |
|
49 error "Term to be evaluated contains free dictionaries" else (); |
|
50 val value_name = "Value.VALUE.value" |
|
51 val program' = program |
|
52 |> Graph.new_node (value_name, |
|
53 Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE))) |
|
54 |> fold (curry Graph.add_edge value_name) deps; |
|
55 val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy |
|
56 (the_default target some_target) NONE "Code" [] naming program' [value_name]; |
|
57 val value_code = space_implode " " |
|
58 (value_name' :: map (enclose "(" ")") args); |
|
59 in ML_Context.value ctxt cookie (program_code, value_code) end; |
|
60 in Code_Thingol.dynamic_eval_value thy postproc evaluator t end; |
|
61 |
|
62 |
|
63 (** instrumentalization by antiquotation **) |
|
64 |
|
65 local |
|
66 |
|
67 structure Code_Antiq_Data = Proof_Data |
|
68 ( |
|
69 type T = (string list * string list) * (bool |
|
70 * (string * ((string * string) list * (string * string) list)) lazy); |
|
71 fun init _ = (([], []), (true, (Lazy.value ("", ([], []))))); |
|
72 ); |
|
73 |
|
74 val is_first_occ = fst o snd o Code_Antiq_Data.get; |
|
75 |
|
76 fun register_code new_tycos new_consts ctxt = |
|
77 let |
|
78 val ((tycos, consts), _) = Code_Antiq_Data.get ctxt; |
|
79 val tycos' = fold (insert (op =)) new_tycos tycos; |
|
80 val consts' = fold (insert (op =)) new_consts consts; |
|
81 val acc_code = Lazy.lazy (fn () => |
|
82 evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts'); |
|
83 in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end; |
|
84 |
|
85 fun register_const const = register_code [] [const]; |
|
86 |
|
87 fun register_datatype tyco constrs = register_code [tyco] constrs; |
|
88 |
|
89 fun print_const const all_struct_name tycos_map consts_map = |
|
90 (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const; |
|
91 |
|
92 fun print_code is_first print_it ctxt = |
|
93 let |
|
94 val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt; |
|
95 val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code; |
|
96 val ml_code = if is_first then ml_code |
|
97 else ""; |
|
98 val all_struct_name = "Isabelle"; |
|
99 in (ml_code, print_it all_struct_name tycos_map consts_map) end; |
|
100 |
|
101 in |
|
102 |
|
103 fun ml_code_antiq raw_const background = |
|
104 let |
|
105 val const = Code.check_const (ProofContext.theory_of background) raw_const; |
|
106 val is_first = is_first_occ background; |
|
107 val background' = register_const const background; |
|
108 in (print_code is_first (print_const const), background') end; |
|
109 |
|
110 end; (*local*) |
|
111 |
|
112 |
|
113 (** reflection support **) |
|
114 |
|
115 fun check_datatype thy tyco consts = |
|
116 let |
|
117 val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco; |
|
118 val missing_constrs = subtract (op =) consts constrs; |
|
119 val _ = if null missing_constrs then [] |
|
120 else error ("Missing constructor(s) " ^ commas (map quote missing_constrs) |
|
121 ^ " for datatype " ^ quote tyco); |
|
122 val false_constrs = subtract (op =) constrs consts; |
|
123 val _ = if null false_constrs then [] |
|
124 else error ("Non-constructor(s) " ^ commas (map quote false_constrs) |
|
125 ^ " for datatype " ^ quote tyco); |
|
126 in () end; |
|
127 |
|
128 fun add_eval_tyco (tyco, tyco') thy = |
|
129 let |
|
130 val k = Sign.arity_number thy tyco; |
|
131 fun pr pr' fxy [] = tyco' |
|
132 | pr pr' fxy [ty] = |
|
133 Code_Printer.concat [pr' Code_Printer.BR ty, tyco'] |
|
134 | pr pr' fxy tys = |
|
135 Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] |
|
136 in |
|
137 thy |
|
138 |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr)) |
|
139 end; |
|
140 |
|
141 fun add_eval_constr (const, const') thy = |
|
142 let |
|
143 val k = Code.args_number thy const; |
|
144 fun pr pr' fxy ts = Code_Printer.brackify fxy |
|
145 (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts))); |
|
146 in |
|
147 thy |
|
148 |> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr))) |
|
149 end; |
|
150 |
|
151 fun add_eval_const (const, const') = Code_Target.add_const_syntax target |
|
152 const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const'))); |
|
153 |
|
154 fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy = |
|
155 thy |
|
156 |> Code_Target.add_reserved target module_name |
|
157 |> Context.theory_map |
|
158 (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body)) |
|
159 |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map |
|
160 |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map |
|
161 |> fold (add_eval_const o apsnd Code_Printer.str) const_map |
|
162 | process (code_body, _) _ (SOME file_name) thy = |
|
163 let |
|
164 val preamble = |
|
165 "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy)) |
|
166 ^ "; DO NOT EDIT! *)"; |
|
167 val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body); |
|
168 in |
|
169 thy |
|
170 end; |
|
171 |
|
172 fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy = |
|
173 let |
|
174 val datatypes = map (fn (raw_tyco, raw_cos) => |
|
175 (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes; |
|
176 val _ = map (uncurry (check_datatype thy)) datatypes; |
|
177 val tycos = map fst datatypes; |
|
178 val constrs = maps snd datatypes; |
|
179 val functions = map (prep_const thy) raw_functions; |
|
180 val result = evaluation_code thy module_name tycos (constrs @ functions) |
|
181 |> (apsnd o apsnd) (chop (length constrs)); |
|
182 in |
|
183 thy |
|
184 |> process result module_name some_file |
|
185 end; |
|
186 |
|
187 val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const; |
|
188 val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const; |
|
189 |
|
190 |
|
191 (** Isar setup **) |
|
192 |
|
193 val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq); |
|
194 |
|
195 local |
|
196 |
|
197 val datatypesK = "datatypes"; |
|
198 val functionsK = "functions"; |
|
199 val fileK = "file"; |
|
200 val andK = "and" |
|
201 |
|
202 val _ = List.app Keyword.keyword [datatypesK, functionsK]; |
|
203 |
|
204 val parse_datatype = |
|
205 Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))); |
|
206 |
|
207 in |
|
208 |
|
209 val _ = |
|
210 Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code" |
|
211 Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype |
|
212 ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) [] |
|
213 -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) [] |
|
214 -- Scan.option (Parse.$$$ fileK |-- Parse.name) |
|
215 >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory |
|
216 (code_reflect_cmd raw_datatypes raw_functions module_name some_file))); |
|
217 |
|
218 end; (*local*) |
|
219 |
|
220 val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I)); |
|
221 |
|
222 end; (*struct*) |
|