From 73b4019ce842893d279d9672017a7866e55d674a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Thu, 31 Dec 2020 09:37:51 +0100
Subject: [PATCH] Headers.
---
headers/library-header | 7 +++++++
src/Enum.ml | 10 ++++++++++
src/Enum.mli | 10 ++++++++++
src/IFSeq.ml | 10 ++++++++++
src/IFSeq.mli | 10 ++++++++++
src/IFSeqList.ml | 10 ++++++++++
src/IFSeqList.mli | 10 ++++++++++
src/IFSeqObj.ml | 10 ++++++++++
src/IFSeqObj.mli | 10 ++++++++++
src/IFSeqSig.ml | 10 ++++++++++
src/IFSeqSyn.ml | 10 ++++++++++
src/IFSeqSyn.mli | 10 ++++++++++
src/bigint.ml | 10 ++++++++++
src/bigint.mli | 10 ++++++++++
14 files changed, 137 insertions(+)
create mode 100644 headers/library-header
diff --git a/headers/library-header b/headers/library-header
new file mode 100644
index 0000000..af67a93
--- /dev/null
+++ b/headers/library-header
@@ -0,0 +1,7 @@
+
+ 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.
diff --git a/src/Enum.ml b/src/Enum.ml
index 2a853dc..89809c0 100644
--- a/src/Enum.ml
+++ b/src/Enum.ml
@@ -1,3 +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. *)
+(******************************************************************************)
+
(* -------------------------------------------------------------------------- *)
(* Core combinators. *)
diff --git a/src/Enum.mli b/src/Enum.mli
index 4ce7f00..0b16b75 100644
--- a/src/Enum.mli
+++ b/src/Enum.mli
@@ -1,3 +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. *)
+(******************************************************************************)
+
(* 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],
diff --git a/src/IFSeq.ml b/src/IFSeq.ml
index b8deaea..cd21753 100644
--- a/src/IFSeq.ml
+++ b/src/IFSeq.ml
@@ -1,3 +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. *)
+(******************************************************************************)
+
(* The default implementation of the signature SEQ is based on IFSeqSyn,
instantiated with the unbounded integers provided by [zarith]. *)
diff --git a/src/IFSeq.mli b/src/IFSeq.mli
index 8300bbe..d0c0cff 100644
--- a/src/IFSeq.mli
+++ b/src/IFSeq.mli
@@ -1,3 +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. *)
+(******************************************************************************)
+
open IFSeqSig
(* An implementation of the signature SEQ,
diff --git a/src/IFSeqList.ml b/src/IFSeqList.ml
index d473dc3..988bde9 100644
--- a/src/IFSeqList.ml
+++ b/src/IFSeqList.ml
@@ -1,3 +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. *)
+(******************************************************************************)
+
(* No need to use unbounded integers here, since we will run out of time and
memory before an overflow occurs. *)
diff --git a/src/IFSeqList.mli b/src/IFSeqList.mli
index 3f57d42..b4fd392 100644
--- a/src/IFSeqList.mli
+++ b/src/IFSeqList.mli
@@ -1,3 +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 is a naive implementation of finite sequences as lists. *)
open IFSeqSig
diff --git a/src/IFSeqObj.ml b/src/IFSeqObj.ml
index 8900bdf..6e8133c 100644
--- a/src/IFSeqObj.ml
+++ b/src/IFSeqObj.ml
@@ -1,3 +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 is an implementation of implicit finite sequences as objects, that is,
records of closures. This is the implementation style proposed in the Feat
paper by Duregard et al. *)
diff --git a/src/IFSeqObj.mli b/src/IFSeqObj.mli
index 4b32859..661f8e4 100644
--- a/src/IFSeqObj.mli
+++ b/src/IFSeqObj.mli
@@ -1,3 +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. *)
+(******************************************************************************)
+
open IFSeqSig
(* This is an implementation of implicit finite sequences as objects, that is,
diff --git a/src/IFSeqSig.ml b/src/IFSeqSig.ml
index d66f142..4462569 100644
--- a/src/IFSeqSig.ml
+++ b/src/IFSeqSig.ml
@@ -1,3 +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. *)
+(******************************************************************************)
+
(* A signature for implicit finite sequences. *)
(* These sequences are implicit, which means that they are not explicitly
diff --git a/src/IFSeqSyn.ml b/src/IFSeqSyn.ml
index ed4599c..f01df79 100644
--- a/src/IFSeqSyn.ml
+++ b/src/IFSeqSyn.ml
@@ -1,3 +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 is an implementation of implicit finite sequences as syntax, that is,
algebraic data structures. This style should be more efficient than the one
used in IFSeqObj, because fewer memory blocks are allocated (one block per
diff --git a/src/IFSeqSyn.mli b/src/IFSeqSyn.mli
index b2dd3c4..81a4c57 100644
--- a/src/IFSeqSyn.mli
+++ b/src/IFSeqSyn.mli
@@ -1,3 +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. *)
+(******************************************************************************)
+
open IFSeqSig
(* This is an implementation of implicit finite sequences as syntax,
diff --git a/src/bigint.ml b/src/bigint.ml
index 52abbe8..e1ccd36 100644
--- a/src/bigint.ml
+++ b/src/bigint.ml
@@ -1,3 +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. *)
+(******************************************************************************)
+
(* Uniform random generation of large integers. Copied and adapted from Jane
Street's bignum library. *)
diff --git a/src/bigint.mli b/src/bigint.mli
index b90a2e6..b1358ee 100644
--- a/src/bigint.mli
+++ b/src/bigint.mli
@@ -1,3 +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. *)
+(******************************************************************************)
+
(* Uniform random generation of large integers. *)
val random: Z.t -> Z.t
--
GitLab