src/Tools/Code/code_runtime.ML
changeset 55683 5732a55b9232
parent 55304 55ac31bc08a4
child 55684 ee49b4f7edc8
equal deleted inserted replaced
55682:def6575032df 55683:5732a55b9232
   197   let
   197   let
   198     val ctxt = Proof_Context.init_global thy;
   198     val ctxt = Proof_Context.init_global thy;
   199     val program = Code_Thingol.consts_program thy consts;
   199     val program = Code_Thingol.consts_program thy consts;
   200     val (ml_modules, target_names) =
   200     val (ml_modules, target_names) =
   201       Code_Target.produce_code_for thy
   201       Code_Target.produce_code_for thy
   202         target NONE module_name [] program (map Constant consts @ map Type_Constructor tycos);
   202         target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos);
   203     val ml_code = space_implode "\n\n" (map snd ml_modules);
   203     val ml_code = space_implode "\n\n" (map snd ml_modules);
   204     val (consts', tycos') = chop (length consts) target_names;
   204     val (consts', tycos') = chop (length consts) target_names;
   205     val consts_map = map2 (fn const =>
   205     val consts_map = map2 (fn const =>
   206       fn NONE =>
   206       fn NONE =>
   207           error ("Constant " ^ (quote o Code.string_of_const thy) const ^
   207           error ("Constant " ^ (quote o Code.string_of_const thy) const ^
   438   |> Code_Target.add_reserved target ml_name
   438   |> Code_Target.add_reserved target ml_name
   439   |> Specification.axiomatization [(b, SOME T, NoSyn)] []
   439   |> Specification.axiomatization [(b, SOME T, NoSyn)] []
   440   |-> (fn ([Const (const, _)], _) =>
   440   |-> (fn ([Const (const, _)], _) =>
   441     Code_Target.set_printings (Constant (const,
   441     Code_Target.set_printings (Constant (const,
   442       [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
   442       [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
   443   #> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
   443   #> tap (fn thy => Code_Target.produce_code thy false [const] target NONE structure_generated []));
   444 
   444 
   445 fun process_file filepath (definienda, thy) =
   445 fun process_file filepath (definienda, thy) =
   446   let
   446   let
   447     val (ml_names, thy') = use_file filepath thy;
   447     val (ml_names, thy') = use_file filepath thy;
   448     val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names;
   448     val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names;