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
efe6fa1e
Commit
efe6fa1e
authored
Jun 23, 2014
by
Julien Lopez
Browse files
Remove old syntax `$IDENT for type variables.
parent
92cc25ff
Changes
14
Expand all
Hide whitespace changes
Inline
Side-by-side
kim_multi.ml
View file @
efe6fa1e
This diff is collapsed.
Click to expand it.
parser/parser.ml
View file @
efe6fa1e
...
...
@@ -406,7 +406,6 @@ EXTEND Gram
tag_type
:
[
[
"_"
->
mk
_loc
(
Internal
(
Types
.
atom
Atoms
.
any
))
|
"$"
;
a
=
ident_or_keyword
->
mk
_loc
(
TVar
a
)
|
a
=
ident_or_keyword
->
mk
_loc
(
Cst
(
Atom
(
ident
a
)))
|
t
=
ANY_IN_NS
->
mk
_loc
(
NsT
(
ident
t
))
]
...
...
tests/lambda/src/lambdaTests.ml
View file @
efe6fa1e
...
...
@@ -28,14 +28,14 @@ let tests_poly_abstr = [
"fun f x : Int : Int -> 2"
;
"Test CDuce.lambda.poly.identity failed"
,
"Abstraction(Dummy,,,,Sel(,[([ Char* ] | Int -> [ Char* ] | Int)],Comp({},{{
`$
A =
Int },{
`$
A = [ Char* ]
"Abstraction(Dummy,,,,Sel(,[([ Char* ] | Int -> [ Char* ] | Int)],Comp({},{{
'
A =
Int },{
'
A = [ Char* ]
}})))"
,
"(fun f x : 'A : 'A -> x) [{A/Int},{A/String}]"
;
"Test CDuce.runtime.poly.tail failed"
,
"Abstraction(Dummy,,,,Sel(,[([ (
`$
A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow)* ] -> [ (
`$
A & Int |
"Abstraction(Dummy,,,,Sel(,[([ (
'
A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow)* ] -> [ (
'
A & Int |
Char |
Atom |
(Any,Any) |
...
...
@@ -43,19 +43,19 @@ Int },{ `$A = [ Char* ]
Arrow)* ])],{}))"
,
"fun tail x : ['A] : ['A] -> match x : ['A] with | (el : 'A) :: (rest : ['A]) -> rest"
;
"Test CDuce.runtime.poly.pair failed"
,
"Abstraction(Dummy,,,,Sel(,[((
`$
A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow,
`$
B & Int | Char |
"Test CDuce.runtime.poly.pair failed"
,
"Abstraction(Dummy,,,,Sel(,[((
'
A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow,
'
B & Int | Char |
Atom | (Any,Any) | <(Any) (Any)>Any | Arrow) ->
`$
A & Int | Char | Atom | (Any,Any) | <(Any) (Any)>Any | Arrow)],{}))"
,
'
A & Int | Char | Atom | (Any,Any) | <(Any) (Any)>Any | Arrow)],{}))"
,
"fun pair x : ('A * 'B) : 'A -> match x : ('A * 'B) with | (z : 'A, y : 'B) -> z"
;
"Test CDuce.runtime.poly.match_abstr failed"
,
"Apply(Match(Abstraction(Dummy,,,,Sel(,[(
`$
A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow ->
`$
A & Int |
"Test CDuce.runtime.poly.match_abstr failed"
,
"Apply(Match(Abstraction(Dummy,,,,Sel(,[(
'
A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow ->
'
A & Int |
Char |
Atom |
(Any,Any) |
<(Any) (Any)>Any |
Arrow)],{})), {accept_chars=false; brs_disp=<disp>; brs_rhs=[| (2, TVar(Local(0),Comp({},{ {
`$
A =
Arrow)],{})), {accept_chars=false; brs_disp=<disp>; brs_rhs=[| (2, TVar(Local(0),Comp({},{ {
'
A =
Int
} }))) |]; brs_stack_pos=0}),Const(3))"
,
"(match (fun f x : 'A : 'A -> x) : ('A -> 'A) with | y : ('A -> 'A) -> y[{A/Int}]).3"
;
...
...
@@ -73,7 +73,7 @@ let tests_poly_abstr = [
"Test CDuce.lambda.identity_applied failed"
,
"Apply(PolyAbstraction([Dummy,Dummy],,{accept_chars=true; brs_disp=<disp>; brs_rhs=[| (1, Var(Local(0))) |]; brs_stack_pos=0},,Sel(Env(1),[(
`$
A ->
`$
A)],{{
`$
A = Int
'
A ->
'
A)],{{
'
A = Int
}})),Const(2))"
,
"(fun f x : 'A : 'A -> x)[{A/Int}].2"
;
];;
...
...
@@ -213,14 +213,14 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
| x : (!(Int|Bool)) -> x).[2; 3]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.misc.map failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction([(
`$
A ->
`$
B,[
`$
A* ] -> [
`$
B* ])],Id)"
"Abstraction([(
'
A ->
'
B,[
'
A* ] -> [
'
B* ])],Id)"
(
run_test_eval
"fun map f : ('A -> 'B) x : ['A] : ['B] ->
match x : ['A] with
| (el : 'A) :: [] -> f.el
| (el : 'A) :: (rest : ['A]) -> ((f.el), ((map.f).rest))"
);
assert_equal
~
msg
:
"Test CDuce.runtime.misc.map_even failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction([([
`$
A* ],[
`$
B* ])],Id)"
"Abstraction([([
'
A* ],[
'
B* ])],Id)"
(
run_test_eval
"(fun map f : ('A->'B) x : ['A] : ['B] ->
match x : ['A] with
| (el : 'A) :: (rest : ['A]) -> ((f.el), ((map.f).rest))
...
...
@@ -254,7 +254,7 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
assert_equal
~
msg
:
"Test CDuce.runtime.misc.map_even_hard failed"
~
printer
:
(
fun
x
->
x
)
"(Atom(true),(
\"
hey
\"
,((3,(5,Atom(nil),Mono),Mono),(Atom(true),(Abstraction([(
`$C,`$
C)],Id),(Atom(false),Atom(nil),Mono),Mono),Mono),Mono),Mono),Mono)"
'C,'
C)],Id),(Atom(false),Atom(nil),Mono),Mono),Mono),Mono),Mono),Mono)"
(
run_test_eval
"(fun map f : ('A->'B) x : ['A] : ['B] ->
match x : ['A] with
| (el : 'A) :: (rest : ['A]) -> ((f.el), ((map.f).rest))
...
...
@@ -456,12 +456,12 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
"poly"
>::
(
fun
test_ctxt
->
assert_equal
~
msg
:
"Test CDuce.runtime.poly.identity_pure failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction([(
`$A,`$
A)],Id)"
"Abstraction([(
'A,'
A)],Id)"
(
run_test_eval
"fun f x : 'A : 'A -> x"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.identity failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction([(
`$A,`$
A)],Sel(1,[(
`$
A ->
`$
A)],{{
`$
A = Int},{
`$
A = [ Char* ]
"Abstraction([(
'A,'
A)],Sel(1,[(
'
A ->
'
A)],{{
'
A = Int},{
'
A = [ Char* ]
}}))"
(
run_test_eval
"(fun f x : 'A : 'A -> x)[{A/Int},{A/String}]"
);
...
...
@@ -475,7 +475,7 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
assert_equal
~
msg
:
"Test CDuce.runtime.poly.tail failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction([([
`$
A* ],[
`$
A* ])],Id)"
"Abstraction([([
'
A* ],[
'
A* ])],Id)"
(
run_test_eval
"fun tail x : ['A] : ['A] -> match x : ['A] with
| (_ : 'A) :: (rest : ['A]) -> rest"
);
...
...
@@ -485,31 +485,30 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
| (_ : 'A) :: (rest : ['A]) -> rest).[3; 7; 8; 5]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.multicomp failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction([(
`$A,`$
A)],Sel(1,[(
`$
A ->
`$
A)],{{
`$
A = Int
~
printer
:
(
fun
x
->
x
)
"Abstraction([(
'A,'
A)],Sel(1,[(
'
A ->
'
A)],{{
'
A = Int
}}))"
(
run_test_eval
"(((fun f x : 'A : 'A -> x)[{A/Int}])[{A/String}])[{A/Bool}]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.multicomp.2 failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction([(
`$A,`$
A)],Sel(1,[(
`$
A ->
`$
A)],Comp(Comp({{
`$
A =
`$B
}},{{`$B = `$
A}}),{{
`$
A =
`$
B
~
printer
:
(
fun
x
->
x
)
"Abstraction([(
'A,'
A)],Sel(1,[(
'
A ->
'
A)],Comp(Comp({{
'
A =
'B}},{{'B =
'
A}}),{{
'
A =
'
B
}})))"
(
run_test_eval
"(((fun f x : 'A : 'A -> x)[{A/'B}])[{B/'A}])[{A/'B}]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.multicomp.3 failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction([(
`$A,`$
A)],Sel(1,[(
`$
A ->
`$
A)],Comp(Comp(Comp({{
`$
B =
`$A
}},{{`$A = `$
B}}),{{
`$
B =
`$
A}}),{{
`$
A =
`$
B
~
printer
:
(
fun
x
->
x
)
"Abstraction([(
'A,'
A)],Sel(1,[(
'
A ->
'
A)],Comp(Comp(Comp({{
'
B =
'A}},{{'A =
'
B}}),{{
'
B =
'
A}}),{{
'
A =
'
B
}})))"
(
run_test_eval
"((((fun f x : 'A : 'A -> x)[{A/'B}])[{B/'A}])[{A/'B}])[{B/'A}]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.multicomp.4 failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction([(`$A,`$A)],Sel(1,[(`$A -> `$A)],Comp({{`$B = Int}},{{`$A =
`$B
~
printer
:
(
fun
x
->
x
)
"Abstraction([('A,'A)],Sel(1,[('A -> 'A)],Comp({{'B = Int}},{{'A = 'B
}})))"
(
run_test_eval
"(((((fun f x : 'A : 'A -> x)[{A/'B}])[{A/Int}])[{B/Int}])[{B/Int}])[{B/'A}]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.multicomp.5 failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction([(
`$A,`$
A)],Sel(1,[(
`$
A ->
`$
A)],Comp(Comp({{
`$
D =
`$C
},{`$C = `$B
}},{{
`$
B =
`$
C}}),{{
`$
A =
`$
B},{
`$
C =
`$
D
~
printer
:
(
fun
x
->
x
)
"Abstraction([(
'A,'
A)],Sel(1,[(
'
A ->
'
A)],Comp(Comp({{
'
D =
'C},{'C = 'B
}},{{
'
B =
'
C}}),{{
'
A =
'
B},{
'
C =
'
D
}})))"
(
run_test_eval
"((((fun f x : 'A : 'A -> x)[{A/'B},{C/'D}])[{B/'C}])[{B/'D}])[{D/'C},{C/'B}]"
);
...
...
tests/lambda/src/typedTests.ml
View file @
efe6fa1e
...
...
@@ -20,28 +20,28 @@ let tests_typer_list = [
"Test CDuce.typed.fun.identity",
"fun f x : 'A : 'A -> x",
"fun f (
`$
A ->
`$
A) x -> x";
"fun f (
'
A ->
'
A) x -> x";
"Test CDuce.typed.fun.identity.int",
"fun f x : 'A : 'A -> 2",
"fun f (
`$
A ->
`$
A) x -> x";
"fun f (
'
A ->
'
A) x -> x";
"Test CDuce.typed.fun.match",
"fun f x : ('A | Int) : ('A | Int) -> x",
"fun f (
`$
A ->
`$
A) x & Int -> x | x -> x";
"fun f (
'
A ->
'
A) x & Int -> x | x -> x";
"Test CDuce.typed.fun.partial 1",
"fun f x : 'A : 'A -> 2",
"fun f (
`$
A ->
`$
A ->
`$
A) x -> fun g -> g x";
"fun f (
'
A ->
'
A ->
'
A) x -> fun g -> g x";
"Test CDuce.typed.fun.partial 2",
"fun f x : 'A : 'A -> 2",
"fun f ( g :
`$
A ->
`$
B ) ( x :
`$
A) :
`$
B = g x";
"fun f ( g :
'
A ->
'
B ) ( x :
'
A) :
'
B = g x";
*)
"Test CDuce.typed.fun.partial 2"
,
"fun f x : 'A : 'A -> 2"
,
"let id ( y :
`$
A ) :
`$
B = y in id"
;
"let id ( y :
'
A ) :
'
B = y in id"
;
]
...
...
tests/lambda/src/valueTests.ml
View file @
efe6fa1e
...
...
@@ -28,11 +28,11 @@ let tests_poly_abstr = [
"(fun (x : 'A) : 'A = x) `a"
;
"Test CDuce.lambda.partial"
,
"Abstraction([(
`$
A,Int -> Int)],Id)"
,
"Abstraction([(
'
A,Int -> Int)],Id)"
,
"fun ('A -> (Int -> Int)) | _ -> (fun ('B -> 'B) y -> y)"
;
"Test CDuce.lambda.appl_partial"
,
"Abstraction([(
`$B,`$
B)],Id)"
,
"Abstraction([(
'B,'
B)],Id)"
,
"(fun ('A -> (Int -> Int)) | _ -> (fun ('B -> 'B) y -> y)) 3"
;
];;
...
...
tests/libtest/applyTest.ml
View file @
efe6fa1e
This diff is collapsed.
Click to expand it.
tests/libtest/gen_apps.sh
View file @
efe6fa1e
...
...
@@ -15,9 +15,9 @@ function cduce_type
t2
=
$(
echo
"
$t1
"
|
sed
-e
"s/
\(\[
[^]]*
\]\)
list/[
\1
* ]/g"
)
t3
=
$(
echo
"
$t2
"
|
sed
-e
"s/
\(\[
[^]]*
\]\)
list/[
\1
* ]/g"
)
t4
=
$(
echo
"
$t3
"
|
sed
-e
"s/
\(\[
[^]]*
\]\)
list/[
\1
* ]/g"
)
t5
=
$(
echo
"
$t4
"
|
sed
-e
"s/'
\(
[_a-z]*
\)
/
\
`
$
\
U
\1
/g"
)
t5
=
$(
echo
"
$t4
"
|
sed
-e
"s/'
\(
[_a-z]*
\)
/
\
'
\U\1
/g"
)
t6
=
$(
echo
"
$t5
"
|
sed
-e
"s/
\(
int
\|
bool
\)
/
\u\1
/g"
|
sed
-e
"s/unit/[]/g"
|
sed
-e
's/_//g'
)
echo
"type t =
$t6
"
|
sed
-e
'
s/\(
`$
[A-Z]*\)/Any/g
'
>
test.cd
echo
"type t =
$t6
"
|
sed
-e
"
s/
\(
'
[A-Z]*
\)
/Any/g
"
>
test.cd
cduce
-c
test.cd
>
/dev/null 2>&1
if
[
"
$?
"
=
"0"
]
;
then
echo
$t6
...
...
@@ -67,14 +67,14 @@ for i in `seq 0 "$last_type"`; do
ACCNAME
=
${
FUNNAME
[
$first
]
}
ACCTYPE
=
${
FUNTYPE
[
$first
]
}
echo
"(*
${
ARGNAME
}
${
ACCNAME
}
*)"
FTYPE
=
"
$(
echo
${
ACCTYPE
}
|
sed
-e
'
s:\(
`$
[A-Z]*\):\1'
$num
':g
'
)
"
FTYPE
=
"
$(
echo
${
ACCTYPE
}
|
sed
-e
"
s:
\(
\'
[A-Z]*
\)
:
\1
\
'
$num
\
'
:g
"
)
"
print_line
"
$ARG
"
"
$FTYPE
"
num
=
$((
$num
+
1
))
ACCTYPE
=
"(
$FTYPE
)"
for
j
in
$others
;
do
ACCNAME
=
"
$ACCNAME
&
${
FUNNAME
[
$j
]
}
"
echo
"(*
${
ARGNAME
}
${
ACCNAME
}
*)"
FTYPE
=
"
$(
echo
${
FUNTYPE
[
$j
]
}
|
sed
-e
'
s:\(
`$
[A-Z]*\):\1'
$num
':g
'
)
"
FTYPE
=
"
$(
echo
${
FUNTYPE
[
$j
]
}
|
sed
-e
"
s:
\(
\'
[A-Z]*
\)
:
\1
\
'
$num
\
'
:g
"
)
"
ACCTYPE
=
"
$ACCTYPE
& (
${
FTYPE
}
)"
print_line
"
$ARG
"
"
${
ACCTYPE
}
"
num
=
$((
$num
+
1
))
...
...
tests/libtest/gen_multi.py
View file @
efe6fa1e
...
...
@@ -9,14 +9,14 @@ def f (a,a1,p1) :
tmplist
=
[[
""
for
i
in
xrange
(
6
)]
for
i
in
xrange
(
arity
)]
for
i
in
range
(
arity
)
:
a
=
[
"
`$
A%d"
%
j
for
j
in
range
(
i
+
1
)]
a
=
[
"
'
A%d"
%
j
for
j
in
range
(
i
+
1
)]
f1
=
" -> "
.
join
(
a
)
p1
=
" , "
.
join
(
a
)
tn1
,
tn2
,
tn3
=
f
(
f1
,
"
`$
A0"
,
p1
)
a
=
[
"(
`$
A%d%d ->
`$
A%d)"
%
(
j
,
j
,
j
)
for
j
in
range
(
i
+
1
)]
tn1
,
tn2
,
tn3
=
f
(
f1
,
"
'
A0"
,
p1
)
a
=
[
"(
'
A%d%d ->
'
A%d)"
%
(
j
,
j
,
j
)
for
j
in
range
(
i
+
1
)]
f1
=
" -> "
.
join
(
a
)
p1
=
" , "
.
join
(
a
)
sn1
,
sn2
,
sn3
=
f
(
f1
,
"
`$
A1"
,
p1
)
sn1
,
sn2
,
sn3
=
f
(
f1
,
"
'
A1"
,
p1
)
tmplist
[
i
]
=
[
tn1
,
tn2
,
tn3
,
sn1
,
sn2
,
sn3
]
slist
=
[]
...
...
tests/libtest/gen_multi.sh
View file @
efe6fa1e
...
...
@@ -9,12 +9,12 @@ do
echo
-n
'"'
for
j
in
`
seq
1
$i
`
do
echo
-n
'
`$
A'
${
PREF
}${
j
}
' -> '
echo
-n
'
'
A
'${PREF}${j}'
->
'
done
echo '
Int
", ['
for j in
`
seq
1
$i
`
do
echo
'"
`$
B'
${
PREF
}${
j
}
'";'
echo '"
'
B'
${
PREF
}${
j
}
'";'
#echo '"Int";'
done
echo
"];"
...
...
@@ -26,30 +26,30 @@ echo "];;"
echo
"let funs_hh = ["
for
i
in
`
seq
1 15
`
do
echo
-n
'"(
`$
A'
${
PREF
}
1
' ->
`$
B'
${
PREF
}
1
' ) '
echo
-n
'"(
'
A
'${PREF}1'
->
'
B'
${
PREF
}
1
' ) '
for
j
in
`
seq
2
$i
`
do
echo
-n
'-> (
`$
A'
${
PREF
}${
j
}
' ->
`$
B'
${
PREF
}${
j
}
' ) '
echo
-n
'-> (
'
A
'${PREF}${j}'
->
'
B'
${
PREF
}${
j
}
' ) '
done
echo
-n
'->
`$
A'
${
PREF
}
1
' '
echo
-n
'->
'
A
'${PREF}1'
'
for j in `seq 2 $i`
do
echo
-n
'->
`$
A'
${
PREF
}${
j
}
' '
echo -n '
->
'
A'
${
PREF
}${
j
}
' '
done
echo
-n
' -> ('
echo
-n
'
`$
B'
${
PREF
}
1
echo
-n
'
'
B
'${PREF}1
for j in `seq 2 $i`
do
echo
-n
',
`$
B'
${
PREF
}${
j
}
echo -n '
,
'
B'
${
PREF
}${
j
}
done
echo
')", ['
for
j
in
`
seq
1
$i
`
do
echo
'" (
`$
C'
${
PREF
}${
j
}
' ->
`$
D'
${
PREF
}${
j
}
' ) ";'
# & (
`$
E'${PREF}${j}' ->
`$
F'${PREF}${j}') ";'
echo
'" (
'
C
'${PREF}${j}'
->
'
D'
${
PREF
}${
j
}
' ) ";'
# & (
'
E'${PREF}${j}' ->
'
F'${PREF}${j}') ";'
done
for
j
in
`
seq
1
$i
`
do
echo
'" (
`$
C'
${
PREF
}${
j
}
' )";'
# |
`$
E'${PREF}${j}') ";'
echo
'" (
'
C
'${PREF}${j}'
)
";' # |
'
E'
${
PREF
}${
j
}
') "
;
'
done
echo "];"
PREF=$(($PREF + 1 ))
...
...
tests/libtest/printTest.ml
View file @
efe6fa1e
...
...
@@ -19,36 +19,36 @@ let print_tests = [
"(Int,Int)"
;
"Int -> Int"
;
"Bool -> Bool"
;
"Int ->
`$
A"
;
"Int ->
'
A"
;
"[] -> []"
;
"Int ->
`$
A"
;
"(
`$
A -> Bool)"
;
"(
`$
B ->
`$
B)"
;
"Int ->
'
A"
;
"(
'
A -> Bool)"
;
"(
'
B ->
'
B)"
;
"(Int -> Bool)"
;
"(Int -> Int) | (Bool -> Bool)"
;
"(Int -> Int) | (Bool -> Bool)"
;
"([0--*] & `true)"
;
"(
`$
A | Int) & ((Any
\\
`$
A) | Bool)"
;
"(
`$
A | (
`$
B ,
`$
C))"
;
"(
'
A | Int) & ((Any
\\
'
A) | Bool)"
;
"(
'
A | (
'
B ,
'
C))"
;
"(Int , Int)"
;
"(
`$
A ->
`$
B) -> [
`$
A ] -> [
`$
B ]"
;
"((Int -> Bool) | ((
`$
A
\\
Int) -> (
`$
B
\\
Int))) ->
`$
Gamma"
;
"((
`$
A , Int) & (
`$
B , Bool))"
;
"(
'
A ->
'
B) -> [
'
A ] -> [
'
B ]"
;
"((Int -> Bool) | ((
'
A
\\
Int) -> (
'
B
\\
Int))) ->
'
Gamma"
;
"((
'
A , Int) & (
'
B , Bool))"
;
"(Int , (*Int & Bool*) Empty)"
;
"((
`$
A , Int) | (
`$
B , Bool))"
;
"((
'
A , Int) | (
'
B , Bool))"
;
"(Int , (Int | Bool))"
;
"((Int | Bool) -> Int)"
;
"((Int | Bool) -> Int)"
;
"(Int -> Int) | (Bool -> Bool)"
;
"((Int,Int) , (Int | Bool))"
;
"(
`$
A,Int) | ((
`$
B,Int),Bool)"
;
"((
`$
A , Int) | (
`$
B , Bool))"
;
"(
'
A,Int) | ((
'
B,Int),Bool)"
;
"((
'
A , Int) | (
'
B , Bool))"
;
"(Int , (Int | Bool))"
;
"((
`$
A , Int) & (
`$
B , Bool))"
;
"((
'
A , Int) & (
'
B , Bool))"
;
"(Int , (Int & Bool))"
;
"(
`$
A ->
`$
B) -> [
`$
A ] -> [
`$
B ]"
;
"((Int -> Bool) & ((
`$
A
\\
Int) -> (
`$
A
\\
Int)))"
;
"((Int -> Int) & (Bool -> Bool)) ->
`$
T"
;
"(
'
A ->
'
B) -> [
'
A ] -> [
'
B ]"
;
"((Int -> Bool) & ((
'
A
\\
Int) -> (
'
A
\\
Int)))"
;
"((Int -> Int) & (Bool -> Bool)) ->
'
T"
;
]
let
test_print
=
...
...
tests/libtest/tallyingTest.ml
View file @
efe6fa1e
...
...
@@ -80,9 +80,9 @@ let test_constraint_ops () = [
"prod neg"
,
mk_prod
[
N
(
"Int"
,
V
"B"
);
N
(
"Bool"
,
V
"B"
)]
,
mk_pp
(
N
(
"Int | Bool"
,
V
"B"
));
"prod var"
,
mk_prod
[
N
(
"
`$B
"
,
V
"A"
);
P
(
V
"B"
,
"Bool | Int"
)]
,
"prod var"
,
mk_prod
[
N
(
"
('B)
"
,
V
"A"
);
P
(
V
"B"
,
"Bool | Int"
)]
,
mk_union_res
[
N
(
"
`$B
"
,
V
"A"
);
P
(
V
"B"
,
"Bool | Int"
)]
[
N
(
"
('B)
"
,
V
"A"
);
P
(
V
"B"
,
"Bool | Int"
)]
[]
;
"empty"
,
mk_union
[
P
(
V
"A"
,
"Empty"
)]
[
P
(
V
"A"
,
"Empty"
)]
,
mk_pp
(
P
(
V
"A"
,
"Empty"
));
...
...
@@ -134,30 +134,30 @@ let norm_tests () = [
"(Int,Int)"
,
"Empty"
,
Tallying
.
CS
.
unsat
;
"Int -> Int"
,
"Empty"
,
Tallying
.
CS
.
unsat
;
"Bool -> Bool"
,
"Int ->
`$A
"
,
Tallying
.
CS
.
unsat
;
"Bool -> Bool"
,
"Int ->
('A)
"
,
Tallying
.
CS
.
unsat
;
"Int"
,
"Bool"
,
Tallying
.
CS
.
unsat
;
"Int"
,
"Empty"
,
Tallying
.
CS
.
unsat
;
"[] -> []"
,
"Int ->
`$A
"
,
Tallying
.
CS
.
unsat
;
"[] -> []"
,
"Int ->
('A)
"
,
Tallying
.
CS
.
unsat
;
"Any"
,
"Empty"
,
Tallying
.
CS
.
unsat
;
"Empty"
,
"Empty"
,
Tallying
.
CS
.
sat
;
"(
`$A
-> Bool)"
,
"(
`$B -> `$B
)"
,
mk_s
[
"(
('A)
-> Bool)"
,
"(
('B) -> ('B)
)"
,
mk_s
[
[
P
(
V
"B"
,
"Empty"
)];
[
N
(
"
`$B
"
,
V
"A"
);
N
(
"Bool"
,
V
"B"
)]
[
N
(
"
('B)
"
,
V
"A"
);
N
(
"Bool"
,
V
"B"
)]
];
"
`$B"
,
"`$A
"
,
mk_s
[[
N
(
"
`$B
"
,
V
"A"
)]];
"
`$B
"
,
"Empty"
,
mk_s
[[
P
(
V
"B"
,
"Empty"
)]];
"Int"
,
"
`$B
"
,
mk_s
[[
N
(
"Int"
,
V
"B"
)]];
"Int"
,
"(
`$A | `$B
)"
,
mk_s
[[
N
(
"Int
\\
`$B
"
,
V
"A"
)]];
"
('B)"
,
"('A)
"
,
mk_s
[[
N
(
"
('B)
"
,
V
"A"
)]];
"
('B)
"
,
"Empty"
,
mk_s
[[
P
(
V
"B"
,
"Empty"
)]];
"Int"
,
"
('B)
"
,
mk_s
[[
N
(
"Int"
,
V
"B"
)]];
"Int"
,
"(
('A) | ('B)
)"
,
mk_s
[[
N
(
"Int
\\
('B)
"
,
V
"A"
)]];
"(Int -> Bool)"
,
"(
`$A -> `$B
)"
,
mk_s
[
"(Int -> Bool)"
,
"(
('A) -> ('B)
)"
,
mk_s
[
[
P
(
V
"A"
,
"Empty"
)];
[
P
(
V
"A"
,
"Int"
);
N
(
"Bool"
,
V
"B"
)]
];
"(Int -> Int) | (Bool -> Bool)"
,
"(
`$A -> `$B
)"
,
mk_s
[
"(Int -> Int) | (Bool -> Bool)"
,
"(
('A) -> ('B)
)"
,
mk_s
[
[
P
(
V
"A"
,
"Empty"
)];
(* All these are subsumed as less general then (A <= 0) *)
[
P
(
V
"A"
,
"Empty"
);
N
(
"Int"
,
V
"B"
)];
...
...
@@ -165,52 +165,52 @@ let norm_tests () = [
[
P
(
V
"A"
,
"Empty"
);
N
(
"Int | Bool"
,
V
"B"
)]
];
"(
`$A -> `$B
)"
,
"(Int -> Int) | (Bool -> Bool)"
,
mk_s
[
"(
('A) -> ('B)
)"
,
"(Int -> Int) | (Bool -> Bool)"
,
mk_s
[
[
P
(
V
"B"
,
"Int"
);
N
(
"Int"
,
V
"A"
)];
[
P
(
V
"B"
,
"Bool"
);
N
(
"Bool"
,
V
"A"
)];
];
(*
"([0--*] & `true)", "(
`$A
| Int) & ((Any \\
`$A
) | Bool)",
"([0--*] & `true)", "(
('A)
| Int) & ((Any \\
('A)
) | Bool)",
*)
"(
`$A , `$B
)"
,
"(Int , Bool)"
,
mk_s
[
"(
('A) , ('B)
)"
,
"(Int , Bool)"
,
mk_s
[
[
P
(
V
"A"
,
"Empty"
)];
[
P
(
V
"B"
,
"Empty"
)];
[
P
(
V
"A"
,
"Int"
);
P
(
V
"B"
,
"Bool"
)]
];
"{a=(
`$A , `$B
)}"
,
"{a=(Int , Bool)}"
,
mk_s
[
"{a=(
('A) , ('B)
)}"
,
"{a=(Int , Bool)}"
,
mk_s
[
[
P
(
V
"A"
,
"Empty"
)];
[
P
(
V
"B"
,
"Empty"
)];
[
P
(
V
"A"
,
"Int"
);
P
(
V
"B"
,
"Bool"
)]
];
"{a=(Int , Bool)}"
,
"{a=(
`$A , `$B
)}"
,
mk_s
[
[
N
(
"Int"
,
V
"A"
);
N
(
"Bool"
,
V
"B"
)]
];
"{a=(Int , Bool)}"
,
"{a=(
('A) , ('B)
)}"
,
mk_s
[
[
N
(
"Int"
,
V
"A"
);
N
(
"Bool"
,
V
"B"
)]
];
"(Int , Bool)"
,
"(
`$A , `$B
)"
,
mk_s
[
[
N
(
"Int"
,
V
"A"
);
N
(
"Bool"
,
V
"B"
)]
];
"(Bool , Bool)"
,
"(
`$A , `$B
)"
,
mk_s
[
[
N
(
"Bool"
,
V
"A"
);
N
(
"Bool"
,
V
"B"
)]
];
"(Int , Bool)"
,
"(
('A) , ('B)
)"
,
mk_s
[
[
N
(
"Int"
,
V
"A"
);
N
(
"Bool"
,
V
"B"
)]
];
"(Bool , Bool)"
,
"(
('A) , ('B)
)"
,
mk_s
[
[
N
(
"Bool"
,
V
"A"
);
N
(
"Bool"
,
V
"B"
)]
];
"(
`$A | (`$B , `$C
))"
,
"(Int , Int)"
,
mk_s
[
"(
('A) | (('B) , ('C)
))"
,
"(Int , Int)"
,
mk_s
[
[
P
(
V
"A"
,
"(Int , Int)"
);
P
(
V
"B"
,
"Empty"
)];
[
P
(
V
"A"
,
"(Int , Int)"
);
P
(
V
"C"
,
"Empty"
)];
[
P
(
V
"A"
,
"(Int , Int)"
);
P
(
V
"B"
,
"Int"
);
P
(
V
"C"
,
"Int"
)];
];
"(
`$A
, Int) | (
`$B
, Bool))"
,
"(Int , (Int | Bool))"
,
mk_s
[
"(
('A)
, Int) | (
('B)
, Bool))"
,
"(Int , (Int | Bool))"
,
mk_s
[
[
P
(
V
"A"
,
"Int"
);
P
(
V
"B"
,
"Int"
)]
];
"(
`$A
->
`$
B) -> [
`$A
] -> [
`$B
]"
,
"((Int -> Bool) | ((
`$A
\\
Int) -> (
`$B
\\
Int))) ->
`$
Gamma"
,
mk_s
[
[
P
(
V
"A"
,
"Empty"
);
N
(
"[
`$A
] -> [
`$B
]"
,
V
"Gamma"
)]
"(
('A)
->
('
B)
)
-> [
('A)
] -> [
('B)
]"
,
"((Int -> Bool) | ((
('A)
\\
Int) -> (
('B)
\\
Int))) ->
('
Gamma
)
"
,
mk_s
[
[
P
(
V
"A"
,
"Empty"
);
N
(
"[
('A)
] -> [
('B)
]"
,
V
"Gamma"
)]
];
"Int -> Bool"
,
"
`$A
"
,
mk_s
[[
N
(
"Int -> Bool"
,
V
"A"
)]];
"Int -> Bool"
,
"
('A)
"
,
mk_s
[[
N
(
"Int -> Bool"
,
V
"A"
)]];
"((
`$A
, Int) & (
`$B
, Bool))"
,
"(Int , (*Int & Bool*) Empty)"
,
Tallying
.
CS
.
sat
;
"((
('A)
, Int) & (
('B)
, Bool))"
,
"(Int , (*Int & Bool*) Empty)"
,
Tallying
.
CS
.
sat
;
"((
`$A
, Int) | (
`$B
, Bool))"
,
"(Int , (Int | Bool))"
,
mk_s
[
"((
('A)
, Int) | (
('B)
, Bool))"
,
"(Int , (Int | Bool))"
,
mk_s
[
[
P
(
V
"A"
,
"Int"
);
P
(
V
"B"
,
"Int"
)]
];
...
...
@@ -237,17 +237,17 @@ let merge_tests () = [
"unsat 1"
,
mk_s
[[
P
(
V
"A"
,
"Int | Bool"
);
N
(
"Int"
,
V
"B"
);
P
(
V
"B"
,
"Empty"
)]]
,
Tallying
.
CS
.
unsat
;
"unsat 2"
,
mk_s
[[
N
(
"Bool"
,
V
"B"
);
N
(
"
`$B
"
,
V
"A"
);
P
(
V
"A"
,
"Empty"
)]]
,
Tallying
.
CS
.
unsat
;
"unsat 2"
,
mk_s
[[
N
(
"Bool"
,
V
"B"
);
N
(
"
('B)
"
,
V
"A"
);
P
(
V
"A"
,
"Empty"
)]]
,
Tallying
.
CS
.
unsat
;
"quad"
,
mk_s
[[
N
(
"Bool"
,
V
"B"
);
N
(
"Int"
,
V
"B"
);
N
(
"
`$B
"
,
V
"A"
);
P
(
V
"A"
,
"Int | Bool"
)]]
,
"quad"
,
mk_s
[[
N
(
"Bool"
,
V
"B"
);
N
(
"Int"
,
V
"B"
);
N
(
"
('B)
"
,
V
"A"
);
P
(
V
"A"
,
"Int | Bool"
)]]
,
mk_s
[
[
N
(
"
`$B
"
,
V
"A"
);
P
(
V
"A"
,
"Int | Bool"
);
N
(
"Int | Bool"
,
V
"B"
);
P
(
V
"B"
,
"Int | Bool"
)]
[
N
(
"
('B)
"
,
V
"A"
);
P
(
V
"A"
,
"Int | Bool"
);
N
(
"Int | Bool"
,
V
"B"
);
P
(
V
"B"
,
"Int | Bool"
)]
];
"add one"
,
mk_s
[[
N
(
"
`$B
"
,
V
"A"
);
P
(
V
"A"
,
"Int | Bool"
)]]
,
mk_s
[[
N
(
"
`$B
"
,
V
"A"
);
P
(
V
"A"
,
"Int | Bool"
);
P
(
V
"B"
,
"Int | Bool"
)]];
"add one"
,
mk_s
[[
N
(
"
('B)
"
,
V
"A"
);
P
(
V
"A"
,
"Int | Bool"
)]]
,
mk_s
[[
N
(
"
('B)
"
,
V
"A"
);
P
(
V
"A"
,
"Int | Bool"
);
P
(
V
"B"
,
"Int | Bool"
)]];
"A B"
,
mk_s
[[
P
(
V
"A"
,
"
`$B
"
)]]
,
mk_pp
(
P
(
V
"A"
,
"
`$B
"
));
"A B"
,
mk_s
[[
P
(
V
"A"
,
"
('B)
"
)]]
,
mk_pp
(
P
(
V
"A"
,
"
('B)
"
));
""
,
mk_s
[[
P
(
V
"B"
,
"Empty"
)]]
,
mk_pp
(
P
(
V
"B"
,
"Empty"
));
...
...
@@ -280,48 +280,48 @@ let mk_e ll =
)
ll
let
tallying_tests
=
[
[(
"((Int | Bool) -> Int)"
,
"(
`$A -> `$B
)"
)]
,
mk_e
[
[(
"((Int | Bool) -> Int)"
,
"(
('A) -> ('B)
)"
)]
,
mk_e
[
[(
V
"A"
,
"Empty"
)];
[(
V
"A"
,
"Int | Bool"
);(
V
"B"
,
"Int"
)]
];
[(
"((Int | Bool) -> Int)"
,
"(
`$A -> `$B
)"
);
(
"(
`$A
-> Bool)"
,
"(
`$B -> `$B
)"
)]
,
mk_e
[
[(
"((Int | Bool) -> Int)"
,
"(
('A) -> ('B)
)"
);
(
"(
('A)
-> Bool)"
,
"(
('B) -> ('B)
)"
)]
,
mk_e
[
[(
V
"A"
,
"Int | Bool"
);(
V
"B"
,
"Int | Bool"
)];
[(
V
"A"
,
"Empty"
);(
V
"B"
,
"Empty"
)]
];
[(
"(Int -> Bool)"
,
"(
`$A -> `$B
)"
)]
,
mk_e
[
[(
"(Int -> Bool)"
,
"(
('A) -> ('B)
)"
)]
,
mk_e
[
[(
V
"A"
,
"Empty"
)];
[(
V
"A"
,
"Int"
);(
V
"B"
,
"Bool"
)];
];
[(
"(Int -> Int) | (Bool -> Bool)"
,
"(
`$A -> `$B
)"
)]
,
mk_e
[
[(
"(Int -> Int) | (Bool -> Bool)"
,
"(
('A) -> ('B)
)"
)]
,
mk_e
[
[(
V
"A"
,
"Empty"
)];
];
[(
"((Int,Int) , (Int | Bool))"
,
"(
`$A
,Int) | ((
`$B
,Int),Bool)"
)]
,
mk_e
[
[(
"((Int,Int) , (Int | Bool))"
,
"(
('A)
,Int) | ((
('B)
,Int),Bool)"
)]
,
mk_e
[
[(
V
"A"
,
"(Int,Int)"
);
(
V
"B"
,
"Int"
)]
];
[(
"((
`$A
, Int) | (
`$B
, Bool))"
,
"(Int , (Int | Bool))"
)]
,
mk_e
[
[(
"((
('A)
, Int) | (
('B)
, Bool))"
,
"(Int , (Int | Bool))"
)]
,
mk_e
[
[(
V
"A"
,
"Int"
);(
V
"B"
,
"Int"
)]
];
[(
"[] -> []"
,
"Int ->
`$A
"
)]
,
[]
;
[(
"Bool -> Bool"
,
"Int ->
`$A
"
)]
,
[]
;
[(
"[] -> []"
,
"Int ->
('A)
"
)]
,
[]
;
[(
"Bool -> Bool"
,
"Int ->
('A)
"
)]
,
[]
;
[(
"((
`$A
, Int) & (
`$B
, Bool))"
,
"(Int , (Int & Bool))"
)]
,
[[]];
[(
"((
('A)
, Int) & (
('B)
, Bool))"
,
"(Int , (Int & Bool))"
)]
,
[[]];
(* map even *)
(* [("(
`$A -> `$B
) -> [
`$A
] -> [
`$B
]","((Int -> Bool) & ((
`$A
\\ Int) -> (
`$A
\\ Int)))")], [[]];*)
[(
"(
`$A -> `$A
)"
,
"((Int -> Int) & (Bool -> Bool)) ->
`$T
"
)]
,
mk_e
[]
;
(* [("(
('A) -> ('B)
) -> [
('A)
] -> [
('B)
]","((Int -> Bool) & ((
('A)
\\ Int) -> (
('A)
\\ Int)))")], [[]];*)
[(
"(
('A) -> ('A)
)"
,
"((Int -> Int) & (Bool -> Bool)) ->
('T)
"
)]
,
mk_e
[]
;
(* records *)
[(
"{a=Int}"
,
"Any"
)]
,
[[]];
[(
"{a=
`$A
}"
,
"Any"
)]
,
[[]];
[(
"{a=
('A)
}"
,
"Any"
)]
,
[[]];
[(
"{a=Int}"
,
"{a=(Int|Bool)}"
)]
,
[[]];
(*
[("{a=Bool -> Bool}","{b=Int ->
`$A
}")], [[]];
[("{a=(Int -> Int) | (Bool -> Bool)}","{b=(
`$A -> `$B
)}")], [[]];
[("{a=Int} -> Int", "{a=
`$A
} ->
`$A
")], [[]];
[("{a=Bool -> Bool}","{b=Int ->
('A)
}")], [[]];
[("{a=(Int -> Int) | (Bool -> Bool)}","{b=(
('A) -> ('B)
)}")], [[]];
[("{a=Int} -> Int", "{a=
('A)
} ->
('A)
")], [[]];
*)
]
...
...
@@ -353,100 +353,100 @@ let test_tallying =
let
apply_raw_tests
=
[
"iter hd"
,
"(
`$A
-> []) -> [
`$A
* ] -> []"
,
"[
`$
A0* ] ->
`$
A0"
;
"(
('A)
-> []) -> [
('A)
* ] -> []"
,
"[
('
A0
)
* ] ->
('
A0
)
"
;
"iteri assoc"
,
"(Int ->
`$A
-> []) -> [
`$A
* ] -> []"
,
"
`$
A1 -> [ (
`$
A1 ,
`$
B1)* ] ->
`$
B1"
;
"(Int ->
('A)
-> []) -> [
('A)
* ] -> []"
,
"
('
A1
)
-> [ (
('
A1
)
,
('
B1)
)
* ] ->
('
B1
)
"
;
"map length"
,
"(
`$A -> `$B
) -> [
`$A
* ] -> [
`$B
* ]"
,
"[
`$
A3* ] -> Int"
;
"(
('A) -> ('B)
) -> [
('A)
* ] -> [
('B)
* ]"
,
"[
('
A3
)
* ] -> Int"
;
"map length & hd"
,
"(
`$A
->
`$
B) -> [
`$A
* ] -> [
`$B
* ]"
,
"([
`$
A3* ] -> Int) & ([
`$
A4* ] ->
`$
A4)"
;
"(
('A)
->
('
B)
)
-> [
('A)
* ] -> [
('B)
* ]"
,
"([
('
A3
)
* ] -> Int) & ([
('
A4
)
* ] ->
('
A4)
)
"
;
"mapi mem"
,
"(Int ->
`$A -> `$B
) -> [
`$A
* ] -> [
`$B
* ]"
,
"
`$
A45 -> [
`$
A45* ] -> Bool"
;
"(Int ->
('A) -> ('B)
) -> [
('A)
* ] -> [
('B)
* ]"
,
"
('
A45
)
-> [
('
A45
)
* ] -> Bool"
;
"mapi mem & memq"
,
"(Int ->
`$A -> `$B
) -> [
`$A
* ] -> [
`$B
* ]"
,
"(
`$
A45 -> [
`$
A45* ] -> Bool) & (
`$
A46 -> [