helm/software/lambda-delta/src/common/alpha.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module E = Entity
  13
  14 (* internal functions *******************************************************)
  15
  16 let rec rename ns n =
  17    let token, mode = n in
  18    let n = token ^ "_", mode in
  19    if List.mem n ns then rename ns n else n
  20
  21 let alpha_name acc attr =
  22    let ns, a = acc in
  23    match attr with
  24       | E.Name n ->
  25          if List.mem n ns then
  26             let n = rename ns n in
  27             n :: ns, E.Name n :: a
  28          else
  29             n :: ns, attr :: a
  30       | _        -> assert false
  31
  32 (* interface functions ******************************************************)
  33
  34 let alpha ns a =
  35    let f a names =
  36       let _, names = List.fold_left alpha_name (ns, []) (List.rev names) in
  37       List.rev_append a names
  38    in
  39    E.get_names f a