Skip to content
GitLab
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
5d9c8545
Commit
5d9c8545
authored
Apr 01, 2015
by
Kim Nguyễn
Browse files
Further refactoring of type iterators.
parent
3e105c5e
Changes
5
Hide whitespace changes
Inline
Side-by-side
types/bool.ml
View file @
5d9c8545
...
...
@@ -350,7 +350,7 @@ sig
(** returns the union of all leaves in the BDD *)
val
leafconj
:
t
->
Atom
.
t
val
get_kind
:
t
->
(
Var
.
t
list
*
Var
.
t
list
*
Atom
.
t
option
)
list
val
is_empty
:
t
->
bool
val
extract
:
t
->
[
`Empty
|
`Full
|
`Split
of
(
elem
*
t
*
t
*
t
)
]
...
...
@@ -431,4 +431,24 @@ struct
|
True
->
`Full
|
Split
(
_
,
x
,
p
,
i
,
n
)
->
`Split
(
x
,
p
,
i
,
n
)
(* todo optimize *)
let
get_kind
t
=
let
rec
split_vars
l
acc
=
match
l
with
`Var
v
::
r
->
split_vars
r
(
v
::
acc
)
|
[
`Atm
a
]
->
List
.
rev
acc
,
Some
a
|
[]
->
List
.
rev
acc
,
None
|
_
->
assert
false
in
List
.
map
(
fun
(
pos
,
neg
)
->
let
pos
,
atm
=
split_vars
pos
[]
in
let
neg
=
List
.
map
(
function
`Var
v
->
v
|
_
->
assert
false
)
neg
in
let
oatm
=
match
atm
with
Some
a
when
T
.
equal
a
T
.
full
->
None
|
_
->
atm
in
(
pos
,
neg
,
oatm
))
(
get
t
)
end
types/bool.mli
View file @
5d9c8545
...
...
@@ -39,8 +39,8 @@ sig
(** returns the union of all leaves in the BDD *)
val
leafconj
:
t
->
Atom
.
t
val
leafconj
:
t
->
Atom
.
t
val
get_kind
:
t
->
(
Var
.
t
list
*
Var
.
t
list
*
Atom
.
t
option
)
list
val
is_empty
:
t
->
bool
val
extract
:
t
->
[
`Empty
|
`Full
|
`Split
of
(
elem
*
t
*
t
*
t
)
]
...
...
types/type_tallying.ml
View file @
5d9c8545
...
...
@@ -314,8 +314,6 @@ let big_prod delta f acc l =
Constr
.
prod
delta
acc
(
f
pos
neg
)
)
acc
l
(* norm generates a constraint set for the costraint t <= 0 *)
module
NormMemoHash
=
Hashtbl
.
Make
(
Custom
.
Pair
(
Descr
)(
Var
.
Set
))
...
...
types/types.ml
View file @
5d9c8545
...
...
@@ -1632,62 +1632,114 @@ module Iter =
DescrHash
.
add
memo
res
res
;
res
let
compute
~
cup
~
cap
~
neg
~
var
~
atoms
~
ints
~
chars
~
times
~
xml
~
arrow
~
record
~
abstract
~
absent
t
=
module
type
Ops
=
sig
type
t
val
cup
:
t
list
->
t
val
cap
:
t
list
->
t
val
neg
:
t
->
t
val
var
:
Var
.
t
list
*
Var
.
t
list
->
t
val
atoms
:
Atoms
.
t
->
t
val
ints
:
Intervals
.
t
->
t
val
chars
:
Chars
.
t
->
t
val
times
:
Pair
.
t
->
t
val
xml
:
Pair
.
t
->
t
val
arrow
:
Pair
.
t
->
t
val
record
:
Rec
.
t
->
t
val
abstract
:
Abstracts
.
t
->
t
val
absent
:
bool
->
t
end
let
compute_ops
(
type
res
)
(
module
O
:
Ops
with
type
t
=
res
)
t
=
let
t
=
simplify
t
in
let
any_node2
=
any_node
,
any_node
in
let
any_atoms
=
atoms
Atoms
.
full
in
let
any_ints
=
ints
Intervals
.
full
in
let
any_chars
=
chars
Chars
.
full
in
let
any_abstract
=
abstract
Abstracts
.
full
in
let
any_times
=
times
any_node2
in
let
any_xml
=
xml
any_node2
in
let
any_record
=
record
(
true
,
LabelMap
.
empty
)
in
let
any_arrow
=
arrow
(
empty_node
,
any_node
)
in
let
var_or
do_atom
=
function
`Var
v
->
var
v
|
`Atm
atm
->
do_atom
atm
let
module
P
=
struct
include
O
let
any_pair
=
Pair
.
atom
(
any_node
,
any_node
)
let
any_record
=
Rec
.
atom
(
true
,
LabelMap
.
empty
)
let
any_arrow
=
Pair
.
atom
(
empty_node
,
any_node
)
let
oatm
cap
any
f
x
=
match
x
with
None
->
f
any
|
Some
a
->
f
(
cap
a
any
)
let
atoms
=
oatm
Atoms
.
cap
Atoms
.
full
atoms
let
ints
=
oatm
Intervals
.
cap
Intervals
.
full
ints
let
chars
=
oatm
Chars
.
cap
Chars
.
full
chars
let
times
=
oatm
Pair
.
cap
any_pair
times
let
xml
=
oatm
Pair
.
cap
any_pair
xml
let
arrow
=
oatm
Pair
.
cap
any_arrow
arrow
let
record
=
oatm
Rec
.
cap
any_record
record
let
abstract
=
oatm
Abstracts
.
cap
Abstracts
.
full
abstract
end
in
let
simple_bdd
(
type
bdd
)
(
type
atom
)
any
do_atom
(
module
B
:
Bool
.
S
with
type
t
=
bdd
and
type
elem
=
atom
)
acc
bv
=
List
.
fold_left
(
fun
acc
(
ipos
,
ineg
)
->
match
List
.
map
do_atom
ipos
,
List
.
map
do_atom
ineg
with
|
[]
,
[]
->
any
::
acc
|
[
e
]
,
[]
->
e
::
acc
|
[]
,
l
->
cap
(
any
::
List
.
map
neg
l
)
::
acc
|
l1
,
l2
->
cap
(
l1
@
List
.
map
neg
l2
)
::
acc
)
acc
(
B
.
get
bv
)
let
bdd
(
type
atom
)
do_atom
(
module
V
:
VarType
with
type
Atom
.
t
=
atom
)
acc
t
=
List
.
fold_left
(
fun
acc
(
vpos
,
vneg
,
oatm
)
->
let
res
=
[(
do_atom
oatm
)
;
P
.
var
(
vpos
,
vneg
)]
in
(
P
.
cap
res
)
::
acc
)
acc
V
.(
get_kind
(
proj
t
))
in
let
cplx_bdd
(
type
atom
)
(
type
atom2
)
any
do_atom
(
module
V
:
VarType
with
type
Atom
.
t
=
atom
and
type
Atom
.
elem
=
atom2
)
acc
bdd
=
simple_bdd
(
cap
[]
)
(
var_or
(
fun
t
->
cup
(
simple_bdd
(
any
)
do_atom
(
module
V
.
Atom
)
[]
t
)))
(
module
V
)
acc
bdd
let
acc
=
[
P
.
absent
(
Descr
.
get_absent
t
)
]
in
let
acc
=
bdd
P
.
atoms
(
module
VarAtoms
)
acc
t
in
let
acc
=
bdd
P
.
ints
(
module
VarIntervals
)
acc
t
in
let
acc
=
bdd
P
.
chars
(
module
VarChars
)
acc
t
in
let
acc
=
bdd
P
.
times
(
module
VarTimes
)
acc
t
in
let
acc
=
bdd
P
.
xml
(
module
VarXml
)
acc
t
in
let
acc
=
bdd
P
.
arrow
(
module
VarArrow
)
acc
t
in
let
acc
=
bdd
P
.
record
(
module
VarRec
)
acc
t
in
let
acc
=
bdd
P
.
abstract
(
module
VarAbstracts
)
acc
t
in
O
.
cup
acc
let
compute
(
type
res
)
~
default
?
cup
?
cap
?
neg
?
var
?
atoms
?
ints
?
chars
?
times
?
xml
?
arrow
?
record
?
abstract
?
absent
t
=
let
get
f
x
=
match
f
with
None
->
default
|
Some
f
->
f
x
in
let
module
O
=
struct
type
t
=
res
let
cup
=
get
cup
let
cap
=
get
cap
let
neg
=
get
neg
let
var
(
vpos
,
vneg
)
=
let
var
=
get
var
in
cap
((
List
.
map
var
vpos
)
@
(
List
.
map
(
fun
x
->
neg
(
var
x
))
vneg
))
let
atoms
=
get
atoms
let
ints
=
get
ints
let
chars
=
get
chars
let
times
=
get
times
let
xml
=
get
xml
let
arrow
=
get
arrow
let
record
=
get
record
let
abstract
=
get
abstract
let
absent
=
get
absent
end
in
let
acc
=
absent
t
.
absent
in
let
acc
=
simple_bdd
any_ints
(
var_or
ints
)
(
module
VarIntervals
)
acc
t
.
ints
in
let
acc
=
simple_bdd
any_atoms
(
var_or
atoms
)
(
module
VarAtoms
)
acc
t
.
atoms
in
let
acc
=
simple_bdd
any_chars
(
var_or
chars
)
(
module
VarChars
)
acc
t
.
chars
in
let
acc
=
simple_bdd
any_abstract
(
var_or
abstract
)
(
module
VarAbstracts
)
acc
t
.
abstract
in
let
acc
=
cplx_bdd
any_times
times
(
module
VarTimes
)
acc
t
.
times
in
let
acc
=
cplx_bdd
any_xml
xml
(
module
VarXml
)
acc
t
.
xml
in
let
acc
=
cplx_bdd
any_arrow
arrow
(
module
VarArrow
)
acc
t
.
arrow
in
let
acc
=
cplx_bdd
any_record
record
(
module
VarRec
)
acc
t
.
record
in
match
acc
with
[
e
]
->
e
|
_
->
cup
acc
compute_ops
(
module
O
:
Ops
with
type
t
=
res
)
t
let
compute_deep
~
default
?
cup
?
cap
?
neg
?
var
?
atoms
?
ints
?
chars
?
times
?
xml
?
arrow
?
record
?
abstract
?
absent
t
=
let
get
f
x
=
match
f
with
None
->
default
|
Some
f
->
f
x
in
let
cup
=
get
cup
in
let
cap
=
get
cap
in
let
times
=
get
times
in
let
xml
=
get
xml
in
let
record
=
get
record
in
let
neg
=
get
neg
in
let
bdd
(
type
bdd
)
(
type
atom
)
do_atom
(
module
B
:
Bool
.
S
with
type
t
=
bdd
and
type
elem
=
atom
)
bv
=
cup
(
List
.
fold_left
(
fun
acc
(
ipos
,
ineg
)
->
match
List
.
map
do_atom
ipos
,
List
.
map
do_atom
ineg
with
|
[
e
]
,
[]
->
e
::
acc
|
[]
,
l
->
cap
(
List
.
map
neg
l
)
::
acc
|
l1
,
l2
->
cap
(
l1
@
List
.
map
neg
l2
)
::
acc
)
[]
(
B
.
get
bv
))
in
compute
~
default
~
cup
~
cap
~
neg
~
var
:
(
get
var
)
~
atoms
:
(
get
atoms
)
~
ints
:
(
get
ints
)
~
chars
:
(
get
chars
)
~
times
:
(
bdd
times
(
module
Pair
))
~
xml
:
(
bdd
xml
(
module
Pair
))
~
arrow
:
(
bdd
(
get
arrow
)
(
module
Pair
))
~
record
:
(
bdd
record
(
module
Rec
))
~
abstract
:
(
get
abstract
)
~
absent
:
(
get
absent
)
t
end
module
Variable
=
...
...
@@ -1704,7 +1756,6 @@ module Variable =
Var
.
Set
.(
cup
a1
s1
,
cup
a2
s2
,
cup
a3
s3
))
empty3
l
in
let
cst_empty3
_
=
empty3
in
let
rec
loop
t
=
try
DescrHash
.
find
memo
t
...
...
@@ -1712,21 +1763,11 @@ module Variable =
Not_found
->
DescrHash
.
add
memo
t
empty3
;
let
res
=
Iter
.
compute
~
cup
:
merge
~
cap
:
merge
~
neg
:
(
fun
(
a
,
b
,
c
)
->
(
a
,
c
,
b
))
~
var
:
(
fun
v
->
let
e
=
Var
.
Set
.
singleton
v
in
e
,
e
,
Var
.
Set
.
empty
)
~
ints
:
cst_empty3
~
chars
:
cst_empty3
~
atoms
:
cst_empty3
~
abstract
:
cst_empty3
~
xml
:
prod
~
times
:
prod
~
arrow
:
arrow
~
record
:
record
~
absent
:
(
fun
_
->
[]
)
t
Iter
.
compute_deep
~
default
:
empty3
~
cup
:
merge
~
cap
:
merge
~
neg
:
(
fun
(
a
,
b
,
c
)
->
(
a
,
c
,
b
))
~
var
:
(
fun
v
->
let
e
=
Var
.
Set
.
singleton
v
in
e
,
e
,
Var
.
Set
.
empty
)
~
times
:
prod
~
xml
:
prod
~
arrow
:
arrow
~
record
:
record
t
in
DescrHash
.
replace
memo
t
res
;
res
...
...
@@ -1739,13 +1780,13 @@ module Variable =
and
_
,
y2
,
z2
=
loop
(
descr
t2
)
in
Var
.
Set
.(
empty
,
cup
z1
y2
,
cup
y1
z2
)
and
record
(
b
,
lm
)
=
let
_
,
y
,
z
=
merge
(
List
.
map
(
fun
(
_
,
t
)
->
(
loop
(
descr
t
)))
(
LabelMap
.
get
lm
))
let
_
,
y
,
z
=
merge
(
List
.
map
(
fun
(
_
,
t
)
->
(
loop
(
descr
t
)))
(
LabelMap
.
get
lm
))
in
Var
.
Set
.
empty
,
y
,
z
in
loop
t
let
no_var
t
=
let
memo
=
DescrHash
.
create
17
in
let
rec
loop
t
=
...
...
@@ -1754,23 +1795,11 @@ module Variable =
with
Not_found
->
DescrHash
.
add
memo
t
()
;
Iter
.
compute
~
cup
:
ignore
~
cap
:
ignore
~
neg
:
ignore
Iter
.
compute_deep
~
default
:
()
~
var
:
(
fun
_
->
raise
Not_found
)
~
ints
:
ignore
~
chars
:
ignore
~
atoms
:
ignore
~
abstract
:
ignore
~
xml
:
prod
~
times
:
prod
~
arrow
:
prod
~
record
:
record
~
absent
:
(
fun
_
->
[]
)
t
and
prod
(
t1
,
t2
)
=
loop
(
descr
t1
);
loop
(
descr
t2
)
~
xml
:
prod
~
times
:
prod
~
arrow
:
prod
~
record
:
record
t
and
prod
(
t1
,
t2
)
=
loop
(
descr
t1
);
loop
(
descr
t2
)
and
record
(
b
,
lm
)
=
List
.
iter
(
fun
(
_
,
t
)
->
(
loop
(
descr
t
)))
(
LabelMap
.
get
lm
)
...
...
@@ -1789,8 +1818,7 @@ module Variable =
res
let
all_vars
t
=
let
_
,
_
,
_
,
all
=
collect_vars
t
in
all
let
_
,
_
,
_
,
all
=
collect_vars
t
in
all
let
is_ground
=
let
h
=
DescrHash
.
create
17
in
...
...
@@ -1803,8 +1831,7 @@ module Variable =
let
no_var
=
is_ground
let
is_closed
delta
t
=
Var
.
Set
.
subset
(
all_vars
t
)
delta
let
is_closed
delta
t
=
Var
.
Set
.
subset
(
all_vars
t
)
delta
let
all_tlv
t
=
let
tlv
,
_
,
_
,
_
=
collect_vars
t
in
tlv
...
...
@@ -1994,8 +2021,8 @@ module Print = struct
let
worth_complement
d
=
let
c
=
Iter
.
fold
(
fun
(
module
V
:
VarType
)
t
acc
->
if
is_empty
(
V
.
inj
(
V
.
proj
t
))
then
acc
+
1
else
acc
)
(
diff
any
d
)
0
if
is_empty
(
V
.
inj
(
V
.
proj
t
))
then
acc
+
1
else
acc
)
(
diff
any
d
)
0
in
c
>=
5
...
...
@@ -2729,9 +2756,7 @@ module Print = struct
let
pair
(
n1
,
n2
)
=
nodes
:=
NodeSet
.
add
n1
(
NodeSet
.
add
n2
!
nodes
)
in
Iter
.
compute
~
cup
:
ignore
~
cap
:
ignore
~
neg
:
ignore
~
var
:
ignore
~
atoms
:
ignore
~
ints
:
ignore
~
chars
:
ignore
~
abstract
:
ignore
~
absent
:
(
fun
_
->
[]
)
Iter
.
compute_deep
~
default
:
()
~
times
:
pair
~
xml
:
pair
~
arrow
:
pair
~
record
:
(
fun
(
_
,
lm
)
->
LabelMap
.
iter
(
fun
n
->
nodes
:=
NodeSet
.
add
n
!
nodes
)
lm
)
t
;
match
NodeSet
.
elements
!
nodes
with
...
...
@@ -3150,7 +3175,7 @@ module Positive = struct
in
res
.
descr
<-
Some
t
;
res
and
loop_struct
t
=
Iter
.
compute
Iter
.
compute
_deep
~
default
:
(
cup
[]
)
~
cup
~
cap
~
neg
~
var
~
ints
:
interval
~
chars
:
char
...
...
@@ -3162,7 +3187,7 @@ module Positive = struct
~
record
:
(
fun
(
b
,
lm
)
->
record
b
(
List
.
map
(
fun
(
l
,
t
)
->
let
t
=
descr
t
in
t
.
absent
,
l
,
loop
t
)
(
LabelMap
.
get
lm
)))
~
absent
:
(
function
true
->
[
ty
Record
.
absent
]
|
_
->
[]
)
t
~
absent
:
(
function
true
->
ty
Record
.
absent
|
_
->
cup
[]
)
t
in
loop
t
...
...
types/types.mli
View file @
5d9c8545
...
...
@@ -169,6 +169,24 @@ module Iter : sig
val
map
:
?
abs
:
(
bool
->
bool
)
->
(
var_type
->
t
->
t
)
->
t
->
t
val
iter
:
?
abs
:
(
bool
->
unit
)
->
(
var_type
->
t
->
unit
)
->
t
->
unit
val
fold
:
?
abs
:
(
bool
->
'
a
->
'
a
)
->
(
var_type
->
t
->
'
a
->
'
a
)
->
t
->
'
a
->
'
a
module
type
Ops
=
sig
type
t
val
cup
:
t
list
->
t
val
cap
:
t
list
->
t
val
neg
:
t
->
t
val
var
:
Var
.
t
list
*
Var
.
t
list
->
t
val
atoms
:
Atoms
.
t
->
t
val
ints
:
Intervals
.
t
->
t
val
chars
:
Chars
.
t
->
t
val
times
:
Pair
.
t
->
t
val
xml
:
Pair
.
t
->
t
val
arrow
:
Pair
.
t
->
t
val
record
:
Rec
.
t
->
t
val
abstract
:
Abstracts
.
t
->
t
val
absent
:
bool
->
t
end
val
compute_ops
:
(
module
Ops
with
type
t
=
'
a
)
->
t
->
'
a
end
(** Positive systems and least solutions **)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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