11520
|
1 |
(* Title: Pure/codegen.ML
|
|
2 |
ID: $Id$
|
11539
|
3 |
Author: Stefan Berghofer, TU Muenchen
|
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
11520
|
5 |
|
11539
|
6 |
Generic code generator.
|
11520
|
7 |
*)
|
|
8 |
|
|
9 |
signature CODEGEN =
|
|
10 |
sig
|
|
11 |
val quiet_mode : bool ref
|
|
12 |
val message : string -> unit
|
|
13 |
|
|
14 |
datatype mixfix =
|
|
15 |
Arg
|
|
16 |
| Ignore
|
|
17 |
| Pretty of Pretty.T
|
|
18 |
| Term of term;
|
|
19 |
|
|
20 |
val add_codegen: string ->
|
|
21 |
(theory -> (exn option * string) Graph.T -> string -> bool -> term ->
|
|
22 |
((exn option * string) Graph.T * Pretty.T) option) -> theory -> theory
|
|
23 |
val print_codegens: theory -> unit
|
|
24 |
val generate_code: theory -> (string * string) list -> string
|
|
25 |
val generate_code_i: theory -> (string * term) list -> string
|
|
26 |
val assoc_consts: (xstring * string option * mixfix list) list -> theory -> theory
|
|
27 |
val assoc_consts_i: (xstring * typ option * mixfix list) list -> theory -> theory
|
|
28 |
val assoc_types: (xstring * string) list -> theory -> theory
|
|
29 |
val get_assoc_code: theory -> string -> typ -> mixfix list option
|
|
30 |
val get_assoc_types: theory -> (string * string) list
|
|
31 |
val invoke_codegen: theory -> (exn option * string) Graph.T ->
|
|
32 |
string -> bool -> term -> (exn option * string) Graph.T * Pretty.T
|
|
33 |
val mk_const_id: Sign.sg -> string -> string
|
|
34 |
val mk_type_id: Sign.sg -> string -> string
|
|
35 |
val rename_term: term -> term
|
|
36 |
val get_defn: theory -> string -> typ -> ((term list * term) * int option) option
|
|
37 |
val is_instance: theory -> typ -> typ -> bool
|
|
38 |
val parens: Pretty.T -> Pretty.T
|
|
39 |
val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
|
|
40 |
val eta_expand: term -> term list -> int -> term
|
|
41 |
val parsers: OuterSyntax.parser list
|
|
42 |
val setup: (theory -> theory) list
|
|
43 |
end;
|
|
44 |
|
|
45 |
structure Codegen : CODEGEN =
|
|
46 |
struct
|
|
47 |
|
|
48 |
val quiet_mode = ref true;
|
|
49 |
fun message s = if !quiet_mode then () else writeln s;
|
|
50 |
|
|
51 |
(**** Mixfix syntax ****)
|
|
52 |
|
|
53 |
datatype mixfix =
|
|
54 |
Arg
|
|
55 |
| Ignore
|
|
56 |
| Pretty of Pretty.T
|
|
57 |
| Term of term;
|
|
58 |
|
|
59 |
fun is_arg Arg = true
|
|
60 |
| is_arg Ignore = true
|
|
61 |
| is_arg _ = false;
|
|
62 |
|
|
63 |
fun terms_of [] = []
|
|
64 |
| terms_of (Term t :: ms) = t :: terms_of ms
|
|
65 |
| terms_of (_ :: ms) = terms_of ms;
|
|
66 |
|
|
67 |
val num_args = length o filter is_arg;
|
|
68 |
|
|
69 |
|
|
70 |
(**** theory data ****)
|
|
71 |
|
|
72 |
(* data kind 'Pure/codegen' *)
|
|
73 |
|
|
74 |
structure CodegenArgs =
|
|
75 |
struct
|
|
76 |
val name = "Pure/codegen";
|
|
77 |
type T =
|
|
78 |
{codegens : (string * (theory -> (exn option * string) Graph.T -> string ->
|
|
79 |
bool -> term -> ((exn option * string) Graph.T * Pretty.T) option)) list,
|
|
80 |
consts : ((string * typ) * mixfix list) list,
|
|
81 |
types : (string * string) list};
|
|
82 |
|
|
83 |
val empty = {codegens = [], consts = [], types = []};
|
|
84 |
val copy = I;
|
|
85 |
val prep_ext = I;
|
|
86 |
|
|
87 |
fun merge ({codegens = codegens1, consts = consts1, types = types1},
|
|
88 |
{codegens = codegens2, consts = consts2, types = types2}) =
|
|
89 |
{codegens = rev (merge_alists (rev codegens1) (rev codegens2)),
|
|
90 |
consts = merge_alists consts1 consts2,
|
|
91 |
types = merge_alists types1 types2};
|
|
92 |
|
|
93 |
fun print sg (cs:T) = Pretty.writeln
|
|
94 |
(Pretty.strs ("code generators:" :: map fst (#codegens cs)));
|
|
95 |
end;
|
|
96 |
|
|
97 |
structure CodegenData = TheoryDataFun(CodegenArgs);
|
|
98 |
val print_codegens = CodegenData.print;
|
|
99 |
|
|
100 |
|
|
101 |
(**** add new code generator to theory ****)
|
|
102 |
|
|
103 |
fun add_codegen name f thy =
|
|
104 |
let val {codegens, consts, types} = CodegenData.get thy
|
|
105 |
in (case assoc (codegens, name) of
|
|
106 |
None => CodegenData.put {codegens = (name, f)::codegens,
|
|
107 |
consts = consts, types = types} thy
|
|
108 |
| Some _ => error ("Code generator " ^ name ^ " already declared"))
|
|
109 |
end;
|
|
110 |
|
|
111 |
|
|
112 |
(**** associate constants with target language code ****)
|
|
113 |
|
|
114 |
fun gen_assoc_consts prep_type xs thy = foldl (fn (thy, (s, tyopt, syn)) =>
|
|
115 |
let
|
|
116 |
val sg = sign_of thy;
|
|
117 |
val {codegens, consts, types} = CodegenData.get thy;
|
|
118 |
val cname = Sign.intern_const sg s;
|
|
119 |
in
|
|
120 |
(case Sign.const_type sg cname of
|
|
121 |
Some T =>
|
|
122 |
let val T' = (case tyopt of
|
|
123 |
None => T
|
|
124 |
| Some ty =>
|
|
125 |
let val U = prep_type sg ty
|
|
126 |
in if Type.typ_instance (Sign.tsig_of sg, U, T) then U
|
|
127 |
else error ("Illegal type constraint for constant " ^ cname)
|
|
128 |
end)
|
|
129 |
in (case assoc (consts, (cname, T')) of
|
|
130 |
None => CodegenData.put {codegens = codegens,
|
|
131 |
consts = ((cname, T'), syn) :: consts, types = types} thy
|
|
132 |
| Some _ => error ("Constant " ^ cname ^ " already associated with code"))
|
|
133 |
end
|
|
134 |
| _ => error ("Not a constant: " ^ s))
|
|
135 |
end) (thy, xs);
|
|
136 |
|
|
137 |
val assoc_consts_i = gen_assoc_consts (K I);
|
|
138 |
val assoc_consts = gen_assoc_consts (fn sg => typ_of o read_ctyp sg);
|
|
139 |
|
|
140 |
(**** associate types with target language types ****)
|
|
141 |
|
|
142 |
fun assoc_types xs thy = foldl (fn (thy, (s, syn)) =>
|
|
143 |
let
|
|
144 |
val {codegens, consts, types} = CodegenData.get thy;
|
|
145 |
val tc = Sign.intern_tycon (sign_of thy) s
|
|
146 |
in
|
|
147 |
(case assoc (types, tc) of
|
|
148 |
None => CodegenData.put {codegens = codegens, consts = consts,
|
|
149 |
types = (tc, syn) :: types} thy
|
|
150 |
| Some _ => error ("Type " ^ tc ^ " already associated with code"))
|
|
151 |
end) (thy, xs);
|
|
152 |
|
|
153 |
fun get_assoc_types thy = #types (CodegenData.get thy);
|
11546
|
154 |
|
11520
|
155 |
|
|
156 |
(**** retrieve definition of constant ****)
|
|
157 |
|
|
158 |
fun is_instance thy T1 T2 =
|
|
159 |
Type.typ_instance (Sign.tsig_of (sign_of thy), T1, Type.varifyT T2);
|
|
160 |
|
|
161 |
fun get_assoc_code thy s T = apsome snd (find_first (fn ((s', T'), _) =>
|
|
162 |
s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
|
|
163 |
|
|
164 |
fun get_defn thy s T =
|
|
165 |
let
|
|
166 |
val axms = flat (map (Symtab.dest o #axioms o Theory.rep_theory)
|
|
167 |
(thy :: Theory.ancestors_of thy));
|
|
168 |
val defs = mapfilter (fn (_, t) =>
|
|
169 |
(let
|
|
170 |
val (lhs, rhs) = Logic.dest_equals t;
|
|
171 |
val (c, args) = strip_comb lhs;
|
|
172 |
val (s', T') = dest_Const c
|
|
173 |
in if s=s' then Some (T', (args, rhs)) else None end) handle TERM _ =>
|
|
174 |
None) axms;
|
|
175 |
val i = find_index (is_instance thy T o fst) defs
|
|
176 |
in
|
|
177 |
if i>=0 then Some (snd (nth_elem (i, defs)),
|
|
178 |
if length defs = 1 then None else Some i)
|
|
179 |
else None
|
|
180 |
end;
|
|
181 |
|
|
182 |
|
|
183 |
(**** make valid ML identifiers ****)
|
|
184 |
|
|
185 |
fun gen_mk_id kind rename sg s =
|
|
186 |
let
|
|
187 |
val (xs as x::_) = explode (rename (space_implode "_"
|
|
188 |
(NameSpace.unpack (Sign.cond_extern sg kind s))));
|
|
189 |
fun check_str [] = ""
|
|
190 |
| check_str (x::xs) =
|
|
191 |
(if Symbol.is_letter x orelse Symbol.is_digit x orelse x="_" then x
|
|
192 |
else "_" ^ string_of_int (ord x)) ^ check_str xs
|
|
193 |
in
|
|
194 |
(if not (Symbol.is_letter x) then "id" else "") ^ check_str xs
|
|
195 |
end;
|
|
196 |
|
|
197 |
val mk_const_id = gen_mk_id Sign.constK I;
|
|
198 |
val mk_type_id = gen_mk_id Sign.typeK
|
|
199 |
(fn s => if s mem ThmDatabase.ml_reserved then s ^ "_type" else s);
|
|
200 |
|
|
201 |
fun rename_term t =
|
|
202 |
let
|
|
203 |
val names = add_term_names (t, map (fst o fst o dest_Var) (term_vars t));
|
|
204 |
val clash = names inter ThmDatabase.ml_reserved;
|
|
205 |
val ps = clash ~~ variantlist (clash, names);
|
|
206 |
|
|
207 |
fun rename (Var ((a, i), T)) = Var ((if_none (assoc (ps, a)) a, i), T)
|
|
208 |
| rename (Free (a, T)) = Free (if_none (assoc (ps, a)) a, T)
|
|
209 |
| rename (Abs (s, T, t)) = Abs (s, T, rename t)
|
|
210 |
| rename (t $ u) = rename t $ rename u
|
|
211 |
| rename t = t;
|
|
212 |
in
|
|
213 |
rename t
|
|
214 |
end;
|
|
215 |
|
|
216 |
|
|
217 |
(**** invoke suitable code generator for term t ****)
|
|
218 |
|
|
219 |
fun invoke_codegen thy gr dep brack t = (case get_first
|
|
220 |
(fn (_, f) => f thy gr dep brack t) (#codegens (CodegenData.get thy)) of
|
|
221 |
None => error ("Unable to generate code for term:\n" ^
|
|
222 |
Sign.string_of_term (sign_of thy) t ^ "\nrequired by:\n" ^
|
|
223 |
commas (Graph.all_succs gr [dep]))
|
|
224 |
| Some x => x)
|
|
225 |
|
|
226 |
|
|
227 |
(**** code generator for mixfix expressions ****)
|
|
228 |
|
|
229 |
fun parens p = Pretty.block [Pretty.str "(", p, Pretty.str ")"];
|
|
230 |
|
|
231 |
fun pretty_fn [] p = [p]
|
|
232 |
| pretty_fn (x::xs) p = Pretty.str ("fn " ^ x ^ " =>") ::
|
|
233 |
Pretty.brk 1 :: pretty_fn xs p;
|
|
234 |
|
|
235 |
fun pretty_mixfix [] [] _ = []
|
|
236 |
| pretty_mixfix (Arg :: ms) (p :: ps) qs = p :: pretty_mixfix ms ps qs
|
|
237 |
| pretty_mixfix (Ignore :: ms) (p :: ps) qs = pretty_mixfix ms ps qs
|
|
238 |
| pretty_mixfix (Pretty p :: ms) ps qs = p :: pretty_mixfix ms ps qs
|
|
239 |
| pretty_mixfix (Term _ :: ms) ps (q :: qs) = q :: pretty_mixfix ms ps qs;
|
|
240 |
|
|
241 |
|
|
242 |
(**** default code generator ****)
|
|
243 |
|
|
244 |
fun eta_expand t ts i =
|
|
245 |
let
|
|
246 |
val (Ts, _) = strip_type (fastype_of t);
|
|
247 |
val j = i - length ts
|
|
248 |
in
|
|
249 |
foldr (fn (T, t) => Abs ("x", T, t))
|
|
250 |
(take (j, Ts), list_comb (t, ts @ map Bound (j-1 downto 0)))
|
|
251 |
end;
|
|
252 |
|
|
253 |
fun mk_app _ p [] = p
|
|
254 |
| mk_app brack p ps = if brack then
|
|
255 |
Pretty.block (Pretty.str "(" ::
|
|
256 |
separate (Pretty.brk 1) (p :: ps) @ [Pretty.str ")"])
|
|
257 |
else Pretty.block (separate (Pretty.brk 1) (p :: ps));
|
|
258 |
|
|
259 |
fun new_names t xs = variantlist (xs,
|
|
260 |
map (fst o fst o dest_Var) (term_vars t) union
|
|
261 |
add_term_names (t, ThmDatabase.ml_reserved));
|
|
262 |
|
|
263 |
fun new_name t x = hd (new_names t [x]);
|
|
264 |
|
|
265 |
fun default_codegen thy gr dep brack t =
|
|
266 |
let
|
|
267 |
val (u, ts) = strip_comb t;
|
|
268 |
fun mapcode brack' gr ts = foldl_map
|
|
269 |
(fn (gr, t) => invoke_codegen thy gr dep brack' t) (gr, ts)
|
|
270 |
|
|
271 |
in (case u of
|
|
272 |
Var ((s, i), _) =>
|
|
273 |
let val (gr', ps) = mapcode true gr ts
|
|
274 |
in Some (gr', mk_app brack (Pretty.str (s ^
|
|
275 |
(if i=0 then "" else string_of_int i))) ps)
|
|
276 |
end
|
|
277 |
|
|
278 |
| Free (s, _) =>
|
|
279 |
let val (gr', ps) = mapcode true gr ts
|
|
280 |
in Some (gr', mk_app brack (Pretty.str s) ps) end
|
|
281 |
|
|
282 |
| Const (s, T) =>
|
|
283 |
(case get_assoc_code thy s T of
|
|
284 |
Some ms =>
|
|
285 |
let val i = num_args ms
|
|
286 |
in if length ts < i then
|
|
287 |
default_codegen thy gr dep brack (eta_expand u ts i)
|
|
288 |
else
|
|
289 |
let
|
|
290 |
val ts1 = take (i, ts);
|
|
291 |
val ts2 = drop (i, ts);
|
|
292 |
val (gr1, ps1) = mapcode false gr ts1;
|
|
293 |
val (gr2, ps2) = mapcode true gr1 ts2;
|
|
294 |
val (gr3, ps3) = mapcode false gr2 (terms_of ms);
|
|
295 |
in
|
|
296 |
Some (gr3, mk_app brack (Pretty.block (pretty_mixfix ms ps1 ps3)) ps2)
|
|
297 |
end
|
|
298 |
end
|
|
299 |
| None => (case get_defn thy s T of
|
|
300 |
None => None
|
|
301 |
| Some ((args, rhs), k) =>
|
|
302 |
let
|
|
303 |
val id = mk_const_id (sign_of thy) s ^ (case k of
|
|
304 |
None => "" | Some i => "_def" ^ string_of_int i);
|
|
305 |
val (gr', ps) = mapcode true gr ts;
|
|
306 |
in
|
|
307 |
Some (Graph.add_edge (id, dep) gr' handle Graph.UNDEF _ =>
|
|
308 |
let
|
|
309 |
val _ = message ("expanding definition of " ^ s);
|
|
310 |
val (Ts, _) = strip_type T;
|
|
311 |
val (args', rhs') =
|
|
312 |
if not (null args) orelse null Ts then (args, rhs) else
|
|
313 |
let val v = Free (new_name rhs "x", hd Ts)
|
|
314 |
in ([v], betapply (rhs, v)) end;
|
|
315 |
val (gr1, p) = invoke_codegen thy (Graph.add_edge (id, dep)
|
|
316 |
(Graph.new_node (id, (None, "")) gr')) id false rhs';
|
|
317 |
val (gr2, xs) = mapcode false gr1 args';
|
|
318 |
in Graph.map_node id (K (None, Pretty.string_of (Pretty.block
|
|
319 |
(Pretty.str (if null args' then "val " else "fun ") ::
|
|
320 |
separate (Pretty.brk 1) (Pretty.str id :: xs) @
|
|
321 |
[Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr2
|
|
322 |
end, mk_app brack (Pretty.str id) ps)
|
|
323 |
end))
|
|
324 |
|
|
325 |
| Abs _ =>
|
|
326 |
let
|
|
327 |
val (bs, Ts) = ListPair.unzip (strip_abs_vars u);
|
|
328 |
val t = strip_abs_body u
|
|
329 |
val bs' = new_names t bs;
|
|
330 |
val (gr1, ps) = mapcode true gr ts;
|
|
331 |
val (gr2, p) = invoke_codegen thy gr1 dep false
|
|
332 |
(subst_bounds (map Free (rev (bs' ~~ Ts)), t));
|
|
333 |
in
|
|
334 |
Some (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @
|
|
335 |
[Pretty.str ")"])) ps)
|
|
336 |
end
|
|
337 |
|
|
338 |
| _ => None)
|
|
339 |
end;
|
|
340 |
|
|
341 |
|
|
342 |
fun output_code gr xs = implode (map (snd o Graph.get_node gr)
|
|
343 |
(rev (Graph.all_preds gr xs)));
|
|
344 |
|
|
345 |
fun gen_generate_code prep_term thy = Pretty.setmp_margin 80 (fn xs =>
|
|
346 |
let
|
|
347 |
val sg = sign_of thy;
|
|
348 |
val gr = Graph.new_node ("<Top>", (None, "")) Graph.empty;
|
|
349 |
val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
|
|
350 |
(invoke_codegen thy gr "<Top>" false t)) (gr, map (apsnd (prep_term sg)) xs)
|
|
351 |
in
|
|
352 |
"structure Generated =\nstruct\n\n" ^
|
|
353 |
output_code gr' ["<Top>"] ^
|
|
354 |
space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
|
|
355 |
[Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
|
|
356 |
"\n\nend;\n\nopen Generated;\n"
|
|
357 |
end);
|
|
358 |
|
|
359 |
val generate_code_i = gen_generate_code (K I);
|
|
360 |
val generate_code = gen_generate_code
|
|
361 |
(fn sg => term_of o read_cterm sg o rpair TypeInfer.logicT);
|
|
362 |
|
|
363 |
fun parse_mixfix rd s =
|
|
364 |
(case Scan.finite Symbol.stopper (Scan.repeat
|
|
365 |
( $$ "_" >> K Arg
|
|
366 |
|| $$ "?" >> K Ignore
|
|
367 |
|| $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
|
|
368 |
|| $$ "{" |-- $$ "*" |-- Scan.repeat1
|
|
369 |
( $$ "'" |-- Scan.one Symbol.not_eof
|
|
370 |
|| Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
|
|
371 |
$$ "*" --| $$ "}" >> (Term o rd o implode)
|
|
372 |
|| Scan.repeat1
|
|
373 |
( $$ "'" |-- Scan.one Symbol.not_eof
|
|
374 |
|| Scan.unless ($$ "_" || $$ "?" || $$ "/" || $$ "{" |-- $$ "*")
|
|
375 |
(Scan.one Symbol.not_eof)) >> (Pretty o Pretty.str o implode)))
|
|
376 |
(Symbol.explode s) of
|
|
377 |
(p, []) => p
|
|
378 |
| _ => error ("Malformed annotation: " ^ quote s));
|
|
379 |
|
11546
|
380 |
structure P = OuterParse and K = OuterSyntax.Keyword;
|
11520
|
381 |
|
|
382 |
val assoc_typeP =
|
|
383 |
OuterSyntax.command "types_code"
|
11546
|
384 |
"associate types with target language types" K.thy_decl
|
11520
|
385 |
(Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")") >>
|
|
386 |
(Toplevel.theory o assoc_types));
|
|
387 |
|
|
388 |
val assoc_constP =
|
|
389 |
OuterSyntax.command "consts_code"
|
11546
|
390 |
"associate constants with target language code" K.thy_decl
|
11520
|
391 |
(Scan.repeat1
|
|
392 |
(P.xname -- (Scan.option (P.$$$ "::" |-- P.string)) --|
|
|
393 |
P.$$$ "(" -- P.string --| P.$$$ ")") >>
|
|
394 |
(fn xs => Toplevel.theory (fn thy => assoc_consts
|
|
395 |
(map (fn ((name, optype), mfx) => (name, optype, parse_mixfix
|
|
396 |
(term_of o read_cterm (sign_of thy) o rpair TypeInfer.logicT) mfx))
|
|
397 |
xs) thy)));
|
|
398 |
|
|
399 |
val generate_codeP =
|
11546
|
400 |
OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl
|
11520
|
401 |
(Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")") --
|
11546
|
402 |
Scan.repeat1 (P.name --| P.$$$ "=" -- P.string) >>
|
11520
|
403 |
(fn (opt_fname, xs) => Toplevel.theory (fn thy =>
|
|
404 |
((case opt_fname of
|
|
405 |
None => use_text Context.ml_output false
|
|
406 |
| Some fname => File.write (Path.unpack fname))
|
|
407 |
(generate_code thy xs); thy))));
|
|
408 |
|
|
409 |
val parsers = [assoc_typeP, assoc_constP, generate_codeP];
|
|
410 |
|
|
411 |
val setup = [CodegenData.init, add_codegen "default" default_codegen];
|
|
412 |
|
|
413 |
end;
|
|
414 |
|
|
415 |
OuterSyntax.add_parsers Codegen.parsers;
|