No commit message

No commit message

Version

+# Why/Jessie/Krakatoa version
+VERSION=2.21
+# Caduceus version
+CVERSION=1.21

src/hashcons.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) Jean-Christophe Filliatre                               *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(*s Hash tables for hash-consing. (Some code is borrowed from the ocaml
+    standard library, which is copyright 1996 INRIA.) *)
+
+let gentag =
+  let r = ref 0 in
+  fun () -> incr r; !r
+
+module type HashedType =
+  sig
+    type node
+    val equal : node -> node -> bool
+    val hash : node -> int
+
+    type t
+    val node : t -> node
+  end
+
+module type S =
+  sig
+    type node
+    type t
+    val hashcons : node -> (node -> int -> t) -> t
+    val iter : (t -> unit) -> unit
+    val stats : unit -> int * int * int * int * int * int
+  end
+
+module Make(H : HashedType) : (S with type node = H.node and type t = H.t) = 
+struct
+
+  type node = H.node
+  type t = H.t
+
+  type table = {
+    mutable table : t Weak.t array;
+    mutable totsize : int;             (* sum of the bucket sizes *)
+    mutable limit : int;               (* max ratio totsize/table length *)
+  }
+
+  let emptybucket = Weak.create 0
+
+  let create sz =
+    let sz = if sz < 7 then 7 else sz in
+    let sz = if sz > Sys.max_array_length then Sys.max_array_length else sz in
+    {
+      table = Array.create sz emptybucket;
+      totsize = 0;
+      limit = 3;
+    }
+
+  let clear t =
+    for i = 0 to Array.length t.table - 1 do
+      t.table.(i) <- emptybucket
+    done;
+    t.totsize <- 0;
+    t.limit <- 3
+  
+  let fold f t init =
+    let rec fold_bucket i b accu =
+      if i >= Weak.length b then accu else
+      match Weak.get b i with
+      | Some v -> fold_bucket (i+1) b (f v accu)
+      | None -> fold_bucket (i+1) b accu
+    in
+    Array.fold_right (fold_bucket 0) t.table init
+
+  let count t =
+    let rec count_bucket i b accu =
+      if i >= Weak.length b then accu else
+      count_bucket (i+1) b (accu + (if Weak.check b i then 1 else 0))
+    in
+    Array.fold_right (count_bucket 0) t.table 0
+
+  let next_sz n = min (3*n/2 + 3) (Sys.max_array_length - 1)
+
+  let rec resize t =
+    let oldlen = Array.length t.table in
+    let newlen = next_sz oldlen in
+    if newlen > oldlen then begin
+      let newt = create newlen in
+      newt.limit <- t.limit + 100;          (* prevent resizing of newt *)
+      fold (fun d () -> add newt d (H.hash (H.node d))) t ();
+      t.table <- newt.table;
+      t.limit <- t.limit + 2;
+    end
+
+  and add t d hkey =
+    let index = hkey mod (Array.length t.table) in
+    let bucket = t.table.(index) in
+    let sz = Weak.length bucket in
+    let rec loop i =
+      if i >= sz then begin
+        let newsz = min (sz + 3) (Sys.max_array_length - 1) in
+        if newsz <= sz then 
+	  failwith "Hashcons.Make: hash bucket cannot grow more";
+        let newbucket = Weak.create newsz in
+        Weak.blit bucket 0 newbucket 0 sz;
+        Weak.set newbucket i (Some d);
+        t.table.(index) <- newbucket;
+        t.totsize <- t.totsize + (newsz - sz);
+        if t.totsize > t.limit * Array.length t.table then resize t;
+      end else begin
+        if Weak.check bucket i
+        then loop (i+1)
+        else Weak.set bucket i (Some d)
+      end
+    in
+    loop 0
+
+  let t = create 5003
+
+  let hashcons d f =
+    let hkey = H.hash d in
+    let index = hkey mod (Array.length t.table) in
+    let bucket = t.table.(index) in
+    let sz = Weak.length bucket in
+    let rec loop i =
+      if i >= sz then begin
+	let hnode = f d (gentag ()) in
+	add t hnode hkey;
+	hnode
+      end else begin
+        match Weak.get_copy bucket i with
+        | Some v when H.equal (H.node v) d -> 
+	    begin match Weak.get bucket i with
+              | Some v -> v
+              | None -> loop (i+1)
+            end
+        | _ -> loop (i+1)
+      end
+    in
+    loop 0
+  
+  let iter f =
+    let rec iter_bucket i b =
+      if i >= Weak.length b then () else
+      match Weak.get b i with
+      | Some v -> f v; iter_bucket (i+1) b
+      | None -> iter_bucket (i+1) b
+    in
+    Array.iter (iter_bucket 0) t.table
+
+  let stats () =
+    let len = Array.length t.table in
+    let lens = Array.map Weak.length t.table in
+    Array.sort compare lens;
+    let totlen = Array.fold_left ( + ) 0 lens in
+    (len, count t, totlen, lens.(0), lens.(len/2), lens.(len-1))
+  
+end

src/hashcons.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) Jean-Christophe Filliatre                               *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(*s Hash tables for hash consing. 
+
+    Hash consed values are of the
+    following type [hash_consed]. The field [tag] contains a unique
+    integer (for values hash consed with the same table). The field
+    [hkey] contains the hash key of the value (without modulo) for
+    possible use in other hash tables (and internally when hash
+    consing tables are resized). The field [node] contains the value
+    itself. 
+
+    Hash consing tables are using weak pointers, so that values that are no
+    more referenced from anywhere else can be erased by the GC. *)
+
+module type HashedType =
+  sig
+    type node
+    val equal : node -> node -> bool
+    val hash : node -> int
+
+    type t
+    val node : t -> node
+  end
+
+module type S =
+  sig
+    type node
+    type t
+
+    val hashcons : node -> (node -> int -> t) -> t
+      (** [hashcons n f] hash-cons the value [n] using function [f] i.e. returns
+	  any existing value in the table equal to [n], if any; 
+	  otherwise, creates a new value with function [f], stores it
+	  in the table and returns it. Function [f] is passed
+	  the node [n] as first argument and the unique id as second argument.
+      *)
+
+    val iter : (t -> unit) -> unit
+      (** [iter f] iterates [f] over all elements of the table . *)
+    val stats : unit -> int * int * int * int * int * int
+      (** Return statistics on the table.  The numbers are, in order:
+	  table length, number of entries, sum of bucket lengths,
+	  smallest bucket length, median bucket length, biggest 
+	  bucket length. *)
+  end
+
+module Make(H : HashedType) : (S with type node = H.node and type t = H.t)

version.sh

+ #!/bin/sh
+
+# Note: the BINDIR variable is a free variable
+# Note: the LIBDIR variable is a free variable
+# Note: the COQVER variable is a free variable
+# Note: the mkdirs are needed for the Ocamlbuild Makefile.
+
+. ./Version
+
+# Why
+WHYVF=src/version.ml
+mkdir -p src
+echo "let coqversion = \"$COQVER\"" > $WHYVF
+echo "let version = \"$VERSION\"" >> $WHYVF
+echo "let date = \""`date`"\"" >> $WHYVF
+echo "let bindir = \"$BINDIR\"" >> $WHYVF
+echo "let libdir = \"$LIBDIR/why\"" >> $WHYVF
+
+
+# Doc
+DOCF=doc/version.tex
+mkdir -p doc
+printf '\\newcommand{\\whyversion}{'$VERSION'}\n' > $DOCF
+printf '\\newcommand{\\caduceusversion}{'$CVERSION'}\n' >> $DOCF