--- 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;
--- 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 **)