src/Tools/Code/code_target.ML
changeset 37821 3cbb22cec751
parent 37819 000049335247
child 37822 cf3588177676
     1.1 --- a/src/Tools/Code/code_target.ML	Wed Jul 14 14:53:44 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Wed Jul 14 14:53:44 2010 +0200
     1.3 @@ -11,7 +11,8 @@
     1.4  
     1.5    type serializer
     1.6    type literals = Code_Printer.literals
     1.7 -  val add_target: string * (serializer * literals) -> theory -> theory
     1.8 +  val add_target: string * { serializer: serializer, literals: literals, check: unit }
     1.9 +    -> theory -> theory
    1.10    val extend_target: string *
    1.11        (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    1.12      -> theory -> theory
    1.13 @@ -26,7 +27,7 @@
    1.14      -> 'a -> serialization
    1.15    val serialize: theory -> string -> int option -> string option -> Token.T list
    1.16      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    1.17 -  val serialize_custom: theory -> string * (serializer * literals)
    1.18 +  val serialize_custom: theory -> string * serializer
    1.19      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    1.20    val the_literals: theory -> string -> literals
    1.21    val export: serialization -> unit
    1.22 @@ -114,39 +115,39 @@
    1.23    -> string list                        (*selected statements*)
    1.24    -> serialization;
    1.25  
    1.26 -datatype serializer_entry = Serializer of serializer * Code_Printer.literals
    1.27 -  | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    1.28 +datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, check: unit }
    1.29 +  | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    1.30  
    1.31  datatype target = Target of {
    1.32    serial: serial,
    1.33 -  serializer: serializer_entry,
    1.34 +  description: description,
    1.35    reserved: string list,
    1.36    includes: (Pretty.T * string list) Symtab.table,
    1.37    name_syntax_table: name_syntax_table,
    1.38    module_alias: string Symtab.table
    1.39  };
    1.40  
    1.41 -fun make_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
    1.42 -  Target { serial = serial, serializer = serializer, reserved = reserved, 
    1.43 +fun make_target ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))) =
    1.44 +  Target { serial = serial, description = description, reserved = reserved, 
    1.45      includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
    1.46 -fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
    1.47 -  make_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
    1.48 -fun merge_target strict target (Target { serial = serial1, serializer = serializer,
    1.49 +fun map_target f ( Target { serial, description, reserved, includes, name_syntax_table, module_alias } ) =
    1.50 +  make_target (f ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))));
    1.51 +fun merge_target strict target (Target { serial = serial1, description = description,
    1.52    reserved = reserved1, includes = includes1,
    1.53    name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
    1.54 -    Target { serial = serial2, serializer = _,
    1.55 +    Target { serial = serial2, description = _,
    1.56        reserved = reserved2, includes = includes2,
    1.57        name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
    1.58    if serial1 = serial2 orelse not strict then
    1.59 -    make_target ((serial1, serializer),
    1.60 +    make_target ((serial1, description),
    1.61        ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)),
    1.62          (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
    1.63            Symtab.join (K fst) (module_alias1, module_alias2))
    1.64      ))
    1.65    else
    1.66 -    error ("Incompatible serializers: " ^ quote target);
    1.67 +    error ("Incompatible targets: " ^ quote target);
    1.68  
    1.69 -fun the_serializer (Target { serializer, ... }) = serializer;
    1.70 +fun the_description (Target { description, ... }) = description;
    1.71  fun the_reserved (Target { reserved, ... }) = reserved;
    1.72  fun the_includes (Target { includes, ... }) = includes;
    1.73  fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
    1.74 @@ -172,14 +173,14 @@
    1.75    let
    1.76      val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
    1.77      val _ = case seri
    1.78 -     of Extends (super, _) => if is_some (lookup_target super) then ()
    1.79 +     of Extension (super, _) => if is_some (lookup_target super) then ()
    1.80            else error ("Unknown code target language: " ^ quote super)
    1.81        | _ => ();
    1.82 -    val overwriting = case (Option.map the_serializer o lookup_target) target
    1.83 +    val overwriting = case (Option.map the_description o lookup_target) target
    1.84       of NONE => false
    1.85 -      | SOME (Extends _) => true
    1.86 -      | SOME (Serializer _) => (case seri
    1.87 -         of Extends _ => error ("Will not overwrite existing target " ^ quote target)
    1.88 +      | SOME (Extension _) => true
    1.89 +      | SOME (Fundamental _) => (case seri
    1.90 +         of Extension _ => error ("Will not overwrite existing target " ^ quote target)
    1.91            | _ => true);
    1.92      val _ = if overwriting
    1.93        then warning ("Overwriting existing target " ^ quote target)
    1.94 @@ -192,9 +193,9 @@
    1.95                Symtab.empty))))
    1.96    end;
    1.97  
    1.98 -fun add_target (target, seri) = put_target (target, Serializer seri);
    1.99 +fun add_target (target, seri) = put_target (target, Fundamental seri);
   1.100  fun extend_target (target, (super, modify)) =
   1.101 -  put_target (target, Extends (super, modify));
   1.102 +  put_target (target, Extension (super, modify));
   1.103  
   1.104  fun map_target_data target f thy =
   1.105    let
   1.106 @@ -224,9 +225,9 @@
   1.107    let
   1.108      val ((targets, _), _) = Targets.get thy;
   1.109      fun literals target = case Symtab.lookup targets target
   1.110 -     of SOME data => (case the_serializer data
   1.111 -         of Serializer (_, literals) => literals
   1.112 -          | Extends (super, _) => literals super)
   1.113 +     of SOME data => (case the_description data
   1.114 +         of Fundamental { literals, ... } => literals
   1.115 +          | Extension (super, _) => literals super)
   1.116        | NONE => error ("Unknown code target language: " ^ quote target);
   1.117    in literals end;
   1.118  
   1.119 @@ -286,15 +287,15 @@
   1.120          val data = case Symtab.lookup targets target
   1.121           of SOME data => data
   1.122            | NONE => error ("Unknown code target language: " ^ quote target);
   1.123 -      in case the_serializer data
   1.124 -       of Serializer _ => (I, data)
   1.125 -        | Extends (super, modify) => let
   1.126 +      in case the_description data
   1.127 +       of Fundamental _ => (I, data)
   1.128 +        | Extension (super, modify) => let
   1.129              val (modify', data') = collapse_hierarchy super
   1.130            in (modify' #> modify naming, merge_target false target (data', data)) end
   1.131        end;
   1.132      val (modify, data) = collapse_hierarchy target;
   1.133 -    val (serializer, _) = the_default (case the_serializer data
   1.134 -     of Serializer seri => seri) alt_serializer;
   1.135 +    val serializer = the_default (case the_description data
   1.136 +     of Fundamental seri => #serializer seri) alt_serializer;
   1.137      val reserved = the_reserved data;
   1.138      fun select_include names_all (name, (content, cs)) =
   1.139        if null cs then SOME (name, content)
   1.140 @@ -376,9 +377,8 @@
   1.141  fun export_code thy cs seris =
   1.142    let
   1.143      val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
   1.144 -    fun mk_seri_dest dest = case dest
   1.145 -     of "-" => export
   1.146 -      | f => file (Path.explode f)
   1.147 +    fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export
   1.148 +      else file (Path.explode dest);
   1.149      val _ = map (fn (((target, module), dest), args) =>
   1.150        (mk_seri_dest dest (serialize thy target NONE module args naming program cs'))) seris;
   1.151    in () end;
   1.152 @@ -524,7 +524,7 @@
   1.153    (Scan.repeat1 Parse.term_group
   1.154    -- Scan.repeat (Parse.$$$ inK |-- Parse.name
   1.155       -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
   1.156 -     --| Parse.$$$ fileK -- Parse.name
   1.157 +     -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
   1.158       -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
   1.159    ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
   1.160