src/Tools/Code/code_target.ML
changeset 38929 d9ac9dee764d
parent 38928 0e6f54c9d201
child 38933 bd77e092f67c
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 15:08:04 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 15:21:42 2010 +0200
     1.3 @@ -12,14 +12,18 @@
     1.4    val export_code_for: theory -> Path.T option -> string -> int option -> string option -> Token.T list
     1.5      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
     1.6    val produce_code_for: theory -> string -> int option -> string option -> Token.T list
     1.7 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string * string option list
     1.8 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
     1.9 +  val present_code_for: theory -> string -> int option -> string option -> Token.T list
    1.10 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
    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 +  val produce_code: theory -> string list
    1.18      -> string -> int option -> string option -> Token.T list -> string * string option list
    1.19 +  val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
    1.20 +    -> string -> int option -> string option -> Token.T list -> string
    1.21    val check_code: theory -> string list
    1.22      -> ((string * bool) * Token.T list) list -> unit
    1.23  
    1.24 @@ -65,17 +69,19 @@
    1.25  
    1.26  (** abstract nonsense **)
    1.27  
    1.28 -datatype destination = File of Path.T option | String of string list;
    1.29 +datatype destination = Export of Path.T option | Produce | Present of string list;
    1.30  type serialization = int -> destination -> (string * string option list) option;
    1.31  
    1.32 -fun stmt_names_of_destination (String stmt_names) = stmt_names
    1.33 +fun stmt_names_of_destination (Present stmt_names) = stmt_names
    1.34    | stmt_names_of_destination _ = [];
    1.35  
    1.36 -fun serialization output _ content width (File some_path) = (output width some_path content; NONE)
    1.37 -  | serialization _ string content width (String _) = SOME (string width content);
    1.38 +fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
    1.39 +  | serialization _ string content width Produce = SOME (string width content)
    1.40 +  | serialization _ string content width (Present _) = SOME (string width content);
    1.41  
    1.42 -fun file some_path f = (f (File some_path); ());
    1.43 -fun string stmt_names f = the (f (String stmt_names));
    1.44 +fun export some_path f = (f (Export some_path); ());
    1.45 +fun produce f = the (f Produce);
    1.46 +fun present stmt_names f = fst (the (f (Present stmt_names)));
    1.47  
    1.48  
    1.49  (** theory data **)
    1.50 @@ -353,10 +359,13 @@
    1.51  in
    1.52  
    1.53  fun export_code_for thy some_path target some_width some_module_name args naming program names =
    1.54 -  file some_path (mount_serializer thy target some_width some_module_name args naming program names);
    1.55 +  export some_path (mount_serializer thy target some_width some_module_name args naming program names);
    1.56  
    1.57 -fun produce_code_for thy target some_width some_module_name args naming program (names, selects) =
    1.58 -  string selects (mount_serializer thy target some_width some_module_name args naming program names);
    1.59 +fun produce_code_for thy target some_width some_module_name args naming program names =
    1.60 +  produce (mount_serializer thy target some_width some_module_name args naming program names);
    1.61 +
    1.62 +fun present_code_for thy target some_width some_module_name args naming program (names, selects) =
    1.63 +  present selects (mount_serializer thy target some_width some_module_name args naming program names);
    1.64  
    1.65  fun check_code_for thy target strict args naming program names_cs =
    1.66    let
    1.67 @@ -367,7 +376,7 @@
    1.68      fun ext_check env_param p =
    1.69        let 
    1.70          val destination = make_destination p;
    1.71 -        val _ = file (SOME destination) (mount_serializer thy target (SOME 80)
    1.72 +        val _ = export (SOME destination) (mount_serializer thy target (SOME 80)
    1.73            (SOME module_name) args naming program names_cs);
    1.74          val cmd = make_command env_param module_name;
    1.75        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    1.76 @@ -415,10 +424,15 @@
    1.77  fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
    1.78    ((map o apfst o apsnd) prep_destination seris);
    1.79  
    1.80 -fun produce_code thy cs names_stmt target some_width some_module_name args =
    1.81 +fun produce_code thy cs target some_width some_module_name args =
    1.82    let
    1.83      val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
    1.84 -  in produce_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end;
    1.85 +  in produce_code_for thy target some_width some_module_name args naming program names_cs end;
    1.86 +
    1.87 +fun present_code thy cs names_stmt target some_width some_module_name args =
    1.88 +  let
    1.89 +    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
    1.90 +  in present_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end;
    1.91  
    1.92  fun check_code thy cs seris =
    1.93    let