Commit f4b661e6 authored by Kim Nguyễn's avatar Kim Nguyễn

Finish refactoring bool and bool var. Use first class module without too much performance impact.

Move the bool.ml{,i} files in types/ where they belong.
parent 97f55b3a
......@@ -161,7 +161,7 @@ OBJECTS = \
driver/cduce_config.cmo misc/stats.cmo misc/custom.cmo misc/encodings.cmo \
misc/upool.cmo misc/pretty.cmo misc/ns.cmo misc/imap.cmo misc/html.cmo misc/utils.cmo \
\
types/compunit.cmo types/sortedList.cmo types/ident.cmo types/var.cmo misc/bool.cmo \
types/compunit.cmo types/sortedList.cmo types/ident.cmo types/var.cmo types/bool.cmo \
types/intervals.cmo types/chars.cmo types/atoms.cmo types/normal.cmo \
types/types.cmo compile/auto_pat.cmo \
types/sequence.cmo types/builtin_defs.cmo \
......
......@@ -30,8 +30,8 @@ types/var.cmo : misc/utils.cmo types/sortedList.cmi types/ident.cmo \
misc/custom.cmo types/var.cmi
types/var.cmx : misc/utils.cmx types/sortedList.cmx types/ident.cmx \
misc/custom.cmx types/var.cmi
misc/bool.cmo : types/var.cmi misc/custom.cmo misc/bool.cmi
misc/bool.cmx : types/var.cmx misc/custom.cmx misc/bool.cmi
types/bool.cmo : types/var.cmi misc/custom.cmo types/bool.cmi
types/bool.cmx : types/var.cmx misc/custom.cmx types/bool.cmi
types/intervals.cmo : types/intervals.cmi
types/intervals.cmx : types/intervals.cmi
types/chars.cmo : misc/custom.cmo types/chars.cmi
......@@ -45,12 +45,12 @@ types/normal.cmx : types/normal.cmi
types/types.cmo : types/var.cmi misc/utils.cmo misc/stats.cmi \
types/sortedList.cmi misc/pretty.cmi misc/ns.cmi types/normal.cmi \
types/intervals.cmi types/ident.cmo misc/encodings.cmi misc/custom.cmo \
types/compunit.cmi types/chars.cmi misc/bool.cmi types/atoms.cmi \
types/compunit.cmi types/chars.cmi types/bool.cmi types/atoms.cmi \
types/types.cmi
types/types.cmx : types/var.cmx misc/utils.cmx misc/stats.cmx \
types/sortedList.cmx misc/pretty.cmx misc/ns.cmx types/normal.cmx \
types/intervals.cmx types/ident.cmx misc/encodings.cmx misc/custom.cmx \
types/compunit.cmx types/chars.cmx misc/bool.cmx types/atoms.cmx \
types/compunit.cmx types/chars.cmx types/bool.cmx types/atoms.cmx \
types/types.cmi
compile/auto_pat.cmo : types/types.cmi types/ident.cmo types/chars.cmi \
types/atoms.cmi compile/auto_pat.cmi
......@@ -290,9 +290,9 @@ query/query_aggregates.cmo : runtime/value.cmi types/sequence.cmi \
compile/operators.cmi types/intervals.cmi types/builtin_defs.cmi
query/query_aggregates.cmx : runtime/value.cmx types/sequence.cmx \
compile/operators.cmx types/intervals.cmx types/builtin_defs.cmx
parser/cduce_curl.cmo : runtime/value.cmi parser/url.cmi \
parser/cduce_netclient.cmo : runtime/value.cmi parser/url.cmi \
driver/cduce_config.cmi
parser/cduce_curl.cmx : runtime/value.cmx parser/url.cmx \
parser/cduce_netclient.cmx : runtime/value.cmx parser/url.cmx \
driver/cduce_config.cmx
runtime/cduce_pxp.cmo : runtime/value.cmi parser/url.cmi \
schema/schema_xml.cmi runtime/load_xml.cmi driver/cduce_config.cmi \
......@@ -365,14 +365,14 @@ misc/html.cmi :
types/compunit.cmi :
types/sortedList.cmi : misc/custom.cmo
types/var.cmi : types/sortedList.cmi misc/custom.cmo
misc/bool.cmi : types/var.cmi misc/custom.cmo
types/intervals.cmi : misc/custom.cmo misc/bool.cmi
types/chars.cmi : misc/custom.cmo misc/bool.cmi
types/bool.cmi : types/var.cmi misc/custom.cmo
types/intervals.cmi : misc/custom.cmo types/bool.cmi
types/chars.cmi : misc/custom.cmo types/bool.cmi
types/atoms.cmi : misc/ns.cmi misc/encodings.cmi misc/custom.cmo \
misc/bool.cmi
types/bool.cmi
types/normal.cmi :
types/types.cmi : types/var.cmi misc/ns.cmi types/intervals.cmi \
types/ident.cmo misc/custom.cmo types/chars.cmi misc/bool.cmi \
types/ident.cmo misc/custom.cmo types/chars.cmi types/bool.cmi \
types/atoms.cmi
compile/auto_pat.cmi : types/types.cmi types/ident.cmo types/chars.cmi \
types/atoms.cmi
......
......@@ -15,7 +15,7 @@ sig
val cap : t -> t -> t
val diff : t -> t -> t
val atom : elem -> t
val is_empty : t -> bool
val iter: (elem-> unit) -> t -> unit
val compute:
......@@ -26,7 +26,6 @@ sig
atom:(elem -> 'b) -> t -> 'b
val trivially_disjoint: t -> t -> bool
end
......@@ -86,9 +85,8 @@ struct
let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
Split (h, x,True,False,False)
let neg_atom x =
let h = X.hash x + 16637 in (* partial evaluation of compute_hash... *)
Split (h, x,False,False,True)
let is_empty t = (t == False)
let rec iter f = function
| Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
......@@ -193,12 +191,25 @@ struct
| [] -> false
| b :: l -> (equal a b) || (has_same a l)
let rec split x p i n =
if i == True then True
else if equal p n then p ++ i
module type LeafOpts =
sig
val split0 : elem -> t -> t -> t ->t
val merge_leaves : elem -> elem -> bool
val cup : elem -> elem -> t
val cap : elem -> elem -> t
val diff : elem -> elem -> t
end
let make_ops (module LO : LeafOpts) =
let rec split x p i n =
if i == True then True
else if equal p n then p ++ i
else let p = simplify p [i] and n = simplify n [i] in
if equal p n then p ++ i
else split0 x p i n
else
LO.split0 x p i n
and simplify a l =
match a with
......@@ -228,92 +239,97 @@ struct
else match (a,b) with
| True, _ | _, True -> True
| False, a | a, False -> a
| Split (_,x1, True,False,False),
Split (_,x2, True,False,False) when LO.merge_leaves x1 x2 ->
LO.cup x1 x2
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
else if c < 0 then split x1 p1 (i1 ++ b) n1
else split x2 p2 (i2 ++ a) n2
(* seems better not to make ++ and this split mutually recursive;
(* seems better not to make ++ and this split mutually recursive;
is the invariant still inforced ? *)
in
let rec ( ** ) a b =
if a == b then a else
match (a,b) with
| True, a | a, True -> a
| False, _ | _, False -> False
| Split (_,x1, True,False,False),
Split (_,x2, True,False,False) when LO.merge_leaves x1 x2 ->
LO.cap x1 x2
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
split x1
(p1 ** (p2 ++ i2) ++ (p2 ** i1))
(i1 ** i2)
(n1 ** (n2 ++ i2) ++ (n2 ** i1))
else if c < 0 then split x1 (p1 ** b) (i1 ** b) (n1 ** b)
else split x2 (p2 ** a) (i2 ** a) (n2 ** a)
in
let rec neg = function
| True -> False
| False -> True
| Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
| Split (_,x, False,i,n) -> split x (neg i) (neg (i ++ n)) False
| Split (_,x, p,False,n) -> split x (neg p) (neg (p ++ n)) (neg n)
| Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
in
let rec ( // ) a b =
(* if equal a b then False *)
if a == b then False
else match (a,b) with
| False,_ | _, True -> False
| a, False -> a
| True, b -> neg b
| Split (_,x1, True,False,False),
Split (_,x2, True,False,False) when LO.merge_leaves x1 x2 ->
LO.diff x1 x2
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
if (i2 == False) && (n2 == False) then
split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
else
split x1 ((p1++i1) // (p2++i2)) False ((n1++i1) // (n2++i2))
else if c < 0 then
split x1 (p1 // b) (i1 // b) (n1 // b)
else
split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
in
let rec trivially_disjoint a b =
if a == b then a == False
else match (a,b) with
| True, a | a, True -> a == False
| False, _ | _, False -> true
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
(* try expanding -> p1 p2; p1 i2; i1 p2; i1 i2 ... *)
trivially_disjoint (p1 ++ i1) (p2 ++ i2) &&
trivially_disjoint (n1 ++ i1) (n2 ++ i2)
else if c < 0 then
trivially_disjoint p1 b &&
trivially_disjoint i1 b &&
trivially_disjoint n1 b
else
trivially_disjoint p2 a &&
trivially_disjoint i2 a &&
trivially_disjoint n2 a
in
( ++ ), ( ** ), ( // ),trivially_disjoint
let rec ( ** ) a b = if a == b then a else match (a,b) with
| True, a | a, True -> a
| False, _ | _, False -> False
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
split x1
(p1 ** (p2 ++ i2) ++ (p2 ** i1))
(i1 ** i2)
(n1 ** (n2 ++ i2) ++ (n2 ** i1))
(* if (p2 == True) && (n2 == False)
then split x1 (p1 ++ i1) (i1 ** i2) (n1 ** i2)
else if (p2 == False) && (n2 == True)
then split x1 (p1 ** i2) (i1 ** i2) (n1 ++ i1)
else
split x1 ((p1++i1) ** (p2 ++ i2)) False ((n1 ++ i1) ** (n2 ++ i2))
*)
else if c < 0 then split x1 (p1 ** b) (i1 ** b) (n1 ** b)
else split x2 (p2 ** a) (i2 ** a) (n2 ** a)
module SimpleOpts : LeafOpts = struct
let split0 = split0
let cup _ _ = assert false
let cap _ _ = assert false
let diff _ _ = assert false
let merge_leaves _ _ = false
end
let rec trivially_disjoint a b =
if a == b then a == False
else match (a,b) with
| True, a | a, True -> a == False
| False, _ | _, False -> true
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
(* try expanding -> p1 p2; p1 i2; i1 p2; i1 i2 ... *)
trivially_disjoint (p1 ++ i1) (p2 ++ i2) &&
trivially_disjoint (n1 ++ i1) (n2 ++ i2)
else if c < 0 then
trivially_disjoint p1 b &&
trivially_disjoint i1 b &&
trivially_disjoint n1 b
else
trivially_disjoint p2 a &&
trivially_disjoint i2 a &&
trivially_disjoint n2 a
let rec neg = function
| True -> False
| False -> True
| Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
| Split (_,x, False,i,n) -> split x (neg i) (neg (i ++ n)) False
| Split (_,x, p,False,n) -> split x (neg p) (neg (p ++ n)) (neg n)
(* | Split (_,x, p, False, False) ->
split x False (neg p) True
| Split (_,x, False, False, n) -> split x True (neg n) False *)
| Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
let rec ( // ) a b =
(* if equal a b then False *)
if a == b then False
else match (a,b) with
| False,_ | _, True -> False
| a, False -> a
| True, b -> neg b
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
if (i2 == False) && (n2 == False)
then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
(* else if (i2 == False) && (p2 == False)
then split x1 (p1 ++ i1) (i1 // n2) (n1 // n2) *)
else
split x1 ((p1++i1) // (p2 ++ i2)) False ((n1++i1) // (n2 ++ i2))
else if c < 0 then
split x1 (p1 // b) (i1 // b) (n1 // b)
(* split x1 ((p1 ++ i1)// b) False ((n1 ++i1) // b) *)
else
split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
let cup = ( ++ )
let cap = ( ** )
let diff = ( // )
let cup, cap, diff, trivially_disjoint = make_ops (module SimpleOpts)
end
......@@ -331,7 +347,6 @@ sig
val leafconj: t -> Atom.t
val is_empty : t -> bool
val extract : t -> [ `Empty | `Full | `Split of (elem * t * t * t) ]
end
......@@ -367,164 +382,43 @@ struct
(aux T.empty x)
let full = split0 (`Atm T.full) True False False
let is_empty = function False -> true | _ -> false
let rec split x p i n =
if X.equal (`Atm T.empty) x then False
(* 0?p:i:n -> 0 *)
else if i == True then True
(* x?p:1:n -> 1 *)
else if equal p n then p ++ i
else let p = simplify p [i] and n = simplify n [i] in
(* x?p:i:n when p = n -> bdd of (p ++ i) *)
if equal p n then p ++ i
else split0 x p i n
let split0 a p i n =
match a, p, i, n with
`Atm x, True, False, False when T.is_empty x -> False
| `Atm _, True, False, False
| `Var _, _, _, _ -> split0 a p i n
| `Atm _, _, _, _ -> assert false
(* simplify t l -> bdd of ( t // l ) *)
and simplify a l =
match a with
| False -> False
| True -> if has_true l then False else True
| Split (_,`Atm x, False,False,True) ->
split (`Atm(T.diff T.full x)) True False False
| Split (_,x,p,i,n) ->
if (has_true l) || (has_same a l) then False
else s_aux2 a x p i n [] [] [] l
and s_aux2 a x p i n ap ai an = function
| [] ->
let p = simplify p ap
and n = simplify n an
and i = simplify i ai in
if equal p n then p ++ i else split0 x p i n
| b :: l -> s_aux3 a x p i n ap ai an l b
and s_aux3 a x p i n ap ai an l = function
| False -> s_aux2 a x p i n ap ai an l
| True -> assert false
| Split (_,x2,p2,i2,n2) as b ->
if equal a b then False
else let c = X.compare x2 x in
if c < 0 then s_aux3 a x p i n ap ai an l i2
else if c > 0 then s_aux2 a x p i n (b :: ap) (b :: ai) (b :: an) l
else s_aux2 a x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
(* Inv : all leafs are of type Atm and they are always merged *)
(* union *)
and ( ++ ) a b = if a == b then a
else match (a,b) with
| True, _ | _, True -> True
| False, a | a, False -> a
| Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, True,False,False) ->
split (`Atm (T.cup x1 x2)) True False False
| Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, False,False,True)
| Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, False,False,True)
| Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, True,False,False) ->
assert false
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
else if c < 0 then split x1 p1 (i1 ++ b) n1
else split x2 p2 (i2 ++ a) n2
(* seems better not to make ++ and this split mutually recursive;
is the invariant still inforced ? *)
(* intersection *)
let rec ( ** ) a b = if a == b then a else match (a,b) with
| True, a | a, True -> a
| False, _ | _, False -> False
| Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, True,False,False) ->
split (`Atm(T.cap x1 x2)) True False False
| Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, False,False,True) ->
split (`Atm(T.cap (T.diff T.full x1) (T.diff T.full x2))) True False False
| Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, False,False,True) ->
split (`Atm(T.cap x1 (T.diff T.full x2))) True False False
| Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, True,False,False) ->
split (`Atm(T.cap (T.diff T.full x1) x2)) True False False
let full = split0 (`Atm T.full) True False False
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
split x1
(p1 ** (p2 ++ i2) ++ (p2 ** i1))
(i1 ** i2)
(n1 ** (n2 ++ i2) ++ (n2 ** i1))
else if c < 0 then split x1 (p1 ** b) (i1 ** b) (n1 ** b)
else split x2 (p2 ** a) (i2 ** a) (n2 ** a)
let rec trivially_disjoint a b =
if a == b then a == False
else match (a,b) with
| True, a | a, True -> a == False
| False, _ | _, False -> true
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
(* try expanding -> p1 p2; p1 i2; i1 p2; i1 i2 ... *)
trivially_disjoint (p1 ++ i1) (p2 ++ i2) &&
trivially_disjoint (n1 ++ i1) (n2 ++ i2)
else if c < 0 then
trivially_disjoint p1 b &&
trivially_disjoint i1 b &&
trivially_disjoint n1 b
else
trivially_disjoint p2 a &&
trivially_disjoint i2 a &&
trivially_disjoint n2 a
let rec neg = function
| True -> False
| False -> True
| Split (_,`Atm x, True,False,False) -> split0 (`Atm(T.diff T.full x)) True False False
| Split (_,`Atm x, False,False,True) -> split0 (`Atm(T.diff T.full x)) True False False
| Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
| Split (_,x, False,i,n) -> split x (neg i) (neg (i ++ n)) False
| Split (_,x, p,False,n) -> split x (neg p) (neg (p ++ n)) (neg n)
| Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
let rec ( // ) a b =
let negatm = T.diff T.full in
if a == b then False
else match (a,b) with
| False,_ | _, True -> False
| a, False -> a
| True, b -> neg b
| Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, True,False,False) ->
split (`Atm(T.diff x1 x2)) True False False
| Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, False,False,True) ->
split (`Atm(T.diff (negatm x1) (negatm x2))) True False False
| Split (_,`Atm x1, True,False,False), Split (_,`Atm x2, False,False,True) ->
split (`Atm(T.diff x1 (negatm x2))) True False False
| Split (_,`Atm x1, False,False,True), Split (_,`Atm x2, True,False,False) ->
split (`Atm(T.diff (negatm x1) x2)) True False False
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
if (i2 == False) && (n2 == False)
then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
else
split x1 ((p1++i1) // (p2 ++ i2)) False ((n1++i1) // (n2 ++ i2))
else if c < 0 then
split x1 (p1 // b) (i1 // b) (n1 // b)
else
split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
let cup = ( ++ )
let cap = ( ** )
let diff = ( // )
module VarOpts : LeafOpts = struct
let split0 = split0
let cup a b =
match a, b with
`Atm x1, `Atm x2 ->
split0 (`Atm (T.cup x1 x2)) True False False
| _ -> assert false
let cap a b =
match a, b with
`Atm x1, `Atm x2 ->
split0 (`Atm (T.cap x1 x2)) True False False
| _ -> assert false
let diff a b =
match a, b with
`Atm x1, `Atm x2 ->
split0 (`Atm (T.diff x1 x2)) True False False
| _ -> assert false
let merge_leaves a b =
match a, b with
`Atm _, `Atm _ -> true
| _ -> false
end
let cup, cap, diff, trivially_disjoint = make_ops (module VarOpts)
let extract =
function
......
......@@ -11,7 +11,7 @@ sig
val cap : t -> t -> t
val diff : t -> t -> t
val atom : elem -> t
val is_empty : t -> bool
val iter: (elem-> unit) -> t -> unit
val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment