Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
cduce
cduce
Commits
32448f02
Commit
32448f02
authored
May 02, 2014
by
Pietro Abate
Browse files
WIP
parent
5005c436
Changes
1
Hide whitespace changes
Inline
Sidebyside
tests/libtest/tallyingTest.ml
View file @
32448f02
...
...
@@ 46,21 +46,15 @@ end)
type
pp
=
P
of
vv
*
string

N
of
string
*
vv
and
vv
=
V
of
string
let
mk_pp
=
function

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
>
Tallying
.
CS
.
prod
(
mk_pp
c
)
acc
)
Tallying
.
CS
.
sat
l
let
mk_union
l1
l2
=
Tallying
.
CS
.
union
(
mk_prod
l1
)
(
mk_prod
l2
)
let
mk_s
ll
=
let
aux
l
=
List
.
fold_left
(
fun
acc
>
function

P
(
V
alpha
,
t
)
>
Tallying
.
CS
.
M
.
add
(
true
,
Var
.
mk
alpha
)
(
parse_typ
t
)
acc

N
(
t
,
V
alpha
)
>
Tallying
.
CS
.
M
.
add
(
false
,
Var
.
mk
alpha
)
(
parse_typ
t
)
acc
)
Tallying
.
CS
.
M
.
empty
l
in
List
.
fold_left
(
fun
acc
l
>
Tallying
.
CS
.
union
(
mk_prod
l
)
acc
Tallying
.
CS
.
S
.
add
(
aux
l
)
acc
)
Tallying
.
CS
.
S
.
empty
ll
let
mk_union_res
l1
l2
=
...
...
@@ 84,8 +78,19 @@ let mk_union_res l1 l2 =

[]
,
l2
>
(
Tallying
.
CS
.
S
.
singleton
(
aux
l2
))

l1
,
l2
>
Tallying
.
CS
.
S
.
union
(
Tallying
.
CS
.
S
.
singleton
(
aux
l1
))
(
Tallying
.
CS
.
S
.
singleton
(
aux
l2
))
(* check invariants on the constraints sets *)
let
mk_pp
=
function

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
>
Tallying
.
CS
.
prod
(
mk_pp
c
)
acc
)
Tallying
.
CS
.
sat
l
let
mk_union
l1
l2
=
Tallying
.
CS
.
union
(
mk_prod
l1
)
(
mk_prod
l2
)
let
test_constraint_ops
()
=
[
"prod pos"
,
mk_prod
[
P
(
V
"A"
,
"Int"
);
P
(
V
"A"
,
"Bool"
)]
,
mk_pp
(
P
(
V
"A"
,
"Int & Bool"
));
...
...
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