# HG changeset patch
# User haftmann
# Date 1241441391 -7200
# Node ID 64ff53fc0c0cb5322b3993433d433c737e1f8148
# Parent  de0a20a030fdf9d9f73f5631f41b399ccd650bd2
removed code_name module

diff -r de0a20a030fd -r 64ff53fc0c0c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon May 04 14:49:50 2009 +0200
+++ b/src/HOL/IsaMakefile	Mon May 04 14:49:51 2009 +0200
@@ -92,7 +92,6 @@
   $(SRC)/Tools/auto_solve.ML \
   $(SRC)/Tools/code/code_haskell.ML \
   $(SRC)/Tools/code/code_ml.ML \
-  $(SRC)/Tools/code/code_name.ML \
   $(SRC)/Tools/code/code_printer.ML \
   $(SRC)/Tools/code/code_target.ML \
   $(SRC)/Tools/code/code_thingol.ML \
diff -r de0a20a030fd -r 64ff53fc0c0c src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Mon May 04 14:49:50 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Mon May 04 14:49:51 2009 +0200
@@ -59,7 +59,7 @@
       |> expand_eta thy
       |> map (AxClass.overload thy)
       |> map_filter (meta_eq_to_obj_eq thy)
-      |> Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var
+      |> Code_Unit.norm_varnames thy
       |> map (rpair opt_name)
   in if null thms then NONE else SOME thms end;
 
diff -r de0a20a030fd -r 64ff53fc0c0c src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Mon May 04 14:49:50 2009 +0200
+++ b/src/Pure/Isar/code_unit.ML	Mon May 04 14:49:51 2009 +0200
@@ -45,7 +45,7 @@
   val rewrite_eqn: simpset -> thm -> thm
   val rewrite_head: thm list -> thm -> thm
   val norm_args: theory -> thm list -> thm list 
-  val norm_varnames: theory -> (string -> string) -> (string -> string) -> thm list -> thm list
+  val norm_varnames: theory -> thm list -> thm list
 
   (*case certificates*)
   val case_cert: thm -> string * (int * string list)
@@ -161,9 +161,10 @@
     |> map (Conv.fconv_rule Drule.beta_eta_conversion)
   end;
 
-fun canonical_tvars thy purify_tvar thm =
+fun canonical_tvars thy thm =
   let
     val ctyp = Thm.ctyp_of thy;
+    val purify_tvar = unprefix "'" #> Name.desymbolize false #> prefix "'";
     fun tvars_subst_for thm = (fold_types o fold_atyps)
       (fn TVar (v_i as (v, _), sort) => let
             val v' = purify_tvar v
@@ -180,9 +181,10 @@
     val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
   in Thm.instantiate (inst, []) thm end;
 
-fun canonical_vars thy purify_var thm =
+fun canonical_vars thy thm =
   let
     val cterm = Thm.cterm_of thy;
+    val purify_var = Name.desymbolize false;
     fun vars_subst_for thm = fold_aterms
       (fn Var (v_i as (v, _), ty) => let
             val v' = purify_var v
@@ -199,13 +201,14 @@
     val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
   in Thm.instantiate ([], inst) thm end;
 
-fun canonical_absvars purify_var thm =
+fun canonical_absvars thm =
   let
     val t = Thm.plain_prop_of thm;
+    val purify_var = Name.desymbolize false;
     val t' = Term.map_abs_vars purify_var t;
   in Thm.rename_boundvars t t' thm end;
 
-fun norm_varnames thy purify_tvar purify_var thms =
+fun norm_varnames thy thms =
   let
     fun burrow_thms f [] = []
       | burrow_thms f thms =
@@ -215,10 +218,10 @@
           |> Conjunction.elim_balanced (length thms)
   in
     thms
-    |> map (canonical_vars thy purify_var)
-    |> map (canonical_absvars purify_var)
+    |> map (canonical_vars thy)
+    |> map canonical_absvars
     |> map Drule.zero_var_indexes
-    |> burrow_thms (canonical_tvars thy purify_tvar)
+    |> burrow_thms (canonical_tvars thy)
     |> Drule.zero_var_indexes_list
   end;
 
diff -r de0a20a030fd -r 64ff53fc0c0c src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Mon May 04 14:49:50 2009 +0200
+++ b/src/Tools/Code_Generator.thy	Mon May 04 14:49:51 2009 +0200
@@ -9,7 +9,6 @@
 uses
   "~~/src/Tools/value.ML"
   "~~/src/Tools/quickcheck.ML"
-  "~~/src/Tools/code/code_name.ML"
   "~~/src/Tools/code/code_wellsorted.ML" 
   "~~/src/Tools/code/code_thingol.ML"
   "~~/src/Tools/code/code_printer.ML"
diff -r de0a20a030fd -r 64ff53fc0c0c src/Tools/code/code_name.ML
--- a/src/Tools/code/code_name.ML	Mon May 04 14:49:50 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-(*  Title:      Tools/code/code_name.ML
-    Author:     Florian Haftmann, TU Muenchen
-
-Some code generator infrastructure concerning names.
-*)
-
-signature CODE_NAME =
-sig
-  val purify_name: bool -> string -> string
-  val purify_var: string -> string
-  val purify_tvar: string -> string
-  val purify_base: string -> string
-
-  val read_const_exprs: theory -> string list -> string list * string list
-end;
-
-structure Code_Name: CODE_NAME =
-struct
-
-(** purification **)
-
-fun purify_name upper = 
-  let
-    fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
-      else (if forall Symbol.is_ascii_upper cs
-        then map else nth_map 0) Symbol.to_ascii_lower cs;
-  in
-    Name.desymbolize
-    #> explode
-    #> upper_lower
-    #> implode
-  end;
-
-val purify_var = purify_name false;
-
-fun purify_tvar "" = "'a"
-  | purify_tvar v =
-      (unprefix "'" #> purify_name false #> prefix "'") v;
-
-(*FIMXE non-canonical function treating non-canonical names*)
-fun purify_base "op &" = "and"
-  | purify_base "op |" = "or"
-  | purify_base "op -->" = "implies"
-  | purify_base "op :" = "member"
-  | purify_base "op =" = "eq"
-  | purify_base "*" = "product"
-  | purify_base "+" = "sum"
-  | purify_base s = purify_name false s;
-
-
-(** misc **)
-
-fun read_const_exprs thy =
-  let
-    fun consts_of some_thyname =
-      let
-        val thy' = case some_thyname
-         of SOME thyname => ThyInfo.the_theory thyname thy
-          | NONE => thy;
-        val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
-          ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
-        fun belongs_here c =
-          not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
-      in case some_thyname
-       of NONE => cs
-        | SOME thyname => filter belongs_here cs
-      end;
-    fun read_const_expr "*" = ([], consts_of NONE)
-      | read_const_expr s = if String.isSuffix ".*" s
-          then ([], consts_of (SOME (unsuffix ".*" s)))
-          else ([Code_Unit.read_const thy s], []);
-  in pairself flat o split_list o map read_const_expr end;
-
-end;
diff -r de0a20a030fd -r 64ff53fc0c0c src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Mon May 04 14:49:50 2009 +0200
+++ b/src/Tools/code/code_target.ML	Mon May 04 14:49:51 2009 +0200
@@ -326,7 +326,7 @@
 fun add_module_alias target (thyname, modlname) =
   let
     val xs = Long_Name.explode modlname;
-    val xs' = map (Code_Name.purify_name true) xs;
+    val xs' = map (Name.desymbolize true) xs;
   in if xs' = xs
     then map_module_alias target (Symtab.update (thyname, modlname))
     else error ("Invalid module name: " ^ quote modlname ^ "\n"
@@ -502,7 +502,7 @@
 
 fun read_const_exprs thy cs =
   let
-    val (cs1, cs2) = Code_Name.read_const_exprs thy cs;
+    val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
     val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
     val names4 = transitivly_non_empty_funs thy naming program;
     val cs5 = map_filter
diff -r de0a20a030fd -r 64ff53fc0c0c src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Mon May 04 14:49:50 2009 +0200
+++ b/src/Tools/code/code_thingol.ML	Mon May 04 14:49:51 2009 +0200
@@ -81,6 +81,7 @@
   val is_cons: program -> string -> bool
   val contr_classparam_typs: program -> string -> itype option list
 
+  val read_const_exprs: theory -> string list -> string list * string list
   val consts_program: theory -> string list -> string list * (naming * program)
   val cached_program: theory -> naming * program
   val eval_conv: theory -> (sort -> sort)
@@ -239,10 +240,18 @@
     | NONE => (case Code.get_datatype_of_constr thy c
        of SOME dtco => thyname_of_tyco thy dtco
         | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c);
+  fun purify_base "op &" = "and"
+    | purify_base "op |" = "or"
+    | purify_base "op -->" = "implies"
+    | purify_base "op :" = "member"
+    | purify_base "op =" = "eq"
+    | purify_base "*" = "product"
+    | purify_base "+" = "sum"
+    | purify_base s = Name.desymbolize false s;
   fun namify thy get_basename get_thyname name =
     let
       val prefix = get_thyname thy name;
-      val base = (Code_Name.purify_base o get_basename) name;
+      val base = (purify_base o get_basename) name;
     in Long_Name.append prefix base end;
 in
 
@@ -782,6 +791,27 @@
 
 (** diagnostic commands **)
 
+fun read_const_exprs thy =
+  let
+    fun consts_of some_thyname =
+      let
+        val thy' = case some_thyname
+         of SOME thyname => ThyInfo.the_theory thyname thy
+          | NONE => thy;
+        val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
+          ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
+        fun belongs_here c =
+          not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
+      in case some_thyname
+       of NONE => cs
+        | SOME thyname => filter belongs_here cs
+      end;
+    fun read_const_expr "*" = ([], consts_of NONE)
+      | read_const_expr s = if String.isSuffix ".*" s
+          then ([], consts_of (SOME (unsuffix ".*" s)))
+          else ([Code_Unit.read_const thy s], []);
+  in pairself flat o split_list o map read_const_expr end;
+
 fun code_depgr thy consts =
   let
     val (_, eqngr) = Code_Wellsorted.obtain thy consts [];
@@ -818,8 +848,8 @@
 structure P = OuterParse
 and K = OuterKeyword
 
-fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
-fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
+fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
+fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
 
 in
 
diff -r de0a20a030fd -r 64ff53fc0c0c src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Mon May 04 14:49:50 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML	Mon May 04 14:49:51 2009 +0200
@@ -107,7 +107,7 @@
     | NONE => let
         val eqns = Code.these_eqns thy c
           |> burrow_fst (Code_Unit.norm_args thy)
-          |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
+          |> burrow_fst (Code_Unit.norm_varnames thy);
         val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns;
       in ((lhs, rhss), eqns) end;