From 28322ab3b5bb6159909add8d7f61ccef98b3dbd0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Bour?= Date: Wed, 24 Nov 2021 14:29:56 +0100 Subject: [PATCH] Add Indexing module --- src/Fix.ml | 1 + src/Indexing.ml | 154 +++++++++++++++++++++++++++++++++++++++++++++++ src/Indexing.mli | 135 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 290 insertions(+) create mode 100644 src/Indexing.ml create mode 100644 src/Indexing.mli diff --git a/src/Fix.ml b/src/Fix.ml index 212dc3b..2acb291 100644 --- a/src/Fix.ml +++ b/src/Fix.ml @@ -27,6 +27,7 @@ module Glue = Glue module Memoize = Memoize module Numbering = Numbering module GraphNumbering = GraphNumbering +module Indexing = Indexing module Tabulate = Tabulate module Gensym = Gensym module HashCons = HashCons diff --git a/src/Indexing.ml b/src/Indexing.ml new file mode 100644 index 0000000..c2b98a3 --- /dev/null +++ b/src/Indexing.ml @@ -0,0 +1,154 @@ +(******************************************************************************) +(* *) +(* 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 + +type 'n cardinal = int lazy_t + +let cardinal (lazy x : 'n cardinal) : int = x + +type 'n index = int + +module type CARDINAL = sig type n val n : n cardinal end + +module Const(X : sig val cardinal : int end) = +struct + type n + let () = assert (X.cardinal >= 0) + let n = lazy X.cardinal +end + +module Empty = struct + type n + let n = lazy 0 +end + +let const c : (module CARDINAL) = + assert (c >= 0); + (module struct type n let n = lazy c end) + +module Gensym() = struct + type n + let counter = ref 0 + let n = lazy !counter + + let fresh () = + assert (not (Lazy.is_val n)); + let result = !counter in + incr counter; + result +end + +(** Sum of two sets. + These definitions implements the disjoint union operator L + R. *) + +type ('l, 'r) either = + | L of 'l + | R of 'r + +module type SUM = sig + type l and r + include CARDINAL + val inj_l : l index -> n index + val inj_r : r index -> n index + val prj : n index -> (l index, r index) either +end + +module Sum(L : CARDINAL)(R : CARDINAL) = +struct + type n = unit + + type l = L.n + type r = R.n + + let l_n = cardinal L.n + let r_n = R.n + + let n = + if Lazy.is_val r_n then + let n = l_n + cardinal r_n in + lazy n + else + lazy (l_n + cardinal r_n) + + let inj_l x = x + let inj_r y = l_n + y + let prj x = if x < l_n then L x else R (x - l_n) +end + +let sum (type l r) + (l : l cardinal) + (r : r cardinal) = + let module L = struct type n = l let n = l end in + let module R = struct type n = r let n = r end in + (module Sum(L)(R) : SUM with type l = l and type r = r) + +(** Manipulate elements from a finite set *) +module Index = struct + type 'n t = 'n index + + let of_int (c : _ cardinal) i = + let lazy c = c in + assert (i >= 0 && i < c); i + + let to_int i = i + + exception End_of_set + + let enumerate (c : 'n cardinal) = + let c = cardinal c in + let k = ref 0 in + (fun () -> + let result = !k in + if result >= c then raise End_of_set; + incr k; + result) + + let iter (c : 'n cardinal) f = + let lazy c = c in + for i = 0 to c - 1 do + f i + done +end + +(** Manipulate fixed-size vectors, whose domain is a type-level [set] *) +type ('n, 'a) vector = 'a array + +module Vector = struct + type ('n, 'a) t = ('n, 'a) vector + + (* Modular abstraction guarantee that get and set calls are always safe. *) + let get = Array.unsafe_get + let set = Array.unsafe_set + let set_cons t i x = set t i (x :: get t i) + + let length vec = let c = Array.length vec in lazy c + + let empty = [||] + + let make (n : _ cardinal) v = + let n = cardinal n in + Array.make n v + + let make' (n : _ cardinal) f = + let n = cardinal n in + if n = 0 then + empty + else + Array.make n (f ()) + + let init (n : _ cardinal) f = + let n = cardinal n in + Array.init n f + + let map = Array.map +end diff --git a/src/Indexing.mli b/src/Indexing.mli new file mode 100644 index 0000000..2d6bd06 --- /dev/null +++ b/src/Indexing.mli @@ -0,0 +1,135 @@ +(******************************************************************************) +(* *) +(* 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. *) +(* *) +(******************************************************************************) + +(** Type-level indexation: construct types whose values are enforced to belong + to finite sets of integers [0..n-1] and are represented as [int] at + runtime. Two values from different subsets cannot be mixed. + + A phantom parameter ['n] to represent a set at the type-level. +*) + +(** A value of type [c : n cardinal] witnesses the fact that the set [n] has + cardinal [c]. + A [cardinal] is always greater than or equal to 0. +*) +type 'n cardinal + +(** The [cardinal] function returns the cardinal of a set as an integer. + If the set is potentially-growing (produced by the [Gensym] functor below), + calling [cardinal] has the side-effect of fixing the cardinal: + no new elements can be added, calling the [fresh] function is forbidden. +*) +val cardinal : 'n cardinal -> int + +(** A value of type [i : n index] is an integer that is guaranteed to belong + to the set [n]. + If [c : n cardinal], then [0 <= i < c]. + + Note: elements of a finite set are called [index] because their main + purpose is to index information in fixed-size vectors. + See [Vector] sub-module below. +*) +type 'n index = private int + +(** Type-level sets are introduced by modules (to create fresh type names). + A new set is represented by a pair of a fresh abstract type [n] and a + [cardinal] value that represents the cardinal of the set. *) +module type CARDINAL = sig type n val n : n cardinal end + +(** Create a new type for a set with a determined cardinal. *) +module Const(X : sig val cardinal : int end) : CARDINAL +val const : int -> (module CARDINAL) + +(** The empty set *) +module Empty: CARDINAL + +(** "Gensym", for sets whose cardinality is not yet known. + Creates a new set to which elements can be added as long as its cardinal + has not been observed. *) +module Gensym() : sig + include CARDINAL + + (** Add a new element is the set if [cardinal] has not been forced yet. + It is forbidden to call [fresh] after forcing the cardinal. *) + val fresh : unit -> n index +end + +(** Sum of two sets. + These definitions implements the disjoint union operator L + R. *) + +(** The type [either] is used to tell whether a value belongs to the left or + the right set *) +type ('l, 'r) either = + | L of 'l + | R of 'r + +(** The SUM module type. + It defines a set [n] and exposes the isomorphism between [n] and [l + r]. +*) +module type SUM = sig + type l and r + include CARDINAL + val inj_l : l index -> n index + val inj_r : r index -> n index + val prj : n index -> (l index, r index) either +end + +(** Introduce a new set that is the sum of [L] and [R]. + It is strict in [L.cardinal] but not [R.cardinal]: if [R] is an instance + of [Gensym()] that has not been forced, new elements can still be added. + Forcing the resulting cardinal forces [R.cardinal] too. +*) +module Sum(L : CARDINAL)(R : CARDINAL) : + SUM with type l := L.n + and type r := R.n + +val sum : 'l cardinal -> 'r cardinal -> + (module SUM with type l = 'l and type r = 'r) + +(** Manipulate elements from a finite set *) +module Index : sig + type 'n t = 'n index + + (** [of_int cardinal n] returns [n] at a finer index type, witnessing that + the value belongs to the finite set defined by [ 0 .. cardinal [. + It is forbidden to call [of_int] when [n] is outside of this interval. *) + val of_int : 'n cardinal -> int -> 'n index + + val to_int : 'n index -> int + + (** [enumerate cardinal] returns an imperative iterator, that will return + indexes from 0 to cardinal-1, increasing after each call. + Calling again after reaching cardinal-1 raises [End_of_set]. *) + val enumerate : 'n cardinal -> (unit -> 'n index) + exception End_of_set + + val iter : 'n cardinal -> ('n index -> unit) -> unit +end + +(** Manipulate fixed-size vectors, whose domain is a type-level [set] *) +type ('n, 'a) vector = private 'a array + +module Vector : sig + type ('n, 'a) t = ('n, 'a) vector + + val get : ('n, 'a) t -> 'n index -> 'a + val set : ('n, 'a) t -> 'n index -> 'a -> unit + val set_cons : ('n, 'a list) t -> 'n index -> 'a -> unit + + val length : ('n, 'a) t -> 'n cardinal + val empty : (_, _) t + + val make : 'n cardinal -> 'a -> ('n, 'a) t + val make' : 'n cardinal -> (unit -> 'a) -> ('n, 'a) t + val init : 'n cardinal -> ('n index -> 'a) -> ('n, 'a) t + val map : ('a -> 'b) -> ('n, 'a) t -> ('n, 'b) t +end -- GitLab