# HG changeset patch
# User haftmann
# Date 1255342759 -7200
# Node ID 9aa8dfef16ff71c13d689f8edd78c6f21eecb06b
# Parent  793c993c63aa4f0cba73a32214e398e28b03aaf2
factored out Code_Printer.aux_params

diff -r 793c993c63aa -r 9aa8dfef16ff src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Mon Oct 12 09:25:27 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Mon Oct 12 12:19:19 2009 +0200
@@ -456,19 +456,6 @@
           end
       | pr_case is_closure thm vars fxy ((_, []), _) =
           (concat o map str) ["failwith", "\"empty case\""];
-    fun fish_params vars eqs =
-      let
-        fun fish_param _ (w as SOME _) = w
-          | fish_param (IVar (SOME v)) NONE = SOME v
-          | fish_param _ NONE = NONE;
-        fun fillup_param _ (_, SOME v) = v
-          | fillup_param x (i, NONE) = x ^ string_of_int i;
-        val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);
-        val x = Name.variant (map_filter I fished1) "x";
-        val fished2 = map_index (fillup_param x) fished1;
-        val (fished3, _) = Name.variants fished2 Name.context;
-        val vars' = Code_Printer.intro_vars fished3 vars;
-      in map (Code_Printer.lookup_var vars') fished3 end;
     fun pr_stmt (MLExc (name, n)) =
           let
             val exc_str =
@@ -555,7 +542,7 @@
                         (fold Code_Thingol.add_constnames (map (snd o fst) eqs) []);
                     val vars = reserved_names
                       |> Code_Printer.intro_vars consts;
-                    val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
+                    val dummy_parms = (map str o Code_Printer.aux_params vars o map (fst o fst)) eqs;
                   in
                     Pretty.block (
                       Pretty.breaks dummy_parms
@@ -587,7 +574,6 @@
                 (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_funn "let rec" funn :: map (pr_funn "and") funns);
             val pseudo_ps = map pr_pseudo_fun pseudo_funs;
diff -r 793c993c63aa -r 9aa8dfef16ff src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Mon Oct 12 09:25:27 2009 +0200
+++ b/src/Tools/Code/code_printer.ML	Mon Oct 12 12:19:19 2009 +0200
@@ -6,6 +6,11 @@
 
 signature CODE_PRINTER =
 sig
+  type itype = Code_Thingol.itype
+  type iterm = Code_Thingol.iterm
+  type const = Code_Thingol.const
+  type dict = Code_Thingol.dict
+
   val nerror: thm -> string -> 'a
 
   val @@ : 'a * 'a -> 'a list
@@ -22,6 +27,7 @@
   val make_vars: string list -> var_ctxt
   val intro_vars: string list -> var_ctxt -> var_ctxt
   val lookup_var: var_ctxt -> string -> string
+  val aux_params: var_ctxt -> iterm list list -> string list
 
   type literals
   val Literals: { literal_char: string -> string, literal_string: string -> string,
@@ -47,10 +53,6 @@
   val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
   val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
 
-  type itype = Code_Thingol.itype
-  type iterm = Code_Thingol.iterm
-  type const = Code_Thingol.const
-  type dict = Code_Thingol.dict
   type tyco_syntax
   type const_syntax
   type proto_const_syntax
@@ -118,6 +120,20 @@
 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
 
+fun aux_params vars lhss =
+  let
+    fun fish_param _ (w as SOME _) = w
+      | fish_param (IVar (SOME v)) NONE = SOME v
+      | fish_param _ NONE = NONE;
+    fun fillup_param _ (_, SOME v) = v
+      | fillup_param x (i, NONE) = x ^ string_of_int i;
+    val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
+    val x = Name.variant (map_filter I fished1) "x";
+    val fished2 = map_index (fillup_param x) fished1;
+    val (fished3, _) = Name.variants fished2 Name.context;
+    val vars' = intro_vars fished3 vars;
+  in map (lookup_var vars') fished3 end;
+
 
 (** pretty literals **)