Merge remote-tracking branch 'origin/fix'

This modifies the analyses in [Grammar] to use [Fix] as the fixed point
computation algorithm.

src/Boolean.ml

+(* The Boolean lattice. *)
+
+type property =
+    bool
+
+let bottom =
+  false
+
+let equal (b1 : bool) (b2 : bool) =
+  b1 = b2
+
+let is_maximal b =
+  b
+

src/Boolean.mli

+include Fix.PROPERTY with type property = bool
+

src/CompletedNat.ml

+(* The natural numbers, completed with [Infinity], and ordered towards
+   zero (i.e. [Infinity] is [bottom], [Finite 0] is [top]). *)
+
+type t =
+| Finite of int
+| Infinity
+
+type property =
+  t
+
+let equal p1 p2 =
+  match p1, p2 with
+  | Finite i1, Finite i2 ->
+      i1 = i2
+  | Infinity, Infinity ->
+      true
+  | _, _ ->
+      false
+
+let bottom =
+  Infinity
+
+let is_maximal p =
+  match p with
+  | Finite 0 ->
+      true
+  | _ ->
+      false
+
+let min p1 p2 =
+  match p1, p2 with
+  | Finite i1, Finite i2 ->
+      if i1 <= i2 then p1 else p2
+  | p, Infinity
+  | Infinity, p ->
+      p
+
+let min_lazy p1 p2 =
+  match p1 with
+  | Finite 0 ->
+      p1
+  | _ ->
+      min p1 (Lazy.force p2)
+
+let add p1 p2 =
+  match p1, p2 with
+  | Finite i1, Finite i2 ->
+      Finite (i1 + i2)
+  | _, _ ->
+      Infinity
+
+let add_lazy p1 p2 =
+  match p1 with
+  | Infinity ->
+      Infinity
+  | _ ->
+      add p1 (Lazy.force p2)
+
+let print p =
+  match p with
+  | Finite i ->
+      string_of_int i
+  | Infinity ->
+      "infinity"

src/CompletedNat.mli

+(* The natural numbers, completed with [Infinity], and ordered towards
+   zero (i.e. [Infinity] is [bottom], [Finite 0] is [top]). *)
+
+type t =
+| Finite of int
+| Infinity
+
+include Fix.PROPERTY with type property = t
+
+val min: t -> t -> t
+val add: t -> t -> t
+
+val min_lazy: t -> t Lazy.t -> t
+val add_lazy: t -> t Lazy.t -> t
+
+val print: t -> string

src/CompletedNatWitness.ml

+(* This is an enriched version of [CompletedNat], where we compute not just
+   numbers, but also lists of matching length. During the fixed point
+   computation, instead of manipulating actual lists, we manipulate only
+   recipes for constructing lists. These recipes can be evaluated by the user
+   after the fixed point has been reached. *)
+
+(* A property is either [Finite (n, xs)], where [n] is a natural number and
+   [xs] is a (recipe for constructing a) list of length [n]; or [Infinity]. *)
+
+type 'a t =
+| Finite of int * 'a list Lazy.t
+| Infinity
+
+let equal p1 p2 =
+  match p1, p2 with
+  | Finite (i1, _), Finite (i2, _) ->
+      i1 = i2
+  | Infinity, Infinity ->
+      true
+  | _, _ ->
+      false
+
+let bottom =
+  Infinity
+
+let is_maximal p =
+  match p with
+  | Finite (0, _) ->
+      true
+  | _ ->
+      false
+
+let min p1 p2 =
+  match p1, p2 with
+  | Finite (i1, _), Finite (i2, _) ->
+      if i1 <= i2 then p1 else p2
+  | p, Infinity
+  | Infinity, p ->
+      p
+
+let min_lazy p1 p2 =
+  match p1 with
+  | Finite (0, _) ->
+      p1
+  | _ ->
+      min p1 (Lazy.force p2)
+
+let add p1 p2 =
+  match p1, p2 with
+  | Finite (i1, xs1), Finite (i2, xs2) ->
+      Finite (
+        i1 + i2,
+        (* The only list operation in the code! *)
+        lazy (Lazy.force xs1 @ Lazy.force xs2)
+      )
+  | _, _ ->
+      Infinity
+
+let add_lazy p1 p2 =
+  match p1 with
+  | Infinity ->
+      Infinity
+  | _ ->
+      add p1 (Lazy.force p2)
+
+let print conv p =
+  match p with
+  | Finite (i, xs) ->
+      string_of_int i ^ " " ^
+      String.concat " " (List.map conv (Lazy.force xs))
+  | Infinity ->
+      "infinity"

src/CompletedNatWitness.mli

+(* This is an enriched version of [CompletedNat], where we compute not just
+   numbers, but also lists of matching length. During the fixed point
+   computation, instead of manipulating actual lists, we manipulate only
+   recipes for constructing lists. These recipes can be evaluated by the user
+   after the fixed point has been reached. *)
+
+(* A property is either [Finite (n, xs)], where [n] is a natural number and
+   [xs] is a (recipe for constructing a) list of length [n]; or [Infinity]. *)
+
+type 'a t =
+| Finite of int * 'a list Lazy.t
+| Infinity
+
+val bottom: 'a t
+val equal: 'a t -> 'b t -> bool
+val is_maximal: 'a t -> bool
+
+val min: 'a t -> 'a t -> 'a t
+val add: 'a t -> 'a t -> 'a t
+
+val min_lazy: 'a t -> 'a t Lazy.t -> 'a t
+val add_lazy: 'a t -> 'a t Lazy.t -> 'a t
+
+val print: ('a -> string) -> 'a t -> string

src/Maps.ml

+(* BEGIN PERSISTENT_MAPS *)
+module type PERSISTENT_MAPS = sig
+  type key
+  type 'data t
+  val empty: 'data t
+  val add: key -> 'data -> 'data t -> 'data t
+  val find: key -> 'data t -> 'data
+  val iter: (key -> 'data -> unit) -> 'data t -> unit
+end
+(* END PERSISTENT_MAPS *)
+
+(* BEGIN IMPERATIVE_MAPS *)
+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
+(* END IMPERATIVE_MAPS *)
+
+(* BEGIN IMPERATIVE_MAP *)
+module type IMPERATIVE_MAP = sig
+  type key
+  type data
+  val set: key -> data -> unit
+  val get: key -> data option
+end
+(* END IMPERATIVE_MAP *)
+
+module PersistentMapsToImperativeMaps
+  (M : PERSISTENT_MAPS)
+     : IMPERATIVE_MAPS with type key = M.key
+		        and type 'data t = 'data M.t ref
+= struct
+
+  type key =
+      M.key
+  
+  type 'data t =
+      'data M.t ref
+      
+  let create () =
+    ref M.empty
+
+  let clear t =
+    t := M.empty
+    
+  let add k d t =
+    t := M.add k d !t
+
+  let find k t =
+    M.find k !t
+
+  let iter f t =
+    M.iter f !t
+
+end
+
+module ImperativeMapsToImperativeMap
+  (M : IMPERATIVE_MAPS)
+  (D : sig type data end)
+     : IMPERATIVE_MAP with type key = M.key
+		       and type data = D.data
+= struct
+
+  type key =
+      M.key
+
+  type data =
+      D.data
+
+  let m =
+    M.create()
+
+  let set k d =
+    M.add k d m
+
+  let get k =
+    try
+      Some (M.find k m)
+    with Not_found ->
+      None
+
+end
+
+module ConsecutiveIntegerKeysToImperativeMaps
+  (K : sig val n: int end)
+  : IMPERATIVE_MAPS with type key = int
+                     and type 'data t = 'data option array
+
+= struct
+
+  open K
+
+  type key =
+      int
+
+  type 'data t =
+      'data option array
+
+  let create () =
+    Array.make n None
+
+  let clear m =
+    Array.fill m 0 n None
+
+  let add key data m =
+    m.(key) <- Some data
+
+  let find key m =
+    match m.(key) with
+    | None ->
+	raise Not_found
+    | Some data ->
+	data
+
+  let iter f m =
+    Array.iteri (fun key data ->
+      match data with
+      | None ->
+	  ()
+      | Some data ->
+	  f key data
+    ) m
+
+end
+
+module HashTableAsImperativeMaps
+  (H : Hashtbl.HashedType)
+     : IMPERATIVE_MAPS with type key = H.t
+= struct
+
+  include Hashtbl.Make(H)
+
+  let create () =
+    create 1023
+
+  let add key data table =
+    add table key data
+
+  let find table key =
+    find key table
+
+end
+
+module TrivialHashedType
+  (T : sig type t end)
+     : Hashtbl.HashedType with type t = T.t
+= struct
+
+  include T
+
+  let equal =
+    (=)
+
+  let hash =
+    Hashtbl.hash
+
+end
+

src/Maps.mli

+(* This module defines three signatures for association maps, together
+   with a number of conversion functors. *)
+
+(* Following the convention of the ocaml standard library, the [find]
+   functions raise [Not_found] when the key is not a member of the
+   domain of the map. By contrast, [get] returns an option. *)
+
+(* BEGIN PERSISTENT_MAPS *)
+module type PERSISTENT_MAPS = sig
+  type key
+  type 'data t
+  val empty: 'data t
+  val add: key -> 'data -> 'data t -> 'data t
+  val find: key -> 'data t -> 'data
+  val iter: (key -> 'data -> unit) -> 'data t -> unit
+end
+(* END PERSISTENT_MAPS *)
+
+(* BEGIN IMPERATIVE_MAPS *)
+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
+(* END IMPERATIVE_MAPS *)
+
+(* BEGIN IMPERATIVE_MAP *)
+module type IMPERATIVE_MAP = sig
+  type key
+  type data
+  val set: key -> data -> unit
+  val get: key -> data option
+end
+(* END IMPERATIVE_MAP *)
+
+(* 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. *)
+
+module PersistentMapsToImperativeMaps
+  (M : PERSISTENT_MAPS)
+     : IMPERATIVE_MAPS with type key = M.key
+		        and type 'data t = 'data M.t ref
+
+(* An implementation of imperative maps can be made to satisfy the interface
+   of a single imperative map. This map is obtained via a single call to [create]. *)
+
+module ImperativeMapsToImperativeMap
+  (M : IMPERATIVE_MAPS)
+  (D : sig type data end)
+     : IMPERATIVE_MAP with type key = M.key
+		       and type data = D.data
+
+(* An implementation of imperative maps as arrays is possible if keys
+   are consecutive integers. *)
+
+module ConsecutiveIntegerKeysToImperativeMaps
+  (K : sig val n: int end)
+  : IMPERATIVE_MAPS with type key = int
+                     and type 'data t = 'data option array
+
+(* An implementation of imperative maps as a hash table. *)
+
+module HashTableAsImperativeMaps
+  (H : Hashtbl.HashedType)
+     : IMPERATIVE_MAPS with type key = H.t
+
+(* A trivial implementation of equality and hashing. *)
+
+module TrivialHashedType
+  (T : sig type t end)
+     : Hashtbl.HashedType with type t = T.t
+

src/conflict.ml

@@ -187,14 +187,14 @@ let rec follow1 tok derivation offset' = function
 	 at the moment, so let's skip it. *)
       derivation
   | (item, _, offset) :: configs ->
-      let _, _, rhs, pos, length = Item.def item in
+      let prod, _, rhs, pos, length = Item.def item in
       if offset = offset' then
 
 	(* This is an epsilon transition. Attack a new line and add
 	   a comment that explains why the lookahead symbol is
 	   produced or inherited. *)
 	
-	let nullable, first = Analysis.nullable_first_rhs rhs (pos + 1) in
+	let nullable, first = Analysis.nullable_first_prod prod (pos + 1) in
 
 	if TerminalSet.mem tok first then
 
@@ -304,7 +304,7 @@ let explain_reduce_item
       if pos < length then
 	match rhs.(pos) with
 	| Symbol.N nt ->
-	    let nullable, first = Analysis.nullable_first_rhs rhs (pos + 1) in
+	    let nullable, first = Analysis.nullable_first_prod prod (pos + 1) in
 	    let first : bool = TerminalSet.mem tok first in
 	    let lookahead' =
 	      if nullable then first || lookahead else first

src/grammar.mli

@@ -373,12 +373,12 @@ module Analysis : sig
 
   val first: Nonterminal.t -> TerminalSet.t
 
-  (* [nullable_first_rhs rhs i] considers the string of symbols found at
-     offset [i] in the array [rhs]. It returns its NULLABLE flag as well
+  (* [nullable_first_prod prod i] considers the suffix of the the production
+     [prod] defined by offset [i]. It returns its NULLABLE flag as well
      as its FIRST set. The offset [i] must be contained between [0] and
-     [n], where [n] is the length of [rhs], inclusive. *)
+     [n], inclusive, where [n] is the length of production [prod]. *)
 
-  val nullable_first_rhs: Symbol.t array -> int -> bool * TerminalSet.t
+  val nullable_first_prod: Production.index -> int -> bool * TerminalSet.t
 
   (* [explain_first_rhs tok rhs i] explains why the token [tok] appears
      in the FIRST set for the string of symbols found at offset [i] in

src/invariant.ml

@@ -170,7 +170,9 @@ open StateLattice
 let stack_states : Lr1.node -> property =
 
   let module F =
-    Fix.Make(Lr1.ImperativeNodeMap)(StateLattice)
+    Fix.Make
+      (Maps.PersistentMapsToImperativeMaps(Lr1.NodeMap))
+      (StateLattice)
   in
 
   F.lfp (fun node (get : Lr1.node -> property) ->

src/item.ml

@@ -171,7 +171,7 @@ module Closure (L : Lookahead.S) = struct
 
 	let constant, transmits =
 	  if pos < length then
-	    let nullable, first = Analysis.nullable_first_rhs rhs (pos + 1) in
+	    let nullable, first = Analysis.nullable_first_prod prod (pos + 1) in
 	    L.constant first, nullable
 	  else
 	    (* No epsilon transitions leave this item. *)

src/lr1.ml

@@ -64,31 +64,6 @@ module NodeSet =
 module NodeMap =
   Map.Make (Node)
 
-module ImperativeNodeMap = struct
-
-  type key =
-      NodeMap.key
-
-  type 'data t =
-      'data NodeMap.t ref
-
-  let create () =
-    ref NodeMap.empty
-
-  let clear t =
-    t := NodeMap.empty
-
-  let add k d t =
-    t := NodeMap.add k d !t
-
-  let find k t =
-    NodeMap.find k !t
-
-  let iter f t =
-    NodeMap.iter f !t
-
-end
-
 (* ------------------------------------------------------------------------ *)
 
 (* Output debugging information if [--follow-construction] is enabled. *)

src/lr1.mli

@@ -25,8 +25,6 @@ module NodeSet : Set.S with type elt = node
 
 module NodeMap : Map.S with type key = node
 
-module ImperativeNodeMap : Fix.IMPERATIVE_MAPS with type key = node
-
 (* These are the automaton's entry states, indexed by the start productions. *)
 
 val entry: node ProductionMap.t