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
fd087b49
Commit
fd087b49
authored
Oct 05, 2007
by
Pietro Abate
Browse files
[r2003-03-06 22:23:45 by cvscast] Empty log message
Original author: cvscast Date: 2003-03-06 22:23:45+00:00
parent
f5cbbde4
Changes
3
Hide whitespace changes
Inline
Side-by-side
types/boolean.ml
View file @
fd087b49
...
...
@@ -98,17 +98,6 @@ let compute ~empty ~full ~cup ~cap ~diff ~atom t =
let
compute_bool
f
=
compute
~
empty
~
full
~
cup
~
cap
~
diff
~
atom
:
f
let
equal_list
e
l1
l2
=
if
List
.
length
l1
<>
List
.
length
l2
then
raise
Recursive
.
NotEqual
;
List
.
iter2
e
l1
l2
let
equal_line
e
(
p1
,
n1
)
(
p2
,
n2
)
=
equal_list
e
p1
p2
;
equal_list
e
n1
n2
let
equal
e
a
b
=
equal_list
(
equal_line
e
)
a
b
let
print
any
f
=
List
.
map
...
...
types/boolean.mli
View file @
fd087b49
...
...
@@ -28,8 +28,6 @@ val compute: empty:'d -> full:'c -> cup:('d -> 'c -> 'd)
atom
:
(
'
a
->
'
b
)
->
'
a
t
->
'
d
val
compute_bool
:
(
'
a
->
'
b
t
)
->
'
a
t
->
'
b
t
val
equal
:
(
'
a
->
'
b
->
unit
)
->
'
a
t
->
'
b
t
->
unit
val
print
:
string
->
(
Format
.
formatter
->
'
a
->
unit
)
->
'
a
t
->
(
Format
.
formatter
->
unit
)
list
...
...
types/types.ml
View file @
fd087b49
...
...
@@ -22,183 +22,183 @@ type const = Integer of Big_int.big_int | Atom of atom | Char of Chars.Unichar.t
type
pair_kind
=
[
`Normal
|
`XML
]
type
descr
=
{
atoms
:
atom
Atoms
.
t
;
ints
:
Intervals
.
t
;
chars
:
Chars
.
t
;
times
:
(
node
*
node
)
Boolean
.
t
;
xml
:
(
node
*
node
)
Boolean
.
t
;
arrow
:
(
node
*
node
)
Boolean
.
t
;
record
:
(
bool
*
(
label
,
(
bool
*
node
))
SortedMap
.
t
)
Boolean
.
t
;
}
and
node
=
{
id
:
int
;
mutable
descr
:
descr
;
}
let
empty
=
{
times
=
Boolean
.
empty
;
xml
=
Boolean
.
empty
;
arrow
=
Boolean
.
empty
;
record
=
Boolean
.
empty
;
ints
=
Intervals
.
empty
;
atoms
=
Atoms
.
empty
;
chars
=
Chars
.
empty
;
}
let
any
=
{
times
=
Boolean
.
full
;
xml
=
Boolean
.
full
;
arrow
=
Boolean
.
full
;
record
=
Boolean
.
full
;
ints
=
Intervals
.
any
;
atoms
=
Atoms
.
any
;
chars
=
Chars
.
any
;
}
type
descr
=
{
atoms
:
atom
Atoms
.
t
;
ints
:
Intervals
.
t
;
chars
:
Chars
.
t
;
times
:
(
node
*
node
)
Boolean
.
t
;
xml
:
(
node
*
node
)
Boolean
.
t
;
arrow
:
(
node
*
node
)
Boolean
.
t
;
record
:
(
bool
*
(
label
,
(
bool
*
node
))
SortedMap
.
t
)
Boolean
.
t
;
}
and
node
=
{
id
:
int
;
mutable
descr
:
descr
;
}
let
interval
i
=
{
empty
with
ints
=
i
}
let
times
x
y
=
{
empty
with
times
=
Boolean
.
atom
(
x
,
y
)
}
let
xml
x
y
=
{
empty
with
xml
=
Boolean
.
atom
(
x
,
y
)
}
let
arrow
x
y
=
{
empty
with
arrow
=
Boolean
.
atom
(
x
,
y
)
}
let
record
label
opt
t
=
{
empty
with
record
=
Boolean
.
atom
(
true
,
[
label
,
(
opt
,
t
)])
}
let
record'
x
=
{
empty
with
record
=
Boolean
.
atom
x
}
let
atom
a
=
{
empty
with
atoms
=
a
}
let
char
c
=
{
empty
with
chars
=
c
}
let
constant
=
function
|
Integer
i
->
interval
(
Intervals
.
atom
i
)
|
Atom
a
->
atom
(
Atoms
.
atom
a
)
|
Char
c
->
char
(
Chars
.
atom
c
)
let
cup
x
y
=
if
x
==
y
then
x
else
{
times
=
Boolean
.
cup
x
.
times
y
.
times
;
xml
=
Boolean
.
cup
x
.
xml
y
.
xml
;
arrow
=
Boolean
.
cup
x
.
arrow
y
.
arrow
;
record
=
Boolean
.
cup
x
.
record
y
.
record
;
ints
=
Intervals
.
cup
x
.
ints
y
.
ints
;
atoms
=
Atoms
.
cup
x
.
atoms
y
.
atoms
;
chars
=
Chars
.
cup
x
.
chars
y
.
chars
;
}
let
cap
x
y
=
if
x
==
y
then
x
else
{
times
=
Boolean
.
cap
x
.
times
y
.
times
;
xml
=
Boolean
.
cap
x
.
xml
y
.
xml
;
record
=
Boolean
.
cap
x
.
record
y
.
record
;
arrow
=
Boolean
.
cap
x
.
arrow
y
.
arrow
;
ints
=
Intervals
.
cap
x
.
ints
y
.
ints
;
atoms
=
Atoms
.
cap
x
.
atoms
y
.
atoms
;
chars
=
Chars
.
cap
x
.
chars
y
.
chars
;
}
let
empty
=
{
times
=
Boolean
.
empty
;
xml
=
Boolean
.
empty
;
arrow
=
Boolean
.
empty
;
record
=
Boolean
.
empty
;
ints
=
Intervals
.
empty
;
atoms
=
Atoms
.
empty
;
chars
=
Chars
.
empty
;
}
let
any
=
{
times
=
Boolean
.
full
;
xml
=
Boolean
.
full
;
arrow
=
Boolean
.
full
;
record
=
Boolean
.
full
;
ints
=
Intervals
.
any
;
atoms
=
Atoms
.
any
;
chars
=
Chars
.
any
;
}
let
interval
i
=
{
empty
with
ints
=
i
}
let
times
x
y
=
{
empty
with
times
=
Boolean
.
atom
(
x
,
y
)
}
let
xml
x
y
=
{
empty
with
xml
=
Boolean
.
atom
(
x
,
y
)
}
let
arrow
x
y
=
{
empty
with
arrow
=
Boolean
.
atom
(
x
,
y
)
}
let
record
label
opt
t
=
{
empty
with
record
=
Boolean
.
atom
(
true
,
[
label
,
(
opt
,
t
)])
}
let
record'
x
=
{
empty
with
record
=
Boolean
.
atom
x
}
let
atom
a
=
{
empty
with
atoms
=
a
}
let
char
c
=
{
empty
with
chars
=
c
}
let
constant
=
function
|
Integer
i
->
interval
(
Intervals
.
atom
i
)
|
Atom
a
->
atom
(
Atoms
.
atom
a
)
|
Char
c
->
char
(
Chars
.
atom
c
)
let
diff
x
y
=
if
x
==
y
then
empty
else
{
times
=
Boolean
.
diff
x
.
times
y
.
times
;
xml
=
Boolean
.
diff
x
.
xml
y
.
xml
;
arrow
=
Boolean
.
diff
x
.
arrow
y
.
arrow
;
record
=
Boolean
.
diff
x
.
record
y
.
record
;
ints
=
Intervals
.
diff
x
.
ints
y
.
ints
;
atoms
=
Atoms
.
diff
x
.
atoms
y
.
atoms
;
chars
=
Chars
.
diff
x
.
chars
y
.
chars
;
}
let
count
=
ref
0
let
make
()
=
incr
count
;
{
id
=
!
count
;
descr
=
empty
}
let
define
n
d
=
n
.
descr
<-
d
let
cons
d
=
incr
count
;
{
id
=
!
count
;
descr
=
d
}
let
descr
n
=
n
.
descr
let
internalize
n
=
n
let
id
n
=
n
.
id
let
rec
equal_rec
r1
r2
=
(
r1
==
r2
)
||
match
(
r1
,
r2
)
with
let
cup
x
y
=
if
x
==
y
then
x
else
{
times
=
Boolean
.
cup
x
.
times
y
.
times
;
xml
=
Boolean
.
cup
x
.
xml
y
.
xml
;
arrow
=
Boolean
.
cup
x
.
arrow
y
.
arrow
;
record
=
Boolean
.
cup
x
.
record
y
.
record
;
ints
=
Intervals
.
cup
x
.
ints
y
.
ints
;
atoms
=
Atoms
.
cup
x
.
atoms
y
.
atoms
;
chars
=
Chars
.
cup
x
.
chars
y
.
chars
;
}
let
cap
x
y
=
if
x
==
y
then
x
else
{
times
=
Boolean
.
cap
x
.
times
y
.
times
;
xml
=
Boolean
.
cap
x
.
xml
y
.
xml
;
record
=
Boolean
.
cap
x
.
record
y
.
record
;
arrow
=
Boolean
.
cap
x
.
arrow
y
.
arrow
;
ints
=
Intervals
.
cap
x
.
ints
y
.
ints
;
atoms
=
Atoms
.
cap
x
.
atoms
y
.
atoms
;
chars
=
Chars
.
cap
x
.
chars
y
.
chars
;
}
let
diff
x
y
=
if
x
==
y
then
empty
else
{
times
=
Boolean
.
diff
x
.
times
y
.
times
;
xml
=
Boolean
.
diff
x
.
xml
y
.
xml
;
arrow
=
Boolean
.
diff
x
.
arrow
y
.
arrow
;
record
=
Boolean
.
diff
x
.
record
y
.
record
;
ints
=
Intervals
.
diff
x
.
ints
y
.
ints
;
atoms
=
Atoms
.
diff
x
.
atoms
y
.
atoms
;
chars
=
Chars
.
diff
x
.
chars
y
.
chars
;
}
let
count
=
ref
0
let
make
()
=
incr
count
;
{
id
=
!
count
;
descr
=
empty
}
let
define
n
d
=
n
.
descr
<-
d
let
cons
d
=
incr
count
;
{
id
=
!
count
;
descr
=
d
}
let
descr
n
=
n
.
descr
let
internalize
n
=
n
let
id
n
=
n
.
id
let
rec
equal_rec
r1
r2
=
(
r1
==
r2
)
||
match
(
r1
,
r2
)
with
|
(
l1
,
(
o1
,
x1
))
::
r1
,
(
l2
,
(
o2
,
x2
))
::
r2
->
(
l1
=
l2
)
&&
(
o1
=
o2
)
&&
(
x1
.
id
=
x2
.
id
)
&&
(
equal_rec
r1
r2
)
|
_
->
false
let
rec
equal_rec_list
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
o1
,
r1
)
::
l1
,
(
o2
,
r2
)
::
l2
->
(
o1
=
o2
)
&&
(
equal_rec
r1
r2
)
|
_
->
false
let
rec
equal_rec_bool
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
p1
,
n1
)
::
l1
,
(
p2
,
n2
)
::
l2
->
(
equal_rec_list
p1
p2
)
&&
(
equal_rec_list
n1
n2
)
&&
(
equal_rec_bool
l1
l2
)
|
_
->
false
let
rec
equal_times_list
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
x1
,
y1
)
::
l1
,
(
x2
,
y2
)
::
l2
->
(
x1
.
id
=
x2
.
id
)
&&
(
y1
.
id
=
y2
.
id
)
&&
(
equal_times_list
l1
l2
)
|
_
->
false
let
rec
equal_times_bool
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
p1
,
n1
)
::
l1
,
(
p2
,
n2
)
::
l2
->
(
equal_times_list
p1
p2
)
&&
(
equal_times_list
n1
n2
)
&&
(
equal_times_bool
l1
l2
)
|
_
->
false
let
equal_descr
a
b
=
(
a
.
atoms
=
b
.
atoms
)
&&
(
a
.
chars
=
b
.
chars
)
&&
(
a
.
ints
=
b
.
ints
)
&&
(
equal_times_bool
a
.
times
b
.
times
)
&&
(
equal_times_bool
a
.
xml
b
.
xml
)
&&
(
equal_times_bool
a
.
arrow
b
.
arrow
)
&&
(
equal_rec_bool
a
.
record
b
.
record
)
let
rec
hash_times_list
accu
=
function
|
(
x
,
y
)
::
l
->
hash_times_list
(
accu
*
257
+
x
.
id
*
17
+
y
.
id
)
l
|
[]
->
accu
+
17
let
rec
hash_times_bool
accu
=
function
|
(
p
,
n
)
::
l
->
hash_times_bool
(
hash_times_list
(
hash_times_list
accu
p
)
n
)
l
|
[]
->
accu
+
3
let
rec
hash_rec
accu
=
function
|
(
l
,
(
o
,
x
))
::
rem
->
hash_rec
(
257
*
accu
+
17
*
(
LabelPool
.
hash
l
)
+
x
.
id
)
rem
|
[]
->
accu
+
5
let
rec
hash_rec_list
accu
=
function
|
(
o
,
r
)
::
l
->
hash_rec_list
(
hash_rec
accu
r
)
l
|
[]
->
accu
+
17
let
rec
hash_rec_bool
accu
=
function
|
(
p
,
n
)
::
l
->
hash_rec_bool
(
hash_rec_list
(
hash_rec_list
accu
p
)
n
)
l
|
[]
->
accu
+
3
let
hash_descr
a
=
let
accu
=
(
Hashtbl
.
hash
a
.
ints
)
+
17
*
(
Hashtbl
.
hash
a
.
atoms
)
+
257
*
(
Hashtbl
.
hash
a
.
chars
)
in
let
accu
=
hash_times_bool
accu
a
.
times
in
let
accu
=
hash_times_bool
accu
a
.
xml
in
let
accu
=
hash_times_bool
accu
a
.
arrow
in
let
accu
=
hash_rec_bool
accu
a
.
record
in
accu
let
rec
equal_rec_list
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
o1
,
r1
)
::
l1
,
(
o2
,
r2
)
::
l2
->
(
o1
=
o2
)
&&
(
equal_rec
r1
r2
)
|
_
->
false
let
rec
equal_rec_bool
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
p1
,
n1
)
::
l1
,
(
p2
,
n2
)
::
l2
->
(
equal_rec_list
p1
p2
)
&&
(
equal_rec_list
n1
n2
)
&&
(
equal_rec_bool
l1
l2
)
|
_
->
false
let
rec
equal_times_list
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
x1
,
y1
)
::
l1
,
(
x2
,
y2
)
::
l2
->
(
x1
.
id
=
x2
.
id
)
&&
(
y1
.
id
=
y2
.
id
)
&&
(
equal_times_list
l1
l2
)
|
_
->
false
let
rec
equal_times_bool
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
p1
,
n1
)
::
l1
,
(
p2
,
n2
)
::
l2
->
(
equal_times_list
p1
p2
)
&&
(
equal_times_list
n1
n2
)
&&
(
equal_times_bool
l1
l2
)
|
_
->
false
let
equal_descr
a
b
=
(
a
.
atoms
=
b
.
atoms
)
&&
(
a
.
chars
=
b
.
chars
)
&&
(
a
.
ints
=
b
.
ints
)
&&
(
equal_times_bool
a
.
times
b
.
times
)
&&
(
equal_times_bool
a
.
xml
b
.
xml
)
&&
(
equal_times_bool
a
.
arrow
b
.
arrow
)
&&
(
equal_rec_bool
a
.
record
b
.
record
)
let
rec
hash_times_list
accu
=
function
|
(
x
,
y
)
::
l
->
hash_times_list
(
accu
*
257
+
x
.
id
*
17
+
y
.
id
)
l
|
[]
->
accu
+
17
let
rec
hash_times_bool
accu
=
function
|
(
p
,
n
)
::
l
->
hash_times_bool
(
hash_times_list
(
hash_times_list
accu
p
)
n
)
l
|
[]
->
accu
+
3
let
rec
hash_rec
accu
=
function
|
(
l
,
(
o
,
x
))
::
rem
->
hash_rec
(
257
*
accu
+
17
*
(
LabelPool
.
hash
l
)
+
x
.
id
)
rem
|
[]
->
accu
+
5
let
rec
hash_rec_list
accu
=
function
|
(
o
,
r
)
::
l
->
hash_rec_list
(
hash_rec
accu
r
)
l
|
[]
->
accu
+
17
let
rec
hash_rec_bool
accu
=
function
|
(
p
,
n
)
::
l
->
hash_rec_bool
(
hash_rec_list
(
hash_rec_list
accu
p
)
n
)
l
|
[]
->
accu
+
3
let
hash_descr
a
=
let
accu
=
(
Hashtbl
.
hash
a
.
ints
)
+
17
*
(
Hashtbl
.
hash
a
.
atoms
)
+
257
*
(
Hashtbl
.
hash
a
.
chars
)
in
let
accu
=
hash_times_bool
accu
a
.
times
in
let
accu
=
hash_times_bool
accu
a
.
xml
in
let
accu
=
hash_times_bool
accu
a
.
arrow
in
let
accu
=
hash_rec_bool
accu
a
.
record
in
accu
module
DescrHash
=
Hashtbl
.
Make
(
...
...
@@ -211,43 +211,10 @@ module DescrHash =
let
print_descr
=
ref
(
fun
_
_
->
assert
false
)
(*
let define n d = check d; define n d
*)
(*
let any_rec = cons { empty with record = Boolean.full }
let any_node = make ();;
define any_node {
times = Boolean.full;
xml = Boolean.atom
(cons { empty with atoms = Atoms.any },
cons (times any_rec any_node));
arrow = Boolean.full;
record= Boolean.full;
ints = Intervals.any;
atoms = Atoms.any;
chars = Chars.any;
};;
internalize any_node;;
let any = descr any_node
*)
let
neg
x
=
diff
any
x
let
any_node
=
cons
any
(*
let get_record r =
let add = SortedMap.add (fun (o1,t1) (o2,t2) -> (o1&&o2, cap t1 t2)) in
let line (p,n) =
let accu = List.fold_left
(fun accu (l,o,t) -> add l (o,descr t) accu) [] p in
List.fold_left
(fun accu (l,o,t) -> add l (not o,neg (descr t)) accu) accu n in
List.map line r
*)
module
LabelSet
=
Set
.
Make
(
LabelPool
)
let
get_record
r
=
...
...
@@ -330,14 +297,15 @@ let rec exists max f =
module
Assumptions
=
Set
.
Make
(
struct
type
t
=
descr
let
compare
=
compare
end
)
let
memo
=
ref
Assumptions
.
empty
let
cache_false
=
ref
Assumptions
.
empty
let
cache_false
=
DescrHash
.
create
33000
exception
NotEmpty
let
trivially_empty
d
=
d
=
empty
let
trivially_empty
d
=
equal_descr
d
empty
(* Remove generic equality ... *)
let
rec
empty_rec
d
=
if
Assumptions
.
mem
d
!
cache_false
then
false
if
DescrHash
.
mem
cache_false
d
then
false
else
if
Assumptions
.
mem
d
!
memo
then
true
else
if
not
(
Intervals
.
is_empty
d
.
ints
)
then
false
else
if
not
(
Atoms
.
is_empty
d
.
atoms
)
then
false
...
...
@@ -353,7 +321,7 @@ let rec empty_rec d =
then
true
else
(
memo
:=
backup
;
cache_false
:=
Assumptions
.
add
d
!
cache_false
;
DescrHash
.
add
cache_false
d
()
;
false
)
)
...
...
@@ -364,11 +332,6 @@ and empty_rec_times c =
and
empty_rec_times_aux
(
left
,
right
)
=
let
rec
aux
accu1
accu2
=
function
|
(
t1
,
t2
)
::
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*)
(* THIS IS NOT SOUND !!! *)
if
trivially_empty
(
cap_t
accu1
t1
)
||
trivially_empty
(
cap_t
accu2
t2
)
then
aux
accu1
accu2
right
...
...
@@ -381,16 +344,8 @@ and empty_rec_times_aux (left,right) =
in
let
(
accu1
,
accu2
)
=
cap_product
left
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 *)
(
(* (if (List.length right > 2) then
let (cup1,cup2) = cup_product right in
(empty_rec (diff accu1 cup1)) && (empty_rec (diff accu2 cup2))
else true)
&& *)
(
try
aux
accu1
accu2
right
;
true
with
NotEmpty
->
false
)
)
and
empty_rec_arrow
c
=
List
.
for_all
empty_rec_arrow_aux
c
...
...
@@ -420,7 +375,7 @@ and empty_rec_record_aux (labels,(oleft,(left_opt,left)),rights) =
exists
(
Array
.
length
left
)
(
fun
i
->
(
not
(
left_opt
.
(
i
)
&&
right_opt
.
(
i
)))
&&
(
empty
_rec
(
cap
left
.
(
i
)
right
.
(
i
))))
(
trivially_
empty
(
cap
left
.
(
i
)
right
.
(
i
))))
in
if
next
then
aux
rights
else
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment