# HG changeset patch # User haftmann # Date 1292919363 -3600 # Node ID e284a364f724b683f891f7f2113e356fb155e850 # Parent e65a122057ad39d8c658c0a6e7dede8c99307624# Parent d990badc97a3f73b54d6d316396de2a55e9fe362 merged diff -r e65a122057ad -r e284a364f724 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Tue Dec 21 08:38:03 2010 +0100 +++ b/src/Tools/Code/code_haskell.ML Tue Dec 21 09:16:03 2010 +0100 @@ -296,7 +296,7 @@ end; fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms, - includes, module_alias, class_syntax, tyco_syntax, const_syntax, program } = + includes, module_alias, class_syntax, tyco_syntax, const_syntax } program = let (* build program *) diff -r e65a122057ad -r e284a364f724 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Dec 21 08:38:03 2010 +0100 +++ b/src/Tools/Code/code_ml.ML Tue Dec 21 09:16:03 2010 +0100 @@ -789,7 +789,7 @@ fun serialize_ml target print_ml_module print_ml_stmt with_signatures { labelled_name, reserved_syms, includes, module_alias, - class_syntax, tyco_syntax, const_syntax, program } = + class_syntax, tyco_syntax, const_syntax } program = let (* build program *) diff -r e65a122057ad -r e284a364f724 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Tue Dec 21 08:38:03 2010 +0100 +++ b/src/Tools/Code/code_runtime.ML Tue Dec 21 09:16:03 2010 +0100 @@ -95,7 +95,7 @@ val _ = if Code_Thingol.contains_dict_var t then error "Term to be evaluated contains free dictionaries" else (); val v' = Name.variant (map fst vs) "a"; - val vs' = (v', []) :: vs + val vs' = (v', []) :: vs; val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty]; val value_name = "Value.value.value" val program' = program diff -r e65a122057ad -r e284a364f724 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Tue Dec 21 08:38:03 2010 +0100 +++ b/src/Tools/Code/code_scala.ML Tue Dec 21 09:16:03 2010 +0100 @@ -329,7 +329,7 @@ end; fun serialize_scala { labelled_name, reserved_syms, includes, - module_alias, class_syntax, tyco_syntax, const_syntax, program } = + module_alias, class_syntax, tyco_syntax, const_syntax } program = let (* build program *) diff -r e65a122057ad -r e284a364f724 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Dec 21 08:38:03 2010 +0100 +++ b/src/Tools/Code/code_target.ML Tue Dec 21 09:16:03 2010 +0100 @@ -28,6 +28,10 @@ val check_code: theory -> string list -> ((string * bool) * Token.T list) list -> unit + val evaluator: theory -> string -> Code_Thingol.naming -> Code_Thingol.program + -> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm + -> string * string + type serializer type literals = Code_Printer.literals val add_target: string * { serializer: serializer, literals: literals, @@ -118,8 +122,8 @@ module_alias: string -> string option, class_syntax: string -> string option, tyco_syntax: string -> Code_Printer.tyco_syntax option, - const_syntax: string -> Code_Printer.activated_const_syntax option, - program: Code_Thingol.program } + const_syntax: string -> Code_Printer.activated_const_syntax option } + -> Code_Thingol.program -> serialization; datatype description = Fundamental of { serializer: serializer, @@ -313,7 +317,7 @@ val program4 = Graph.subgraph (member (op =) names4) program3; in (names4, program4) end; -fun invoke_serializer thy abortable serializer literals reserved all_includes +fun prepare_serializer thy abortable serializer literals reserved all_includes module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax module_name args naming proto_program names = let @@ -328,18 +332,18 @@ then SOME (name, content) else NONE; val includes = map_filter select_include (Symtab.dest all_includes); in - serializer args { + (serializer args { labelled_name = Code_Thingol.labelled_name thy proto_program, reserved_syms = reserved, includes = includes, module_alias = if module_name = "" then Symtab.lookup module_alias else K (SOME module_name), class_syntax = Symtab.lookup class_syntax, tyco_syntax = Symtab.lookup tyco_syntax, - const_syntax = Symtab.lookup const_syntax, - program = program } + const_syntax = Symtab.lookup const_syntax }, + program) end; -fun mount_serializer thy target some_width module_name args = +fun mount_serializer thy target some_width module_name args naming program names = let val (default_width, abortable, data, modify) = activate_target thy target; val serializer = case the_description data @@ -348,12 +352,18 @@ val module_alias = the_module_alias data val { class, instance, tyco, const } = the_symbol_syntax data; val literals = the_literals thy target; + val (prepared_serializer, prepared_program) = prepare_serializer thy + abortable serializer literals reserved (the_includes data) module_alias + class instance tyco const module_name args + naming (modify naming program) names val width = the_default default_width some_width; - in fn naming => fn program => fn names => - invoke_serializer thy abortable serializer literals reserved - (the_includes data) module_alias class instance tyco const module_name args - naming (modify naming program) names width - end; + in (fn program => prepared_serializer program width, prepared_program) end; + +fun invoke_serializer thy target some_width module_name args naming program names = + let + val (mounted_serializer, prepared_program) = mount_serializer thy + target some_width module_name args naming program names; + in mounted_serializer prepared_program end; fun assert_module_name "" = error ("Empty module name not allowed.") | assert_module_name module_name = module_name; @@ -361,18 +371,18 @@ in fun export_code_for thy some_path target some_width module_name args = - export some_path ooo mount_serializer thy target some_width module_name args; + export some_path ooo invoke_serializer thy target some_width module_name args; fun produce_code_for thy target some_width module_name args = let - val serializer = mount_serializer thy target some_width (assert_module_name module_name) args; + val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args; in fn naming => fn program => fn names => produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names) end; fun present_code_for thy target some_width module_name args = let - val serializer = mount_serializer thy target some_width (assert_module_name module_name) args; + val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args; in fn naming => fn program => fn (names, selects) => present selects (serializer naming program names) end; @@ -386,7 +396,7 @@ fun ext_check env_param p = let val destination = make_destination p; - val _ = export (SOME destination) (mount_serializer thy target (SOME 80) + val _ = export (SOME destination) (invoke_serializer thy target (SOME 80) module_name args naming program names_cs); val cmd = make_command env_param module_name; in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0 @@ -400,6 +410,28 @@ else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param) end; +fun evaluation mounted_serializer prepared_program deps ((vs, ty), t) = + let + val _ = if Code_Thingol.contains_dict_var t then + error "Term to be evaluated contains free dictionaries" else (); + val v' = Name.variant (map fst vs) "a"; + val vs' = (v', []) :: vs; + val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty]; + val value_name = "Value.value.value" + val program = prepared_program + |> Graph.new_node (value_name, + Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE))) + |> fold (curry Graph.add_edge value_name) deps; + val (program_code, deresolve) = produce (mounted_serializer program); + val value_name' = the (deresolve value_name); + in (program_code, value_name') end; + +fun evaluator thy target naming program deps = + let + val (mounted_serializer, prepared_program) = mount_serializer thy + target NONE "Code" [] naming program deps; + in evaluation mounted_serializer prepared_program deps end; + end; (* local *)