tuned
authorhaftmann
Mon Aug 30 17:20:33 2010 +0200 (2010-08-30)
changeset 3891848d62f237944
parent 38917 c7da3cc88135
child 38919 fd6b9bdb428e
tuned
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Mon Aug 30 16:42:54 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Aug 30 17:20:33 2010 +0200
     1.3 @@ -9,6 +9,22 @@
     1.4    val cert_tyco: theory -> string -> string
     1.5    val read_tyco: theory -> string -> string
     1.6  
     1.7 +  val export_code_for: theory -> Path.T option -> string -> int option -> string option -> Token.T list
     1.8 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
     1.9 +  val produce_code_for: theory -> string -> int option -> string option -> Token.T list
    1.10 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string * string option list
    1.11 +  val check_code_for: theory -> string -> bool -> Token.T list
    1.12 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    1.13 +
    1.14 +  val export_code: theory -> string list
    1.15 +    -> (((string * string option) * Path.T option) * Token.T list) list -> unit
    1.16 +  val produce_code: theory -> string list -> (Code_Thingol.naming -> string list)
    1.17 +    -> string -> int option -> string option -> Token.T list -> string * string option list
    1.18 +  val check_code: theory -> string list
    1.19 +    -> ((string * bool) * Token.T list) list -> unit
    1.20 +
    1.21 +  val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    1.22 +
    1.23    type serializer
    1.24    type literals = Code_Printer.literals
    1.25    val add_target: string * { serializer: serializer, literals: literals,
    1.26 @@ -18,25 +34,19 @@
    1.27        (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    1.28      -> theory -> theory
    1.29    val assert_target: theory -> string -> string
    1.30 -
    1.31 -  type destination
    1.32 +  val the_literals: theory -> string -> literals
    1.33    type serialization
    1.34    val parse_args: 'a parser -> Token.T list -> 'a
    1.35    val serialization: (int -> Path.T option -> 'a -> unit)
    1.36      -> (int -> 'a -> string * string option list)
    1.37      -> 'a -> int -> serialization
    1.38 +  val set_default_code_width: int -> theory -> theory
    1.39  
    1.40 -  val serialize: theory -> string -> int option -> string option -> Token.T list
    1.41 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    1.42 +  (*FIXME drop asap*)
    1.43 +  val code_of: theory -> string -> int option -> string
    1.44 +    -> string list -> (Code_Thingol.naming -> string list) -> string * string option list
    1.45    val serialize_custom: theory -> string * serializer -> string option
    1.46      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    1.47 -  val check: theory -> string list
    1.48 -    -> Code_Thingol.naming -> Code_Thingol.program -> string -> bool -> Token.T list -> unit
    1.49 -  val code_of: theory -> string -> int option -> string
    1.50 -    -> string list -> (Code_Thingol.naming -> string list) -> string * string option list
    1.51 -  val set_default_code_width: int -> theory -> theory
    1.52 -  val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    1.53 -  val the_literals: theory -> string -> literals
    1.54  
    1.55    val allow_abort: string -> theory -> theory
    1.56    type tyco_syntax = Code_Printer.tyco_syntax
    1.57 @@ -70,7 +80,7 @@
    1.58  fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
    1.59    | serialization _ string pretty width (String _) = SOME (string width pretty);
    1.60  
    1.61 -fun file some_path f = f (File some_path);
    1.62 +fun file some_path f = (f (File some_path); ());
    1.63  fun string stmt_names f = the (f (String stmt_names));
    1.64  
    1.65  
    1.66 @@ -324,7 +334,13 @@
    1.67  
    1.68  fun serialize thy = mount_serializer thy NONE;
    1.69  
    1.70 -fun check thy names_cs naming program target strict args =
    1.71 +fun export_code_for thy some_path target some_width some_module_name args naming program names =
    1.72 +  file some_path (serialize thy target some_width some_module_name args naming program names);
    1.73 +
    1.74 +fun produce_code_for thy target some_width some_module_name args naming program (names, selects) =
    1.75 +  string selects (serialize thy target some_width some_module_name args naming program names);
    1.76 +
    1.77 +fun check_code_for thy target strict args naming program names_cs =
    1.78    let
    1.79      val module_name = "Code_Test";
    1.80      val { env_var, make_destination, make_command } =
    1.81 @@ -382,22 +398,30 @@
    1.82        if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
    1.83    in union (op =) cs3 cs1 end;
    1.84  
    1.85 +fun prep_destination "" = NONE
    1.86 +  | prep_destination "-" = NONE
    1.87 +  | prep_destination s = SOME (Path.explode s);
    1.88 +
    1.89  fun export_code thy cs seris =
    1.90    let
    1.91      val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
    1.92 -    fun mk_destination dest = if dest = "" orelse dest = "-"
    1.93 -      then NONE else SOME (Path.explode dest);
    1.94 -    val _ = map (fn (((target, module), dest), args) =>
    1.95 -      (file (mk_destination dest) (serialize thy target NONE module args naming program names_cs))) seris;
    1.96 +    val _ = map (fn (((target, module_name), some_path), args) =>
    1.97 +      export_code_for thy some_path target NONE module_name args naming program names_cs) seris;
    1.98    in () end;
    1.99  
   1.100 -fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
   1.101 +fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
   1.102 +  ((map o apfst o apsnd) prep_destination seris);
   1.103 +
   1.104 +fun produce_code thy cs names_stmt target some_width some_module_name args =
   1.105 +  let
   1.106 +    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
   1.107 +  in produce_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end;
   1.108  
   1.109  fun check_code thy cs seris =
   1.110    let
   1.111      val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
   1.112 -    val _ = map (fn ((target, strict), args) => check thy names_cs naming program
   1.113 -      target strict args) seris;
   1.114 +    val _ = map (fn ((target, strict), args) =>
   1.115 +      check_code_for thy target strict args naming program names_cs) seris;
   1.116    in () end;
   1.117  
   1.118  fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;