Commit 1f0b52f8 authored by Pietro Abate's avatar Pietro Abate

[r2003-03-06 13:51:30 by cvscast] Empty log message

Original author: cvscast
Date: 2003-03-06 13:51:30+00:00
parent 0dfcb292
type T = [ `A? `B? `C? `D? `E? `F? `G? `H? `I? `J?
`K? `L? `M? `N? `O? `P? `Q? `R? ];;
`K? `L? `M? `N? `O? `P? `Q? `R? `S? `T? ];;
(*
let fun f (Any -> T) T & x -> x | x -> f x;;
......@@ -7,21 +7,25 @@ let fun f (Any -> T) T & x -> x | x -> f x;;
debug compile Any T;;
*)
(*
debug compile T
P1 where
P1 = (`A & (a := 1), P2) | (a := 2) & P2 and
P2 = (`B & (b := 1), P3) | (b := 2) & P3 and
P3 = (`C & (c := 1), P4) | (c := 2) & P4 and
P4 = (`D & (d := 1), P5) | (d := 2) & P5 and
P5 = `nil;;
*)
P5 = (`E & (e := 1), P6) | (e := 2) & P6 and
P6 = (`F & (f := 1), P7) | (f := 2) & P7 and
P7 = (`G & (g := 1), P8) | (g := 2) & P8 and
P8 = (`H & (h := 1), P9) | (h := 2) & P9 and
P9 = `nil;;
(*
match [ `A `B `C ] with (P1 where
P1 = (`A & (a := 1), P2) | (a := 2) & P2 and
P2 = (`B & (b := 1), P3) | (b := 2) & P3 and
P3 = (`C & (c := 1), P4) | (c := 2) & P4 and
P4 = (`D & (d := 1), P5) | (d := 2) & P5 and
P1 = (`A & (a := '1'), P2) | (a := '2') & P2 and
P2 = (`B & (b := '1'), P3) | (b := '2') & P3 and
P3 = (`C & (c := '1'), P4) | (c := '2') & P4 and
P4 = (`D & (d := '1'), P5) | (d := '2') & P5 and
P5 = `nil) -> (a,b,c,d);;
*)
......@@ -293,6 +293,8 @@ let cache_false = ref Assumptions.empty
exception NotEmpty
let trivially_empty d = d = empty
let rec empty_rec d =
if Assumptions.mem d !cache_false then false
else if Assumptions.mem d !memo then true
......@@ -324,38 +326,19 @@ and empty_rec_times_aux (left,right) =
(* This avoids explosion with huge rhs (+/- degenerated partitioning)
May be slower when List.length right is small; could optimize
this case... *)
if empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2) then
(* if empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2) then*)
(* THIS IS NOT SOUND !!! *)
if trivially_empty (cap_t accu1 t1) ||
trivially_empty (cap_t accu2 t2) then
aux accu1 accu2 right
else
let accu1' = diff_t accu1 t1 in
if not (empty_rec accu1') then aux accu1' accu2 right;
let accu2' = diff_t accu2 t2 in
if not (empty_rec accu2') then aux accu1 accu2' right
if not (empty_rec accu2') then aux accu1 accu2' right
| [] -> raise NotEmpty
in
let (accu1,accu2) = cap_product left in
(*
let right' = List.filter
(fun (t1,t2) ->
not
(empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2)
)
) right in
if List.length right > 15 then (
Format.fprintf Format.std_formatter "[%i=>%i]@."
(List.length right) (List.length right');
Format.fprintf Format.std_formatter "(%a,%a)@."
!print_descr accu1
!print_descr accu2;
List.iter (fun (t1,t2) ->
Format.fprintf Format.std_formatter "\ (%a,%a)@."
!print_descr (descr t1)
!print_descr (descr t2);
) right
);
let right = right' in
*)
(empty_rec accu1) || (empty_rec accu2) ||
(* OPT? It does'nt seem so ... The hope was to return false quickly
for large right hand-side *)
......@@ -536,6 +519,7 @@ This version explodes when dealing with
(t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
don't call normal_aux *)
let get ?(kind=`Normal) d =
match kind with
| `Normal -> get_aux d.times
......
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