85 fun reject_vars thy t = |
85 fun reject_vars thy t = |
86 let |
86 let |
87 val ctxt = Proof_Context.init_global thy; |
87 val ctxt = Proof_Context.init_global thy; |
88 in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end; |
88 in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end; |
89 |
89 |
90 fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target); |
90 fun obtain_evaluator thy some_target naming program consts expr = |
|
91 Code_Target.evaluator thy (the_default target some_target) naming program consts expr |
|
92 |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules)); |
91 |
93 |
92 fun evaluation cookie thy evaluator vs_t args = |
94 fun evaluation cookie thy evaluator vs_t args = |
93 let |
95 let |
94 val ctxt = Proof_Context.init_global thy; |
96 val ctxt = Proof_Context.init_global thy; |
95 val (program_code, value_name) = evaluator vs_t; |
97 val (program_code, value_name) = evaluator vs_t; |
190 fun evaluation_code thy module_name tycos consts = |
192 fun evaluation_code thy module_name tycos consts = |
191 let |
193 let |
192 val ctxt = Proof_Context.init_global thy; |
194 val ctxt = Proof_Context.init_global thy; |
193 val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts; |
195 val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts; |
194 val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; |
196 val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; |
195 val (ml_code, target_names) = |
197 val (ml_modules, target_names) = |
196 Code_Target.produce_code_for thy |
198 Code_Target.produce_code_for thy |
197 target NONE module_name [] naming program (consts' @ tycos'); |
199 target NONE module_name [] naming program (consts' @ tycos'); |
|
200 val ml_code = space_implode "\n\n" (map snd ml_modules); |
198 val (consts'', tycos'') = chop (length consts') target_names; |
201 val (consts'', tycos'') = chop (length consts') target_names; |
199 val consts_map = map2 (fn const => |
202 val consts_map = map2 (fn const => |
200 fn NONE => |
203 fn NONE => |
201 error ("Constant " ^ (quote o Code.string_of_const thy) const ^ |
204 error ("Constant " ^ (quote o Code.string_of_const thy) const ^ |
202 "\nhas a user-defined serialization") |
205 "\nhas a user-defined serialization") |