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
e0fb3c2c
Commit
e0fb3c2c
authored
Jun 13, 2014
by
Pietro Abate
Browse files
Code review. Minor changes
parent
241c06cc
Changes
1
Hide whitespace changes
Inline
Side-by-side
types/types.ml
View file @
e0fb3c2c
...
...
@@ -2404,20 +2404,21 @@ struct
|
`Record
of
bool
*
(
bool
*
Ns
.
Label
.
t
*
v
)
list
]
and
v
=
{
mutable
def
:
rhs
;
mutable
node
:
node
option
}
let
rec
make_descr
seen
v
=
if
List
.
memq
v
seen
then
empty
else
let
seen
=
v
::
seen
in
match
v
.
def
with
|
`Type
d
->
d
|
`Variable
d
->
var
d
|
`Variable
d
->
var
d
|
`Cup
vl
->
List
.
fold_left
(
fun
acc
v
->
cup
acc
(
make_descr
seen
v
))
empty
vl
|
`Cap
vl
->
List
.
fold_left
(
fun
acc
v
->
cap
acc
(
make_descr
seen
v
))
any
vl
|
`Times
(
v1
,
v2
)
->
times
(
make_node
v1
)
(
make_node
v2
)
|
`Arrow
(
v1
,
v2
)
->
arrow
(
make_node
v1
)
(
make_node
v2
)
|
`Xml
(
v1
,
v2
)
->
xml
(
make_node
v1
)
(
make_node
v2
)
|
`Record
(
b
,
flst
)
->
rec_of_list
b
(
List
.
map
(
fun
(
b
,
l
,
v
)
->
(
b
,
l
,
make_descr
seen
v
))
flst
)
|
`Neg
v
->
neg
(
make_descr
seen
v
)
|
`Record
(
b
,
flst
)
->
rec_of_list
b
(
List
.
map
(
fun
(
b
,
l
,
v
)
->
(
b
,
l
,
make_descr
seen
v
))
flst
)
|
`Neg
v
->
neg
(
make_descr
seen
v
)
and
make_node
v
=
match
v
.
node
with
...
...
@@ -2428,7 +2429,8 @@ struct
let
d
=
make_descr
[]
v
in
define
n
d
;
n
(* Kim: We shadow the corresponding definitions in the outer module *)
(* We shadow the corresponding definitions in the outer module *)
let
forward
()
=
{
def
=
`Cup
[]
;
node
=
None
}
let
def
v
d
=
v
.
def
<-
d
let
cons
d
=
let
v
=
forward
()
in
def
v
d
;
v
...
...
@@ -2546,59 +2548,41 @@ struct
in
aux
v
subst
let
print
ppf
v
=
let
id
=
ref
0
in
let
memo
=
MemoHash
.
create
17
in
let
rec
aux
v
=
let
rec
aux
ppf
v
=
try
let
s
=
MemoHash
.
find
memo
v
in
Format
.
fprintf
ppf
"%s"
s
with
Not_found
->
begin
let
node_name
=
Printf
.
sprintf
"X_%i"
!
id
in
incr
id
;
(*memo := (v, node_v) :: !memo; *)
MemoHash
.
add
memo
v
node_name
;
match
v
.
def
with
|
`Type
d
->
Format
.
fprintf
ppf
"`Type(%a)"
Print
.
print
d
|
`Variable
d
->
Format
.
fprintf
ppf
"`Var(%a)"
Var
.
print
d
|
`Cup
vl
->
Format
.
fprintf
ppf
"`Cup("
;
List
.
iter
(
fun
v
->
Format
.
fprintf
ppf
" "
;
aux
v
)
vl
;
Format
.
fprintf
ppf
")"
|
`Cap
vl
->
Format
.
fprintf
ppf
"`Cap("
;
List
.
iter
(
fun
v
->
Format
.
fprintf
ppf
" "
;
aux
v
)
vl
;
Format
.
fprintf
ppf
")"
|
`Times
(
v1
,
v2
)
->
Format
.
fprintf
ppf
"`Times("
;
aux
v1
;
Format
.
fprintf
ppf
","
;
aux
v2
;
Format
.
fprintf
ppf
")"
;
|
`Arrow
(
v1
,
v2
)
->
Format
.
fprintf
ppf
"`Arrow("
;
aux
v1
;
Format
.
fprintf
ppf
","
;
aux
v2
;
Format
.
fprintf
ppf
")"
;
|
`Xml
(
v1
,
v2
)
->
Format
.
fprintf
ppf
"`Xml("
;
aux
v1
;
Format
.
fprintf
ppf
","
;
aux
v2
;
Format
.
fprintf
ppf
")"
;
|
`Record
_
->
()
|
`Neg
v
->
Format
.
fprintf
ppf
"`Neg("
;
aux
v
;
Format
.
fprintf
ppf
")"
;
end
with
Not_found
->
begin
let
node_name
=
Printf
.
sprintf
"X_%i"
!
id
in
incr
id
;
MemoHash
.
add
memo
v
node_name
;
let
print_lst
f
ppf
l
=
let
rec
aux
ppf
=
function
|
[]
->
Format
.
fprintf
ppf
"@."
|
[
h
]
->
Format
.
fprintf
ppf
"%a"
f
h
|
h
::
t
->
Format
.
fprintf
ppf
"%a ;%a"
f
h
aux
t
in
match
l
with
|
[]
->
Format
.
fprintf
ppf
"[]"
|_
->
Format
.
fprintf
ppf
"[%a]"
aux
l
in
match
v
.
def
with
|
`Type
d
->
Format
.
fprintf
ppf
"`Type(%a)"
Print
.
print
d
|
`Variable
d
->
Format
.
fprintf
ppf
"`Var(%a)"
Var
.
print
d
|
`Cup
vl
->
Format
.
fprintf
ppf
"`Cup(%a)"
(
print_lst
aux
)
vl
|
`Cap
vl
->
Format
.
fprintf
ppf
"`Cap(%a)"
(
print_lst
aux
)
vl
|
`Times
(
v1
,
v2
)
->
Format
.
fprintf
ppf
"`Times(%a,%a)"
aux
v1
aux
v2
|
`Arrow
(
v1
,
v2
)
->
Format
.
fprintf
ppf
"`Arrow(%a,%a)"
aux
v1
aux
v2
|
`Xml
(
v1
,
v2
)
->
Format
.
fprintf
ppf
"`Xml(%a,%a)"
aux
v1
aux
v2
|
`Record
_
->
Format
.
fprintf
ppf
"`Record"
|
`Neg
v
->
Format
.
fprintf
ppf
"`Neg(%a)"
aux
v
end
in
aux
v
(* returns a recursive type where all occurrences of alpha n t
* are substituted with a recursive variable X *)
let
substituterec
t
alpha
=
...
...
@@ -2639,57 +2623,51 @@ struct
let
new_t
=
substitute_aux
dec
(
subst
h
)
in
descr
(
solve
new_t
)
(* Kim: we cannot use the variance annotation of variables to simplify them,
since variables are shared amongst types. If we have two types
A -> A and (A,A) (produced by the algorithm) then we can still simplify the
latter but the variance annotation tells us that A is invariant.
*)
let
rec
pretty_name
i
acc
=
let
ni
,
nm
=
i
/
26
,
i
mod
26
in
let
acc
=
acc
^
(
String
.
make
1
(
OldChar
.
chr
(
OldChar
.
code
'
A'
+
nm
)))
in
if
ni
==
0
then
acc
else
pretty_name
ni
acc
(* We cannot use the variance annotation of variables to simplify them,
since variables are shared amongst types. If we have two types
A -> A and (A,A) (produced by the algorithm) then we can still simplify the
latter but the variance annotation tells us that A is invariant.
*)
let
collect_variables
v
=
let
module
Memo
=
Hashtbl
.
Make
(
struct
type
t
=
bool
*
v
let
hash
=
Hashtbl
.
hash
let
equal
(
a
,
b
)
(
c
,
d
)
=
a
==
c
&&
b
==
d
end
)
in
let
vars
=
Hashtbl
.
create
17
in
let
memo
=
Memo
.
create
17
in
let
t_emp
=
cup
[]
in
let
t_any
=
cap
[]
in
let
idx
=
ref
0
in
let
rec
pretty_name
i
acc
=
let
ni
,
nm
=
i
/
26
,
i
mod
26
in
let
acc
=
acc
^
(
String
.
make
1
(
OldChar
.
chr
(
OldChar
.
code
'
A'
+
nm
)))
in
if
ni
==
0
then
acc
else
pretty_name
ni
acc
let
collect_variables
v
=
(* we memoize based on the pair (pos, v), since v can occur both
* positively and negatively. and we want to manage the variables
* differently in both cases *)
let
module
Memo
=
Hashtbl
.
Make
(
struct
type
t
=
bool
*
v
let
hash
=
Hashtbl
.
hash
let
equal
(
a
,
b
)
(
c
,
d
)
=
a
==
c
&&
b
==
d
end
)
in
let
vars
=
Hashtbl
.
create
17
in
let
memo
=
Memo
.
create
17
in
let
t_emp
=
cup
[]
in
let
t_any
=
cap
[]
in
let
idx
=
ref
0
in
let
rec
aux
pos
v
=
if
not
(
Memo
.
mem
memo
(
pos
,
v
))
then
let
()
=
Memo
.
add
memo
(
pos
,
v
)
()
in
match
v
.
def
with
|
`Type
d
->
()
|
`Variable
d
->
begin
try
|
`Variable
d
->
begin
try
let
td
=
Hashtbl
.
find
vars
d
in
if
((
td
==
t_emp
)
&&
not
pos
)
||
((
td
==
t_any
)
&&
pos
)
then
(* polarity conflict, replace the binding by a new,
pretty-printed variable *)
begin
let
id
=
pretty_name
!
idx
""
in
let
x
=
var
(
Var
.
mk
~
fresh
:
false
id
)
in
incr
idx
;
Hashtbl
.
replace
vars
d
x
;
end
with
Not_found
->
(* first time we see a variable,
set to empty for covariant and
any for contravariant *)
Hashtbl
.
add
vars
d
(
if
pos
then
t_emp
else
t_any
)
end
(* polarity conflict, replace the binding by a new, pretty-printed variable *)
if
((
td
==
t_emp
)
&&
not
pos
)
||
((
td
==
t_any
)
&&
pos
)
then
begin
let
id
=
pretty_name
!
idx
""
in
let
x
=
var
(
Var
.
mk
~
fresh
:
false
id
)
in
incr
idx
;
Hashtbl
.
replace
vars
d
x
;
end
(* first time we see a variable, set to empty for covariant and
any for contravariant *)
with
Not_found
->
Hashtbl
.
add
vars
d
(
if
pos
then
t_emp
else
t_any
)
end
|
`Cup
vl
|
`Cap
vl
->
List
.
iter
(
fun
v
->
aux
pos
v
)
vl
|
`Times
(
v1
,
v2
)
|
`Xml
(
v1
,
v2
)
->
(
aux
pos
v1
);
(
aux
pos
v2
)
|
`Arrow
(
v1
,
v2
)
->
(
aux
(
not
pos
)
v1
);
(
aux
pos
v2
)
...
...
@@ -2699,46 +2677,39 @@ struct
aux
true
v
;
vars
let
clean_variables
t
=
if
no_var
t
then
t
else
begin
let
dec
=
decompose
t
in
let
h
=
collect_variables
dec
in
let
new_t
=
substitute_aux
dec
(
fun
d
->
try
Hashtbl
.
find
h
d
with
Not_found
->
assert
false
)
in
descr
(
solve
new_t
)
end
let
clean_variables
t
=
if
no_var
t
then
t
else
begin
let
dec
=
decompose
t
in
let
h
=
collect_variables
dec
in
let
new_t
=
substitute_aux
dec
(
fun
d
->
try
Hashtbl
.
find
h
d
with
Not_found
->
assert
false
)
in
descr
(
solve
new_t
)
end
let
rec
uniq
=
function
|
([]
|
[
_
])
as
l
->
l
|
t1
::
((
t2
::
_
)
as
l1
)
->
if
equiv
t1
t2
then
uniq
l1
else
t1
::
uniq
l1
let
clean_type
t
=
if
no_var
t
then
t
else
let
t
=
clean_variables
t
in
let
arrow_t
,
non_arrow_t
=
{
empty
with
arrow
=
t
.
arrow
}
,
{
t
with
arrow
=
empty
.
arrow
}
in
let
_
,
u_arrow
=
Arrow
.
get
arrow_t
in
List
.
fold_left
(
fun
acc
i_arrow
->
T
.
cup
acc
(
let
conj_arrow
=
(
List
.
fold_left
(
fun
acc
(
dom
,
cdom
)
->
let
clean_type
t
=
if
no_var
t
then
t
else
let
t
=
clean_variables
t
in
let
arrow_t
,
non_arrow_t
=
{
empty
with
arrow
=
t
.
arrow
}
,
{
t
with
arrow
=
empty
.
arrow
}
in
let
_
,
u_arrow
=
Arrow
.
get
arrow_t
in
List
.
fold_left
(
fun
acc
i_arrow
->
T
.
cup
acc
(
let
conj_arrow
=
List
.
fold_left
(
fun
acc
(
dom
,
cdom
)
->
let
indiv_arrow
=
T
.
arrow
(
T
.
cons
dom
)
(
T
.
cons
cdom
)
in
indiv_arrow
::
acc
)
[]
i_arrow
)
in
let
sorted_conj
=
List
.
sort
(
fun
t1
t2
->
if
equiv
t1
t2
then
0
else
compare
t1
t2
)
conj_arrow
in
List
.
fold_left
(
T
.
cap
)
T
.
any
(
uniq
sorted_conj
)
)
)
non_arrow_t
u_arrow
DescrSList
.
add
indiv_arrow
acc
)
DescrSList
.
empty
i_arrow
in
DescrSList
.
fold
(
T
.
cap
)
T
.
any
conj_arrow
)
)
non_arrow_t
u_arrow
end
...
...
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