492 (if member (op =) cTs (SOME cT) then NONE else SOME cT) :: cTs) raw_computation_cTs []; |
492 (if member (op =) cTs (SOME cT) then NONE else SOME cT) :: cTs) raw_computation_cTs []; |
493 val consts' = fold (fn NONE => I | SOME (c, _) => insert (op =) c) |
493 val consts' = fold (fn NONE => I | SOME (c, _) => insert (op =) c) |
494 computation_cTs named_consts; |
494 computation_cTs named_consts; |
495 val program' = Code_Thingol.consts_program ctxt consts'; |
495 val program' = Code_Thingol.consts_program ctxt consts'; |
496 (*FIXME insufficient interfaces require double invocation of code generator*) |
496 (*FIXME insufficient interfaces require double invocation of code generator*) |
|
497 val program'' = Code_Symbol.Graph.merge (K true) (program, program'); |
497 val ((ml_modules, compiled_value), deresolve) = |
498 val ((ml_modules, compiled_value), deresolve) = |
498 Code_Target.compilation_text' ctxt target some_module_name program' |
499 Code_Target.compilation_text' ctxt target some_module_name program'' |
499 (map Code_Symbol.Type_Constructor named_tycos @ map Code_Symbol.Constant consts' @ deps) true vs_ty_evals; |
500 (map Code_Symbol.Type_Constructor named_tycos @ map Code_Symbol.Constant consts' @ deps) true vs_ty_evals; |
500 (*FIXME constrain signature*) |
501 (*FIXME constrain signature*) |
501 fun deresolve_const c = case (deresolve o Code_Symbol.Constant) c of |
502 fun deresolve_const c = case (deresolve o Code_Symbol.Constant) c of |
502 NONE => error ("Constant " ^ (quote o Code.string_of_const thy) c ^ |
503 NONE => error ("Constant " ^ (quote o Code.string_of_const thy) c ^ |
503 "\nhas a user-defined serialization") |
504 "\nhas a user-defined serialization") |