| 320 |
|
|
| 321 |
let diff_t d t = diff d (descr t) |
let diff_t d t = diff d (descr t) |
| 322 |
let cap_t d t = cap d (descr t) |
let cap_t d t = cap d (descr t) |
| 323 |
|
let cup_t d t = cup d (descr t) |
| 324 |
let cap_product l = |
let cap_product l = |
| 325 |
List.fold_left |
List.fold_left |
| 326 |
(fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2)) |
(fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2)) |
| 327 |
(any,any) |
(any,any) |
| 328 |
l |
l |
| 329 |
|
let cup_product l = |
| 330 |
|
List.fold_left |
| 331 |
|
(fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2)) |
| 332 |
|
(empty,empty) |
| 333 |
|
l |
| 334 |
|
|
| 335 |
|
|
| 336 |
module Assumptions = Set.Make(struct type t = descr let compare = compare end) |
module Assumptions = Set.Make(struct type t = descr let compare = compare end) |
| 375 |
in |
in |
| 376 |
let (accu1,accu2) = cap_product left in |
let (accu1,accu2) = cap_product left in |
| 377 |
(empty_rec accu1) || (empty_rec accu2) || |
(empty_rec accu1) || (empty_rec accu2) || |
| 378 |
|
(* OPT? It does'nt seem so ... The hope was to return false quickly |
| 379 |
|
for large right hand-side *) |
| 380 |
|
( |
| 381 |
|
((*if (List length right > 2) then |
| 382 |
|
let (cup1,cup2) = cup_product right in |
| 383 |
|
(empty_rec (diff accu1 cup1)) && (empty_rec (diff accu2 cup2)) |
| 384 |
|
else*) true) |
| 385 |
|
&& |
| 386 |
(try aux accu1 accu2 right; true with NotEmpty -> false) |
(try aux accu1 accu2 right; true with NotEmpty -> false) |
| 387 |
|
) |
| 388 |
|
|
| 389 |
and empty_rec_arrow c = |
and empty_rec_arrow c = |
| 390 |
List.for_all empty_rec_arrow_aux c |
List.for_all empty_rec_arrow_aux c |
Parent Directory
| 
Revision Log
| 
Patch