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
0b1961d9
Commit
0b1961d9
authored
Jul 07, 2014
by
Kim Nguyễn
Browse files
Cosmetic changes.
parent
f93a6ba1
Changes
2
Hide whitespace changes
Inline
Side-by-side
types/types.ml
View file @
0b1961d9
...
...
@@ -150,7 +150,7 @@ module TLV = struct
else
if
p1
then
1
else
-
1
else
c
end
)
let
pp_aux
ppf
pp_elem
s
=
let
pp_aux
ppf
pp_elem
s
=
let
f
ppf
=
function
|
(
v
,
true
)
->
Format
.
fprintf
ppf
"%a"
pp_elem
v
|
(
v
,
false
)
->
Format
.
fprintf
ppf
"~ %a"
pp_elem
v
...
...
@@ -385,7 +385,7 @@ end
and
Pair
:
Bool
.
S
with
type
elem
=
(
Node
.
t
*
Node
.
t
)
=
Bool
.
Make
(
Custom
.
Pair
(
Node
)(
Node
))
and
BoolPair
:
BoolVar
.
S
with
type
s
=
Pair
.
t
=
and
BoolPair
:
BoolVar
.
S
with
type
s
=
Pair
.
t
=
BoolVar
.
Make
(
Pair
)
(* bool = true means that the record is open that is, that
...
...
@@ -1675,7 +1675,7 @@ struct
|
`None
|
`Marked
|
`GlobalName
of
gname
|
`Named
of
U
.
t
]
|
`Named
of
U
.
t
]
}
and
d
=
|
Name
of
gname
...
...
@@ -1789,7 +1789,7 @@ struct
alloc
[
Neg
(
prepare
(
neg
d
))]
else
let
slot
=
alloc
[]
in
if
not
(
worth_abbrev
d
)
then
if
not
(
worth_abbrev
d
)
then
slot
.
state
<-
`Expand
;
DescrHash
.
add
memo
d
slot
;
...
...
@@ -1805,7 +1805,7 @@ struct
(*
alpha ^ ( union )
alpha / ( union ) only if alpha is not present in at most 2
alpha / ( union ) only if alpha is not present in at most 2
*)
let
prepare_boolvar
get
is_full
print
tlv
bdd
=
...
...
@@ -1930,7 +1930,7 @@ struct
slot
and
decompile
d
=
let
aux
t
=
let
aux
t
=
let
tr
=
Product
.
get
t
in
let
tr
=
Product
.
merge_same_first
tr
in
let
tr
=
Product
.
clean_normal
tr
in
...
...
@@ -2008,9 +2008,9 @@ struct
|
[
h
]
->
(
do_print
pri
)
ppf
h
|
h
::
t
->
Format
.
fprintf
ppf
"%a %s@ %a"
(
do_print
pri
)
h
sep
aux
t
in
if
(
pri
>=
2
)
&&
(
List
.
length
def
>=
2
)
then
if
(
pri
>=
2
)
&&
(
List
.
length
def
>=
2
)
then
Format
.
fprintf
ppf
"@[(%a)@]"
aux
def
else
else
aux
ppf
def
and
do_print
pri
ppf
=
function
...
...
@@ -2154,7 +2154,7 @@ struct
let
string_of_type
t
=
Utils
.
string_of_formatter
pp_type
t
let
string_of_node
t
=
Utils
.
string_of_formatter
pp_node
t
let
printf
=
pp_type
Format
.
std_formatter
let
printf
=
pp_type
Format
.
std_formatter
end
...
...
@@ -2525,7 +2525,7 @@ module Positive = struct
@@
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_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
...
...
@@ -2677,7 +2677,7 @@ module Positive = struct
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
)
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 *)
...
...
@@ -2965,7 +2965,7 @@ module Tallying = struct
let
union
=
S
.
union
let
prod
delta
=
S
.
inter
delta
let
merge
delta
=
M
.
inter
delta
let
merge
delta
=
M
.
inter
delta
end
let
normatoms
(
t
,_,_
)
=
if
Atoms
.
is_empty
t
then
CS
.
sat
else
CS
.
unsat
...
...
@@ -2985,7 +2985,7 @@ module Tallying = struct
let
t
=
cap
(
aux
id
constr
p
)
(
aux
neg
constr
n
)
in
(* t = bigdisj ... alpha \in P --> alpha <= neg t *)
(* t = bigdisj ... alpha \in N --> t <= alpha *)
if
b
then
(
neg
t
)
else
t
if
b
then
(
neg
t
)
else
t
let
single_atoms
=
single_aux
atom
...
...
@@ -3242,9 +3242,9 @@ module Tallying = struct
let
x
=
Positive
.
substituterec
t
alpha
in
(* Format.printf "X = %a %a %a\n" Var.pp alpha Print.print x dump t; *)
let
es
=
CS
.
E
.
fold
(
fun
beta
s
acc
->
CS
.
E
.
fold
(
fun
beta
s
acc
->
CS
.
E
.
add
beta
(
Positive
.
substitute
s
(
alpha
,
x
))
acc
)
e1
CS
.
E
.
empty
)
e1
CS
.
E
.
empty
in
(* Format.printf "es = %a\n" CS.print_e es; *)
aux
((
CS
.
E
.
add
alpha
x
sol
))
es
...
...
typing/typer.ml
View file @
0b1961d9
...
...
@@ -964,8 +964,8 @@ and type_check' loc env ed constr precise = match ed with
let
dom
=
Types
.
Arrow
.
domain
(
t1arrow
)
in
let
t2
=
type_check
env
e2
Types
.
any
true
in
let
res
=
if
not
(
Types
.
is_closed
env
.
delta
dom
)
||
not
(
Types
.
is_closed
env
.
delta
t2
)
then
if
not
(
Types
.
is_closed
env
.
delta
dom
)
||
not
(
Types
.
is_closed
env
.
delta
t2
)
then
(* get t2 without constraint check *)
let
(
sl
,
res
)
=
(* s [_delta dom(t) *)
...
...
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