Commit 95b58aaa authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Vendor Fix 20200131.

parent 5474a3ba
Pipeline #117438 passed with stages
in 25 seconds
_build
.merlin
fix.install
*~
François Pottier, Inria Paris <francois.pottier@inria.fr>
# CHANGES
## 2020/01/31
* In `Gensym`, new abstract type `generator`,
with three functions `generator`, `fresh`, and `current`.
* In `Memoize`, new function `visibly_memoize`,
which not only returns a memoized function,
but also provides outside access to the memoization table.
* New signatures `ONGOING_NUMBERING` and `TWO_PHASE_NUMBERING`
and new module `Numbering`,
which provides facilities for numbering things.
* Breaking change: the module `Fix.Number`
is renamed `Fix.GraphNumbering`.
## 2018/11/30
* New release, including new modules (`Gensym`, `Memoize`,
`Tabulate`, `Number`, `HashCons`, `Prop`, `Glue`),
new convenience functors (`Fix.ForHashedType`, etc.),
and new demos.
The least-fixed-point computation algorithm is unchanged.
## 2013/06/11
* Initial release of the package,
containing just `Fix.Make`, the
least-fixed-point computation algorithm.
This diff is collapsed.
# ------------------------------------------------------------------------------
# The name of the library.
THIS := fix
# 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)
# The repository URL (https).
REPO := https://gitlab.inria.fr/fpottier/$(THIS)
# The archive URL (https).
ARCHIVE := $(REPO)/repository/$(DATE)/archive.tar.gz
# ------------------------------------------------------------------------------
.PHONY: all
all:
dune build -p $(THIS)
# [make test] runs all tests.
# Some tests require the following opam packages:
# regenerate
.PHONY: test
test:
dune build @runtest
# [make versions] compiles Fix under many versions of OCaml, whose
# list is specified in the file dune-workspace.versions.
# This requires appropriate opam switches to exist. A missing switch
# can be created like this:
# opam switch create 4.03.0
.PHONY: versions
versions:
@ dune build --workspace dune-workspace.versions -p $(THIS)
.PHONY: install
install: all
dune install -p $(THIS)
.PHONY: clean
clean:
rm -f *~ src/*~
dune clean
.PHONY: uninstall
uninstall:
ocamlfind remove $(THIS) || true
.PHONY: reinstall
reinstall: uninstall
@ make install
.PHONY: show
show: reinstall
@ echo "#require \"fix\";;\n#show Fix;;" | ocaml
.PHONY: pin
pin:
opam pin add $(THIS) .
.PHONY: unpin
unpin:
opam pin remove $(THIS)
HEADACHE := headache
LIBHEAD := $(shell pwd)/headers/library-header
FIND := $(shell if command -v gfind >/dev/null ; then echo gfind ; else echo find ; fi)
.PHONY: headache
headache:
@ $(FIND) src -regex ".*\.ml\(i\|y\|l\)?" \
-exec $(HEADACHE) -h $(LIBHEAD) "{}" ";"
.PHONY: release
release:
# Make sure the current version can be compiled and installed.
@ make uninstall
@ make clean
@ make install
# Check the current package description.
@ opam lint
# Check if everything has been committed.
@ if [ -n "$$(git status --porcelain)" ] ; then \
echo "Error: there remain uncommitted changes." ; \
git status ; \
exit 1 ; \
else \
echo "Now making a release..." ; \
fi
# Create a git tag.
@ git tag -a $(DATE) -m "Release $(DATE)."
# Upload. (This automatically makes a .tar.gz archive available on gitlab.)
@ git push
@ git push --tags
.PHONY: publish
publish:
# Publish an opam description.
@ opam publish -v $(DATE) $(THIS) $(ARCHIVE) .
# Fix: memoization and fixed points made easy
`fix` is an OCaml library that helps with various constructions
that involve memoization and recursion.
## Installation
Type `opam install fix`.
## Overview
At the top of an OCaml module, declare `open Fix`.
This gives you access to the following submodules:
* [`Gensym`](src/Gensym.mli) offers a simple facility
for **generating fresh integer identifiers**.
* [`Memoize`](src/Memoize.mli) offers a number of combinators
that help **construct possibly recursive memoizing functions**, that
is, functions that lazily record their input/output graph,
so as to avoid repeated computation.
* [`Tabulate`](src/Tabulate.mli) offers facilities
for **tabulating a function**, that is, eagerly evaluating this function
at every point in its domain, so as to obtain an equivalent
function that can be queried in constant time.
* [`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.
* [`GraphNumbering`](src/GraphNumbering.mli) offers a facility for
**discovering and numbering the reachable vertices** in a finite directed graph.
* [`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.
* [`Fix`](src/Core.mli) offers support for **computing
the least solution of a set of monotone equations**,
as described in the unpublished paper
[Lazy Least Fixed Points in ML](http://cambium.inria.fr/~fpottier/publis/fpottier-fix.pdf).
In other words, it allows defining a recursive function of
type `variable -> property`, where
**cyclic dependencies** between variables are allowed,
and properties must be equipped with a partial order.
The function thus obtained performs the fixed point
computation on demand, in an incremental manner,
and is memoizing.
* `Prop` defines a few common partial orders, including
[`Prop.Boolean`](src/Boolean.mli),
[`Prop.Option`](src/Option.mli),
[`Prop.Set`](src/Set.mli).
* [`Glue`](src/Glue.mli) contains glue code that helps
build various implementations of association maps.
The signatures that appear in the above files,
such as `MEMOIZER`, `TABULATOR`, `SOLVER`, and so on,
are defined [here](src/Sigs.ml).
## Demos
A few demos are provided:
* [`brz`](demos/brz) sets up a hash-consed representation of regular
expressions and shows how to convert a regular expression to a deterministic
finite-state automaton by Brzozowski's method. This demo exploits almost all
of the submodules listed above, and is accompanied with
[a commentary](misc/post.md).
* [`cyk`](demos/cyk) presents a CYK-style parsing algorithm as an instance of
`Fix`.
* [`cfg`](demos/cfg) uses `Fix` to perform certain static analyses of a
context-free grammar; this includes computing nullability information and
FIRST sets.
* [`fib`](demos/fib) defines Fibonacci's function in several different ways
using the fixed-point combinators offered by `Memoize` and `Fix`.
* [`hco`](demos/hco) sets up simple-minded hash-consed trees
using `HashCons`.
# TODO
* Do something with `src/attic/BoolEqs` and `src/attic/ChopFix`,
or remove them.
* Consider using two data fields in `node` instead of one,
so as to avoid using a separate `data` record. Benchmark.
* Provide an extensible-vector implementation of `IMPERATIVE_MAPS` for
integers? Like `ArraysAsImperativeMaps`, but does not require `n`.
Use `InfiniteArray`.
* Provide an API in the style of Menhir's `FixSolver`, where constraints are
discovered incrementally during a first phase, then the solver is started?
* Develop a test suite. (Use `afl-fuzz`?)
E.g., in `CFG`, write a CFG generator.
Compare `Fix` with a naive solver.
* Develop a performance benchmark.
(env
(dev (flags
:standard
-g
-w @A-4-44
))
(release (flags
:standard
))
)
(lang dune 1.3)
(lang dune 2.0)
(context (opam (switch 4.03.0)))
(context (opam (switch 4.04.2)))
(context (opam (switch 4.05.0)))
(context (opam (switch 4.06.1)))
(context (opam (switch 4.07.1)))
(context (opam (switch 4.08.1)))
(context (opam (switch 4.09.0)))
(context (opam (switch 4.09.0+bytecode-only)))
name: "fix"
opam-version: "2.0"
maintainer: "francois.pottier@inria.fr"
authors: [
"François Pottier <francois.pottier@inria.fr>"
]
homepage: "https://gitlab.inria.fr/fpottier/fix"
dev-repo: "git+https://gitlab.inria.fr/fpottier/fix.git"
bug-reports: "francois.pottier@inria.fr"
build: [
["dune" "build" "-p" name "-j" jobs]
]
depends: [
"ocaml" { >= "4.03" }
"dune" { build & >= "1.3" }
]
synopsis: "Facilities for memoization and fixed points"
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.
(******************************************************************************)
(* *)
(* 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 property =
bool
let bottom =
false
let equal (b1 : bool) (b2 : bool) =
b1 = b2
let is_maximal b =
b
(******************************************************************************)
(* *)
(* 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. *)
(* *)
(******************************************************************************)
(* The Boolean lattice. The ordering is [false <= true]. *)
open Sigs
include PROPERTY with type property = bool
(******************************************************************************)
(* *)
(* Menhir *)
(* Fix *)
(* *)
(* François Pottier, Inria Paris *)
(* Yann Régis-Gianas, PPS, Université Paris Diderot *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the GNU General Public License version 2, as described in the *)
(* file LICENSE. *)
(* terms of the GNU Library General Public License version 2, with a *)
(* special exception on linking, as described in the file LICENSE. *)
(* *)
(******************************************************************************)
(* -------------------------------------------------------------------------- *)
(* Maps. *)
(* We require imperative maps, that is, maps that can be updated in place.
An implementation of persistent maps, such as the one offered by ocaml's
standard library, can easily be turned into an implementation of imperative
maps, so this is a weak requirement. *)
module type IMPERATIVE_MAPS = sig
type key
type 'data t
val create: unit -> 'data t
val clear: 'data t -> unit
val add: key -> 'data -> 'data t -> unit
val find: key -> 'data t -> 'data
val iter: (key -> 'data -> unit) -> 'data t -> unit
end
(* -------------------------------------------------------------------------- *)
(* Properties. *)
(* Properties must form a partial order, equipped with a least element, and
must satisfy the ascending chain condition: every monotone sequence
eventually stabilizes. *)
(* [is_maximal] determines whether a property [p] is maximal with respect to
the partial order. Only a conservative check is required: in any event, it
is permitted for [is_maximal p] to return [false]. If [is_maximal p]
returns [true], then [p] must have no upper bound other than itself. In
particular, if properties form a lattice, then [p] must be the top
element. This feature, not described in the paper, enables a couple of
minor optimizations. *)
module type PROPERTY = sig
type property
val bottom: property
val equal: property -> property -> bool
val is_maximal: property -> bool
end
(* -------------------------------------------------------------------------- *)
(* The dynamic dependency graph. *)
(* An edge from [node1] to [node2] means that [node1] depends on [node2], or
(equivalently) that [node1] observes [node2]. Then, an update of the
current property at [node2] causes a signal to be sent to [node1]. A node
can observe itself. *)
(* This module could be placed in a separate file, but is included here in
order to make [Fix] self-contained. *)
module Graph : sig
(* This module provides a data structure for maintaining and modifying
a directed graph. Each node is allowed to carry a piece of client
data. There are functions for creating a new node, looking up a
node's data, looking up a node's predecessors, and setting or
clearing a node's successors (all at once). *)
type 'data node
(* [create data] creates a new node, with no incident edges, with
client information [data]. Time complexity: constant. *)
val create: 'data -> 'data node
(* [data node] returns the client information associated with
the node [node]. Time complexity: constant. *)
val data: 'data node -> 'data
(* [predecessors node] returns a list of [node]'s predecessors.
Amortized time complexity: linear in the length of the output
list. *)
val predecessors: 'data node -> 'data node list
(* [set_successors src dsts] creates an edge from the node [src] to
each of the nodes in the list [dsts]. Duplicate elements in the
list [dsts] are removed, so that no duplicate edges are created. It
is assumed that [src] initially has no successors. Time complexity:
linear in the length of the input list. *)
val set_successors: 'data node -> 'data node list -> unit
(* [clear_successors node] removes all of [node]'s outgoing edges.
Time complexity: linear in the number of edges that are removed. *)
val clear_successors: 'data node -> unit
(* That's it. *)
end
= struct
(* Using doubly-linked adjacency lists, one could implement [predecessors]
in worst-case linear time with respect to the length of the output list,
[set_successors] in worst-case linear time with respect to the length of
the input list, and [clear_successors] in worst-case linear time with
respect to the number of edges that are removed. We use a simpler
implementation, based on singly-linked adjacency lists, with deferred
removal of edges. It achieves the same complexity bounds, except
[predecessors] only offers an amortized complexity bound. This is good
enough for our purposes, and, in practice, is more efficient by a
constant factor. This simplification was suggested by Arthur
Charguéraud. *)
type 'data node = {
(* The client information associated with this node. *)
data: 'data;
(* This node's incoming and outgoing edges. *)
mutable outgoing: 'data edge list;
mutable incoming: 'data edge list;
(* A transient mark, always set to [false], except when checking
against duplicate elements in a successor list. *)
mutable marked: bool;
}
and 'data edge = {
(* This edge's nodes. Edges are symmetric: source and destination
are not distinguished. Thus, an edge appears both in the outgoing
edge list of its source node and in the incoming edge list of its
destination node. This allows edges to be easily marked as
destroyed. *)
node1: 'data node;
node2: 'data node;
(* Edges that are destroyed are marked as such, but are not
immediately removed from the adjacency lists. *)
mutable destroyed: bool;
}
let create (data : 'data) : 'data node = {
data = data;
outgoing = [];
incoming = [];
marked = false;
}
let data (node : 'data node) : 'data =
node.data
(* [follow src edge] returns the node that is connected to [src]
by [edge]. Time complexity: constant. *)
let follow src edge =
if edge.node1 == src then
edge.node2
else begin
assert (edge.node2 == src);
edge.node1
end
(* The [predecessors] function removes edges that have been marked
destroyed. The cost of removing these has already been paid for,
so the amortized time complexity of [predecessors] is linear in
the length of the output list. *)
let predecessors (node : 'data node) : 'data node list =
let predecessors = List.filter (fun edge -> not edge.destroyed) node.incoming in
node.incoming <- predecessors;
List.map (follow node) predecessors
(* [link src dst] creates a new edge from [src] to [dst], together
with its reverse edge. Time complexity: constant. *)
let link (src : 'data node) (dst : 'data node) : unit =
let edge = {
node1 = src;
node2 = dst;
destroyed = false;
} in
src.outgoing <- edge :: src.outgoing;
dst.incoming <- edge :: dst.incoming
let set_successors (src : 'data node) (dsts : 'data node list) : unit =
assert (src.outgoing = []);
let rec loop = function
| [] ->
()
| dst :: dsts ->
if dst.marked then
loop dsts (* skip duplicate elements *)
else begin
dst.marked <- true;
link src dst;
loop dsts;
dst.marked <- false
end
in
loop dsts
let clear_successors (node : 'data node) : unit =
List.iter (fun edge ->
assert (not edge.destroyed);
edge.destroyed <- true;
) node.outgoing;
node.outgoing <- []
end
open Sigs
(* -------------------------------------------------------------------------- *)
......@@ -246,14 +39,19 @@ type equations =
(* -------------------------------------------------------------------------- *)
(* Data. *)
(* The dependency graph. *)
(* Each node in the dependency graph carries information about a fixed
variable [v]. *)
(* An edge from [node1] to [node2] in the dynamic dependency graph means that
[node1] depends on [node2], or (equivalently) that [node1] observes
[node2]. Then, an update of the current property at [node2] causes a signal
to be sent to [node1]. A node can observe itself. *)
type node =
data Graph.node
(* Each node in the dependency graph corresponds to a specific variable [v],
and carries data about it. *)
and data = {
(* This is the result of the application of [rhs] to the variable [v]. It
......@@ -376,7 +174,6 @@ let freeze () =
(* Workset processing. *)
(* [solve node] re-evaluates the right-hand side at [node]. If this leads to
a change, then the current property is updated, and [node] emits a signal
towards its observers. *)
......@@ -418,24 +215,29 @@ let rec solve (node : node) : unit =
M.find v permanent
with Not_found ->
let subject = node_for v in
(* IFPAPER
subjects := subject :: !subjects;
property subject
ELSE *)
let p = property subject in
if not (P.is_maximal p) then
subjects := subject :: !subjects;
p
(* END *)
in
(* Give control to the client. *)
let new_property = data.rhs request in
(* From now on, prevent any invocation of this instance of [request]
(* From now on, prevent any invocation of this instance of [request] by
the client. *)
alive := false;
(* At this point, [node] has no subjects, as noted above. Thus, the
precondition of [set_successors] is met. We can install [data.subjects]
precondition of [set_successors] is met. We can install [subjects]
as the new set of subjects for this node. *)
(* If we have gathered no subjects in the list [data.subjects], then