src/Tools/Code/code_target.ML
changeset 36271 2ef9dbddfcb8
parent 36121 86b952fc31da
child 36471 5aae37575885
equal deleted inserted replaced
36262:d7d1d87276b7 36271:2ef9dbddfcb8
   327 
   327 
   328 (* code presentation *)
   328 (* code presentation *)
   329 
   329 
   330 fun code_of thy target some_width module_name cs names_stmt =
   330 fun code_of thy target some_width module_name cs names_stmt =
   331   let
   331   let
   332     val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
   332     val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
   333   in
   333   in
   334     string (names_stmt naming)
   334     string (names_stmt naming)
   335       (serialize thy target some_width (SOME module_name) [] naming program names_cs)
   335       (serialize thy target some_width (SOME module_name) [] naming program names_cs)
   336   end;
   336   end;
   337 
   337 
   345   in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
   345   in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
   346 
   346 
   347 fun read_const_exprs thy cs =
   347 fun read_const_exprs thy cs =
   348   let
   348   let
   349     val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
   349     val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
   350     val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
   350     val (names2, (naming, program)) = Code_Thingol.consts_program thy true cs2;
   351     val names4 = transitivly_non_empty_funs thy naming program;
   351     val names3 = transitivly_non_empty_funs thy naming program;
   352     val cs5 = map_filter
   352     val cs3 = map_filter (fn (c, name) =>
   353       (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
   353       if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
   354   in fold (insert (op =)) cs5 cs1 end;
   354   in union (op =) cs3 cs1 end;
   355 
   355 
   356 fun export_code thy cs seris =
   356 fun export_code thy cs seris =
   357   let
   357   let
   358     val (cs', (naming, program)) = Code_Thingol.consts_program thy cs;
   358     val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
   359     fun mk_seri_dest dest = case dest
   359     fun mk_seri_dest dest = case dest
   360      of NONE => compile
   360      of NONE => compile
   361       | SOME "-" => export
   361       | SOME "-" => export
   362       | SOME f => file (Path.explode f)
   362       | SOME f => file (Path.explode f)
   363     val _ = map (fn (((target, module), dest), args) =>
   363     val _ = map (fn (((target, module), dest), args) =>