]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/alpha.ml
- new attributes system
[helm.git] / helm / software / helena / src / common / alpha.ml
index 1eb6b106383c0a1623a2a47430ac11dbe62bb61f..8da7e563b970eedd2a16efb3162476c0b63f2e6f 100644 (file)
 
 module E = Entity
 
-(* internal functions *******************************************************)
-
-let rec rename ns n =
-   let token, mode = n in
-   let n = token ^ "_", mode in
-   if List.mem n ns then rename ns n else n
-
-let alpha_name acc attr =
-   let ns, a = acc in
-   match attr with
-      | E.Name n ->
-        if List.mem n ns then
-            let n = rename ns n in
-           n :: ns, E.Name n :: a
-        else 
-           n :: ns, attr :: a
-      | _        -> assert false 
-
 (* interface functions ******************************************************)
 
-let alpha ns a =
-   let f a names =
-      let _, names = List.fold_left alpha_name (ns, []) (List.rev names) in
-      List.rev_append a names
+let rec alpha mem x a =
+   let err () = a in
+   let f () = match a.E.n_name with
+      | None               -> assert false
+      | Some (token, mode) -> alpha mem x {a with E.n_name = Some (token ^ "_", mode)}
    in
-   E.get_names f a
+   mem err f x a