src/Tools/Code/code_target.ML
changeset 41351 e82fc600a3a5
parent 41344 d990badc97a3
child 41364 aaf5968c67ef
equal deleted inserted replaced
41350:ce825d32b450 41351:e82fc600a3a5
   419     val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
   419     val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
   420     val value_name = "Value.value.value"
   420     val value_name = "Value.value.value"
   421     val program = prepared_program
   421     val program = prepared_program
   422       |> Graph.new_node (value_name,
   422       |> Graph.new_node (value_name,
   423           Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
   423           Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
   424       |> fold (curry Graph.add_edge value_name) deps;
   424       |> fold (curry (perhaps o try o Graph.add_edge) value_name) deps;
   425     val (program_code, deresolve) = produce (mounted_serializer program);
   425     val (program_code, deresolve) = produce (mounted_serializer program);
   426     val value_name' = the (deresolve value_name);
   426     val value_name' = the (deresolve value_name);
   427   in (program_code, value_name') end;
   427   in (program_code, value_name') end;
   428 
   428 
   429 fun evaluator thy target naming program deps =
   429 fun evaluator thy target naming program deps =