clarified various user-defined syntax issues
authorhaftmann
Mon Dec 21 08:32:04 2009 +0100 (2009-12-21)
changeset 341528e5b596d8c73
parent 34151 8d57ce46b3f7
child 34153 5da0f7abbe29
clarified various user-defined syntax issues
src/Tools/Code/code_printer.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_printer.ML	Mon Dec 21 08:32:04 2009 +0100
     1.2 +++ b/src/Tools/Code/code_printer.ML	Mon Dec 21 08:32:04 2009 +0100
     1.3 @@ -59,16 +59,16 @@
     1.4    val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
     1.5  
     1.6    type tyco_syntax
     1.7 +  type simple_const_syntax
     1.8 +  type proto_const_syntax
     1.9    type const_syntax
    1.10 -  type proto_const_syntax
    1.11    val parse_infix: ('a -> 'b) -> lrx * int -> string
    1.12      -> int * ((fixity -> 'b -> Pretty.T)
    1.13      -> fixity -> 'a list -> Pretty.T)
    1.14    val parse_syntax: ('a -> 'b) -> OuterParse.token list
    1.15      -> (int * ((fixity -> 'b -> Pretty.T)
    1.16      -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
    1.17 -  val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
    1.18 -    -> fixity -> (iterm * itype) list -> Pretty.T)) option -> proto_const_syntax option
    1.19 +  val simple_const_syntax: simple_const_syntax -> proto_const_syntax
    1.20    val activate_const_syntax: theory -> literals
    1.21      -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
    1.22    val gen_print_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
    1.23 @@ -219,15 +219,17 @@
    1.24  
    1.25  type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
    1.26    -> fixity -> itype list -> Pretty.T);
    1.27 -type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    1.28 -  -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    1.29 +
    1.30 +type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
    1.31 +  -> fixity -> (iterm * itype) list -> Pretty.T);
    1.32  type proto_const_syntax = int * (string list * (literals -> string list
    1.33    -> (var_ctxt -> fixity -> iterm -> Pretty.T)
    1.34      -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
    1.35 +type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    1.36 +  -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    1.37  
    1.38 -fun simple_const_syntax (SOME (n, f)) = SOME (n,
    1.39 -      ([], (fn _ => fn _ => fn print => fn thm => fn vars => f (print vars))))
    1.40 -  | simple_const_syntax NONE = NONE;
    1.41 +val simple_const_syntax =
    1.42 +  apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars))));
    1.43  
    1.44  fun activate_const_syntax thy literals (n, (cs, f)) naming =
    1.45    fold_map (Code_Thingol.ensure_declared_const thy) cs naming
    1.46 @@ -307,7 +309,7 @@
    1.47  
    1.48  fun parse_syntax prep_arg xs =
    1.49    Scan.option ((
    1.50 -      ((OuterParse.$$$ infixK  >> K X)
    1.51 +      ((OuterParse.$$$ infixK >> K X)
    1.52          || (OuterParse.$$$ infixlK >> K L)
    1.53          || (OuterParse.$$$ infixrK >> K R))
    1.54          -- OuterParse.nat >> parse_infix prep_arg
     2.1 --- a/src/Tools/Code/code_target.ML	Mon Dec 21 08:32:04 2009 +0100
     2.2 +++ b/src/Tools/Code/code_target.ML	Mon Dec 21 08:32:04 2009 +0100
     2.3 @@ -6,9 +6,8 @@
     2.4  
     2.5  signature CODE_TARGET =
     2.6  sig
     2.7 -  include CODE_PRINTER
     2.8 -
     2.9    type serializer
    2.10 +  type literals = Code_Printer.literals
    2.11    val add_target: string * (serializer * literals) -> theory -> theory
    2.12    val extend_target: string *
    2.13        (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    2.14 @@ -39,6 +38,8 @@
    2.15    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    2.16  
    2.17    val allow_abort: string -> theory -> theory
    2.18 +  type tyco_syntax = Code_Printer.tyco_syntax
    2.19 +  type proto_const_syntax = Code_Printer.proto_const_syntax
    2.20    val add_syntax_class: string -> class -> string option -> theory -> theory
    2.21    val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
    2.22    val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
    2.23 @@ -51,7 +52,11 @@
    2.24  struct
    2.25  
    2.26  open Basic_Code_Thingol;
    2.27 -open Code_Printer;
    2.28 +
    2.29 +type literals = Code_Printer.literals;
    2.30 +type tyco_syntax = Code_Printer.tyco_syntax;
    2.31 +type proto_const_syntax = Code_Printer.proto_const_syntax;
    2.32 +
    2.33  
    2.34  (** basics **)
    2.35  
    2.36 @@ -78,8 +83,8 @@
    2.37  datatype name_syntax_table = NameSyntaxTable of {
    2.38    class: string Symtab.table,
    2.39    instance: unit Symreltab.table,
    2.40 -  tyco: tyco_syntax Symtab.table,
    2.41 -  const: proto_const_syntax Symtab.table
    2.42 +  tyco: Code_Printer.tyco_syntax Symtab.table,
    2.43 +  const: Code_Printer.proto_const_syntax Symtab.table
    2.44  };
    2.45  
    2.46  fun mk_name_syntax_table ((class, instance), (tyco, const)) =
    2.47 @@ -103,14 +108,14 @@
    2.48    -> (string * Pretty.T) list           (*includes*)
    2.49    -> (string -> string option)          (*module aliasses*)
    2.50    -> (string -> string option)          (*class syntax*)
    2.51 -  -> (string -> tyco_syntax option)
    2.52 -  -> (string -> const_syntax option)
    2.53 +  -> (string -> Code_Printer.tyco_syntax option)
    2.54 +  -> (string -> Code_Printer.const_syntax option)
    2.55    -> ((Pretty.T -> string) * (Pretty.T -> unit))
    2.56    -> Code_Thingol.program
    2.57    -> string list                        (*selected statements*)
    2.58    -> serialization;
    2.59  
    2.60 -datatype serializer_entry = Serializer of serializer * literals
    2.61 +datatype serializer_entry = Serializer of serializer * Code_Printer.literals
    2.62    | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    2.63  
    2.64  datatype target = Target of {
    2.65 @@ -273,7 +278,7 @@
    2.66      serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
    2.67        (Symtab.lookup module_alias) (Symtab.lookup class')
    2.68        (Symtab.lookup tyco') (Symtab.lookup const')
    2.69 -      (string_of_pretty width, writeln_pretty width)
    2.70 +      (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
    2.71        program4 names2
    2.72    end;
    2.73  
    2.74 @@ -396,32 +401,32 @@
    2.75  fun read_inst thy (raw_tyco, raw_class) =
    2.76    (read_class thy raw_class, read_tyco thy raw_tyco);
    2.77  
    2.78 -fun gen_add_syntax upd del mapp check_x get_check_syn prep target raw_x some_syn thy =
    2.79 +fun gen_add_syntax upd del mapp check_x check_raw_syn prep_syn prep_x target raw_x some_raw_syn thy =
    2.80    let
    2.81 -    val x = prep thy raw_x;
    2.82 -    fun check_syn thy syn = ();
    2.83 -  in case some_syn
    2.84 -   of SOME syn => (map_name_syntax target o mapp) (upd (x, (check_x thy x; check_syn thy syn; syn))) thy
    2.85 +    val x = prep_x thy raw_x |> tap (check_x thy);
    2.86 +    fun prep_check raw_syn = prep_syn (raw_syn |> tap (check_raw_syn thy target));
    2.87 +  in case some_raw_syn
    2.88 +   of SOME raw_syn => (map_name_syntax target o mapp) (upd (x, prep_check raw_syn)) thy
    2.89      | NONE => (map_name_syntax target o mapp) (del x) thy
    2.90    end;
    2.91  
    2.92 -fun gen_add_syntax_class prep =
    2.93 -  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) I prep;
    2.94 +fun gen_add_syntax_class prep_class =
    2.95 +  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) ((K o K o K) ()) I prep_class;
    2.96  
    2.97 -fun gen_add_syntax_inst prep =
    2.98 -  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) I prep;
    2.99 +fun gen_add_syntax_inst prep_inst =
   2.100 +  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) ((K o K o K) ()) I prep_inst;
   2.101  
   2.102 -fun gen_add_syntax_tyco prep =
   2.103 +fun gen_add_syntax_tyco prep_tyco =
   2.104    gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apfst)
   2.105      (fn thy => fn tyco => fn (n, _) => if n <> Sign.arity_number thy tyco
   2.106        then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
   2.107 -      else ()) I prep;
   2.108 +      else ()) ((K o K o K) ()) I prep_tyco;
   2.109  
   2.110 -fun gen_add_syntax_const prep =
   2.111 +fun gen_add_syntax_const prep_const check_raw_syn prep_syn =
   2.112    gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apsnd)
   2.113      (fn thy => fn c => fn (n, _) => if n > Code.args_number thy c
   2.114        then error ("Too many arguments in syntax for constant " ^ quote c)
   2.115 -      else ()) I prep;
   2.116 +      else ()) check_raw_syn prep_syn prep_const;
   2.117  
   2.118  fun add_reserved target =
   2.119    let
   2.120 @@ -438,7 +443,7 @@
   2.121                then warning ("Overwriting existing include " ^ name)
   2.122                else ();
   2.123              val cs = map (read_const thy) raw_cs;
   2.124 -          in Symtab.update (name, (str content, cs)) incls end
   2.125 +          in Symtab.update (name, (Code_Printer.str content, cs)) incls end
   2.126        | add (name, NONE) incls = Symtab.delete name incls;
   2.127    in map_includes target (add args) thy end;
   2.128  
   2.129 @@ -460,12 +465,6 @@
   2.130      val c = prep_const thy raw_c;
   2.131    in thy |> (CodeTargetData.map o apfst o apsnd) (insert (op =) c) end;
   2.132  
   2.133 -fun zip_list (x::xs) f g =
   2.134 -  f
   2.135 -  #-> (fn y =>
   2.136 -    fold_map (fn x => g |-- f >> pair x) xs
   2.137 -    #-> (fn xys => pair ((x, y) :: xys)));
   2.138 -
   2.139  
   2.140  (* concrete syntax *)
   2.141  
   2.142 @@ -474,6 +473,12 @@
   2.143  structure P = OuterParse
   2.144  and K = OuterKeyword
   2.145  
   2.146 +fun zip_list (x::xs) f g =
   2.147 +  f
   2.148 +  #-> (fn y =>
   2.149 +    fold_map (fn x => g |-- f >> pair x) xs
   2.150 +    #-> (fn xys => pair ((x, y) :: xys)));
   2.151 +
   2.152  fun parse_multi_syntax parse_thing parse_syntax =
   2.153    P.and_list1 parse_thing
   2.154    #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
   2.155 @@ -484,7 +489,8 @@
   2.156  val add_syntax_class = gen_add_syntax_class cert_class;
   2.157  val add_syntax_inst = gen_add_syntax_inst cert_inst;
   2.158  val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
   2.159 -val add_syntax_const = gen_add_syntax_const (K I);
   2.160 +val add_syntax_const_simple = gen_add_syntax_const (K I) ((K o K o K) ()) Code_Printer.simple_const_syntax;
   2.161 +val add_syntax_const = gen_add_syntax_const (K I) ((K o K o K) ()) I;
   2.162  val allow_abort = gen_allow_abort (K I);
   2.163  val add_reserved = add_reserved;
   2.164  val add_include = add_include;
   2.165 @@ -492,7 +498,9 @@
   2.166  val add_syntax_class_cmd = gen_add_syntax_class read_class;
   2.167  val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
   2.168  val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
   2.169 -val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
   2.170 +val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) Code_Printer.simple_const_syntax;
   2.171 +val add_syntax_const_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) I;
   2.172 +
   2.173  val allow_abort_cmd = gen_allow_abort Code.read_const;
   2.174  
   2.175  fun parse_args f args =
   2.176 @@ -524,25 +532,23 @@
   2.177  
   2.178  val _ =
   2.179    OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
   2.180 -    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
   2.181 -      (Scan.option (P.minus >> K ()))
   2.182 +    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) (Scan.option (P.minus >> K ()))
   2.183      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   2.184            fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
   2.185    );
   2.186  
   2.187  val _ =
   2.188    OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
   2.189 -    parse_multi_syntax P.xname (parse_syntax I)
   2.190 +    parse_multi_syntax P.xname (Code_Printer.parse_syntax I)
   2.191      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   2.192            fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
   2.193    );
   2.194  
   2.195  val _ =
   2.196    OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
   2.197 -    parse_multi_syntax P.term_group (parse_syntax fst)
   2.198 +    parse_multi_syntax P.term_group (Code_Printer.parse_syntax fst)
   2.199      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   2.200 -      fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const
   2.201 -        (Code_Printer.simple_const_syntax syn)) syns)
   2.202 +      fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
   2.203    );
   2.204  
   2.205  val _ =