Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
cduce
cduce
Commits
bd8a1e50
Commit
bd8a1e50
authored
Oct 05, 2007
by
Pietro Abate
Browse files
[r2003-04-02 12:34:22 by cvscast] Empty log message
Original author: cvscast Date: 2003-04-02 12:34:22+00:00
parent
751f9f93
Changes
14
Hide whitespace changes
Inline
Side-by-side
misc/bool.ml
View file @
bd8a1e50
...
...
@@ -36,6 +36,8 @@ sig
val
print
:
string
->
(
Format
.
formatter
->
'
a
elem
->
unit
)
->
'
a
t
->
(
Format
.
formatter
->
unit
)
list
val
trivially_disjoint
:
'
a
t
->
'
a
t
->
bool
end
module
Make
(
X
:
ARG
)
=
...
...
@@ -74,13 +76,6 @@ struct
|
_
,
False
->
1
(*
let rec hash = function
| True -> 1
| False -> 2
| Split (x, p,i,n) ->
(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
*)
let
rec
hash
=
function
|
True
->
1
|
False
->
0
...
...
@@ -180,6 +175,7 @@ struct
- no ``subsumption'
*)
(*
let rec simplify a b =
if equal a b then False
else match (a,b) with
...
...
@@ -204,7 +200,9 @@ struct
if (p1 != p1') || (n1 != n1') || (i1 != i1')
then split x1 p1' i1' n1'
else a
(*
*)
let
rec
simplify
a
l
=
if
(
a
=
False
)
then
False
else
simpl_aux1
a
[]
l
and
simpl_aux1
a
accu
=
function
...
...
@@ -239,10 +237,12 @@ struct
simpl_aux2
x
p
i
n
(
b
::
ap
)
(
b
::
ai
)
(
b
::
an
)
l
else
simpl_aux2
x
p
i
n
(
p2
::
i2
::
ap
)
(
i2
::
ai
)
(
n2
::
i2
::
an
)
l
*)
let
split
x
p
i
n
=
split
x
(
simplify
p
i
)
i
(
simplify
n
i
)
split
x
(
simplify
p
[
i
])
i
(
simplify
n
[
i
])
let
rec
(
++
)
a
b
=
(* if equal a b then a *)
...
...
@@ -270,8 +270,8 @@ struct
is the invariant still inforced ? *)
let
rec
(
**
)
a
b
=
(* if equal a b then a *)
if
a
==
b
then
a
(* if equal a b then a *)
if
a
==
b
then
a
else
match
(
a
,
b
)
with
|
True
,
a
|
a
,
True
->
a
|
False
,
_
|
_
,
False
->
False
...
...
@@ -281,17 +281,36 @@ struct
(* split x1
(p1 ** (p2 ++ i2) ++ (p2 ** i1))
(i1 ** i2)
(n1 ** (n2 ++ i2) ++ (n2 ** i1))
*)
(n1 ** (n2 ++ i2) ++ (n2 ** i1)) *)
split
x1
((
p1
++
i1
)
**
(
p2
++
i2
))
False
((
n1
++
i1
)
**
(
n2
++
i2
))
((
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
)
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
...
...
@@ -301,8 +320,8 @@ struct
|
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
(* if equal a b then False
*)
if
a
==
b
then
False
else
match
(
a
,
b
)
with
|
False
,_
|
_
,
True
->
False
|
a
,
False
->
a
...
...
@@ -315,7 +334,7 @@ struct
False
((
n1
++
i1
)
//
(
n2
++
i2
))
else
if
c
<
0
then
split
x1
(
p1
//
b
)
(
i1
//
b
)
(
n1
//
b
)
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
))
...
...
@@ -325,9 +344,17 @@ struct
let
cap
=
(
**
)
let
diff
=
(
//
)
(*
let diff x y =
(*
let d = diff x y in
let d = diff x y in
Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"
dump x dump y dump d; *)
diff
x
y
dump x dump y dump d;
d
let cap x y =
let d = cap x y in
Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX**Z = %a@\n"
dump x dump y dump d;
d
*)
end
misc/bool.mli
View file @
bd8a1e50
...
...
@@ -13,6 +13,7 @@ sig
type
'
a
elem
type
'
a
t
val
dump
:
Format
.
formatter
->
'
a
t
->
unit
val
equal
:
'
a
t
->
'
a
t
->
bool
...
...
@@ -36,6 +37,8 @@ sig
val
print
:
string
->
(
Format
.
formatter
->
'
a
elem
->
unit
)
->
'
a
t
->
(
Format
.
formatter
->
unit
)
list
val
trivially_disjoint
:
'
a
t
->
'
a
t
->
bool
end
module
Make
(
X
:
ARG
)
:
S
with
type
'
a
elem
=
'
a
X
.
t
tests/html2latex.cd
View file @
bd8a1e50
...
...
@@ -132,6 +132,7 @@ let fun do_table (Xtable -> String) _ -> raise "<table> nothandled";;
do_tbodies
*)
match load_xml "tst_html2latex.xml" with
| x
&
Xhtml -> print (do_html x)
| _ -> raise "Input file is not XHTML !";;
...
...
types/atoms.ml
View file @
bd8a1e50
...
...
@@ -38,6 +38,14 @@ let contains x = function
|
Finite
s
->
SList
.
mem
s
x
|
Cofinite
s
->
not
(
SList
.
mem
s
x
)
let
disjoint
s
t
=
match
(
s
,
t
)
with
|
(
Finite
s
,
Finite
t
)
->
SList
.
disjoint
s
t
|
(
Finite
s
,
Cofinite
t
)
->
SList
.
subset
s
t
|
(
Cofinite
s
,
Finite
t
)
->
SList
.
subset
t
s
|
(
Cofinite
s
,
Cofinite
t
)
->
false
let
is_empty
=
function
|
Finite
[]
->
true
|
_
->
false
...
...
types/atoms.mli
View file @
bd8a1e50
...
...
@@ -21,6 +21,7 @@ val diff : t -> t -> t
val
atom
:
v
->
t
val
contains
:
v
->
t
->
bool
val
disjoint
:
t
->
t
->
bool
val
is_empty
:
t
->
bool
val
is_atom
:
t
->
v
option
val
sample
:
t
->
v
...
...
types/boolean.ml
View file @
bd8a1e50
...
...
@@ -30,7 +30,8 @@ sig
val
print
:
string
->
(
Format
.
formatter
->
'
a
elem
->
unit
)
->
'
a
t
->
(
Format
.
formatter
->
unit
)
list
val
trivially_disjoint
:
'
a
t
->
'
a
t
->
bool
val
check
:
'
a
t
->
unit
end
...
...
@@ -195,6 +196,8 @@ let print any f =
)
)
let
trivially_disjoint
a
b
=
cap
a
b
=
[]
let
check
b
=
()
(*
SSList.check b;
...
...
types/boolean.mli
View file @
bd8a1e50
...
...
@@ -39,6 +39,7 @@ sig
(
Format
.
formatter
->
unit
)
list
val
trivially_disjoint
:
'
a
t
->
'
a
t
->
bool
val
check
:
'
a
t
->
unit
end
...
...
types/chars.ml
View file @
bd8a1e50
...
...
@@ -83,6 +83,15 @@ let diff i1 i2 = neg (cup (neg i1) i2)
let
is_empty
i
=
i
=
[]
let
rec
disjoint
(
a
:
t
)
b
=
match
(
a
,
b
)
with
|
[]
,_
|
_
,
[]
->
true
|
(
xa
,
ya
)
::
a'
,
(
xb
,
yb
)
::
b'
->
if
xa
=
xb
then
false
else
if
xa
<
xb
then
(
ya
<
xb
)
&&
(
disjoint
a'
b
)
else
(
yb
<
xa
)
&&
(
disjoint
a
b'
)
let
contains
n
=
List
.
exists
(
fun
(
a
,
b
)
->
(
n
>=
a
)
&&
(
n
<=
b
))
let
sample
=
function
...
...
types/chars.mli
View file @
bd8a1e50
...
...
@@ -21,7 +21,7 @@ val diff : t -> t -> t
val
char_class
:
v
->
v
->
t
val
atom
:
v
->
t
val
disjoint
:
t
->
t
->
bool
val
is_empty
:
t
->
bool
val
contains
:
v
->
t
->
bool
val
sample
:
t
->
v
...
...
types/intervals.ml
View file @
bd8a1e50
open
Big_int
(* Hack to compute hash value for bigints *)
let
hash_nat
x
=
Nat
.
nth_digit_nat
x
0
let
hash_bigint
(
sign
,
nat
)
=
sign
*
17
+
hash_nat
nat
type
v
=
big_int
let
print_v
ppf
i
=
Format
.
fprintf
ppf
"%s"
(
string_of_big_int
i
)
let
vcompare
=
compare_big_int
let
vhash
=
num_digits_big_int
(* improve this *)
let
vhash
x
=
hash_bigint
(
Obj
.
magic
x
)
(* num_digits_big_int x *)
(* improve this *)
let
mk
=
big_int_of_string
let
vadd
=
add_big_int
let
vmult
=
mult_big_int
...
...
@@ -128,6 +133,25 @@ let diff i1 i2 =
let
is_empty
=
function
[]
->
true
|
_
->
false
let
rec
disjoint
a
b
=
match
(
a
,
b
)
with
|
[]
,_
|
_
,
[]
->
true
|
Any
::_,_
|
_
,
Any
::_
->
false
|
Left
_
::_,
Left
_
::_
->
false
|
Right
_
::_,
Right
_
::_
->
false
|
Left
x
::
a
,
Bounded
(
y
,_
)
::
_
->
(
lt_big_int
x
y
)
&&
(
disjoint
a
b
)
|
Bounded
(
y
,_
)
::
_
,
Left
x
::
b
->
(
lt_big_int
x
y
)
&&
(
disjoint
a
b
)
|
Left
x
::
_
,
Right
y
::
_
->
lt_big_int
x
y
|
Right
y
::
_
,
Left
x
::
_
->
lt_big_int
x
y
|
Right
y
::
_
,
Bounded
(
_
,
x
)
::
_
->
lt_big_int
x
y
|
Bounded
(
_
,
x
)
::
_
,
Right
y
::
_
->
lt_big_int
x
y
|
Bounded
(
xa
,
ya
)
::
a'
,
Bounded
(
xb
,
yb
)
::
b'
->
let
c
=
compare_big_int
xa
xb
in
if
c
=
0
then
false
else
if
c
<
0
then
(
lt_big_int
ya
xb
)
&&
(
disjoint
a'
b
)
else
(
lt_big_int
yb
xa
)
&&
(
disjoint
a
b'
)
(* TODO: can optimize this to stop running through the list earlier *)
let
contains
n
=
...
...
@@ -211,10 +235,11 @@ let dump s i =
let diff i1 i2 =
let ppf = Format.std_formatter in
Format.fprintf ppf "Intervals.diff
.
";
Format.fprintf ppf "Intervals.diff
:
";
dump "i1" i1;
dump "i2" i2;
dump "
~
i1
|
i2" (
cup (neg
i1
)
i2);
dump "i1
-
i2" (
diff
i1 i2);
Format.fprintf ppf "@\n";
diff i1 i2
*)
types/intervals.mli
View file @
bd8a1e50
...
...
@@ -28,6 +28,7 @@ val left : v -> t
val
right
:
v
->
t
val
atom
:
v
->
t
val
disjoint
:
t
->
t
->
bool
val
is_empty
:
t
->
bool
val
contains
:
v
->
t
->
bool
val
sample
:
t
->
v
...
...
types/normal.ml
View file @
bd8a1e50
...
...
@@ -12,6 +12,7 @@ end
type
'
a
bool
=
(
'
a
list
*
'
a
list
)
list
(*
module Make(X1 : S)(X2 : S) =
struct
type t = (X1.t * X2.t) list
...
...
@@ -59,17 +60,18 @@ struct
let line res (p,n) =
let (d1,d2) = bigcap p in
if not ((X1.is_empty d1) || (X2.is_empty d2)) then
(
let
resid
=
ref
d1
in
(let resid = ref
X1.empty
in
List.iter
(fun (t1,t2) ->
let t1 = X1.cap d1 t1 in
if not (X1.is_empty t1) then
(
resid
:=
X1
.
diff
!
resid
t1
;
(resid := X1.
cup
!resid t1;
let t2 = X2.diff d2 t2 in
if not (X2.is_empty t2) then add res t1 t2 !res
)
) (normal n);
if
not
(
X1
.
is_empty
!
resid
)
then
add
res
!
resid
d2
!
res
)
let d1 = X1.diff d1 !resid in
if not (X1.is_empty d1) then add res d1 d2 !res)
let boolean_normal x =
let res = ref (Obj.magic 0) in
...
...
@@ -94,3 +96,71 @@ struct
if X1.is_empty (X1.cap t1 restr) then accu
else X2.cup accu t2) X2.empty
end
*)
module
Make
(
X1
:
S
)(
X2
:
S
)
=
struct
type
t
=
(
X1
.
t
*
X2
.
t
)
list
(* Possible optimizations:
- check whether t1 or t2 is empty initially
- check s1 = t1 (structural equility)
*)
let
rec
add
root
t1
t2
=
function
|
[]
->
(
t1
,
t2
)
::
root
|
(
s1
,
s2
)
::
rem
->
let
i
=
X1
.
cap
t1
s1
in
if
X1
.
is_empty
i
then
add
((
s1
,
s2
)
::
root
)
t1
t2
rem
else
(
let
root
=
(
i
,
X2
.
cup
t2
s2
)
::
root
in
let
k
=
X1
.
diff
s1
t1
in
let
root
=
if
not
(
X1
.
is_empty
k
)
then
(
k
,
s2
)
::
root
else
root
in
let
j
=
X1
.
diff
t1
s1
in
if
not
(
X1
.
is_empty
j
)
then
add
root
j
t2
rem
else
root
)
let
normal
x
=
List
.
fold_left
(
fun
accu
(
t1
,
t2
)
->
add
[]
t1
t2
accu
)
[]
x
let
rec
bigcap_aux
t1
t2
=
function
|
(
s1
,
s2
)
::
rem
->
bigcap_aux
(
X1
.
cap
t1
s1
)
(
X2
.
cap
t2
s2
)
rem
|
[]
->
(
t1
,
t2
)
let
bigcap
=
bigcap_aux
X1
.
any
X2
.
any
(* optimize: one knows that the t1 are pairwise disjoint ... *)
let
line
accu
(
p
,
n
)
=
let
(
d1
,
d2
)
=
bigcap
p
in
if
not
((
X1
.
is_empty
d1
)
||
(
X2
.
is_empty
d2
))
then
(
let
resid
=
ref
X1
.
empty
in
let
accu
=
List
.
fold_left
(
fun
accu
(
t1
,
t2
)
->
let
i
=
X1
.
cap
d1
t1
in
if
not
(
X1
.
is_empty
i
)
then
(
resid
:=
X1
.
cup
!
resid
t1
;
let
t2
=
X2
.
diff
d2
t2
in
if
not
(
X2
.
is_empty
t2
)
then
add
[]
i
t2
accu
else
accu
)
else
accu
)
accu
(
normal
n
)
in
let
d1
=
X1
.
diff
d1
!
resid
in
if
not
(
X1
.
is_empty
d1
)
then
add
[]
d1
d2
accu
else
accu
)
else
accu
let
boolean_normal
x
=
List
.
fold_left
line
[]
x
let
boolean
x
=
List
.
fold_left
(
fun
accu
x
->
(
line
[]
x
)
@
accu
)
[]
x
let
pi1
=
List
.
fold_left
(
fun
accu
(
t1
,
t2
)
->
X1
.
cup
accu
t1
)
X1
.
empty
let
pi2
=
List
.
fold_left
(
fun
accu
(
t1
,
t2
)
->
X2
.
cup
accu
t2
)
X2
.
empty
let
pi2_restricted
restr
=
List
.
fold_left
(
fun
accu
(
t1
,
t2
)
->
if
X1
.
is_empty
(
X1
.
cap
t1
restr
)
then
accu
else
X2
.
cup
accu
t2
)
X2
.
empty
end
types/patterns.ml
View file @
bd8a1e50
...
...
@@ -206,6 +206,7 @@ module Normal : sig
nrecord
:
record
;
}
val
dummy
:
t
val
compare_nf
:
t
->
t
->
int
val
any_basic
:
Types
.
descr
...
...
@@ -360,6 +361,7 @@ struct
|
Some
l
->
RecLabel
(
l
,
NLineProd
.
empty
)
|
None
->
RecNolabel
(
None
,
None
))
}
let
dummy
=
nempty
None
let
ncup
nf1
nf2
=
...
...
@@ -745,6 +747,12 @@ struct
let
cur_id
=
State
.
ref
"Patterns.cur_id"
0
(* TODO: save dispatchers ? *)
module
NfMap
=
Map
.
Make
(
struct
type
t
=
Normal
.
t
let
compare
=
Normal
.
compare_nf
end
)
module
DispMap
=
Map
.
Make
(
struct
type
t
=
Types
.
descr
*
Normal
.
t
array
...
...
@@ -881,15 +889,31 @@ struct
)
LabelPool
.
dummy_max
!
accu
in
let
lab
=
if
lab
=
LabelPool
.
dummy_max
then
None
else
Some
lab
in
let
accu
=
List
.
map
(
fun
(
ty
,
pl
,
i
,
info
)
->
let
p
=
Normal
.
normal
lab
ty
pl
in
(
p
,
[
i
,
p
.
Normal
.
ncatchv
,
info
]))
!
accu
in
(* eliminate this generic comparison *)
let
sorted
=
Array
.
of_list
(
SortedMap
.
from_list
SortedList
.
cup
accu
)
in
let
infos
=
Array
.
map
snd
sorted
in
let
disp
=
dispatcher
t
(
Array
.
map
fst
sorted
)
lab
in
let
pats
=
ref
NfMap
.
empty
in
let
nb_p
=
ref
0
in
List
.
iter
(
fun
(
ty
,
pl
,
i
,
info
)
->
let
p
=
Normal
.
normal
lab
ty
pl
in
let
x
=
(
i
,
p
.
Normal
.
ncatchv
,
info
)
in
try
let
s
=
NfMap
.
find
p
!
pats
in
s
:=
x
::
!
s
with
Not_found
->
pats
:=
NfMap
.
add
p
(
ref
[
x
])
!
pats
;
incr
nb_p
)
!
accu
;
let
infos
=
Array
.
make
!
nb_p
[]
in
let
ps
=
Array
.
make
!
nb_p
Normal
.
dummy
in
let
count
=
ref
0
in
NfMap
.
iter
(
fun
p
l
->
let
i
=
!
count
in
infos
.
(
i
)
<-
!
l
;
ps
.
(
i
)
<-
p
;
count
:=
succ
i
)
!
pats
;
assert
(
!
nb_p
=
!
count
);
let
disp
=
dispatcher
t
ps
lab
in
let
result
(
t
,_,
m
)
=
let
selected
=
Array
.
create
(
Array
.
length
pl
)
[]
in
let
add
r
(
i
,
ncv
,
inf
)
=
selected
.
(
i
)
<-
(
r
,
ncv
,
inf
)
::
selected
.
(
i
)
in
...
...
@@ -1170,7 +1194,7 @@ struct
let
lab
=
if
lab
=
LabelPool
.
dummy_max
then
None
else
Some
lab
in
let
pl
=
Array
.
of_list
(
List
.
map
(
fun
p
->
Normal
.
normal
lab
Types
.
Record
.
any_or_absent
[
p
])
pl
)
in
(
List
.
map
(
fun
p
->
Normal
.
normal
lab
(*t*)
Types
.
Record
.
any_or_absent
[
p
])
pl
)
in
show
ppf
t
pl
lab
;
Format
.
fprintf
ppf
"# compiled dispatchers: %i@
\n
"
!
cur_id
...
...
types/types.ml
View file @
bd8a1e50
...
...
@@ -225,6 +225,16 @@ let hash_descr a =
let
accu
=
if
a
.
absent
then
accu
+
5
else
accu
in
accu
(* TODO: optimize disjoint check for boolean combinations *)
let
trivially_disjoint
a
b
=
(
Chars
.
disjoint
a
.
chars
b
.
chars
)
&&
(
Intervals
.
disjoint
a
.
ints
b
.
ints
)
&&
(
Atoms
.
disjoint
a
.
atoms
b
.
atoms
)
&&
(
BoolPair
.
trivially_disjoint
a
.
times
b
.
times
)
&&
(
BoolPair
.
trivially_disjoint
a
.
xml
b
.
xml
)
&&
(
BoolPair
.
trivially_disjoint
a
.
arrow
b
.
arrow
)
&&
(
BoolRec
.
trivially_disjoint
a
.
record
b
.
record
)
module
Descr
=
struct
...
...
@@ -372,6 +382,7 @@ let set s =
s
.
notify
<-
Nothing
;
raise
NotEmpty
let
count_slot
=
ref
0
let
rec
big_conj
f
l
n
=
match
l
with
|
[]
->
set
n
...
...
@@ -396,12 +407,17 @@ and slot d =
(
not
d
.
absent
))
then
slot_not_empty
else
try
DescrHash
.
find
memo
d
with
Not_found
->
(* incr count_slot;
Printf.eprintf "%i;" !count_slot; *)
(* Format.fprintf Format.std_formatter "Empty:%a@\n" !print_descr d; *)
let
s
=
{
status
=
Maybe
;
active
=
false
;
notify
=
Nothing
}
in
DescrHash
.
add
memo
d
s
;
(
try
iter_s
s
check_times
(
BoolPair
.
get
d
.
times
);
iter_s
s
check_times
(
BoolPair
.
get
d
.
xml
);
(* Format.fprintf Format.std_formatter "check_times_bool:@[%a@]@\n"
BoolPair.dump d.times; *)
(* check_times_bool any any d.times s; *)
iter_s
s
check_times
(
BoolPair
.
get
d
.
times
);
iter_s
s
check_times
(
BoolPair
.
get
d
.
xml
);
iter_s
s
check_arrow
(
BoolPair
.
get
d
.
arrow
);
iter_s
s
check_record
(
get_record
d
.
record
);
if
s
.
active
then
marks
:=
s
::
!
marks
else
s
.
status
<-
Empty
;
...
...
@@ -414,27 +430,61 @@ and check_times (left,right) s =
flush stderr; *)
let
rec
aux
accu1
accu2
right
s
=
match
right
with
|
(
t1
,
t2
)
::
right
->
if
trivially_empty
(
cap_t
accu1
t1
)
||
trivially_empty
(
cap_t
accu2
t2
)
then
(
let
t1
=
descr
t1
and
t2
=
descr
t2
in
if
trivially_disjoint
accu1
t1
||
trivially_disjoint
accu2
t2
then
(
aux
accu1
accu2
right
s
)
else
(
let
accu1'
=
diff_t
accu1
t1
in
guard
accu1'
(
aux
accu1'
accu2
right
)
s
;
let
accu2'
=
diff_t
accu2
t2
in
guard
accu2'
(
aux
accu1
accu2'
right
)
s
let
accu1'
=
diff
accu1
t1
in
guard
accu1'
(
aux
accu1'
accu2
right
)
s
;
let
accu2'
=
diff
accu2
t2
in
guard
accu2'
(
aux
accu1
accu2'
right
)
s
(* let accu1 = cap accu1 t1 in (* TODO: approximation of cap ... *)
let accu2' = diff accu2 t2 in
guard accu1 (guard accu2' (aux accu1 accu2' right)) s *)
)
|
[]
->
set
s
in
(*
if List.length right > 6 then (
Printf.eprintf "HEURISTIC\n"; flush stderr;
let
(
accu1
,
accu2
)
=
cap_product
left
in
(*
if List.length right > 6 then (
Printf.eprintf "HEURISTIC\n"; flush stderr;
let (n1,n2) = cup_product right in
let n1 = diff accu1 n1 and n2 = diff accu2 n2 in
guard n1 set s;
guard n2 set s;
Printf.eprintf "HEURISTIC failed\n"; flush stderr;
); *)
let
(
accu1
,
accu2
)
=
cap_product
left
in
Printf.eprintf "HEURISTIC failed\n"; flush stderr;
); *)
guard
accu1
(
guard
accu2
(
aux
accu1
accu2
right
))
s
(*
and check_times_bool accu1 accu2 b s =
match b with
| BoolPair.True -> guard accu1 (guard accu2 set) s
| BoolPair.False -> ()
| BoolPair.Split (_, (t1,t2), p,i,n) ->
check_times_bool accu1 accu2 i s;
let t1 = descr t1 and t2 = descr t2 in
if (trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2)
then check_times_bool accu1 accu2 n s else
(
if p <> BoolPair.False then
(let accu1 = cap accu1 t1
and accu2 = cap accu2 t2 in
if not (trivially_empty accu1 || trivially_empty accu2) then
check_times_bool accu1 accu2 p s);
if n <> BoolPair.False then
(let accu1' = diff accu1 t1 in
check_times_bool accu1' accu2 n s;
let accu2' = diff accu2 t2 in
check_times_bool accu1 accu2' n s)
)
*)
and
check_arrow
(
left
,
right
)
s
=
let
single_right
(
s1
,
s2
)
s
=
let
rec
aux
accu1
accu2
left
s
=
match
left
with
...
...
@@ -453,10 +503,9 @@ and check_record (labels,(oleft,left),rights) s =
|
[]
->
set
s
|
(
oright
,
right
)
::
rights
->
let
next
=
(
oleft
&&
(
not
oright
))
||
(* ggg... why ??? check this line *)
(
oleft
&&
(
not
oright
))
||
exists
(
Array
.
length
left
)
(
fun
i
->
trivially_empty
(
cap
left
.
(
i
)
right
.
(
i
)))
<