src/Pure/Tools/codegen_serializer.ML

-(*  Title:      Pure/Tools/codegen_serializer.ML
+    (*  Title:      Pure/Tools/codegen_serializer.ML
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Serializer from intermediate language ("Thin-gol") to
 target languages (like SML or Haskell).

    -> (string -> string) -> (string -> string) -> string -> theory -> theory;
   val add_undefined: string -> string -> string -> theory -> theory;
   val add_pretty_imperative_monad_bind: string -> string -> theory -> theory;
 
   type serializer;
-  val add_serializer : string * serializer -> theory -> theory;
-  val get_serializer: theory -> string -> Args.T list
+  val add_serializer: string * serializer -> theory -> theory;
+  val get_serializer: theory -> string -> Args.T list -> (theory -> string -> string)
     -> string list option -> CodegenThingol.code -> unit;
   val assert_serializer: theory -> string -> string;
 
   val const_has_serialization: theory -> string list -> string -> bool;
   val tyco_has_serialization: theory -> string list -> string -> bool;
 
   val eval_verbose: bool ref;
-  val eval_term: theory -> CodegenThingol.code
+  val eval_term: theory -> (theory -> string -> string) -> CodegenThingol.code
     -> (string * 'a option ref) * CodegenThingol.iterm -> 'a;
   val code_width: int ref;
 end;
 
 structure CodegenSerializer: CODEGEN_SERIALIZER =

     BR
   | NOBR
   | INFX of (int * lrx);
 
 val APP = INFX (~1, L);
-
-type typ_syntax = int * ((fixity -> itype -> Pretty.T)
-  -> fixity -> itype list -> Pretty.T);
-type term_syntax = int * ((CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T)
-  -> CodegenNames.var_ctxt ->  fixity -> iterm list -> Pretty.T);
 
 fun eval_lrx L L = false
   | eval_lrx R R = false
   | eval_lrx _ _ = true;
 

   gen_brackify (eval_fxy BR fxy_ctxt) (Pretty.breaks ps);
 
 fun brackify_infix infx fxy_ctxt ps =
   gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
 
+type class_syntax = string * (string -> string option);
+type typ_syntax = int * ((fixity -> itype -> Pretty.T)
+  -> fixity -> itype list -> Pretty.T);
+type term_syntax = int * ((CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T)
+  -> CodegenNames.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+
 
 (* user-defined syntax *)
 
 datatype 'a mixfix =
     Arg of fixity
   | Pretty of Pretty.T;
 
-fun mk_mixfix (fixity_this, mfx) =
+fun mk_mixfix prep_arg (fixity_this, mfx) =
   let
     fun is_arg (Arg _) = true
       | is_arg _ = false;
     val i = (length o filter is_arg) mfx;
     fun fillin _ [] [] =
           []
       | fillin pr (Arg fxy :: mfx) (a :: args) =
-          pr fxy a :: fillin pr mfx args
+          (pr fxy o prep_arg) a :: fillin pr mfx args
       | fillin pr (Pretty p :: mfx) args =
           p :: fillin pr mfx args
       | fillin _ [] _ =
           error ("Inconsistent mixfix: too many arguments")
       | fillin _ _ [] =

   in
     (i, fn pr => fn fixity_ctxt => fn args =>
       gen_brackify (eval_fxy fixity_this fixity_ctxt) (fillin pr mfx args))
   end;
 
-fun parse_infix (x, i) s =
+fun parse_infix prep_arg (x, i) s =
   let
     val l = case x of L => INFX (i, L) | _ => INFX (i, X);
     val r = case x of R => INFX (i, R) | _ => INFX (i, X);
   in
-    mk_mixfix (INFX (i, x), [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
+    mk_mixfix prep_arg (INFX (i, x), [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
   end;
 
-fun parse_mixfix s =
+fun parse_mixfix prep_arg s =
   let
     val sym_any = Scan.one Symbol.not_eof;
     val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
          ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
       || ($$ "_" >> K (Arg BR))

       || (Scan.repeat1
            (   $$ "'" |-- sym_any
             || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
                  sym_any) >> (Pretty o str o implode)));
   in case Scan.finite Symbol.stopper parse (Symbol.explode s)
-   of ((_, p as [_]), []) => mk_mixfix (NOBR, p)
-    | ((b, p as _ :: _ :: _), []) => mk_mixfix (if b then NOBR else BR, p)
+   of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
+    | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
     | _ => Scan.!! (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
   end;
 
 fun parse_args f args =
   case Scan.read Args.stopper f args

     | NONE => error "Bad serializer arguments";
 
 
 (* generic serializer combinators *)
 
-fun gen_pr_app pr_app' pr_term const_syntax vars fxy (app as ((c, (_, ty)), ts)) =
+fun gen_pr_app pr_app' pr_term const_syntax vars fxy (app as ((c, (_, tys)), ts)) =
   case const_syntax c
    of NONE => brackify fxy (pr_app' vars app)
     | SOME (i, pr) =>
         let
-          val k = if i < 0 then (length o fst o CodegenThingol.unfold_fun) ty else i
+          val k = if i < 0 then length tys else i;
+          fun pr' fxy ts = pr pr_term vars fxy (ts ~~ curry Library.take k tys);
         in if k = length ts
-          then 
-            pr pr_term vars fxy ts
-          else if k < length ts
-          then case chop k ts of (ts1, ts2) =>
-            brackify fxy (pr pr_term vars APP ts1 :: map (pr_term vars BR) ts2)
+          then pr' fxy ts
+        else if k < length ts
+          then case chop k ts of (ts1, ts2) => brackify fxy (pr' APP ts1 :: map (pr_term vars BR) ts2)
           else pr_term vars fxy (CodegenThingol.eta_expand app k)
         end;
 
 fun gen_pr_bind pr_bind' pr_term fxy ((v, pat), ty) vars =
   let

             | NONE => NONE;
   in CodegenThingol.unfoldr dest_monad t end;
 
 fun pretty_ml_string c_nil c_cons mk_char mk_string target_implode =
   let
-    fun pretty pr vars fxy [t] =
+    fun pretty pr vars fxy [(t, _)] =
       case implode_list c_nil c_cons t
        of SOME ts => (case implode_string mk_char mk_string ts
            of SOME p => p
             | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr vars BR t])
         | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr vars BR t]

       brackify_infix (target_fxy, R) fxy [
         pr (INFX (target_fxy, X)) t1,
         str target_cons,
         pr (INFX (target_fxy, R)) t2
       ];
-    fun pretty pr vars fxy [t1, t2] =
+    fun pretty pr vars fxy [(t1, _), (t2, _)] =
       case Option.map (cons t1) (implode_list c_nil c_cons t2)
        of SOME ts =>
             (case mk_char_string
              of SOME (mk_char, mk_string) =>
                   (case implode_string mk_char mk_string ts

         | NONE => default (pr vars) fxy t1 t2;
   in (2, pretty) end;
 
 val pretty_imperative_monad_bind =
   let
-    fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T) vars fxy [t1, (v, ty) `|-> t2] =
-          pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
-      | pretty pr vars fxy [t1, t2] =
+    fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T)
+          vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
+            pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
+      | pretty pr vars fxy [(t1, _), (t2, ty2)] =
           let
             (*this code suffers from the lack of a proper concept for bindings*)
             val vs = CodegenThingol.fold_varnames cons t2 [];
             val v = Name.variant vs "x";
             val vars' = CodegenNames.intro_vars [v] vars;
             val var = IVar v;
-            val ty = "" `%% []; (*an approximation*)
+            val ty = (hd o fst o CodegenThingol.unfold_fun) ty2;
           in pr vars' fxy (ICase ((t1, ty), ([(var, t2 `$ var)]))) end;
   in (2, pretty) end;
 
 
 

   | MLClass of string * ((class * string) list * (vname * (string * itype) list))
   | MLClassinst of string * ((class * (string * (vname * sort) list))
         * ((class * (string * (string * dict list list))) list
       * (string * iterm) list));
 
-fun pr_sml tyco_syntax const_syntax keyword_vars deresolv is_cons ml_def =
+fun pr_sml tyco_syntax const_syntax labelled_name keyword_vars deresolv is_cons ml_def =
   let
     val pr_label = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
     fun pr_dicts fxy ds =
       let
         fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"

               :: pr_term vars NOBR td
               :: pr "of" b
               :: map (pr "|") bs
             )
           end
-    and pr_app' vars (app as ((c, (iss, ty)), ts)) =
+    and pr_app' vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then let
-        val k = (length o fst o CodegenThingol.unfold_fun) ty
+        val k = length tys
       in if k < 2 then 
         (str o deresolv) c :: map (pr_term vars BR) ts
       else if k = length ts then
         [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
       else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else

                   | mk (_::_) _ = "fun"
                   | mk [] vs = if (null o filter_out (null o snd)) vs then "val" else "fun";
                 fun chk (_, ((ts, _) :: _, (vs, _))) NONE = SOME (mk ts vs)
                   | chk (_, ((ts, _) :: _, (vs, _))) (SOME defi) =
                       if defi = mk ts vs then SOME defi
-                      else error ("Mixing simultaneous vals and funs not implemented");
+                      else error ("Mixing simultaneous vals and funs not implemented: "
+                        ^ commas (map (labelled_name o fst) funns));
               in the (fold chk funns NONE) end;
             fun pr_funn definer (name, (eqs as eq::eqs', (raw_vs, ty))) =
               let
                 val vs = filter_out (null o snd) raw_vs;
                 val shift = if null eqs' then I else

   ] @ content @ [
     str "",
     str ("end; (*struct " ^ name ^ "*)")
   ]);
 
-fun pr_ocaml tyco_syntax const_syntax keyword_vars deresolv is_cons ml_def =
+fun pr_ocaml tyco_syntax const_syntax labelled_name keyword_vars deresolv is_cons ml_def =
   let
     fun pr_dicts fxy ds =
       let
         fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
           | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);

               :: pr_term vars NOBR td
               :: pr "with" b
               :: map (pr "|") bs
             )
           end
-    and pr_app' vars (app as ((c, (iss, ty)), ts)) =
+    and pr_app' vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then
-        if (length o fst o CodegenThingol.unfold_fun) ty = length ts
+        if length tys = length ts
         then case ts
          of [] => [(str o deresolv) c]
           | [t] => [(str o deresolv) c, pr_term vars BR t]
           | _ => [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
-        else [pr_term vars BR (CodegenThingol.eta_expand app ((length o fst o CodegenThingol.unfold_fun) ty))]
+        else [pr_term vars BR (CodegenThingol.eta_expand app (length tys))]
       else (str o deresolv) c
         :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
     and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
     and pr_bind' ((NONE, NONE), _) = str "_"
       | pr_bind' ((SOME v, NONE), _) = str v

   ]);
 
 val code_width = ref 80;
 fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
 
-fun seri_ml pr_def pr_modl output reserved_user module_alias module_prolog
-  (_ : string -> (string * (string -> string option)) option) tyco_syntax const_syntax code =
+fun seri_ml pr_def pr_modl output labelled_name reserved_user module_alias module_prolog
+  (_ : string -> class_syntax option) tyco_syntax const_syntax code =
   let
     val is_cons = fn node => case CodegenThingol.get_def code node
      of CodegenThingol.Datatypecons _ => true
       | _ => false;
     datatype node =

       in (x, (nsp_fun, nsp_typ')) end;
     fun mk_funs defs =
       fold_map
         (fn (name, CodegenThingol.Fun info) =>
               map_nsp_fun (name_def false name) >> (fn base => (base, (name, info)))
-          | (name, def) => error ("Function block containing illegal def: " ^ quote name)
+          | (name, def) => error ("Function block containing illegal definition: " ^ labelled_name name)
         ) defs
       >> (split_list #> apsnd MLFuns);
     fun mk_datatype defs =
       fold_map
         (fn (name, CodegenThingol.Datatype info) =>
               map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
           | (name, CodegenThingol.Datatypecons _) =>
               map_nsp_fun (name_def true name) >> (fn base => (base, NONE))
-          | (name, def) => error ("Datatype block containing illegal def: " ^ quote name)
+          | (name, def) => error ("Datatype block containing illegal definition: " ^ labelled_name name)
         ) defs
       >> (split_list #> apsnd (map_filter I
-        #> (fn [] => error ("Datatype block without data: " ^ (commas o map (quote o fst)) defs)
+        #> (fn [] => error ("Datatype block without data definition: " ^ (commas o map (labelled_name o fst)) defs)
              | infos => MLDatas infos)));
     fun mk_class defs =
       fold_map
         (fn (name, CodegenThingol.Class info) =>
               map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
           | (name, CodegenThingol.Classrel _) =>
               map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
           | (name, CodegenThingol.Classop _) =>
               map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
-          | (name, def) => error ("Class block containing illegal def: " ^ quote name)
+          | (name, def) => error ("Class block containing illegal definition: " ^ labelled_name name)
         ) defs
       >> (split_list #> apsnd (map_filter I
-        #> (fn [] => error ("Class block without class: " ^ (commas o map (quote o fst)) defs)
+        #> (fn [] => error ("Class block without class definition: " ^ (commas o map (labelled_name o fst)) defs)
              | [info] => MLClass info)));
     fun mk_inst [(name, CodegenThingol.Classinst info)] =
       map_nsp_fun (name_def false name)
       >> (fn base => ([base], MLClassinst (name, info)));
     fun add_group mk defs nsp_nodes =

           |> fold (fold (insert (op =)) o Graph.imm_succs code) names
           |> subtract (op =) names;
         val (modls, _) = (split_list o map dest_name) names;
         val modl = (the_single o distinct (op =)) modls
           handle Empty =>
-            error ("Illegal mutual dependencies: " ^ commas names);
+            error ("Illegal mutual dependencies: " ^ commas (map labelled_name names));
         val modl' = name_modl modl;
         val modl_explode = NameSpace.explode modl';
         fun add_dep name name'' =
           let
             val modl'' = (name_modl o fst o dest_name) name'';

           add_group mk_class defs
       | group_defs ((defs as (_, CodegenThingol.Classop _)::_)) =
           add_group mk_class defs
       | group_defs ((defs as [(_, CodegenThingol.Classinst _)])) =
           add_group mk_inst defs
-      | group_defs defs = error ("Illegal mutual dependencies: " ^ (commas o map fst) defs)
+      | group_defs defs = error ("Illegal mutual dependencies: " ^ (commas o map (labelled_name o fst)) defs)
     val (_, nodes) =
       empty_module
       |> fold group_defs (map (AList.make (Graph.get_node code))
           (rev (Graph.strong_conn code)))
     fun deresolver prefix name = 

               of Module (_, (_, g)) => g) modl'
           |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
       in
         NameSpace.implode (remainder @ [defname'])
       end handle Graph.UNDEF _ =>
-        error "Unknown name: " ^ quote name;
+        error ("Unknown definition name: " ^ labelled_name name);
     fun the_prolog modlname = case module_prolog modlname
      of NONE => []
       | SOME p => [p, str ""];
     fun pr_node prefix (Def (_, NONE)) =
           NONE
       | pr_node prefix (Def (_, SOME def)) =
-          SOME (pr_def tyco_syntax const_syntax init_vars (deresolver prefix) is_cons def)
+          SOME (pr_def tyco_syntax const_syntax labelled_name init_vars (deresolver prefix) is_cons def)
       | pr_node prefix (Module (dmodlname, (_, nodes))) =
           SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
             @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
                 o rev o flat o Graph.strong_conn) nodes)));
     val p = pr_modl "ROOT" (the_prolog "" @ separate (str "") ((map_filter

 
 val pr_bind_haskell = gen_pr_bind pr_bind';
 
 in
 
-fun pr_haskell class_syntax tyco_syntax const_syntax keyword_vars deresolv_here deresolv deriving_show def =
+fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name keyword_vars deresolv_here deresolv deriving_show def =
   let
     fun class_name class = case class_syntax class
      of NONE => deresolv class
       | SOME (class, _) => class;
     fun classop_name class classop = case class_syntax class

           end;
   in pr_def def end;
 
 fun pretty_haskell_monad c_mbind c_kbind =
   let
-    fun pretty pr vars fxy [t] =
+    fun pretty pr vars fxy [(t, _)] =
       let
         val pr_bind = pr_bind_haskell pr;
         fun pr_mbind (NONE, t) vars =
               (semicolon [pr vars NOBR t], vars)
           | pr_mbind (SOME (bind, true), t) vars = vars

   "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
   "import", "default", "forall", "let", "in", "class", "qualified", "data",
   "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
 ];
 
-fun seri_haskell module_prefix destination string_classes reserved_user module_alias module_prolog
+fun seri_haskell module_prefix destination string_classes labelled_name reserved_user module_alias module_prolog
   class_syntax tyco_syntax const_syntax code =
   let
     val _ = Option.map File.check destination;
     val empty_names = Name.make_context (reserved_haskell @ reserved_user);
     val name_modl = mk_modl_name_tab empty_names module_prefix module_alias code
-    fun add_def (name, (def, deps : string list)) =
+    fun add_def (name, (def, deps)) =
       let
         val (modl, base) = dest_name name;
         fun name_def base = Name.variants [base] #>> the_single;
         fun add_fun upper (nsp_fun, nsp_typ) =
           let

         (Graph.strong_conn code |> flat)) Symtab.empty;
     val init_vars = CodegenNames.make_vars (reserved_haskell @ reserved_user);
     fun deresolv name =
       (fst o fst o the o AList.lookup (op =) ((fst o snd o the
         o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
-        handle Option => "(error \"undefined name " ^ name ^ "\")";
+        handle Option => error ("Unknown definition name: " ^ labelled_name name);
     fun deresolv_here name =
       (snd o fst o the o AList.lookup (op =) ((fst o snd o the
         o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
-        handle Option => "(error \"undefined name " ^ name ^ "\")";
+        handle Option => error ("Unknown definition name: " ^ labelled_name name);
     fun deriving_show tyco =
       let
         fun deriv _ "fun" = false
           | deriv tycos tyco = member (op =) tycos tyco orelse
               case the_default CodegenThingol.Bot (try (Graph.get_node code) tyco)

                     (maps snd cs)
         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
               andalso forall (deriv' tycos) tys
           | deriv' _ (ITyVar _) = true
       in deriv [] tyco end;
-    fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax init_vars
-      deresolv_here (if qualified then deresolv else deresolv_here) (if string_classes then deriving_show else K false);
+    fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_vars
+      deresolv_here (if qualified then deresolv else deresolv_here)
+      (if string_classes then deriving_show else K false);
     fun write_module (SOME destination) modlname =
           let
             val filename = case modlname
              of "" => Path.explode "Main.hs"
               | _ => (Path.ext "hs" o Path.explode o implode o separate "/" o NameSpace.explode) modlname;

       seri_haskell module_prefix (Option.map Path.explode destination) string_classes));
 
 
 (** diagnosis serializer **)
 
-fun seri_diagnosis _ _ _ _ _ code =
+fun seri_diagnosis labelled_name _ _ _ _ _ code =
   let
     val init_vars = CodegenNames.make_vars reserved_haskell;
-    val pr = pr_haskell (K NONE) (K NONE) (K NONE) init_vars I I (K false);
+    val pr = pr_haskell (K NONE) (K NONE) (K NONE) labelled_name init_vars I I (K false);
   in
     []
     |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
     |> Pretty.chunks2
     |> code_output

     Symtab.merge (op =) (alias1, alias2),
     Symtab.merge (op =) (prolog1, prolog2)
   );
 
 type serializer = Args.T list
+  -> (string -> string)
   -> string list
   -> (string -> string option)
   -> (string -> Pretty.T option)
-  -> (string -> (string * (string -> string option)) option)
+  -> (string -> class_syntax option)
   -> (string -> typ_syntax option)
   -> (string -> term_syntax option)
   -> CodegenThingol.code -> unit;
 
 datatype target = Target of {

   #> add_serializer (target_OCaml, isar_seri_ocaml)
   #> add_serializer (target_Haskell, isar_seri_haskell)
   #> add_serializer (target_diag, (fn _ => fn _ => seri_diagnosis))
 );
 
-fun get_serializer thy target args = fn cs =>
+fun get_serializer thy target args labelled_name = fn cs =>
   let
     val data = case Symtab.lookup (CodegenSerializerData.get thy) target
      of SOME data => data
       | NONE => error ("Unknown code target language: " ^ quote target);
     val seri = the_serializer data;

     fun fun_of sys = (Option.map fst oo Symtab.lookup) sys;
     val project = if target = target_diag then I
       else CodegenThingol.project_code
         (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs;
   in
-    project #> seri args reserved (Symtab.lookup alias) (Symtab.lookup prolog)
+    project #> seri args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
       (fun_of class) (fun_of tyco) (fun_of const)
   end;
 
 val eval_verbose = ref false;
 
-fun eval_term thy code ((ref_name, reff), t) =
+fun eval_term thy labelled_name code ((ref_name, reff), t) =
   let
     val val_name = "eval.EVAL.EVAL";
     val val_name' = "ROOT.eval.EVAL";
     val data = (the o Symtab.lookup (CodegenSerializerData.get thy)) "SML"
     val reserved = the_reserved data;

     code
     |> CodegenThingol.add_eval_def (val_name, t)
     |> CodegenThingol.project_code
         (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const)
           (SOME [val_name])
-    |> seri_ml pr_sml pr_sml_modl I reserved (Symtab.lookup alias) (Symtab.lookup prolog)
+    |> seri_ml pr_sml pr_sml_modl I (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
         (fun_of class) (fun_of tyco) (fun_of const)
     |> eval
   end;
 
 fun assert_serializer thy target =

     val pr = pretty_haskell_monad c_mbind'' c_kbind''
   in
     thy
     |> gen_add_syntax_const (K I) target_Haskell c_run' (SOME pr)
     |> gen_add_syntax_const (K I) target_Haskell c_mbind'
-          (no_bindings (SOME (parse_infix (L, 1) ">>=")))
+          (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))
     |> gen_add_syntax_const (K I) target_Haskell c_kbind'
-          (no_bindings (SOME (parse_infix (L, 1) ">>")))
+          (no_bindings (SOME (parse_infix fst (L, 1) ">>")))
   end;
 
 val add_syntax_class = gen_add_syntax_class read_class CodegenConsts.read_const;
 val add_syntax_inst = gen_add_syntax_inst read_class read_type;
 val add_syntax_tyco = gen_add_syntax_tyco read_type;

   #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
         (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
 
 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
 
-fun parse_syntax xs =
+fun parse_syntax prep_arg xs =
   Scan.option ((
       ((P.$$$ infixK  >> K X)
         || (P.$$$ infixlK >> K L)
         || (P.$$$ infixrK >> K R))
-        -- P.nat >> parse_infix
-      || Scan.succeed parse_mixfix)
+        -- P.nat >> parse_infix prep_arg
+      || Scan.succeed (parse_mixfix prep_arg))
       -- P.string
       >> (fn (parse, s) => parse s)) xs;
 
 val (code_classK, code_instanceK, code_typeK, code_constK, code_monadK,
   code_reservedK, code_modulenameK, code_moduleprologK) =

           fold (fn (raw_inst, add_del) => add_syntax_inst target raw_inst add_del) syns)
   );
 
 val code_typeP =
   OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
-    parse_multi_syntax P.xname parse_syntax
+    parse_multi_syntax P.xname (parse_syntax I)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
           fold (fn (raw_tyco, syn) => add_syntax_tyco target raw_tyco syn) syns)
   );
 
 val code_constP =
   OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
-    parse_multi_syntax P.term parse_syntax
+    parse_multi_syntax P.term (parse_syntax fst)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
           fold (fn (raw_const, syn) => add_syntax_const target raw_const (no_bindings syn)) syns)
   );
 
 val code_monadP =