var.ml 2.38 KB
Newer Older
1
module V = struct
2

3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

  type kind = Source | Internal

  type t = { name : Ident.U.t ;
	     id : int ;
	     kind : kind }

  let print_kind ppf k = Format.fprintf ppf "%s"
    (match k with Source -> "Source" | Internal -> "Internal")

  let compare_kind k1 k2 = if k1 == k2 then 0 else if k1 < k2 then -1 else 1

  let dump ppf t =
    Format.fprintf ppf "%a(%d_%a)" Ident.U.print t.name t.id print_kind t.kind

  let compare x y =
    let c = compare_kind x.kind y.kind in
    if c == 0 then
      let c = Pervasives.compare x.id y.id in
      if c == 0 then Ident.U.compare x.name y.name
      else c
    else c

26
  let equal x y =
27
    x == y || (x.kind == y.kind && x.id == y.id && Ident.U.equal x.name y.name)
28

29
  let hash x = Hashtbl.hash (x.id,x.name,x.kind)
30

31
  let check x = assert (x.id >= 0)
32

33
34
35
  let refresh v =
    (* according to Alain, a thread safe way to generate a unique ID *)
    { v with id = Oo.id (object end) }
36

37
38
39
40
41
  let mk ?(internal=false) id = { name = Ident.U.mk id;
				  id = 0;
				  kind = if internal then Internal else Source;
				}
  let is_internal x = x.kind == Internal
42

43
44
  let ident x = Ident.U.get_str x.name
  let print ppf x = Format.fprintf ppf "'%a" Ident.U.print x.name
45
46
end

47

48

Pietro Abate's avatar
Pietro Abate committed
49
module Set = struct
50
51
  include SortedList.Make(V)
  let dump ppf s = Utils.pp_list ~sep:";" ~delim:("{","}") V.dump ppf (get s)
52
  let print ppf s = Utils.pp_list ~sep:";" ~delim:("{","}") V.print ppf (get s)
Pietro Abate's avatar
Pietro Abate committed
53
end
54

55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

include V
let gen set =
  let idx = ref 0 in
  let rec freshvar () =
    let rec pretty i acc =
      let ni,nm = i/26, i mod 26 in
      let acc = acc ^
        (String.make 1 (Char.chr (Char.code 'a' + nm)))
      in
      if ni == 0 then acc else pretty ni acc
    in
    let x = mk (pretty !idx "") in
    if Set.mem set x then
      (* if the name is taken by a variable in delta, restart *)
      (incr idx; freshvar ())
    else x
  in
  freshvar ()

75
type 'a var_or_atom = [ `Atm of 'a | `Var of t ]
76

77
module Make (X : Custom.T) = struct
78
79
  type t = X.t var_or_atom
  let hash = function `Atm t -> 17 + 17 * X.hash t | `Var x -> 997 + 17 * V.hash x
80

81
  let check = function `Atm t -> X.check t | `Var _ -> ()
82

83
84
  let compare t1 t2 =
    match t1,t2 with
85
    |`Var x, `Var y -> compare x y
86
87
88
89
    |`Atm x, `Atm y -> X.compare x y
    |`Var _, `Atm _ -> -1
    |`Atm _, `Var _ -> 1

90
  let equal t1 t2 = (compare t1 t2) == 0
91

92
93
  let dump ppf = function
    |`Atm x -> X.dump ppf x
94
    |`Var x -> V.dump ppf x
95
end
96