src/Tools/Code/code_eval.ML
changeset 37437 4202e11ae7dc
parent 37216 3165bc303f66
child 37448 3bd4b3809bee
equal deleted inserted replaced
37433:a2a89563bfcb 37437:4202e11ae7dc
    53         val _ = if Code_Thingol.contains_dictvar t then
    53         val _ = if Code_Thingol.contains_dictvar t then
    54           error "Term to be evaluated contains free dictionaries" else ();
    54           error "Term to be evaluated contains free dictionaries" else ();
    55         val value_name = "Value.VALUE.value"
    55         val value_name = "Value.VALUE.value"
    56         val program' = program
    56         val program' = program
    57           |> Graph.new_node (value_name,
    57           |> Graph.new_node (value_name,
    58               Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (NONE, true))])))
    58               Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
    59           |> fold (curry Graph.add_edge value_name) deps;
    59           |> fold (curry Graph.add_edge value_name) deps;
    60         val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
    60         val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
    61           (the_default target some_target) "" naming program' [value_name];
    61           (the_default target some_target) "" naming program' [value_name];
    62         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
    62         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
    63           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
    63           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";