# HG changeset patch # User haftmann # Date 1283252938 -7200 # Node ID 15f8cffdbf5d30e0823d7fff7abb8859a6a23dd0 # Parent fd6b9bdb428e81834ba067dcb1a0949f30ddab3d dropped legacy interfaces diff -r fd6b9bdb428e -r 15f8cffdbf5d doc-src/more_antiquote.ML --- a/doc-src/more_antiquote.ML Mon Aug 30 18:32:40 2010 +0200 +++ b/doc-src/more_antiquote.ML Tue Aug 31 13:08:58 2010 +0200 @@ -127,9 +127,9 @@ (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name)) (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) => let val thy = ProofContext.theory_of ctxt in - Code_Target.code_of thy - target NONE "Example" (mk_cs thy) + Code_Target.produce_code thy (mk_cs thy) (fn naming => maps (fn f => f thy naming) mk_stmtss) + target NONE (SOME "Example") [] |> fst |> typewriter end); diff -r fd6b9bdb428e -r 15f8cffdbf5d src/Tools/Code/code_eval.ML --- a/src/Tools/Code/code_eval.ML Mon Aug 30 18:32:40 2010 +0200 +++ b/src/Tools/Code/code_eval.ML Tue Aug 31 13:08:58 2010 +0200 @@ -29,8 +29,8 @@ val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; val struct_name = if struct_name_hint = "" then eval_struct_name else struct_name_hint; - val (ml_code, target_names) = Code_ML.evaluation_code_of thy target - struct_name naming program (consts' @ tycos'); + val (ml_code, target_names) = Code_Target.produce_code_for thy + target NONE (SOME struct_name) [] naming program (consts' @ tycos', []); val (consts'', tycos'') = chop (length consts') target_names; val consts_map = map2 (fn const => fn NONE => error ("Constant " ^ (quote o Code.string_of_const thy) const @@ -57,8 +57,8 @@ |> Graph.new_node (value_name, Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE))) |> fold (curry Graph.add_edge value_name) deps; - val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy - (the_default target some_target) "" naming program' [value_name]; + val (value_code, [SOME value_name']) = Code_Target.produce_code_for thy + (the_default target some_target) NONE (SOME "") [] naming program ([value_name], []); val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name' ^ space_implode " " (map (enclose "(" ")") args) ^ " end"; in ML_Context.evaluate ctxt false reff sml_code end; diff -r fd6b9bdb428e -r 15f8cffdbf5d src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Mon Aug 30 18:32:40 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Tue Aug 31 13:08:58 2010 +0200 @@ -8,8 +8,6 @@ sig val target_SML: string val target_OCaml: string - val evaluation_code_of: theory -> string -> string - -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T) -> Code_Printer.fixity -> 'a list -> Pretty.T option val setup: theory -> theory @@ -943,13 +941,6 @@ end; (*local*) -(** for instrumentalization **) - -fun evaluation_code_of thy target struct_name = - Code_Target.serialize_custom thy (target, fn module_name => fn [] => - serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name); - - (** Isar setup **) fun isar_serializer_sml module_name = diff -r fd6b9bdb428e -r 15f8cffdbf5d src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Mon Aug 30 18:32:40 2010 +0200 +++ b/src/Tools/Code/code_target.ML Tue Aug 31 13:08:58 2010 +0200 @@ -42,12 +42,6 @@ -> 'a -> int -> serialization val set_default_code_width: int -> theory -> theory - (*FIXME drop asap*) - val code_of: theory -> string -> int option -> string - -> string list -> (Code_Thingol.naming -> string list) -> string * string option list - val serialize_custom: theory -> string * serializer -> string option - -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list - val allow_abort: string -> theory -> theory type tyco_syntax = Code_Printer.tyco_syntax type const_syntax = Code_Printer.const_syntax @@ -77,8 +71,8 @@ fun stmt_names_of_destination (String stmt_names) = stmt_names | stmt_names_of_destination _ = []; -fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE) - | serialization _ string pretty width (String _) = SOME (string width pretty); +fun serialization output _ content width (File some_path) = (output width some_path content; NONE) + | serialization _ string content width (String _) = SOME (string width content); fun file some_path f = (f (File some_path); ()); fun string stmt_names f = the (f (String stmt_names)); @@ -291,7 +285,7 @@ program4 (names1, presentation_names) width end; -fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination = +fun mount_serializer thy target some_width raw_module_name args naming program names destination = let val ((targets, abortable), default_width) = Targets.get thy; fun collapse_hierarchy target = @@ -306,8 +300,8 @@ in (modify' #> modify naming, merge_target false target (data', data)) end end; val (modify, data) = collapse_hierarchy target; - val serializer = the_default (case the_description data - of Fundamental seri => #serializer seri) alt_serializer; + val serializer = case the_description data + of Fundamental seri => #serializer seri; val presentation_names = stmt_names_of_destination destination; val module_name = if null presentation_names then raw_module_name else SOME "Code"; @@ -332,13 +326,11 @@ in -fun serialize thy = mount_serializer thy NONE; - fun export_code_for thy some_path target some_width some_module_name args naming program names = - file some_path (serialize thy target some_width some_module_name args naming program names); + file some_path (mount_serializer thy target some_width some_module_name args naming program names); fun produce_code_for thy target some_width some_module_name args naming program (names, selects) = - string selects (serialize thy target some_width some_module_name args naming program names); + string selects (mount_serializer thy target some_width some_module_name args naming program names); fun check_code_for thy target strict args naming program names_cs = let @@ -349,7 +341,7 @@ fun ext_check env_param p = let val destination = make_destination p; - val _ = file (SOME destination) (serialize thy target (SOME 80) + val _ = file (SOME destination) (mount_serializer thy target (SOME 80) (SOME 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 @@ -363,24 +355,9 @@ else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param) end; -fun serialize_custom thy (target_name, seri) module_name naming program names = - mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String []) - |> the; - end; (* local *) -(* code presentation *) - -fun code_of thy target some_width module_name cs names_stmt = - let - val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; - in - string (names_stmt naming) - (serialize thy target some_width (SOME module_name) [] naming program names_cs) - end; - - (* code generation *) fun transitivly_non_empty_funs thy naming program =