# HG changeset patch
# User haftmann
# Date 1258035027 -3600
# Node ID a9bb3f0637739cfa9b699c71d48e07975a8229eb
# Parent  dcaada178c6f8012aa6a3d8e4358af195aa92a58
accomplish mutual recursion between fun and inst

diff -r dcaada178c6f -r a9bb3f063773 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Nov 12 15:10:24 2009 +0100
+++ b/src/Tools/Code/code_ml.ML	Thu Nov 12 15:10:27 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Tools/code/code_ml.ML
+(*  Title:      Tools/code/code_ml.ML_
     Author:     Florian Haftmann, TU Muenchen
 
 Serializer for SML and OCaml.
@@ -25,29 +25,34 @@
 val target_OCaml = "OCaml";
 val target_Eval = "Eval";
 
-datatype ml_stmt =
-    MLExc of string * int
-  | MLVal of string * ((typscheme * iterm) * (thm * bool))
-  | MLFuns of (string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)) list * string list
-  | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
-  | MLClass of string * (vname * ((class * string) list * (string * itype) list))
-  | MLClassinst of string * ((class * (string * (vname * sort) list))
+datatype ml_binding =
+    ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
+  | ML_Instance of string * ((class * (string * (vname * sort) list))
         * ((class * (string * (string * dict list list))) list
       * ((string * const) * (thm * bool)) list));
 
-fun stmt_names_of (MLExc (name, _)) = [name]
-  | stmt_names_of (MLVal (name, _)) = [name]
-  | stmt_names_of (MLFuns (fs, _)) = map fst fs
-  | stmt_names_of (MLDatas ds) = map fst ds
-  | stmt_names_of (MLClass (name, _)) = [name]
-  | stmt_names_of (MLClassinst (name, _)) = [name];
+datatype ml_stmt =
+    ML_Exc of string * int
+  | ML_Val of ml_binding
+  | ML_Funs of ml_binding list * string list
+  | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
+  | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
+
+fun stmt_name_of_binding (ML_Function (name, _)) = name
+  | stmt_name_of_binding (ML_Instance (name, _)) = name;
+
+fun stmt_names_of (ML_Exc (name, _)) = [name]
+  | stmt_names_of (ML_Val binding) = [stmt_name_of_binding binding]
+  | stmt_names_of (ML_Funs (bindings, _)) = map stmt_name_of_binding bindings
+  | stmt_names_of (ML_Datas ds) = map fst ds
+  | stmt_names_of (ML_Class (name, _)) = [name];
 
 
 (** SML serailizer **)
 
 fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
   let
-    fun pr_dicts fxy ds =
+    fun pr_dicts is_pseudo_fun fxy ds =
       let
         fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
           | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
@@ -58,7 +63,9 @@
           | pr_proj (ps as _ :: _) p =
               brackets [Pretty.enum " o" "(" ")" ps, p];
         fun pr_dict fxy (DictConst (inst, dss)) =
-              brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
+              brackify fxy ((str o deresolve) inst ::
+                (if is_pseudo_fun inst then [str "()"]
+                else map (pr_dicts is_pseudo_fun BR) dss))
           | pr_dict fxy (DictVar (classrels, v)) =
               pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
       in case ds
@@ -66,11 +73,11 @@
         | [d] => pr_dict fxy d
         | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
       end;
-    fun pr_tyvar_dicts vs =
+    fun pr_tyvar_dicts is_pseudo_fun vs =
       vs
       |> map (fn (v, sort) => map_index (fn (i, _) =>
            DictVar ([], (v, (i, length sort)))) sort)
-      |> map (pr_dicts BR);
+      |> map (pr_dicts is_pseudo_fun BR);
     fun pr_tycoexpr fxy (tyco, tys) =
       let
         val tyco' = (str o deresolve) tyco
@@ -83,144 +90,155 @@
          of NONE => pr_tycoexpr fxy (tyco, tys)
           | SOME (i, pr) => pr pr_typ fxy tys)
       | pr_typ fxy (ITyVar v) = str ("'" ^ v);
-    fun pr_term is_closure thm vars fxy (IConst c) =
-          pr_app is_closure thm vars fxy (c, [])
-      | pr_term is_closure thm vars fxy (IVar NONE) =
+    fun pr_term is_pseudo_fun thm vars fxy (IConst c) =
+          pr_app is_pseudo_fun thm vars fxy (c, [])
+      | pr_term is_pseudo_fun thm vars fxy (IVar NONE) =
           str "_"
-      | pr_term is_closure thm vars fxy (IVar (SOME v)) =
+      | pr_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
           str (lookup_var vars v)
-      | pr_term is_closure thm vars fxy (t as t1 `$ t2) =
+      | pr_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
-           of SOME c_ts => pr_app is_closure thm vars fxy c_ts
+           of SOME c_ts => pr_app is_pseudo_fun thm vars fxy c_ts
             | NONE => brackify fxy
-               [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
-      | pr_term is_closure thm vars fxy (t as _ `|=> _) =
+               [pr_term is_pseudo_fun thm vars NOBR t1, pr_term is_pseudo_fun thm vars BR t2])
+      | pr_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
           let
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
             fun pr (pat, ty) =
-              pr_bind is_closure thm NOBR pat
+              pr_bind is_pseudo_fun thm NOBR pat
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map pr binds vars;
-          in brackets (ps @ [pr_term is_closure thm vars' NOBR t']) end
-      | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) =
+          in brackets (ps @ [pr_term is_pseudo_fun thm vars' NOBR t']) end
+      | pr_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
           (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
-                then pr_case is_closure thm vars fxy cases
-                else pr_app is_closure thm vars fxy c_ts
-            | NONE => pr_case is_closure thm vars fxy cases)
-    and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) =
+                then pr_case is_pseudo_fun thm vars fxy cases
+                else pr_app is_pseudo_fun thm vars fxy c_ts
+            | NONE => pr_case is_pseudo_fun thm vars fxy cases)
+    and pr_app' is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
       if is_cons c then
         let
           val k = length tys
         in if k < 2 then 
-          (str o deresolve) c :: map (pr_term is_closure thm vars BR) ts
+          (str o deresolve) c :: map (pr_term is_pseudo_fun thm vars BR) ts
         else if k = length ts then
-          [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term is_closure thm vars NOBR) ts)]
-        else [pr_term is_closure thm vars BR (Code_Thingol.eta_expand k app)] end
-      else if is_closure c
+          [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term is_pseudo_fun thm vars NOBR) ts)]
+        else [pr_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)] end
+      else if is_pseudo_fun c
         then (str o deresolve) c @@ str "()"
       else
         (str o deresolve) c
-          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
-    and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
+          :: (map (pr_dicts is_pseudo_fun BR) o filter_out null) iss @ map (pr_term is_pseudo_fun thm vars BR) ts
+    and pr_app is_pseudo_fun thm vars = gen_pr_app (pr_app' is_pseudo_fun) (pr_term is_pseudo_fun)
       syntax_const thm vars
-    and pr_bind is_closure = gen_pr_bind (pr_term is_closure)
-    and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
+    and pr_bind is_pseudo_fun = gen_pr_bind (pr_term is_pseudo_fun)
+    and pr_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind is_closure thm NOBR pat
-              |>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t])
+              |> pr_bind is_pseudo_fun thm NOBR pat
+              |>> (fn p => semicolon [str "val", p, str "=", pr_term is_pseudo_fun thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in
             Pretty.chunks [
               [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
-              [str ("in"), Pretty.fbrk, pr_term is_closure thm vars' NOBR body] |> Pretty.block,
+              [str ("in"), Pretty.fbrk, pr_term is_pseudo_fun thm vars' NOBR body] |> Pretty.block,
               str ("end")
             ]
           end
-      | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
+      | pr_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR pat vars;
+                val (p, vars') = pr_bind is_pseudo_fun thm NOBR pat vars;
               in
-                concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
+                concat [str delim, p, str "=>", pr_term is_pseudo_fun thm vars' NOBR body]
               end;
           in
             brackets (
               str "case"
-              :: pr_term is_closure thm vars NOBR t
+              :: pr_term is_pseudo_fun thm vars NOBR t
               :: pr "of" clause
               :: map (pr "|") clauses
             )
           end
-      | pr_case is_closure thm vars fxy ((_, []), _) =
+      | pr_case is_pseudo_fun thm vars fxy ((_, []), _) =
           (concat o map str) ["raise", "Fail", "\"empty case\""];
-    fun pr_stmt (MLExc (name, n)) =
+    fun pr_binding is_pseudo_fun needs_typ definer (ML_Function (name, ((vs, ty), eqs as eq :: eqs'))) =
           let
-            val exc_str =
-              (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
+            val vs_dict = filter_out (null o snd) vs;
+            val shift = if null eqs' then I else
+              map (Pretty.block o single o Pretty.block o single);
+            fun pr_eq definer ((ts, t), (thm, _)) =
+              let
+                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
+                val vars = reserved
+                  |> intro_base_names
+                       (is_none o syntax_const) deresolve consts
+                  |> intro_vars ((fold o Code_Thingol.fold_varnames)
+                       (insert (op =)) ts []);
+                val prolog = if needs_typ then
+                  concat [str definer, (str o deresolve) name, str ":", pr_typ NOBR ty]
+                    else Pretty.strs [definer, deresolve name];
+              in
+                concat (
+                  prolog
+                  :: (if is_pseudo_fun name then [str "()"]
+                      else pr_tyvar_dicts is_pseudo_fun vs_dict
+                        @ map (pr_term is_pseudo_fun thm vars BR) ts)
+                  @ str "="
+                  @@ pr_term is_pseudo_fun thm vars NOBR t
+                )
+              end
           in
-            (concat o map str) (
-              (if n = 0 then "val" else "fun")
-              :: deresolve name
-              :: replicate n "_"
-              @ "="
-              :: "raise"
-              :: "Fail"
-              @@ exc_str
+            (Pretty.block o Pretty.fbreaks o shift) (
+              pr_eq definer eq
+              :: map (pr_eq "|") eqs'
             )
           end
-      | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
-          let
-            val consts = Code_Thingol.add_constnames t [];
-            val vars = reserved
-              |> intro_base_names
-                  (is_none o syntax_const) deresolve consts;
-          in
-            concat [
-              str "val",
-              (str o deresolve) name,
-              str ":",
-              pr_typ NOBR ty,
-              str "=",
-              pr_term (K false) thm vars NOBR t
-            ]
-          end
-      | pr_stmt (MLFuns (funn :: funns, pseudo_funs)) =
+      | pr_binding is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
           let
-            fun pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
-              let
-                val vs_dict = filter_out (null o snd) vs;
-                val shift = if null eqs' then I else
-                  map (Pretty.block o single o Pretty.block o single);
-                fun pr_eq definer ((ts, t), (thm, _)) =
-                  let
-                    val consts = fold Code_Thingol.add_constnames (t :: ts) [];
-                    val vars = reserved
-                      |> intro_base_names
-                           (is_none o syntax_const) deresolve consts
-                      |> intro_vars ((fold o Code_Thingol.fold_varnames)
-                           (insert (op =)) ts []);
-                  in
-                    concat (
-                      str definer
-                      :: (str o deresolve) name
-                      :: (if member (op =) pseudo_funs name then [str "()"]
-                          else pr_tyvar_dicts vs_dict
-                            @ map (pr_term (member (op =) pseudo_funs) thm vars BR) ts)
-                      @ str "="
-                      @@ pr_term (member (op =) pseudo_funs) thm vars NOBR t
-                    )
-                  end
-              in
-                (Pretty.block o Pretty.fbreaks o shift) (
-                  pr_eq definer eq
-                  :: map (pr_eq "|") eqs'
-                )
-              end;
+            fun pr_superclass (_, (classrel, dss)) =
+              concat [
+                (str o Long_Name.base_name o deresolve) classrel,
+                str "=",
+                pr_dicts is_pseudo_fun NOBR [DictConst dss]
+              ];
+            fun pr_classparam ((classparam, c_inst), (thm, _)) =
+              concat [
+                (str o Long_Name.base_name o deresolve) classparam,
+                str "=",
+                pr_app (K false) thm reserved NOBR (c_inst, [])
+              ];
+          in
+            concat (
+              str definer
+              :: (str o deresolve) inst
+              :: (if is_pseudo_fun inst then [str "()"]
+                  else pr_tyvar_dicts is_pseudo_fun arity)
+              @ str "="
+              :: Pretty.enum "," "{" "}"
+                (map pr_superclass superarities @ map pr_classparam classparam_insts)
+              :: str ":"
+              @@ pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
+            )
+          end;
+    fun pr_stmt (ML_Exc (name, n)) =
+          (concat o map str) (
+            (if n = 0 then "val" else "fun")
+            :: deresolve name
+            :: replicate n "_"
+            @ "="
+            :: "raise"
+            :: "Fail"
+            @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name ^ ";"
+          )
+      | pr_stmt (ML_Val binding) =
+          semicolon [pr_binding (K false) true "val" binding]
+      | pr_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
+          let
+            val pr_binding' = pr_binding (member (op =) pseudo_funs) false;
             fun pr_pseudo_fun name = concat [
                 str "val",
                 (str o deresolve) name,
@@ -228,10 +246,11 @@
                 (str o deresolve) name,
                 str "();"
               ];
-            val (ps, p) = split_last (pr_funn "fun" funn :: map (pr_funn "and") funns);
+            val (ps, p) = split_last
+              (pr_binding' "fun" binding :: map (pr_binding' "and") bindings);
             val pseudo_ps = map pr_pseudo_fun pseudo_funs;
           in Pretty.chunks (ps @ Pretty.block ([p, str ";"]) :: pseudo_ps) end
-     | pr_stmt (MLDatas (datas as (data :: datas'))) =
+     | pr_stmt (ML_Datas (datas as (data :: datas'))) =
           let
             fun pr_co (co, []) =
                   str (deresolve co)
@@ -258,7 +277,7 @@
             val (ps, p) = split_last
               (pr_data "datatype" data :: map (pr_data "and") datas');
           in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end
-     | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
+     | pr_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
           let
             val w = first_upper v ^ "_";
             fun pr_superclass_field (class, classrel) =
@@ -300,32 +319,6 @@
               :: map pr_superclass_proj superclasses
               @ map pr_classparam_proj classparams
             )
-          end
-     | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
-          let
-            fun pr_superclass (_, (classrel, dss)) =
-              concat [
-                (str o Long_Name.base_name o deresolve) classrel,
-                str "=",
-                pr_dicts NOBR [DictConst dss]
-              ];
-            fun pr_classparam ((classparam, c_inst), (thm, _)) =
-              concat [
-                (str o Long_Name.base_name o deresolve) classparam,
-                str "=",
-                pr_app (K false) thm reserved NOBR (c_inst, [])
-              ];
-          in
-            semicolon ([
-              str (if null arity then "val" else "fun"),
-              (str o deresolve) inst ] @
-              pr_tyvar_dicts arity @ [
-              str "=",
-              Pretty.enum "," "{" "}"
-                (map pr_superclass superarities @ map pr_classparam classparam_insts),
-              str ":",
-              pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
-            ])
           end;
   in pr_stmt end;
 
@@ -354,14 +347,16 @@
 
 fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
   let
-    fun pr_dicts fxy ds =
+    fun pr_dicts is_pseudo_fun fxy ds =
       let
         fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
           | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
         fun pr_proj ps p =
           fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
         fun pr_dict fxy (DictConst (inst, dss)) =
-              brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
+              brackify fxy ((str o deresolve) inst ::
+                (if is_pseudo_fun inst then [str "()"]
+                else map (pr_dicts is_pseudo_fun BR) dss))
           | pr_dict fxy (DictVar (classrels, v)) =
               pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
       in case ds
@@ -369,11 +364,11 @@
         | [d] => pr_dict fxy d
         | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
       end;
-    fun pr_tyvar_dicts vs =
+    fun pr_tyvar_dicts is_pseudo_fun vs =
       vs
       |> map (fn (v, sort) => map_index (fn (i, _) =>
            DictVar ([], (v, (i, length sort)))) sort)
-      |> map (pr_dicts BR);
+      |> map (pr_dicts is_pseudo_fun BR);
     fun pr_tycoexpr fxy (tyco, tys) =
       let
         val tyco' = (str o deresolve) tyco
@@ -386,103 +381,73 @@
          of NONE => pr_tycoexpr fxy (tyco, tys)
           | SOME (i, pr) => pr pr_typ fxy tys)
       | pr_typ fxy (ITyVar v) = str ("'" ^ v);
-    fun pr_term is_closure thm vars fxy (IConst c) =
-          pr_app is_closure thm vars fxy (c, [])
-      | pr_term is_closure thm vars fxy (IVar NONE) =
+    fun pr_term is_pseudo_fun thm vars fxy (IConst c) =
+          pr_app is_pseudo_fun thm vars fxy (c, [])
+      | pr_term is_pseudo_fun thm vars fxy (IVar NONE) =
           str "_"
-      | pr_term is_closure thm vars fxy (IVar (SOME v)) =
+      | pr_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
           str (lookup_var vars v)
-      | pr_term is_closure thm vars fxy (t as t1 `$ t2) =
+      | pr_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
-           of SOME c_ts => pr_app is_closure thm vars fxy c_ts
+           of SOME c_ts => pr_app is_pseudo_fun thm vars fxy c_ts
             | NONE =>
-                brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
-      | pr_term is_closure thm vars fxy (t as _ `|=> _) =
+                brackify fxy [pr_term is_pseudo_fun thm vars NOBR t1, pr_term is_pseudo_fun thm vars BR t2])
+      | pr_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
           let
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
-            val (ps, vars') = fold_map (pr_bind is_closure thm BR o fst) binds vars;
-          in brackets (str "fun" :: ps @ str "->" @@ pr_term is_closure thm vars' NOBR t') end
-      | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
+            val (ps, vars') = fold_map (pr_bind is_pseudo_fun thm BR o fst) binds vars;
+          in brackets (str "fun" :: ps @ str "->" @@ pr_term is_pseudo_fun thm vars' NOBR t') end
+      | pr_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
-                then pr_case is_closure thm vars fxy cases
-                else pr_app is_closure thm vars fxy c_ts
-            | NONE => pr_case is_closure thm vars fxy cases)
-    and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) =
+                then pr_case is_pseudo_fun thm vars fxy cases
+                else pr_app is_pseudo_fun thm vars fxy c_ts
+            | NONE => pr_case is_pseudo_fun thm vars fxy cases)
+    and pr_app' is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
       if is_cons c then
         if length tys = length ts
         then case ts
          of [] => [(str o deresolve) c]
-          | [t] => [(str o deresolve) c, pr_term is_closure thm vars BR t]
+          | [t] => [(str o deresolve) c, pr_term is_pseudo_fun thm vars BR t]
           | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
-                    (map (pr_term is_closure thm vars NOBR) ts)]
-        else [pr_term is_closure thm vars BR (Code_Thingol.eta_expand (length tys) app)]
-      else if is_closure c
+                    (map (pr_term is_pseudo_fun thm vars NOBR) ts)]
+        else [pr_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand (length tys) app)]
+      else if is_pseudo_fun c
         then (str o deresolve) c @@ str "()"
       else (str o deresolve) c
-        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
-    and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
+        :: ((map (pr_dicts is_pseudo_fun BR) o filter_out null) iss @ map (pr_term is_pseudo_fun thm vars BR) ts)
+    and pr_app is_pseudo_fun = gen_pr_app (pr_app' is_pseudo_fun) (pr_term is_pseudo_fun)
       syntax_const
-    and pr_bind is_closure = gen_pr_bind (pr_term is_closure)
-    and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
+    and pr_bind is_pseudo_fun = gen_pr_bind (pr_term is_pseudo_fun)
+    and pr_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind is_closure thm NOBR pat
+              |> pr_bind is_pseudo_fun thm NOBR pat
               |>> (fn p => concat
-                  [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
+                  [str "let", p, str "=", pr_term is_pseudo_fun thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
           in
             brackify_block fxy (Pretty.chunks ps) []
-              (pr_term is_closure thm vars' NOBR body)
+              (pr_term is_pseudo_fun thm vars' NOBR body)
           end
-      | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
+      | pr_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR pat vars;
-              in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
+                val (p, vars') = pr_bind is_pseudo_fun thm NOBR pat vars;
+              in concat [str delim, p, str "->", pr_term is_pseudo_fun thm vars' NOBR body] end;
           in
             brackets (
               str "match"
-              :: pr_term is_closure thm vars NOBR t
+              :: pr_term is_pseudo_fun thm vars NOBR t
               :: pr "with" clause
               :: map (pr "|") clauses
             )
           end
-      | pr_case is_closure thm vars fxy ((_, []), _) =
+      | pr_case is_pseudo_fun thm vars fxy ((_, []), _) =
           (concat o map str) ["failwith", "\"empty case\""];
-    fun pr_stmt (MLExc (name, n)) =
-          let
-            val exc_str =
-              (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
-          in
-            (concat o map str) (
-              "let"
-              :: deresolve name
-              :: replicate n "_"
-              @ "="
-              :: "failwith"
-              @@ exc_str
-            )
-          end
-      | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
-          let
-            val consts = Code_Thingol.add_constnames t [];
-            val vars = reserved
-              |> intro_base_names
-                  (is_none o syntax_const) deresolve consts;
-          in
-            concat [
-              str "let",
-              (str o deresolve) name,
-              str ":",
-              pr_typ NOBR ty,
-              str "=",
-              pr_term (K false) thm vars NOBR t
-            ]
-          end
-      | pr_stmt (MLFuns (funn :: funns, pseudo_funs)) =
+    fun pr_binding is_pseudo_fun needs_typ definer (ML_Function (name, ((vs, ty), eqs))) =
           let
             fun pr_eq ((ts, t), (thm, _)) =
               let
@@ -494,9 +459,9 @@
                       (insert (op =)) ts []);
               in concat [
                 (Pretty.block o Pretty.commas)
-                  (map (pr_term (member (op =) pseudo_funs) thm vars NOBR) ts),
+                  (map (pr_term is_pseudo_fun thm vars NOBR) ts),
                 str "->",
-                pr_term (member (op =) pseudo_funs) thm vars NOBR t
+                pr_term is_pseudo_fun thm vars NOBR t
               ] end;
             fun pr_eqs is_pseudo [((ts, t), (thm, _))] =
                   let
@@ -509,9 +474,9 @@
                   in
                     concat (
                       (if is_pseudo then [str "()"]
-                        else map (pr_term (member (op =) pseudo_funs) thm vars BR) ts)
+                        else map (pr_term is_pseudo_fun thm vars BR) ts)
                       @ str "="
-                      @@ pr_term (member (op =) pseudo_funs) thm vars NOBR t
+                      @@ pr_term is_pseudo_fun thm vars NOBR t
                     )
                   end
               | pr_eqs _ (eqs as (eq as (([_], _), _)) :: eqs') =
@@ -548,13 +513,58 @@
                            o single o pr_eq) eqs'
                     )
                   end;
-            fun pr_funn definer (name, ((vs, ty), eqs)) =
-              concat (
-                str definer
-                :: (str o deresolve) name
-                :: pr_tyvar_dicts (filter_out (null o snd) vs)
-                @| pr_eqs (member (op =) pseudo_funs name) eqs
-              );
+            val prolog = if needs_typ then
+              concat [str definer, (str o deresolve) name, str ":", pr_typ NOBR ty]
+                else Pretty.strs [definer, deresolve name];
+          in
+            concat (
+              prolog
+              :: pr_tyvar_dicts is_pseudo_fun (filter_out (null o snd) vs)
+              @| pr_eqs (is_pseudo_fun name) eqs
+            )
+          end
+      | pr_binding is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
+          let
+            fun pr_superclass (_, (classrel, dss)) =
+              concat [
+                (str o deresolve) classrel,
+                str "=",
+                pr_dicts is_pseudo_fun NOBR [DictConst dss]
+              ];
+            fun pr_classparam_inst ((classparam, c_inst), (thm, _)) =
+              concat [
+                (str o deresolve) classparam,
+                str "=",
+                pr_app (K false) thm reserved NOBR (c_inst, [])
+              ];
+          in
+            concat (
+              str definer
+              :: (str o deresolve) inst
+              :: pr_tyvar_dicts is_pseudo_fun arity
+              @ str "="
+              @@ brackets [
+                enum_default "()" ";" "{" "}" (map pr_superclass superarities
+                  @ map pr_classparam_inst classparam_insts),
+                str ":",
+                pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
+              ]
+            )
+          end;
+     fun pr_stmt (ML_Exc (name, n)) =
+          (concat o map str) (
+            "let"
+            :: deresolve name
+            :: replicate n "_"
+            @ "="
+            :: "failwith"
+            @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name ^ ";;"
+          )
+      | pr_stmt (ML_Val binding) =
+           Pretty.block [pr_binding (K false) true "let" binding, str ";;"]
+      | pr_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
+          let
+            val pr_binding' = pr_binding (member (op =) pseudo_funs) false;
             fun pr_pseudo_fun name = concat [
                 str "let",
                 (str o deresolve) name,
@@ -563,10 +573,10 @@
                 str "();;"
               ];
             val (ps, p) = split_last
-              (pr_funn "let rec" funn :: map (pr_funn "and") funns);
+              (pr_binding' "let rec" binding :: map (pr_binding' "and") bindings);
             val pseudo_ps = map pr_pseudo_fun pseudo_funs;
           in Pretty.chunks (ps @ Pretty.block ([p, str ";;"]) :: pseudo_ps) end
-     | pr_stmt (MLDatas (datas as (data :: datas'))) =
+     | pr_stmt (ML_Datas (datas as (data :: datas'))) =
           let
             fun pr_co (co, []) =
                   str (deresolve co)
@@ -593,7 +603,7 @@
             val (ps, p) = split_last
               (pr_data "type" data :: map (pr_data "and") datas');
           in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end
-     | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
+     | pr_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
           let
             val w = "_" ^ first_upper v;
             fun pr_superclass_field (class, classrel) =
@@ -623,36 +633,8 @@
               )
             ]
             :: map pr_classparam_proj classparams
-          ) end
-     | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
-          let
-            fun pr_superclass (_, (classrel, dss)) =
-              concat [
-                (str o deresolve) classrel,
-                str "=",
-                pr_dicts NOBR [DictConst dss]
-              ];
-            fun pr_classparam_inst ((classparam, c_inst), (thm, _)) =
-              concat [
-                (str o deresolve) classparam,
-                str "=",
-                pr_app (K false) thm reserved NOBR (c_inst, [])
-              ];
-          in
-            concat (
-              str "let"
-              :: (str o deresolve) inst
-              :: pr_tyvar_dicts arity
-              @ str "="
-              @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
-                enum_default "()" ";" "{" "}" (map pr_superclass superarities
-                  @ map pr_classparam_inst classparam_insts),
-                str ":",
-                pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
-              ]
-            )
-          end;
-  in pr_stmt end;
+          ) end;
+ in pr_stmt end;
 
 fun pr_ocaml_module name content =
   Pretty.chunks (
@@ -744,32 +726,41 @@
         val base' = if upper then first_upper base else base;
         val ([base''], nsp') = Name.variants [base'] nsp;
       in (base'', nsp') end;
-    fun rearrange_fun name (tysm as (vs, ty), raw_eqs) =
+    fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) =
+          let
+            val eqs = filter (snd o snd) raw_eqs;
+            val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
+               of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
+                  then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], NONE)
+                  else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
+                | _ => (eqs, NONE)
+              else (eqs, NONE)
+          in (ML_Function (name, (tysm, eqs')), is_value) end
+      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, arity)), _))) =
+          (ML_Instance (name, stmt), if null arity then SOME (name, false) else NONE)
+      | ml_binding_of_stmt (name, _) =
+          error ("Binding block containing illegal statement: " ^ labelled_name name)
+    fun add_fun (name, stmt) =
       let
-        val eqs = filter (snd o snd) raw_eqs;
-        val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
-         of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
-            then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], false)
-            else (eqs, not (member (op =) (Code_Thingol.add_constnames t []) name))
-          | _ => (eqs, false)
-          else (eqs, false)
-      in ((name, (tysm, eqs')), is_value) end;
-    fun check_kind [((name, (tysm, [(([], t), thm)])), true)] = MLVal (name, ((tysm, t), thm))
-      | check_kind [((name, ((vs, ty), [])), _)] =
-          MLExc (name, (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)
-      | check_kind funns =
-          MLFuns (map fst funns, map_filter
-            (fn ((name, ((vs, _), [(([], _), _)])), _) =>
-                  if null (filter_out (null o snd) vs) then SOME name else NONE
-              | _ => NONE) funns);
-    fun add_funs stmts = fold_map
-        (fn (name, Code_Thingol.Fun (_, stmt)) =>
-              map_nsp_fun_yield (mk_name_stmt false name)
-              #>> rpair (rearrange_fun name stmt)
-          | (name, _) =>
-              error ("Function block containing illegal statement: " ^ labelled_name name)
-        ) stmts
-      #>> (split_list #> apsnd check_kind);
+        val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
+        val ml_stmt = case binding
+         of ML_Function (name, ((vs, ty), [])) =>
+              ML_Exc (name, (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)
+          | _ => case some_value_name
+             of NONE => ML_Funs ([binding], [])
+              | SOME (name, true) => ML_Funs ([binding], [name])
+              | SOME (name, false) => ML_Val binding
+      in
+        map_nsp_fun_yield (mk_name_stmt false name)
+        #>> (fn name' => ([name'], ml_stmt))
+      end;
+    fun add_funs stmts =
+      let
+        val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst);
+      in
+        fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts
+        #>> rpair ml_stmt
+      end;
     fun add_datatypes stmts =
       fold_map
         (fn (name, Code_Thingol.Datatype (_, stmt)) =>
@@ -782,7 +773,7 @@
       #>> (split_list #> apsnd (map_filter I
         #> (fn [] => error ("Datatype block without data statement: "
                   ^ (commas o map (labelled_name o fst)) stmts)
-             | stmts => MLDatas stmts)));
+             | stmts => ML_Datas stmts)));
     fun add_class stmts =
       fold_map
         (fn (name, Code_Thingol.Class (_, stmt)) =>
@@ -797,11 +788,10 @@
       #>> (split_list #> apsnd (map_filter I
         #> (fn [] => error ("Class block without class statement: "
                   ^ (commas o map (labelled_name o fst)) stmts)
-             | [stmt] => MLClass stmt)));
-    fun add_inst [(name, Code_Thingol.Classinst stmt)] =
-      map_nsp_fun_yield (mk_name_stmt false name)
-      #>> (fn base => ([base], MLClassinst (name, stmt)));
-    fun add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
+             | [stmt] => ML_Class stmt)));
+    fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
+          add_fun stmt
+      | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
           add_funs stmts
       | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
           add_datatypes stmts
@@ -813,8 +803,10 @@
           add_class stmts
       | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
           add_class stmts
-      | add_stmts ((stmts as [(_, Code_Thingol.Classinst _)])) =
-          add_inst stmts
+      | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
+          add_fun stmt
+      | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
+          add_funs stmts
       | add_stmts stmts = error ("Illegal mutual dependencies: " ^
           (commas o map (labelled_name o fst)) stmts);
     fun add_stmts' stmts nsp_nodes =