# HG changeset patch
# User haftmann
# Date 1255350174 -7200
# Node ID d61e303fc7e553612ccadaa91fb157bdd284b2a3
# Parent  0300f8dd63ea073e0088d0f66b862102ced531c7# Parent  bd72e72c3ee33b0cb8acae3437ba0cc4045e988b
merged

diff -r 0300f8dd63ea -r d61e303fc7e5 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Mon Oct 12 13:40:28 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Mon Oct 12 14:22:54 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 0300f8dd63ea -r d61e303fc7e5 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Mon Oct 12 13:40:28 2009 +0200
+++ b/src/Tools/Code/code_printer.ML	Mon Oct 12 14:22:54 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 **)
 
diff -r 0300f8dd63ea -r d61e303fc7e5 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Oct 12 13:40:28 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Oct 12 14:22:54 2009 +0200
@@ -46,6 +46,7 @@
   val split_pat_abs: iterm -> ((iterm * itype) * iterm) option
   val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
   val unfold_const_app: iterm -> (const * iterm list) option
+  val is_IVar: iterm -> bool
   val eta_expand: int -> const * iterm list -> iterm
   val contains_dictvar: iterm -> bool
   val locally_monomorphic: iterm -> bool
@@ -136,6 +137,9 @@
   | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
     (*see also signature*)
 
+fun is_IVar (IVar _) = true
+  | is_IVar _ = false;
+
 val op `$$ = Library.foldl (op `$);
 val op `|==> = Library.foldr (op `|=>);