Commit 6ee6ef2e authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Improve pretty printing of Bdds and add debug directive to interactively...

Improve pretty printing of Bdds and add debug directive to interactively inspect the internal representation of types.
parent edd4e79d
...@@ -9,11 +9,11 @@ exception InvalidObjectFilename of string ...@@ -9,11 +9,11 @@ exception InvalidObjectFilename of string
let extra_specs = ref [] let extra_specs = ref []
(* if set to false toplevel exception aren't cought. (* if set to false toplevel exception aren't cought.
* Useful for debugging with OCAMLRUNPARAM="b" *) * Useful for debugging with OCAMLRUNPARAM="b" *)
let catch_exceptions = true let catch_exceptions = true
(* retuns a filename without the suffix suff if any *) (* retuns a filename without the suffix suff if any *)
let prefix filename suff = let prefix filename suff =
if Filename.check_suffix filename suff then if Filename.check_suffix filename suff then
try try
...@@ -39,7 +39,7 @@ let rec is_abstraction = function ...@@ -39,7 +39,7 @@ let rec is_abstraction = function
| Ast.LocatedExpr (_,e) -> is_abstraction e | Ast.LocatedExpr (_,e) -> is_abstraction e
| _ -> false | _ -> false
let print_norm ppf d = let print_norm ppf d =
Types.Print.pp_type ppf ((*Types.normalize*) d) Types.Print.pp_type ppf ((*Types.normalize*) d)
let print_sample ppf s = let print_sample ppf s =
...@@ -74,7 +74,7 @@ let directive_help ppf = ...@@ -74,7 +74,7 @@ let directive_help ppf =
#reinit_ns;; reinitialize namespace processing #reinit_ns;; reinitialize namespace processing
#help;; shows this help message #help;; shows this help message
#print_type <type>;; dump internal representation of <type> #print_type <type>;; dump internal representation of <type>
#debug ;; #debug ;;
#silent;; turn off outputs from the toplevel #silent;; turn off outputs from the toplevel
#verbose;; turn on outputs from the toplevel #verbose;; turn on outputs from the toplevel
#builtins;; shows embedded OCaml values #builtins;; shows embedded OCaml values
...@@ -83,7 +83,8 @@ let directive_help ppf = ...@@ -83,7 +83,8 @@ let directive_help ppf =
let directive_help_debug ppf = let directive_help_debug ppf =
Format.fprintf ppf Format.fprintf ppf
"Debug sub-directives: "Debug sub-directives:
#debug sybtype <type> <type> ;; check if t1 < t2 for all substitutions #debug subtype <type> <type> ;; check if t1 < t2 for all substitutions
#debug bdd <type>;; dump the internal type representation
#debug typed <expr> ;; dump typed internal representation #debug typed <expr> ;; dump typed internal representation
#debug lambda <expr> ;; dump lambda internal representation #debug lambda <expr> ;; dump lambda internal representation
#debug accept <???> ;; #debug accept <???> ;;
...@@ -95,33 +96,33 @@ let directive_help_debug ppf = ...@@ -95,33 +96,33 @@ let directive_help_debug ppf =
let rec print_exn ppf = function let rec print_exn ppf = function
| Location (loc, w, exn) -> | Location (loc, w, exn) ->
Cduce_loc.print_loc ppf (loc,w); Cduce_loc.print_loc ppf (loc,w);
Cduce_loc.html_hilight (loc,w); Cduce_loc.html_hilight (loc,w);
print_exn ppf exn print_exn ppf exn
| Value.CDuceExn v -> | Value.CDuceExn v ->
Format.fprintf ppf "Uncaught CDuce exception: @[%a@]@." Format.fprintf ppf "Uncaught CDuce exception: @[%a@]@."
print_value v print_value v
| Typer.WrongLabel (t,l) -> | Typer.WrongLabel (t,l) ->
Format.fprintf ppf "Wrong record selection; field %a " Format.fprintf ppf "Wrong record selection; field %a "
Label.print_attr l; Label.print_attr l;
Format.fprintf ppf "not present in an expression of type:@.%a@." Format.fprintf ppf "not present in an expression of type:@.%a@."
print_norm t print_norm t
| Typer.ShouldHave (t,msg) -> | Typer.ShouldHave (t,msg) ->
Format.fprintf ppf "This expression should have type:@.%a@.%a@." Format.fprintf ppf "This expression should have type:@.%a@.%a@."
print_norm t print_norm t
print_protect msg print_protect msg
| Typer.ShouldHave2 (t1,msg,t2) -> | Typer.ShouldHave2 (t1,msg,t2) ->
Format.fprintf ppf "This expression should have type:@.%a@.%a %a@." Format.fprintf ppf "This expression should have type:@.%a@.%a %a@."
print_norm t1 print_norm t1
print_protect msg print_protect msg
print_norm t2 print_norm t2
| Typer.Error s -> | Typer.Error s ->
Format.fprintf ppf "%a@." print_protect s Format.fprintf ppf "%a@." print_protect s
| Typer.Constraint (s,t) -> | Typer.Constraint (s,t) ->
Format.fprintf ppf "This expression should have type:@.%a@." Format.fprintf ppf "This expression should have type:@.%a@."
print_norm t; print_norm t;
Format.fprintf ppf "but its inferred type is:@.%a@." Format.fprintf ppf "but its inferred type is:@.%a@."
print_norm s; print_norm s;
Format.fprintf ppf "which is not a subtype, as shown by the sample:@.%a@." Format.fprintf ppf "which is not a subtype, as shown by the sample:@.%a@."
print_sample (Sample.get (Types.diff s t)) print_sample (Sample.get (Types.diff s t))
| Typer.NonExhaustive t -> | Typer.NonExhaustive t ->
Format.fprintf ppf "This pattern matching is not exhaustive@."; Format.fprintf ppf "This pattern matching is not exhaustive@.";
...@@ -132,7 +133,7 @@ let rec print_exn ppf = function ...@@ -132,7 +133,7 @@ let rec print_exn ppf = function
Format.fprintf ppf "Unbound identifier %a%s@." Ident.print x Format.fprintf ppf "Unbound identifier %a%s@." Ident.print x
(if tn then " (it is a type name)" else "") (if tn then " (it is a type name)" else "")
| Typer.UnboundExtId (cu,x) -> | Typer.UnboundExtId (cu,x) ->
Format.fprintf ppf "Unbound external identifier %a:%a@." Format.fprintf ppf "Unbound external identifier %a:%a@."
U.print (Librarian.name cu) U.print (Librarian.name cu)
Ident.print x Ident.print x
| Ulexer.Error (i,j,s) -> | Ulexer.Error (i,j,s) ->
...@@ -140,7 +141,7 @@ let rec print_exn ppf = function ...@@ -140,7 +141,7 @@ let rec print_exn ppf = function
Cduce_loc.print_loc ppf loc; Cduce_loc.print_loc ppf loc;
Cduce_loc.html_hilight loc; Cduce_loc.html_hilight loc;
Format.fprintf ppf "%s" s Format.fprintf ppf "%s" s
| Parser.Error s | Stream.Error s -> | Parser.Error s | Stream.Error s ->
Format.fprintf ppf "Parsing error: %a@." print_protect s Format.fprintf ppf "Parsing error: %a@." print_protect s
| Librarian.InconsistentCrc name -> | Librarian.InconsistentCrc name ->
Format.fprintf ppf "Link error:@."; Format.fprintf ppf "Link error:@.";
...@@ -163,14 +164,14 @@ let rec print_exn ppf = function ...@@ -163,14 +164,14 @@ let rec print_exn ppf = function
| Cduce_loc.Generic s -> | Cduce_loc.Generic s ->
Format.fprintf ppf "%a@." print_protect s Format.fprintf ppf "%a@." print_protect s
| Ns.Label.Not_unique ((ns1,s1),(ns2,s2)) -> | Ns.Label.Not_unique ((ns1,s1),(ns2,s2)) ->
Format.fprintf ppf "Collision on label hash: {%a}:%a, {%a}:%a" Format.fprintf ppf "Collision on label hash: {%a}:%a, {%a}:%a"
U.print (Ns.Uri.value ns1) U.print (Ns.Uri.value ns1)
U.print s1 U.print s1
U.print (Ns.Uri.value ns2) U.print (Ns.Uri.value ns2)
U.print s2 U.print s2
| Ns.Uri.Not_unique (ns1,ns2) -> | Ns.Uri.Not_unique (ns1,ns2) ->
Format.fprintf ppf "Collision on namespaces hash: %a, %a" Format.fprintf ppf "Collision on namespaces hash: %a, %a"
U.print ns1 U.print ns1
U.print ns2 U.print ns2
| Sequence.Error (Sequence.CopyTag (t,expect)) -> | Sequence.Error (Sequence.CopyTag (t,expect)) ->
Format.fprintf ppf "Tags in %a will be copied, but only %a are allowed.@.Counter-example:%a@." Format.fprintf ppf "Tags in %a will be copied, but only %a are allowed.@.Counter-example:%a@."
...@@ -185,12 +186,12 @@ let rec print_exn ppf = function ...@@ -185,12 +186,12 @@ let rec print_exn ppf = function
| Sequence.Error (Sequence.UnderTag (t,exn)) -> | Sequence.Error (Sequence.UnderTag (t,exn)) ->
Format.fprintf ppf "Under tag %a:@." Types.Print.pp_type t; Format.fprintf ppf "Under tag %a:@." Types.Print.pp_type t;
print_exn ppf exn print_exn ppf exn
| exn -> | exn ->
(* raise exn *) (* raise exn *)
Format.fprintf ppf "%a@." print_protect (Printexc.to_string exn) Format.fprintf ppf "%a@." print_protect (Printexc.to_string exn)
let eval_quiet tenv cenv e = let eval_quiet tenv cenv e =
let (e,_) = Typer.type_expr tenv e in let (e,_) = Typer.type_expr tenv e in
Compile.compile_eval_expr cenv e Compile.compile_eval_expr cenv e
...@@ -201,6 +202,13 @@ let debug ppf tenv cenv = function ...@@ -201,6 +202,13 @@ let debug ppf tenv cenv = function
and t2 = Types.descr (Typer.typ tenv t2) in and t2 = Types.descr (Typer.typ tenv t2) in
let s = Types.subtype t1 t2 in let s = Types.subtype t1 t2 in
Format.fprintf ppf "%a %a %a : %b@." print_norm t1 print_protect "<=" print_norm t2 s Format.fprintf ppf "%a %a %a : %b@." print_norm t1 print_protect "<=" print_norm t2 s
| `Bdd (t) ->
Format.fprintf ppf "[DEBUG:bdd]@.";
let t = Types.descr (Typer.typ tenv t) in
Format.fprintf ppf "@[%a@]@." Types.Print.dump t
| `Id_bdd (i) ->
Format.fprintf ppf "[DEBUG:id_bdd]@.";
Format.fprintf ppf "@[%a@]@." Types.Print.dump_by_id i
| `Sample t -> | `Sample t ->
Format.fprintf ppf "[DEBUG:sample]@."; Format.fprintf ppf "[DEBUG:sample]@.";
(try (try
...@@ -209,7 +217,7 @@ let debug ppf tenv cenv = function ...@@ -209,7 +217,7 @@ let debug ppf tenv cenv = function
Format.fprintf ppf "witness: %a@." Types.Witness.pp (Types.witness t); Format.fprintf ppf "witness: %a@." Types.Witness.pp (Types.witness t);
with Not_found -> with Not_found ->
Format.fprintf ppf "Empty type : no sample !@.") Format.fprintf ppf "Empty type : no sample !@.")
| `Filter (t,p) -> | `Filter (t,p) ->
let t = Typer.typ tenv t let t = Typer.typ tenv t
and p = Typer.pat tenv p in and p = Typer.pat tenv p in
Format.fprintf ppf "[DEBUG:filter t=%a p=%a]@." Format.fprintf ppf "[DEBUG:filter t=%a p=%a]@."
...@@ -217,7 +225,7 @@ let debug ppf tenv cenv = function ...@@ -217,7 +225,7 @@ let debug ppf tenv cenv = function
Patterns.Print.pp (Patterns.descr p); Patterns.Print.pp (Patterns.descr p);
let f = Patterns.filter (Types.descr t) p in let f = Patterns.filter (Types.descr t) p in
IdMap.iteri (fun x t -> IdMap.iteri (fun x t ->
Format.fprintf ppf " %a:%a@." Format.fprintf ppf " %a:%a@."
Ident.print x Ident.print x
print_norm (Types.descr t)) f print_norm (Types.descr t)) f
| `Accept p -> | `Accept p ->
...@@ -228,7 +236,7 @@ let debug ppf tenv cenv = function ...@@ -228,7 +236,7 @@ let debug ppf tenv cenv = function
| `Compile (t,pl) -> | `Compile (t,pl) ->
Format.fprintf ppf "[DEBUG:compile]@."; Format.fprintf ppf "[DEBUG:compile]@.";
let no = ref (-1) in let no = ref (-1) in
let t = Types.descr (Typer.typ tenv t) let t = Types.descr (Typer.typ tenv t)
and pl = List.map (fun p -> incr no; (Typer.pat tenv p, !no)) pl in and pl = List.map (fun p -> incr no; (Typer.pat tenv p, !no)) pl in
let (state,rhs) = Patterns.Compile.make_branches t pl in let (state,rhs) = Patterns.Compile.make_branches t pl in
...@@ -242,11 +250,11 @@ let debug ppf tenv cenv = function ...@@ -242,11 +250,11 @@ let debug ppf tenv cenv = function
| `Single t -> | `Single t ->
Format.fprintf ppf "[DEBUG:single]@."; Format.fprintf ppf "[DEBUG:single]@.";
let t = Typer.typ tenv t in let t = Typer.typ tenv t in
(try (try
let c = Sample.single (Types.descr t) in let c = Sample.single (Types.descr t) in
Format.fprintf ppf "Constant:%a@." Types.Print.pp_const c Format.fprintf ppf "Constant:%a@." Types.Print.pp_const c
with with
| Exit -> Format.fprintf ppf "Non constant@." | Exit -> Format.fprintf ppf "Non constant@."
| Not_found -> Format.fprintf ppf "Empty@.") | Not_found -> Format.fprintf ppf "Empty@.")
| `Typed e -> | `Typed e ->
Format.fprintf ppf "[DEBUG:typed]@."; Format.fprintf ppf "[DEBUG:typed]@.";
...@@ -299,17 +307,17 @@ let print_value_opt ppf = function ...@@ -299,17 +307,17 @@ let print_value_opt ppf = function
let show ppf id t v = let show ppf id t v =
if !silent then () if !silent then ()
else Format.fprintf ppf "@[%a : @[%a%a@]@]@." else Format.fprintf ppf "@[%a : @[%a%a@]@]@."
print_id_opt id print_id_opt id
print_norm t print_norm t
print_value_opt v print_value_opt v
let ev_top ~run ~show ?directive phs = let ev_top ~run ~show ?directive phs =
let (tenv,cenv,_) = let (tenv,cenv,_) =
Compile.comp_unit ~run ~show ?directive Compile.comp_unit ~run ~show ?directive
!typing_env !compile_env phs in !typing_env !compile_env phs in
typing_env := tenv; typing_env := tenv;
compile_env := cenv compile_env := cenv
let phrases ppf phs = let phrases ppf phs =
ev_top ~run:true ~show:(show ppf) ~directive:(directive ppf) phs ev_top ~run:true ~show:(show ppf) ~directive:(directive ppf) phs
...@@ -317,10 +325,10 @@ let phrases ppf phs = ...@@ -317,10 +325,10 @@ let phrases ppf phs =
let catch_exn ppf_err exn = let catch_exn ppf_err exn =
if not catch_exceptions then raise exn; if not catch_exceptions then raise exn;
match exn with match exn with
| (End_of_file | Failure _ | Not_found | Invalid_argument _ | Sys.Break) | (End_of_file | Failure _ | Not_found | Invalid_argument _ | Sys.Break)
as e -> as e ->
raise e raise e
| exn -> | exn ->
print_exn ppf_err exn; print_exn ppf_err exn;
Format.fprintf ppf_err "@." Format.fprintf ppf_err "@."
...@@ -341,7 +349,7 @@ let compile src out_dir = ...@@ -341,7 +349,7 @@ let compile src out_dir =
if not (Filename.check_suffix src ".cd") if not (Filename.check_suffix src ".cd")
then raise (InvalidInputFilename src); then raise (InvalidInputFilename src);
let cu = Filename.chop_suffix (Filename.basename src) ".cd" in let cu = Filename.chop_suffix (Filename.basename src) ".cd" in
let out_dir = let out_dir =
match out_dir with match out_dir with
| None -> Filename.dirname src | None -> Filename.dirname src
| Some x -> x in | Some x -> x in
...@@ -350,10 +358,10 @@ let compile src out_dir = ...@@ -350,10 +358,10 @@ let compile src out_dir =
Librarian.compile_save !verbose name src out; Librarian.compile_save !verbose name src out;
exit 0 exit 0
with exn -> catch_exn Format.err_formatter exn; exit 1 with exn -> catch_exn Format.err_formatter exn; exit 1
let compile_run src = let compile_run src =
try try
let name = let name =
if src = "" then "<stdin>" if src = "" then "<stdin>"
else else
if not (Filename.check_suffix src ".cd") if not (Filename.check_suffix src ".cd")
...@@ -363,7 +371,7 @@ let compile_run src = ...@@ -363,7 +371,7 @@ let compile_run src =
Librarian.compile_run !verbose name src; Librarian.compile_run !verbose name src;
with exn -> catch_exn Format.err_formatter exn; exit 1 with exn -> catch_exn Format.err_formatter exn; exit 1
let run obj = let run obj =
Cduce_loc.obj_path := (Filename.dirname obj)::!Cduce_loc.obj_path ; Cduce_loc.obj_path := (Filename.dirname obj)::!Cduce_loc.obj_path ;
let obj = Filename.basename obj in let obj = Filename.basename obj in
try try
...@@ -381,7 +389,7 @@ let eval s = ...@@ -381,7 +389,7 @@ let eval s =
let vals = ref [] in let vals = ref [] in
let show id t v = let show id t v =
match id,v with match id,v with
| Some id, Some v -> | Some id, Some v ->
vals := (Some (Atoms.V.mk id),v) :: !vals vals := (Some (Atoms.V.mk id),v) :: !vals
| None, Some v -> | None, Some v ->
vals := (None,v) :: !vals vals := (None,v) :: !vals
...@@ -389,18 +397,18 @@ let eval s = ...@@ -389,18 +397,18 @@ let eval s =
in in
ev_top ~run:true ~show phs; ev_top ~run:true ~show phs;
List.rev !vals List.rev !vals
let eval s = let eval s =
try eval s try eval s
with exn -> with exn ->
let b = Buffer.create 1024 in let b = Buffer.create 1024 in
let ppf = Format.formatter_of_buffer b in let ppf = Format.formatter_of_buffer b in
print_exn ppf exn; print_exn ppf exn;
Format.fprintf ppf "@."; Format.fprintf ppf "@.";
Value.failwith' (Buffer.contents b) Value.failwith' (Buffer.contents b)
let () =
let () =
Operators.register_fun "eval_expr" Builtin_defs.string_latin1 Types.any Operators.register_fun "eval_expr" Builtin_defs.string_latin1 Types.any
(fun v -> (fun v ->
match eval (Value.cduce2ocaml_string v) with match eval (Value.cduce2ocaml_string v) with
......
...@@ -19,7 +19,7 @@ sig ...@@ -19,7 +19,7 @@ sig
val iter: (elem-> unit) -> t -> unit val iter: (elem-> unit) -> t -> unit
val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b) val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b)
-> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) -> -> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
atom:(elem -> 'b) -> t -> 'b atom:(elem -> 'b) -> t -> 'b
...@@ -55,13 +55,13 @@ struct ...@@ -55,13 +55,13 @@ struct
the minimum of the two when egality ... *) the minimum of the two when egality ... *)
let rec compare a b = let rec compare a b =
if (a == b) then 0 if (a == b) then 0
else match (a,b) with 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 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 = 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 p1 p2 in if c <> 0 then c
else let c = compare i1 i2 in if c <> 0 then c else let c = compare i1 i2 in if c <> 0 then c
else compare n1 n2 else compare n1 n2
| True,_ -> -1 | True,_ -> -1
| _, True -> 1 | _, True -> 1
...@@ -74,7 +74,7 @@ struct ...@@ -74,7 +74,7 @@ struct
| False -> 0 | False -> 0
| Split(h, _,_,_,_) -> h | Split(h, _,_,_,_) -> h
let compute_hash x p i n = let compute_hash x p i n =
(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n) (X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
let rec check = function let rec check = function
...@@ -89,7 +89,7 @@ struct ...@@ -89,7 +89,7 @@ struct
let atom x = let atom x =
let h = X.hash x + 17 in (* partial evaluation of compute_hash... *) 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 neg_atom x =
let h = X.hash x + 16637 in (* partial evaluation of compute_hash... *) let h = X.hash x + 16637 in (* partial evaluation of compute_hash... *)
Split (h, x,False,False,True) Split (h, x,False,False,True)
...@@ -99,11 +99,11 @@ struct ...@@ -99,11 +99,11 @@ struct
| _ -> () | _ -> ()
let rec dump ppf = function let rec dump ppf = function
| True -> Format.fprintf ppf "+" | True -> Format.fprintf ppf ""
| False -> Format.fprintf ppf "-" | False -> Format.fprintf ppf ""
| Split (_,x, p,i,n) -> | Split (_,x, p,i,n) ->
Format.fprintf ppf "%i(@[%a,%a,%a@])" Format.fprintf ppf "@[@[%a@][@[<hov>%a,@\n%a,@\n%a@]]@]"
(* X.dump x *) (X.hash x) dump p dump i dump n X.dump x dump p dump i dump n
let rec print f ppf = function let rec print f ppf = function
| True -> Format.fprintf ppf "Any" | True -> Format.fprintf ppf "Any"
...@@ -111,25 +111,25 @@ struct ...@@ -111,25 +111,25 @@ struct
| Split (_, x, p,i, n) -> | Split (_, x, p,i, n) ->
let flag = ref false in let flag = ref false in
let b () = if !flag then Format.fprintf ppf " | " else flag := true in let b () = if !flag then Format.fprintf ppf " | " else flag := true in
(match p with (match p with
| True -> b(); Format.fprintf ppf "%a" f x | True -> b(); Format.fprintf ppf "%a" f x
| False -> () | False -> ()
| _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p ); | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
(match i with (match i with
| True -> assert false; | True -> assert false;
| False -> () | False -> ()
| _ -> b(); print f ppf i); | _ -> b(); print f ppf i);
(match n with (match n with
| True -> b (); Format.fprintf ppf "@[~%a@]" f x | True -> b (); Format.fprintf ppf "@[~%a@]" f x
| False -> () | False -> ()
| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n) | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
let print a f = function let print a f = function
| True -> [ fun ppf -> Format.fprintf ppf "%s" a ] | True -> [ fun ppf -> Format.fprintf ppf "%s" a ]
| False -> [] | False -> []
| c -> [ fun ppf -> print f ppf c ] | c -> [ fun ppf -> print f ppf c ]
let rec get accu pos neg = function let rec get accu pos neg = function
| True -> (pos,neg) :: accu | True -> (pos,neg) :: accu
| False -> accu | False -> accu
...@@ -139,7 +139,7 @@ struct ...@@ -139,7 +139,7 @@ struct
let accu = get accu pos (x::neg) n in let accu = get accu pos (x::neg) n in
let accu = get accu pos neg i in let accu = get accu pos neg i in
accu accu
let get x = get [] [] [] x let get x = get [] [] [] x
let rec get' accu pos neg = function let rec get' accu pos neg = function
...@@ -171,7 +171,7 @@ struct ...@@ -171,7 +171,7 @@ struct
cup (cup p i) n cup (cup p i) n
in in
aux b aux b
(* Invariant: correct hash value *) (* Invariant: correct hash value *)
let split0 x pos ign neg = let split0 x pos ign neg =
...@@ -194,7 +194,7 @@ struct ...@@ -194,7 +194,7 @@ struct
| b :: l -> (equal a b) || (has_same a l) | b :: l -> (equal a b) || (has_same a l)
let rec split x p i n = let rec split x p i n =
if i == True then True if i == True then True
else if equal p n then p ++ i else if equal p n then p ++ i
else let p = simplify p [i] and n = simplify n [i] in else let p = simplify p [i] and n = simplify n [i] in
if equal p n then p ++ i if equal p n then p ++ i
...@@ -208,17 +208,17 @@ struct ...@@ -208,17 +208,17 @@ struct
if (has_true l) || (has_same a l) then False if (has_true l) || (has_same a l) then False
else s_aux2 a x p i n [] [] [] l else s_aux2 a x p i n [] [] [] l
and s_aux2 a x p i n ap ai an = function and s_aux2 a x p i n ap ai an = function
| [] -> | [] ->
let p = simplify p ap let p = simplify p ap
and n = simplify n an and n = simplify n an
and i = simplify i ai in