49 val value_name = "Value.VALUE.value" |
49 val value_name = "Value.VALUE.value" |
50 val program' = program |
50 val program' = program |
51 |> Graph.new_node (value_name, |
51 |> Graph.new_node (value_name, |
52 Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE))) |
52 Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE))) |
53 |> fold (curry Graph.add_edge value_name) deps; |
53 |> fold (curry Graph.add_edge value_name) deps; |
54 val (value_code, [SOME value_name']) = Code_Target.produce_code_for thy |
54 val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy |
55 (the_default target some_target) NONE (SOME "") [] naming program [value_name]; |
55 (the_default target some_target) NONE (SOME "Code") [] naming program' [value_name]; |
56 val sml_code = "let\n" ^ value_code ^ "\nin " ^ Long_Name.base_name value_name' |
56 val value_code = space_implode " " |
57 ^ space_implode " " (map (enclose "(" ")") args) ^ " end"; |
57 (value_name' :: map (enclose "(" ")") args); |
58 in ML_Context.evaluate ctxt false reff sml_code end; |
58 in ML_Context.evaluate ctxt false reff (program_code, value_code) end; |
59 in Code_Thingol.dynamic_eval_value thy postproc evaluator t end; |
59 in Code_Thingol.dynamic_eval_value thy postproc evaluator t end; |
60 |
60 |
61 |
61 |
62 (** instrumentalization by antiquotation **) |
62 (** instrumentalization by antiquotation **) |
63 |
63 |