From 4f265eb7d78b740292b5543d94f9f0fa40d206d5 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Wed, 12 Oct 2016 10:41:26 +0200 Subject: [PATCH] * Seal the representation of states * Compile with -principal -warning-error @3 --- Remakefile.in | 2 +- configure.in | 2 +- src/ata.ml | 20 ++++++++++---------- src/cache.ml | 6 +++--- src/hcons.mli | 2 +- src/naive_tree.ml | 4 ++-- src/ptset.ml | 2 +- src/ptset.mli | 2 +- src/run.ml | 8 ++++---- src/state.ml | 21 ++++++--------------- src/state.mli | 10 ++++------ src/stateSet.ml | 2 +- src/stateSet.mli | 2 +- src/xpath/compile.ml | 12 ++++++------ 14 files changed, 42 insertions(+), 53 deletions(-) diff --git a/Remakefile.in b/Remakefile.in index 1ff0b30..c1f2b25 100644 --- a/Remakefile.in +++ b/Remakefile.in @@ -17,7 +17,7 @@ OCAMLDEP = @OCAMLDEP@ ODEPS = tools/odeps.sh $(OCAMLDEP) OCAMLC = @OCAMLC@ OCAMLOPT = @OCAMLOPT@ -OCAMLFLAGS = @OCAMLFLAGS@ +OCAMLFLAGS = @OCAMLFLAGS@ OCAMLOPTFLAGS = @OCAMLOPTFLAGS@ OCAMLCFLAGS = @OCAMLCFLAGS@ OCAMLYACC = @OCAMLYACC@ diff --git a/configure.in b/configure.in index 5bcb4c0..297c4e5 100644 --- a/configure.in +++ b/configure.in @@ -168,7 +168,7 @@ fi #compilation options #debugging mode -OCAMLFLAGS=$OCAMLFLAGS +OCAMLFLAGS="-principal -warn-error @3 $OCAMLFLAGS" CAMLP4FLAGS=$CAMLP4FLAGS OCAMLCFLAGS=$OCAMLCFLAGS OCAMLOPTFLAGS=$OCAMLOPTFLAGS diff --git a/src/ata.ml b/src/ata.ml index 190c4c7..5f7a282 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -184,8 +184,8 @@ module Transition = type t = State.t * QNameSet.t * Formula.t let equal (a, b, c) (d, e, f) = a == d && b == e && c == f - let hash (a, b, c) = - HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int)) + let hash ((a, b, c) : t) = + HASHINT4 (PRIME1, ((a) :> int), ((QNameSet.uid b) :> int), ((Formula.uid c) :> int)) end) let print ppf t = let q, l, f = t.node in @@ -276,10 +276,10 @@ let print fmt a = ) ([], 0, 0) sorted_trs in let line = Pretty.line (max_all + max_pre + 6) in - let prev_q = ref State.dummy in + let prev_q = ref State.dummy_state in fprintf fmt "%s@\n" line; List.iter (fun (q, s1, s2, s3) -> - if !prev_q != q && !prev_q != State.dummy then fprintf fmt "%s@\n" line; + if !prev_q != q && !prev_q != State.dummy_state then fprintf fmt "%s@\n" line; prev_q := q; fprintf fmt "%s, %s" s1 s2; fprintf fmt "%s" @@ -387,7 +387,7 @@ let normalize_negations auto = with Not_found -> (* create a new state and add it to the todo queue *) - let nq = State.make () in + let nq = State.next () in auto.states <- StateSet.add nq auto.states; Hashtbl.add memo_state (q, false) nq; Queue.add (q, false) todo; nq @@ -409,7 +409,7 @@ let normalize_negations auto = with Not_found -> let nq = if b then q else - let nq = State.make () in + let nq = State.next () in auto.states <- StateSet.add nq auto.states; nq in @@ -597,7 +597,7 @@ let rename_states mapper a = let copy a = let mapper = Hashtbl.create MED_H_SIZE in let () = - StateSet.iter (fun q -> Hashtbl.add mapper q (State.make())) a.states + StateSet.iter (fun q -> Hashtbl.add mapper q (State.next())) a.states in rename_states mapper a @@ -657,7 +657,7 @@ let link a1 a2 q link_phi = let union a1 a2 = let a1 = copy a1 in let a2 = copy a2 in - let q = State.make () in + let q = State.next () in let link_phi = StateSet.fold (fun q phi -> Formula.(or_ (stay q) phi)) @@ -669,7 +669,7 @@ let union a1 a2 = let inter a1 a2 = let a1 = copy a1 in let a2 = copy a2 in - let q = State.make () in + let q = State.next () in let link_phi = StateSet.fold (fun q phi -> Formula.(and_ (stay q) phi)) @@ -680,7 +680,7 @@ let inter a1 a2 = let neg a = let a = copy a in - let q = State.make () in + let q = State.next () in let link_phi = StateSet.fold (fun q phi -> Formula.(and_ (not_(stay q)) phi)) diff --git a/src/cache.ml b/src/cache.ml index d0f7ac5..e5ee434 100644 --- a/src/cache.ml +++ b/src/cache.ml @@ -24,7 +24,7 @@ struct type 'a index = int -> 'a let level a = a.level let create_with_level level a = { - line = Array.create 0 a; + line = Array.make 0 a; dummy = a; offset = ~-1; level = level; @@ -41,7 +41,7 @@ struct if i < offset then begin (* bottom resize *) let pad = offset - i in let nlen = len + pad in - let narray = Array.create nlen a.dummy in + let narray = Array.make nlen a.dummy in for j = 0 to len - 1 do narray.(j+pad) <- a.line.(j) done; @@ -51,7 +51,7 @@ struct end else begin (* top resize *) (* preventively allocate the space for the following elements *) let nlen = ((i - offset + 1) lsl 1) + 1 in - let narray = Array.create nlen a.dummy in + let narray = Array.make nlen a.dummy in for j = 0 to len - 1 do narray.(j) <- a.line.(j); done; diff --git a/src/hcons.mli b/src/hcons.mli index 05def66..6a6ede8 100644 --- a/src/hcons.mli +++ b/src/hcons.mli @@ -35,7 +35,7 @@ module Weak (H : Common_sig.HashedType) : S with type data = H.t explicitely by calling [init]. *) -module PosInt : Abstract with type data = int and type t = int +module PosInt : Abstract with type data = int and type t = private int (** Compact implementation of hashconsed positive integer that avoids boxing. [PosInt.make v] raises [Invalid_argument] if [ v < 0 ] diff --git a/src/naive_tree.ml b/src/naive_tree.ml index 38421e0..3cefe18 100644 --- a/src/naive_tree.ml +++ b/src/naive_tree.ml @@ -211,7 +211,7 @@ first_child=%a; next_sibling=%a; parent=%a }" Expat.final psr; let root = List.hd ctx.stack in root.next_sibling <- nil; - let a = Array.create ctx.current_preorder nil in + let a = Array.make ctx.current_preorder nil in let rec loop n = if n != nil then begin @@ -244,7 +244,7 @@ first_child=%a; next_sibling=%a; parent=%a }" Expat.Expat_error e -> error e parser_ let parse_file fd = - let buffer = String.create 4096 in + let buffer = String.make 4096 '\000' in let parser_, finalize = create_parser () in let rec loop () = let read = input fd buffer 0 4096 in diff --git a/src/ptset.ml b/src/ptset.ml index 779d24f..4dbd1a3 100644 --- a/src/ptset.ml +++ b/src/ptset.ml @@ -374,7 +374,7 @@ struct include Make(Hcons.PosInt) let print ppf s = Format.pp_print_string ppf "{ "; - iter (fun i -> Format.fprintf ppf "%i " i) s; + iter (fun i -> Format.fprintf ppf "%i " (i :> int)) s; Format.pp_print_string ppf "}"; Format.pp_print_flush ppf () end diff --git a/src/ptset.mli b/src/ptset.mli index 632832c..076e824 100644 --- a/src/ptset.mli +++ b/src/ptset.mli @@ -25,5 +25,5 @@ module Weak (H : Hcons.Abstract) : S with type elt = H.t with weak internal storage. See {!Hcons.Weak}. *) -module PosInt : S with type elt = int +module PosInt : S with type elt = Hcons.PosInt.t (** Implementation of hashconsed sets of positive integers *) diff --git a/src/run.ml b/src/run.ml index be8bbeb..0ae25f9 100644 --- a/src/run.ml +++ b/src/run.ml @@ -66,7 +66,7 @@ struct ((Obj.magic kind) lsl 4) end -let dummy_set = StateSet.singleton State.dummy +let dummy_set = StateSet.singleton State.dummy_state @@ -107,9 +107,9 @@ type 'a run = { stats : stats; } -let dummy_form = Ata.Formula.stay State.dummy +let dummy_form = Ata.Formula.stay State.dummy_state -let get_form run tag q = +let get_form run tag (q : State.t) = let auto = run.auto in let fetch_trans_cache = run.fetch_trans_cache in let stats = run.stats in @@ -211,7 +211,7 @@ struct { tree = tree; auto = auto; - sat = (let a = Array.create len StateSet.empty in + sat = (let a = Array.make len StateSet.empty in IFHTML([a], a)); pass = 0; fetch_trans_cache = Cache.N2.create dummy_form; diff --git a/src/state.ml b/src/state.ml index 4fbfc1c..4b02d59 100644 --- a/src/state.ml +++ b/src/state.ml @@ -14,23 +14,14 @@ (***********************************************************************) open Format +include Hcons.PosInt -type t = int -let make = +let next = let id = ref ~-1 in - fun () -> incr id; !id + fun () -> incr id; make !id -let compare = (-) +let compare (a : t) (b : t) = (a :> int) - (b :> int) -let equal = (==) +let print fmt (x : t) = fprintf fmt "q%a" Pretty.pp_subscript (x :> int) -external hash : t -> int = "%identity" - -let print fmt x = fprintf fmt "q%a" Pretty.pp_subscript x - -let dump fmt x = print fmt x - -let check x = - if x < 0 then failwith (Printf.sprintf "State: Assertion %i < 0 failed" x) - -let dummy = max_int +let dummy_state = make max_int diff --git a/src/state.mli b/src/state.mli index 1d25a67..8b4420c 100644 --- a/src/state.mli +++ b/src/state.mli @@ -14,13 +14,11 @@ (***********************************************************************) (** Implementation of states *) +include module type of Hcons.PosInt +include Common_sig.OrderedType with type t := t -include Common_sig.Type with type t = int - -val make : unit -> t -(** Generate a fresh state *) - -val dummy : t +val next : unit -> t +val dummy_state : t (** Dummy state that can never be returned by [make ()] *) val print : Format.formatter -> t -> unit diff --git a/src/stateSet.ml b/src/stateSet.ml index 47ad460..c55ff6e 100644 --- a/src/stateSet.ml +++ b/src/stateSet.ml @@ -15,7 +15,7 @@ open Format -include Ptset.Make (Hcons.PosInt) +include Ptset.Make (State) let print ppf s = fprintf ppf "{ %a }" diff --git a/src/stateSet.mli b/src/stateSet.mli index 1a628a4..30c5063 100644 --- a/src/stateSet.mli +++ b/src/stateSet.mli @@ -14,7 +14,7 @@ (***********************************************************************) (** Implementation of sets of states *) -include Ptset.S with type elt = int +include Ptset.S with type elt = State.t val print : Format.formatter -> t -> unit (** Pretty printer *) diff --git a/src/xpath/compile.ml b/src/xpath/compile.ml index e8ab6fc..20f06be 100644 --- a/src/xpath/compile.ml +++ b/src/xpath/compile.ml @@ -40,7 +40,7 @@ let root_set = QNameSet.singleton QName.document *) let compile_axis_test axis (test,kind) phi trans states = - let q = State.make () in + let q = State.next () in let phi = match kind with Tree.NodeKind.Node -> phi | _ -> phi %% F.is kind @@ -65,7 +65,7 @@ let compile_axis_test axis (test,kind) phi trans states = ]) :: trans, states) | Descendant true -> - let q' = State.make () in + let q' = State.next () in (F.stay q ++ F.first_child q', (q', [ QNameSet.any => F.stay q ++ F.first_child q' ++ F.next_sibling q'; ]):: @@ -73,7 +73,7 @@ let compile_axis_test axis (test,kind) phi trans states = states) | Parent -> - let q' = State.make () in + let q' = State.next () in let move = F.parent q ++ F.previous_sibling q' in (move, (q, [ test => phi ]) @@ -81,7 +81,7 @@ let compile_axis_test axis (test,kind) phi trans states = (q' @: states)) | Ancestor self -> - let q' = State.make () in + let q' = State.next () in let move = F.parent q' ++ F.previous_sibling q' in (if self then F.stay q ++ F.stay q' else F.stay q'), (q', [ QNameSet.any => move ++ F.parent q]) @@ -208,7 +208,7 @@ let compile_top_level_step_list l trans states = in loop ll trans2 states2 phi2 in - let starting = State.make () in + let starting = State.next () in let phi0, trans0, states0 = compile_axis_test Self @@ -236,7 +236,7 @@ let path p = let builder = Ata.Builder.make () in (** ensure that we have a single selecting state at the end *) let phi_sel = StateSet.fold (fun q acc -> F.or_ (F.stay q) acc) mstates F.false_ in - let q_sel = State.make () in + let q_sel = State.next () in let states = StateSet.add q_sel states in let mstates = StateSet.singleton q_sel in let trans = (q_sel, [QNameSet.any, phi_sel]) :: trans in -- 2.17.1