src/Pure/Tools/codegen_serializer.ML

   | 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 * ((vname list -> fixity -> iterm -> Pretty.T) -> fixity
-  -> iterm list -> Pretty.T);
+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;
 

     | NONE => error "bad serializer arguments";
 
 
 (* generic serializer combinators *)
 
-fun gen_pr_app pr_app' pr_term const_syntax fxy (app as ((c, (_, ty)), ts)) =
+fun gen_pr_app pr_app' pr_term const_syntax vars fxy (app as ((c, (_, ty)), ts)) =
   case const_syntax c
-   of NONE => brackify fxy (pr_app' app)
+   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
         in if k = length ts
           then 
-            pr pr_term fxy ts
+            pr pr_term vars fxy ts
           else if k < length ts
           then case chop k ts of (ts1, ts2) =>
-            brackify fxy (pr pr_term APP ts1 :: map (pr_term [] BR) ts2)
-          else pr_term [] fxy (CodegenThingol.eta_expand app k)
+            brackify fxy (pr pr_term vars 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
     val vs = case pat

             | 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 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 [] BR t])
-        | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr [] BR t]
+            | 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]
   in (1, pretty) end;
 
 fun pretty_list c_nil c_cons mk_list mk_char_string (target_fxy, target_cons) =
   let
     fun default pr fxy t1 t2 =
       brackify_infix (target_fxy, R) fxy [
         pr (INFX (target_fxy, X)) t1,
         str target_cons,
         pr (INFX (target_fxy, R)) t2
       ];
-    fun pretty pr 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
                    of SOME p => p
-                    | NONE => mk_list (map (pr [] NOBR) ts))
-              | NONE => mk_list (map (pr [] NOBR) ts))
-        | NONE => default (pr []) fxy t1 t2;
+                    | NONE => mk_list (map (pr vars NOBR) ts))
+              | NONE => mk_list (map (pr vars NOBR) ts))
+        | NONE => default (pr vars) fxy t1 t2;
   in (2, pretty) end;
 
 val pretty_imperative_monad_bind =
   let
-    fun pretty (pr : vname list -> fixity -> iterm -> Pretty.T) fxy [t1, (v, ty) `|-> t2] =
-          pr [] fxy (ICase ((t1, ty), ([(IVar v, t2)])))
-      | pretty _ _ _ = error "bad arguments for imperative monad bind";
+    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 _ _ _ _ = error "bad arguments for imperative monad bind";
   in (2, pretty) end;
-
-fun pretty_haskell_monad c_mbind c_kbind =
-  let
-    fun pr_bnd pr ((SOME v, NONE), _) = str "<FOO>"
-      | pr_bnd pr ((NONE, SOME t), _) = str "<FOO>"
-      | pr_bnd pr ((SOME v, SOME t), _) = str "<FOO>";
-    fun pr_bind pr (NONE, t) = semicolon [pr [] NOBR t]
-      | pr_bind pr (SOME (bind, true), t) = semicolon [pr_bnd pr bind, str "<-", pr [] NOBR t]
-      | pr_bind pr (SOME (bind, false), t) = semicolon [str "let", pr_bnd pr bind, str "=", pr [] NOBR t];
-    fun brack fxy p = if eval_fxy BR fxy then Pretty.block [str "(", p, str ")"] else p;
-    fun pretty pr fxy [t] =
-      let
-        val (binds, t) = implode_monad c_mbind c_kbind t;
-      in (brack fxy o Pretty.block_enclose (str "do {", str "}")) (
-        map (pr_bind pr) binds
-        @| pr [] NOBR t
-      ) end;
-  in (1, pretty) end;
 
 
 
 (** name auxiliary **)
 

       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
         (str o deresolv) c
           :: ((map (pr_insts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
-    and pr_app vars fxy (app as ((c, (iss, ty)), ts)) =
-      gen_pr_app (pr_app' vars) (fn vars' => pr_term (CodegenNames.intro_vars vars' vars))
-        const_syntax fxy app
+    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
       | pr_bind' ((NONE, SOME p), _) = p
       | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
     and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;

           | [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 (str o deresolv) c
         :: ((map (pr_insts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
-    and pr_app vars fxy (app as ((c, (iss, ty)), ts)) =
-      gen_pr_app (pr_app' vars) (fn vars' => pr_term (CodegenNames.intro_vars vars' vars))
-        const_syntax fxy app
+    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
       | pr_bind' ((NONE, SOME p), _) = p
       | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
     and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;

   end;
 
 
 (** Haskell serializer **)
 
+local
+
+fun pr_bind' ((NONE, NONE), _) = str "_"
+  | pr_bind' ((SOME v, NONE), _) = str v
+  | pr_bind' ((NONE, SOME p), _) = p
+  | pr_bind' ((SOME v, SOME p), _) = brackets [str v, str "@", p]
+
+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 =
   let
     fun class_name class = case class_syntax class
      of NONE => deresolv class
       | SOME (class, _) => class;

               str "})"
             ) (map pr bs)
           end
     and pr_app' vars ((c, _), ts) =
       (str o deresolv) c :: map (pr_term vars BR) ts
-    and pr_app vars fxy =
-      gen_pr_app (pr_app' vars) (fn vars' => pr_term (CodegenNames.intro_vars vars' vars))
-        const_syntax fxy
-    and pr_bind' ((NONE, NONE), _) = str "_"
-      | pr_bind' ((SOME v, NONE), _) = str v
-      | pr_bind' ((NONE, SOME p), _) = p
-      | pr_bind' ((SOME v, SOME p), _) = brackets [str v, str "@", p]
-    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;
+    and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
+    and pr_bind fxy = pr_bind_haskell pr_term fxy;
     fun pr_def (name, CodegenThingol.Fun (eqs, (vs, ty))) =
           let
             val tyvars = CodegenNames.intro_vars (map fst vs) keyword_vars;
             fun pr_eq (ts, t) =
               let

               ],
               str "};"
             ) (map pr_instdef classop_defs)
           end;
   in pr_def def end;
+
+fun pretty_haskell_monad c_mbind c_kbind =
+  let
+    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
+              |> pr_bind NOBR bind
+              |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
+          | pr_mbind (SOME (bind, false), t) vars = vars
+              |> pr_bind NOBR bind
+              |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
+        val (binds, t) = implode_monad c_mbind c_kbind t;
+        val (ps, vars') = fold_map pr_mbind binds vars;
+        fun brack p = if eval_fxy BR fxy then Pretty.block [str "(", p, str ")"] else p;
+      in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
+  in (1, pretty) end;
+
+end; (*local*)
 
 val reserved_haskell = [
   "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"

   in
     thy
     |> (CodegenSerializerData.map o Symtab.map_entry target o map_target) f
   end;
 
+val target_SML = "SML";
+val target_OCaml = "OCaml";
+val target_Haskell = "Haskell";
 val target_diag = "diag";
 
 val _ = Context.add_setup (
   CodegenSerializerData.init
-  #> add_serializer ("SML", isar_seri_sml)
-  #> add_serializer ("OCaml", isar_seri_ocaml)
-  #> add_serializer ("Haskell", isar_seri_haskell)
+  #> add_serializer (target_SML, isar_seri_sml)
+  #> 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 =>
   let

     val tyco = Sign.intern_type thy raw_tyco;
     val _ = if Sign.declared_tyname thy tyco then ()
       else error ("No such type constructor: " ^ quote raw_tyco);
   in tyco end;
 
-fun idfs_of_const_names thy c =
+fun idfs_of_const thy c =
   let
     val c' = (c, Sign.the_const_type thy c);
     val c'' = CodegenConsts.norm_of_typ thy c';
   in (c'', CodegenNames.const thy c'') end;
+
+fun gen_add_haskell_monad prep_const c_run c_mbind c_kbind thy =
+  let
+    val c_run' =
+      (CodegenConsts.norm thy o prep_const thy) c_run;
+    val c_mbind'' =
+      (CodegenNames.const thy o CodegenConsts.norm thy o prep_const thy) c_mbind;
+    val c_kbind'' =
+      (CodegenNames.const thy o CodegenConsts.norm thy o prep_const thy) c_kbind;
+    val pr = pretty_haskell_monad c_mbind'' c_kbind''
+  in
+    thy
+    |> gen_add_syntax_const (K I) target_Haskell c_run' (SOME pr)
+  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;
 val add_syntax_const = gen_add_syntax_const CodegenConsts.read_const;

   P.and_list1 parse_thing
   #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
         (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
 
 fun no_bindings x = (Option.map o apsnd)
-  (fn pretty => fn pr => pretty (pr [])) x;
+  (fn pretty => fn pr => fn vars => pretty (pr vars)) x;
 
 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
 
 fun parse_syntax xs =
   Scan.option ((

 
 in
 
 fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy =
   let
-    val (_, nil'') = idfs_of_const_names thy nill;
-    val (cons', cons'') = idfs_of_const_names thy cons;
+    val (_, nil'') = idfs_of_const thy nill;
+    val (cons', cons'') = idfs_of_const thy cons;
     val pr = pretty_list nil'' cons'' mk_list mk_char_string target_cons;
   in
     thy
     |> gen_add_syntax_const (K I) target cons' (SOME pr)
   end;
 
 fun add_pretty_ml_string target nill cons str mk_char mk_string target_implode thy =
   let
-    val (_, nil'') = idfs_of_const_names thy nill;
-    val (_, cons'') = idfs_of_const_names thy cons;
-    val (str', _) = idfs_of_const_names thy str;
+    val (_, nil'') = idfs_of_const thy nill;
+    val (_, cons'') = idfs_of_const thy cons;
+    val (str', _) = idfs_of_const thy str;
     val pr = pretty_ml_string nil'' cons'' mk_char mk_string target_implode;
   in
     thy
     |> gen_add_syntax_const (K I) target str' (SOME pr)
   end;
 
 fun add_undefined target undef target_undefined thy =
   let
-    val (undef', _) = idfs_of_const_names thy undef;
-    fun pr _ _ _ = str target_undefined;
+    val (undef', _) = idfs_of_const thy undef;
+    fun pr _ _ _ _ = str target_undefined;
   in
     thy
     |> gen_add_syntax_const (K I) target undef' (SOME (~1, pr))
   end;
 
 fun add_pretty_imperative_monad_bind target bind thy =
   let
-    val (bind', _) = idfs_of_const_names thy bind;
+    val (bind', _) = idfs_of_const thy bind;
     val pr = pretty_imperative_monad_bind
   in
     thy
     |> gen_add_syntax_const (K I) target bind' (SOME pr)
   end;
+
+val add_haskell_monad = gen_add_haskell_monad CodegenConsts.read_const;
 
 val code_classP =
   OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
     parse_multi_syntax P.xname
       (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1

     parse_multi_syntax P.term parse_syntax
     >> (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 =
-  OuterSyntax.command code_typeK "define code syntax for Haskell monads" K.thy_decl (
-    parse_multi_syntax P.xname parse_syntax
-    >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_tyco, syn) => add_syntax_monad target raw_tyco syn) syns)
-  );*)
+val code_monadP =
+  OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl (
+    P.term -- P.term -- P.term
+    >> (fn ((raw_run, raw_mbind), raw_kbind) => Toplevel.theory 
+          (add_haskell_monad raw_run raw_mbind raw_kbind))
+  );
 
 val code_reservedP =
   OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl (
     P.name -- Scan.repeat1 P.name
     >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)

   )
 
 val _ = OuterSyntax.add_keywords [infixK, infixlK, infixrK];
 
 val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP,
-  code_reservedP, code_modulenameP, code_moduleprologP];
+  code_reservedP, code_modulenameP, code_moduleprologP, code_monadP];
 
 (*including serializer defaults*)
 val _ = Context.add_setup (
   gen_add_syntax_tyco (K I) "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
       (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [