Source file idGenerator.ml

(** This module implements various useful modules to generate IDs and
    to keep track of there association with string as in a symbol table *)

module Log = Xlog.Make (struct
  let name = "IdGenerator"
end)

(** Signature of modules encoding symbol tables *)
module type CorrespondanceTableTYPE = sig
  type identifier
  (** [identifier] is the type of the identifier stored in the
      table. It is meant to be associated with a [string] *)

  type table
  (** The type of the table *)

  val empty : table
  (** [empty] is an empty table *)

  val find_id_of_sym : string -> table -> identifier option
  (** [find_id_of_sym sym t] returns [Some id] where [id] is the
     identifier of the string [sym] stored in [t], and returns [None]
     if no such identifier exists. *)

  val find_sym_from_id : identifier -> table -> string
  (** [find_sym_from_id id t] returns the string (i.e. the symbol)
     corresponding to the identifier [id] in table [t]. *)

  val add_sym : string -> table -> identifier * table
  (** [add_sym sym t] returns a pair [(id,t')] where [id] is the
      identifier associated with [sym] in [t']. If [sym] already was
      in [t] then [t']=[t] and [id] is the identifier which it was
      associated with. Otherwise, a new identifier is generated and
      the new association is stored in [t'].*)

  val pp : Format.formatter -> table -> unit
  (** [pp f t] pretty prints the table [t] on the formatter [f] *)

  val fold : (identifier -> string -> 'a -> 'a) -> table -> 'a -> 'a
  (** [fold f table a] returns [f id1 sym1 (f id2 sym2 ( ... ( f idN
      symN a) ... ))] where the [(id,sym)] pairs are the ones that are
      stored in the table [table]. The order of these key-value pairs in
      the table is unspecified. *)
end

(** Signature of modules encoding a generator of identifiers *)
module type IdGen_TYPE = sig
  type id
  (** The type of the identifier generated *)

  type t
  (** The type of the generator *)

  val init : unit -> t
  (** [init ()] returns a new generator *)

  val get_fresh_id : t -> id * t
  (** [get_fresh_id gen] returnds a pair [(id,gen')] where [id] is a
      fresh [id] and [gen'] a new generator that knows [id] was already
      generated.*)

  val eq : id -> id -> bool
  (** [eq id1 id2] returns [true] if [id1=id2] and [fase] otherwise. *)

  val compare : id -> id -> int
  (** [compare id1 id2] returns an integer which is [0] if [id1=id2],
      negative of [id1] is less than [id2] and positive otherwise. *)

  val id_to_string : id -> string

  module IdMap : Map.S with type key = id
  (** [IdMap] implements maps whose keys are identifiers *)

  module Table : CorrespondanceTableTYPE with type identifier = id
  (** [Table] implements correspondance tables with the current
      identifiers *)
end

(** Signature of encoding identifiers *)
module type IdType = sig
  type t
  (** The type of the identifiers *)

  val compare : t -> t -> int
  (** [compare id1 id2] returns an integer which is [0] if [id1=id2],
      negative of [id1] is less than [id2] and positive otherwise. *)

  val succ : t -> t
  (** [succ id] returns a new identifer strictly greater than [id] *)

  val start : t
  (** [start] is some identifer *)

  val to_string : t -> string
  (** [to_string id] returns a string describing the identifier *)

  val pp : Format.formatter -> t -> unit
  (** [pp f id] pretty prints the id [id] on the formatter [f] *)
end

(** This module is a functor that generates a identifier generator
    from a module implementing these identifiers *)

module IdGen (ID : IdType) = struct
  type id = ID.t
  type t = Generator of id

  let init () = Generator ID.start
  let get_fresh_id (Generator n) = (n, Generator (ID.succ n))
  let eq i j = ID.compare i j = 0
  let compare = ID.compare
  let id_to_string = ID.to_string

  module IdMap = Map.Make (ID)

  module Table = struct
    type identifier = id
    type table = { symbols : id Tries.Tries.t; ids : string IdMap.t; gen : t }

    let empty =
      { symbols = Tries.Tries.empty; ids = IdMap.empty; gen = init () }

    let find_id_of_sym symbol { symbols = table; ids = _; gen = _ } =
      Tries.Tries.find symbol table

    let find_sym_from_id id { symbols = _; ids = table; gen = _ } =
      match IdMap.find_opt id table with
      | None -> 
        let () = Log.err (fun m -> m "id '%s' not found in table." (ID.to_string id)) in
        assert false
      | Some v -> v

    let add_sym sym ({ symbols = syms; ids; gen = vargen } as table) =
      match Tries.Tries.find sym syms with
      | Some v -> (v, table)
      | None ->
        let new_var, new_vargen = get_fresh_id vargen in
        ( new_var,
          {
            symbols = Option.get (Tries.Tries.add sym new_var syms);
            ids = IdMap.add new_var sym ids;
            gen = new_vargen;
          } )

    let idmap_pp m map =
      IdMap.iter
        (fun key value -> Format.fprintf m "@[%a ->@ %30s@]" ID.pp key value)
        map

    let pp m { symbols = syms; ids; gen = _ } =
      let () =
        Format.fprintf m "@[Table from symbols to ids:@\n@[<v 3>%a]@]@."
          (Tries.Tries.pp (fun fmt sym id ->
               Format.fprintf fmt "%10s -> %a" sym ID.pp id))
          syms
      in
      Format.fprintf m "@[Table from symbols to ids:@\n@[<v 3>%a]@]@." idmap_pp
        ids

    let fold f table start = IdMap.fold f table.ids start
  end
end

module IntId = struct
  type t = int

  let compare i j = i - j
  let succ i = i + 1
  let start = 0
  let to_string = string_of_int
  let pp = Format.pp_print_int
end

module IntIdGen = IdGen (IntId)
(** Module implementing the special case where identifiers ar
    integers. *)