dropped legacy interfaces
authorhaftmann
Tue Aug 31 13:08:58 2010 +0200 (2010-08-31)
changeset 3892115f8cffdbf5d
parent 38919 fd6b9bdb428e
child 38922 ec2a8efd8990
dropped legacy interfaces
doc-src/more_antiquote.ML
src/Tools/Code/code_eval.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_target.ML
     1.1 --- a/doc-src/more_antiquote.ML	Mon Aug 30 18:32:40 2010 +0200
     1.2 +++ b/doc-src/more_antiquote.ML	Tue Aug 31 13:08:58 2010 +0200
     1.3 @@ -127,9 +127,9 @@
     1.4    (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
     1.5    (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
     1.6      let val thy = ProofContext.theory_of ctxt in
     1.7 -      Code_Target.code_of thy
     1.8 -        target NONE "Example" (mk_cs thy)
     1.9 +      Code_Target.produce_code thy (mk_cs thy)
    1.10          (fn naming => maps (fn f => f thy naming) mk_stmtss)
    1.11 +        target NONE (SOME "Example") []
    1.12        |> fst
    1.13        |> typewriter
    1.14      end);
     2.1 --- a/src/Tools/Code/code_eval.ML	Mon Aug 30 18:32:40 2010 +0200
     2.2 +++ b/src/Tools/Code/code_eval.ML	Tue Aug 31 13:08:58 2010 +0200
     2.3 @@ -29,8 +29,8 @@
     2.4      val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
     2.5      val struct_name = if struct_name_hint = "" then eval_struct_name
     2.6        else struct_name_hint;
     2.7 -    val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
     2.8 -      struct_name naming program (consts' @ tycos');
     2.9 +    val (ml_code, target_names) = Code_Target.produce_code_for thy
    2.10 +      target NONE (SOME struct_name) [] naming program (consts' @ tycos', []);
    2.11      val (consts'', tycos'') = chop (length consts') target_names;
    2.12      val consts_map = map2 (fn const => fn NONE =>
    2.13          error ("Constant " ^ (quote o Code.string_of_const thy) const
    2.14 @@ -57,8 +57,8 @@
    2.15            |> Graph.new_node (value_name,
    2.16                Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
    2.17            |> fold (curry Graph.add_edge value_name) deps;
    2.18 -        val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
    2.19 -          (the_default target some_target) "" naming program' [value_name];
    2.20 +        val (value_code, [SOME value_name']) = Code_Target.produce_code_for thy
    2.21 +          (the_default target some_target) NONE (SOME "") [] naming program ([value_name], []);
    2.22          val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
    2.23            ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
    2.24        in ML_Context.evaluate ctxt false reff sml_code end;
     3.1 --- a/src/Tools/Code/code_ml.ML	Mon Aug 30 18:32:40 2010 +0200
     3.2 +++ b/src/Tools/Code/code_ml.ML	Tue Aug 31 13:08:58 2010 +0200
     3.3 @@ -8,8 +8,6 @@
     3.4  sig
     3.5    val target_SML: string
     3.6    val target_OCaml: string
     3.7 -  val evaluation_code_of: theory -> string -> string
     3.8 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
     3.9    val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
    3.10      -> Code_Printer.fixity -> 'a list -> Pretty.T option
    3.11    val setup: theory -> theory
    3.12 @@ -943,13 +941,6 @@
    3.13  end; (*local*)
    3.14  
    3.15  
    3.16 -(** for instrumentalization **)
    3.17 -
    3.18 -fun evaluation_code_of thy target struct_name =
    3.19 -  Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
    3.20 -    serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
    3.21 -
    3.22 -
    3.23  (** Isar setup **)
    3.24  
    3.25  fun isar_serializer_sml module_name =
     4.1 --- a/src/Tools/Code/code_target.ML	Mon Aug 30 18:32:40 2010 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 13:08:58 2010 +0200
     4.3 @@ -42,12 +42,6 @@
     4.4      -> 'a -> int -> serialization
     4.5    val set_default_code_width: int -> theory -> theory
     4.6  
     4.7 -  (*FIXME drop asap*)
     4.8 -  val code_of: theory -> string -> int option -> string
     4.9 -    -> string list -> (Code_Thingol.naming -> string list) -> string * string option list
    4.10 -  val serialize_custom: theory -> string * serializer -> string option
    4.11 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    4.12 -
    4.13    val allow_abort: string -> theory -> theory
    4.14    type tyco_syntax = Code_Printer.tyco_syntax
    4.15    type const_syntax = Code_Printer.const_syntax
    4.16 @@ -77,8 +71,8 @@
    4.17  fun stmt_names_of_destination (String stmt_names) = stmt_names
    4.18    | stmt_names_of_destination _ = [];
    4.19  
    4.20 -fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
    4.21 -  | serialization _ string pretty width (String _) = SOME (string width pretty);
    4.22 +fun serialization output _ content width (File some_path) = (output width some_path content; NONE)
    4.23 +  | serialization _ string content width (String _) = SOME (string width content);
    4.24  
    4.25  fun file some_path f = (f (File some_path); ());
    4.26  fun string stmt_names f = the (f (String stmt_names));
    4.27 @@ -291,7 +285,7 @@
    4.28        program4 (names1, presentation_names) width
    4.29    end;
    4.30  
    4.31 -fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
    4.32 +fun mount_serializer thy target some_width raw_module_name args naming program names destination =
    4.33    let
    4.34      val ((targets, abortable), default_width) = Targets.get thy;
    4.35      fun collapse_hierarchy target =
    4.36 @@ -306,8 +300,8 @@
    4.37            in (modify' #> modify naming, merge_target false target (data', data)) end
    4.38        end;
    4.39      val (modify, data) = collapse_hierarchy target;
    4.40 -    val serializer = the_default (case the_description data
    4.41 -     of Fundamental seri => #serializer seri) alt_serializer;
    4.42 +    val serializer = case the_description data
    4.43 +    of Fundamental seri => #serializer seri;
    4.44      val presentation_names = stmt_names_of_destination destination;
    4.45      val module_name = if null presentation_names
    4.46        then raw_module_name else SOME "Code";
    4.47 @@ -332,13 +326,11 @@
    4.48  
    4.49  in
    4.50  
    4.51 -fun serialize thy = mount_serializer thy NONE;
    4.52 -
    4.53  fun export_code_for thy some_path target some_width some_module_name args naming program names =
    4.54 -  file some_path (serialize thy target some_width some_module_name args naming program names);
    4.55 +  file some_path (mount_serializer thy target some_width some_module_name args naming program names);
    4.56  
    4.57  fun produce_code_for thy target some_width some_module_name args naming program (names, selects) =
    4.58 -  string selects (serialize thy target some_width some_module_name args naming program names);
    4.59 +  string selects (mount_serializer thy target some_width some_module_name args naming program names);
    4.60  
    4.61  fun check_code_for thy target strict args naming program names_cs =
    4.62    let
    4.63 @@ -349,7 +341,7 @@
    4.64      fun ext_check env_param p =
    4.65        let 
    4.66          val destination = make_destination p;
    4.67 -        val _ = file (SOME destination) (serialize thy target (SOME 80)
    4.68 +        val _ = file (SOME destination) (mount_serializer thy target (SOME 80)
    4.69            (SOME module_name) args naming program names_cs);
    4.70          val cmd = make_command env_param module_name;
    4.71        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    4.72 @@ -363,24 +355,9 @@
    4.73      else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
    4.74    end;
    4.75  
    4.76 -fun serialize_custom thy (target_name, seri) module_name naming program names =
    4.77 -  mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
    4.78 -  |> the;
    4.79 -
    4.80  end; (* local *)
    4.81  
    4.82  
    4.83 -(* code presentation *)
    4.84 -
    4.85 -fun code_of thy target some_width module_name cs names_stmt =
    4.86 -  let
    4.87 -    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
    4.88 -  in
    4.89 -    string (names_stmt naming)
    4.90 -      (serialize thy target some_width (SOME module_name) [] naming program names_cs)
    4.91 -  end;
    4.92 -
    4.93 -
    4.94  (* code generation *)
    4.95  
    4.96  fun transitivly_non_empty_funs thy naming program =