src/Tools/Code/code_target.ML
changeset 34152 8e5b596d8c73
parent 34081 bb01fd325c6b
child 34173 458ced35abb8
     1.1 --- a/src/Tools/Code/code_target.ML	Mon Dec 21 08:32:04 2009 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Dec 21 08:32:04 2009 +0100
     1.3 @@ -6,9 +6,8 @@
     1.4  
     1.5  signature CODE_TARGET =
     1.6  sig
     1.7 -  include CODE_PRINTER
     1.8 -
     1.9    type serializer
    1.10 +  type literals = Code_Printer.literals
    1.11    val add_target: string * (serializer * literals) -> theory -> theory
    1.12    val extend_target: string *
    1.13        (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    1.14 @@ -39,6 +38,8 @@
    1.15    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    1.16  
    1.17    val allow_abort: string -> theory -> theory
    1.18 +  type tyco_syntax = Code_Printer.tyco_syntax
    1.19 +  type proto_const_syntax = Code_Printer.proto_const_syntax
    1.20    val add_syntax_class: string -> class -> string option -> theory -> theory
    1.21    val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
    1.22    val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
    1.23 @@ -51,7 +52,11 @@
    1.24  struct
    1.25  
    1.26  open Basic_Code_Thingol;
    1.27 -open Code_Printer;
    1.28 +
    1.29 +type literals = Code_Printer.literals;
    1.30 +type tyco_syntax = Code_Printer.tyco_syntax;
    1.31 +type proto_const_syntax = Code_Printer.proto_const_syntax;
    1.32 +
    1.33  
    1.34  (** basics **)
    1.35  
    1.36 @@ -78,8 +83,8 @@
    1.37  datatype name_syntax_table = NameSyntaxTable of {
    1.38    class: string Symtab.table,
    1.39    instance: unit Symreltab.table,
    1.40 -  tyco: tyco_syntax Symtab.table,
    1.41 -  const: proto_const_syntax Symtab.table
    1.42 +  tyco: Code_Printer.tyco_syntax Symtab.table,
    1.43 +  const: Code_Printer.proto_const_syntax Symtab.table
    1.44  };
    1.45  
    1.46  fun mk_name_syntax_table ((class, instance), (tyco, const)) =
    1.47 @@ -103,14 +108,14 @@
    1.48    -> (string * Pretty.T) list           (*includes*)
    1.49    -> (string -> string option)          (*module aliasses*)
    1.50    -> (string -> string option)          (*class syntax*)
    1.51 -  -> (string -> tyco_syntax option)
    1.52 -  -> (string -> const_syntax option)
    1.53 +  -> (string -> Code_Printer.tyco_syntax option)
    1.54 +  -> (string -> Code_Printer.const_syntax option)
    1.55    -> ((Pretty.T -> string) * (Pretty.T -> unit))
    1.56    -> Code_Thingol.program
    1.57    -> string list                        (*selected statements*)
    1.58    -> serialization;
    1.59  
    1.60 -datatype serializer_entry = Serializer of serializer * literals
    1.61 +datatype serializer_entry = Serializer of serializer * Code_Printer.literals
    1.62    | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    1.63  
    1.64  datatype target = Target of {
    1.65 @@ -273,7 +278,7 @@
    1.66      serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
    1.67        (Symtab.lookup module_alias) (Symtab.lookup class')
    1.68        (Symtab.lookup tyco') (Symtab.lookup const')
    1.69 -      (string_of_pretty width, writeln_pretty width)
    1.70 +      (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
    1.71        program4 names2
    1.72    end;
    1.73  
    1.74 @@ -396,32 +401,32 @@
    1.75  fun read_inst thy (raw_tyco, raw_class) =
    1.76    (read_class thy raw_class, read_tyco thy raw_tyco);
    1.77  
    1.78 -fun gen_add_syntax upd del mapp check_x get_check_syn prep target raw_x some_syn thy =
    1.79 +fun gen_add_syntax upd del mapp check_x check_raw_syn prep_syn prep_x target raw_x some_raw_syn thy =
    1.80    let
    1.81 -    val x = prep thy raw_x;
    1.82 -    fun check_syn thy syn = ();
    1.83 -  in case some_syn
    1.84 -   of SOME syn => (map_name_syntax target o mapp) (upd (x, (check_x thy x; check_syn thy syn; syn))) thy
    1.85 +    val x = prep_x thy raw_x |> tap (check_x thy);
    1.86 +    fun prep_check raw_syn = prep_syn (raw_syn |> tap (check_raw_syn thy target));
    1.87 +  in case some_raw_syn
    1.88 +   of SOME raw_syn => (map_name_syntax target o mapp) (upd (x, prep_check raw_syn)) thy
    1.89      | NONE => (map_name_syntax target o mapp) (del x) thy
    1.90    end;
    1.91  
    1.92 -fun gen_add_syntax_class prep =
    1.93 -  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) I prep;
    1.94 +fun gen_add_syntax_class prep_class =
    1.95 +  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) ((K o K o K) ()) I prep_class;
    1.96  
    1.97 -fun gen_add_syntax_inst prep =
    1.98 -  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) I prep;
    1.99 +fun gen_add_syntax_inst prep_inst =
   1.100 +  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) ((K o K o K) ()) I prep_inst;
   1.101  
   1.102 -fun gen_add_syntax_tyco prep =
   1.103 +fun gen_add_syntax_tyco prep_tyco =
   1.104    gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apfst)
   1.105      (fn thy => fn tyco => fn (n, _) => if n <> Sign.arity_number thy tyco
   1.106        then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
   1.107 -      else ()) I prep;
   1.108 +      else ()) ((K o K o K) ()) I prep_tyco;
   1.109  
   1.110 -fun gen_add_syntax_const prep =
   1.111 +fun gen_add_syntax_const prep_const check_raw_syn prep_syn =
   1.112    gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apsnd)
   1.113      (fn thy => fn c => fn (n, _) => if n > Code.args_number thy c
   1.114        then error ("Too many arguments in syntax for constant " ^ quote c)
   1.115 -      else ()) I prep;
   1.116 +      else ()) check_raw_syn prep_syn prep_const;
   1.117  
   1.118  fun add_reserved target =
   1.119    let
   1.120 @@ -438,7 +443,7 @@
   1.121                then warning ("Overwriting existing include " ^ name)
   1.122                else ();
   1.123              val cs = map (read_const thy) raw_cs;
   1.124 -          in Symtab.update (name, (str content, cs)) incls end
   1.125 +          in Symtab.update (name, (Code_Printer.str content, cs)) incls end
   1.126        | add (name, NONE) incls = Symtab.delete name incls;
   1.127    in map_includes target (add args) thy end;
   1.128  
   1.129 @@ -460,12 +465,6 @@
   1.130      val c = prep_const thy raw_c;
   1.131    in thy |> (CodeTargetData.map o apfst o apsnd) (insert (op =) c) end;
   1.132  
   1.133 -fun zip_list (x::xs) f g =
   1.134 -  f
   1.135 -  #-> (fn y =>
   1.136 -    fold_map (fn x => g |-- f >> pair x) xs
   1.137 -    #-> (fn xys => pair ((x, y) :: xys)));
   1.138 -
   1.139  
   1.140  (* concrete syntax *)
   1.141  
   1.142 @@ -474,6 +473,12 @@
   1.143  structure P = OuterParse
   1.144  and K = OuterKeyword
   1.145  
   1.146 +fun zip_list (x::xs) f g =
   1.147 +  f
   1.148 +  #-> (fn y =>
   1.149 +    fold_map (fn x => g |-- f >> pair x) xs
   1.150 +    #-> (fn xys => pair ((x, y) :: xys)));
   1.151 +
   1.152  fun parse_multi_syntax parse_thing parse_syntax =
   1.153    P.and_list1 parse_thing
   1.154    #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
   1.155 @@ -484,7 +489,8 @@
   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_syntax_const_simple = gen_add_syntax_const (K I) ((K o K o K) ()) Code_Printer.simple_const_syntax;
   1.161 +val add_syntax_const = gen_add_syntax_const (K I) ((K o K o K) ()) I;
   1.162  val allow_abort = gen_allow_abort (K I);
   1.163  val add_reserved = add_reserved;
   1.164  val add_include = add_include;
   1.165 @@ -492,7 +498,9 @@
   1.166  val add_syntax_class_cmd = gen_add_syntax_class read_class;
   1.167  val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
   1.168  val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
   1.169 -val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
   1.170 +val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) Code_Printer.simple_const_syntax;
   1.171 +val add_syntax_const_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) I;
   1.172 +
   1.173  val allow_abort_cmd = gen_allow_abort Code.read_const;
   1.174  
   1.175  fun parse_args f args =
   1.176 @@ -524,25 +532,23 @@
   1.177  
   1.178  val _ =
   1.179    OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
   1.180 -    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
   1.181 -      (Scan.option (P.minus >> K ()))
   1.182 +    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) (Scan.option (P.minus >> K ()))
   1.183      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   1.184            fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
   1.185    );
   1.186  
   1.187  val _ =
   1.188    OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
   1.189 -    parse_multi_syntax P.xname (parse_syntax I)
   1.190 +    parse_multi_syntax P.xname (Code_Printer.parse_syntax I)
   1.191      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   1.192            fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
   1.193    );
   1.194  
   1.195  val _ =
   1.196    OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
   1.197 -    parse_multi_syntax P.term_group (parse_syntax fst)
   1.198 +    parse_multi_syntax P.term_group (Code_Printer.parse_syntax fst)
   1.199      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   1.200 -      fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const
   1.201 -        (Code_Printer.simple_const_syntax syn)) syns)
   1.202 +      fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
   1.203    );
   1.204  
   1.205  val _ =