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
bafc0253
Commit
bafc0253
authored
May 26, 2014
by
Pietro Abate
Browse files
More refacting of lambda test parse
parent
aff63904
Changes
4
Hide whitespace changes
Inline
Side-by-side
tests/lambda/src/compute.ml
View file @
bafc0253
...
...
@@ -78,7 +78,7 @@ let rec _to_typed env l expr =
|
String
(
_
,
s
)
->
let
i
=
Big_int
.
big_int_of_int
0
in
let
s
=
Types
.
String
(
0
,
(
String
.
length
s
)
-
1
,
s
,
Types
.
Integer
i
)
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
(
type_of_string
"String"
)
;
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
Builtin_defs
.
string
;
exp_descr
=
Cst
s
}
|
Bool
(
origloc
,
b
)
->
let
t
=
Builtin_defs
.
true_type
in
...
...
@@ -120,15 +120,15 @@ and type_of_sigma x s =
and
type_of_ptype
=
let
open
Types
in
function
|
Type
(
t
)
->
type_of_string
t
|
PType
(
t
,
s
)
->
if
s
=
[[]]
then
var
(
`Var
(
Var
.
make_id
t
))
else
type_of_sigma
t
s
|
TPair
(
t1
,
t2
)
->
times
(
cons
(
type_of_ptype
t1
))
(
cons
(
type_of_ptype
t2
))
|
TUnion
(
t1
,
t2
)
->
cup
(
type_of_ptype
t1
)
(
type_of_ptype
t2
)
|
TInter
(
t1
,
t2
)
->
cap
(
type_of_ptype
t1
)
(
type_of_ptype
t2
)
|
TNot
(
t
)
->
neg
(
type_of_ptype
t
)
|
TArrow
(
t1
,
t2
)
->
arrow
(
cons
(
type_of_ptype
t1
))
(
cons
(
type_of_ptype
t2
))
|
TSeq
(
t
)
->
Sequence
.
star
(
type_of_ptype
t
)
|
Type
(
t
)
->
type_of_string
t
|
PType
(
t
,
[[]])
->
var
(
`Var
(
Var
.
make_id
t
))
|
PType
(
t
,
s
)
->
type_of_sigma
t
s
|
TPair
(
t1
,
t2
)
->
times
(
cons
(
type_of_ptype
t1
))
(
cons
(
type_of_ptype
t2
))
|
TUnion
(
t1
,
t2
)
->
cup
(
type_of_ptype
t1
)
(
type_of_ptype
t2
)
|
TInter
(
t1
,
t2
)
->
cap
(
type_of_ptype
t1
)
(
type_of_ptype
t2
)
|
TNot
(
t
)
->
neg
(
type_of_ptype
t
)
|
TArrow
(
t1
,
t2
)
->
arrow
(
cons
(
type_of_ptype
t1
))
(
cons
(
type_of_ptype
t2
))
|
TSeq
(
t
)
->
Printf
.
eprintf
"ffffff
\n
"
;
Sequence
.
star
(
type_of_ptype
t
)
and
first_param
loc
iface
=
let
rec
_first_param
loc
accu
=
function
...
...
tests/lambda/src/lambdaTests.ml
View file @
bafc0253
...
...
@@ -65,9 +65,11 @@ Int
]
let
tests_poly_abstr
=
[
(*
"Test CDuce.lambda.const_abstr failed",
"Abstraction(Dummy,,,,Sel((Int -> Int),{}))",
"fun f x : 'A[{A/Int}] : 'A[{A/Int}] -> 2";
*)
"Test CDuce.lambda.const_abstr failed"
,
"Abstraction(Dummy,,,,Sel(,(Int -> Int),{}))"
,
...
...
tests/lambda/src/parse.ml
View file @
bafc0253
...
...
@@ -44,34 +44,44 @@ module ExprParser = struct
[
"abstr"
RIGHTA
[
"fun"
;
x
=
LIDENT
;
p
=
LIST1
param
;
":"
;
t
=
type_id
;
"->"
;
e
=
SELF
->
let
rec
make_fv
accu
nb
=
function
|
_
::
[]
|
[]
->
accu
|
(
_
,
name
,
_
)
::
rest
->
make_fv
(
accu
@
[
nb
,
name
])
(
nb
+
1
)
rest
in
let
rec
aux
acc
t
fv
=
function
|
(
loc
,
pname
,
ptype
)
::
[]
->
let
t
=
TArrow
(
ptype
,
t
)
in
Abstr
(
_loc
,
x
,
t
,
[]
,
[
_loc
,
MVar
(
loc
,
pname
,
ptype
)
,
acc
])
|
(
loc
,
pname
,
ptype
)
::
rest
->
let
t
=
TArrow
(
ptype
,
t
)
in
let
newfv
=
match
fv
with
|
_
::
rest
->
rest
|
[]
->
assert
false
in
aux
(
Abstr
(
_loc
,
"_"
,
t
,
fv
,
[
_loc
,
MVar
(
loc
,
pname
,
ptype
)
,
acc
]))
t
newfv
rest
|
[]
->
acc
in
aux
e
t
(
make_fv
[
0
,
x
]
1
p
)
(
List
.
rev
p
)
let
rec
make_fv
accu
nb
=
function
|
_
::
[]
|
[]
->
accu
|
(
_
,
name
,
_
)
::
rest
->
make_fv
(
accu
@
[
nb
,
name
])
(
nb
+
1
)
rest
in
let
rec
aux
acc
t
fv
=
function
|
(
loc
,
pname
,
ptype
)
::
[]
->
let
t
=
TArrow
(
ptype
,
t
)
in
Abstr
(
_loc
,
x
,
t
,
[]
,
[
_loc
,
MVar
(
loc
,
pname
,
ptype
)
,
acc
])
|
(
loc
,
pname
,
ptype
)
::
rest
->
let
t
=
TArrow
(
ptype
,
t
)
in
let
newfv
=
match
fv
with
|
_
::
rest
->
rest
|
[]
->
assert
false
in
aux
(
Abstr
(
_loc
,
"_"
,
t
,
fv
,
[
_loc
,
MVar
(
loc
,
pname
,
ptype
)
,
acc
]))
t
newfv
rest
|
[]
->
acc
in
aux
e
t
(
make_fv
[
0
,
x
]
1
p
)
(
List
.
rev
p
)
|
"fun"
;
t
=
type_id
;
b
=
LIST1
branch
->
Abstr
(
_loc
,
"_"
,
t
,
[]
,
b
)
|
"let"
;
x
=
LIDENT
;
":"
;
t
=
type_id
;
"="
;
v
=
SELF
;
"in"
;
e
=
SELF
;
":"
;
te
=
type_id
->
Match
(
_loc
,
v
,
t
,
[
_loc
,
MVar
(
_loc
,
x
,
t
)
,
e
])
|
"let"
;
x
=
LIDENT
;
":"
;
t
=
type_id
;
"="
;
v
=
SELF
;
"in"
;
e
=
SELF
;
":"
;
te
=
type_id
->
Match
(
_loc
,
v
,
t
,
[
_loc
,
MVar
(
_loc
,
x
,
t
)
,
e
])
|
"if"
;
e1
=
SELF
;
"then"
;
e2
=
SELF
->
let
b
=
[(
_loc
,
MBool
(
_loc
,
true
)
,
e2
);
(
_loc
,
MBool
(
_loc
,
false
)
,
Var
(
_loc
,
"`nil"
))]
in
Match
(
_loc
,
e1
,
Type
(
"Bool"
)
,
b
)
let
b
=
[
(
_loc
,
MBool
(
_loc
,
true
)
,
e2
);
(
_loc
,
MBool
(
_loc
,
false
)
,
Var
(
_loc
,
"`nil"
))]
in
Match
(
_loc
,
e1
,
Type
(
"Bool"
)
,
b
)
|
"if"
;
e1
=
SELF
;
"then"
;
e2
=
SELF
;
"else"
;
e3
=
SELF
->
let
b
=
[(
_loc
,
MBool
(
_loc
,
true
)
,
e2
);
(
_loc
,
MBool
(
_loc
,
false
)
,
e3
)]
in
Match
(
_loc
,
e1
,
Type
(
"Bool"
)
,
b
)
let
b
=
[
(
_loc
,
MBool
(
_loc
,
true
)
,
e2
);
(
_loc
,
MBool
(
_loc
,
false
)
,
e3
)]
in
Match
(
_loc
,
e1
,
Type
(
"Bool"
)
,
b
)
|
"match"
;
e
=
SELF
;
":"
;
t
=
type_id
;
"with"
;
b
=
LIST1
branch
->
Match
(
_loc
,
e
,
t
,
b
)
]
Match
(
_loc
,
e
,
t
,
b
)
]
|
"egal"
LEFTA
[
e1
=
SELF
;
"="
;
e2
=
SELF
->
Op
(
_loc
,
"="
,
e1
,
e2
)
]
|
"add"
LEFTA
...
...
@@ -96,8 +106,8 @@ module ExprParser = struct
|
"int"
[
x
=
INT
->
Int
(
_loc
,
int_of_string
x
)
]
|
"string"
[
x
=
STRING
->
String
(
_loc
,
x
)
]
|
"bool"
[
"`"
;
x
=
LIDENT
->
Bool
(
_loc
,
x
)
]
|
"subst"
NONA
[
e
=
SELF
;
"["
;
s
=
LIST0
sigma
SEP
","
;
"]"
->
Subst
(
_loc
,
e
,
s
)
]
|
"subst"
NONA
[
e
=
SELF
;
"["
;
s
=
LIST0
sigma
SEP
","
;
"]"
->
Subst
(
_loc
,
e
,
s
)
]
];
sigma
:
[[
"{"
;
l
=
LIST0
subst
SEP
";"
;
"}"
->
l
]];
...
...
@@ -106,8 +116,8 @@ module ExprParser = struct
param
:
[[
p
=
LIDENT
;
":"
;
t
=
type_id
->
_loc
,
p
,
t
]];
branch
:
[
"branch"
[
"|"
;
t
=
match_value
;
"->"
;
e
=
expression
->
_loc
,
t
,
e
]
branch
:
[
"branch"
[
"|"
;
t
=
match_value
;
"->"
;
e
=
expression
->
_loc
,
t
,
e
]
];
match_value
:
...
...
@@ -135,18 +145,21 @@ module ExprParser = struct
|
"empty"
[
"["
;
"]"
->
MVar
(
_loc
,
"`nil"
,
Type
(
"Any"
))
]
];
type_id
:
[
"atom_type"
[
t
=
UIDENT
->
Type
(
t
)
]
type_id
:
[
"atom_type"
[
t
=
UIDENT
->
Type
(
t
)
]
|
[
"'"
;
t1
=
UIDENT
;
"["
;
s
=
LIST0
sigma
SEP
","
;
"]"
->
PType
(
t1
,
s
)
]
|
[
"("
;
t
=
complex_type_id
;
")"
->
t
]
|
[
"["
;
t
=
complex_type_id
;
"]"
->
TSeq
(
t
)
]
];
complex_type_id
:
[
"complex_type"
LEFTA
[
t
=
UIDENT
->
Type
(
t
)
|
"("
;
t
=
SELF
;
")"
->
t
]
[
t
=
UIDENT
->
Type
(
t
)
|
"("
;
t
=
SELF
;
")"
->
t
]
|
[
"'"
;
t1
=
UIDENT
;
"["
;
s
=
LIST0
sigma
SEP
","
;
"]"
->
PType
(
t1
,
s
)
]
|
[
t1
=
SELF
;
"*"
;
t2
=
SELF
->
TPair
(
t1
,
t2
)
|
t1
=
SELF
;
"->"
;
t2
=
SELF
->
TArrow
(
t1
,
t2
)
]
|
[
t1
=
SELF
;
"|"
;
t2
=
SELF
->
TUnion
(
t1
,
t2
)
|
t1
=
SELF
;
"&"
;
t2
=
SELF
->
TInter
(
t1
,
t2
)
]
|
[
t1
=
SELF
;
"*"
;
t2
=
SELF
->
TPair
(
t1
,
t2
)
|
t1
=
SELF
;
"->"
;
t2
=
SELF
->
TArrow
(
t1
,
t2
)
]
|
[
t1
=
SELF
;
"|"
;
t2
=
SELF
->
TUnion
(
t1
,
t2
)
|
t1
=
SELF
;
"&"
;
t2
=
SELF
->
TInter
(
t1
,
t2
)
]
|
[
"!"
;
t
=
SELF
->
TNot
(
t
)
]
|
[
"["
;
t
=
complex_type_id
;
"]"
->
TSeq
(
t
)
]
];
...
...
tests/lambda/src/valueTests.ml
View file @
bafc0253
...
...
@@ -24,8 +24,23 @@ let run_test_compile msg expected totest =
let
tests_poly_abstr
=
[
"Test CDuce.lambda.const_abstr failed"
,
"
Abstraction(Dummy,,,,Sel((Int -> Int),{}))
"
,
""
,
"fun f x : 'A[{A/Int}] : 'A[{A/Int}] -> 2"
;
"Test CDuce.lambda.identity"
,
""
,
"(fun f x : 'A[{A/Int}] : 'A[{A/Int}] -> x).2"
;
"Test CDuce.lambda.let"
,
""
,
"let x : Int = 3 in x : Int"
;
"Test CDuce.lambda.apply"
,
""
,
"(fun f x : Int : Int -> x).2"
;
];;
let
tests_compile
=
"CDuce compile tests (Typed -> Lambda )"
>:::
...
...
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