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
f49dc4b9
Commit
f49dc4b9
authored
Aug 21, 2014
by
Kim Nguyễn
Browse files
Make the type Var.t completely abstract.
parent
f32ff557
Changes
4
Hide whitespace changes
Inline
Side-by-side
types/boolVar.ml
View file @
f49dc4b9
...
...
@@ -151,7 +151,7 @@ module Make (T : E) : S with type s = T.t = struct
in
let
a
=
atom
(
`Atm
T
.
full
)
in
let
h
=
compute_hash
v
a
`False
`False
in
(
`Split
(
h
,
v
,
a
,
`False
,
`False
)
:>
t
)
(
`Split
(
h
,
`Var
v
,
a
,
`False
,
`False
)
:>
t
)
let
rec
iter
f
=
function
|
`Split
(
_
,
x
,
p
,
i
,
n
)
->
f
x
;
iter
f
p
;
iter
f
i
;
iter
f
n
...
...
types/types.ml
View file @
f49dc4b9
...
...
@@ -960,8 +960,8 @@ let get_variables main_memo temp_memo t =
)
acc
(
BV
.
get
bdd
)
in
let
get_vars_boolvar
get_atom
pos
(
tlvp
,
tlvn
,
vars
)
=
function
|
(
`Var
v
)
as
x
when
pos
->
Var
.
Set
.
add
x
tlvp
,
tlvn
,
Var
.
Set
.
add
x
vars
|
(
`Var
v
)
as
x
->
tlvp
,
Var
.
Set
.
add
x
tlvn
,
Var
.
Set
.
add
x
vars
|
`Var
v
when
pos
->
Var
.
Set
.
add
v
tlvp
,
tlvn
,
Var
.
Set
.
add
v
vars
|
`Var
v
->
tlvp
,
Var
.
Set
.
add
v
tlvn
,
Var
.
Set
.
add
v
vars
|
`Atm
x
->
let
_
,
_
,
vars'
=
get_atom
pos
(
Var
.
Set
.
empty
,
Var
.
Set
.
empty
,
vars
)
x
in
...
...
@@ -1794,7 +1794,7 @@ struct
List
.
fold_left
(
fun
(
acc_v
,
acc_a
)
e
->
match
e
with
`Atm
_
->
(
acc_v
,
op
e
acc_a
)
|
`Var
_
as
x
->
(
Var
.
Set
.
add
x
acc_v
,
acc_a
)
|
`Var
x
->
(
Var
.
Set
.
add
x
acc_v
,
acc_a
)
)
(
Var
.
Set
.
empty
,
init
)
l
in
let
fill_line
(
type
s
)
...
...
@@ -2690,7 +2690,7 @@ module Positive = struct
|
l
->
(
cap
l
)
::
acc
)
acc
dnf
in
let
or_var
f
=
function
|
(
`Var
_
)
as
v
->
var
v
|
`Var
x
->
var
x
|
`Atm
a
->
f
a
in
let
decompose_kind
any
make
dnf
acc
=
...
...
@@ -3161,7 +3161,7 @@ module Tallying = struct
let
aux
f
constr
l
=
List
.
fold_left
(
fun
acc
->
function
|
`Var
a
->
cap
acc
(
f
(
var
(
`Var
a
)
))
|
`Var
a
->
cap
acc
(
f
(
var
a
))
|
`Atm
a
->
cap
acc
(
f
(
constr
a
))
)
any
l
in
...
...
@@ -3196,27 +3196,27 @@ module Tallying = struct
Var
.
compare
v1
v2
else
if
monov1
then
1
else
-
1
in
in
match
(
p
,
n
)
with
|
([]
,
(
`Var
x
)
::
neg
)
->
|
([]
,
(
`Var
x
)
::
neg
)
->
let
t
=
single
(
false
,
x
,
[]
,
neg
)
in
CS
.
singleton
(
Neg
(
t
,
`Var
x
))
CS
.
singleton
(
Neg
(
t
,
x
))
|
((
`Var
x
)
::
pos
,
[]
)
->
let
t
=
single
(
true
,
x
,
pos
,
[]
)
in
CS
.
singleton
(
Pos
(
`Var
x
,
t
))
CS
.
singleton
(
Pos
(
x
,
t
))
|
((
`Var
x
)
::
pos
,
(
`Var
y
)
::
neg
)
->
if
_compare
delta
(
`Var
x
)
(
`Var
y
)
<
0
then
if
_compare
delta
x
y
<
0
then
let
t
=
single
(
true
,
x
,
pos
,
n
)
in
CS
.
singleton
(
Pos
(
`Var
x
,
t
))
CS
.
singleton
(
Pos
(
x
,
t
))
else
let
t
=
single
(
false
,
y
,
p
,
neg
)
in
CS
.
singleton
(
Neg
(
t
,
`Var
y
))
CS
.
singleton
(
Neg
(
t
,
y
))
|
([
`Atm
a
]
,
(
`Var
x
)
::
neg
)
->
let
t
=
single
(
false
,
x
,
p
,
neg
)
in
CS
.
singleton
(
Neg
(
t
,
`Var
x
))
CS
.
singleton
(
Neg
(
t
,
x
))
|
([
`Atm
t
]
,
[]
)
->
norm_rec
(
t
,
delta
,
mem
)
|_,_
->
assert
false
...
...
@@ -3265,7 +3265,7 @@ module Tallying = struct
in
res
end
in
in
(* Format.printf "Normalizing %a yields %a\n%!" Print.pp_type t CS.pp_s res; *)
res
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
...
...
@@ -3400,7 +3400,7 @@ module Tallying = struct
let
solve
s
=
let
aux
((
`Var
v
)
as
alpha
)
(
s
,
t
)
acc
=
let
aux
alpha
(
s
,
t
)
acc
=
(* we cannot solve twice the same variable *)
assert
(
not
(
CS
.
E
.
mem
alpha
acc
));
let
pre
=
Printf
.
sprintf
"#fr_%s_"
(
Var
.
id
alpha
)
in
...
...
types/var.ml
View file @
f49dc4b9
...
...
@@ -7,46 +7,37 @@ module V = struct
let
equal
x
y
=
Pervasives
.
compare
x
.
id
y
.
id
=
0
let
hash
x
=
Hashtbl
.
hash
x
.
id
let
check
_
=
()
let
id
x
=
x
.
id
let
is_internal
x
=
let
s
=
x
.
repr
in
String
.
length
s
>=
1
&&
s
.
[
0
]
==
'
#
'
let
make_id
?
repr
id
=
match
repr
with
|
None
->
{
id
=
id
;
repr
=
id
}
|
Some
r
->
{
id
=
id
;
repr
=
r
}
end
type
var
=
[
`Var
of
V
.
t
]
module
VAR
=
struct
type
t
=
var
let
dump
ppf
(
`Var
x
)
=
Format
.
fprintf
ppf
"%a"
V
.
dump
x
let
compare
(
`Var
x
)
(
`Var
y
)
=
V
.
compare
x
y
let
equal
v1
v2
=
(
compare
v1
v2
)
=
0
let
hash
(
`Var
x
)
=
V
.
hash
x
let
check
_
=
()
end
include
VAR
let
id
(
`Var
x
)
=
x
.
V
.
id
let
is_internal
(
`Var
x
)
=
let
s
=
x
.
V
.
repr
in
String
.
length
s
>=
1
&&
s
.
[
0
]
==
'
#
'
;;
let
mk
?
repr
id
=
make_id
?
repr
id
let
pp
ppf
(
`Var
x
)
=
Format
.
fprintf
ppf
"'%s"
x
.
V
.
repr
let
pp
ppf
x
=
Format
.
fprintf
ppf
"'%s"
x
.
repr
let
mk
?
repr
id
=
`Var
(
V
.
make_id
?
repr
id
)
let
fresh
:
?
pre
:
string
->
unit
->
[
>
var
]
=
let
fresh
:
?
pre
:
string
->
unit
->
t
=
let
counter
=
ref
0
in
fun
?
(
pre
=
"_fresh_"
)
->
fun
_
->
let
id
=
(
Printf
.
sprintf
"%s%d"
pre
!
counter
)
in
let
v
=
mk
id
in
incr
counter
;
v
;;
end
include
V
type
var
=
t
module
Set
=
struct
include
SortedList
.
Make
(
V
AR
)
let
dump
ppf
s
=
Utils
.
pp_list
~
sep
:
";"
~
delim
:
(
"{"
,
"}"
)
V
AR
.
dump
ppf
(
get
s
)
let
pp
ppf
s
=
Utils
.
pp_list
~
sep
:
";"
~
delim
:
(
"{"
,
"}"
)
pp
ppf
(
get
s
)
include
SortedList
.
Make
(
V
)
let
dump
ppf
s
=
Utils
.
pp_list
~
sep
:
";"
~
delim
:
(
"{"
,
"}"
)
V
.
dump
ppf
(
get
s
)
let
pp
ppf
s
=
Utils
.
pp_list
~
sep
:
";"
~
delim
:
(
"{"
,
"}"
)
V
.
pp
ppf
(
get
s
)
let
printf
=
pp
Format
.
std_formatter
let
union
=
cup
let
inter
=
cap
...
...
@@ -55,16 +46,17 @@ module Set = struct
let
fold
=
fold
end
type
'
a
pairvar
=
[
`Atm
of
'
a
|
var
]
module
type
MAKE
=
functor
(
X
:
Custom
.
T
)
->
Custom
.
T
with
type
t
=
X
.
t
pairvar
type
'
a
pairvar
=
[
`Atm
of
'
a
|
`Var
of
t
]
module
Make
(
X
:
Custom
.
T
)
=
struct
type
t
=
X
.
t
pairvar
let
hash
=
function
`Atm
t
->
X
.
hash
t
|
`Var
x
->
V
.
hash
x
let
check
=
function
`Atm
t
->
X
.
check
t
|
`Var
_
->
()
let
compare
t1
t2
=
match
t1
,
t2
with
|
`Var
x
,
`Var
y
->
compare
(
`Var
x
)
(
`Var
y
)
|
`Var
x
,
`Var
y
->
compare
x
y
|
`Atm
x
,
`Atm
y
->
X
.
compare
x
y
|
`Var
_
,
`Atm
_
->
-
1
|
`Atm
_
,
`Var
_
->
1
...
...
@@ -73,5 +65,5 @@ module Make (X : Custom.T) = struct
let
dump
ppf
=
function
|
`Atm
x
->
X
.
dump
ppf
x
|
`Var
x
->
dump
ppf
(
`Var
x
)
|
`Var
x
->
V
.
dump
ppf
x
end
types/var.mli
View file @
f49dc4b9
module
V
:
sig
include
Custom
.
T
val
make_id
:
?
repr
:
string
->
string
->
t
end
type
var
=
[
`Var
of
V
.
t
]
include
Custom
.
T
type
var
=
t
include
Custom
.
T
with
type
t
=
var
val
pp
:
Format
.
formatter
->
var
->
unit
val
mk
:
?
repr
:
string
->
string
->
var
val
fresh
:
?
pre
:
string
->
unit
->
var
val
id
:
var
->
string
val
is_internal
:
var
->
bool
val
pp
:
Format
.
formatter
->
t
->
unit
val
mk
:
?
repr
:
string
->
string
->
t
val
fresh
:
?
pre
:
string
->
unit
->
t
val
id
:
t
->
string
val
is_internal
:
t
->
bool
module
Set
:
sig
include
Custom
.
T
...
...
@@ -33,6 +28,6 @@ module Set : sig
val
choose
:
t
->
var
end
type
'
a
pairvar
=
[
`Atm
of
'
a
|
var
]
module
type
MAKE
=
functor
(
X
:
Custom
.
T
)
->
Custom
.
T
with
type
t
=
X
.
t
pairvar
module
Make
:
MAKE
type
'
a
pairvar
=
[
`Atm
of
'
a
|
`Var
of
t
]
module
Make
(
X
:
Custom
.
T
)
:
Custom
.
T
with
type
t
=
X
.
t
pairvar
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