# HG changeset patch # User haftmann # Date 1162560163 -3600 # Node ID dae0416fddfdc85d7d0b30602c284ed4840de1c5 # Parent 17f144c6e2f2af1eba440ca92945efb82e1d37b7 dropped name_mangler.ML diff -r 17f144c6e2f2 -r dae0416fddfd src/Pure/General/ROOT.ML --- a/src/Pure/General/ROOT.ML Fri Nov 03 14:22:42 2006 +0100 +++ b/src/Pure/General/ROOT.ML Fri Nov 03 14:22:43 2006 +0100 @@ -16,7 +16,6 @@ use "source.ML"; use "symbol.ML"; use "name_space.ML"; -use "name_mangler.ML"; use "seq.ML"; use "susp.ML"; use "rat.ML"; diff -r 17f144c6e2f2 -r dae0416fddfd src/Pure/General/name_mangler.ML --- a/src/Pure/General/name_mangler.ML Fri Nov 03 14:22:42 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,143 +0,0 @@ -(* Title: Pure/General/name_mangler.ML - ID: $Id$ - Author: Florian Haftmann, TU Muenchen - -Generic name mangler -- provides bijective mappings from any expressions -to strings and vice versa. -*) - -signature NAME_MANGLER = -sig - type ctxt - type src - type T - val mk_unique: ('b * 'b -> bool) -> ('a * int -> 'b) - -> 'a -> 'b list -> 'b * 'b list - val mk_unique_multi: ('b * 'b -> bool) -> ('a * int -> 'b) - -> 'a list -> 'b list -> 'b list * 'b list - val empty: T - val get: ctxt -> T -> src -> string - val rev: ctxt -> T -> string -> src - val declare: ctxt -> src -> T -> string * T - val declare_multi: ctxt -> src list -> T -> string list * T - val merge: T * T -> T - val dest: T -> (src * string) list -end; - -functor NameManglerFun ( - type ctxt - type src - val ord: src * src -> order - val mk: ctxt -> src * int -> string - val is_valid: ctxt -> string -> bool - val maybe_unique: ctxt -> src -> string option - val re_mangle: ctxt -> string -> src -) : NAME_MANGLER = -struct - -structure Srctab = TableFun ( - type key = src - val ord = ord -); - -type ctxt = ctxt; -type src = src; -type T = string Srctab.table * src Symtab.table; - -fun mk_unique eq mk seed used = - let - fun mk_name i = - let - val name = mk (seed, i) - in - if member eq used name - then mk_name (i+1) - else name - end; - val name = mk_name 0; - in (name, name :: used) end; - -fun mk_unique_multi eq mk seeds used = - let - fun mk_names i = - if i < 2 then - let - val names = map (fn seed => mk (seed, i)) seeds - in - if null (gen_inter eq (used, names)) - andalso (not oo has_duplicates) eq names - then names - else mk_names (i+1) - end - else - used - |> fold_map (mk_unique eq mk) seeds - |> fst; - val names = mk_names 0; - in (names, fold cons names used) end; - -val empty = (Srctab.empty, Symtab.empty); - -fun get ctxt (tab_f, _) x = - case Srctab.lookup tab_f x - of SOME s => s - | NONE => (the o maybe_unique ctxt) x; - -fun rev ctxt (_, tab_r) s = - case Symtab.lookup tab_r s - of SOME x => x - | NONE => re_mangle ctxt s; - -fun declare ctxt x (tabs as (tab_f, tab_r)) = - case maybe_unique ctxt x - of NONE => - let - fun mk_it (seed, i) = - let - val name = mk ctxt (seed, i) - in - if is_valid ctxt name - andalso (not oo Symtab.defined) tab_r name - then name - else mk_it (seed, i+1) - end; - val name = (fst oooo mk_unique) (op =) mk_it x []; - in - (name, - (tab_f |> Srctab.update (x, name), - tab_r |> Symtab.update (name, x))) - end - | SOME s => (s, tabs) - -fun declare_multi ctxt xs (tabs as (tab_f, tab_r)) = - let - val xs' = map (maybe_unique ctxt) xs - in - if forall is_some xs' - then (map the xs', tabs) - else - let - fun mk_it (seed, i) = - let - val name = mk ctxt (seed, i) - in - if is_valid ctxt name - andalso (not oo Symtab.defined) tab_r name - then name - else mk_it (seed, i+1) - end; - val names = (fst oooo mk_unique_multi) (op =) mk_it xs []; - in - (names, - (tab_f |> fold2 (curry Srctab.update) xs names, - tab_r |> fold2 (curry Symtab.update) names xs)) - end - end; - -fun merge ((tab_f_1, tab_r_1), (tab_f_2, tab_r_2)) = - (Srctab.merge (op = : string * string -> bool) (tab_f_1, tab_f_2), - Symtab.merge (is_equal o ord) (tab_r_1, tab_r_2)); - -fun dest (tab_f, _) = Srctab.dest tab_f; - -end; \ No newline at end of file diff -r 17f144c6e2f2 -r dae0416fddfd src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Nov 03 14:22:42 2006 +0100 +++ b/src/Pure/IsaMakefile Fri Nov 03 14:22:43 2006 +0100 @@ -25,7 +25,7 @@ $(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML \ General/buffer.ML General/file.ML General/graph.ML General/heap.ML \ - General/history.ML General/name_mangler.ML General/name_space.ML \ + General/history.ML General/name_space.ML \ General/ord_list.ML General/output.ML General/path.ML \ General/position.ML General/pretty.ML General/rat.ML General/scan.ML \ General/secure.ML General/seq.ML General/source.ML General/stack.ML \