type t = { fresh : bool; id : string; } let make_id ?(fresh=false) id = { id = id ; fresh = fresh } let dump ppf t = Format.fprintf ppf "{id=%s;fresh=%b}" t.id t.fresh let compare x y = Pervasives.compare x.id y.id let equal x y = Pervasives.compare x.id y.id = 0 let hash x = Hashtbl.hash x.id type var = [ `Var of t ] type 'a pairvar = [ `Atm of 'a | var ] let dump ppf (`Var x) = Format.fprintf ppf "%a" dump x let print ppf (`Var x) = Format.fprintf ppf "`$%s" x.id let compare (`Var x) (`Var y) = compare x y let equal v1 v2 = (compare v1 v2) = 0 let id (`Var t) = t.id let is_fresh (`Var t) = t.fresh module Set = struct include Set.Make( struct type t = var let compare = compare end) let aux_print sep printer ppf s = let rec aux ppf = function |[] -> () |[h] -> printer ppf h |h::l -> Format.fprintf ppf "%a %s %a" printer h sep aux l in aux ppf (elements s) let dump ppf s = aux_print ";" dump ppf s let print ppf s = aux_print ";" print ppf s let is_empty s = equal s empty let from_list l = List.fold_left (fun acc x -> add x acc) empty l end module Make (X : Custom.T) = struct type t = X.t pairvar let hash = function `Atm t -> X.hash t | `Var x -> hash x let check = function `Atm t -> X.check t | `Var _ -> () let compare t1 t2 = match t1,t2 with |`Var x, `Var y -> compare (`Var x) (`Var y) |`Atm x, `Atm y -> X.compare x y |`Var _, `Atm _ -> -1 |`Atm _, `Var _ -> 1 let equal t1 t2 = (compare t1 t2) = 0 let dump ppf = function |`Atm x -> X.dump ppf x |`Var x -> dump ppf (`Var x) end let mk ?fresh id = `Var (make_id ?fresh id) let fresh : ?pre: string -> unit -> [> var ] = let counter = ref 0 in fun ?(pre="_fresh_") -> fun _ -> let id = (Printf.sprintf "%s%d" pre !counter) in let v = mk ~fresh:true id in incr counter; v