# HG changeset patch
# User haftmann
# Date 1255355198 -7200
# Node ID 3e9809678574ff368bd87c33b08d9019a6bc1c5c
# Parent  d61e303fc7e553612ccadaa91fb157bdd284b2a3
intro_base_names combinator

diff -r d61e303fc7e5 -r 3e9809678574 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Mon Oct 12 14:22:54 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML	Mon Oct 12 15:46:38 2009 +0200
@@ -144,12 +144,10 @@
             val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
             fun pr_eq ((ts, t), (thm, _)) =
               let
-                val consts = map_filter
-                  (fn c => if (is_some o syntax_const) c
-                    then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                    (fold Code_Thingol.add_constnames (t :: ts) []);
+                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = init_syms
-                  |> Code_Printer.intro_vars consts
+                  |> Code_Printer.intro_base_names
+                      (is_none o syntax_const) deresolve consts
                   |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
                        (insert (op =)) ts []);
               in
diff -r d61e303fc7e5 -r 3e9809678574 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Mon Oct 12 14:22:54 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Mon Oct 12 15:46:38 2009 +0200
@@ -175,12 +175,10 @@
           end
       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
           let
-            val consts = map_filter
-              (fn c => if (is_some o syntax_const) c
-                then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                (Code_Thingol.add_constnames t []);
+            val consts = Code_Thingol.add_constnames t [];
             val vars = reserved_names
-              |> Code_Printer.intro_vars consts;
+              |> Code_Printer.intro_base_names
+                  (is_none o syntax_const) deresolve consts;
           in
             concat [
               str "val",
@@ -200,12 +198,10 @@
                   map (Pretty.block o single o Pretty.block o single);
                 fun pr_eq definer ((ts, t), (thm, _)) =
                   let
-                    val consts = map_filter
-                      (fn c => if (is_some o syntax_const) c
-                        then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                        (fold Code_Thingol.add_constnames (t :: ts) []);
+                    val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                     val vars = reserved_names
-                      |> Code_Printer.intro_vars consts
+                      |> Code_Printer.intro_base_names
+                           (is_none o syntax_const) deresolve consts
                       |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
                            (insert (op =)) ts []);
                   in
@@ -472,12 +468,10 @@
           end
       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
           let
-            val consts = map_filter
-              (fn c => if (is_some o syntax_const) c
-                then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                (Code_Thingol.add_constnames t []);
+            val consts = Code_Thingol.add_constnames t [];
             val vars = reserved_names
-              |> Code_Printer.intro_vars consts;
+              |> Code_Printer.intro_base_names
+                  (is_none o syntax_const) deresolve consts;
           in
             concat [
               str "let",
@@ -492,12 +486,10 @@
           let
             fun pr_eq ((ts, t), (thm, _)) =
               let
-                val consts = map_filter
-                  (fn c => if (is_some o syntax_const) c
-                    then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                    (fold Code_Thingol.add_constnames (t :: ts) []);
+                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved_names
-                  |> Code_Printer.intro_vars consts
+                  |> Code_Printer.intro_base_names
+                      (is_none o syntax_const) deresolve consts
                   |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in concat [
@@ -508,12 +500,10 @@
               ] end;
             fun pr_eqs is_pseudo [((ts, t), (thm, _))] =
                   let
-                    val consts = map_filter
-                      (fn c => if (is_some o syntax_const) c
-                        then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                        (fold Code_Thingol.add_constnames (t :: ts) []);
+                    val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                     val vars = reserved_names
-                      |> Code_Printer.intro_vars consts
+                      |> Code_Printer.intro_base_names
+                          (is_none o syntax_const) deresolve consts
                       |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
                           (insert (op =)) ts []);
                   in
@@ -536,12 +526,10 @@
                   )
               | pr_eqs _ (eqs as eq :: eqs') =
                   let
-                    val consts = map_filter
-                      (fn c => if (is_some o syntax_const) c
-                        then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                        (fold Code_Thingol.add_constnames (map (snd o fst) eqs) []);
+                    val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
                     val vars = reserved_names
-                      |> Code_Printer.intro_vars consts;
+                  |> Code_Printer.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;
                   in
                     Pretty.block (
diff -r d61e303fc7e5 -r 3e9809678574 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Mon Oct 12 14:22:54 2009 +0200
+++ b/src/Tools/Code/code_printer.ML	Mon Oct 12 15:46:38 2009 +0200
@@ -27,6 +27,8 @@
   val make_vars: string list -> var_ctxt
   val intro_vars: string list -> var_ctxt -> var_ctxt
   val lookup_var: var_ctxt -> string -> string
+  val intro_base_names: (string -> bool) -> (string -> string)
+    -> string list -> var_ctxt -> var_ctxt
   val aux_params: var_ctxt -> iterm list list -> string list
 
   type literals
@@ -134,6 +136,13 @@
     val vars' = intro_vars fished3 vars;
   in map (lookup_var vars') fished3 end;
 
+fun intro_base_names no_syntax deresolve names = names 
+  |> map_filter (fn name => if no_syntax name then
+      let val name' = deresolve name in
+        if Long_Name.is_qualified name' then NONE else SOME name'
+      end else NONE)
+  |> intro_vars;
+
 
 (** pretty literals **)