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
a8a4c258
Commit
a8a4c258
authored
Jun 12, 2014
by
Julien Lopez
Browse files
Updating TLV to check if a type is a type variable; still one test fails
parent
9b693d33
Changes
3
Hide whitespace changes
Inline
Side-by-side
tests/lambda/Makefile
View file @
a8a4c258
...
...
@@ -37,6 +37,16 @@ debug: $(OUTDEBUG)
%.byte
:
_import
$(COMPILER)
-use-ocamlfind
-tag
debug
$@
# Shortcuts
ast
:
astprinterTests.native
lambda
:
lambdaTests.native
typed
:
typedTests.native
value
:
valueTests.native
tests
:
make
-C
tests
...
...
tests/libtest/typesTest.ml
View file @
a8a4c258
...
...
@@ -13,18 +13,18 @@ let to_string pp t =
;;
let
tlv_tests
=
[
"is_var"
,
[
(*
"`$A", Types.is_var, true;
"`$A"
,
Types
.
is_var
,
true
;
"Int"
,
Types
.
is_var
,
false
;
"Empty"
,
Types
.
is_var
,
false
;
"Any", Types.is_var, false;
*)
"Any"
,
Types
.
is_var
,
false
;
"`$A & Int"
,
Types
.
is_var
,
false
;
(*
"`$A & Any", Types.is_var, true;
"`$A & Any"
,
Types
.
is_var
,
true
;
"`$A | Int"
,
Types
.
is_var
,
false
;
"(`$A,Int)"
,
Types
.
is_var
,
false
;
"Any
\\
`$A"
,
Types
.
is_var
,
true
;
(* ~`$A *)
"`$A \\ Any", Types.is_var, false; (* Empty *)
*)
"`$A
\\
Any"
,
Types
.
is_var
,
false
;
(* Empty *)
];
(*
"no_var"
,
[
"Int"
,
Types
.
no_var
,
true
;
"Any"
,
Types
.
no_var
,
true
;
...
...
@@ -55,7 +55,7 @@ let tlv_tests = [ "is_var", [
"`$A | (Char,Int)"
,
Types
.
has_tlv
,
true
;
"Any
\\
`$A"
,
Types
.
has_tlv
,
true
;
];
*)
]
let
test_tlv_operations
=
...
...
types/types.ml
View file @
a8a4c258
...
...
@@ -512,16 +512,13 @@ let update_tlv x y t =
(
aux
BoolRec
.
get
t
.
record
)
]
in
let
fv
t
=
if
Descr
.
equal
t
Descr
.
empty
then
Var
.
Set
.
empty
,
false
else
Var
.
Set
.
union
x
.
toplvars
.
fv
y
.
toplvars
.
fv
,
t
.
toplvars
.
isvar
in
let
fv
,
isvar
=
fv
t
in
let
fv
t
=
if
Descr
.
is_empty
t
then
Var
.
Set
.
empty
else
Var
.
Set
.
union
x
.
toplvars
.
fv
y
.
toplvars
.
fv
in
{
t
with
toplvars
=
{
tlv
=
tlv
t
;
fv
=
fv
;
isvar
=
isvar
fv
=
fv
t
;
isvar
=
t
.
toplvars
.
isvar
}
}
;;
...
...
@@ -531,47 +528,63 @@ let abstract a = { empty with abstract = a }
let
get_abstract
t
=
t
.
abstract
let
is_var
t
=
TLV
.
is_single
t
.
toplvars
let
no_var
t
=
TLV
.
no_variables
t
.
toplvars
let
has_tlv
t
=
TLV
.
has_toplevel
t
.
toplvars
let
all_vars
t
=
t
.
toplvars
.
TLV
.
fv
let
all_tlv
t
=
t
.
toplvars
.
TLV
.
tlv
let
cup
x
y
=
if
x
==
y
then
x
else
update_tlv
x
y
{
times
=
BoolPair
.
cup
x
.
times
y
.
times
;
xml
=
BoolPair
.
cup
x
.
xml
y
.
xml
;
arrow
=
BoolPair
.
cup
x
.
arrow
y
.
arrow
;
record
=
BoolRec
.
cup
x
.
record
y
.
record
;
ints
=
BoolIntervals
.
cup
x
.
ints
y
.
ints
;
atoms
=
BoolAtoms
.
cup
x
.
atoms
y
.
atoms
;
chars
=
BoolChars
.
cup
x
.
chars
y
.
chars
;
abstract
=
Abstract
.
cup
x
.
abstract
y
.
abstract
;
absent
=
x
.
absent
||
y
.
absent
;
toplvars
=
TLV
.
empty
}
if
x
==
y
then
x
else
let
t
=
{
times
=
BoolPair
.
cup
x
.
times
y
.
times
;
xml
=
BoolPair
.
cup
x
.
xml
y
.
xml
;
arrow
=
BoolPair
.
cup
x
.
arrow
y
.
arrow
;
record
=
BoolRec
.
cup
x
.
record
y
.
record
;
ints
=
BoolIntervals
.
cup
x
.
ints
y
.
ints
;
atoms
=
BoolAtoms
.
cup
x
.
atoms
y
.
atoms
;
chars
=
BoolChars
.
cup
x
.
chars
y
.
chars
;
abstract
=
Abstract
.
cup
x
.
abstract
y
.
abstract
;
absent
=
x
.
absent
||
y
.
absent
;
toplvars
=
TLV
.
empty
}
in
let
isvar
=
(
is_var
x
&&
x
==
t
)
||
(
is_var
y
&&
y
==
t
)
in
update_tlv
x
y
{
t
with
toplvars
=
{
t
.
toplvars
with
TLV
.
isvar
=
isvar
}}
let
cap
x
y
=
if
x
==
y
then
x
else
update_tlv
x
y
{
ints
=
BoolIntervals
.
cap
x
.
ints
y
.
ints
;
times
=
BoolPair
.
cap
x
.
times
y
.
times
;
xml
=
BoolPair
.
cap
x
.
xml
y
.
xml
;
record
=
BoolRec
.
cap
x
.
record
y
.
record
;
arrow
=
BoolPair
.
cap
x
.
arrow
y
.
arrow
;
atoms
=
BoolAtoms
.
cap
x
.
atoms
y
.
atoms
;
chars
=
BoolChars
.
cap
x
.
chars
y
.
chars
;
abstract
=
Abstract
.
cap
x
.
abstract
y
.
abstract
;
absent
=
x
.
absent
&&
y
.
absent
;
toplvars
=
TLV
.
empty
}
if
x
==
y
then
x
else
let
t
=
{
ints
=
BoolIntervals
.
cap
x
.
ints
y
.
ints
;
times
=
BoolPair
.
cap
x
.
times
y
.
times
;
xml
=
BoolPair
.
cap
x
.
xml
y
.
xml
;
record
=
BoolRec
.
cap
x
.
record
y
.
record
;
arrow
=
BoolPair
.
cap
x
.
arrow
y
.
arrow
;
atoms
=
BoolAtoms
.
cap
x
.
atoms
y
.
atoms
;
chars
=
BoolChars
.
cap
x
.
chars
y
.
chars
;
abstract
=
Abstract
.
cap
x
.
abstract
y
.
abstract
;
absent
=
x
.
absent
&&
y
.
absent
;
toplvars
=
TLV
.
empty
}
in
let
isvar
=
(
is_var
x
&&
x
==
t
)
||
(
is_var
y
&&
y
==
t
)
in
update_tlv
x
y
{
t
with
toplvars
=
{
t
.
toplvars
with
TLV
.
isvar
=
isvar
}}
let
diff
x
y
=
if
x
==
y
then
empty
else
update_tlv
x
y
{
times
=
BoolPair
.
diff
x
.
times
y
.
times
;
xml
=
BoolPair
.
diff
x
.
xml
y
.
xml
;
arrow
=
BoolPair
.
diff
x
.
arrow
y
.
arrow
;
record
=
BoolRec
.
diff
x
.
record
y
.
record
;
ints
=
BoolIntervals
.
diff
x
.
ints
y
.
ints
;
atoms
=
BoolAtoms
.
diff
x
.
atoms
y
.
atoms
;
chars
=
BoolChars
.
diff
x
.
chars
y
.
chars
;
abstract
=
Abstract
.
diff
x
.
abstract
y
.
abstract
;
absent
=
x
.
absent
&&
not
y
.
absent
;
toplvars
=
TLV
.
empty
}
if
x
==
y
then
empty
else
let
t
=
{
times
=
BoolPair
.
diff
x
.
times
y
.
times
;
xml
=
BoolPair
.
diff
x
.
xml
y
.
xml
;
arrow
=
BoolPair
.
diff
x
.
arrow
y
.
arrow
;
record
=
BoolRec
.
diff
x
.
record
y
.
record
;
ints
=
BoolIntervals
.
diff
x
.
ints
y
.
ints
;
atoms
=
BoolAtoms
.
diff
x
.
atoms
y
.
atoms
;
chars
=
BoolChars
.
diff
x
.
chars
y
.
chars
;
abstract
=
Abstract
.
diff
x
.
abstract
y
.
abstract
;
absent
=
x
.
absent
&&
not
y
.
absent
;
toplvars
=
TLV
.
empty
}
in
let
isvar
=
(
x
==
any
&&
is_var
y
)
||
(
is_var
x
&&
y
==
empty
)
in
update_tlv
x
y
{
t
with
toplvars
=
{
t
.
toplvars
with
TLV
.
isvar
=
isvar
}}
(* TODO: optimize disjoint check for boolean combinations *)
let
trivially_disjoint
a
b
=
...
...
@@ -601,13 +614,6 @@ and const_node c = cons (constant c)
let
neg
x
=
diff
any
x
let
is_var
t
=
TLV
.
is_single
t
.
toplvars
let
no_var
t
=
TLV
.
no_variables
t
.
toplvars
let
has_tlv
t
=
TLV
.
has_toplevel
t
.
toplvars
let
all_vars
t
=
t
.
toplvars
.
TLV
.
fv
let
all_tlv
t
=
t
.
toplvars
.
TLV
.
tlv
let
any_node
=
cons
any
let
empty_node
=
cons
empty
...
...
@@ -3044,10 +3050,10 @@ module Tallying = struct
else
begin
if
is_empty
t
then
CS
.
sat
(* if there is only one variable then is it A <= 0 or 1 <= A *)
(*
else if is_var t then
else
if
is_var
t
then
let
(
v
,
p
)
=
TLV
.
max
t
.
toplvars
in
let
s
=
if
p
then
(
Pos
(
v
,
empty
))
else
(
Neg
(
any
,
v
))
in
CS.singleton s
*)
CS
.
singleton
s
(* if there are no vars, and it is not empty then unsat *)
else
if
no_var
t
then
CS
.
unsat
else
begin
...
...
@@ -3208,12 +3214,12 @@ module Tallying = struct
Hashtbl
.
add
cache
alpha
()
;
(* if t containts only a toplevel variable and nothing else
* means that the constraint is of the form (alpha,beta). *)
(*
if is_var t then begin
if
is_var
t
then
begin
let
(
beta
,_
)
=
TLV
.
max
t
.
toplvars
in
let
acc1
=
aux
beta
(
empty
,
any
)
acc
in
(* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
aux
alpha
(
s
,
t
)
acc1
end else
*)
end
else
(* alpha = ( s v fresh) ^ t *)
aux
alpha
(
s
,
t
)
acc
;
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