src/Tools/Code/code_target.ML
changeset 37822 cf3588177676
parent 37821 3cbb22cec751
child 37824 365e37fe93f3
equal deleted inserted replaced
37821:3cbb22cec751 37822:cf3588177676
     9   val cert_tyco: theory -> string -> string
     9   val cert_tyco: theory -> string -> string
    10   val read_tyco: theory -> string -> string
    10   val read_tyco: theory -> string -> string
    11 
    11 
    12   type serializer
    12   type serializer
    13   type literals = Code_Printer.literals
    13   type literals = Code_Printer.literals
    14   val add_target: string * { serializer: serializer, literals: literals, check: unit }
    14   val add_target: string * { serializer: serializer, literals: literals,
    15     -> theory -> theory
    15     check: { env_var: string, make_destination: Path.T -> Path.T,
       
    16       make_command: string -> Path.T -> string -> string } } -> theory -> theory
    16   val extend_target: string *
    17   val extend_target: string *
    17       (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    18       (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    18     -> theory -> theory
    19     -> theory -> theory
    19   val assert_target: theory -> string -> string
    20   val assert_target: theory -> string -> string
    20 
    21 
    33   val export: serialization -> unit
    34   val export: serialization -> unit
    34   val file: Path.T -> serialization -> unit
    35   val file: Path.T -> serialization -> unit
    35   val string: string list -> serialization -> string
    36   val string: string list -> serialization -> string
    36   val code_of: theory -> string -> int option -> string
    37   val code_of: theory -> string -> int option -> string
    37     -> string list -> (Code_Thingol.naming -> string list) -> string
    38     -> string list -> (Code_Thingol.naming -> string list) -> string
    38   val external_check: theory -> string -> string
    39   val check: theory -> string -> unit
    39     -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> unit
       
    40   val set_default_code_width: int -> theory -> theory
    40   val set_default_code_width: int -> theory -> theory
    41   val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    41   val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    42 
    42 
    43   val allow_abort: string -> theory -> theory
    43   val allow_abort: string -> theory -> theory
    44   type tyco_syntax = Code_Printer.tyco_syntax
    44   type tyco_syntax = Code_Printer.tyco_syntax
   113   -> ((Pretty.T -> string) * (Pretty.T -> unit))
   113   -> ((Pretty.T -> string) * (Pretty.T -> unit))
   114   -> Code_Thingol.program
   114   -> Code_Thingol.program
   115   -> string list                        (*selected statements*)
   115   -> string list                        (*selected statements*)
   116   -> serialization;
   116   -> serialization;
   117 
   117 
   118 datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, check: unit }
   118 datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
       
   119       check: { env_var: string, make_destination: Path.T -> Path.T,
       
   120         make_command: string -> Path.T -> string -> string } }
   119   | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
   121   | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
   120 
   122 
   121 datatype target = Target of {
   123 datatype target = Target of {
   122   serial: serial,
   124   serial: serial,
   123   description: description,
   125   description: description,
   219 
   221 
   220 (** serializer usage **)
   222 (** serializer usage **)
   221 
   223 
   222 (* montage *)
   224 (* montage *)
   223 
   225 
   224 fun the_literals thy =
   226 fun the_fundamental thy =
   225   let
   227   let
   226     val ((targets, _), _) = Targets.get thy;
   228     val ((targets, _), _) = Targets.get thy;
   227     fun literals target = case Symtab.lookup targets target
   229     fun fundamental target = case Symtab.lookup targets target
   228      of SOME data => (case the_description data
   230      of SOME data => (case the_description data
   229          of Fundamental { literals, ... } => literals
   231          of Fundamental data => data
   230           | Extension (super, _) => literals super)
   232           | Extension (super, _) => fundamental super)
   231       | NONE => error ("Unknown code target language: " ^ quote target);
   233       | NONE => error ("Unknown code target language: " ^ quote target);
   232   in literals end;
   234   in fundamental end;
       
   235 
       
   236 fun the_literals thy = #literals o the_fundamental thy;
   233 
   237 
   234 local
   238 local
   235 
   239 
   236 fun activate_syntax lookup_name src_tab = Symtab.empty
   240 fun activate_syntax lookup_name src_tab = Symtab.empty
   237   |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
   241   |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
   351     val names3 = transitivly_non_empty_funs thy naming program;
   355     val names3 = transitivly_non_empty_funs thy naming program;
   352     val cs3 = map_filter (fn (c, name) =>
   356     val cs3 = map_filter (fn (c, name) =>
   353       if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
   357       if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
   354   in union (op =) cs3 cs1 end;
   358   in union (op =) cs3 cs1 end;
   355 
   359 
   356 fun external_check thy target env_var make_destination make_command =
   360 fun check thy target =
   357   let
   361   let
       
   362     val { env_var, make_destination, make_command } =
       
   363       (#check o the_fundamental thy) target;
   358     val env_param = getenv env_var;
   364     val env_param = getenv env_var;
   359     fun ext_check env_param p =
   365     fun ext_check env_param p =
   360       let 
   366       let 
   361         val module_name = "Code_Test";
   367         val module_name = "Code_Test";
   362         val (cs, (naming, program)) =
   368         val (cs, (naming, program)) =
   372   in if env_param = ""
   378   in if env_param = ""
   373     then warning (env_var ^ " not set; skipped code check for " ^ target)
   379     then warning (env_var ^ " not set; skipped code check for " ^ target)
   374     else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
   380     else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
   375   end;
   381   end;
   376 
   382 
       
   383 
   377 fun export_code thy cs seris =
   384 fun export_code thy cs seris =
   378   let
   385   let
   379     val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
   386     val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
   380     fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export
   387     fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export
   381       else file (Path.explode dest);
   388       else file (Path.explode dest);