Commit d6874f85 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Update fix to version 20201120.

The main change is that Fix.DataFlow now requires [leq_join] instead
of separate [leq] and [join] functions.

The rest of the changes are documentation comments and a few new
features which Menhir does not use.

There should be no change in functionality.
parent 3e1c3a22
# CHANGES
## 2020/02/XX
## 2020/11/20
* New module `DataFlow`, which performs a forward data flow analysis over a
directed graph. (Such a computation could previously be performed by using
......@@ -8,6 +8,11 @@
required access to predecessors. The new algorithm is easier to use and is
more efficient.)
* In `Memoize`, new combinator `curried`, which can be used in combination
with `fix` or `defensive_fix`. Thus, for instance, `curried fix` is a
fixed point combinator that constructs a memoizing two-argument curried
function.
## 2020/01/31
* In `Gensym`, new abstract type `generator`,
......@@ -24,7 +29,7 @@
* Breaking change: the module `Fix.Number`
is renamed `Fix.GraphNumbering`.
## 2018/11/30
## 2018/12/06
* New release, including new modules (`Gensym`, `Memoize`,
`Tabulate`, `Number`, `HashCons`, `Prop`, `Glue`),
......
......@@ -68,6 +68,16 @@ pin:
unpin:
opam pin remove $(THIS)
.PHONY: doc
doc:
dune build @doc
@echo You can find the documentation in _build/default/_doc/_html/index.html
.PHONY: export
export: doc
ssh yquem.inria.fr rm -rf public_html/$(THIS)/doc
scp -r _build/default/_doc/_html yquem.inria.fr:public_html/$(THIS)/doc
HEADACHE := headache
LIBHEAD := $(shell pwd)/headers/library-header
FIND := $(shell if command -v gfind >/dev/null ; then echo gfind ; else echo find ; fi)
......@@ -105,6 +115,7 @@ publish:
@ opam publish -v $(DATE) $(THIS) $(ARCHIVE) .
MENHIR_WORKING_COPY=$(HOME)/dev/menhir
FIX_COPY=$(MENHIR_WORKING_COPY)/fix
.PHONY: menhir
menhir:
......@@ -115,6 +126,7 @@ menhir:
exit 1 ; \
fi
# Copy our source files to the Menhir repository.
@ (cd .. && cp -r fix $(MENHIR_WORKING_COPY))
@ rm -rf $(FIX_COPY)
@ cp -r $(shell pwd) $(FIX_COPY)
# Remove a number of unneeded subdirectories.
@ (cd $(MENHIR_WORKING_COPY)/fix && rm -rf .git demos misc)
@ (cd $(FIX_COPY) && rm -rf .git demos misc)
......@@ -66,6 +66,13 @@ The signatures that appear in the above files,
such as `MEMOIZER`, `TABULATOR`, `SOLVER`, and so on,
are defined [here](src/Sigs.ml).
The documentation is built by `make doc` and is then found in the
file `_build/default/_doc/_html/index.html`.
The [documentation of the latest released
version](http://cambium.inria.fr/~fpottier/fix/doc/fix/Fix/index.html)
is also available online.
## Demos
A few demos are provided:
......
# TODO
* In `MEMOIZER`, some variations are missing, e.g. `visibly_fix`,
`visibly_defensive_fix`.
* Think about a heterogeneous version of the fixed point computation
algorithm, where valuations have type `forall 'a. 'a variable -> 'a property`.
(This would internally require using heterogenous maps...)
* Do something with `src/attic/BoolEqs` and `src/attic/ChopFix`,
or remove them.
......
......@@ -2,7 +2,7 @@
(dev (flags
:standard
-g
-w @A-4-44
-w @A-4-44-67
))
(release (flags
:standard
......
......@@ -6,5 +6,5 @@
(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.1)))
(context (opam (switch 4.09.0+bytecode-only)))
......@@ -10,7 +10,7 @@
(* *)
(******************************************************************************)
(* The Boolean lattice. The ordering is [false <= true]. *)
(**The Boolean lattice. The ordering is [false <= true]. *)
open Sigs
......
......@@ -10,9 +10,17 @@
(* *)
(******************************************************************************)
(**[Fix] 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". 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. *)
open Sigs
(* [Make] constructs a solver for a type [key] that is equipped with
(**[Make] constructs a solver for a type [key] that is equipped with
an implementation of imperative maps and a type [property] that is
equipped with [bottom], [equal], and [is_maximal] functions. *)
......@@ -23,7 +31,7 @@ module Make
with type variable = M.key
and type property = P.property
(* [ForOrderedType] is a special case of [Make] where it
(**[ForOrderedType] is a special case of [Make] where it
suffices to pass an ordered type [T] as an argument.
A reference to a persistent map is used to hold the
memoization table. *)
......@@ -35,7 +43,7 @@ module ForOrderedType
with type variable = T.t
and type property = P.property
(* [ForHashedType] is a special case of [Make] where it
(**[ForHashedType] is a special case of [Make] where it
suffices to pass a hashed type [T] as an argument. A
hash table is used to hold the memoization table. *)
......@@ -46,7 +54,7 @@ module ForHashedType
with type variable = T.t
and type property = P.property
(* [ForType] is a special case of [Make] where it suffices
(**[ForType] is a special case of [Make] where it suffices
to pass an arbitrary type [T] as an argument. A hash table
is used to hold the memoization table. OCaml's built-in
generic equality and hash functions are used. *)
......
......@@ -23,9 +23,15 @@ open Sigs
discovery of dependencies, whereas in this situation, all dependencies are
explicitly provided by the user. *)
(* We require a minimal semi-lattice, equipped with a [leq_join] operation, as
opposed to a semi-lattice, which offers separate [leq] and [join]
operations. Although [leq_join] is less powerful, it is sufficient for our
purposes, and is potentially more efficient than the sequence of [leq]
[join]. *)
module Run
(M : MINIMAL_IMPERATIVE_MAPS)
(P : SEMI_LATTICE)
(P : MINIMAL_SEMI_LATTICE)
(G : DATA_FLOW_GRAPH with type variable = M.key and type property = P.property)
= struct
open P
......@@ -73,9 +79,12 @@ module Run
schedule x'
| p ->
(* [x'] has been discovered earlier. *)
if not (P.leq p' p) then begin
(* [x'] is affected by this update and must itself be scheduled. *)
M.add x' (P.join p' p) properties;
let p'' = P.leq_join p' p in
if p'' != p then begin
(* The failure of the physical equality test [p'' == p] implies that
[P.leq p' p] does not hold. Thus, [x'] is affected by this update
and must itself be scheduled. *)
M.add x' p'' properties;
schedule x'
end
......
......@@ -10,69 +10,71 @@
(* *)
(******************************************************************************)
(**[DataFlow] performs a forward data flow analysis over a directed graph. *)
open Sigs
(* [Run] requires a type [variable] that is equipped with an implementation of
(**[Run] requires a type [variable] that is equipped with an implementation of
imperative maps, a type [property] that is equipped with [leq] and [join]
functions, and a data flow graph whose edges describe the propagation of
properties. It performs a forward data flow analysis and returns its
result. *)
(* The function [solution] has type [variable -> property option]. A reachable
(**The function [solution] has type [variable -> property option]. A reachable
variable is mapped to [Some _]; an unreachable one is mapped to [None]. *)
module Run
(M : MINIMAL_IMPERATIVE_MAPS)
(P : SEMI_LATTICE)
(P : MINIMAL_SEMI_LATTICE)
(G : DATA_FLOW_GRAPH with type variable = M.key and type property = P.property)
: SOLUTION
with type variable = G.variable
and type property = P.property option
(* [ForOrderedType] is a special case of [Run] where it
(**[ForOrderedType] is a special case of [Run] where it
suffices to pass an ordered type [T] as an argument.
A reference to a persistent map is used to hold the
memoization table. *)
module ForOrderedType
(T : OrderedType)
(P : SEMI_LATTICE)
(P : MINIMAL_SEMI_LATTICE)
(G : DATA_FLOW_GRAPH with type variable = T.t and type property = P.property)
: SOLUTION
with type variable = G.variable
and type property = P.property option
(* [ForHashedType] is a special case of [Run] where it
(**[ForHashedType] is a special case of [Run] where it
suffices to pass a hashed type [T] as an argument. A
hash table is used to hold the memoization table. *)
module ForHashedType
(T : HashedType)
(P : SEMI_LATTICE)
(P : MINIMAL_SEMI_LATTICE)
(G : DATA_FLOW_GRAPH with type variable = T.t and type property = P.property)
: SOLUTION
with type variable = G.variable
and type property = P.property option
(* [ForType] is a special case of [Run] where it suffices
(**[ForType] is a special case of [Run] where it suffices
to pass an arbitrary type [T] as an argument. A hash table
is used to hold the memoization table. OCaml's built-in
generic equality and hash functions are used. *)
module ForType
(T : TYPE)
(P : SEMI_LATTICE)
(P : MINIMAL_SEMI_LATTICE)
(G : DATA_FLOW_GRAPH with type variable = T.t and type property = P.property)
: SOLUTION
with type variable = G.variable
and type property = P.property option
(* [ForIntSegment] is a special case of [Run] where the type of variables
is the integer segment [0..n). An array is used to hold the table. *)
(**[ForIntSegment] is a special case of [Run] where the type of variables
is the integer segment [\[0..n)]. An array is used to hold the table. *)
module ForIntSegment
(K : sig val n: int end)
(P : SEMI_LATTICE)
(P : MINIMAL_SEMI_LATTICE)
(G : DATA_FLOW_GRAPH with type variable = int and type property = P.property)
: SOLUTION
with type variable = G.variable
......
......@@ -33,12 +33,22 @@ module HashCons = HashCons
module DataFlow = DataFlow
module Prop = struct
(* A number of ready-made implementations of the signature [PROPERTY]. *)
(**[Prop] offers a number of ready-made implementations of the
signature [PROPERTY]. *)
(**The lattice of Booleans. *)
module Boolean = Boolean
(* These declarations are set up so that the user sees [Prop.Option] and
[Prop.Set] as functors. *)
(* The following declarations are set up so that the user sees
[Prop.Option] and [Prop.Set] as functors. *)
(**The lattice of options. *)
include Option
(**The lattice of sets. *)
include Set
end
(* As a special case, [Core] is renamed [Fix]. Thus, if the user has declared
......
......@@ -10,21 +10,24 @@
(* *)
(******************************************************************************)
(* A gensym is a generator of unique integer identifiers. *)
(**[Gensym] offers a simple facility for generating fresh integer
identifiers. *)
(**A gensym is a generator of unique integer identifiers. *)
type gensym =
unit -> int
(* [make()] produces a new gensym. *)
(**[make()] produces a new gensym. *)
val make : unit -> gensym
(* A slightly more powerful abstraction is a generator whose current state
(**A slightly more powerful abstraction is a generator whose current state
can be inspected (without modification). *)
type generator
(* [generator()] creates a new generator. [fresh generator] causes the
(**[generator()] creates a new generator. [fresh generator] causes the
generator to create and return a fresh integer identifier. [current
generator] returns the generator's current state, that is, the next
available integer identifier. *)
......
......@@ -157,3 +157,16 @@ end
module HashTablesAsImperativeMaps (H : HashedType) =
Adapt(Hashtbl.Make(H))
module MinimalSemiLattice (P : SEMI_LATTICE) = struct
type property =
P.property
let leq_join p' p =
if P.leq p' p then
p
else
P.join p' p
end
......@@ -10,11 +10,14 @@
(* *)
(******************************************************************************)
(**[Glue] contains glue code that helps build various implementations of
association maps. *)
open Sigs
(* -------------------------------------------------------------------------- *)
(* Some common types, packaged as modules of signature [TYPE]. *)
(**Some common types, packaged as modules of signature [TYPE]. *)
module CHAR : TYPE with type t = char
module INT : TYPE with type t = int
......@@ -22,14 +25,14 @@ module STRING : TYPE with type t = string
(* -------------------------------------------------------------------------- *)
(* An arbitrary type can be equipped with an ordering function,
(**An arbitrary type can be equipped with an ordering function,
just by using OCaml's built-in generic comparison function. *)
module TrivialOrderedType
(T : TYPE)
: OrderedType with type t = T.t
(* An arbitrary type can be equipped with equality and hash functions,
(**An arbitrary type can be equipped with equality and hash functions,
just by using OCaml's built-in generic equality and hash functions. *)
module TrivialHashedType
......@@ -38,7 +41,7 @@ module TrivialHashedType
(* -------------------------------------------------------------------------- *)
(* If there is an injection of [t] into [u], then an ordering on [u] gives
(**If there is an injection of [t] into [u], then an ordering on [u] gives
rise to an ordering on [t]. *)
module InjectOrderedType
......@@ -46,7 +49,7 @@ module InjectOrderedType
(I : INJECTION with type u := U.t)
: OrderedType with type t = I.t
(* If there is an injection of [t] into [u], then a hashed-type structure
(**If there is an injection of [t] into [u], then a hashed-type structure
on [u] can be transported to [t]. *)
module InjectHashedType
......@@ -54,7 +57,7 @@ module InjectHashedType
(I : INJECTION with type u := U.t)
: HashedType with type t = I.t
(* If there is an injection of [t] into [u], then an implementation of minimal
(**If there is an injection of [t] into [u], then an implementation of minimal
imperative maps for the type [u] can be transported to the type [t]. *)
module InjectMinimalImperativeMaps
......@@ -62,7 +65,7 @@ module InjectMinimalImperativeMaps
(I : INJECTION with type u := M.key)
: MINIMAL_IMPERATIVE_MAPS with type key = I.t
(* If there is an injection of [t] into [u], and if the inverse mapping can be
(**If there is an injection of [t] into [u], and if the inverse mapping can be
effectively computed, then an implementation of imperative maps for the
type [u] can be transported to the type [t]. *)
......@@ -74,9 +77,9 @@ module InjectImperativeMaps
(* -------------------------------------------------------------------------- *)
(* Implementations of various map signatures. *)
(**Implementations of various map signatures. *)
(* An implementation of persistent maps can be made to satisfy the interface
(**An implementation of persistent maps can be made to satisfy the interface
of imperative maps. An imperative map is represented as a persistent map,
wrapped within a reference cell. *)
......@@ -85,7 +88,7 @@ module PersistentMapsToImperativeMaps
: IMPERATIVE_MAPS with type key = M.key
and type 'data t = 'data M.t ref
(* An implementation of imperative maps as arrays is possible if keys
(**An implementation of imperative maps as arrays is possible if keys
are consecutive integers. *)
module ArraysAsImperativeMaps
......@@ -93,9 +96,19 @@ module ArraysAsImperativeMaps
: IMPERATIVE_MAPS with type key = int
and type 'data t = 'data option array
(* An implementation of imperative maps as a hash table. *)
(**An implementation of imperative maps as a hash table. *)
module HashTablesAsImperativeMaps
(H : HashedType)
: IMPERATIVE_MAPS with type key = H.t
and type 'data t = 'data Hashtbl.Make(H).t
(* -------------------------------------------------------------------------- *)
(**[MinimalSemiLattice] converts a semi-lattice to a minimal semi-lattice;
that is, it implements [leq_join] in terms of separate [leq] and [join]
operations. *)
module MinimalSemiLattice
(P : SEMI_LATTICE)
: MINIMAL_SEMI_LATTICE with type property = P.property
(******************************************************************************)
(* *)
(* 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. *)
(* *)
(******************************************************************************)
(* 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. *)
(* -------------------------------------------------------------------------- *)
(* Nodes and edges. *)
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;
}
(* -------------------------------------------------------------------------- *)
(* Node creation. *)
let create data = {
data = data;
outgoing = [];
incoming = [];
marked = false;
}
(* Data access. *)
let data node =
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) =
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) =
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 =
List.iter (fun edge ->
assert (not edge.destroyed);
edge.destroyed <- true;
) node.outgoing;
node.outgoing <- []
<
(******************************************************************************)
(* *)
(* 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. *)
(* *)
(******************************************************************************)
(* 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