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
fc179124
Commit
fc179124
authored
Aug 28, 2014
by
Kim Nguyễn
Browse files
Merge branch 'master' of
https://git.cduce.org/cduce
parents
bb37c0ca
737730a2
Changes
12
Hide whitespace changes
Inline
Side-by-side
.ocamlinit
View file @
fc179124
...
...
@@ -28,7 +28,7 @@ let mk_pp = function
let mk_prod l =
List.fold_left (fun acc2 c ->
Tallying.CS.prod (mk_pp c) acc2
Tallying.CS.prod
Var.Set.empty
(mk_pp c) acc2
) Tallying.CS.sat l
let mk_union l1 l2 =
...
...
compile/compile.ml
View file @
fc179124
...
...
@@ -5,7 +5,6 @@ type env = {
cu
:
Compunit
.
t
option
;
(* None: toplevel *)
vars
:
var_loc
Env
.
t
;
(* Id.t to var_loc *)
sigma
:
sigma
;
(* symbolic substitutions (Lambda.sigma) *)
gamma
:
Types
.
Node
.
t
IdMap
.
map
;
(* map of type variables to types *)
xi
:
Var
.
Set
.
t
IdMap
.
map
;
stack_size
:
int
;
max_stack
:
int
ref
;
...
...
@@ -13,19 +12,17 @@ type env = {
}
let
pp_vars
ppf
vars
=
Ident
.
pp_env
Lambda
.
Print
.
pp_vloc
ppf
vars
let
pp_gamma
ppf
gamma
=
Ident
.
pp_idmap
Types
.
Print
.
pp_node
ppf
gamma
let
pp_item
ppf
(
s
,
t
)
=
Format
.
fprintf
ppf
"%s : %a"
s
Lambda
.
Print
.
pp_vloc
t
in
Ident
.
pp_env
pp_item
ppf
vars
let
pp_xi
ppf
xi
=
Ident
.
pp_idmap
Var
.
Set
.
pp
ppf
xi
let
pp_item
ppf
(
s
,
t
)
=
Format
.
fprintf
ppf
"%s : %a"
s
Var
.
Set
.
pp
t
in
Ident
.
pp_idmap
pp_item
ppf
xi
let
pp_env
ppf
env
=
Format
.
fprintf
ppf
"{vars=%a,sigma=%a,
gamma=%a,
xi=%a}"
Format
.
fprintf
ppf
"{vars=%a,sigma=%a,xi=%a}"
pp_vars
env
.
vars
Lambda
.
Print
.
pp_sigma
env
.
sigma
pp_gamma
env
.
gamma
pp_xi
env
.
xi
let
global_size
env
=
env
.
global_size
...
...
@@ -34,7 +31,6 @@ let mk cu = {
cu
=
cu
;
vars
=
Env
.
empty
;
sigma
=
Lambda
.
Identity
;
gamma
=
IdMap
.
empty
;
xi
=
IdMap
.
empty
;
stack_size
=
0
;
max_stack
=
ref
0
;
...
...
@@ -126,8 +122,8 @@ let rec comp s1 s2 = match s1, s2 with
(* from intermediate explicitely typed language to Evaluation language (lambda) *)
(* Typed -> Lambda *)
let
rec
compile
env
e
=
compile_aux
env
e
.
Typed
.
exp_descr
and
compile_aux
env
=
function
let
rec
compile
env
e
=
compile_aux
env
e
.
Typed
.
exp_typ
e
.
Typed
.
exp_descr
and
compile_aux
env
te
=
function
|
Typed
.
Forget
(
e
,_
)
->
compile
env
e
|
Typed
.
Check
(
t0
,
e
,
t
)
->
let
d
=
Patterns
.
Compile
.
make_checker
!
t0
(
Types
.
descr
t
)
in
...
...
@@ -135,7 +131,7 @@ and compile_aux env = function
|
Typed
.
Var
x
->
Var
(
find
x
env
)
|
Typed
.
TVar
x
->
let
v
=
find
x
env
in
let
ts
=
Types
.
all_vars
(
Types
.
descr
(
IdMap
.
assoc
x
env
.
gamma
))
in
let
ts
=
Types
.
all_vars
te
in
let
is_mono
x
=
if
Var
.
Set
.
is_empty
ts
then
true
else
let
from_xi
=
try
IdMap
.
assoc
x
env
.
xi
with
Not_found
->
Var
.
Set
.
empty
in
...
...
@@ -184,7 +180,7 @@ and compile_aux env = function
|
[]
->
[]
in
Op
(
op
,
aux
args
)
|
Typed
.
NsTable
(
ns
,
e
)
->
NsTable
(
ns
,
compile_aux
env
e
)
NsTable
(
ns
,
compile_aux
env
te
e
)
and
compile_abstr
env
a
=
let
fun_env
,
fun_name
=
...
...
@@ -234,7 +230,6 @@ and compile_abstr env a =
let
slots
=
Array
.
of_list
(
List
.
rev
slots
)
in
let
env
=
{
env
with
vars
=
fun_env
;
gamma
=
IdMap
.
merge
(
fun
_
v2
->
v2
)
env
.
gamma
fun_name
;
stack_size
=
0
;
max_stack
=
ref
0
}
in
...
...
@@ -254,9 +249,6 @@ and compile_branches env (brs : Typed.branches) =
(* Don't compile unused branches, because they have not been type checked. *)
let
used
=
List
.
filter
(
fun
br
->
br
.
Typed
.
br_used
)
brs
.
Typed
.
br_branches
in
let
b
=
List
.
map
(
compile_branch
env
)
used
in
(* here I need to pull type information from each pattern and then
* compute for each variable gamma(x) . I should be able to compute gamma(x)
* using the information computed in (disp,rhs) *)
let
(
disp
,
rhs
)
=
Patterns
.
Compile
.
make_branches
brs
.
Typed
.
br_typ
b
in
{
brs_stack_pos
=
env
.
stack_size
;
brs_accept_chars
=
not
(
Types
.
Char
.
is_empty
brs
.
Typed
.
br_accept
);
...
...
@@ -264,14 +256,11 @@ and compile_branches env (brs : Typed.branches) =
brs_rhs
=
rhs
}
(* p_i / t_i -> br.Typed.br_pat / br.Typed.br_type
* p_i / t_i is used here to add elements to env.gamma *)
(* p_i / t_i -> br.Typed.br_pat / br.Typed.br_type *)
and
compile_branch
env
br
=
let
env
=
List
.
fold_left
enter_local
env
(
Patterns
.
fv
br
.
Typed
.
br_pat
)
in
let
m
=
Patterns
.
filter
(
Types
.
descr
(
Patterns
.
accept
br
.
Typed
.
br_pat
))
br
.
Typed
.
br_pat
in
let
env
=
{
env
with
gamma
=
IdMap
.
merge
(
fun
_
v2
->
v2
)
env
.
gamma
m
;
xi
=
IdMap
.
merge
(
fun
_
v2
->
v2
)
env
.
xi
br
.
Typed
.
br_vars_poly
}
in
...
...
@@ -343,28 +332,12 @@ let run_show ~run ~show tenv cenv codes ids =
let
let_decl
~
run
~
show
(
tenv
,
cenv
,
codes
)
p
e
=
let
(
tenv
,
decl
,
ids
)
=
Typer
.
type_let_decl
tenv
p
e
in
let
(
cenv
,
code
)
=
compile_let_decl
cenv
decl
in
(* XXX I've the impression I'm duplicating information here
* as cenv.gamma == tenv.gamma *)
let
cenv
=
{
cenv
with
gamma
=
List
.
fold_left
(
fun
acc
(
id
,
t
)
->
(* an old binding is showed by a new one *)
IdMap
.
add
id
(
Types
.
cons
t
)
(
IdMap
.
remove
id
acc
)
)
cenv
.
gamma
ids
;
}
in
run_show
~
run
~
show
tenv
cenv
code
ids
;
(
tenv
,
cenv
,
List
.
rev_append
code
codes
)
let
let_funs
~
run
~
show
(
tenv
,
cenv
,
codes
)
funs
=
let
(
tenv
,
funs
,
ids
)
=
Typer
.
type_let_funs
tenv
funs
in
let
(
cenv
,
code
)
=
compile_rec_funs
cenv
funs
in
let
cenv
=
{
cenv
with
gamma
=
List
.
fold_left
(
fun
acc
(
id
,
t
)
->
(* an old binding is showed by a new one *)
IdMap
.
add
id
(
Types
.
cons
t
)
(
IdMap
.
remove
id
acc
)
)
cenv
.
gamma
ids
;
}
in
run_show
~
run
~
show
tenv
cenv
code
ids
;
(
tenv
,
cenv
,
List
.
rev_append
code
codes
)
...
...
parser/ast.ml
View file @
fc179124
...
...
@@ -105,7 +105,6 @@ and branches = (ppat * pexpr) list
and
ppat
=
ppat'
located
and
ppat'
=
|
TVar
of
U
.
t
(** polymorphic type variables *)
|
PatVar
of
U
.
t
list
|
Cst
of
pexpr
|
NsT
of
U
.
t
...
...
parser/parser.ml
View file @
fc179124
...
...
@@ -25,7 +25,7 @@ module Gram = Camlp4.Struct.Grammar.Static.Make(Ulexer)
let
id_dummy
=
U
.
mk
"$$$"
let
ident
s
=
let
ident
_aux
s
=
let
b
=
Buffer
.
create
(
String
.
length
s
)
in
let
rec
aux
i
=
if
(
i
=
String
.
length
s
)
then
Buffer
.
contents
b
...
...
@@ -35,8 +35,8 @@ let ident s =
in
aux
0
let
label
s
=
U
.
mk
(
ident
s
)
let
ident
s
=
U
.
mk
(
ident
s
)
let
label
s
=
U
.
mk
(
ident
_aux
s
)
let
ident
s
=
U
.
mk
(
ident
_aux
s
)
let
prog
=
Gram
.
Entry
.
mk
"prog"
let
top_phrases
=
Gram
.
Entry
.
mk
"toplevel phrases"
...
...
@@ -596,17 +596,17 @@ EXTEND Gram
located_ident
:
[
[
a
=
ident_or_keyword
->
(
lop
_loc
,
ident
a
)
]
];
pat
:
[
[
x
=
pat
;
"where"
;
b
=
LIST1
[
(
la
,
a
)
=
located_ident
;
"="
;
y
=
pat
->
(
la
,
a
,
y
)
]
SEP
"and"
->
mk
_loc
(
Recurs
(
x
,
b
))
]
[
x
=
pat
;
"where"
;
b
=
LIST1
[
(
la
,
a
)
=
located_ident
;
"="
;
y
=
pat
->
(
la
,
a
,
y
)
]
SEP
"and"
->
mk
_loc
(
Recurs
(
x
,
b
))
]
|
RIGHTA
[
x
=
pat
;
"->"
;
y
=
pat
->
mk
_loc
(
Arrow
(
x
,
y
))
|
x
=
pat
;
"@"
;
y
=
pat
->
mk
_loc
(
Concat
(
x
,
y
))
|
x
=
pat
;
"+"
;
y
=
pat
->
mk
_loc
(
Merge
(
x
,
y
))
]
|
"no_arrow"
[
x
=
pat
;
"|"
;
y
=
pat
->
mk
_loc
(
Or
(
x
,
y
))
]
|
"simple"
[
x
=
pat
;
"&"
;
y
=
pat
->
mk
_loc
(
And
(
x
,
y
))
|
x
=
pat
;
"
\\
"
;
y
=
pat
->
mk
_loc
(
Diff
(
x
,
y
))
]
|
"var_typ"
[
x
=
PTYPE
->
mk
_loc
(
TVar
(
ident
x
))
]
|
"var_typ"
[
x
=
PTYPE
->
mk
_loc
(
Internal
(
Types
.
var
(
Var
.
mk
(
ident_aux
x
))))
]
|
[
"{"
;
r
=
record_spec
;
"}"
->
r
|
"ref"
;
p
=
pat
->
...
...
parser/ulexer.ml
View file @
fc179124
...
...
@@ -186,6 +186,8 @@ let regexp qname = (ncname ':')? ncname
(* Should be [^ xml_letter ] *)
let
regexp
not_xml_letter
=
[
^
'
A'
-
'
Z'
'
a'
-
'
z'
'
0
'
-
'
9
'
'
_'
]
let
regexp
character
=
_
|
'\\'
[
'\\'
'
"' '
\'
'] | "
\\
n
" | "
\\
t
" | "
\\
r
"
| '
\\
' 'x' ['0'-'9' 'a'-'f' 'A'-'F']+ ';' | '
\\
' ['0'-'9']+ ';'
let illegal lexbuf =
error
...
...
@@ -226,7 +228,7 @@ let rec token = lexer
string
(
L
.
lexeme_start
lexbuf
)
'
"' lexbuf;
let s = get_stored_string () in
return_loc start (L.lexeme_end lexbuf) (STRING s)
|
"'"
"
\\
"
?
_
"'"
->
| "
'
"
character
"
'
" ->
L.rollback lexbuf;
(fun _ -> lexer
| "
'
" -> let start = L.lexeme_start lexbuf in
...
...
@@ -280,7 +282,7 @@ and token2 = lexer
string (L.lexeme_start lexbuf) '"' lexbuf;
let s = get_stored_string () in
return_loc start (L.lexeme_end lexbuf) (STRING s)
|
"'"
"
\\
"
?
_
"'--'"
"
\\
"
?
_
"'"
| "'"
character "'--'" character
"'"
| "'" [^ '\'']+ "'" not_xml_letter ->
L.rollback lexbuf;
(fun _ -> lexer
...
...
@@ -345,7 +347,7 @@ and token2toplevel = lexer
string (L.lexeme_start lexbuf) '"' lexbuf;
let s = get_stored_string () in
return_loc start (L.lexeme_end lexbuf) (STRING s)
|
"'"
"
\\
"
?
_
"'--'"
"
\\
"
?
_
"'"
| "'"
character "'--'" character
"'"
| "'" ((";"[^ ";'"]) | [^ ";'"])* ";"? "'" not_xml_letter ->
L.rollback lexbuf;
(fun _ -> lexer
...
...
tests/libtest/tallyingTest.ml
View file @
fc179124
...
...
@@ -61,8 +61,8 @@ let mk_union_res l1 l2 =
(* check invariants on the constraints sets *)
let
mk_pp
=
function
|
P
(
V
alpha
,
t
)
->
Tallying
.
CS
.
singleton
Var
.
Set
.
empty
(
Tallying
.
Pos
(
Var
.
mk
alpha
,
parse_typ
t
))
|
N
(
t
,
V
alpha
)
->
Tallying
.
CS
.
singleton
Var
.
Set
.
empty
(
Tallying
.
Neg
(
parse_typ
t
,
Var
.
mk
alpha
))
|
P
(
V
alpha
,
t
)
->
Tallying
.
CS
.
singleton
(
Tallying
.
Pos
(
Var
.
mk
alpha
,
parse_typ
t
))
|
N
(
t
,
V
alpha
)
->
Tallying
.
CS
.
singleton
(
Tallying
.
Neg
(
parse_typ
t
,
Var
.
mk
alpha
))
let
mk_prod
l
=
List
.
fold_left
(
fun
acc
c
->
...
...
@@ -339,8 +339,9 @@ let test_tallying =
let
s_sigma
=
Tallying
.(
s
$$
sigma
)
in
let
t_sigma
=
Tallying
.(
t
$$
sigma
)
in
assert_equal
~
pp_diff
:
(
fun
fmt
_
->
Format
.
fprintf
fmt
"s @ sigma_i = %a
\n
"
Types
.
Print
.
pp_type
s_sigma
;
Format
.
fprintf
fmt
"t @ sigma_i = %a
\n
"
Types
.
Print
.
pp_type
t_sigma
Format
.
fprintf
fmt
"sigma_i = %a
\n
"
Types
.
Tallying
.
CS
.
pp_e
sigma
;
Format
.
fprintf
fmt
"s @@ sigma_i = %a
\n
"
Types
.
Print
.
pp_type
s_sigma
;
Format
.
fprintf
fmt
"t @@ sigma_i = %a
\n
"
Types
.
Print
.
pp_type
t_sigma
)
(
Types
.
subtype
s_sigma
t_sigma
)
true
)
sigma
)
l
...
...
types/builtin.mli
View file @
fc179124
(* Typing environment with built-in types *)
val
env
:
Typer
.
t
(* Typing environment with built-in types *)
val
argv
:
Value
.
t
ref
types/ident.ml
View file @
fc179124
...
...
@@ -22,9 +22,9 @@ type label = Ns.Label.t
type
'
a
label_map
=
'
a
LabelMap
.
map
let
pp_env
f
ppf
env
=
let
f
ppf
(
e
,
v
)
=
Format
.
fprintf
ppf
"%a:%a"
p
rin
t
e
f
v
in
let
f
ppf
(
e
,
v
)
=
f
ppf
((
Id
.
to_st
rin
g
e
)
,
v
)
in
Utils
.
pp_list
~
delim
:
(
"<"
,
">"
)
~
sep
:
";"
f
ppf
(
Env
.
bindings
env
)
let
pp_idmap
f
ppf
map
=
let
f
ppf
(
e
,
v
)
=
Format
.
fprintf
ppf
"%a:%a"
p
rin
t
e
f
v
in
let
f
ppf
(
e
,
v
)
=
f
ppf
((
Id
.
to_st
rin
g
e
)
,
v
)
in
Utils
.
pp_list
~
delim
:
(
"<"
,
">"
)
~
sep
:
";"
f
ppf
(
IdMap
.
get
map
)
types/types.ml
View file @
fc179124
...
...
@@ -2629,6 +2629,39 @@ module Positive = struct
]
and
v
=
{
mutable
def
:
rhs
;
mutable
node
:
node
option
}
module
MemoHash
=
Hashtbl
.
Make
(
struct
type
t
=
v
let
hash
=
Hashtbl
.
hash
let
equal
u
v
=
u
==
v
end
)
let
pp
ppf
v
=
let
id
=
ref
0
in
let
memo
=
MemoHash
.
create
17
in
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
;
MemoHash
.
add
memo
v
node_name
;
match
v
.
def
with
|
`Type
d
->
Format
.
fprintf
ppf
"`Type(%a)"
Print
.
pp_type
d
|
`Variable
d
->
Format
.
fprintf
ppf
"`Var(%a)"
Var
.
pp
d
|
`Cup
vl
->
Format
.
fprintf
ppf
"`Cup(%a)"
(
Utils
.
pp_list
aux
)
vl
|
`Cap
vl
->
Format
.
fprintf
ppf
"`Cap(%a)"
(
Utils
.
pp_list
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
ppf
v
let
printf
=
pp
Format
.
std_formatter
let
rec
make_descr
seen
v
=
if
List
.
memq
v
seen
then
empty
else
...
...
@@ -2675,17 +2708,17 @@ module Positive = struct
let
decompose
t
=
let
memo
=
DescrHash
.
create
17
in
let
decompose_conj
f_atom
sign
ilist
acc
=
let
decompose_conj
acc
f_atom
sign
ilist
acc
=
List
.
fold_left
(
fun
acc
e
->
let
ne
=
f_atom
e
in
(
sign
ne
)
::
acc
)
acc
ilist
(
sign
ne
)
::
acc
)
acc
ilist
in
let
decompose_dnf
t_any
f_atom
dnf
acc
=
List
.
fold_left
(
fun
acc
(
ipos
,
ineg
)
->
match
decompose_conj
f_atom
neg
ineg
@@
decompose_conj
f_atom
(
fun
x
->
x
)
ipos
[
t_any
]
with
let
lacc
=
decompose_conj
[]
f_atom
neg
ineg
in
let
lacc
=
decompose_conj
lacc
f_atom
(
fun
x
->
x
)
ipos
[
t_any
]
in
match
lacc
with
|
[
v
]
->
v
::
acc
|
l
->
(
cap
l
)
::
acc
)
acc
dnf
in
...
...
@@ -2713,102 +2746,61 @@ module Positive = struct
cup
(
decompose_dnf
(
ty
any
)
(
fun
(
b
,
l
)
->
make
b
(
format_rec
b
[]
(
LabelMap
.
get
l
)))
(
Rec
.
get
bdd
)
[]
))
dnf
acc
and
decompose_type
t
=
try
DescrHash
.
find
memo
t
with
Not_found
->
let
node_t
=
forward
()
in
if
no_var
t
then
ty
t
else
let
()
=
DescrHash
.
add
memo
t
node_t
in
let
descr_t
=
decompose_kind
Atom
.
any
atom
(
BoolAtoms
.
get
t
.
atoms
)
@@
decompose_kind
Int
.
any
interval
(
BoolIntervals
.
get
t
.
ints
)
@@
decompose_kind
Char
.
any
char
(
BoolChars
.
get
t
.
chars
)
@@
decompose_bdd
Product
.
any
times
(
BoolPair
.
get
t
.
times
)
@@
decompose_bdd
Product
.
any_xml
xml
(
BoolPair
.
get
t
.
xml
)
@@
decompose_bdd
Arrow
.
any
arrow
(
BoolPair
.
get
t
.
arrow
)
@@
decompose_rec
Record
.
any
record
(
BoolRec
.
get
t
.
record
)
@@
decompose_kind
Abstract
.
any
abstract
(
BoolAbstracts
.
get
t
.
abstract
)
[]
in
node_t
.
def
<-
(
cup
descr_t
)
.
def
;
node_t
try
DescrHash
.
find
memo
t
with
Not_found
->
let
node_t
=
forward
()
in
if
no_var
t
then
ty
t
else
let
()
=
DescrHash
.
add
memo
t
node_t
in
let
descr_t
=
decompose_kind
Atom
.
any
atom
(
BoolAtoms
.
get
t
.
atoms
)
@@
decompose_kind
Int
.
any
interval
(
BoolIntervals
.
get
t
.
ints
)
@@
decompose_kind
Char
.
any
char
(
BoolChars
.
get
t
.
chars
)
@@
decompose_bdd
Product
.
any
times
(
BoolPair
.
get
t
.
times
)
@@
decompose_bdd
Product
.
any_xml
xml
(
BoolPair
.
get
t
.
xml
)
@@
decompose_bdd
Arrow
.
any
arrow
(
BoolPair
.
get
t
.
arrow
)
@@
decompose_rec
Record
.
any
record
(
BoolRec
.
get
t
.
record
)
@@
decompose_kind
Abstract
.
any
abstract
(
BoolAbstracts
.
get
t
.
abstract
)
[]
in
node_t
.
def
<-
(
cup
descr_t
)
.
def
;
node_t
in
decompose_type
t
let
solve
v
=
internalize
(
make_node
v
)
module
MemoHash
=
Hashtbl
.
Make
(
struct
type
t
=
v
let
hash
=
Hashtbl
.
hash
let
equal
u
v
=
u
==
v
end
)
let
substitute_aux
delta
v
subst
=
let
memo
=
MemoHash
.
create
17
in
let
rec
aux
v
subst
=
try
MemoHash
.
find
memo
v
with
Not_found
->
begin
let
node_v
=
forward
()
in
MemoHash
.
add
memo
v
node_v
;
let
new_v
=
match
v
.
def
with
|
`Type
d
->
`Type
d
|
`Variable
d
when
Var
.
Set
.
mem
d
delta
->
v
.
def
|
`Variable
d
->
(
subst
d
)
.
def
|
`Cup
vl
->
`Cup
(
List
.
map
(
fun
v
->
aux
v
subst
)
vl
)
|
`Cap
vl
->
`Cap
(
List
.
map
(
fun
v
->
aux
v
subst
)
vl
)
|
`Times
(
v1
,
v2
)
->
`Times
(
aux
v1
subst
,
aux
v2
subst
)
|
`Arrow
(
v1
,
v2
)
->
`Arrow
(
aux
v1
subst
,
aux
v2
subst
)
|
`Xml
(
v1
,
v2
)
->
`Xml
(
aux
v1
subst
,
aux
v2
subst
)
|
`Record
(
b
,
flst
)
->
`Record
(
b
,
List
.
map
(
fun
(
b
,
l
,
v
)
->
(
b
,
l
,
aux
v
subst
))
flst
)
|
`Neg
v
->
`Neg
(
aux
v
subst
)
in
node_v
.
def
<-
new_v
;
node_v
end
in
aux
v
subst
let
pp
ppf
v
=
let
id
=
ref
0
in
let
memo
=
MemoHash
.
create
17
in
let
rec
aux
ppf
v
=
try
let
s
=
MemoHash
.
find
memo
v
in
Format
.
fprintf
ppf
"%s"
s
try
MemoHash
.
find
memo
v
with
Not_found
->
begin
let
node_name
=
Printf
.
sprintf
"X_%i"
!
id
in
incr
id
;
MemoHash
.
add
memo
v
node_name
;
match
v
.
def
with
|
`Type
d
->
Format
.
fprintf
ppf
"`Type(%a)"
Print
.
pp_type
d
|
`Variable
d
->
Format
.
fprintf
ppf
"`Var(%a)"
Var
.
pp
d
|
`Cup
vl
->
Format
.
fprintf
ppf
"`Cup(%a)"
(
Utils
.
pp_list
aux
)
vl
|
`Cap
vl
->
Format
.
fprintf
ppf
"`Cap(%a)"
(
Utils
.
pp_list
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
let
node_v
=
forward
()
in
MemoHash
.
add
memo
v
node_v
;
let
new_v
=
match
v
.
def
with
|
`Type
d
->
`Type
d
|
`Variable
d
when
Var
.
Set
.
mem
d
delta
->
v
.
def
|
`Variable
d
->
(
subst
d
)
.
def
|
`Cup
vl
->
`Cup
(
List
.
map
(
fun
v
->
aux
v
subst
)
vl
)
|
`Cap
vl
->
`Cap
(
List
.
map
(
fun
v
->
aux
v
subst
)
vl
)
|
`Times
(
v1
,
v2
)
->
`Times
(
aux
v1
subst
,
aux
v2
subst
)
|
`Arrow
(
v1
,
v2
)
->
`Arrow
(
aux
v1
subst
,
aux
v2
subst
)
|
`Xml
(
v1
,
v2
)
->
`Xml
(
aux
v1
subst
,
aux
v2
subst
)
|
`Record
(
b
,
flst
)
->
`Record
(
b
,
List
.
map
(
fun
(
b
,
l
,
v
)
->
(
b
,
l
,
aux
v
subst
))
flst
)
|
`Neg
v
->
`Neg
(
aux
v
subst
)
in
node_v
.
def
<-
new_v
;
node_v
end
in
aux
ppf
v
let
printf
=
pp
Format
.
std_formatter
let
dump
ppf
t
=
pp
ppf
(
decompose
t
)
aux
v
subst
(* returns a recursive type where all occurrences of alpha n t
* are substituted with a recursive variable X *)
let
substituterec
t
alpha
=
let
subst
x
d
=
if
Var
.
equal
d
alpha
then
x
else
var
d
in
if
no_var
t
then
t
else
begin
let
subst
x
d
=
if
Var
.
equal
d
alpha
then
x
else
var
d
in
let
x
=
forward
()
in
define
x
(
substitute_aux
Var
.
Set
.
empty
(
decompose
t
)
(
subst
x
));
descr
(
solve
x
)
...
...
@@ -2823,16 +2815,13 @@ module Positive = struct
descr
(
solve
new_t
)
end
let
substitutefree
delta
=
let
idx
=
ref
0
in
fun
t
->
if
no_var
t
then
t
else
let
substitutefree
delta
t
=
if
no_var
t
then
t
else
let
h
=
Hashtbl
.
create
17
in
let
subst
h
d
=
try
Hashtbl
.
find
h
d
with
Not_found
->
begin
let
id
=
Printf
.
sprintf
"_%s_%d"
(
Var
.
id
d
)
!
idx
in
let
x
=
var
(
Var
.
mk
~
repr
:
(
Var
.
id
d
)
id
)
in
incr
idx
;
let
x
=
var
(
Var
.
fresh
d
)
in
Hashtbl
.
add
h
d
x
;
x
end
...
...
@@ -2844,7 +2833,7 @@ module Positive = struct
(* 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.
*)
latter but the variance annotation tells us that A is invariant. *)
let
collect_variables
delta
v
=
(* we memoize based on the pair (pos, v), since v can occur both
positively and negatively. and we want to manage the variables
...
...
@@ -2871,20 +2860,25 @@ module Positive = struct
let
t_emp
=
cup
[]
in
let
t_any
=
cap
[]
in
let
idx
=
ref
0
in
let
is_internal
x
=
let
s
=
Var
.
id
x
in
String
.
length
s
>=
1
&&
s
.
[
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
when
Var
.
Set
.
mem
d
delta
||
(
not
(
Var
.
is_internal
d
)
&&
not
pos
)
->
Hashtbl
.
replace
vars
d
v
|
`Variable
d
when
Var
.
Set
.
mem
d
delta
||
(
not
(
is_internal
d
)
&&
not
pos
)
->
Hashtbl
.
replace
vars
d
v
|
`Variable
d
->
begin
try
let
td
=
Hashtbl
.
find
vars
d
in
(* polarity conflict, replace the binding by a new, pretty-printed variable *)
if
((
td
==
t_emp
)
&&
not
pos
)
||
((
td
==
t_any
)
&&
pos
)
then
Hashtbl
.
replace
vars
d
(
var
(
freshvar
idx
))
(* first time we see a variable, set to empty for covariant and
any for contravariant *)
(* 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
)
...
...
@@ -2913,6 +2907,7 @@ module Positive = struct
if
no_var
t
then
t
else
clean_variables
delta
t
let
dump
ppf
t
=
pp
ppf
(
decompose
t
)
end
...
...
@@ -2929,9 +2924,10 @@ module Tallying = struct
(* we require that types are semantically equivalent and not structurally
* equivalent *)
let
semantic_compare
t1
t2
=
if
Descr
.
equal
t1
t2
then
0
else
if
equiv
t1
t2
then
0
else
Descr
.
compare
t1
t2
let
c
=
Descr
.
compare
t1
t2
in
if
c
=
0
then
0
else
if
equiv
t1
t2
then
0
else
c
(* constraint set : map to store constraints of the form (s <= alpha <= t) *)
module
M
=
struct
...
...
@@ -2980,14 +2976,7 @@ module Tallying = struct
Not_found
->
inf
,
sup
in
if
Var
.
Set
.
mem
v
delta
then
map
(* if ((equal inf empty) && (equal sup any)) ||
(equal (var v) inf && equal (var v) sup) then
map
else
raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v)))
*)
else
VarMap
.
add
v
(
new_i
,
new_s
)
map
else
VarMap
.
add
v
(
new_i
,
new_s
)
map
let
inter
delta
map1
map2
=
VarMap
.
fold
(
add
delta
)
map1
map2
let
fold
=
VarMap
.
fold
...
...
@@ -2996,7 +2985,7 @@ module Tallying = struct
end
(* equation set : (s < alpha < t) stored as
*
{ alpha -> ((s v beta) ^ t) } with beta fresh *)
{ alpha -> ((s v beta) ^ t) } with beta fresh *)
module
E
=
struct
include
Map
.
Make
(
struct
type
t
=
Var
.
var
...
...
@@ -3004,9 +2993,9 @@ module Tallying = struct
end
)
let
pp
ppf
e
=
Utils
.
pp_list
~
delim
:
(
"{"
,
"}"
)
(
fun
ppf
->
fun
(
v
,
t
)
->
Format
.
fprintf
ppf
"%a = %a@,"
Var
.
pp
v
Print
.
pp_type
t
)
ppf
(
bindings
e
)
Utils
.
pp_list
~
delim
:
(
"{"
,
"}"
)
(
fun
ppf
->
fun
(
v
,
t
)
->
Format
.
fprintf
ppf
"%a = %a@,"
Var
.
pp
v
Print
.
pp_type
t
)
ppf
(
bindings
e
)
end
...
...
@@ -3401,11 +3390,11 @@ module Tallying = struct
let
solve
delta
s
=
let
aux
alpha
(
s
,
t
)
acc
=
(* we cannot solve twice the same variable *)
(* we cannot solve twice the same variable *)
assert
(
not
(
CS
.
E
.
mem
alpha
acc
));
let
pre
=
Printf
.
sprintf
"#fr_%s
_
"
(
Var
.
id
alpha
)
in
let
b
=
var
(
Var
.
fresh