Commit 578074cc authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Vendor Feat.

parent 9665ceff
(vendored_dirs fix pprint) (vendored_dirs fix feat pprint)
(data_only_dirs analysis attic headers releases www) (data_only_dirs analysis attic headers releases www)
[François Pottier](mailto:francois.pottier@inria.fr)
The MIT License
Copyright (c) 2019 François Pottier, Inria <francois.pottier@inria.fr>
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
(lang dune 1.3)
(******************************************************************************)
(* *)
(* 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. *)
type 'a enum =
int -> 'a IFSeq.seq
let empty : 'a enum =
fun _s ->
IFSeq.empty
let zero =
empty
let enum (xs : 'a IFSeq.seq) : 'a enum =
fun s ->
if s = 0 then xs else IFSeq.empty
let just (x : 'a) : 'a enum =
(* enum (IFSeq.singleton x) *)
fun s ->
if s = 0 then IFSeq.singleton x else IFSeq.empty
let pay (enum : 'a enum) : 'a enum =
fun s ->
if s = 0 then IFSeq.empty else enum (s-1)
let sum (enum1 : 'a enum) (enum2 : 'a enum) : 'a enum =
fun s ->
IFSeq.sum (enum1 s) (enum2 s)
let ( ++ ) =
sum
let exists (xs : 'a list) (enum : 'a -> 'b enum) : 'b enum =
fun s ->
IFSeq.exists xs (fun x -> enum x s)
(* [up i j] is the list of the integers of [i] included up to [j] included. *)
let rec up i j =
if i <= j then
i :: up (i + 1) j
else
[]
(* This definition of [product] may seem slightly inefficient, as it builds
intermediate lists, but this is essentially irrelevant when it is used
in the definition of a memoized function. The overhead is paid only once. *)
let product (enum1 : 'a enum) (enum2 : 'b enum) : ('a * 'b) enum =
fun s ->
IFSeq.bigsum (
List.map (fun s1 ->
let s2 = s - s1 in
IFSeq.product (enum1 s1) (enum2 s2)
) (up 0 s)
)
let ( ** ) =
product
let balanced_product (enum1 : 'a enum) (enum2 : 'b enum) : ('a * 'b) enum =
fun s ->
if s mod 2 = 0 then
let s = s / 2 in
IFSeq.product (enum1 s) (enum2 s)
else
let s = s / 2 in
IFSeq.sum
(IFSeq.product (enum1 s) (enum2 (s+1)))
(IFSeq.product (enum1 (s+1)) (enum2 s))
let ( *-* ) =
balanced_product
let map (phi : 'a -> 'b) (enum : 'a enum) : 'b enum =
fun s ->
IFSeq.map phi (enum s)
(* -------------------------------------------------------------------------- *)
(* Convenience functions. *)
let finite (xs : 'a list) : 'a enum =
List.fold_left (++) zero (List.map just xs)
let bool : bool enum =
just false ++ just true
(* also: [finite [false; true]] *)
let list (elem : 'a enum) : 'a list enum =
let cons (x, xs) = x :: xs in
Fix.Memoize.Int.fix (fun list ->
just [] ++ pay (map cons (elem ** list))
)
let dlist fix elem =
let cons x xs = x :: xs in
fix (fun dlist env ->
just [] ++ pay (
exists (elem env) (fun (x, env') ->
map (cons x) (dlist env')
)
)
)
(* -------------------------------------------------------------------------- *)
(* Sampling. *)
let rec sample m e i j k =
if i < j then
IFSeq.sample m (e i) (fun () -> sample m e (i + 1) j k ())
else
k
(******************************************************************************)
(* *)
(* 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
(* The library fix has been renamed vendored_fix so as to prevent Dune
from complaining about a conflict with a copy of fix that might be
installed on the user's system. *)
(* As a result, the library is now accessible under the name Vendored_fix.
Because we do not want to pollute our sources with this name, we define the
module Fix as an alias for Vendored_fix. *)
include Vendored_fix
(******************************************************************************)
(* *)
(* 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]. *)
include IFSeqSyn.Make(Z)
(* Iterated sum. *)
let bigsum ss =
List.fold_left sum zero ss
(* Indexed iterated sum. *)
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]. *)
(* 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. *)
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 x = get s i in
Seq.Cons (x, sample (m - 1) s k)
else
k
(* If the sequence [s] is short enough, then produce all of its elements;
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
(******************************************************************************)
(* *)
(* 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,
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
(******************************************************************************)
(* *)
(* 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. *)
type index =
int
type 'a seq =
'a list
let empty =
[]
let zero =
empty
let singleton x =
[x]
let one =
singleton
let rev =
List.rev
let sum =
(@)
let ( ++ ) =
sum
let product (s1 : 'a seq) (s2 : 'b seq) : ('a * 'b) seq =
List.flatten (s1 |> List.map (fun x1 ->
s2 |> List.map (fun x2 ->
(x1, x2)
)
))
let ( ** ) =
product
let map =
List.map
let rec up i j =
if i < j then
i :: up (i + 1) j
else
[]
let length =
List.length
let get =
List.nth
let foreach s k =
List.iter k s
let rec to_seq xs k =
(* this is [Seq.of_list] *)
fun () ->
match xs with
| [] ->
k()
| x :: xs ->
Seq.Cons (x, to_seq xs k)
(******************************************************************************)
(* *)
(* 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
include IFSEQ with type index = int
and type 'a seq = 'a list
(******************************************************************************)
(* *)
(* 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. *)
(* In this implementation, the constructors have time complexity O(1),
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
type index =
Z.t
(* A sequence stores its length (which is computed at construction time)
as well as [get] and [foreach] methods. *)
(* The [foreach] method takes a Boolean sense as a parameter. This allows
us to easily implement the [foreach] method of a reversed sequence, as
produced by the [rev] combinator. *)
(* For comments on [to_seq], see IFSeqSyn. *)
type ('a, 'b) producer =
('a -> 'b Seq.t -> 'b Seq.t) -> 'b Seq.t -> 'b Seq.t
type 'a seq = {
length : index;
get : index -> 'a;
foreach: bool -> ('a -> unit) -> unit;
to_seq : 'b . bool -> ('a, 'b) producer;
}
let is_empty s =
Z.equal s.length Z.zero
let out_of_bounds () =
failwith "Index is out of bounds."
let empty =
let length = Z.zero
and get _ = out_of_bounds()
and foreach _sense _k = ()
and to_seq _sense _cons k = k in
{ length; get; foreach; to_seq }
let zero =
empty
let singleton x =
let length = Z.one
and get i = if Z.equal i Z.zero then x else out_of_bounds()
and foreach _sense k = k x
and to_seq _sense cons k = cons x k in
{ length; get; foreach; to_seq }
let one =
singleton
let rev s =
let length =
s.length
and get i =
s.get (Z.sub (Z.pred s.length) i)
and foreach sense k =
s.foreach (not sense) k
and to_seq sense cons k =
s.to_seq (not sense) cons k
in
{ length; get; foreach; to_seq }
let sum s1 s2 =
let length =
Z.add s1.length s2.length
and get i =
if Z.lt i s1.length then s1.get i
else s2.get (Z.sub i s1.length)
and foreach sense k =
let s1, s2 = if sense then s1, s2 else s2, s1 in
s1.foreach sense k;
s2.foreach sense k
and to_seq sense cons k =
let s1, s2 = if sense then s1, s2 else s2, s1 in
s1.to_seq sense cons (fun () -> s2.to_seq sense cons k ())
in
{ length; get; foreach; to_seq }
let sum s1 s2 =
(* To save space and reduce access time, we recognize an empty sequence as a
neutral element for concatenation. *)
if is_empty s1 then
s2
else if is_empty s2 then
s1
else
sum s1 s2
let ( ++ ) =
sum
let product s1 s2 =
let length =
Z.mul s1.length s2.length
and get i =
let q, r = Z.div_rem i s2.length in
s1.get q, s2.get r
and foreach sense k =
s1.foreach sense (fun x1 ->
s2.foreach sense (fun x2 ->
k (x1, x2)
)
)
and to_seq sense cons k =
s1.to_seq sense (fun x1 k ->
s2.to_seq sense (fun x2 k ->
cons (x1, x2) k
) k
) k
in
{ length; get; foreach; to_seq }
let product s1 s2 =
(* To save space, we recognize an empty sequence as an absorbing element for
product. This also eliminates the risk of a division by zero in the above
code, which could arise if the user attempts an out-of-bounds access. *)
if is_empty s1 || is_empty s2 then
empty
else
product s1 s2
let ( ** ) =
product
let map phi s =
let length = s.length
and get i = phi (s.get i)
and foreach sense k = s.foreach sense (fun x -> k (phi x))
and to_seq sense cons k = s.to_seq sense (fun x k -> cons (phi x) k) k in
{ length; get; foreach; to_seq }
let map phi s =
(* To save space, we recognize an empty sequence as a fixed point for map. *)
if is_empty s then