distributed literal code generation out of central infrastructure
authorhaftmann
Tue Sep 02 20:38:17 2008 +0200 (2008-09-02)
changeset 2809029af3c712d2b
parent 28089 66ae1926482a
child 28091 50f2d6ba024c
distributed literal code generation out of central infrastructure
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Message.thy
src/HOL/List.thy
src/HOL/Tools/numeral.ML
src/Tools/code/code_target.ML
     1.1 --- a/src/HOL/Library/Code_Char.thy	Tue Sep 02 20:07:51 2008 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Tue Sep 02 20:38:17 2008 +0200
     1.3 @@ -25,22 +25,8 @@
     1.4    (Haskell "Char")
     1.5  
     1.6  setup {*
     1.7 -let
     1.8 -  val charr = @{const_name Char}
     1.9 -  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
    1.10 -    @{const_name Nibble2}, @{const_name Nibble3},
    1.11 -    @{const_name Nibble4}, @{const_name Nibble5},
    1.12 -    @{const_name Nibble6}, @{const_name Nibble7},
    1.13 -    @{const_name Nibble8}, @{const_name Nibble9},
    1.14 -    @{const_name NibbleA}, @{const_name NibbleB},
    1.15 -    @{const_name NibbleC}, @{const_name NibbleD},
    1.16 -    @{const_name NibbleE}, @{const_name NibbleF}];
    1.17 -in
    1.18 -  fold (fn target => Code_Target.add_literal_char target charr nibbles)
    1.19 -    ["SML", "OCaml", "Haskell"]
    1.20 -  #> Code_Target.add_literal_list_string "Haskell"
    1.21 -    @{const_name Nil} @{const_name Cons} charr nibbles
    1.22 -end
    1.23 +  fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"] 
    1.24 +  #> add_literal_list_string "Haskell"
    1.25  *}
    1.26  
    1.27  code_instance char :: eq
     2.1 --- a/src/HOL/Library/Code_Message.thy	Tue Sep 02 20:07:51 2008 +0200
     2.2 +++ b/src/HOL/Library/Code_Message.thy	Tue Sep 02 20:38:17 2008 +0200
     2.3 @@ -40,21 +40,8 @@
     2.4    (Haskell "String")
     2.5  
     2.6  setup {*
     2.7 -let
     2.8 -  val charr = @{const_name Char}
     2.9 -  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
    2.10 -    @{const_name Nibble2}, @{const_name Nibble3},
    2.11 -    @{const_name Nibble4}, @{const_name Nibble5},
    2.12 -    @{const_name Nibble6}, @{const_name Nibble7},
    2.13 -    @{const_name Nibble8}, @{const_name Nibble9},
    2.14 -    @{const_name NibbleA}, @{const_name NibbleB},
    2.15 -    @{const_name NibbleC}, @{const_name NibbleD},
    2.16 -    @{const_name NibbleE}, @{const_name NibbleF}];
    2.17 -in
    2.18 -  fold (fn target => Code_Target.add_literal_message target
    2.19 -    charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR})
    2.20 -  ["SML", "OCaml", "Haskell"]
    2.21 -end
    2.22 +  fold (fn target => add_literal_message @{const_name STR} target)
    2.23 +    ["SML", "OCaml", "Haskell"]
    2.24  *}
    2.25  
    2.26  code_reserved SML string
     3.1 --- a/src/HOL/List.thy	Tue Sep 02 20:07:51 2008 +0200
     3.2 +++ b/src/HOL/List.thy	Tue Sep 02 20:38:17 2008 +0200
     3.3 @@ -3449,10 +3449,145 @@
     3.4    (OCaml "[]")
     3.5    (Haskell "[]")
     3.6  
     3.7 +ML {*
     3.8 +local
     3.9 +
    3.10 +open Basic_Code_Thingol;
    3.11 +val nil' = Code_Name.const @{theory} @{const_name Nil};
    3.12 +val cons' = Code_Name.const @{theory} @{const_name Cons};
    3.13 +val char' = Code_Name.const @{theory} @{const_name Char}
    3.14 +val nibbles' = map (Code_Name.const @{theory})
    3.15 +   [@{const_name Nibble0}, @{const_name Nibble1},
    3.16 +    @{const_name Nibble2}, @{const_name Nibble3},
    3.17 +    @{const_name Nibble4}, @{const_name Nibble5},
    3.18 +    @{const_name Nibble6}, @{const_name Nibble7},
    3.19 +    @{const_name Nibble8}, @{const_name Nibble9},
    3.20 +    @{const_name NibbleA}, @{const_name NibbleB},
    3.21 +    @{const_name NibbleC}, @{const_name NibbleD},
    3.22 +    @{const_name NibbleE}, @{const_name NibbleF}];
    3.23 +
    3.24 +fun implode_list t =
    3.25 +  let
    3.26 +    fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
    3.27 +          if c = cons'
    3.28 +          then SOME (t1, t2)
    3.29 +          else NONE
    3.30 +      | dest_cons _ = NONE;
    3.31 +    val (ts, t') = Code_Thingol.unfoldr dest_cons t;
    3.32 +  in case t'
    3.33 +   of IConst (c, _) => if c = nil' then SOME ts else NONE
    3.34 +    | _ => NONE
    3.35 +  end;
    3.36 +
    3.37 +fun decode_char (IConst (c1, _), IConst (c2, _)) =
    3.38 +      let
    3.39 +        fun idx c = find_index (curry (op =) c) nibbles';
    3.40 +        fun decode ~1 _ = NONE
    3.41 +          | decode _ ~1 = NONE
    3.42 +          | decode n m = SOME (chr (n * 16 + m));
    3.43 +      in decode (idx c1) (idx c2) end
    3.44 +  | decode_char _ = NONE;
    3.45 +
    3.46 +fun implode_string mk_char mk_string ts =
    3.47 +  let
    3.48 +    fun implode_char (IConst (c, _) `$ t1 `$ t2) =
    3.49 +          if c = char' then decode_char (t1, t2) else NONE
    3.50 +      | implode_char _ = NONE;
    3.51 +    val ts' = map implode_char ts;
    3.52 +  in if forall is_some ts'
    3.53 +    then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
    3.54 +    else NONE
    3.55 +  end;
    3.56 +
    3.57 +fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
    3.58 +  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
    3.59 +    pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
    3.60 +    Code_Printer.str target_cons,
    3.61 +    pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
    3.62 +  ];
    3.63 +
    3.64 +fun pretty_list literals =
    3.65 +  let
    3.66 +    val mk_list = Code_Printer.literal_list literals;
    3.67 +    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
    3.68 +      case Option.map (cons t1) (implode_list t2)
    3.69 +       of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
    3.70 +        | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    3.71 +  in (2, pretty) end;
    3.72 +
    3.73 +fun pretty_list_string literals =
    3.74 +  let
    3.75 +    val mk_list = Code_Printer.literal_list literals;
    3.76 +    val mk_char = Code_Printer.literal_char literals;
    3.77 +    val mk_string = Code_Printer.literal_string literals;
    3.78 +    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
    3.79 +      case Option.map (cons t1) (implode_list t2)
    3.80 +       of SOME ts => (case implode_string mk_char mk_string ts
    3.81 +           of SOME p => p
    3.82 +            | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
    3.83 +        | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    3.84 +  in (2, pretty) end;
    3.85 +
    3.86 +fun pretty_char literals =
    3.87 +  let
    3.88 +    val mk_char = Code_Printer.literal_char literals;
    3.89 +    fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
    3.90 +      case decode_char (t1, t2)
    3.91 +       of SOME c => (Code_Printer.str o mk_char) c
    3.92 +        | NONE => Code_Printer.nerror thm "Illegal character expression";
    3.93 +  in (2, pretty) end;
    3.94 +
    3.95 +fun pretty_message literals =
    3.96 +  let
    3.97 +    val mk_char = Code_Printer.literal_char literals;
    3.98 +    val mk_string = Code_Printer.literal_string literals;
    3.99 +    fun pretty _ thm _ _ _ [(t, _)] =
   3.100 +      case implode_list t
   3.101 +       of SOME ts => (case implode_string mk_char mk_string ts
   3.102 +           of SOME p => p
   3.103 +            | NONE => Code_Printer.nerror thm "Illegal message expression")
   3.104 +        | NONE => Code_Printer.nerror thm "Illegal message expression";
   3.105 +  in (1, pretty) end;
   3.106 +
   3.107 +in
   3.108 +
   3.109 +fun add_literal_list target thy =
   3.110 +  let
   3.111 +    val pr = pretty_list (Code_Target.the_literals thy target);
   3.112 +  in
   3.113 +    thy
   3.114 +    |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
   3.115 +  end;
   3.116 +
   3.117 +fun add_literal_list_string target thy =
   3.118 +  let
   3.119 +    val pr = pretty_list_string (Code_Target.the_literals thy target);
   3.120 +  in
   3.121 +    thy
   3.122 +    |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
   3.123 +  end;
   3.124 +
   3.125 +fun add_literal_char target thy =
   3.126 +  let
   3.127 +    val pr = pretty_char (Code_Target.the_literals thy target);
   3.128 +  in
   3.129 +    thy
   3.130 +    |> Code_Target.add_syntax_const target @{const_name Char} (SOME pr)
   3.131 +  end;
   3.132 +
   3.133 +fun add_literal_message str target thy =
   3.134 +  let
   3.135 +    val pr = pretty_message (Code_Target.the_literals thy target);
   3.136 +  in
   3.137 +    thy
   3.138 +    |> Code_Target.add_syntax_const target str (SOME pr)
   3.139 +  end;
   3.140 +
   3.141 +end;
   3.142 +*}
   3.143 +
   3.144  setup {*
   3.145 -  fold (fn target => Code_Target.add_literal_list target
   3.146 -    @{const_name Nil} @{const_name Cons}
   3.147 -  ) ["SML", "OCaml", "Haskell"]
   3.148 +  fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"]
   3.149  *}
   3.150  
   3.151  code_instance list :: eq
     4.1 --- a/src/HOL/Tools/numeral.ML	Tue Sep 02 20:07:51 2008 +0200
     4.2 +++ b/src/HOL/Tools/numeral.ML	Tue Sep 02 20:38:17 2008 +0200
     4.3 @@ -55,9 +55,34 @@
     4.4  
     4.5  (* code generator *)
     4.6  
     4.7 -fun add_code number_of negative unbounded target =
     4.8 -  Code_Target.add_literal_numeral target negative unbounded number_of
     4.9 -  @{const_name Int.Pls} @{const_name Int.Min}
    4.10 -  @{const_name Int.Bit0} @{const_name Int.Bit1};
    4.11 +local open Basic_Code_Thingol in
    4.12 +
    4.13 +fun add_code number_of negative unbounded target thy =
    4.14 +  let
    4.15 +    val pls' = Code_Name.const thy @{const_name Int.Pls};
    4.16 +    val min' = Code_Name.const thy @{const_name Int.Min};
    4.17 +    val bit0' = Code_Name.const thy @{const_name Int.Bit0};
    4.18 +    val bit1' = Code_Name.const thy @{const_name Int.Bit1};
    4.19 +    val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target;
    4.20 +    fun dest_bit thm (IConst (c, _)) = if c = bit0' then 0
    4.21 +          else if c = bit1' then 1
    4.22 +          else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
    4.23 +      | dest_bit thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
    4.24 +    fun dest_numeral thm (IConst (c, _)) = if c = pls' then SOME 0
    4.25 +          else if c = min' then
    4.26 +            if negative then SOME ~1 else NONE
    4.27 +          else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
    4.28 +      | dest_numeral thm (t1 `$ t2) =
    4.29 +          let val (n, b) = (dest_numeral thm t2, dest_bit thm t1)
    4.30 +          in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
    4.31 +      | dest_numeral thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
    4.32 +    fun pretty _ thm _ _ _ [(t, _)] =
    4.33 +      (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral thm) t;
    4.34 +  in
    4.35 +    thy
    4.36 +    |> Code_Target.add_syntax_const target number_of (SOME (1, pretty))
    4.37 +  end;
    4.38 +
    4.39 +end; (*local*)
    4.40  
    4.41  end;
     5.1 --- a/src/Tools/code/code_target.ML	Tue Sep 02 20:07:51 2008 +0200
     5.2 +++ b/src/Tools/code/code_target.ML	Tue Sep 02 20:38:17 2008 +0200
     5.3 @@ -30,6 +30,7 @@
     5.4      -> Code_Thingol.program -> string list -> serialization
     5.5    val serialize_custom: theory -> string * (serializer * literals)
     5.6      -> Code_Thingol.program -> string list -> string * string list
     5.7 +  val the_literals: theory -> string -> literals
     5.8    val compile: serialization -> unit
     5.9    val export: serialization -> unit
    5.10    val file: Path.T -> serialization -> unit
    5.11 @@ -50,15 +51,6 @@
    5.12    val add_syntax_constP: string -> string -> OuterParse.token list
    5.13      -> (theory -> theory) * OuterParse.token list
    5.14    val add_reserved: string -> string -> theory -> theory
    5.15 -
    5.16 -  val add_literal_list: string -> string -> string -> theory -> theory
    5.17 -  val add_literal_list_string: string -> string -> string
    5.18 -    -> string -> string list -> theory -> theory
    5.19 -  val add_literal_char: string -> string -> string list -> theory -> theory
    5.20 -  val add_literal_numeral: string -> bool -> bool -> string -> string -> string
    5.21 -    -> string -> string -> theory -> theory
    5.22 -  val add_literal_message: string -> string -> string list -> string
    5.23 -    -> string -> string -> theory -> theory
    5.24  end;
    5.25  
    5.26  structure Code_Target : CODE_TARGET =
    5.27 @@ -93,120 +85,6 @@
    5.28    | mk_serialization target _ _ string code (String _) = SOME (string code);
    5.29  
    5.30  
    5.31 -(** pretty syntax **)
    5.32 -
    5.33 -(* list, char, string, numeral and monad abstract syntax transformations *)
    5.34 -
    5.35 -fun implode_list c_nil c_cons t =
    5.36 -  let
    5.37 -    fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
    5.38 -          if c = c_cons
    5.39 -          then SOME (t1, t2)
    5.40 -          else NONE
    5.41 -      | dest_cons _ = NONE;
    5.42 -    val (ts, t') = Code_Thingol.unfoldr dest_cons t;
    5.43 -  in case t'
    5.44 -   of IConst (c, _) => if c = c_nil then SOME ts else NONE
    5.45 -    | _ => NONE
    5.46 -  end;
    5.47 -
    5.48 -fun decode_char c_nibbles (IConst (c1, _), IConst (c2, _)) =
    5.49 -      let
    5.50 -        fun idx c = find_index (curry (op =) c) c_nibbles;
    5.51 -        fun decode ~1 _ = NONE
    5.52 -          | decode _ ~1 = NONE
    5.53 -          | decode n m = SOME (chr (n * 16 + m));
    5.54 -      in decode (idx c1) (idx c2) end
    5.55 -  | decode_char _ _ = NONE;
    5.56 -
    5.57 -fun implode_string c_char c_nibbles mk_char mk_string ts =
    5.58 -  let
    5.59 -    fun implode_char (IConst (c, _) `$ t1 `$ t2) =
    5.60 -          if c = c_char then decode_char c_nibbles (t1, t2) else NONE
    5.61 -      | implode_char _ = NONE;
    5.62 -    val ts' = map implode_char ts;
    5.63 -  in if forall is_some ts'
    5.64 -    then (SOME o str o mk_string o implode o map_filter I) ts'
    5.65 -    else NONE
    5.66 -  end;
    5.67 -
    5.68 -fun implode_numeral thm negative c_pls c_min c_bit0 c_bit1 =
    5.69 -  let
    5.70 -    fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0
    5.71 -          else if c = c_bit1 then 1
    5.72 -          else nerror thm "Illegal numeral expression: illegal bit"
    5.73 -      | dest_bit _ = nerror thm "Illegal numeral expression: illegal bit";
    5.74 -    fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
    5.75 -          else if c = c_min then
    5.76 -            if negative then SOME ~1 else NONE
    5.77 -          else nerror thm "Illegal numeral expression: illegal leading digit"
    5.78 -      | dest_numeral (t1 `$ t2) =
    5.79 -          let val (n, b) = (dest_numeral t2, dest_bit t1)
    5.80 -          in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
    5.81 -      | dest_numeral _ = nerror thm "Illegal numeral expression: illegal term";
    5.82 -  in dest_numeral #> the_default 0 end;
    5.83 -
    5.84 -
    5.85 -(* literal syntax printing *)
    5.86 -
    5.87 -fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
    5.88 -  brackify_infix (target_fxy, R) fxy [
    5.89 -    pr (INFX (target_fxy, X)) t1,
    5.90 -    str target_cons,
    5.91 -    pr (INFX (target_fxy, R)) t2
    5.92 -  ];
    5.93 -
    5.94 -fun pretty_list c_nil c_cons literals =
    5.95 -  let
    5.96 -    val mk_list = literal_list literals;
    5.97 -    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
    5.98 -      case Option.map (cons t1) (implode_list c_nil c_cons t2)
    5.99 -       of SOME ts => mk_list (map (pr vars NOBR) ts)
   5.100 -        | NONE => default_list (infix_cons literals) (pr vars) fxy t1 t2;
   5.101 -  in (2, pretty) end;
   5.102 -
   5.103 -fun pretty_list_string c_nil c_cons c_char c_nibbles literals =
   5.104 -  let
   5.105 -    val mk_list = literal_list literals;
   5.106 -    val mk_char = literal_char literals;
   5.107 -    val mk_string = literal_string literals;
   5.108 -    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
   5.109 -      case Option.map (cons t1) (implode_list c_nil c_cons t2)
   5.110 -       of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
   5.111 -           of SOME p => p
   5.112 -            | NONE => mk_list (map (pr vars NOBR) ts))
   5.113 -        | NONE => default_list (infix_cons literals) (pr vars) fxy t1 t2;
   5.114 -  in (2, pretty) end;
   5.115 -
   5.116 -fun pretty_char c_char c_nibbles literals =
   5.117 -  let
   5.118 -    val mk_char = literal_char literals;
   5.119 -    fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
   5.120 -      case decode_char c_nibbles (t1, t2)
   5.121 -       of SOME c => (str o mk_char) c
   5.122 -        | NONE => nerror thm "Illegal character expression";
   5.123 -  in (2, pretty) end;
   5.124 -
   5.125 -fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 literals =
   5.126 -  let
   5.127 -    val mk_numeral = literal_numeral literals;
   5.128 -    fun pretty _ thm _ _ _ [(t, _)] =
   5.129 -      (str o mk_numeral unbounded o implode_numeral thm negative c_pls c_min c_bit0 c_bit1) t;
   5.130 -  in (1, pretty) end;
   5.131 -
   5.132 -fun pretty_message c_char c_nibbles c_nil c_cons literals =
   5.133 -  let
   5.134 -    val mk_char = literal_char literals;
   5.135 -    val mk_string = literal_string literals;
   5.136 -    fun pretty _ thm _ _ _ [(t, _)] =
   5.137 -      case implode_list c_nil c_cons t
   5.138 -       of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
   5.139 -           of SOME p => p
   5.140 -            | NONE => nerror thm "Illegal message expression")
   5.141 -        | NONE => nerror thm "Illegal message expression";
   5.142 -  in (1, pretty) end;
   5.143 -
   5.144 -
   5.145  (** theory data **)
   5.146  
   5.147  datatype name_syntax_table = NameSyntaxTable of {
   5.148 @@ -507,62 +385,6 @@
   5.149        | NONE => error ("Unknown code target language: " ^ quote target);
   5.150    in literals end;
   5.151  
   5.152 -fun add_literal_list target nill cons thy =
   5.153 -  let
   5.154 -    val nil' = Code_Name.const thy nill;
   5.155 -    val cons' = Code_Name.const thy cons;
   5.156 -    val pr = pretty_list nil' cons' (the_literals thy target);
   5.157 -  in
   5.158 -    thy
   5.159 -    |> add_syntax_const target cons (SOME pr)
   5.160 -  end;
   5.161 -
   5.162 -fun add_literal_list_string target nill cons charr nibbles thy =
   5.163 -  let
   5.164 -    val nil' = Code_Name.const thy nill;
   5.165 -    val cons' = Code_Name.const thy cons;
   5.166 -    val charr' = Code_Name.const thy charr;
   5.167 -    val nibbles' = map (Code_Name.const thy) nibbles;
   5.168 -    val pr = pretty_list_string nil' cons' charr' nibbles' (the_literals thy target);
   5.169 -  in
   5.170 -    thy
   5.171 -    |> add_syntax_const target cons (SOME pr)
   5.172 -  end;
   5.173 -
   5.174 -fun add_literal_char target charr nibbles thy =
   5.175 -  let
   5.176 -    val charr' = Code_Name.const thy charr;
   5.177 -    val nibbles' = map (Code_Name.const thy) nibbles;
   5.178 -    val pr = pretty_char charr' nibbles' (the_literals thy target);
   5.179 -  in
   5.180 -    thy
   5.181 -    |> add_syntax_const target charr (SOME pr)
   5.182 -  end;
   5.183 -
   5.184 -fun add_literal_numeral target unbounded negative number_of pls min bit0 bit1 thy =
   5.185 -  let
   5.186 -    val pls' = Code_Name.const thy pls;
   5.187 -    val min' = Code_Name.const thy min;
   5.188 -    val bit0' = Code_Name.const thy bit0;
   5.189 -    val bit1' = Code_Name.const thy bit1;
   5.190 -    val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' (the_literals thy target);
   5.191 -  in
   5.192 -    thy
   5.193 -    |> add_syntax_const target number_of (SOME pr)
   5.194 -  end;
   5.195 -
   5.196 -fun add_literal_message target charr nibbles nill cons str thy =
   5.197 -  let
   5.198 -    val charr' = Code_Name.const thy charr;
   5.199 -    val nibbles' = map (Code_Name.const thy) nibbles;
   5.200 -    val nil' = Code_Name.const thy nill;
   5.201 -    val cons' = Code_Name.const thy cons;
   5.202 -    val pr = pretty_message charr' nibbles' nil' cons' (the_literals thy target);
   5.203 -  in
   5.204 -    thy
   5.205 -    |> add_syntax_const target str (SOME pr)
   5.206 -  end;
   5.207 -
   5.208  
   5.209  (** serializer usage **)
   5.210