src/Tools/Code/code_target.ML
changeset 48568 084cd758a8ab
parent 48426 7b03314ee2ac
child 50768 2172f82de515
equal deleted inserted replaced
48566:6e5702395491 48568:084cd758a8ab
    11   val read_const_exprs: theory -> string list -> string list
    11   val read_const_exprs: theory -> string list -> string list
    12 
    12 
    13   val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
    13   val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
    14     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    14     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    15   val produce_code_for: theory -> string -> int option -> string -> Token.T list
    15   val produce_code_for: theory -> string -> int option -> string -> Token.T list
    16     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    16     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> (string * string) list * string option list
    17   val present_code_for: theory -> string -> int option -> string -> Token.T list
    17   val present_code_for: theory -> string -> int option -> string -> Token.T list
    18     -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
    18     -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
    19   val check_code_for: theory -> string -> bool -> Token.T list
    19   val check_code_for: theory -> string -> bool -> Token.T list
    20     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    20     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    21 
    21 
    22   val export_code: theory -> string list
    22   val export_code: theory -> string list
    23     -> (((string * string) * Path.T option) * Token.T list) list -> unit
    23     -> (((string * string) * Path.T option) * Token.T list) list -> unit
    24   val produce_code: theory -> string list
    24   val produce_code: theory -> string list
    25     -> string -> int option -> string -> Token.T list -> string * string option list
    25     -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
    26   val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
    26   val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
    27     -> string -> int option -> string -> Token.T list -> string
    27     -> string -> int option -> string -> Token.T list -> string
    28   val check_code: theory -> string list
    28   val check_code: theory -> string list
    29     -> ((string * bool) * Token.T list) list -> unit
    29     -> ((string * bool) * Token.T list) list -> unit
    30 
    30 
       
    31   val generatedN: string
    31   val evaluator: theory -> string -> Code_Thingol.naming -> Code_Thingol.program
    32   val evaluator: theory -> string -> Code_Thingol.naming -> Code_Thingol.program
    32     -> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
    33     -> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
    33     -> string * string
    34     -> (string * string) list * string
    34 
    35 
    35   type serializer
    36   type serializer
    36   type literals = Code_Printer.literals
    37   type literals = Code_Printer.literals
    37   val add_target: string * { serializer: serializer, literals: literals,
    38   val add_target: string * { serializer: serializer, literals: literals,
    38     check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }
    39     check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }
    43   val assert_target: theory -> string -> string
    44   val assert_target: theory -> string -> string
    44   val the_literals: theory -> string -> literals
    45   val the_literals: theory -> string -> literals
    45   type serialization
    46   type serialization
    46   val parse_args: 'a parser -> Token.T list -> 'a
    47   val parse_args: 'a parser -> Token.T list -> 'a
    47   val serialization: (int -> Path.T option -> 'a -> unit)
    48   val serialization: (int -> Path.T option -> 'a -> unit)
    48     -> (string list -> int -> 'a -> string * (string -> string option))
    49     -> (string list -> int -> 'a -> (string * string) list * (string -> string option))
    49     -> 'a -> serialization
    50     -> 'a -> serialization
    50   val set_default_code_width: int -> theory -> theory
    51   val set_default_code_width: int -> theory -> theory
    51 
    52 
    52   val allow_abort: string -> theory -> theory
    53   val allow_abort: string -> theory -> theory
    53   type tyco_syntax = Code_Printer.tyco_syntax
    54   type tyco_syntax = Code_Printer.tyco_syntax
    75 
    76 
    76 
    77 
    77 (** abstract nonsense **)
    78 (** abstract nonsense **)
    78 
    79 
    79 datatype destination = Export of Path.T option | Produce | Present of string list;
    80 datatype destination = Export of Path.T option | Produce | Present of string list;
    80 type serialization = int -> destination -> (string * (string -> string option)) option;
    81 type serialization = int -> destination -> ((string * string) list * (string -> string option)) option;
    81 
    82 
    82 fun serialization output _ content width (Export some_path) =
    83 fun serialization output _ content width (Export some_path) =
    83       (output width some_path content; NONE)
    84       (output width some_path content; NONE)
    84   | serialization _ string content width Produce =
    85   | serialization _ string content width Produce =
    85       string [] width content |> SOME
    86       string [] width content |> SOME
    86   | serialization _ string content width (Present stmt_names) =
    87   | serialization _ string content width (Present stmt_names) =
    87      string stmt_names width content
    88      string stmt_names width content
    88      |> apfst (Pretty.output (SOME width) o Pretty.str)
    89      |> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str)
    89      |> SOME;
    90      |> SOME;
    90 
    91 
    91 fun export some_path f = (f (Export some_path); ());
    92 fun export some_path f = (f (Export some_path); ());
    92 fun produce f = the (f Produce);
    93 fun produce f = the (f Produce);
    93 fun present stmt_names f = fst (the (f (Present stmt_names)));
    94 fun present stmt_names f = space_implode "\n\n" (map snd (fst (the (f (Present stmt_names)))));
    94 
    95 
    95 
    96 
    96 (** theory data **)
    97 (** theory data **)
    97 
    98 
    98 datatype symbol_syntax_data = Symbol_Syntax_Data of {
    99 datatype symbol_syntax_data = Symbol_Syntax_Data of {
   376 fun using_master_directory thy =
   377 fun using_master_directory thy =
   377   Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory thy));
   378   Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory thy));
   378 
   379 
   379 in
   380 in
   380 
   381 
       
   382 val generatedN = "Generated_Code";
       
   383 
   381 fun export_code_for thy some_path target some_width module_name args =
   384 fun export_code_for thy some_path target some_width module_name args =
   382   export (using_master_directory thy some_path)
   385   export (using_master_directory thy some_path)
   383   ooo invoke_serializer thy target some_width module_name args;
   386   ooo invoke_serializer thy target some_width module_name args;
   384 
   387 
   385 fun produce_code_for thy target some_width module_name args =
   388 fun produce_code_for thy target some_width module_name args =
   396     present selects (serializer naming program names)
   399     present selects (serializer naming program names)
   397   end;
   400   end;
   398 
   401 
   399 fun check_code_for thy target strict args naming program names_cs =
   402 fun check_code_for thy target strict args naming program names_cs =
   400   let
   403   let
   401     val module_name = "Generated_Code";
       
   402     val { env_var, make_destination, make_command } =
   404     val { env_var, make_destination, make_command } =
   403       (#check o the_fundamental thy) target;
   405       (#check o the_fundamental thy) target;
   404     fun ext_check p =
   406     fun ext_check p =
   405       let
   407       let
   406         val destination = make_destination p;
   408         val destination = make_destination p;
   407         val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
   409         val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
   408           module_name args naming program names_cs);
   410           generatedN args naming program names_cs);
   409         val cmd = make_command module_name;
   411         val cmd = make_command generatedN;
   410       in
   412       in
   411         if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
   413         if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
   412         then error ("Code check failed for " ^ target ^ ": " ^ cmd)
   414         then error ("Code check failed for " ^ target ^ ": " ^ cmd)
   413         else ()
   415         else ()
   414       end;
   416       end;
   437   in (program_code, value_name') end;
   439   in (program_code, value_name') end;
   438 
   440 
   439 fun evaluator thy target naming program consts =
   441 fun evaluator thy target naming program consts =
   440   let
   442   let
   441     val (mounted_serializer, prepared_program) = mount_serializer thy
   443     val (mounted_serializer, prepared_program) = mount_serializer thy
   442       target NONE "Generated_Code" [] naming program consts;
   444       target NONE generatedN [] naming program consts;
   443   in evaluation mounted_serializer prepared_program consts end;
   445   in evaluation mounted_serializer prepared_program consts end;
   444 
   446 
   445 end; (* local *)
   447 end; (* local *)
   446 
   448 
   447 
   449