Commit a2da41f0 authored by Pietro Abate's avatar Pietro Abate
Browse files

Adapt Types.Descr.t to use the new BDD base data structure

parent 1c1ca633
......@@ -8,8 +8,8 @@ true: -traverse
<compile>: include
<schema>: include
<runtime>: include
#<{misc,types,typing,schema,compile,runtime}/*.cmx>: for-pack(Cduce_test)
<{misc,types}/*.cmx>: for-pack(Cduce_test)
<{misc,types,typing,schema,compile,runtime}/*.cmx>: for-pack(Cduce_test)
#<{misc,types}/*.cmx>: for-pack(Cduce_test)
<{misc,types}/*.cmx>: for-pack(Cduce_boolvar)
<parser/**>: package(ulex), package(netstring), syntax(camlp4o)
......
......@@ -17,4 +17,3 @@ Normal
Pretty
Stats
BoolVar
Types
......@@ -10,6 +10,7 @@ SortedList
Atoms
Bool
Chars
BoolVar
Ident
Intervals
Inttbl
......@@ -23,7 +24,6 @@ Parser
Builtin_defs
Cduce_loc
Sequence
Sample
Patterns
Lambda
Value
......
......@@ -170,21 +170,22 @@ module Sum(X : T)(Y : T) = struct
| Right t -> Format.fprintf ppf "R%a" Y.dump t
end
type 'a pairvar = Atm of 'a | Var of String.t
type var = [ `Var of String.t ]
type 'a pairvar = [ `Atm of 'a | var ]
module Var (X : T) = struct
type t = X.t pairvar
let hash = function Atm t -> X.hash t | Var s -> String.hash s
let check = function Atm t -> X.check t | Var _ -> ()
let hash = function `Atm t -> X.hash t | `Var s -> (* String.hash s *) Hashtbl.hash (`Var s)
let check = function `Atm t -> X.check t | `Var _ -> ()
let compare t1 t2 =
match t1,t2 with
|Atm x, Atm y -> X.compare x y
|Var x, Var y -> String.compare x y
|Var _, Atm _ -> -1
|Atm _, Var _ -> 1
|`Atm x, `Atm y -> X.compare x y
|`Var x, `Var y -> String.compare x y
|`Var _, `Atm _ -> -1
|`Atm _, `Var _ -> 1
let equal t1 t2 = (compare t1 t2) = 0
let dump ppf = function
|Atm x -> X.dump ppf x
|Var x -> String.dump ppf x
|`Atm x -> X.dump ppf x
|`Var x -> String.dump ppf x
end
......@@ -46,7 +46,7 @@ and pexpr =
(* CDuce is a Lambda-calculus ... *)
| Var of U.t
| TVar of Types.Vars.V.t
| TVar of BoolVar.Vars.V.t
| Apply of pexpr * pexpr
| Abstraction of abstr
......
......@@ -62,7 +62,7 @@ let tuple_queue =
List.fold_right (fun x q -> Pair (x, q))
let char = mknoloc (Internal (Types.char (Types.BoolChars.atom (Custom.Atm Chars.any))))
let char = mknoloc (Internal (Types.char (Types.BoolChars.atom (`Atm Chars.any))))
let string_regexp = Star (Elem char)
let seq_of_string s =
......@@ -298,7 +298,7 @@ EXTEND Gram
| e1 = expr; "&&"; e2 = expr -> exp _loc (logical_and e1 e2)
| e = expr; op = "/"; p = pat LEVEL "simple" ->
(* transform e with <(Atom)>[($$$::t|_)*] -> [$$$] *)
let tag = mk _loc (Internal (Types.atom (Types.BoolAtoms.atom (Custom.Atm (Atoms.any))))) in
let tag = mk _loc (Internal (Types.atom (Types.BoolAtoms.atom (`Atm (Atoms.any))))) in
let att = mk _loc (Internal Types.Record.any) in
let any = mk _loc (Internal Types.any) in
let re = Star(Alt(SeqCapture(noloc,id_dummy,Elem p), Elem any)) in
......@@ -307,7 +307,7 @@ EXTEND Gram
exp _loc (Transform (e,[p, Var id_dummy]))
| e = expr; "/@"; a = ident_or_keyword ->
(* transform e with <(Atom) {a=$$$}>_ -> [$$$] *)
let tag = mk _loc (Internal (Types.atom (Types.BoolAtoms.atom (Custom.Atm (Atoms.any))))) in
let tag = mk _loc (Internal (Types.atom (Types.BoolAtoms.atom (`Atm (Atoms.any))))) in
let any = mk _loc (Internal Types.any) in
let att = mk _loc (Record
(true, [(label a,
......@@ -330,7 +330,7 @@ EXTEND Gram
set_ref
(Var stk)
(concat (get_ref (Var stk)) (Pair (Var id_dummy,cst_nil))) in
let tag = mknoloc (Internal (Types.atom (Types.BoolAtoms.atom (Custom.Atm (Atoms.any))))) in
let tag = mknoloc (Internal (Types.atom (Types.BoolAtoms.atom (`Atm (Atoms.any))))) in
let att = mknoloc (Internal Types.Record.any) in
let any = mknoloc (Internal Types.any) in
let re = (SeqCapture(noloc,y,Star(Elem(any)))) in
......@@ -403,7 +403,7 @@ EXTEND Gram
tag: [ [ a = ident_or_keyword -> exp _loc (Atom (ident a)) ] ];
tag_type: [
[ "_" -> mk _loc (Internal (Types.atom (Types.BoolAtoms.atom (Custom.Atm (Atoms.any)))))
[ "_" -> mk _loc (Internal (Types.atom (Types.BoolAtoms.atom (`Atm (Atoms.any)))))
| "$"; a = ident_or_keyword -> mk _loc (Cst (TVar a))
| a = ident_or_keyword -> mk _loc (Cst (Atom (ident a)))
| t = ANY_IN_NS -> mk _loc (NsT (ident t))
......@@ -569,13 +569,13 @@ EXTEND Gram
| i = STRING1; "--"; j = STRING1 ->
let i = Chars.V.mk_int (parse_char _loc i)
and j = Chars.V.mk_int (parse_char _loc j) in
Elem (mk _loc (Internal (Types.char (Types.BoolChars.atom (Custom.Atm (Chars.char_class i j))))))
Elem (mk _loc (Internal (Types.char (Types.BoolChars.atom (`Atm (Chars.char_class i j))))))
| s = STRING1 ->
List.fold_right
(fun c accu ->
let c = Chars.V.mk_int c in
let c = Chars.atom c in
Seq (Elem (mknoloc (Internal (Types.char (Types.BoolChars.atom (Custom.Atm c))))), accu))
Seq (Elem (mknoloc (Internal (Types.char (Types.BoolChars.atom (`Atm c))))), accu))
(seq_of_string s)
Epsilon ]
| [ e = pat LEVEL "simple" -> Elem e
......@@ -619,20 +619,20 @@ EXTEND Gram
| i = INT ; "--"; j = INT ->
let i = Intervals.V.mk i
and j = Intervals.V.mk j in
mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (Custom.Atm (Intervals.bounded i j)))))
mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (`Atm (Intervals.bounded i j)))))
| i = INT ->
let i = Intervals.V.mk i in
mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (Custom.Atm (Intervals.atom i)))))
mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (`Atm (Intervals.atom i)))))
| "*"; "--"; j = INT ->
let j = Intervals.V.mk j in
mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (Custom.Atm (Intervals.left j)))))
mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (`Atm (Intervals.left j)))))
| i = INT; "--"; "*" ->
let i = Intervals.V.mk i in
mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (Custom.Atm (Intervals.right i)))))
mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (`Atm (Intervals.right i)))))
| i = char ->
mk _loc (Internal (Types.char (Types.BoolChars.atom (Custom.Atm (Chars.char_class i i)))))
mk _loc (Internal (Types.char (Types.BoolChars.atom (`Atm (Chars.char_class i i)))))
| i = char ; "--"; j = char ->
mk _loc (Internal (Types.char (Types.BoolChars.atom (Custom.Atm (Chars.char_class i j)))))
mk _loc (Internal (Types.char (Types.BoolChars.atom (`Atm (Chars.char_class i j)))))
| "`"; c = tag_type -> c
| "("; l = LIST1 pat SEP ","; ")" -> multi_prod _loc l
| "["; r = [ r = regexp -> r | -> Epsilon ];
......@@ -657,7 +657,7 @@ EXTEND Gram
(fun c ->
mknoloc (Internal
(Types.char
(Types.BoolChars.atom (Custom.Atm (
(Types.BoolChars.atom (`Atm (
(Chars.atom
(Chars.V.mk_int c))))))))
(seq_of_string s) in
......
......@@ -480,7 +480,7 @@ let int_type (name,min,max) =
| None, None ->
Intervals.any
in
ignore (primitive name (Types.interval (Types.BoolIntervals.atom (Custom.Atm ival))) (validate_interval ival name))
ignore (primitive name (Types.interval (Types.BoolIntervals.atom (`Atm ival))) (validate_interval ival name))
let () =
List.iter int_type [
......
......@@ -192,7 +192,7 @@ let simple_union name members =
let xsi_nil_atom = Atoms.V.mk (Schema_xml.xsi, Utf8.mk "nil")
let xsi_nil_type = Types.atom (Types.BoolAtoms.atom (Custom.Atm (Atoms.atom xsi_nil_atom)))
let xsi_nil_type = Types.atom (Types.BoolAtoms.atom (`Atm (Atoms.atom xsi_nil_atom)))
let xsi_nil_label = Ns.Label.mk (Schema_xml.xsi, Utf8.mk "nil")
let merge_attribute_uses l =
......
......@@ -7,22 +7,28 @@ module type S = sig
val mk_atm : string -> t
end
module BoolChars : S = struct
module BoolChars : S with type s = Chars.t = struct
include BoolVar.Make(Chars)
let mk_var s = atom (Custom.Var s)
let mk_atm c = atom (Custom.Atm (Chars.atom (Chars.V.mk_char c.[0] )))
let mk_var s = atom (`Var s)
let mk_atm c = atom (`Atm (Chars.atom (Chars.V.mk_char c.[0] )))
end
module BoolAtoms : S with type bt = Atoms.t = struct
module BoolAtoms : S with type s = Atoms.t = struct
include BoolVar.Make(Atoms)
let mk_var s = atom (Custom.Var s)
let mk_atm s = atom (Custom.Atm (Atoms.atom (Atoms.V.mk_ascii s)))
let mk_var s = atom (`Var s)
let mk_atm s = atom (`Atm (Atoms.atom (Atoms.V.mk_ascii s)))
end
module BoolIntervals : S = struct
module BoolIntervals : S with type s = Intervals.t = struct
include BoolVar.Make(Intervals)
let mk_var s = atom (Custom.Var s)
let mk_atm s = atom (Custom.Atm (Intervals.atom (Intervals.V.mk s)))
let mk_var s = atom (`Var s)
let mk_atm s = atom (`Atm (Intervals.atom (Intervals.V.mk s)))
end
module BoolVars : S with type s = BoolVar.Vars.t = struct
include BoolVar.BoolVars
let mk_var s = atom (`Var s)
let mk_atm s = failwith "AA"
end
module ExprParser (B : S) = struct
......@@ -58,6 +64,7 @@ end
module BCP = ExprParser(BoolChars)
module BAP = ExprParser(BoolAtoms)
module BIP = ExprParser(BoolIntervals)
module BVP = ExprParser(BoolVars)
(*
XXX this needs much more infrastructure as in types.ml
......@@ -73,14 +80,59 @@ let atoms_tests = [
"associativity union", BAP.os "(atm foo v atm bar) v atm baz", BAP.os "atm foo v (atm bar v atm baz)";
"difference", BAP.os "(atm foo ^ atm bar) v var alpha", BAP.os "var alpha";
"difference empty", BAP.os "atm foo ^ atm bar", BAP.os "Empty";
"splitvar vars empty", fst(BoolAtoms.splitvars (BAP.os "atm foo")), BAP.os "Empty";
"splitvar atm empty", snd(BoolAtoms.splitvars (BAP.os "var alpha")), BAP.os "Empty";
"splitvar vars 1 ", fst(BoolAtoms.splitvars (BAP.os "var alpha v (atm foo ^ var beta) v var gamma")), BAP.os "var alpha v var gamma";
"splitvar atm 1", snd(BoolAtoms.splitvars (BAP.os "var alpha v (atm foo ^ var beta) v var gamma")), BAP.os "atm foo ^ var beta";
"splitvar atm 2", snd(BoolAtoms.splitvars (BAP.os "var alpha v atm foo")), BAP.os "atm foo";
"splitvar vars 2", fst(BoolAtoms.splitvars (BAP.os "var alpha v atm foo")), BAP.os "var alpha";
];;
let atoms_splitvar_vars =
"vars splitvar" >:::
List.map (fun (descr, s1,s2) ->
(Printf.sprintf "test %s" descr) >:: (fun _ ->
assert_equal (BoolVar.BoolVars.equal ( s1 :> BoolVar.BoolVars.t ) s2) true
)
) [
"vars empty", fst(BoolAtoms.extractvars (BAP.os "atm foo")), BVP.os "Empty";
"vars 1 ", fst(BoolAtoms.extractvars (BAP.os "var alpha v (atm foo ^ var beta) v var gamma")), BVP.os "var alpha v var gamma";
"vars 2", fst(BoolAtoms.extractvars (BAP.os "var alpha v atm foo")), BVP.os "var alpha";
"vars 2", fst(BoolAtoms.extractvars (BAP.os "var alpha v atm foo")), fst(BoolChars.extractvars (BCP.os "var alpha v atm c"));
]
;;
let atoms_splitvar_atm =
"atoms splitvar" >:::
List.map (fun (descr, s1,s2) ->
(Printf.sprintf "test %s" descr) >:: (fun _ ->
assert_equal (BoolAtoms.equal s1 s2) true
)
) [
"atm empty", snd(BoolAtoms.extractvars (BAP.os "var alpha")), BAP.os "Empty";
"atm 1", snd(BoolAtoms.extractvars (BAP.os "var alpha v (atm foo ^ var beta) v var gamma")), BAP.os "atm foo ^ var beta";
"atm 2", snd(BoolAtoms.extractvars (BAP.os "var alpha v atm foo")), BAP.os "atm foo";
]
;;
let splitvar_mixed_union_var =
"splitvar union" >:::
List.map (fun (descr, s1,s2,r) ->
(Printf.sprintf "test %s" descr) >:: (fun _ ->
assert_equal (BoolVar.BoolVars.equal (BoolVar.BoolVars.cup s1 s2) r) true
)
) [
"atoms/chars", fst(BoolAtoms.extractvars (BAP.os "atm foo")), fst(BoolChars.extractvars (BCP.os "var alpha v atm x")), BVP.os "var alpha";
"atoms/chars", fst(BoolAtoms.extractvars (BAP.os "var alpha v atm foo")), fst(BoolChars.extractvars (BCP.os "var alpha v atm c")), BVP.os "var alpha";
]
;;
let splitvar_mixed_union_atm =
"splitvar union" >:::
List.map (fun (descr, s1,s2,r) ->
(Printf.sprintf "test %s" descr) >:: (fun _ ->
assert_equal (BoolAtoms.equal (BoolAtoms.cup s1 s2) r) true
)
) [
"atoms/chars", snd(BoolAtoms.extractvars (BAP.os "atm foo")), fst(BoolChars.extractvars (BCP.os "var alpha v atm x")), BAP.os "var alpha v atm foo";
]
;;
let atoms_structure =
"atoms structure" >:::
List.map (fun (descr, s1,s2) ->
......@@ -115,6 +167,11 @@ let atoms_contains =
let all =
"all tests" >::: [
atoms_structure;
atoms_contains;
atoms_splitvar_atm;
atoms_splitvar_vars;
splitvar_mixed_union_atm;
splitvar_mixed_union_var
]
let main () =
......
......@@ -17,7 +17,15 @@ Types.subtype t1 t2 ;;
let subtype_tests = [
"Int" , "Any", true;
"`a | Int" , "`a", false;
"`A | Int" , "`A", false;
"`A | ( 0--* | *--0)" , "`A", false;
"42 | Int" , "42", false;
"Int" , "Empty", false;
"'c' | Int" , "1", false;
"`A | Char" , "`A", false;
"`A | (`A,`B)" , "`A", false;
"`A -> `B | Int" , "`A -> `B", false;
"(`A,`B) | Int" , "(`A,`B)", false;
"Any" , "Any", true;
"Empty" , "Empty", true;
"Empty" , "Any", true;
......@@ -28,17 +36,16 @@ let subtype_tests = [
"1--5" , "1--*", true;
"1--5" , "1--5", true;
"Any -> `a" , "Any", true;
"`a -> `b | Int" , "`a -> `b", false;
"Any -> `A" , "Any", true;
"`a -> `b" , "`a -> `b", true;
"`A -> `B" , "`A -> `B", true;
"Any -> `a" , "Any -> Any", true;
"`a -> `b" , "Empty -> Any", true;
"(`a -> `c) | (`b -> `c)" , "(`a & `b) -> `c", true;
"(`a & `b) | (`a & `c)" , "`a & (`b | `c)", true;
"`a & (`b | `c)" , "(`a & `b) | (`a & `c)", true;
"(`a,`b) | (`c,`d)" , "((`a | `c) , (`b | `d))", true;
"(`a , `b & `c)" , "(`a,`b) & (`a,`c)", true;
"`A -> `B" , "Empty -> Any", true;
"(`A -> `C) | (`B -> `C)" , "(`A & `B) -> `C", true;
"(`A & `B) | (`A & `C)" , "`A & (`B | `C)", true;
"`A & (`B | `C)" , "(`A & `B) | (`A & `C)", true;
"(`A,`B) | (`C,`D)" , "((`A | `C) , (`B | `D))", true;
"(`A , `B & `C)" , "(`A,`B) & (`A,`C)", true;
(*
"mu x . Int -> (Nat , x)" , "mu x . Nat -> (Int , x)", true;
"mu x . (a,x)" , "mu y . (a,y)", true;
......@@ -46,16 +53,21 @@ let subtype_tests = [
"Any" , "Int", false ;
"Any" , "Empty", false ;
"`a -> `b" , "`a", false ;
"Any -> `a" , "Empty", false ;
"Any -> `a" , "Any -> Empty", false ;
"`a -> `b" , "`a -> `c", false ;
"`A -> `B" , "`A", false ;
"Any -> `A" , "Empty", false ;
"Any -> `A" , "Any -> Empty", false ;
"`A -> `B" , "`A -> `C", false ;
"Int" , "0--*", false ;
"1--5" , "1--4", false ;
"Int" , "0--*", false ;
"`$X" , "Any", true;
"`$X | Int" , "Any", true;
"Any", "`$X | (Any \\ `$X)", true;
"Any", "(42 & `$X) | (Any \\ (42 & `$X))", true;
"Any", "(41 & `$X) | (Any \\ (42 & `$X))", false;
"Any", "Any \\ Char", false;
];;
let test_subtype =
......@@ -64,7 +76,7 @@ let test_subtype =
(Printf.sprintf " %s <: %s " s1 s2) >:: (fun _ ->
let t1 = parse_typ s1 in
let t2 = parse_typ s2 in
let result = Types.subtype t1 t2 in
let result = Types.subtype t1 t2 in
if result <> expected then
begin
(* Printf.printf "subtyping error %s <: %s\n" s1 s2; *)
......
......@@ -19,12 +19,25 @@ end
module type S =
sig
type bt
type elem
include Custom.T
type s
type elem = s Custom.pairvar
type 'a bdd =
[ `True
| `False
| `Split of int * 'a * ('a bdd) * ('a bdd) * ('a bdd) ]
(*
include Custom.T
*)
type t = elem bdd
val dump : Format.formatter -> t -> unit
val check : t -> unit
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
(* returns the union of all leaves in the BDD *)
val get: t -> bt
val get: t -> s
(* val get': t -> (elem list * (elem list) list) list *)
......@@ -37,6 +50,7 @@ sig
val cap : t -> t -> t
val diff : t -> t -> t
val atom : elem -> t
val vars : Custom.var -> t
val iter: (elem-> unit) -> t -> unit
......@@ -46,14 +60,18 @@ sig
val is_empty : t -> bool
val splitvars : t -> t * t
val print: string -> t -> (Format.formatter -> unit) list
val trivially_disjoint: t -> t -> bool
val extractvars : t -> [> `Var of Custom.String.t ] bdd * t
end
(*
module type MAKE = functor (T : E) -> S with type elem = T.t Custom.pairvar
*)
(* ternary BDD
* where the nodes are Atm of X.t | Var of String.t
* Variables are always before Values
......@@ -72,115 +90,122 @@ end
*
* *)
(* module type MAKE = functor (T : E) -> S with type elem = T.t Custom.pairvar *)
module Make(T : E) =
module Make(T : E) : S with type s = T.t =
struct
(* ternary decision trees . cf section 11.3.3 Frish PhD *)
(* plus variables *)
(* Custom.Atm are containers (Atoms, Chars, Intervals, Pairs ... )
* Custom.Var are String
(* `Atm are containers (Atoms, Chars, Intervals, Pairs ... )
* `Var are String
*)
type bt = T.t
type s = T.t
module X = Custom.Var(T)
type elem = T.t Custom.pairvar
type t =
| True
| False
| Split of int * elem * t * t * t
let rec equal a b =
type elem = s Custom.pairvar
type 'a bdd =
[ `True
| `False
| `Split of int * 'a * ('a bdd) * ('a bdd) * ('a bdd) ]
type t = elem bdd
let rec equal_aux eq a b =
(a == b) ||
match (a,b) with
| Split (h1,x1,p1,i1,n1), Split (h2,x2,p2,i2,n2) ->
| `Split (h1,x1,p1,i1,n1), `Split (h2,x2,p2,i2,n2) ->
(h1 == h2) &&
(equal p1 p2) && (equal i1 i2) &&
(equal n1 n2) && (X.equal x1 x2)
(equal_aux eq p1 p2) && (equal_aux eq i1 i2) &&
(equal_aux eq n1 n2) && (eq x1 x2)
| _ -> false
let equal = equal_aux X.equal
(* Idea: add a mutable "unique" identifier and set it to
the minimum of the two when egality ... *)
let rec compare a b =
if (a == b) then 0
else match (a,b) with
| Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
| `Split (h1,x1, p1,i1,n1), `Split (h2,x2, p2,i2,n2) ->
if h1 < h2 then -1 else if h1 > h2 then 1
else let c = X.compare x1 x2 in if c <> 0 then c
else let c = compare p1 p2 in if c <> 0 then c
else let c = compare i1 i2 in if c <> 0 then c
else compare n1 n2
| True,_ -> -1
| _, True -> 1
| False,_ -> -1
| _,False -> 1
| `True,_ -> -1
| _, `True -> 1
| `False,_ -> -1
| _,`False -> 1
let rec hash = function
| True -> 1
| False -> 0
| Split(h, _,_,_,_) -> h
| `True -> 1
| `False -> 0
| `Split(h, _,_,_,_) -> h
let compute_hash x p i n =
(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
(Hashtbl.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
let rec check = function
| True | False -> ()
| Split (h,x,p,i,n) ->
| `True -> assert false;
| `False -> ()
| `Split (h,x,p,i,n) ->
assert (h = compute_hash x p i n);
(match p with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
(match i with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
(match n with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
(match p with `Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
(match i with `Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
(match n with `Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
X.check x; check p; check i; check n
let atom x =
let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
Split (h, x,True,False,False)
`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)
`Split (h, x,`False,`False,`True)
let vars v =
let a = atom (`Atm T.full) in
let h = compute_hash v a `False `False in
( `Split (h,v,a,`False,`False) :> t )
let rec iter f = function
| Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
| `Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
| _ -> ()
let rec dump ppf = function
| True -> Format.fprintf ppf "+"
| False -> Format.fprintf ppf "-"
| Split (_,x, p,i,n) ->
Format.fprintf ppf "%i(@[%a,%a,%a@])"
(* X.dump x *) (X.hash x) dump p dump i dump n
| `True -> Format.fprintf ppf "+"
| `False -> Format.fprintf ppf "-"
| `Split (_,x, p,i,n) ->
Format.fprintf ppf "%a(@[%a,%a,%a@])"
X.dump x (*X.hash x*) dump p dump i dump n