From 9b75e9a2074c357fc2c823156451209d2a4cef8b Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Wed, 19 Dec 2012 16:33:58 +0100 Subject: [PATCH] Compile again. --- src/formula.ml | 36 ++++++++++-------------------------- src/formula.mli | 6 ++---- src/pretty.ml | 1 + src/pretty.mli | 1 + src/ptset.ml | 12 ++++++------ src/qNameSet.ml | 20 +++++++++++++++++++- src/qNameSet.mli | 7 ++++++- src/sigs.ml | 1 - 8 files changed, 45 insertions(+), 39 deletions(-) diff --git a/src/formula.ml b/src/formula.ml index 1dd0f14..4c58e3c 100644 --- a/src/formula.ml +++ b/src/formula.ml @@ -60,7 +60,7 @@ module rec Node : Hcons.S end type t = Node.t -let hash x = x.Node.key +let hash x = x.Node.hash let uid x = x.Node.id let equal = Node.equal let expr f = f.Node.node.pos @@ -96,6 +96,9 @@ let rec print ?(parent=false) ppf f = match dir with | `Left -> Pretty.down_arrow, Pretty.subscript 1 | `Right -> Pretty.down_arrow, Pretty.subscript 2 + | `Epsilon -> Pretty.epsilon, "" + | `Up1 -> Pretty.up_arrow, Pretty.subscript 1 + | `Up2 -> Pretty.up_arrow, Pretty.subscript 2 in fprintf fmt "%s%s" a_str d_str; State.print fmt s; @@ -111,36 +114,20 @@ let is_true f = (expr f) == True let is_false f = (expr f) == False -let cons pos neg s1 s2 size1 size2 = - let nnode = Node.make { pos = neg; neg = (Obj.magic 0); st = s2; size = size2 } in - let pnode = Node.make { pos = pos; neg = nnode ; st = s1; size = size1 } in +let cons pos neg = + let nnode = Node.make { pos = neg; neg = (Obj.magic 0); } in + let pnode = Node.make { pos = pos; neg = nnode } in (Node.node nnode).neg <- pnode; (* works because the neg field isn't taken into account for hashing ! *) pnode,nnode -let empty_pair = StateSet.empty, StateSet.empty -let true_,false_ = cons True False empty_pair empty_pair 0 0 +let true_,false_ = cons True False let atom_ d p s = - let si = StateSet.singleton s in - let ss = match d with - | `Left -> si, StateSet.empty - | `Right -> StateSet.empty, si - in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1) + fst (cons (Move(d,p,s)) (Move(d,not p,s))) let not_ f = f.Node.node.neg -let union_pair (l1,r1) (l2, r2) = - StateSet.union l1 l2, - StateSet.union r1 r2 - -let merge_states f1 f2 = - let sp = - union_pair (st f1) (st f2) - and sn = - union_pair (st (not_ f1)) (st (not_ f2)) - in - sp,sn let order f1 f2 = if uid f1 < uid f2 then f2,f1 else f1,f2 @@ -159,10 +146,7 @@ let or_ f1 f2 = (* commutativity of | *) else let f1, f2 = order f1 f2 in - let psize = (size f1) + (size f2) in - let nsize = (size (not_ f1)) + (size (not_ f2)) in - let sp, sn = merge_states f1 f2 in - fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)) sp sn psize nsize) + fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2))) let and_ f1 f2 = diff --git a/src/formula.mli b/src/formula.mli index 9b2659f..78edcfc 100644 --- a/src/formula.mli +++ b/src/formula.mli @@ -15,7 +15,8 @@ (** Implementation of hashconsed Boolean formulae *) -type move = [ `Left |`Right ] +type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ] + (** Direction for automata predicates *) type 'formula expr = @@ -52,9 +53,6 @@ val expr : t -> t expr val compare : t -> t -> int (** Comparison of formulae *) -val size : t -> int -(** Syntactic size of the formula *) - val print : Format.formatter -> t -> unit (** Pretty printer *) diff --git a/src/pretty.ml b/src/pretty.ml index 02c413f..bd9d410 100644 --- a/src/pretty.ml +++ b/src/pretty.ml @@ -86,6 +86,7 @@ let up_arrow = "↑" let right_arrow = "→" let left_arrow = "←" let epsilon = "ϵ" +let big_sigma = "∑" let cap = "∩" let cup = "∪" let lnot = "¬" diff --git a/src/pretty.mli b/src/pretty.mli index cb1b870..fb7e309 100644 --- a/src/pretty.mli +++ b/src/pretty.mli @@ -22,6 +22,7 @@ val up_arrow : string val right_arrow : string val left_arrow : string val epsilon : string +val big_sigma : string val cap : string val cup : string val lnot : string diff --git a/src/ptset.ml b/src/ptset.ml index 774b9fc..c4a1b33 100644 --- a/src/ptset.ml +++ b/src/ptset.ml @@ -119,10 +119,10 @@ struct loop 7 let hbit = Array.init 256 naive_highest_bit - (* - external clz : int -> int = "caml_clz" "noalloc" - external leading_bit : int -> int = "caml_leading_bit" "noalloc" - *) + (* + external clz : int -> int = "caml_clz" "noalloc" + external leading_bit : int -> int = "caml_leading_bit" "noalloc" + *) let highest_bit x = try let n = (x) lsr 24 in @@ -182,14 +182,14 @@ struct in rmv t - (* should run in O(1) thanks to Hash consing *) + (* should run in O(1) thanks to hash consing *) let equal a b = Node.equal a b let compare a b = (Uid.to_int (Node.uid a)) - (Uid.to_int (Node.uid b)) let rec merge s t = - if (equal s t) (* This is cheap thanks to hash-consing *) + if equal s t (* This is cheap thanks to hash-consing *) then s else match Node.node s, Node.node t with diff --git a/src/qNameSet.ml b/src/qNameSet.ml index 4035957..87c750e 100644 --- a/src/qNameSet.ml +++ b/src/qNameSet.ml @@ -15,4 +15,22 @@ include FiniteCofinite.Make(Ptset.Make(QName)) -module Weak = FiniteCofinite.Weak(Ptset.Weak(QName)) +let print_finite fmt e conv = + Format.fprintf fmt "{"; + Pretty.print_list ~sep:"," QName.print fmt (conv e); + Format.fprintf fmt "}" + +let printer fmt e test conv inv = + if test e then print_finite fmt e conv + else begin + Format.fprintf fmt "%s \\ " Pretty.big_sigma; + print_finite fmt (inv e) conv + end + +let print fmt e = printer fmt e is_finite elements complement + +module Weak = +struct + include FiniteCofinite.Weak(Ptset.Weak(QName)) + let print fmt e = printer fmt e is_finite elements complement +end diff --git a/src/qNameSet.mli b/src/qNameSet.mli index 71d1478..10c3be3 100644 --- a/src/qNameSet.mli +++ b/src/qNameSet.mli @@ -18,5 +18,10 @@ or cofinite *) include FiniteCofinite.S with type elt = QName.t +include Sigs.AUX.Printable with type t := t -module Weak : FiniteCofinite.S with type elt = QName.t +module Weak : + sig + include FiniteCofinite.S with type elt = QName.t + include Sigs.AUX.Printable with type t := t + end diff --git a/src/sigs.ml b/src/sigs.ml index dc98baf..9fc3e86 100644 --- a/src/sigs.ml +++ b/src/sigs.ml @@ -151,7 +151,6 @@ struct (** Equality between hashconsed values. Equivalent to [==] *) val equal : t -> t -> bool - (** Initializes the internal storage. Any previously hashconsed element is discarded. *) val init : unit -> unit -- 2.17.1