src/Tools/code/code_name.ML

 Some code generator infrastructure concerning names.
 *)
 
 signature CODE_NAME =
 sig
-  structure StringPairTab: TABLE
-  val first_upper: string -> string
-  val first_lower: string -> string
-  val dest_name: string -> string * string
-
   val purify_var: string -> string
   val purify_tvar: string -> string
-  val purify_sym: string -> string
-  val purify_base: bool -> string -> string
+  val purify_base: string -> string
   val check_modulename: string -> string
 
-  type var_ctxt
-  val make_vars: string list -> var_ctxt
-  val intro_vars: string list -> var_ctxt -> var_ctxt
-  val lookup_var: var_ctxt -> string -> string
-
   val read_const_exprs: theory -> string list -> string list * string list
-  val mk_name_module: Name.context -> string option -> (string -> string option)
-    -> 'a Graph.T -> string -> string
 end;
 
 structure Code_Name: CODE_NAME =
 struct
 
-(** auxiliary **)
-
-structure StringPairTab =
-  TableFun(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
-
-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;
-
-val dest_name =
-  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
-
-
 (** purification **)
 
-fun purify_name upper lower =
+fun purify_name upper =
   let
     fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
     val is_junk = not o is_valid andf Symbol.is_regular;
     val junk = Scan.many is_junk;
     val scan_valids = Symbol.scanner "Malformed input"
       ((junk |--
         (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
         --| junk))
       ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
     fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
-      else if lower then (if forall Symbol.is_ascii_upper cs
-        then map else nth_map 0) Symbol.to_ascii_lower cs
-      else cs;
+      else (if forall Symbol.is_ascii_upper cs
+        then map else nth_map 0) Symbol.to_ascii_lower cs;
   in
     explode
     #> scan_valids
     #> space_implode "_"
     #> explode
     #> upper_lower
     #> implode
   end;
 
 fun purify_var "" = "x"
-  | purify_var v = purify_name false true v;
+  | purify_var v = purify_name false v;
 
 fun purify_tvar "" = "'a"
   | purify_tvar v =
       (unprefix "'" #> explode #> filter Symbol.is_ascii_letter #> cons "'" #> implode) v;
 

   (*FIMXE should disappear as soon as hierarchical theory name spaces are available*)
   #> Symbol.scanner "Malformed name"
       (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
   #> implode
   #> Long_Name.explode
-  #> map (purify_name true false);
+  #> map (purify_name true);
 
 (*FIMXE non-canonical function treating non-canonical names*)
-fun purify_base _ "op &" = "and"
-  | purify_base _ "op |" = "or"
-  | purify_base _ "op -->" = "implies"
-  | purify_base _ "{}" = "empty"
-  | purify_base _ "op :" = "member"
-  | purify_base _ "op Int" = "intersect"
-  | purify_base _ "op Un" = "union"
-  | purify_base _ "*" = "product"
-  | purify_base _ "+" = "sum"
-  | purify_base lower s = if String.isPrefix "op =" s
-      then "eq" ^ purify_name false lower s
-      else purify_name false lower s;
-
-val purify_sym = purify_base false;
+fun purify_base "op &" = "and"
+  | purify_base "op |" = "or"
+  | purify_base "op -->" = "implies"
+  | purify_base "op :" = "member"
+  | purify_base "*" = "product"
+  | purify_base "+" = "sum"
+  | purify_base s = if String.isPrefix "op =" s
+      then "eq" ^ purify_name false s
+      else purify_name false s;
 
 fun check_modulename mn =
   let
     val mns = Long_Name.explode mn;
-    val mns' = map (purify_name true false) mns;
+    val mns' = map (purify_name true) mns;
   in
     if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
       ^ "perhaps try " ^ quote (Long_Name.implode mns'))
   end;
-
-
-(** variable name contexts **)
-
-type var_ctxt = string Symtab.table * Name.context;
-
-fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
-  Name.make_context names);
-
-fun intro_vars names (namemap, namectxt) =
-  let
-    val (names', namectxt') = Name.variants names namectxt;
-    val namemap' = fold2 (curry Symtab.update) names names' namemap;
-  in (namemap', namectxt') end;
-
-fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
- of SOME name' => name'
-  | NONE => error ("Invalid name in context: " ^ quote name);
 
 
 (** misc **)
 
 fun read_const_exprs thy =

       | 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 mk_name_module reserved_names 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))
-          |> Long_Name.implode;
-    fun mk_prefix name = case module_prefix
-     of SOME module_prefix => Long_Name.append module_prefix name
-      | NONE => name;
-    val tab =
-      Symtab.empty
-      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
-           o fst o dest_name o fst)
-             program
-  in the o Symtab.lookup tab end;
-
 end;