src/Tools/Code/code_target.ML
changeset 38925 ced825abdc1d
parent 38924 fcd1d0457e27
child 38926 24f82786cc57
equal deleted inserted replaced
38924:fcd1d0457e27 38925:ced825abdc1d
    37   val the_literals: theory -> string -> literals
    37   val the_literals: theory -> string -> literals
    38   type serialization
    38   type serialization
    39   val parse_args: 'a parser -> Token.T list -> 'a
    39   val parse_args: 'a parser -> Token.T list -> 'a
    40   val serialization: (int -> Path.T option -> 'a -> unit)
    40   val serialization: (int -> Path.T option -> 'a -> unit)
    41     -> (int -> 'a -> string * string option list)
    41     -> (int -> 'a -> string * string option list)
    42     -> 'a -> int -> serialization
    42     -> 'a -> serialization
    43   val set_default_code_width: int -> theory -> theory
    43   val set_default_code_width: int -> theory -> theory
    44 
    44 
    45   val allow_abort: string -> theory -> theory
    45   val allow_abort: string -> theory -> theory
    46   type tyco_syntax = Code_Printer.tyco_syntax
    46   type tyco_syntax = Code_Printer.tyco_syntax
    47   type const_syntax = Code_Printer.const_syntax
    47   type const_syntax = Code_Printer.const_syntax
    64 
    64 
    65 
    65 
    66 (** abstract nonsense **)
    66 (** abstract nonsense **)
    67 
    67 
    68 datatype destination = File of Path.T option | String of string list;
    68 datatype destination = File of Path.T option | String of string list;
    69 type serialization = destination -> (string * string option list) option;
    69 type serialization = int -> destination -> (string * string option list) option;
    70 
    70 
    71 fun stmt_names_of_destination (String stmt_names) = stmt_names
    71 fun stmt_names_of_destination (String stmt_names) = stmt_names
    72   | stmt_names_of_destination _ = [];
    72   | stmt_names_of_destination _ = [];
    73 
    73 
    74 fun serialization output _ content width (File some_path) = (output width some_path content; NONE)
    74 fun serialization output _ content width (File some_path) = (output width some_path content; NONE)
   110   -> (string -> string option)          (*class syntax*)
   110   -> (string -> string option)          (*class syntax*)
   111   -> (string -> Code_Printer.tyco_syntax option)
   111   -> (string -> Code_Printer.tyco_syntax option)
   112   -> (string -> Code_Printer.activated_const_syntax option)
   112   -> (string -> Code_Printer.activated_const_syntax option)
   113   -> Code_Thingol.program
   113   -> Code_Thingol.program
   114   -> (string list * string list)        (*selected statements*)
   114   -> (string list * string list)        (*selected statements*)
   115   -> int
       
   116   -> serialization;
   115   -> serialization;
   117 
   116 
   118 datatype description = Fundamental of { serializer: serializer,
   117 datatype description = Fundamental of { serializer: serializer,
   119       literals: literals,
   118       literals: literals,
   120       check: { env_var: string, make_destination: Path.T -> Path.T,
   119       check: { env_var: string, make_destination: Path.T -> Path.T,
   125 datatype target = Target of {
   124 datatype target = Target of {
   126   serial: serial,
   125   serial: serial,
   127   description: description,
   126   description: description,
   128   reserved: string list,
   127   reserved: string list,
   129   includes: (Pretty.T * string list) Symtab.table,
   128   includes: (Pretty.T * string list) Symtab.table,
   130   symbol_syntax_data: symbol_syntax_data,
   129   module_alias: string Symtab.table,
   131   module_alias: string Symtab.table
   130   symbol_syntax: symbol_syntax_data
   132 };
   131 };
   133 
   132 
   134 fun make_target ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias))) =
   133 fun make_target ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))) =
   135   Target { serial = serial, description = description, reserved = reserved, 
   134   Target { serial = serial, description = description, reserved = reserved, 
   136     includes = includes, symbol_syntax_data = symbol_syntax_data, module_alias = module_alias };
   135     includes = includes, module_alias = module_alias, symbol_syntax = symbol_syntax };
   137 fun map_target f ( Target { serial, description, reserved, includes, symbol_syntax_data, module_alias } ) =
   136 fun map_target f ( Target { serial, description, reserved, includes, module_alias, symbol_syntax } ) =
   138   make_target (f ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias))));
   137   make_target (f ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))));
   139 fun merge_target strict target (Target { serial = serial1, description = description,
   138 fun merge_target strict target (Target { serial = serial1, description = description,
   140   reserved = reserved1, includes = includes1,
   139   reserved = reserved1, includes = includes1,
   141   symbol_syntax_data = symbol_syntax_data1, module_alias = module_alias1 },
   140   module_alias = module_alias1, symbol_syntax = symbol_syntax1 },
   142     Target { serial = serial2, description = _,
   141     Target { serial = serial2, description = _,
   143       reserved = reserved2, includes = includes2,
   142       reserved = reserved2, includes = includes2,
   144       symbol_syntax_data = symbol_syntax_data2, module_alias = module_alias2 }) =
   143       module_alias = module_alias2, symbol_syntax = symbol_syntax2 }) =
   145   if serial1 = serial2 orelse not strict then
   144   if serial1 = serial2 orelse not strict then
   146     make_target ((serial1, description),
   145     make_target ((serial1, description),
   147       ((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
   146       ((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
   148         (merge_symbol_syntax_data (symbol_syntax_data1, symbol_syntax_data2),
   147         (Symtab.join (K snd) (module_alias1, module_alias2),
   149           Symtab.join (K snd) (module_alias1, module_alias2))
   148           merge_symbol_syntax_data (symbol_syntax1, symbol_syntax2))
   150     ))
   149     ))
   151   else
   150   else
   152     error ("Incompatible targets: " ^ quote target);
   151     error ("Incompatible targets: " ^ quote target);
   153 
   152 
   154 fun the_description (Target { description, ... }) = description;
   153 fun the_description (Target { description, ... }) = description;
   155 fun the_reserved (Target { reserved, ... }) = reserved;
   154 fun the_reserved (Target { reserved, ... }) = reserved;
   156 fun the_includes (Target { includes, ... }) = includes;
   155 fun the_includes (Target { includes, ... }) = includes;
   157 fun the_symbol_syntax_data (Target { symbol_syntax_data = Symbol_Syntax_Data x, ... }) = x;
       
   158 fun the_module_alias (Target { module_alias , ... }) = module_alias;
   156 fun the_module_alias (Target { module_alias , ... }) = module_alias;
       
   157 fun the_symbol_syntax (Target { symbol_syntax = Symbol_Syntax_Data x, ... }) = x;
   159 
   158 
   160 structure Targets = Theory_Data
   159 structure Targets = Theory_Data
   161 (
   160 (
   162   type T = (target Symtab.table * string list) * int;
   161   type T = (target Symtab.table * string list) * int;
   163   val empty = ((Symtab.empty, []), 80);
   162   val empty = ((Symtab.empty, []), 80);
   191       else (); 
   190       else (); 
   192   in
   191   in
   193     thy
   192     thy
   194     |> (Targets.map o apfst o apfst o Symtab.update)
   193     |> (Targets.map o apfst o apfst o Symtab.update)
   195           (target, make_target ((serial (), seri), (([], Symtab.empty),
   194           (target, make_target ((serial (), seri), (([], Symtab.empty),
   196             (make_symbol_syntax_data ((Symtab.empty, Symreltab.empty),
   195             (Symtab.empty, make_symbol_syntax_data ((Symtab.empty, Symreltab.empty),
   197               (Symtab.empty, Symtab.empty)), Symtab.empty))))
   196               (Symtab.empty, Symtab.empty))))))
   198   end;
   197   end;
   199 
   198 
   200 fun add_target (target, seri) = put_target (target, Fundamental seri);
   199 fun add_target (target, seri) = put_target (target, Fundamental seri);
   201 fun extend_target (target, (super, modify)) =
   200 fun extend_target (target, (super, modify)) =
   202   put_target (target, Extension (super, modify));
   201   put_target (target, Extension (super, modify));
   211 
   210 
   212 fun map_reserved target =
   211 fun map_reserved target =
   213   map_target_data target o apsnd o apfst o apfst;
   212   map_target_data target o apsnd o apfst o apfst;
   214 fun map_includes target =
   213 fun map_includes target =
   215   map_target_data target o apsnd o apfst o apsnd;
   214   map_target_data target o apsnd o apfst o apsnd;
   216 fun map_name_syntax target =
       
   217   map_target_data target o apsnd o apsnd o apfst o map_symbol_syntax_data;
       
   218 fun map_module_alias target =
   215 fun map_module_alias target =
   219   map_target_data target o apsnd o apsnd o apsnd;
   216   map_target_data target o apsnd o apsnd o apfst;
       
   217 fun map_symbol_syntax target =
       
   218   map_target_data target o apsnd o apsnd o apsnd o map_symbol_syntax_data;
   220 
   219 
   221 fun set_default_code_width k = (Targets.map o apsnd) (K k);
   220 fun set_default_code_width k = (Targets.map o apsnd) (K k);
   222 
   221 
   223 
   222 
   224 (** serializer usage **)
   223 (** serializer usage **)
   312         | NONE => false) cs
   311         | NONE => false) cs
   313       then SOME (name, content) else NONE;
   312       then SOME (name, content) else NONE;
   314     fun includes names_all = map_filter (select_include names_all)
   313     fun includes names_all = map_filter (select_include names_all)
   315       ((Symtab.dest o the_includes) data);
   314       ((Symtab.dest o the_includes) data);
   316     val module_alias = the_module_alias data 
   315     val module_alias = the_module_alias data 
   317     val { class, instance, tyco, const } = the_symbol_syntax_data data;
   316     val { class, instance, tyco, const } = the_symbol_syntax data;
   318     val literals = the_literals thy target;
   317     val literals = the_literals thy target;
   319     val width = the_default default_width some_width;
   318     val width = the_default default_width some_width;
   320   in
   319   in
   321     invoke_serializer thy abortable serializer literals reserved
   320     invoke_serializer thy abortable serializer literals reserved
   322       includes module_alias class instance tyco const module_name args
   321       includes module_alias class instance tyco const module_name args
   432   let
   431   let
   433     val x = prep_x thy raw_x;
   432     val x = prep_x thy raw_x;
   434     val change = case some_raw_syn
   433     val change = case some_raw_syn
   435      of SOME raw_syn => upd (x, prep_syn thy x raw_syn)
   434      of SOME raw_syn => upd (x, prep_syn thy x raw_syn)
   436       | NONE => del x;
   435       | NONE => del x;
   437   in (map_name_syntax target o mapp) change thy end;
   436   in (map_symbol_syntax target o mapp) change thy end;
   438 
   437 
   439 fun gen_add_class_syntax prep_class =
   438 fun gen_add_class_syntax prep_class =
   440   gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class ((K o K) I);
   439   gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class ((K o K) I);
   441 
   440 
   442 fun gen_add_instance_syntax prep_inst =
   441 fun gen_add_instance_syntax prep_inst =