# HG changeset patch # User berghofe # Date 1086094762 -7200 # Node ID 9fc1a5cf9b5a2f5d783ee6c0fc2a3a62428ff274 # Parent 252d9b36bf445272b9924518ee3e03e70d68a17a Improved name mangling function. diff -r 252d9b36bf44 -r 9fc1a5cf9b5a src/Pure/codegen.ML --- a/src/Pure/codegen.ML Tue Jun 01 12:36:26 2004 +0200 +++ b/src/Pure/codegen.ML Tue Jun 01 14:59:22 2004 +0200 @@ -36,6 +36,7 @@ (exn option * string) Graph.T * term -> (exn option * string) Graph.T * Pretty.T val invoke_tycodegen: theory -> string -> bool -> (exn option * string) Graph.T * typ -> (exn option * string) Graph.T * Pretty.T + val mk_id: string -> string val mk_const_id: Sign.sg -> string -> string val mk_type_id: Sign.sg -> string -> string val rename_term: term -> term @@ -273,34 +274,55 @@ (**** make valid ML identifiers ****) -fun gen_mk_id kind rename sg s = +fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse + Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x; + +fun dest_sym s = (case split_last (snd (take_prefix (equal "\\") (explode s))) of + ("<" :: "^" :: xs, ">") => (true, implode xs) + | ("<" :: xs, ">") => (false, implode xs) + | _ => sys_error "dest_sym"); + +fun mk_id s = if s = "" then "" else let - val (xs as x::_) = explode (rename (space_implode "_" - (NameSpace.unpack (Sign.cond_extern sg kind s)))); - fun check_str [] = "" - | check_str (" " :: xs) = "_" ^ check_str xs - | check_str (x :: xs) = - (if Symbol.is_letdig x then x - else "_" ^ string_of_int (ord x)) ^ check_str xs + fun check_str [] = [] + | check_str xs = (case take_prefix is_ascii_letdig xs of + ([], " " :: zs) => check_str zs + | ([], "_" :: zs) => check_str zs + | ([], z :: zs) => + if size z = 1 then string_of_int (ord z) :: check_str zs + else (case dest_sym z of + (true, "isub") => check_str zs + | (true, "isup") => "" :: check_str zs + | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs) + | (ys, zs) => implode ys :: check_str zs); + val s' = space_implode "_" + (flat (map (check_str o Symbol.explode) (NameSpace.unpack s))) in - (if not (Symbol.is_letter x) then "id" else "") ^ check_str xs + if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s' end; -val mk_const_id = gen_mk_id Sign.constK - (fn s => if s mem ThmDatabase.ml_reserved then s ^ "_const" else s); +fun mk_const_id sg s = + let val s' = mk_id (Sign.cond_extern sg Sign.constK s) + in if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' end; -val mk_type_id = gen_mk_id Sign.typeK - (fn s => if s mem ThmDatabase.ml_reserved then s ^ "_type" else s); +fun mk_type_id sg s = + let val s' = mk_id (Sign.cond_extern sg Sign.typeK s) + in if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' end; fun rename_terms ts = let val names = foldr add_term_names (ts, map (fst o fst) (Drule.vars_of_terms ts)); - val clash = names inter ThmDatabase.ml_reserved; - val ps = clash ~~ variantlist (clash, names); + val reserved = names inter ThmDatabase.ml_reserved; + val (illegal, alt_names) = split_list (mapfilter (fn s => + let val s' = mk_id s in if s = s' then None else Some (s, s') end) names) + val ps = (reserved @ illegal) ~~ + variantlist (map (suffix "'") reserved @ alt_names, names); - fun rename (Var ((a, i), T)) = Var ((if_none (assoc (ps, a)) a, i), T) - | rename (Free (a, T)) = Free (if_none (assoc (ps, a)) a, T) + fun rename_id s = if_none (assoc (ps, s)) s; + + fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T) + | rename (Free (a, T)) = Free (rename_id a, T) | rename (Abs (s, T, t)) = Abs (s, T, rename t) | rename (t $ u) = rename t $ rename u | rename t = t; @@ -387,7 +409,7 @@ separate (Pretty.brk 1) (p :: ps) @ [Pretty.str ")"]) else Pretty.block (separate (Pretty.brk 1) (p :: ps)); -fun new_names t xs = variantlist (xs, +fun new_names t xs = variantlist (map mk_id xs, map (fst o fst o dest_Var) (term_vars t) union add_term_names (t, ThmDatabase.ml_reserved));