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
7c04c5ae
Commit
7c04c5ae
authored
Jun 26, 2014
by
Pietro Abate
Browse files
Minor refactoring and API Change Var.print -> Var.pp
parent
53b9e879
Changes
4
Hide whitespace changes
Inline
Side-by-side
types/types.ml
View file @
7c04c5ae
...
...
@@ -153,8 +153,8 @@ module TLV = struct
end
)
let
print
sep
ppf
s
=
let
aux1
ppf
=
function
|
(
v
,
true
)
->
Format
.
fprintf
ppf
"%a"
Var
.
p
rint
v
|
(
v
,
false
)
->
Format
.
fprintf
ppf
"~ %a"
Var
.
p
rint
v
|
(
v
,
true
)
->
Format
.
fprintf
ppf
"%a"
Var
.
p
p
v
|
(
v
,
false
)
->
Format
.
fprintf
ppf
"~ %a"
Var
.
p
p
v
in
let
rec
aux
ppf
=
function
|
[]
->
()
...
...
@@ -198,7 +198,7 @@ module TLV = struct
let
print
ppf
x
=
Set
.
print
";"
ppf
x
.
tlv
let
dump
ppf
x
=
Format
.
fprintf
ppf
"<fv = {%a} ; tlv = {%a}>"
Var
.
Set
.
p
rint
x
.
fv
(
Set
.
print
";"
)
x
.
tlv
Var
.
Set
.
p
p
x
.
fv
(
Set
.
print
";"
)
x
.
tlv
let
mem
v
x
=
Set
.
mem
v
x
.
tlv
end
...
...
@@ -1803,7 +1803,7 @@ struct
let
(
_
,
l1
)
=
List
.
fold_left
(
fun
(
has_tlv
,
acc
)
->
function
|
(
`Var
v
)
as
x
when
(
TLV
.
mem
(
x
,
true
)
tlv
)
->
(
true
,
acc
)
|
(
`Var
v
)
as
x
->
(
has_tlv
,
(
Atomic
(
fun
ppf
->
Var
.
p
rint
ppf
x
))
::
acc
)
|
(
`Var
v
)
as
x
->
(
has_tlv
,
(
Atomic
(
fun
ppf
->
Var
.
p
p
ppf
x
))
::
acc
)
|
`Atm
bdd
->
begin
match
has_tlv
,
acc
with
|
true
,
[]
->
if
is_full
bdd
then
(
has_tlv
,
[]
)
else
(
has_tlv
,
print
bdd
)
...
...
@@ -1815,7 +1815,7 @@ struct
let
l2
=
List
.
fold_left
(
fun
acc
->
function
|
(
`Var
v
)
as
x
when
(
TLV
.
mem
(
x
,
false
)
tlv
)
->
acc
|
(
`Var
v
)
as
x
->
(
Atomic
(
fun
ppf
->
Format
.
fprintf
ppf
"~ %a"
Var
.
p
rint
x
))
::
acc
|
(
`Var
v
)
as
x
->
(
Atomic
(
fun
ppf
->
Format
.
fprintf
ppf
"~ %a"
Var
.
p
p
x
))
::
acc
|
`Atm
bdd
->
assert
false
)
[]
n
in
...
...
@@ -1833,8 +1833,8 @@ struct
let
l
=
TLV
.
Set
.
fold
(
fun
((
`Var
v
)
as
x
,
p
)
acc
->
let
s
=
if
p
then
(
Atomic
(
fun
ppf
->
Var
.
p
rint
ppf
x
))
else
(
Atomic
(
fun
ppf
->
Format
.
fprintf
ppf
"~ %a"
Var
.
p
rint
x
))
if
p
then
(
Atomic
(
fun
ppf
->
Var
.
p
p
ppf
x
))
else
(
Atomic
(
fun
ppf
->
Format
.
fprintf
ppf
"~ %a"
Var
.
p
p
x
))
in
s
::
acc
)
(
all_tlv
not_seq
)
[]
in
...
...
@@ -2566,7 +2566,7 @@ struct
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
.
p
rint
d
|
`Variable
d
->
Format
.
fprintf
ppf
"`Var(%a)"
Var
.
p
p
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
...
...
@@ -2626,7 +2626,7 @@ struct
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
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
=
...
...
@@ -2763,7 +2763,7 @@ module Tallying = struct
let
pp
ppf
map
=
Utils
.
pp_list
~
delim
:
(
"{"
,
"}"
)
(
fun
ppf
(
v
,
(
i
,
s
))
->
Format
.
fprintf
ppf
"%a <= %a <= %a"
Print
.
pp_type
i
Var
.
p
rint
v
Print
.
pp_type
s
Format
.
fprintf
ppf
"%a <= %a <= %a"
Print
.
pp_type
i
Var
.
p
p
v
Print
.
pp_type
s
)
ppf
(
VarMap
.
bindings
map
)
let
compare
map1
map2
=
...
...
@@ -2788,7 +2788,7 @@ module Tallying = struct
let
pp
ppf
e
=
Utils
.
pp_list
~
delim
:
(
"{"
,
"}"
)
(
fun
ppf
->
fun
(
v
,
t
)
->
Format
.
fprintf
ppf
"%a = %a@,"
Var
.
p
rint
v
Print
.
pp_type
t
Format
.
fprintf
ppf
"%a = %a@,"
Var
.
p
p
v
Print
.
pp_type
t
)
ppf
(
bindings
e
)
end
...
...
@@ -3190,14 +3190,14 @@ module Tallying = struct
if
CS
.
E
.
is_empty
e
then
sol
else
begin
let
(
alpha
,
t
)
=
CS
.
E
.
min_binding
e
in
(* Format.printf "Unify -> %a = %a\n" Var.p
rint
alpha Print.print t; *)
(* Format.printf "Unify -> %a = %a\n" Var.p
p
alpha Print.print t; *)
let
e1
=
CS
.
E
.
remove
alpha
e
in
(* Format.printf "e1 = %a\n" CS.print_e e1; *)
(* remove from E \ { (alpha,t) } every occurrences of alpha
* by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
(* substituterec remove also all previously introduced fresh variables *)
let
x
=
Positive
.
substituterec
t
alpha
in
(* Format.printf "X = %a %a %a\n" Var.p
rint
alpha Print.print x dump t; *)
(* Format.printf "X = %a %a %a\n" Var.p
p
alpha Print.print x dump t; *)
let
es
=
CS
.
E
.
fold
(
fun
beta
s
acc
->
CS
.
E
.
add
beta
(
Positive
.
substitute
s
(
alpha
,
x
))
acc
)
e1
CS
.
E
.
empty
in
(* Format.printf "es = %a\n" CS.print_e es; *)
aux
((
CS
.
E
.
add
alpha
x
sol
))
es
...
...
types/var.ml
View file @
7c04c5ae
module
V
=
struct
type
t
=
{
fresh
:
bool
;
id
:
string
;
}
let
make_id
?
(
fresh
=
false
)
id
=
{
id
=
id
;
fresh
=
fresh
}
let
dump
ppf
t
=
Format
.
fprintf
ppf
"{id=%s;fresh=%b}"
t
.
id
t
.
fresh
let
compare
x
y
=
Pervasives
.
compare
x
.
id
y
.
id
let
equal
x
y
=
Pervasives
.
compare
x
.
id
y
.
id
=
0
let
hash
x
=
Hashtbl
.
hash
x
.
id
let
check
_
=
()
let
make_id
?
(
fresh
=
false
)
id
=
{
id
=
id
;
fresh
=
fresh
}
end
type
var
=
[
`Var
of
V
.
t
]
type
'
a
pairvar
=
[
`Atm
of
'
a
|
var
]
type
t
=
var
let
dump
ppf
(
`Var
x
)
=
Format
.
fprintf
ppf
"%a"
V
.
dump
x
let
p
rint
ppf
(
`Var
x
)
=
Format
.
fprintf
ppf
"'%s"
x
.
V
.
id
let
p
p
ppf
(
`Var
x
)
=
Format
.
fprintf
ppf
"'%s"
x
.
V
.
id
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
_
=
()
let
mk
?
fresh
id
=
`Var
(
V
.
make_id
?
fresh
id
)
let
mk
?
fresh
id
=
`Var
(
V
.
make_id
?
fresh
id
)
let
fresh
:
?
pre
:
string
->
unit
->
[
>
var
]
=
let
counter
=
ref
0
in
fun
?
(
pre
=
"_fresh_"
)
->
fun
_
->
...
...
@@ -29,8 +29,8 @@ let fresh : ?pre: string -> unit -> [> var ] =
v
;;
let
id
(
`Var
t
)
=
t
.
V
.
id
let
is_fresh
(
`Var
t
)
=
t
.
V
.
fresh
let
id
(
`Var
x
)
=
x
.
V
.
id
let
is_fresh
(
`Var
x
)
=
x
.
V
.
fresh
module
Set
=
struct
include
Set
.
Make
(
struct
type
t
=
var
let
compare
=
compare
end
)
...
...
@@ -43,11 +43,12 @@ module Set = struct
aux
ppf
(
elements
s
)
let
dump
ppf
s
=
aux_print
";"
dump
ppf
s
let
p
rint
ppf
s
=
aux_print
";"
p
rint
ppf
s
let
p
p
ppf
s
=
aux_print
";"
p
p
ppf
s
let
is_empty
s
=
equal
s
empty
let
from_list
l
=
List
.
fold_left
(
fun
acc
x
->
add
x
acc
)
empty
l
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
(
X
:
Custom
.
T
)
=
struct
...
...
types/var.mli
View file @
7c04c5ae
module
V
:
sig
type
t
include
Custom
.
T
val
make_id
:
?
fresh
:
bool
->
string
->
t
val
dump
:
Format
.
formatter
->
t
->
unit
val
compare
:
t
->
t
->
int
val
equal
:
t
->
t
->
bool
val
hash
:
t
->
int
end
type
var
=
[
`Var
of
V
.
t
]
val
dump
:
Format
.
formatter
->
var
->
unit
val
print
:
Format
.
formatter
->
var
->
unit
val
compare
:
var
->
var
->
int
val
equal
:
var
->
var
->
bool
val
hash
:
var
->
int
include
Custom
.
T
with
type
t
=
var
val
pp
:
Format
.
formatter
->
var
->
unit
val
mk
:
?
fresh
:
bool
->
string
->
var
val
fresh
:
?
pre
:
string
->
unit
->
var
val
id
:
var
->
string
...
...
@@ -23,7 +16,7 @@ val is_fresh : var -> bool
module
Set
:
sig
include
Set
.
S
with
type
elt
=
var
val
dump
:
Format
.
formatter
->
t
->
unit
val
p
rint
:
Format
.
formatter
->
t
->
unit
val
p
p
:
Format
.
formatter
->
t
->
unit
val
is_empty
:
t
->
bool
val
from_list
:
elt
list
->
t
end
...
...
typing/typed.ml
View file @
7c04c5ae
...
...
@@ -188,7 +188,7 @@ module Print = struct
and
pp_fv
ppf
fv
=
Utils
.
pp_list
pp_v
ppf
fv
and
pp_vars_poly
ppf
m
=
let
pp_aux
ppf
(
x
,
s
)
=
Format
.
fprintf
ppf
"%a : %a"
Ident
.
print
x
Var
.
Set
.
p
rint
s
in
let
pp_aux
ppf
(
x
,
s
)
=
Format
.
fprintf
ppf
"%a : %a"
Ident
.
print
x
Var
.
Set
.
p
p
s
in
Utils
.
pp_list
~
sep
:
";"
pp_aux
ppf
(
Ident
.
IdMap
.
get
m
)
let
string_of_typed
=
Utils
.
string_of_formatter
pp_typed
...
...
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