From e2b2324f3d32ffabfb35a405894b8ca249090e94 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Fri, 24 Dec 2021 15:19:00 +0100
Subject: [PATCH] Split into three packages feat-core, feat, feat-num.
---
CHANGES.md | 26 +++++
Makefile | 50 +++++---
demo/Test.ml | 41 +++++--
demo/dune | 5 -
demo/with-feat-num/dune | 7 ++
demo/with-feat/dune | 7 ++
feat-core.opam | 19 +++
feat-core/BigIntSig.ml | 43 +++++++
{src => feat-core}/Enum.ml | 8 +-
feat-core/Enum.mli | 14 +++
feat-core/EnumSig.ml | 130 +++++++++++++++++++++
{src => feat-core}/IFSeq.ml | 19 ++-
{src => feat-core}/IFSeq.mli | 24 ++--
{src => feat-core}/IFSeqList.ml | 0
{src => feat-core}/IFSeqList.mli | 4 +-
{src => feat-core}/IFSeqObj.ml | 16 +--
{src => feat-core}/IFSeqObj.mli | 17 +--
{src => feat-core}/IFSeqSig.ml | 69 +++++++----
{src => feat-core}/IFSeqSyn.ml | 16 +--
{src => feat-core}/IFSeqSyn.mli | 17 +--
{src => feat-core}/Makefile | 0
src/bigint.ml => feat-core/RandomBigInt.ml | 18 ++-
feat-core/RandomBigInt.mli | 17 +++
feat-core/RandomSig.ml | 32 +++++
feat-core/dune | 6 +
feat-num.opam | 19 +++
feat-num/Enum.ml | 11 ++
feat-num/Enum.mli | 11 ++
feat-num/IFSeq.ml | 11 ++
src/bigint.mli => feat-num/IFSeq.mli | 4 +-
feat-num/Makefile | 3 +
feat-num/Num.ml | 33 ++++++
feat-num/Num.mli | 13 +++
feat-num/dune | 6 +
feat.opam | 5 +-
feat/Enum.ml | 11 ++
feat/Enum.mli | 11 ++
feat/IFSeq.ml | 11 ++
feat/IFSeq.mli | 11 ++
feat/Makefile | 3 +
feat/Num.ml | 11 ++
feat/Num.mli | 13 +++
feat/dune | 6 +
src/Enum.mli | 113 ------------------
src/dune | 7 --
45 files changed, 644 insertions(+), 274 deletions(-)
create mode 100644 CHANGES.md
delete mode 100644 demo/dune
create mode 100644 demo/with-feat-num/dune
create mode 100644 demo/with-feat/dune
create mode 100644 feat-core.opam
create mode 100644 feat-core/BigIntSig.ml
rename {src => feat-core}/Enum.ml (97%)
create mode 100644 feat-core/Enum.mli
create mode 100644 feat-core/EnumSig.ml
rename {src => feat-core}/IFSeq.ml (74%)
rename {src => feat-core}/IFSeq.mli (54%)
rename {src => feat-core}/IFSeqList.ml (100%)
rename {src => feat-core}/IFSeqList.mli (90%)
rename {src => feat-core}/IFSeqObj.ml (94%)
rename {src => feat-core}/IFSeqObj.mli (76%)
rename {src => feat-core}/IFSeqSig.ml (55%)
rename {src => feat-core}/IFSeqSyn.ml (95%)
rename {src => feat-core}/IFSeqSyn.mli (75%)
rename {src => feat-core}/Makefile (100%)
rename src/bigint.ml => feat-core/RandomBigInt.ml (86%)
create mode 100644 feat-core/RandomBigInt.mli
create mode 100644 feat-core/RandomSig.ml
create mode 100644 feat-core/dune
create mode 100644 feat-num.opam
create mode 100644 feat-num/Enum.ml
create mode 100644 feat-num/Enum.mli
create mode 100644 feat-num/IFSeq.ml
rename src/bigint.mli => feat-num/IFSeq.mli (90%)
create mode 100644 feat-num/Makefile
create mode 100644 feat-num/Num.ml
create mode 100644 feat-num/Num.mli
create mode 100644 feat-num/dune
create mode 100644 feat/Enum.ml
create mode 100644 feat/Enum.mli
create mode 100644 feat/IFSeq.ml
create mode 100644 feat/IFSeq.mli
create mode 100644 feat/Makefile
create mode 100644 feat/Num.ml
create mode 100644 feat/Num.mli
create mode 100644 feat/dune
delete mode 100644 src/Enum.mli
delete mode 100644 src/dune
diff --git a/CHANGES.md b/CHANGES.md
new file mode 100644
index 0000000..d9fea0e
--- /dev/null
+++ b/CHANGES.md
@@ -0,0 +1,26 @@
+# CHANGES
+
+## 2021/12/24
+
+* The library is now split in three packages: `feat-core`, `feat`, and
+ `feat-num`. `feat-core` is parameterized over an implementation of big
+ integers and over a random number generator. `feat` instantiates `feat-core`
+ with big integers from the library `zarith` and with OCaml's standard random
+ number generator. `feat-num` instantiates `feat-core` with big integers from
+ the library `num` and with OCaml's standard random number generator. The
+ packages `feat` and `feat-num` offer the same API and are interchangeable.
+ (See `demo/with-feat` and `demo/with-feat-num` to see how the same code can
+ be linked with either package.) The three submodules offered both by `feat`
+ and by `feat-num` are `Num`, `IFSeq`, and `Enum`. Compatibility with the
+ previous release of `feat` should be complete as long as only the submodules
+ `IFSeq` and `Enum` were used. (Contributed by Jonah Beckford; reviewed and
+ adapted by François Pottier.)
+
+* Avoid inadvertent uses of OCaml's polymorphic comparison operators on big
+ integers.
+
+* Improved documentation.
+
+## 2020/12/31
+
+* Initial release.
diff --git a/Makefile b/Makefile
index f42699b..42dce89 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,12 @@
# ------------------------------------------------------------------------------
-# The name of the library.
+# The name of the repository.
THIS := feat
+# The libraries (topologically sorted).
+THIS_COMMAS := feat-core,feat,feat-num
+THIS_SPACES := feat-core feat feat-num
+
# The version number is automatically set to the current date,
# unless DATE is defined on the command line.
DATE := $(shell /bin/date +%Y%m%d)
@@ -21,12 +25,13 @@ all:
.PHONY: install
install:
- @ dune build -p $(THIS)
- @ dune install -p $(THIS)
+ @ dune build -p $(THIS_COMMAS)
+ @ dune install -p $(THIS_COMMAS)
.PHONY: clean
clean:
- @ rm -f *~ src/*~ dune-workspace.versions
+ @ rm -f dune-workspace.versions
+ @ $(FIND) . -name "*~" | xargs rm -f
@ dune clean
.PHONY: test
@@ -35,7 +40,7 @@ test:
.PHONY: uninstall
uninstall:
- @ ocamlfind remove $(THIS) || true
+ @ for t in $(THIS_SPACES) ; do ocamlfind remove $$t; done || true
.PHONY: reinstall
reinstall: uninstall
@@ -43,18 +48,15 @@ reinstall: uninstall
.PHONY: show
show: reinstall
- @ echo "#require \"feat\";;\n#show Feat;;" | ocaml
+ @ echo "#require \"feat-core\";;\n#require \"feat\";;\n#require \"feat-num\";;\n#show FeatCore;;\n#show Feat;;\n#show FeatNum;;" | ocaml
.PHONY: pin
pin:
- @ opam pin add $(THIS) .
+ @ for d in $(THIS_SPACES) ; do opam pin --yes add $$d . ; done
.PHONY: unpin
unpin:
- @ opam pin remove $(THIS)
-
-# This requires a version of headache that supports UTF-8; please use
-# https://github.com/fpottier/headache
+ @ opam pin --yes remove $(THIS_SPACES)
HEADACHE := headache
LIBHEAD := $(shell pwd)/headers/library-header
@@ -62,8 +64,10 @@ FIND := $(shell if command -v gfind >/dev/null ; then echo gfind ; else echo
.PHONY: headache
headache:
- @ $(FIND) src -regex ".*\.ml\(i\|y\|l\)?" \
- -exec $(HEADACHE) -h $(LIBHEAD) "{}" ";"
+ @ for d in $(THIS_SPACES) demo ; do \
+ $(FIND) $$d -regex ".*\.ml\(i\|y\|l\)?" \
+ -exec $(HEADACHE) -h $(LIBHEAD) "{}" ";" ; \
+ done
.PHONY: release
release:
@@ -87,11 +91,16 @@ release:
# Upload. (This automatically makes a .tar.gz archive available on gitlab.)
@ git push
@ git push --tags
+# Done.
+ @ echo "Done."
+ @ echo "If happy, please type:"
+ @ echo " \"make publish\" to publish a new opam package"
+ @ echo " \"make export\" to upload the documentation to yquem.inria.fr"
.PHONY: publish
publish:
# Publish an opam description.
- @ opam publish -v $(DATE) $(THIS) $(ARCHIVE) .
+ @ opam publish -v $(DATE) $(THIS_SPACES) $(ARCHIVE)
DOCDIR = _build/default/_doc/_html
DOC = $(DOCDIR)/index.html
@@ -135,6 +144,15 @@ VERSIONS := \
4.09.0+bytecode-only \
4.10.0 \
4.11.1 \
+ 4.12.0 \
+ 4.13.0 \
+
+.PHONY: switches
+switches:
+ @ for v in $(VERSIONS) ; do \
+ opam switch create $$v || \
+ opam install --switch $$v --yes zarith seq fix num; \
+ done
.PHONY: versions
versions:
@@ -149,7 +167,7 @@ handiwork:
@ current=`opam switch show` ; \
for v in $(VERSIONS) ; do \
opam switch $$v && \
- eval $$(opam env) && \
- opam install --yes zarith seq fix.20201120 ; \
+ eval $$(opam env --switch=$$v) && \
+ opam install --yes zarith seq fix.20201120 num; \
done ; \
opam switch $$current
diff --git a/demo/Test.ml b/demo/Test.ml
index 2166d32..8fd03be 100644
--- a/demo/Test.ml
+++ b/demo/Test.ml
@@ -1,6 +1,23 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+(* This demo is written in such a way as to work both with feat (which relies
+ on zarith) and with feat-num (which relies on num). Both feat and feat-num
+ expose a main module (named either Feat or FeatNum) with three submodules
+ named Num, IFSeq, and Enum. We assume that a suitable -open flags has been
+ passed, so these three submodules are available. *)
+
open Printf
open Fix.Memoize.Int
-open Feat.Enum
+let succ i = Num.add i Num.one
+open Enum
(* -------------------------------------------------------------------------- *)
@@ -37,7 +54,7 @@ let list_wb_tree : tree list enum =
(* Enumerating binary trees with two elements in [0; 1]. *)
let elem : int enum =
- enum (Feat.IFSeq.up 0 2)
+ enum (IFSeq.up 0 2)
let etree : tree enum =
fix (fun tree ->
@@ -48,12 +65,12 @@ let etree : tree enum =
(* Testing a sequence. *)
-open Feat.IFSeq
+open IFSeq
let rec subrange i j s accu =
- if i < j then
+ if Num.lt i j then
let accu = get s i :: accu in
- subrange (Z.succ i) j s accu
+ subrange (succ i) j s accu
else
List.rev accu
@@ -61,26 +78,26 @@ let subrange i j s =
subrange i j s []
let range s =
- subrange Z.zero (length s) s
+ subrange Num.zero (length s) s
let test name s =
printf "Testing %s...\n%!" name;
(* Test [length]. *)
- printf " Length: %s\n%!" (Z.to_string (length s));
+ printf " Length: %s\n%!" (Num.to_string (length s));
(* By calling [range s], test [get] at every index within range. *)
- assert (Z.equal (length s) (Z.of_int (List.length (range s))));
+ assert (Num.equal (length s) (Num.of_int (List.length (range s))));
printf " Every random access succeeds.\n";
(* Test [foreach]. We check that it produces the same elements as [get],
in the same order, and that it produces neither too few nor too many
elements. *)
- let i = ref Z.zero in
+ let i = ref Num.zero in
foreach s (fun x1 ->
- assert (Z.lt !i (length s));
+ assert (Num.lt !i (length s));
let x2 = get s !i in
assert (x1 = x2); (* element equality *)
- i := Z.succ !i
+ i := succ !i
);
- assert (Z.equal !i (length s));
+ assert (Num.equal !i (length s));
printf " Iteration via foreach is consistent with random access.\n"
(* -------------------------------------------------------------------------- *)
diff --git a/demo/dune b/demo/dune
deleted file mode 100644
index 386130f..0000000
--- a/demo/dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(test
- (name Test)
- (libraries unix fix zarith feat)
- (flags :standard "-w" "A-44")
-)
diff --git a/demo/with-feat-num/dune b/demo/with-feat-num/dune
new file mode 100644
index 0000000..af5fb2b
--- /dev/null
+++ b/demo/with-feat-num/dune
@@ -0,0 +1,7 @@
+(copy_files ../Test.ml)
+
+(test
+ (name Test)
+ (libraries fix feat-num)
+ (flags :standard "-w" "A-44-70" "-open" "FeatNum")
+)
diff --git a/demo/with-feat/dune b/demo/with-feat/dune
new file mode 100644
index 0000000..72787e4
--- /dev/null
+++ b/demo/with-feat/dune
@@ -0,0 +1,7 @@
+(copy_files ../Test.ml)
+
+(test
+ (name Test)
+ (libraries fix feat)
+ (flags :standard "-w" "A-44-70" "-open" "Feat")
+)
diff --git a/feat-core.opam b/feat-core.opam
new file mode 100644
index 0000000..0b58a57
--- /dev/null
+++ b/feat-core.opam
@@ -0,0 +1,19 @@
+name: "feat-core"
+opam-version: "2.0"
+maintainer: "francois.pottier@inria.fr"
+authors: [
+ "François Pottier <francois.pottier@inria.fr>"
+]
+homepage: "https://gitlab.inria.fr/fpottier/feat"
+dev-repo: "git+https://gitlab.inria.fr/fpottier/feat.git"
+bug-reports: "francois.pottier@inria.fr"
+build: [
+ ["dune" "build" "-p" name "-j" jobs]
+]
+depends: [
+ "ocaml" { >= "4.03" }
+ "dune" { >= "1.3" }
+ "seq"
+ "fix" { >= "20181206" }
+]
+synopsis: "Facilities for enumerating and sampling algebraic data types"
diff --git a/feat-core/BigIntSig.ml b/feat-core/BigIntSig.ml
new file mode 100644
index 0000000..99e9ab7
--- /dev/null
+++ b/feat-core/BigIntSig.ml
@@ -0,0 +1,43 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+(**A signature for big numbers that is satisfied both by [Zarith] and
+ by the older, slower but license-friendly [Num] package. This minimal
+ signature is required by {!IFSeqSyn} and {!IFSeqObj}. *)
+module type BASIC = sig
+ type t
+ val zero : t
+ val one : t
+ val pred : t -> t
+ val add : t -> t -> t
+ val sub : t -> t -> t
+ val mul : t -> t -> t
+ val div_rem : t -> t -> t * t
+ val equal : t -> t -> bool
+ val lt : t -> t -> bool
+ val of_int : int -> t
+ exception Overflow
+ val to_int : t -> int
+end
+
+(**An extended signature for big numbers, providing more functionality. This
+ signature is required by {!RandomBigInt} and by the modules that depend
+ on it, such as {!IFSeq}. *)
+module type EXTENDED = sig
+ include BASIC
+ val leq: t -> t -> bool
+ val geq: t -> t -> bool
+ val (/): t -> t -> t
+ val ( * ): t -> t -> t
+ val (mod): t -> t -> t
+ val (lsl): t -> int -> t
+ val (lor): t -> t -> t
+ val to_string: t -> string
+end
diff --git a/src/Enum.ml b/feat-core/Enum.ml
similarity index 97%
rename from src/Enum.ml
rename to feat-core/Enum.ml
index 89809c0..df49cda 100644
--- a/src/Enum.ml
+++ b/feat-core/Enum.ml
@@ -8,7 +8,11 @@
(* terms of the MIT license, as described in the file LICENSE. *)
(******************************************************************************)
-(* -------------------------------------------------------------------------- *)
+open IFSeqSig
+
+module Make (IFSeq : IFSEQ_EXTENDED) = struct
+
+module IFSeq = IFSeq
(* Core combinators. *)
@@ -124,3 +128,5 @@ let rec sample m e i j k =
IFSeq.sample m (e i) (fun () -> sample m e (i + 1) j k ())
else
k
+
+end
diff --git a/feat-core/Enum.mli b/feat-core/Enum.mli
new file mode 100644
index 0000000..d5a205e
--- /dev/null
+++ b/feat-core/Enum.mli
@@ -0,0 +1,14 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+open IFSeqSig
+open EnumSig
+
+module Make (IFSeq : IFSEQ_EXTENDED) : ENUM with module IFSeq = IFSeq
diff --git a/feat-core/EnumSig.ml b/feat-core/EnumSig.ml
new file mode 100644
index 0000000..da07fc3
--- /dev/null
+++ b/feat-core/EnumSig.ml
@@ -0,0 +1,130 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+open IFSeqSig
+
+(**This is the result signature of the functor {!Enum.Make}. *)
+module type ENUM = sig
+
+ (**This implementation of implicit finite sequences is used as a building
+ block in the definition of the type {!type-enum}, which follows. *)
+ module IFSeq : IFSEQ_EXTENDED
+
+ (**An enumeration of type ['a enum] can be loosely thought of as a set of
+ values of type ['a], equipped with a notion of size. More precisely, it
+ is a function of a size [s] to a subset of inhabitants of size [s],
+ presented as a sequence.
+
+ We expose the fact that enumerations are functions, instead of making
+ [enum] an abstract type, because this allows the user to make recursive
+ definitions. It is up to the user to ensure that recursion is
+ well-founded; as a rule of thumb, every recursive call must appear under
+ {!pay}. It is also up to the user to take precautions so that these
+ functions have constant time complexity (beyond the cost of an
+ initialization phase). This is typically achieved by using a memoizing
+ fixed point combinator instead of an ordinary recursive definition. *)
+ type 'a enum =
+ int -> 'a IFSeq.seq
+
+ (**[empty] is the empty enumeration. *)
+ val empty: 'a enum
+
+ (**[zero] is a synonym for [empty]. *)
+ val zero : 'a enum
+
+ (**The enumeration [just x] contains just the element [x], with size zero.
+ [just x] is equivalent to [finite [x]]. *)
+ val just: 'a -> 'a enum
+
+ (**The enumeration [enum x] contains the elements in the sequence [xs], with
+ size zero. *)
+ val enum: 'a IFSeq.seq -> 'a enum
+
+ (**The enumeration [pay e] contains the same elements as [e], with a size
+ that is increased by one with respect to [e]. *)
+ val pay: 'a enum -> 'a enum
+
+ (**[sum e1 e2] is the union of the enumerations [e1] and [e2]. It is up to
+ the user to ensure that the sets [e1] and [e2] are disjoint. *)
+ val sum : 'a enum -> 'a enum -> 'a enum
+
+ (**[(++)] is a synonym for [sum]. *)
+ val ( ++ ) : 'a enum -> 'a enum -> 'a enum
+
+ (**[exists xs e] is the union of all enumerations of the form [e x], where
+ [x] is drawn from the list [xs]. (This is an indexed sum.) It is up to
+ the user to ensure that the sets [e1] and [e2] are disjoint. *)
+ val exists: 'a list -> ('a -> 'b enum) -> 'b enum
+
+ (**[product e1 e2] is the Cartesian product of the enumerations
+ [e1] and [e2]. *)
+ val product: 'a enum -> 'b enum -> ('a * 'b) enum
+
+ (**[( ** )] is a synonym for [product]. *)
+ val ( ** ) : 'a enum -> 'b enum -> ('a * 'b) enum
+
+ (**[balanced_product e1 e2] is a subset of the Cartesian product [product e1
+ e2] where the sizes of the left-hand and right-hand pair components must
+ differ by at most one. *)
+ val balanced_product: 'a enum -> 'b enum -> ('a * 'b) enum
+
+ (**[( *-* )] is a synonym for [balanced_product]. *)
+ val ( *-* ) : 'a enum -> 'b enum -> ('a * 'b) enum
+
+ (**[map phi e] is the image of the enumeration [e] through the function
+ [phi]. It is up to the user to ensure that [phi] is injective. *)
+ val map: ('a -> 'b) -> 'a enum -> 'b enum
+
+ (**The enumeration [finite xs] contains the elements in the list [xs], with
+ size zero. *)
+ val finite: 'a list -> 'a enum
+
+ (**[bool] is equivalent to [finite [false; true]]. *)
+ val bool: bool enum
+
+ (**If [elem] is an enumeration of the type ['a], then [list elem] is an
+ enumeration of the type ['a list]. It is worth noting that every call to
+ [list elem] produces a fresh memoizing function, so (if possible) one
+ should avoid applying [list] twice to the same argument; that would be a
+ waste of time and space. *)
+ val list: 'a enum -> 'a list enum
+
+ (**Suppose we wish to enumerate lists of elements, where the validity of an
+ element depends on which elements have appeared earlier in the list. For
+ instance, we might wish to enumerate lists of instructions, where the set
+ of permitted instructions at some point depends on the environment at
+ this point, and each instruction produces an updated environment. If
+ [fix] is a suitable fixed point combinator and if the function [elem]
+ describes how elements depend on environments and how elements affect
+ environments, then [dlist fix elem] is such an enumeration. Each list
+ node is considered to have size 1. Because the function [elem] produces a
+ list (as opposed to an enumeration), an element does not have a size.
+
+ The fixed point combinator [fix] is typically of the form [curried fix],
+ where [fix] is a fixed point combinator for keys of type ['env * int].
+ Memoization takes place at keys that are pairs of an environment and a
+ size.
+
+ The function [elem] receives an environment and must return a list of
+ pairs of an element and an updated environment. *)
+ val dlist:
+ ('env -> 'a list enum) Fix.fix ->
+ ('env -> ('a * 'env) list) ->
+ ('env -> 'a list enum)
+
+ (**[sample m e i j k] is a sequence of at most [m] elements of every size
+ comprised between [i] (included) and [j] (excluded) extracted out of the
+ enumeration [e], prepended in front of the existing sequence [k]. At
+ every size, if there at most [m] elements of this size, then all elements
+ of this size are produced; otherwise, a random sample of [m] elements of
+ this size is produced. *)
+ val sample: int -> 'a enum -> int -> int -> 'a Seq.t -> 'a Seq.t
+
+end
diff --git a/src/IFSeq.ml b/feat-core/IFSeq.ml
similarity index 74%
rename from src/IFSeq.ml
rename to feat-core/IFSeq.ml
index cd21753..ce7bb70 100644
--- a/src/IFSeq.ml
+++ b/feat-core/IFSeq.ml
@@ -8,9 +8,10 @@
(* terms of the MIT license, as described in the file LICENSE. *)
(******************************************************************************)
-(* The default implementation of the signature SEQ is based on IFSeqSyn,
- instantiated with the unbounded integers provided by [zarith]. *)
+module Make (Z : BigIntSig.EXTENDED) (R : RandomSig.S) = struct
+(* We have a choice between using IFSeqSyn and using IFSeqObj. We choose the
+ former. *)
include IFSeqSyn.Make(Z)
(* Iterated sum. *)
@@ -23,18 +24,22 @@ let bigsum ss =
let exists (xs : 'a list) (s : 'a -> 'b seq) : 'b seq =
bigsum (List.map s xs)
-(* Extract a randomly chosen sample of [m] elements out of a sequence [s]. *)
+(* [sample] extracts a randomly chosen sample of [m] elements out of a
+ sequence [s]. *)
(* We do not protect against repetitions, as they are unlikely when [s] is
long. *)
(* For some reason, [Z.random] does not exist, and [Random.int] stops
- working at [2^30]. [Bigint.random] works around these problems. *)
+ working at [2^30]. [RandomBigInt.random] works around these problems. *)
+
+module RandomBigInt =
+ RandomBigInt.Make(Z)(R)
let rec sample (m : int) (s : 'a seq) (k : 'a Seq.t) : 'a Seq.t =
if m > 0 then
fun () ->
- let i = Bigint.random (length s) in
+ let i = RandomBigInt.random (length s) in
let x = get s i in
Seq.Cons (x, sample (m - 1) s k)
else
@@ -44,4 +49,6 @@ let rec sample (m : int) (s : 'a seq) (k : 'a Seq.t) : 'a Seq.t =
otherwise produce a randomly chosen sample, as above. *)
let sample (m : int) (s : 'a seq) (k : 'a Seq.t) : 'a Seq.t =
- if length s <= Z.of_int m then to_seq s k else sample m s k
+ if Z.leq (length s) (Z.of_int m) then to_seq s k else sample m s k
+
+end
diff --git a/src/IFSeq.mli b/feat-core/IFSeq.mli
similarity index 54%
rename from src/IFSeq.mli
rename to feat-core/IFSeq.mli
index d0c0cff..909c1bb 100644
--- a/src/IFSeq.mli
+++ b/feat-core/IFSeq.mli
@@ -10,20 +10,10 @@
open IFSeqSig
-(* An implementation of the signature SEQ,
- instantiated with unbounded integers. *)
-
-include IFSEQ with type index = Z.t
-
-(* Iterated sum. *)
-val bigsum: 'a seq list -> 'a seq
-
-(* Indexed iterated sum. *)
-val exists: 'a list -> ('a -> 'b seq) -> 'b seq
-
-(* [sample m s k] is an explicit sequence of at most [m] elements extracted
- out of the implicit sequence [s], prepended in front of the existing
- sequence [k]. If [length s] at most [m], then all elements of [s] are
- produced. Otherwise, a random sample of [m] elements extracted out of
- [s] is produced. *)
-val sample: int -> 'a seq -> 'a Seq.t -> 'a Seq.t
+(**[Make] constructs an implementation of the signature
+ {!IFSeqSig.IFSEQ_EXTENDED}. It is parameterized over an implementation of
+ big integers and a random number generator. *)
+module Make
+ (Z : BigIntSig.EXTENDED)
+ (R : RandomSig.S)
+: IFSEQ_EXTENDED with type index = Z.t
diff --git a/src/IFSeqList.ml b/feat-core/IFSeqList.ml
similarity index 100%
rename from src/IFSeqList.ml
rename to feat-core/IFSeqList.ml
diff --git a/src/IFSeqList.mli b/feat-core/IFSeqList.mli
similarity index 90%
rename from src/IFSeqList.mli
rename to feat-core/IFSeqList.mli
index b4fd392..e4db19f 100644
--- a/src/IFSeqList.mli
+++ b/feat-core/IFSeqList.mli
@@ -12,5 +12,5 @@
open IFSeqSig
-include IFSEQ with type index = int
- and type 'a seq = 'a list
+include IFSEQ_BASIC with type index = int
+ and type 'a seq = 'a list
diff --git a/src/IFSeqObj.ml b/feat-core/IFSeqObj.ml
similarity index 94%
rename from src/IFSeqObj.ml
rename to feat-core/IFSeqObj.ml
index 6e8133c..9fd0e91 100644
--- a/src/IFSeqObj.ml
+++ b/feat-core/IFSeqObj.ml
@@ -16,21 +16,7 @@
under the assumption that the arithmetic operations provided by [Z]
cost O(1) as well. *)
-module Make (Z : sig
- type t
- val zero: t
- val one: t
- val of_int: int -> t
- val pred: t -> t
- val add: t -> t -> t
- val sub: t -> t -> t
- val mul: t -> t -> t
- val div_rem: t -> t -> t * t
- val equal: t -> t -> bool
- val lt: t -> t -> bool
- exception Overflow
- val to_int: t -> int
-end) = struct
+module Make (Z : BigIntSig.BASIC) = struct
type index =
Z.t
diff --git a/src/IFSeqObj.mli b/feat-core/IFSeqObj.mli
similarity index 76%
rename from src/IFSeqObj.mli
rename to feat-core/IFSeqObj.mli
index 661f8e4..bc5cb5a 100644
--- a/src/IFSeqObj.mli
+++ b/feat-core/IFSeqObj.mli
@@ -18,19 +18,4 @@ open IFSeqSig
under the assumption that the arithmetic operations provided by [Z]
cost O(1) as well. *)
-module Make (Z : sig
- type t
- val zero: t
- val one: t
- val of_int: int -> t
- val pred: t -> t
- val add: t -> t -> t
- val sub: t -> t -> t
- val mul: t -> t -> t
- val div_rem: t -> t -> t * t
- val equal: t -> t -> bool
- val lt: t -> t -> bool
- exception Overflow
- val to_int: t -> int
-end)
-: IFSEQ with type index = Z.t
+module Make (Z : BigIntSig.BASIC) : IFSEQ_BASIC with type index = Z.t
diff --git a/src/IFSeqSig.ml b/feat-core/IFSeqSig.ml
similarity index 55%
rename from src/IFSeqSig.ml
rename to feat-core/IFSeqSig.ml
index 4462569..343f692 100644
--- a/src/IFSeqSig.ml
+++ b/feat-core/IFSeqSig.ml
@@ -8,76 +8,103 @@
(* terms of the MIT license, as described in the file LICENSE. *)
(******************************************************************************)
-(* A signature for implicit finite sequences. *)
+(**A signature for implicit finite sequences.
-(* These sequences are implicit, which means that they are not explicitly
+ These sequences are implicit, which means that they are not explicitly
represented in memory as actual sequences of elements; instead, they are
described by a data structure which contains enough information to produce
an arbitrary element upon request. This design decision imposes some
constraints on the operations that can be efficiently supported; for
- instance, [filter] is not supported. *)
+ instance, [filter] is not supported.
-(* This signature forms an applicative functor. *)
+ This signature forms an applicative functor. *)
+module type IFSEQ_BASIC = sig
-module type IFSEQ = sig
-
- (* ['a seq] is the type of sequences whose elements have type ['a]. *)
+ (**['a seq] is the type of sequences whose elements have type ['a]. *)
type 'a seq
- (* Constructors. *)
+ (**Constructors. *)
- (* [empty] is a sequence of length zero. *)
+ (**[empty] is a sequence of length zero. *)
val empty: 'a seq
+
+ (**[zero] is a synonym for [empty]. *)
val zero : 'a seq
- (* [singleton x] is a sequence of length one whose single element is [x]. *)
+ (**[singleton x] is a sequence of length one whose single element is [x]. *)
val singleton: 'a -> 'a seq
+
+ (**[one] is a synonym for [singleton]. *)
val one: 'a -> 'a seq
- (* [rev xs] is the reverse of the sequence [xs]. *)
+ (**[rev xs] is the reverse of the sequence [xs]. *)
val rev: 'a seq -> 'a seq
- (* [sum s1 s2] is the concatenation of the sequences [s1] and [s2]. *)
+ (**[sum s1 s2] is the concatenation of the sequences [s1] and [s2]. *)
val sum : 'a seq -> 'a seq -> 'a seq
+
+ (**[(++)] is a synonym for [sum]. *)
val ( ++ ) : 'a seq -> 'a seq -> 'a seq
- (* [product s1 s2] is the Cartesian product of the sequences [s1] and [s2].
+ (**[product s1 s2] is the Cartesian product of the sequences [s1] and [s2].
Its length is the product of the lengths of [s1] and [s2]. The first pair
component is considered most significant. *)
val product: 'a seq -> 'b seq -> ('a * 'b) seq
+
+ (**[( ** )] is a synonym for [product]. *)
val ( ** ) : 'a seq -> 'b seq -> ('a * 'b) seq
- (* [map phi s] is the image of the sequence [s] through the function [phi].
+ (**[map phi s] is the image of the sequence [s] through the function [phi].
If the user wishes to work with sequences of pairwise distinct elements,
then [phi] should be injective. If furthermore the user wishes to work
with sequences that enumerate all elements of a type, then [phi] should
be surjective. *)
val map: ('a -> 'b) -> 'a seq -> 'b seq
- (* [up i j] is the sequence of the integers from [i] included up to [j]
+ (**[up i j] is the sequence of the integers from [i] included up to [j]
excluded. *)
val up: int -> int -> int seq
(* Observations. *)
- (* The type [index] is the type of integers used to represent indices and
+ (**The type [index] is the type of integers used to represent indices and
lengths. *)
type index
- (* [length s] is the length of the sequence [s]. *)
+ (**[length s] is the length of the sequence [s]. *)
val length: 'a seq -> index
- (* [get s i] is the [i]-th element of the sequence [s]. The index [i] must
+ (**[get s i] is the [i]-th element of the sequence [s]. The index [i] must
be comprised between zero included and [length s] excluded. *)
val get: 'a seq -> index -> 'a
- (* [foreach s k] iterates over all elements of the sequence [s]. Each element
- in turn is passed to the loop body [k]. *)
+ (**[foreach s k] iterates over all elements of the sequence [s]. Each
+ element in turn is passed to the loop body [k]. *)
val foreach: 'a seq -> ('a -> unit) -> unit
- (* [to_seq s k] produces an explicit representation of the sequence [s] as a
+ (**[to_seq s k] produces an explicit representation of the sequence [s] as a
sequence in the sense of OCaml's standard library module [Seq]. This
sequence is prepended in front of the existing sequence [k]. *)
val to_seq: 'a seq -> 'a Seq.t -> 'a Seq.t
end
+
+(**This signature extends {!IFSEQ_BASIC} with more operations. *)
+module type IFSEQ_EXTENDED = sig
+
+ include IFSEQ_BASIC
+
+ (**Iterated sum. *)
+ val bigsum: 'a seq list -> 'a seq
+
+ (**Indexed iterated sum. *)
+ val exists: 'a list -> ('a -> 'b seq) -> 'b seq
+
+ (**[sample m s k] is an explicit sequence of at most [m] elements extracted
+ out of the implicit sequence [s], prepended in front of the existing
+ sequence [k]. If [length s] at most [m], then all elements of [s] are
+ produced. Otherwise, a random sample of [m] elements extracted out of [s]
+ is produced. *)
+ val sample: int -> 'a seq -> 'a Seq.t -> 'a Seq.t
+
+end
diff --git a/src/IFSeqSyn.ml b/feat-core/IFSeqSyn.ml
similarity index 95%
rename from src/IFSeqSyn.ml
rename to feat-core/IFSeqSyn.ml
index f01df79..549bd76 100644
--- a/src/IFSeqSyn.ml
+++ b/feat-core/IFSeqSyn.ml
@@ -18,21 +18,7 @@
under the assumption that the arithmetic operations provided by [Z]
cost O(1) as well. *)
-module Make (Z : sig
- type t
- val zero: t
- val one: t
- val of_int: int -> t
- val pred: t -> t
- val add: t -> t -> t
- val sub: t -> t -> t
- val mul: t -> t -> t
- val div_rem: t -> t -> t * t
- val equal: t -> t -> bool
- val lt: t -> t -> bool
- exception Overflow
- val to_int: t -> int
-end) = struct
+module Make (Z : BigIntSig.BASIC) = struct
type index =
Z.t
diff --git a/src/IFSeqSyn.mli b/feat-core/IFSeqSyn.mli
similarity index 75%
rename from src/IFSeqSyn.mli
rename to feat-core/IFSeqSyn.mli
index 81a4c57..734fe5a 100644
--- a/src/IFSeqSyn.mli
+++ b/feat-core/IFSeqSyn.mli
@@ -17,19 +17,4 @@ open IFSeqSig
under the assumption that the arithmetic operations provided by [Z]
cost O(1) as well. *)
-module Make (Z : sig
- type t
- val zero: t
- val one: t
- val of_int: int -> t
- val pred: t -> t
- val add: t -> t -> t
- val sub: t -> t -> t
- val mul: t -> t -> t
- val div_rem: t -> t -> t * t
- val equal: t -> t -> bool
- val lt: t -> t -> bool
- exception Overflow
- val to_int: t -> int
-end)
-: IFSEQ with type index = Z.t
+module Make (Z : BigIntSig.BASIC) : IFSEQ_BASIC with type index = Z.t
diff --git a/src/Makefile b/feat-core/Makefile
similarity index 100%
rename from src/Makefile
rename to feat-core/Makefile
diff --git a/src/bigint.ml b/feat-core/RandomBigInt.ml
similarity index 86%
rename from src/bigint.ml
rename to feat-core/RandomBigInt.ml
index e1ccd36..70fdb21 100644
--- a/src/bigint.ml
+++ b/feat-core/RandomBigInt.ml
@@ -12,7 +12,7 @@
Street's bignum library. *)
(* [random state range] chooses a [depth] and generates random values using
- [Random.State.bits state], called [1 lsl depth] times and concatenated. The
+ [R.bits state], called [1 lsl depth] times and concatenated. The
preliminary result [n] therefore satisfies [0 <= n < 1 lsl (30 lsl depth)].
In order for the random choice to be uniform between [0] and [range-1],
@@ -23,6 +23,10 @@
The [depth] value is chosen so that repeating is uncommon (1 in 1000 or
less). *)
+open Printf
+
+module Make (Z : BigIntSig.EXTENDED) (R : RandomSig.S) = struct
+
let bits_at_depth (depth : int) : int =
30 lsl depth
@@ -36,9 +40,9 @@ let rec choose_bit_depth_for_range_from range depth =
let choose_bit_depth_for_range (range : Z.t) : int =
choose_bit_depth_for_range_from range 0
-let rec random_bigint_at_depth (state : Random.State.t) depth : Z.t =
+let rec random_bigint_at_depth (state : R.State.t) depth : Z.t =
if depth = 0 then
- Z.of_int (Random.State.bits state)
+ Z.of_int (R.State.bits state)
else
let depth = depth - 1 in
let prefix = random_bigint_at_depth state depth in
@@ -62,11 +66,13 @@ let large_random state range =
let random state range =
if Z.leq range Z.zero then
- failwith (Printf.sprintf "Bigint.random: argument %s <= 0" (Z.to_string range))
+ invalid_arg (sprintf "random: %s is not positive" (Z.to_string range))
else if Z.lt range Z.(one lsl 30) then
- Z.of_int (Random.State.int state (Z.to_int range))
+ Z.of_int (R.State.int state (Z.to_int range))
else
large_random state range
let random range =
- random (Random.get_state()) range
+ random (R.get_state ()) range
+
+end
diff --git a/feat-core/RandomBigInt.mli b/feat-core/RandomBigInt.mli
new file mode 100644
index 0000000..a86255a
--- /dev/null
+++ b/feat-core/RandomBigInt.mli
@@ -0,0 +1,17 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+(* Uniform random generation of large integers. *)
+
+module Make (Z : BigIntSig.EXTENDED) (R : RandomSig.S) : sig
+ (**[random range] generates a random number comprised between 0 (included)
+ and [range] (excluded). [range] must be positive. *)
+ val random: Z.t -> Z.t
+end
diff --git a/feat-core/RandomSig.ml b/feat-core/RandomSig.ml
new file mode 100644
index 0000000..2ba634e
--- /dev/null
+++ b/feat-core/RandomSig.ml
@@ -0,0 +1,32 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+(** A subset of the signature of the module {!Stdlib.Random}. *)
+module type S = sig
+
+ module State : sig
+
+ (** The state of the random number generator. *)
+ type t
+
+ (** [bits s] returns 30 random bits in a nonnegative integer. *)
+ val bits : t -> int
+
+ (** [int bound] returns a random integer comprised between 0 (inclusive)
+ and [bound] (exclusive). [bound] must be greater than 0 and less than
+ 2{^30}. *)
+ val int : t -> int -> int
+
+ end
+
+ (** [get_state()] returns the current state of the generator. *)
+ val get_state : unit -> State.t
+
+end
diff --git a/feat-core/dune b/feat-core/dune
new file mode 100644
index 0000000..5bf681a
--- /dev/null
+++ b/feat-core/dune
@@ -0,0 +1,6 @@
+(library
+ (name FeatCore)
+ (public_name feat-core)
+ (flags "-w" "A-44-67-70")
+ (libraries seq fix)
+)
diff --git a/feat-num.opam b/feat-num.opam
new file mode 100644
index 0000000..838201f
--- /dev/null
+++ b/feat-num.opam
@@ -0,0 +1,19 @@
+name: "feat-num"
+opam-version: "2.0"
+maintainer: "francois.pottier@inria.fr"
+authors: [
+ "François Pottier <francois.pottier@inria.fr>"
+]
+homepage: "https://gitlab.inria.fr/fpottier/feat"
+dev-repo: "git+https://gitlab.inria.fr/fpottier/feat.git"
+bug-reports: "francois.pottier@inria.fr"
+build: [
+ ["dune" "build" "-p" name "-j" jobs]
+]
+depends: [
+ "ocaml" { >= "4.03" }
+ "dune" { >= "1.3" }
+ "feat-core"
+ "num"
+]
+synopsis: "Facilities for enumerating and sampling algebraic data types, using Num for big numbers"
diff --git a/feat-num/Enum.ml b/feat-num/Enum.ml
new file mode 100644
index 0000000..f10b19b
--- /dev/null
+++ b/feat-num/Enum.ml
@@ -0,0 +1,11 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+include FeatCore.Enum.Make(IFSeq)
diff --git a/feat-num/Enum.mli b/feat-num/Enum.mli
new file mode 100644
index 0000000..ec0de7c
--- /dev/null
+++ b/feat-num/Enum.mli
@@ -0,0 +1,11 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+include FeatCore.EnumSig.ENUM with module IFSeq = IFSeq
diff --git a/feat-num/IFSeq.ml b/feat-num/IFSeq.ml
new file mode 100644
index 0000000..46138c8
--- /dev/null
+++ b/feat-num/IFSeq.ml
@@ -0,0 +1,11 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+include FeatCore.IFSeq.Make(Num)(Random)
diff --git a/src/bigint.mli b/feat-num/IFSeq.mli
similarity index 90%
rename from src/bigint.mli
rename to feat-num/IFSeq.mli
index b1358ee..0ae02c5 100644
--- a/src/bigint.mli
+++ b/feat-num/IFSeq.mli
@@ -8,6 +8,4 @@
(* terms of the MIT license, as described in the file LICENSE. *)
(******************************************************************************)
-(* Uniform random generation of large integers. *)
-
-val random: Z.t -> Z.t
+include FeatCore.IFSeqSig.IFSEQ_EXTENDED with type index = Num.t
diff --git a/feat-num/Makefile b/feat-num/Makefile
new file mode 100644
index 0000000..3cf0f89
--- /dev/null
+++ b/feat-num/Makefile
@@ -0,0 +1,3 @@
+.PHONY: all
+all:
+ @ make -C ..
diff --git a/feat-num/Num.ml b/feat-num/Num.ml
new file mode 100644
index 0000000..db81af3
--- /dev/null
+++ b/feat-num/Num.ml
@@ -0,0 +1,33 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+open Big_int
+
+type t = big_int
+let zero = zero_big_int
+let one = big_int_of_int 1
+let pred = pred_big_int
+let add = add_big_int
+let sub = sub_big_int
+let mul = mult_big_int
+let div_rem = quomod_big_int
+let equal = eq_big_int
+let lt = lt_big_int
+let of_int = big_int_of_int
+exception Overflow
+let to_int = try int_of_big_int with Failure _ -> raise Overflow
+let leq = le_big_int
+let geq = ge_big_int
+let (/) = div_big_int
+let ( * ) = mult_big_int
+let (mod) = mod_big_int
+let (lsl) = shift_left_big_int
+let (lor) = or_big_int
+let to_string = string_of_big_int
diff --git a/feat-num/Num.mli b/feat-num/Num.mli
new file mode 100644
index 0000000..1f96177
--- /dev/null
+++ b/feat-num/Num.mli
@@ -0,0 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+(* This module satisfies the signature [BigIntSig.EXTENDED], instantiated with
+ unbounded integers provided by the library [num]. *)
+include FeatCore.BigIntSig.EXTENDED with type t = Big_int.big_int
diff --git a/feat-num/dune b/feat-num/dune
new file mode 100644
index 0000000..ca532ec
--- /dev/null
+++ b/feat-num/dune
@@ -0,0 +1,6 @@
+(library
+ (name FeatNum)
+ (public_name feat-num)
+ (flags "-w" "A-44")
+ (libraries feat-core num)
+)
diff --git a/feat.opam b/feat.opam
index dbec49e..2f312fd 100644
--- a/feat.opam
+++ b/feat.opam
@@ -13,8 +13,7 @@ build: [
depends: [
"ocaml" { >= "4.03" }
"dune" { >= "1.3" }
+ "feat-core"
"zarith"
- "seq"
- "fix" { >= "20181206" }
]
-synopsis: "Facilities for enumerating and sampling algebraic data types"
+synopsis: "Facilities for enumerating and sampling algebraic data types, using Zarith for big numbers"
diff --git a/feat/Enum.ml b/feat/Enum.ml
new file mode 100644
index 0000000..f10b19b
--- /dev/null
+++ b/feat/Enum.ml
@@ -0,0 +1,11 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+include FeatCore.Enum.Make(IFSeq)
diff --git a/feat/Enum.mli b/feat/Enum.mli
new file mode 100644
index 0000000..ec0de7c
--- /dev/null
+++ b/feat/Enum.mli
@@ -0,0 +1,11 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+include FeatCore.EnumSig.ENUM with module IFSeq = IFSeq
diff --git a/feat/IFSeq.ml b/feat/IFSeq.ml
new file mode 100644
index 0000000..46138c8
--- /dev/null
+++ b/feat/IFSeq.ml
@@ -0,0 +1,11 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+include FeatCore.IFSeq.Make(Num)(Random)
diff --git a/feat/IFSeq.mli b/feat/IFSeq.mli
new file mode 100644
index 0000000..0ae02c5
--- /dev/null
+++ b/feat/IFSeq.mli
@@ -0,0 +1,11 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+include FeatCore.IFSeqSig.IFSEQ_EXTENDED with type index = Num.t
diff --git a/feat/Makefile b/feat/Makefile
new file mode 100644
index 0000000..3cf0f89
--- /dev/null
+++ b/feat/Makefile
@@ -0,0 +1,3 @@
+.PHONY: all
+all:
+ @ make -C ..
diff --git a/feat/Num.ml b/feat/Num.ml
new file mode 100644
index 0000000..94e5247
--- /dev/null
+++ b/feat/Num.ml
@@ -0,0 +1,11 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+include Z
diff --git a/feat/Num.mli b/feat/Num.mli
new file mode 100644
index 0000000..4c771fc
--- /dev/null
+++ b/feat/Num.mli
@@ -0,0 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
+(* This module satisfies the signature [BigIntSig.EXTENDED],
+ instantiated with unbounded integers from [zarith]. *)
+include FeatCore.BigIntSig.EXTENDED with type t = Z.t
diff --git a/feat/dune b/feat/dune
new file mode 100644
index 0000000..363d534
--- /dev/null
+++ b/feat/dune
@@ -0,0 +1,6 @@
+(library
+ (name Feat)
+ (public_name feat)
+ (flags "-w" "A-44")
+ (libraries feat-core zarith)
+)
diff --git a/src/Enum.mli b/src/Enum.mli
deleted file mode 100644
index 0b16b75..0000000
--- a/src/Enum.mli
+++ /dev/null
@@ -1,113 +0,0 @@
-(******************************************************************************)
-(* *)
-(* Feat *)
-(* *)
-(* François Pottier, Inria Paris *)
-(* *)
-(* Copyright Inria. All rights reserved. This file is distributed under the *)
-(* terms of the MIT license, as described in the file LICENSE. *)
-(******************************************************************************)
-
-(* An enumeration of type ['a enum] can be loosely thought of as a set of
- values of type ['a], equipped with a notion of size. More precisely, it
- is a function of a size [s] to a subset of inhabitants of size [s],
- presented as a sequence. *)
-
-(* We expose the fact that enumerations are functions, instead of making [enum]
- an abstract type, because this allows the user to make recursive definitions.
- It is up to the user to ensure that recursion is well-founded; as a rule of
- thumb, every recursive call must appear under [pay]. It is also up to the
- user to take precautions so that these functions have constant time
- complexity (beyond the cost of an initialization phase). This is typically
- achieved by using a memoizing fixed point combinator [fix] instead of
- ordinary recursive definitions. *)
-
-type 'a enum =
- int -> 'a IFSeq.seq
-
-(* [empty] is the empty enumeration. *)
-val empty: 'a enum
-val zero : 'a enum
-
-(* The enumeration [just x] contains just the element [x].
- Its size is considered to be zero. *)
-val just: 'a -> 'a enum
-
-(* The enumeration [enum x] contains the elements in the sequence [xs].
- Their size is considered to be zero. *)
-val enum: 'a IFSeq.seq -> 'a enum
-
-(* The enumeration [pay e] contains the same elements as [e],
- but their size is increased by one. *)
-val pay: 'a enum -> 'a enum
-
-(* [sum e1 e2] is the union of the enumerations [e1] and [e2]. It is up
- to the user to ensure that the sets [e1] and [e2] are disjoint. *)
-val sum : 'a enum -> 'a enum -> 'a enum
-val ( ++ ) : 'a enum -> 'a enum -> 'a enum
-
-(* [exists xs e] is the union of all enumerations of the form [e x], where [x]
- is drawn from the list [xs]. (This is an indexed sum.) It is up to the user
- to ensure that the sets [e1] and [e2] are disjoint. *)
-val exists: 'a list -> ('a -> 'b enum) -> 'b enum
-
-(* [product e1 e2] is the Cartesian product of the enumerations
- [e1] and [e2]. *)
-val product: 'a enum -> 'b enum -> ('a * 'b) enum
-val ( ** ) : 'a enum -> 'b enum -> ('a * 'b) enum
-
-(* [product e1 e2] is a subset of the Cartesian product [product e1 e2]
- where the sizes of the left-hand and right-hand pair components must
- differ by at most one. *)
-val balanced_product: 'a enum -> 'b enum -> ('a * 'b) enum
-val ( *-* ) : 'a enum -> 'b enum -> ('a * 'b) enum
-
-(* [map phi e] is the image of the enumeration [e] through the function [phi].
- It is up to the user to ensure that [phi] is injective. *)
-val map: ('a -> 'b) -> 'a enum -> 'b enum
-
-(* The enumeration [finite xs] contains the elements in the list [xs].
- They are considered to have size zero. *)
-val finite: 'a list -> 'a enum
-
-(* [bool] is the enumeration [false; true]. *)
-val bool: bool enum
-
-(* If [elem] is an enumeration of the type ['a], then [list elem] is an
- enumeration of the type ['a list]. It is worth noting that every call
- to [list elem] produces a fresh memoizing function, so (if possible)
- one should avoid applying [list] twice to the same argument; that
- would be a waste of time and space. *)
-val list: 'a enum -> 'a list enum
-
-(* Suppose we wish to enumerate lists of elements, where the validity of an
- element depends on which elements have appeared earlier in the list. For
- instance, we might wish to enumerate lists of instructions, where the set
- of permitted instructions at some point depends on the environment at this
- point, and each instruction produces an updated environment. If [fix] is a
- suitable fixed point combinator and if the function [elem] describes how
- elements depend on environments and how elements affect environments, then
- [dlist fix elem] is such an enumeration. Each list node is considered to
- have size 1. Because the function [elem] produces a list (as opposed to an
- enumeration), an element does not have a size. *)
-
-(* The fixed point combinator [fix] is typically of the form [curried fix],
- where [fix] is a fixed point combinator for keys of type ['env * int].
- Memoization takes place at keys that are pairs of an environment and a
- size. *)
-
-(* The function [elem] receives an environment and must return a list of pairs
- of an element and an updated environment. *)
-
-val dlist:
- ('env -> 'a list enum) Fix.fix ->
- ('env -> ('a * 'env) list) ->
- ('env -> 'a list enum)
-
-(* [sample m e i j k] is a sequence of at most [m] elements of every size
- comprised between [i] (included) and [j] (excluded) extracted out of the
- enumeration [e], prepended in front of the existing sequence [k]. At every
- size, if there at most [m] elements of this size, then all elements of this
- size are produced; otherwise, a random sample of [m] elements of this size
- is produced. *)
-val sample: int -> 'a enum -> int -> int -> 'a Seq.t -> 'a Seq.t
diff --git a/src/dune b/src/dune
deleted file mode 100644
index 90a5a6c..0000000
--- a/src/dune
+++ /dev/null
@@ -1,7 +0,0 @@
-(library
- (name feat)
- (public_name feat)
- (synopsis "Facilities for enumerating and sampling algebraic data types")
- (flags "-w" "A-44")
- (libraries seq zarith fix)
-)
--
GitLab