more complete program generation in presence of dictionaries
authorhaftmann
Sat Feb 18 19:49:29 2017 +0100 (2017-02-18)
changeset 650341846c4551153
parent 65033 6be69d6881cd
child 65035 b46fe5138cb0
more complete program generation in presence of dictionaries
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Feb 17 20:01:17 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Feb 18 19:49:29 2017 +0100
     1.3 @@ -494,8 +494,9 @@
     1.4        computation_cTs named_consts;
     1.5      val program' = Code_Thingol.consts_program ctxt consts';
     1.6        (*FIXME insufficient interfaces require double invocation of code generator*)
     1.7 +    val program'' = Code_Symbol.Graph.merge (K true) (program, program');
     1.8      val ((ml_modules, compiled_value), deresolve) =
     1.9 -      Code_Target.compilation_text' ctxt target some_module_name program'
    1.10 +      Code_Target.compilation_text' ctxt target some_module_name program''
    1.11          (map Code_Symbol.Type_Constructor named_tycos @ map Code_Symbol.Constant consts' @ deps) true vs_ty_evals;
    1.12          (*FIXME constrain signature*)
    1.13      fun deresolve_const c = case (deresolve o Code_Symbol.Constant) c of