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 (j1 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;
