distinguish different classes of const syntax
authorhaftmann
Mon Jul 19 11:55:44 2010 +0200 (2010-07-19)
changeset 37881096c8397c989
parent 37880 3b9ca8d2c5fb
child 37882 1fd0ac61920c
distinguish different classes of const syntax
src/HOL/Tools/list_code.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/string_code.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/HOL/Tools/list_code.ML	Mon Jul 19 11:55:43 2010 +0200
     1.2 +++ b/src/HOL/Tools/list_code.ML	Mon Jul 19 11:55:44 2010 +0200
     1.3 @@ -46,8 +46,8 @@
     1.4              Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
     1.5          | NONE =>
     1.6              default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
     1.7 -  in Code_Target.add_syntax_const target
     1.8 -    @{const_name Cons} (SOME (2, ([@{const_name Nil}, @{const_name Cons}], pretty)))
     1.9 +  in Code_Target.add_syntax_const target @{const_name Cons}
    1.10 +    (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
    1.11    end
    1.12  
    1.13  end;
     2.1 --- a/src/HOL/Tools/numeral.ML	Mon Jul 19 11:55:43 2010 +0200
     2.2 +++ b/src/HOL/Tools/numeral.ML	Mon Jul 19 11:55:44 2010 +0200
     2.3 @@ -77,8 +77,8 @@
     2.4        (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
     2.5    in
     2.6      thy |> Code_Target.add_syntax_const target number_of
     2.7 -      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
     2.8 -        @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
     2.9 +      (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
    2.10 +        @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
    2.11    end;
    2.12  
    2.13  end; (*local*)
     3.1 --- a/src/HOL/Tools/string_code.ML	Mon Jul 19 11:55:43 2010 +0200
     3.2 +++ b/src/HOL/Tools/string_code.ML	Mon Jul 19 11:55:44 2010 +0200
     3.3 @@ -60,7 +60,7 @@
     3.4          | NONE =>
     3.5              List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
     3.6    in Code_Target.add_syntax_const target
     3.7 -    @{const_name Cons} (SOME (2, (cs_summa, pretty)))
     3.8 +    @{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
     3.9    end;
    3.10  
    3.11  fun add_literal_char target =
    3.12 @@ -70,7 +70,7 @@
    3.13         of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
    3.14          | NONE => Code_Printer.eqn_error thm "Illegal character expression";
    3.15    in Code_Target.add_syntax_const target
    3.16 -    @{const_name Char} (SOME (2, (cs_nibbles, pretty)))
    3.17 +    @{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
    3.18    end;
    3.19  
    3.20  fun add_literal_string target =
    3.21 @@ -83,7 +83,7 @@
    3.22                | NONE => Code_Printer.eqn_error thm "Illegal message expression")
    3.23          | NONE => Code_Printer.eqn_error thm "Illegal message expression";
    3.24    in Code_Target.add_syntax_const target 
    3.25 -    @{const_name STR} (SOME (1, (cs_summa, pretty)))
    3.26 +    @{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
    3.27    end;
    3.28  
    3.29  end;
     4.1 --- a/src/Tools/Code/code_haskell.ML	Mon Jul 19 11:55:43 2010 +0200
     4.2 +++ b/src/Tools/Code/code_haskell.ML	Mon Jul 19 11:55:44 2010 +0200
     4.3 @@ -218,30 +218,35 @@
     4.4        | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
     4.5            let
     4.6              val tyvars = intro_vars (map fst vs) reserved;
     4.7 -            fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam
     4.8 -             of NONE => semicolon [
     4.9 -                    (str o deresolve_base) classparam,
    4.10 -                    str "=",
    4.11 -                    print_app tyvars (SOME thm) reserved NOBR (const, [])
    4.12 -                  ]
    4.13 -              | SOME (k, pr) =>
    4.14 -                  let
    4.15 -                    val (c, (_, tys)) = const;
    4.16 -                    val (vs, rhs) = (apfst o map) fst
    4.17 -                      (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
    4.18 -                    val s = if (is_some o syntax_const) c
    4.19 -                      then NONE else (SOME o Long_Name.base_name o deresolve) c;
    4.20 -                    val vars = reserved
    4.21 -                      |> intro_vars (map_filter I (s :: vs));
    4.22 -                    val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
    4.23 -                      (*dictionaries are not relevant at this late stage*)
    4.24 -                  in
    4.25 -                    semicolon [
    4.26 -                      print_term tyvars (SOME thm) vars NOBR lhs,
    4.27 +            fun requires_args classparam = case syntax_const classparam
    4.28 +             of NONE => 0
    4.29 +              | SOME (Code_Printer.Plain_const_syntax _) => 0
    4.30 +              | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
    4.31 +            fun print_classparam_instance ((classparam, const), (thm, _)) =
    4.32 +              case requires_args classparam
    4.33 +               of 0 => semicolon [
    4.34 +                      (str o deresolve_base) classparam,
    4.35                        str "=",
    4.36 -                      print_term tyvars (SOME thm) vars NOBR rhs
    4.37 +                      print_app tyvars (SOME thm) reserved NOBR (const, [])
    4.38                      ]
    4.39 -                  end;
    4.40 +                | k =>
    4.41 +                    let
    4.42 +                      val (c, (_, tys)) = const;
    4.43 +                      val (vs, rhs) = (apfst o map) fst
    4.44 +                        (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
    4.45 +                      val s = if (is_some o syntax_const) c
    4.46 +                        then NONE else (SOME o Long_Name.base_name o deresolve) c;
    4.47 +                      val vars = reserved
    4.48 +                        |> intro_vars (map_filter I (s :: vs));
    4.49 +                      val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
    4.50 +                        (*dictionaries are not relevant at this late stage*)
    4.51 +                    in
    4.52 +                      semicolon [
    4.53 +                        print_term tyvars (SOME thm) vars NOBR lhs,
    4.54 +                        str "=",
    4.55 +                        print_term tyvars (SOME thm) vars NOBR rhs
    4.56 +                      ]
    4.57 +                    end;
    4.58            in
    4.59              Pretty.block_enclose (
    4.60                Pretty.block [
    4.61 @@ -459,7 +464,7 @@
    4.62    in if target = target' then
    4.63      thy
    4.64      |> Code_Target.add_syntax_const target c_bind
    4.65 -        (SOME (pretty_haskell_monad c_bind))
    4.66 +        (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
    4.67    else error "Only Haskell target allows for monad syntax" end;
    4.68  
    4.69  
     5.1 --- a/src/Tools/Code/code_printer.ML	Mon Jul 19 11:55:43 2010 +0200
     5.2 +++ b/src/Tools/Code/code_printer.ML	Mon Jul 19 11:55:44 2010 +0200
     5.3 @@ -67,17 +67,19 @@
     5.4  
     5.5    type tyco_syntax
     5.6    type simple_const_syntax
     5.7 +  type complex_const_syntax
     5.8    type const_syntax
     5.9 -  type activated_const_syntax
    5.10 -  val parse_infix: ('a -> 'b) -> lrx * int -> string
    5.11 -    -> int * ((fixity -> 'b -> Pretty.T)
    5.12 -    -> fixity -> 'a list -> Pretty.T)
    5.13 -  val parse_syntax: ('a -> 'b) -> Token.T list
    5.14 -    -> (int * ((fixity -> 'b -> Pretty.T)
    5.15 -    -> fixity -> 'a list -> Pretty.T)) option * Token.T list
    5.16 +  type activated_complex_const_syntax
    5.17 +  datatype activated_const_syntax = Plain_const_syntax of int * string
    5.18 +    | Complex_const_syntax of activated_complex_const_syntax
    5.19 +  val requires_args: const_syntax -> int
    5.20 +  val parse_const_syntax: Token.T list -> const_syntax option * Token.T list
    5.21 +  val parse_tyco_syntax: Token.T list -> tyco_syntax option * Token.T list
    5.22 +  val plain_const_syntax: string -> const_syntax
    5.23    val simple_const_syntax: simple_const_syntax -> const_syntax
    5.24 +  val complex_const_syntax: complex_const_syntax -> const_syntax
    5.25    val activate_const_syntax: theory -> literals
    5.26 -    -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
    5.27 +    -> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
    5.28    val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
    5.29      -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    5.30      -> (string -> activated_const_syntax option)
    5.31 @@ -243,31 +245,45 @@
    5.32  
    5.33  type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
    5.34    -> fixity -> (iterm * itype) list -> Pretty.T);
    5.35 -type const_syntax = int * (string list * (literals -> string list
    5.36 +
    5.37 +type complex_const_syntax = int * (string list * (literals -> string list
    5.38    -> (var_ctxt -> fixity -> iterm -> Pretty.T)
    5.39      -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
    5.40 -type activated_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    5.41 -  -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    5.42 +
    5.43 +datatype const_syntax = plain_const_syntax of string
    5.44 +  | complex_const_syntax of complex_const_syntax;
    5.45 +
    5.46 +fun requires_args (plain_const_syntax _) = 0
    5.47 +  | requires_args (complex_const_syntax (k, _)) = k;
    5.48  
    5.49  fun simple_const_syntax syn =
    5.50 -  apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn;
    5.51 +  complex_const_syntax (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
    5.52  
    5.53 -fun activate_const_syntax thy literals (n, (cs, f)) naming =
    5.54 -  fold_map (Code_Thingol.ensure_declared_const thy) cs naming
    5.55 -  |-> (fn cs' => pair (n, f literals cs'));
    5.56 +type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    5.57 +  -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
    5.58 +
    5.59 +datatype activated_const_syntax = Plain_const_syntax of int * string
    5.60 +  | Complex_const_syntax of activated_complex_const_syntax;
    5.61  
    5.62 -fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) =
    5.63 +fun activate_const_syntax thy literals c (plain_const_syntax s) naming =
    5.64 +      (Plain_const_syntax (Code.args_number thy c, s), naming)
    5.65 +  | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming =
    5.66 +      fold_map (Code_Thingol.ensure_declared_const thy) cs naming
    5.67 +      |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
    5.68 +
    5.69 +fun gen_print_app print_app_expr print_term syntax_const some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
    5.70    case syntax_const c
    5.71 -   of NONE => brackify fxy (print_app_expr thm vars app)
    5.72 -    | SOME (k, print) =>
    5.73 +   of NONE => brackify fxy (print_app_expr some_thm vars app)
    5.74 +    | SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts)
    5.75 +    | SOME (Complex_const_syntax (k, print)) =>
    5.76          let
    5.77 -          fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs);
    5.78 +          fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
    5.79          in if k = length ts
    5.80            then print' fxy ts
    5.81          else if k < length ts
    5.82            then case chop k ts of (ts1, ts2) =>
    5.83 -            brackify fxy (print' APP ts1 :: map (print_term thm vars BR) ts2)
    5.84 -          else print_term thm vars fxy (Code_Thingol.eta_expand k app)
    5.85 +            brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
    5.86 +          else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
    5.87          end;
    5.88  
    5.89  fun gen_print_bind print_term thm (fxy : fixity) pat vars =
    5.90 @@ -281,7 +297,8 @@
    5.91  
    5.92  datatype 'a mixfix =
    5.93      Arg of fixity
    5.94 -  | Pretty of Pretty.T;
    5.95 +  | String of string
    5.96 +  | Break;
    5.97  
    5.98  fun mk_mixfix prep_arg (fixity_this, mfx) =
    5.99    let
   5.100 @@ -292,8 +309,10 @@
   5.101            []
   5.102        | fillin print (Arg fxy :: mfx) (a :: args) =
   5.103            (print fxy o prep_arg) a :: fillin print mfx args
   5.104 -      | fillin print (Pretty p :: mfx) args =
   5.105 -          p :: fillin print mfx args;
   5.106 +      | fillin print (String s :: mfx) args =
   5.107 +          str s :: fillin print mfx args
   5.108 +      | fillin print (Break :: mfx) args =
   5.109 +          Pretty.brk 1 :: fillin print mfx args;
   5.110    in
   5.111      (i, fn print => fn fixity_ctxt => fn args =>
   5.112        gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args))
   5.113 @@ -304,42 +323,45 @@
   5.114      val l = case x of L => INFX (i, L) | _ => INFX (i, X);
   5.115      val r = case x of R => INFX (i, R) | _ => INFX (i, X);
   5.116    in
   5.117 -    mk_mixfix prep_arg (INFX (i, x),
   5.118 -      [Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
   5.119 +    mk_mixfix prep_arg (INFX (i, x), [Arg l, String " ", String s, Break, Arg r])
   5.120    end;
   5.121  
   5.122 -fun parse_mixfix prep_arg s =
   5.123 +fun parse_mixfix mk_plain mk_complex prep_arg s =
   5.124    let
   5.125      val sym_any = Scan.one Symbol.is_regular;
   5.126      val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
   5.127           ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
   5.128        || ($$ "_" >> K (Arg BR))
   5.129 -      || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
   5.130 +      || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break))
   5.131        || (Scan.repeat1
   5.132             (   $$ "'" |-- sym_any
   5.133              || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
   5.134 -                 sym_any) >> (Pretty o str o implode)));
   5.135 +                 sym_any) >> (String o implode)));
   5.136    in case Scan.finite Symbol.stopper parse (Symbol.explode s)
   5.137 -   of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
   5.138 -    | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
   5.139 +   of ((false, [String s]), []) => mk_plain s
   5.140 +    | ((_, p as [_]), []) => mk_complex (mk_mixfix prep_arg (NOBR, p))
   5.141 +    | ((b, p as _ :: _ :: _), []) => mk_complex (mk_mixfix prep_arg (if b then NOBR else BR, p))
   5.142      | _ => Scan.!!
   5.143          (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
   5.144    end;
   5.145  
   5.146  val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
   5.147  
   5.148 -fun parse_syntax prep_arg xs =
   5.149 -  Scan.option ((
   5.150 +fun parse_syntax mk_plain mk_complex prep_arg =
   5.151 +  Scan.option (
   5.152        ((Parse.$$$ infixK >> K X)
   5.153          || (Parse.$$$ infixlK >> K L)
   5.154          || (Parse.$$$ infixrK >> K R))
   5.155 -        -- Parse.nat >> parse_infix prep_arg
   5.156 -      || Scan.succeed (parse_mixfix prep_arg))
   5.157 -      -- Parse.string
   5.158 -      >> (fn (parse, s) => parse s)) xs;
   5.159 +        -- Parse.nat -- Parse.string
   5.160 +        >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
   5.161 +      || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s)));
   5.162  
   5.163  val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
   5.164  
   5.165 +val parse_tyco_syntax = parse_syntax (fn s => (0, (K o K o K o str) s)) I I;
   5.166 +
   5.167 +val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst;
   5.168 +
   5.169  
   5.170  (** module name spaces **)
   5.171  
     6.1 --- a/src/Tools/Code/code_scala.ML	Mon Jul 19 11:55:43 2010 +0200
     6.2 +++ b/src/Tools/Code/code_scala.ML	Mon Jul 19 11:55:44 2010 +0200
     6.3 @@ -76,17 +76,20 @@
     6.4          (app as ((c, ((arg_typs, _), function_typs)), ts)) =
     6.5        let
     6.6          val k = length ts;
     6.7 -        val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
     6.8          val arg_typs' = if is_pat orelse
     6.9            (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
    6.10 -        val (no_syntax, print') = case syntax_const c
    6.11 -         of NONE => (true, fn ts => applify "(" ")"
    6.12 +        val (l, print') = case syntax_const c
    6.13 +         of NONE => (args_num c, fn ts => applify "(" ")"
    6.14                (print_term tyvars is_pat some_thm vars NOBR) fxy
    6.15                  (applify "[" "]" (print_typ tyvars NOBR)
    6.16                    NOBR ((str o deresolve) c) arg_typs') ts)
    6.17 -          | SOME (_, print) => (false, fn ts =>
    6.18 -              print (print_term tyvars is_pat some_thm) some_thm vars fxy
    6.19 -                (ts ~~ take l function_typs));
    6.20 +          | SOME (Plain_const_syntax (k, s)) => (k, fn ts => applify "(" ")"
    6.21 +              (print_term tyvars is_pat some_thm vars NOBR) fxy
    6.22 +                (applify "[" "]" (print_typ tyvars NOBR)
    6.23 +                  NOBR (str s) arg_typs') ts)
    6.24 +          | SOME (Complex_const_syntax (k, print)) =>
    6.25 +              (k, fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
    6.26 +                (ts ~~ take k function_typs))
    6.27        in if k = l then print' ts
    6.28        else if k < l then
    6.29          print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
    6.30 @@ -355,20 +358,22 @@
    6.31        | _ => false;
    6.32      val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
    6.33        reserved args_num is_singleton_constr deresolver;
    6.34 -    fun print_module name content =
    6.35 -      (name, Pretty.chunks [
    6.36 -        str ("object " ^ name ^ " {"),
    6.37 -        str "",
    6.38 +    fun print_module name imports content =
    6.39 +      (name, Pretty.chunks (
    6.40 +        str ("object " ^ name ^ " {")
    6.41 +        :: (if null imports then []
    6.42 +          else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports)
    6.43 +        @ [str "",
    6.44          content,
    6.45          str "",
    6.46 -        str "}"
    6.47 -      ]);
    6.48 +        str "}"]
    6.49 +      ));
    6.50      fun serialize_module the_module_name sca_program =
    6.51        let
    6.52          val content = Pretty.chunks2 (map_filter
    6.53            (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
    6.54              | (_, (_, NONE)) => NONE) sca_program);
    6.55 -      in print_module the_module_name content end;
    6.56 +      in print_module the_module_name (map fst includes) content end;
    6.57      fun check_destination destination =
    6.58        (File.check destination; destination);
    6.59      fun write_module destination (modlname, content) =
    6.60 @@ -385,7 +390,7 @@
    6.61        (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
    6.62          (write_module (check_destination file)))
    6.63        (rpair [] o cat_lines o map (code_of_pretty o snd))
    6.64 -      (map (uncurry print_module) includes
    6.65 +      (map (fn (name, content) => print_module name [] content) includes
    6.66          @| serialize_module the_module_name sca_program)
    6.67        destination
    6.68    end;
    6.69 @@ -405,7 +410,7 @@
    6.70    literal_char = Library.enclose "'" "'" o char_scala,
    6.71    literal_string = quote o translate_string char_scala,
    6.72    literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
    6.73 -  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
    6.74 +  literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
    6.75    literal_naive_numeral = fn k => if k >= 0
    6.76      then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
    6.77    literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
     7.1 --- a/src/Tools/Code/code_target.ML	Mon Jul 19 11:55:43 2010 +0200
     7.2 +++ b/src/Tools/Code/code_target.ML	Mon Jul 19 11:55:44 2010 +0200
     7.3 @@ -244,11 +244,11 @@
     7.4    |>> map_filter I;
     7.5  
     7.6  fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
     7.7 -  |> fold_map (fn thing_identifier => fn (tab, naming) =>
     7.8 -      case Code_Thingol.lookup_const naming thing_identifier
     7.9 +  |> fold_map (fn c => fn (tab, naming) =>
    7.10 +      case Code_Thingol.lookup_const naming c
    7.11         of SOME name => let
    7.12                val (syn, naming') = Code_Printer.activate_const_syntax thy
    7.13 -                literals (the (Symtab.lookup src_tab thing_identifier)) naming
    7.14 +                literals c (the (Symtab.lookup src_tab c)) naming
    7.15              in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
    7.16          | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
    7.17    |>> map_filter I;
    7.18 @@ -445,12 +445,12 @@
    7.19        then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
    7.20        else syn);
    7.21  
    7.22 -fun gen_add_syntax_const prep_const prep_syn =
    7.23 +fun gen_add_syntax_const prep_const =
    7.24    gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
    7.25 -    (fn thy => fn c => fn raw_syn => let val syn = prep_syn raw_syn in
    7.26 -      if fst syn > Code.args_number thy c
    7.27 +    (fn thy => fn c => fn syn =>
    7.28 +      if Code_Printer.requires_args syn > Code.args_number thy c
    7.29        then error ("Too many arguments in syntax for constant " ^ quote c)
    7.30 -      else syn end);
    7.31 +      else syn);
    7.32  
    7.33  fun add_reserved target =
    7.34    let
    7.35 @@ -496,22 +496,23 @@
    7.36  
    7.37  fun zip_list (x::xs) f g =
    7.38    f
    7.39 -  #-> (fn y =>
    7.40 +  :|-- (fn y =>
    7.41      fold_map (fn x => g |-- f >> pair x) xs
    7.42 -    #-> (fn xys => pair ((x, y) :: xys)));
    7.43 +    :|-- (fn xys => pair ((x, y) :: xys)));
    7.44  
    7.45 -fun parse_multi_syntax parse_thing parse_syntax =
    7.46 -  Parse.and_list1 parse_thing
    7.47 -  #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
    7.48 -        (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"));
    7.49 +fun process_multi_syntax parse_thing parse_syntax change =
    7.50 +  (Parse.and_list1 parse_thing
    7.51 +  :|-- (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
    7.52 +        (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")")))
    7.53 +  >> (Toplevel.theory oo fold)
    7.54 +    (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
    7.55  
    7.56  in
    7.57  
    7.58  val add_syntax_class = gen_add_syntax_class cert_class;
    7.59  val add_syntax_inst = gen_add_syntax_inst cert_inst;
    7.60  val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
    7.61 -val add_syntax_const_simple = gen_add_syntax_const (K I) Code_Printer.simple_const_syntax;
    7.62 -val add_syntax_const = gen_add_syntax_const (K I) I;
    7.63 +val add_syntax_const = gen_add_syntax_const (K I);
    7.64  val allow_abort = gen_allow_abort (K I);
    7.65  val add_reserved = add_reserved;
    7.66  val add_include = add_include;
    7.67 @@ -519,9 +520,7 @@
    7.68  val add_syntax_class_cmd = gen_add_syntax_class read_class;
    7.69  val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
    7.70  val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
    7.71 -val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const Code_Printer.simple_const_syntax;
    7.72 -val add_syntax_const_cmd = gen_add_syntax_const Code.read_const I;
    7.73 -
    7.74 +val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
    7.75  val allow_abort_cmd = gen_allow_abort Code.read_const;
    7.76  
    7.77  fun parse_args f args =
    7.78 @@ -550,32 +549,24 @@
    7.79  
    7.80  val _ =
    7.81    Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
    7.82 -    parse_multi_syntax Parse.xname (Scan.option Parse.string)
    7.83 -    >> (Toplevel.theory oo fold) (fn (target, syns) =>
    7.84 -          fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
    7.85 -  );
    7.86 +    process_multi_syntax Parse.xname (Scan.option Parse.string)
    7.87 +    add_syntax_class_cmd);
    7.88  
    7.89  val _ =
    7.90    Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
    7.91 -    parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
    7.92 +    process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
    7.93        (Scan.option (Parse.minus >> K ()))
    7.94 -    >> (Toplevel.theory oo fold) (fn (target, syns) =>
    7.95 -          fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
    7.96 -  );
    7.97 +    add_syntax_inst_cmd);
    7.98  
    7.99  val _ =
   7.100    Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
   7.101 -    parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I)
   7.102 -    >> (Toplevel.theory oo fold) (fn (target, syns) =>
   7.103 -          fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
   7.104 -  );
   7.105 +    process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
   7.106 +    add_syntax_tyco_cmd);
   7.107  
   7.108  val _ =
   7.109    Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
   7.110 -    parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst)
   7.111 -    >> (Toplevel.theory oo fold) (fn (target, syns) =>
   7.112 -      fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
   7.113 -  );
   7.114 +    process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
   7.115 +    add_syntax_const_cmd);
   7.116  
   7.117  val _ =
   7.118    Outer_Syntax.command "code_reserved" "declare words as reserved for target language"