src/Tools/Code/code_target.ML
changeset 38923 79d7f2b4cf71
parent 38921 15f8cffdbf5d
child 38924 fcd1d0457e27
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 13:15:35 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 13:29:38 2010 +0200
     1.3 @@ -45,10 +45,10 @@
     1.4    val allow_abort: string -> theory -> theory
     1.5    type tyco_syntax = Code_Printer.tyco_syntax
     1.6    type const_syntax = Code_Printer.const_syntax
     1.7 -  val add_syntax_class: string -> class -> string option -> theory -> theory
     1.8 -  val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
     1.9 -  val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
    1.10 -  val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
    1.11 +  val add_class_syntax: string -> class -> string option -> theory -> theory
    1.12 +  val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
    1.13 +  val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
    1.14 +  val add_const_syntax: string -> string -> const_syntax option -> theory -> theory
    1.15    val add_reserved: string -> string -> theory -> theory
    1.16    val add_include: string -> string * (string * string list) option -> theory -> theory
    1.17  end;
    1.18 @@ -63,7 +63,7 @@
    1.19  type const_syntax = Code_Printer.const_syntax;
    1.20  
    1.21  
    1.22 -(** basics **)
    1.23 +(** abstract nonsense **)
    1.24  
    1.25  datatype destination = File of Path.T option | String of string list;
    1.26  type serialization = destination -> (string * string option list) option;
    1.27 @@ -80,21 +80,21 @@
    1.28  
    1.29  (** theory data **)
    1.30  
    1.31 -datatype name_syntax_table = NameSyntaxTable of {
    1.32 +datatype symbol_syntax_data = Symbol_Syntax_Data of {
    1.33    class: string Symtab.table,
    1.34    instance: unit Symreltab.table,
    1.35    tyco: Code_Printer.tyco_syntax Symtab.table,
    1.36    const: Code_Printer.const_syntax Symtab.table
    1.37  };
    1.38  
    1.39 -fun mk_name_syntax_table ((class, instance), (tyco, const)) =
    1.40 -  NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const };
    1.41 -fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) =
    1.42 -  mk_name_syntax_table (f ((class, instance), (tyco, const)));
    1.43 -fun merge_name_syntax_table
    1.44 -  (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
    1.45 -    NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
    1.46 -  mk_name_syntax_table (
    1.47 +fun make_symbol_syntax_data ((class, instance), (tyco, const)) =
    1.48 +  Symbol_Syntax_Data { class = class, instance = instance, tyco = tyco, const = const };
    1.49 +fun map_symbol_syntax_data f (Symbol_Syntax_Data { class, instance, tyco, const }) =
    1.50 +  make_symbol_syntax_data (f ((class, instance), (tyco, const)));
    1.51 +fun merge_symbol_syntax_data
    1.52 +  (Symbol_Syntax_Data { class = class1, instance = instance1, tyco = tyco1, const = const1 },
    1.53 +    Symbol_Syntax_Data { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
    1.54 +  make_symbol_syntax_data (
    1.55      (Symtab.join (K snd) (class1, class2),
    1.56         Symreltab.join (K snd) (instance1, instance2)),
    1.57      (Symtab.join (K snd) (tyco1, tyco2),
    1.58 @@ -128,25 +128,25 @@
    1.59    description: description,
    1.60    reserved: string list,
    1.61    includes: (Pretty.T * string list) Symtab.table,
    1.62 -  name_syntax_table: name_syntax_table,
    1.63 +  symbol_syntax_data: symbol_syntax_data,
    1.64    module_alias: string Symtab.table
    1.65  };
    1.66  
    1.67 -fun make_target ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))) =
    1.68 +fun make_target ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias))) =
    1.69    Target { serial = serial, description = description, reserved = reserved, 
    1.70 -    includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
    1.71 -fun map_target f ( Target { serial, description, reserved, includes, name_syntax_table, module_alias } ) =
    1.72 -  make_target (f ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))));
    1.73 +    includes = includes, symbol_syntax_data = symbol_syntax_data, module_alias = module_alias };
    1.74 +fun map_target f ( Target { serial, description, reserved, includes, symbol_syntax_data, module_alias } ) =
    1.75 +  make_target (f ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias))));
    1.76  fun merge_target strict target (Target { serial = serial1, description = description,
    1.77    reserved = reserved1, includes = includes1,
    1.78 -  name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
    1.79 +  symbol_syntax_data = symbol_syntax_data1, module_alias = module_alias1 },
    1.80      Target { serial = serial2, description = _,
    1.81        reserved = reserved2, includes = includes2,
    1.82 -      name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
    1.83 +      symbol_syntax_data = symbol_syntax_data2, module_alias = module_alias2 }) =
    1.84    if serial1 = serial2 orelse not strict then
    1.85      make_target ((serial1, description),
    1.86        ((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
    1.87 -        (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
    1.88 +        (merge_symbol_syntax_data (symbol_syntax_data1, symbol_syntax_data2),
    1.89            Symtab.join (K snd) (module_alias1, module_alias2))
    1.90      ))
    1.91    else
    1.92 @@ -155,7 +155,7 @@
    1.93  fun the_description (Target { description, ... }) = description;
    1.94  fun the_reserved (Target { reserved, ... }) = reserved;
    1.95  fun the_includes (Target { includes, ... }) = includes;
    1.96 -fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
    1.97 +fun the_symbol_syntax_data (Target { symbol_syntax_data = Symbol_Syntax_Data x, ... }) = x;
    1.98  fun the_module_alias (Target { module_alias , ... }) = module_alias;
    1.99  
   1.100  structure Targets = Theory_Data
   1.101 @@ -194,7 +194,7 @@
   1.102      thy
   1.103      |> (Targets.map o apfst o apfst o Symtab.update)
   1.104            (target, make_target ((serial (), seri), (([], Symtab.empty),
   1.105 -            (mk_name_syntax_table ((Symtab.empty, Symreltab.empty),
   1.106 +            (make_symbol_syntax_data ((Symtab.empty, Symreltab.empty),
   1.107                (Symtab.empty, Symtab.empty)), Symtab.empty))))
   1.108    end;
   1.109  
   1.110 @@ -215,7 +215,7 @@
   1.111  fun map_includes target =
   1.112    map_target_data target o apsnd o apfst o apsnd;
   1.113  fun map_name_syntax target =
   1.114 -  map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
   1.115 +  map_target_data target o apsnd o apsnd o apfst o map_symbol_syntax_data;
   1.116  fun map_module_alias target =
   1.117    map_target_data target o apsnd o apsnd o apsnd;
   1.118  
   1.119 @@ -315,7 +315,7 @@
   1.120      fun includes names_all = map_filter (select_include names_all)
   1.121        ((Symtab.dest o the_includes) data);
   1.122      val module_alias = the_module_alias data 
   1.123 -    val { class, instance, tyco, const } = the_name_syntax data;
   1.124 +    val { class, instance, tyco, const } = the_symbol_syntax_data data;
   1.125      val literals = the_literals thy target;
   1.126      val width = the_default default_width some_width;
   1.127    in
   1.128 @@ -437,19 +437,19 @@
   1.129        | NONE => del x;
   1.130    in (map_name_syntax target o mapp) change thy end;
   1.131  
   1.132 -fun gen_add_syntax_class prep_class =
   1.133 +fun gen_add_class_syntax prep_class =
   1.134    gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class ((K o K) I);
   1.135  
   1.136 -fun gen_add_syntax_inst prep_inst =
   1.137 +fun gen_add_instance_syntax prep_inst =
   1.138    gen_add_syntax (apfst o apsnd, Symreltab.update, Symreltab.delete_safe) prep_inst ((K o K) I);
   1.139  
   1.140 -fun gen_add_syntax_tyco prep_tyco =
   1.141 +fun gen_add_tyco_syntax prep_tyco =
   1.142    gen_add_syntax (apsnd o apfst, Symtab.update, Symtab.delete_safe) prep_tyco
   1.143      (fn thy => fn tyco => fn syn => if fst syn <> Sign.arity_number thy tyco
   1.144        then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
   1.145        else syn);
   1.146  
   1.147 -fun gen_add_syntax_const prep_const =
   1.148 +fun gen_add_const_syntax prep_const =
   1.149    gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
   1.150      (fn thy => fn c => fn syn =>
   1.151        if Code_Printer.requires_args syn > Code.args_number thy c
   1.152 @@ -513,18 +513,18 @@
   1.153  
   1.154  in
   1.155  
   1.156 -val add_syntax_class = gen_add_syntax_class cert_class;
   1.157 -val add_syntax_inst = gen_add_syntax_inst cert_inst;
   1.158 -val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
   1.159 -val add_syntax_const = gen_add_syntax_const (K I);
   1.160 +val add_class_syntax = gen_add_class_syntax cert_class;
   1.161 +val add_instance_syntax = gen_add_instance_syntax cert_inst;
   1.162 +val add_tyco_syntax = gen_add_tyco_syntax cert_tyco;
   1.163 +val add_const_syntax = gen_add_const_syntax (K I);
   1.164  val allow_abort = gen_allow_abort (K I);
   1.165  val add_reserved = add_reserved;
   1.166  val add_include = add_include;
   1.167  
   1.168 -val add_syntax_class_cmd = gen_add_syntax_class read_class;
   1.169 -val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
   1.170 -val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
   1.171 -val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
   1.172 +val add_class_syntax_cmd = gen_add_class_syntax read_class;
   1.173 +val add_instance_syntax_cmd = gen_add_instance_syntax read_inst;
   1.174 +val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
   1.175 +val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
   1.176  val allow_abort_cmd = gen_allow_abort Code.read_const;
   1.177  
   1.178  fun parse_args f args =
   1.179 @@ -554,23 +554,23 @@
   1.180  val _ =
   1.181    Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
   1.182      process_multi_syntax Parse.xname (Scan.option Parse.string)
   1.183 -    add_syntax_class_cmd);
   1.184 +    add_class_syntax_cmd);
   1.185  
   1.186  val _ =
   1.187    Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
   1.188      process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
   1.189        (Scan.option (Parse.minus >> K ()))
   1.190 -    add_syntax_inst_cmd);
   1.191 +    add_instance_syntax_cmd);
   1.192  
   1.193  val _ =
   1.194    Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
   1.195      process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
   1.196 -    add_syntax_tyco_cmd);
   1.197 +    add_tyco_syntax_cmd);
   1.198  
   1.199  val _ =
   1.200    Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
   1.201      process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
   1.202 -    add_syntax_const_cmd);
   1.203 +    add_const_syntax_cmd);
   1.204  
   1.205  val _ =
   1.206    Outer_Syntax.command "code_reserved" "declare words as reserved for target language"