# HG changeset patch
# User haftmann
# Date 1255514204 -7200
# Node ID d2e9b2dab760bc3ea639b44fa1593b3b3ac46073
# Parent  0b92e6359bc4ce894919c4a5805e7cca58b88b31
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology

diff -r 0b92e6359bc4 -r d2e9b2dab760 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Oct 13 14:57:53 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML	Wed Oct 14 11:56:44 2009 +0200
@@ -24,7 +24,7 @@
 (** Haskell serializer **)
 
 fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
-    init_syms deresolve contr_classparam_typs deriving_show =
+    reserved deresolve contr_classparam_typs deriving_show =
   let
     val deresolve_base = Long_Name.base_name o deresolve;
     fun class_name class = case syntax_class class
@@ -34,18 +34,18 @@
      of [] => []
       | classbinds => Pretty.enum "," "(" ")" (
           map (fn (v, class) =>
-            str (class_name class ^ " " ^ Code_Printer.lookup_var tyvars v)) classbinds)
+            str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds)
           @@ str " => ";
     fun pr_typforall tyvars vs = case map fst vs
      of [] => []
       | vnames => str "forall " :: Pretty.breaks
-          (map (str o Code_Printer.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
+          (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
     fun pr_tycoexpr tyvars fxy (tyco, tys) =
       brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
     and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
          of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
           | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
-      | pr_typ tyvars fxy (ITyVar v) = (str o Code_Printer.lookup_var tyvars) v;
+      | pr_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
     fun pr_typdecl tyvars (vs, tycoexpr) =
       Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
     fun pr_typscheme tyvars (vs, ty) =
@@ -63,7 +63,7 @@
       | pr_term tyvars thm vars fxy (IVar NONE) =
           str "_"
       | pr_term tyvars thm vars fxy (IVar (SOME v)) =
-          (str o Code_Printer.lookup_var vars) v
+          (str o lookup_var vars) v
       | pr_term tyvars thm vars fxy (t as _ `|=> _) =
           let
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
@@ -118,7 +118,7 @@
           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
     fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
           let
-            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+            val tyvars = intro_vars (map fst vs) reserved;
             val n = (length o fst o Code_Thingol.unfold_fun) ty;
           in
             Pretty.chunks [
@@ -141,14 +141,14 @@
       | pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
           let
             val eqs = filter (snd o snd) raw_eqs;
-            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+            val tyvars = intro_vars (map fst vs) reserved;
             fun pr_eq ((ts, t), (thm, _)) =
               let
                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
-                val vars = init_syms
-                  |> Code_Printer.intro_base_names
+                val vars = reserved
+                  |> intro_base_names
                       (is_none o syntax_const) deresolve consts
-                  |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
+                  |> intro_vars ((fold o Code_Thingol.fold_varnames)
                        (insert (op =)) ts []);
               in
                 semicolon (
@@ -171,7 +171,7 @@
           end
       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
           let
-            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+            val tyvars = intro_vars (map fst vs) reserved;
           in
             semicolon [
               str "data",
@@ -180,7 +180,7 @@
           end
       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
           let
-            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+            val tyvars = intro_vars (map fst vs) reserved;
           in
             semicolon (
               str "newtype"
@@ -193,7 +193,7 @@
           end
       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
           let
-            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+            val tyvars = intro_vars (map fst vs) reserved;
             fun pr_co (co, tys) =
               concat (
                 (str o deresolve_base) co
@@ -211,7 +211,7 @@
           end
       | pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
           let
-            val tyvars = Code_Printer.intro_vars [v] init_syms;
+            val tyvars = intro_vars [v] reserved;
             fun pr_classparam (classparam, ty) =
               semicolon [
                 (str o deresolve_base) classparam,
@@ -223,7 +223,7 @@
               Pretty.block [
                 str "class ",
                 Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
-                str (deresolve_base name ^ " " ^ Code_Printer.lookup_var tyvars v),
+                str (deresolve_base name ^ " " ^ lookup_var tyvars v),
                 str " where {"
               ],
               str "};"
@@ -231,12 +231,12 @@
           end
       | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
           let
-            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+            val tyvars = intro_vars (map fst vs) reserved;
             fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
              of NONE => semicolon [
                     (str o deresolve_base) classparam,
                     str "=",
-                    pr_app tyvars thm init_syms NOBR (c_inst, [])
+                    pr_app tyvars thm reserved NOBR (c_inst, [])
                   ]
               | SOME (k, pr) =>
                   let
@@ -245,9 +245,9 @@
                       then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
                     val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
                     val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
-                    val vars = init_syms
-                      |> Code_Printer.intro_vars (the_list const)
-                      |> Code_Printer.intro_vars (map_filter I vs);
+                    val vars = reserved
+                      |> intro_vars (the_list const)
+                      |> intro_vars (map_filter I vs);
                     val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
                       (*dictionaries are not relevant at this late stage*)
                   in
@@ -271,24 +271,24 @@
           end;
   in pr_stmt end;
 
-fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
+fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
   let
     val module_alias = if is_some module_name then K module_name else raw_module_alias;
-    val reserved_names = Name.make_context reserved_names;
-    val mk_name_module = Code_Printer.mk_name_module reserved_names module_prefix module_alias program;
+    val reserved = Name.make_context reserved;
+    val mk_name_module = mk_name_module reserved module_prefix module_alias program;
     fun add_stmt (name, (stmt, deps)) =
       let
-        val (module_name, base) = Code_Printer.dest_name name;
+        val (module_name, base) = dest_name name;
         val module_name' = mk_name_module module_name;
         val mk_name_stmt = yield_singleton Name.variants;
         fun add_fun upper (nsp_fun, nsp_typ) =
           let
             val (base', nsp_fun') =
-              mk_name_stmt (if upper then Code_Printer.first_upper base else base) nsp_fun
+              mk_name_stmt (if upper then first_upper base else base) nsp_fun
           in (base', (nsp_fun', nsp_typ)) end;
         fun add_typ (nsp_fun, nsp_typ) =
           let
-            val (base', nsp_typ') = mk_name_stmt (Code_Printer.first_upper base) nsp_typ
+            val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
           in (base', (nsp_fun, nsp_typ')) end;
         val add_name = case stmt
          of Code_Thingol.Fun _ => add_fun false
@@ -306,7 +306,7 @@
               cons (name, (Long_Name.append module_name' base', NONE))
           | _ => cons (name, (Long_Name.append module_name' base', SOME stmt));
       in
-        Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
+        Symtab.map_default (module_name', ([], ([], (reserved, reserved))))
               (apfst (fold (insert (op = : string * string -> bool)) deps))
         #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
         #-> (fn (base', names) =>
@@ -317,19 +317,19 @@
       (Graph.get_node program name, Graph.imm_succs program name))
       (Graph.strong_conn program |> flat)) Symtab.empty;
     fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
-      o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Printer.dest_name) name))) name
+      o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, hs_program) end;
 
 fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
-    raw_reserved_names includes raw_module_alias
+    raw_reserved includes raw_module_alias
     syntax_class syntax_tyco syntax_const program cs destination =
   let
     val stmt_names = Code_Target.stmt_names_of_destination destination;
     val module_name = if null stmt_names then raw_module_name else SOME "Code";
-    val reserved_names = fold (insert (op =) o fst) includes raw_reserved_names;
+    val reserved = fold (insert (op =) o fst) includes raw_reserved;
     val (deresolver, hs_program) = haskell_program_of_program labelled_name
-      module_name module_prefix reserved_names raw_module_alias program;
+      module_name module_prefix reserved raw_module_alias program;
     val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
     fun deriving_show tyco =
       let
@@ -343,9 +343,9 @@
               andalso forall (deriv' tycos) tys
           | deriv' _ (ITyVar _) = true
       in deriv [] tyco end;
-    val reserved_names = Code_Printer.make_vars reserved_names;
+    val reserved = make_vars reserved;
     fun pr_stmt qualified = pr_haskell_stmt labelled_name
-      syntax_class syntax_tyco syntax_const reserved_names
+      syntax_class syntax_tyco syntax_const reserved
       (if qualified then deresolver else Long_Name.base_name o deresolver)
       contr_classparam_typs
       (if string_classes then deriving_show else K false);
diff -r 0b92e6359bc4 -r d2e9b2dab760 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Oct 13 14:57:53 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Wed Oct 14 11:56:44 2009 +0200
@@ -45,12 +45,12 @@
 
 (** SML serailizer **)
 
-fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
+fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
   let
     fun pr_dicts fxy ds =
       let
-        fun pr_dictvar (v, (_, 1)) = Code_Printer.first_upper v ^ "_"
-          | pr_dictvar (v, (i, _)) = Code_Printer.first_upper v ^ string_of_int (i+1) ^ "_";
+        fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
+          | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
         fun pr_proj [] p =
               p
           | pr_proj [p'] p =
@@ -88,7 +88,7 @@
       | pr_term is_closure thm vars fxy (IVar NONE) =
           str "_"
       | pr_term is_closure thm vars fxy (IVar (SOME v)) =
-          str (Code_Printer.lookup_var vars v)
+          str (lookup_var vars v)
       | pr_term is_closure 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
@@ -176,8 +176,8 @@
       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
           let
             val consts = Code_Thingol.add_constnames t [];
-            val vars = reserved_names
-              |> Code_Printer.intro_base_names
+            val vars = reserved
+              |> intro_base_names
                   (is_none o syntax_const) deresolve consts;
           in
             concat [
@@ -199,10 +199,10 @@
                 fun pr_eq definer ((ts, t), (thm, _)) =
                   let
                     val consts = fold Code_Thingol.add_constnames (t :: ts) [];
-                    val vars = reserved_names
-                      |> Code_Printer.intro_base_names
+                    val vars = reserved
+                      |> intro_base_names
                            (is_none o syntax_const) deresolve consts
-                      |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
+                      |> intro_vars ((fold o Code_Thingol.fold_varnames)
                            (insert (op =)) ts []);
                   in
                     concat (
@@ -260,7 +260,7 @@
           in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end
      | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
           let
-            val w = Code_Printer.first_upper v ^ "_";
+            val w = first_upper v ^ "_";
             fun pr_superclass_field (class, classrel) =
               (concat o map str) [
                 deresolve classrel, ":", "'" ^ v, deresolve class
@@ -313,7 +313,7 @@
               concat [
                 (str o Long_Name.base_name o deresolve) classparam,
                 str "=",
-                pr_app (K false) thm reserved_names NOBR (c_inst, [])
+                pr_app (K false) thm reserved NOBR (c_inst, [])
               ];
           in
             semicolon ([
@@ -352,12 +352,12 @@
 
 (** OCaml serializer **)
 
-fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
+fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
   let
     fun pr_dicts fxy ds =
       let
-        fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Printer.first_upper v
-          | pr_dictvar (v, (i, _)) = "_" ^ Code_Printer.first_upper v ^ string_of_int (i+1);
+        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)) =
@@ -391,7 +391,7 @@
       | pr_term is_closure thm vars fxy (IVar NONE) =
           str "_"
       | pr_term is_closure thm vars fxy (IVar (SOME v)) =
-          str (Code_Printer.lookup_var vars v)
+          str (lookup_var vars v)
       | pr_term is_closure 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
@@ -469,8 +469,8 @@
       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
           let
             val consts = Code_Thingol.add_constnames t [];
-            val vars = reserved_names
-              |> Code_Printer.intro_base_names
+            val vars = reserved
+              |> intro_base_names
                   (is_none o syntax_const) deresolve consts;
           in
             concat [
@@ -487,10 +487,10 @@
             fun pr_eq ((ts, t), (thm, _)) =
               let
                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
-                val vars = reserved_names
-                  |> Code_Printer.intro_base_names
+                val vars = reserved
+                  |> intro_base_names
                       (is_none o syntax_const) deresolve consts
-                  |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
+                  |> intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in concat [
                 (Pretty.block o Pretty.commas)
@@ -501,10 +501,10 @@
             fun pr_eqs is_pseudo [((ts, t), (thm, _))] =
                   let
                     val consts = fold Code_Thingol.add_constnames (t :: ts) [];
-                    val vars = reserved_names
-                      |> Code_Printer.intro_base_names
+                    val vars = reserved
+                      |> intro_base_names
                           (is_none o syntax_const) deresolve consts
-                      |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
+                      |> intro_vars ((fold o Code_Thingol.fold_varnames)
                           (insert (op =)) ts []);
                   in
                     concat (
@@ -527,10 +527,10 @@
               | pr_eqs _ (eqs as eq :: eqs') =
                   let
                     val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
-                    val vars = reserved_names
-                  |> Code_Printer.intro_base_names
+                    val vars = reserved
+                      |> intro_base_names
                       (is_none o syntax_const) deresolve consts;
-                    val dummy_parms = (map str o Code_Printer.aux_params vars o map (fst o fst)) eqs;
+                    val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
                   in
                     Pretty.block (
                       Pretty.breaks dummy_parms
@@ -595,7 +595,7 @@
           in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end
      | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
           let
-            val w = "_" ^ Code_Printer.first_upper v;
+            val w = "_" ^ first_upper v;
             fun pr_superclass_field (class, classrel) =
               (concat o map str) [
                 deresolve classrel, ":", "'" ^ v, deresolve class
@@ -636,7 +636,7 @@
               concat [
                 (str o deresolve) classparam,
                 str "=",
-                pr_app (K false) thm reserved_names NOBR (c_inst, [])
+                pr_app (K false) thm reserved NOBR (c_inst, [])
               ];
           in
             concat (
@@ -705,11 +705,11 @@
 
 in
 
-fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
+fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
   let
     val module_alias = if is_some module_name then K module_name else raw_module_alias;
-    val reserved_names = Name.make_context reserved_names;
-    val empty_module = ((reserved_names, reserved_names), Graph.empty);
+    val reserved = Name.make_context reserved;
+    val empty_module = ((reserved, reserved), Graph.empty);
     fun map_node [] f = f
       | map_node (m::ms) f =
           Graph.default_node (m, Module (m, empty_module))
@@ -737,11 +737,11 @@
       let
         val (x, nsp_typ') = f nsp_typ
       in (x, (nsp_fun, nsp_typ')) end;
-    val mk_name_module = Code_Printer.mk_name_module reserved_names NONE module_alias program;
+    val mk_name_module = mk_name_module reserved NONE module_alias program;
     fun mk_name_stmt upper name nsp =
       let
-        val (_, base) = Code_Printer.dest_name name;
-        val base' = if upper then Code_Printer.first_upper base else base;
+        val (_, base) = dest_name name;
+        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) =
@@ -824,7 +824,7 @@
           []
           |> fold (fold (insert (op =)) o Graph.imm_succs program) names
           |> subtract (op =) names;
-        val (module_names, _) = (split_list o map Code_Printer.dest_name) names;
+        val (module_names, _) = (split_list o map dest_name) names;
         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
           handle Empty =>
             error ("Different namespace prefixes for mutual dependencies:\n"
@@ -834,7 +834,7 @@
         val module_name_path = Long_Name.explode module_name;
         fun add_dep name name' =
           let
-            val module_name' = (mk_name_module o fst o Code_Printer.dest_name) name';
+            val module_name' = (mk_name_module o fst o dest_name) name';
           in if module_name = module_name' then
             map_node module_name_path (Graph.add_edge (name, name'))
           else let
@@ -862,7 +862,7 @@
           (rev (Graph.strong_conn program)));
     fun deresolver prefix name = 
       let
-        val module_name = (fst o Code_Printer.dest_name) name;
+        val module_name = (fst o dest_name) name;
         val module_name' = (Long_Name.explode o mk_name_module) module_name;
         val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
         val stmt_name =
@@ -877,7 +877,7 @@
         error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, nodes) end;
 
-fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
+fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved includes raw_module_alias
   _ syntax_tyco syntax_const program stmt_names destination =
   let
     val is_cons = Code_Thingol.is_cons program;
@@ -885,15 +885,15 @@
     val is_present = not (null present_stmt_names);
     val module_name = if is_present then SOME "Code" else raw_module_name;
     val (deresolver, nodes) = ml_node_of_program labelled_name module_name
-      reserved_names raw_module_alias program;
-    val reserved_names = Code_Printer.make_vars reserved_names;
+      reserved raw_module_alias program;
+    val reserved = make_vars reserved;
     fun pr_node prefix (Dummy _) =
           NONE
       | pr_node prefix (Stmt (_, stmt)) = if is_present andalso
           (null o filter (member (op =) present_stmt_names) o stmt_names_of) stmt
           then NONE
           else SOME
-            (pr_stmt labelled_name syntax_tyco syntax_const reserved_names
+            (pr_stmt labelled_name syntax_tyco syntax_const reserved
               (deresolver prefix) is_cons stmt)
       | pr_node prefix (Module (module_name, (_, nodes))) =
           separate (str "")
diff -r 0b92e6359bc4 -r d2e9b2dab760 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Tue Oct 13 14:57:53 2009 +0200
+++ b/src/Tools/Code/code_printer.ML	Wed Oct 14 11:56:44 2009 +0200
@@ -316,13 +316,13 @@
 val dest_name =
   apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
 
-fun mk_name_module reserved_names module_prefix module_alias program =
+fun mk_name_module reserved module_prefix module_alias program =
   let
     fun mk_alias name = case module_alias name
      of SOME name' => name'
       | NONE => name
           |> Long_Name.explode
-          |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
+          |> map (fn name => (the_single o fst) (Name.variants [name] reserved))
           |> Long_Name.implode;
     fun mk_prefix name = case module_prefix
      of SOME module_prefix => Long_Name.append module_prefix name