Commit c5d81829 authored by POTTIER Francois's avatar POTTIER Francois

New module [Numbering].

parent 1c54abc7
......@@ -9,6 +9,10 @@
which not only returns a memoized function,
but also provides outside access to the memoization table.
* New signature `ONGOING_NUMBERING`
and new module `Numbering`,
which provides facilities for numbering things.
## 2018/11/30
* New release, including new modules (`Gensym`, `Memoize`,
......
......@@ -28,6 +28,10 @@ This gives you access to the following submodules:
* [`Number`](src/Number.mli) offers a facility for
**discovering and numbering the reachable vertices** in a directed graph.
* [`Numbering`](src/Numbering.mli) offers a facility for
**assigning a unique number** to each value in a certain finite set
and translating (both ways) between values and their numbers.
* [`HashCons`](src/HashCons.mli) offers support for
**setting up a hash-consed data type**, that is, a data type whose
values carry unique integer identifiers.
......
......@@ -23,12 +23,13 @@ include Sigs
declared [open Fix], then she can use [Glue], [Memoize], etc. If she
hasn't, then she must use [Fix.Glue], [Fix.Memoize], etc. *)
module Glue = Glue
module Memoize = Memoize
module Number = Number
module Tabulate = Tabulate
module Gensym = Gensym
module HashCons = HashCons
module Glue = Glue
module Memoize = Memoize
module Number = Number
module Numbering = Numbering
module Tabulate = Tabulate
module Gensym = Gensym
module HashCons = HashCons
module Prop = struct
(* A number of ready-made implementations of the signature [PROPERTY]. *)
......
(******************************************************************************)
(* *)
(* Fix *)
(* *)
(* François Pottier, Inria Paris *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the GNU Library General Public License version 2, with a *)
(* special exception on linking, as described in the file LICENSE. *)
(* *)
(******************************************************************************)
open Sigs
let force o =
match o with Some x -> x | None -> assert false
module Make (M : IMPERATIVE_MAPS) = struct
type t = M.key
(* Create a generator of fresh integers. *)
open Gensym
let g =
generator()
let current () =
current g
(* Memoizing the function [fun _ -> fresh g] yields the function [encode],
which maps keys to unique integers. We use [visibly_memoize] so as to
have access to the memoization table. This allows us to use operations
such as [M.find] and [M.iter] below. *)
let (encode : t -> int), (table : int M.t) =
let module Memo = Memoize.Make(M) in
Memo.visibly_memoize (fun (_ : t) -> fresh g)
(* Testing whether a key has been encountered already. *)
let has_been_encoded (x : t) : bool =
(* We do not have [M.mem], so we re-implement it in terms of [M.find]. *)
try
let _ = M.find x table in
true
with Not_found ->
false
(* Building a mapping of integer codes back to keys. *)
let reverse_mapping () : t array =
let n = current() in
let reverse : t option array = Array.make n None in
M.iter (fun x i ->
reverse.(i) <- Some x
) table;
Array.map force reverse
module Done () = struct
type t = M.key
let n = current()
let encode = encode
let decode = Array.get (reverse_mapping())
end
end
(******************************************************************************)
(* *)
(* Fix *)
(* *)
(* François Pottier, Inria Paris *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the GNU Library General Public License version 2, with a *)
(* special exception on linking, as described in the file LICENSE. *)
(* *)
(******************************************************************************)
open Sigs
(* The functor [Make] requires an implementation of maps for the type [M.key]
and offers a numbering facility. A typical numbering process is organized
in two phases. During the first phase, the numbering is ongoing; one can
encode keys, but not decode. Applying the functor [Done()] ends the first
phase. A fixed numbering then becomes available, which gives access to the
total number [n] of encoded keys and to both [encode] and [decode]. The
function [decode] is backed by an array of size [n], therefore runs in
constant time. *)
module Make (M : IMPERATIVE_MAPS) : sig
include ONGOING_NUMBERING with type t = M.key
module Done () : NUMBERING with type t = M.key
end
......@@ -203,6 +203,21 @@ end
(* Numberings. *)
(* An ongoing numbering of (a subset of) a type [t] offers a function [encode]
which maps a value of type [t] to a unique integer code. If applied twice
to the same value, [encode] returns the same code; if applied to a value
that has never been encountered, it returns a fresh code. The function
[current] returns the next available code, which is also the number of
values that have been encoded so far. The function [has_been_encoded] tests
whether a value has been encoded already. *)
module type ONGOING_NUMBERING = sig
type t
val encode: t -> int
val current: unit -> int
val has_been_encoded: t -> bool
end
(* A numbering of (a subset of) a type [t] is a triple of an integer [n] and
two functions [encode] and [decode] which represent an isomorphism between
this subset of [t] and the interval [0..n). *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment