* Seal the representation of states
authorKim Nguyễn <kim.nguyen@lri.fr>
Wed, 12 Oct 2016 08:41:26 +0000 (10:41 +0200)
committerKim Nguyễn <kim.nguyen@lri.fr>
Wed, 12 Oct 2016 08:41:26 +0000 (10:41 +0200)
* Compile with -principal -warning-error @3

14 files changed:
Remakefile.in
configure.in
src/ata.ml
src/cache.ml
src/hcons.mli
src/naive_tree.ml
src/ptset.ml
src/ptset.mli
src/run.ml
src/state.ml
src/state.mli
src/stateSet.ml
src/stateSet.mli
src/xpath/compile.ml

index 1ff0b30..c1f2b25 100644 (file)
@@ -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@
index 5bcb4c0..297c4e5 100644 (file)
@@ -168,7 +168,7 @@ fi
 
 #compilation options
 #debugging mode
-OCAMLFLAGS=$OCAMLFLAGS
+OCAMLFLAGS="-principal -warn-error @3 $OCAMLFLAGS"
 CAMLP4FLAGS=$CAMLP4FLAGS
 OCAMLCFLAGS=$OCAMLCFLAGS
 OCAMLOPTFLAGS=$OCAMLOPTFLAGS
index 190c4c7..5f7a282 100644 (file)
@@ -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))
index d0f7ac5..e5ee434 100644 (file)
@@ -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;
index 05def66..6a6ede8 100644 (file)
@@ -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 ]
index 38421e0..3cefe18 100644 (file)
@@ -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
index 779d24f..4dbd1a3 100644 (file)
@@ -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
index 632832c..076e824 100644 (file)
@@ -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 *)
index be8bbeb..0ae25f9 100644 (file)
@@ -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;
index 4fbfc1c..4b02d59 100644 (file)
 (***********************************************************************)
 
 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
index 1d25a67..8b4420c 100644 (file)
 (***********************************************************************)
 
 (** 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
index 47ad460..c55ff6e 100644 (file)
@@ -15,7 +15,7 @@
 
 open Format
 
-include Ptset.Make (Hcons.PosInt)
+include Ptset.Make (State)
 
 let print ppf s =
   fprintf ppf "{ %a }"
index 1a628a4..30c5063 100644 (file)
@@ -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 *)
index e8ab6fc..20f06be 100644 (file)
@@ -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