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
a16f8fff
Commit
a16f8fff
authored
Apr 09, 2014
by
Julien Lopez
Browse files
[TESTS][LAMBDA] Lot of fixes in types; printer for typed complete; 9/10 tests
pass (missing curryfication)
parent
632727ee
Changes
5
Hide whitespace changes
Inline
Side-by-side
tests/lambda/src/compute.ml
View file @
a16f8fff
...
...
@@ -13,13 +13,17 @@ exception Error
(* TODO: We will need a much better representation of types and a much better
function when we'll add union types and polymorphism. *)
let
is_subtype
_
_
=
true
(*t1 t2 = if String.compare t1 t2 = 0 then true else false*)
let
is_subtype
t1
t2
=
if
String
.
compare
t1
t2
=
0
then
true
else
false
let
type_of_string
s
=
match
s
with
|
"Int"
->
interval
[
Intervals
.
Any
]
|
_
->
Types
.
empty
let
rec
type_of_iface
iface
res
=
match
iface
with
|
(
ptype
,
rtype
)
::
rest
->
type_of_iface
rest
(
cup
(
arrow
(
cons
ptype
)
(
cons
rtype
))
res
)
|
[]
->
res
let
rec
_to_typed
env
l
expr
=
(* From Camlp4 locations to CDuce locations *)
let
loc
=
caml_loc_to_cduce
(
get_loc
expr
)
in
...
...
@@ -27,20 +31,20 @@ let rec _to_typed env l expr =
|
Parse
.
Apply
(
_
,
e1
,
e2
)
->
let
_
,
_
,
e1
=
_to_typed
env
l
e1
in
let
_
,
_
,
e2
=
_to_typed
env
l
e2
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
Types
.
empty
;
exp_descr
=
Apply
(
e1
,
e2
)
}
|
Abstr
(
_
,
fun_name
,
params
,
r
eturn_
type
,
body
)
->
parse_abstr
env
l
loc
(
Some
(
0
,
fun_name
))
params
r
eturn_
type
body
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
empty
;
exp_descr
=
Apply
(
e1
,
e2
)
}
|
Abstr
(
_
,
fun_name
,
params
,
rtype
,
body
)
->
parse_abstr
env
l
loc
(
Some
(
0
,
fun_name
))
params
rtype
body
|
Match
(
_
,
e
,
t
,
b
)
->
let
b
=
parse_branches
env
l
t
b
[]
in
(* TODO: Fix br_typ *)
let
brs
=
{
br_typ
=
Types
.
empty
;
br_accept
=
Types
.
empty
;
br_branches
=
b
}
in
let
t
=
type_of_string
t
in
let
brs
=
{
br_typ
=
t
;
br_accept
=
t
;
br_branches
=
b
}
in
let
_
,
_
,
exp_descr
=
_to_typed
env
l
e
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
Types
.
empty
;
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
t
;
exp_descr
=
Match
(
exp_descr
,
brs
)
}
|
Pair
(
_
,
e1
,
e2
)
->
let
_
,
_
,
exp_descr1
=
_to_typed
env
l
e1
in
let
_
,
_
,
exp_descr2
=
_to_typed
env
l
e2
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
Types
.
empty
;
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
empty
;
exp_descr
=
Pair
(
exp_descr1
,
exp_descr2
)
}
|
Var
(
origloc
,
vname
)
->
let
line
=
Loc
.
start_line
origloc
in
...
...
@@ -49,51 +53,59 @@ let rec _to_typed env l expr =
let
index
=
(
try
Locals
.
find
vname
l
with
Not_found
->
Printf
.
eprintf
"File %s, line %d, characters %d-%d:
\n
Unbound identifier %s
\n
"
(
Loc
.
file_name
origloc
)
line
cbegin
cend
vname
;
raise
Error
)
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
Types
.
empty
;
exp_descr
=
Var
(
index
,
vname
)
}
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
empty
;
exp_descr
=
Var
(
index
,
vname
)
}
|
Int
(
_
,
i
)
->
let
i
=
Big_int
.
big_int_of_int
i
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
T
ype
s
.
empty
;
exp_descr
=
Cst
(
Types
.
Integer
i
)
}
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
(
t
ype
_of_string
"Int"
)
;
exp_descr
=
Cst
(
Integer
i
)
}
|
String
(
_
,
s
)
->
let
s
=
Types
.
String
(
0
,
(
String
.
length
s
)
-
1
,
s
,
Types
.
Integer
(
Big_int
.
big_int_of_int
0
))
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
Types
.
empty
;
exp_descr
=
Cst
s
}
let
s
=
String
(
0
,
(
String
.
length
s
)
-
1
,
s
,
Integer
(
Big_int
.
big_int_of_int
0
))
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
(
type_of_string
"String"
);
exp_descr
=
Cst
s
}
and
parse_abstr
env
l
loc
fun_name
params
r
eturn_
type
body
=
let
rec
_parse_abstr
env
l
fv
loc
fun_name
params
r
eturn_
type
body
nb
=
and
parse_abstr
env
l
loc
fun_name
params
rtype
body
=
let
rec
_parse_abstr
env
l
fv
loc
fun_name
params
rtype
body
nb
=
let
brloc
=
caml_loc_to_cduce
(
get_loc
body
)
in
let
empty
,
env
,
l
,
nfv
,
iface
,
rest
=
parse_iface
env
l
params
[]
nb
[]
in
let
empty
,
env
,
l
,
nfv
,
iface
,
rest
=
parse_iface
env
l
params
[]
nb
[]
rtype
in
let
node
=
make_node
(
fv
@
nfv
)
nfv
in
let
body
=
if
empty
then
let
_
,
_
,
body
=
_to_typed
env
l
body
in
body
else
let
_
,
_
,
body
=
_parse_abstr
env
l
(
fv
@
nfv
)
loc
None
rest
r
eturn_
type
body
(
nb
+
1
)
in
body
rtype
body
(
nb
+
1
)
in
body
in
let
b
=
{
br_loc
=
brloc
;
br_used
=
true
;
br_ghost
=
false
;
br_vars_empty
=
[]
;
br_pat
=
node
;
br_body
=
body
}
in
let
brs
=
{
br_typ
=
Types
.
empty
;
br_accept
=
Types
.
empty
;
br_branches
=
[
b
]
}
in
let
brs
=
{
br_typ
=
rtype
;
br_accept
=
any
;
br_branches
=
[
b
]
}
in
let
fun_typ
=
type_of_iface
iface
Types
.
empty
in
let
abstr
=
{
fun_name
=
fun_name
;
fun_iface
=
iface
;
fun_body
=
brs
;
fun_typ
=
Types
.
empty
;
fun_fv
=
[]
}
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
Types
.
empty
;
exp_descr
=
Abstraction
(
abstr
)
}
fun_typ
=
fun_typ
;
fun_fv
=
[]
}
in
(* TODO: Fix exp_typ *)
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
any
;
exp_descr
=
Abstraction
(
abstr
)
}
in
_parse_abstr
env
l
[]
loc
fun_name
params
return_
type
body
0
_parse_abstr
env
l
[]
loc
fun_name
params
(
type_of_string
r
type
)
body
0
and
make_node
fv
nfv
=
let
d
=
(
match
nfv
with
|
el
::
rest
->
Patterns
.
Capture
(
el
)
|
[]
->
Patterns
.
Dummy
)
in
incr
Patterns
.
counter
;
{
Patterns
.
id
=
(
!
Patterns
.
counter
);
Patterns
.
descr
=
(
Types
.
any
,
fv
,
d
);
Patterns
.
accept
=
(
Types
.
make
()
);
Patterns
.
fv
=
fv
}
make_patterns
any
fv
d
and
parse_iface
env
l
params
fv
nb
iface
=
match
params
with
|
(
_
,
pname
,
_
)
::
[]
->
true
,
env
,
(
Locals
.
add
pname
nb
l
)
,
(
fv
@
[
nb
,
pname
])
,
(
iface
@
[
Types
.
empty
,
Types
.
empty
])
,
[]
|
(
_
,
pname
,
_
)
::
rest
->
false
,
env
,
(
Locals
.
add
pname
nb
l
)
,
(
fv
@
[
nb
,
pname
])
,
(
iface
@
[
Types
.
empty
,
Types
.
empty
])
,
rest
and
parse_iface
env
l
params
fv
nb
iface
rtype
=
match
params
with
|
(
_
,
pname
,
ptype
)
::
[]
->
true
,
env
,
(
Locals
.
add
pname
nb
l
)
,
(
fv
@
[
nb
,
pname
])
,
(
iface
@
[
type_of_string
ptype
,
rtype
])
,
[]
|
(
_
,
pname
,
ptype
)
::
rest
->
false
,
env
,
(
Locals
.
add
pname
nb
l
)
,
(
fv
@
[
nb
,
pname
])
,
(
iface
@
[
itype
rest
(
type_of_string
ptype
)
,
rtype
])
,
rest
|
[]
->
true
,
env
,
l
,
fv
,
iface
,
[]
and
itype
iface
res
=
match
iface
with
|
(
_
,
_
,
t
)
::
rest
->
itype
rest
(
arrow
(
cons
res
)
(
cons
(
type_of_string
t
)))
|
[]
->
res
and
parse_branches
env
l
toptype
brs
res
=
match
brs
with
|
(
loc
,
p
,
e
)
::
rest
->
let
brloc
=
caml_loc_to_cduce
loc
in
...
...
@@ -118,16 +130,16 @@ and parse_branches env l toptype brs res = match brs with
and
make_patterns
t
fv
d
=
incr
Patterns
.
counter
;
{
Patterns
.
id
=
(
!
Patterns
.
counter
);
Patterns
.
descr
=
(
t
,
fv
,
d
);
Patterns
.
accept
=
(
Types
.
make
()
);
fv
=
fv
}
Patterns
.
accept
=
(
cons
t
);
fv
=
fv
}
and
parse_match_value
env
l
list
p
toptype
=
match
p
with
(* TODO: Allow pairs in types *)
|
MPair
(
_
)
->
Types
.
empty
,
Patterns
.
Dummy
,
list
,
l
,
false
;
|
MPair
(
_
)
->
empty
,
Patterns
.
Dummy
,
list
,
l
,
false
;
|
MVar
(
_
,
mname
,
mtype
)
->
let
lsize
=
Locals
.
cardinal
l
in
let
l
=
Locals
.
add
mname
lsize
l
in
let
list
=
list
@
[
lsize
,
mname
]
in
let
d1
=
Types
.
any
,
list
,
Patterns
.
Capture
(
lsize
,
mname
)
in
let
d1
=
any
,
list
,
Patterns
.
Capture
(
lsize
,
mname
)
in
let
t2
=
type_of_string
mtype
in
let
d2
=
t2
,
[]
,
Patterns
.
Constr
(
t2
)
in
t2
,
Patterns
.
Cap
(
d1
,
d2
)
,
list
,
l
,
is_subtype
toptype
mtype
...
...
@@ -140,5 +152,5 @@ and parse_match_value env l list p toptype = match p with
t
,
Patterns
.
Constr
(
t
)
,
list
,
l
,
is_subtype
toptype
"String"
let
to_typed
expr
=
let
env
,
_
,
expr
=
_to_typed
empty_toplevel
Locals
.
empty
expr
in
let
env
,
l
,
expr
=
_to_typed
empty_toplevel
Locals
.
empty
expr
in
env
,
expr
tests/lambda/src/main.ml
View file @
a16f8fff
...
...
@@ -13,24 +13,25 @@ let load_file f =
close_in
ic
;
s
let
rec
typed_to_string
e
=
match
e
with
|
Typed
.
Forget
(
e
,
_
)
->
"Forget("
^
typed_to_string
e
.
Typed
.
exp_descr
^
")"
|
Typed
.
Check
(
_
,
e
,
_
)
->
"Check("
^
typed_to_string
e
.
Typed
.
exp_descr
^
")"
let
rec
typed_to_string
e
=
"{typ:"
^
(
Types
.
Print
.
to_string
e
.
Typed
.
exp_typ
)
^
"; descr="
^
(
match
e
.
Typed
.
exp_descr
with
|
Typed
.
Forget
(
e
,
_
)
->
"Forget("
^
typed_to_string
e
^
")"
|
Typed
.
Check
(
_
,
e
,
_
)
->
"Check("
^
typed_to_string
e
^
")"
|
Typed
.
Var
(
id
,
name
)
->
"Var("
^
(
string_of_int
(
Upool
.
int
id
))
^
", "
^
(
Encodings
.
Utf8
.
to_string
name
)
^
")"
|
Typed
.
ExtVar
(
_
,
(
id
,
name
)
,
_
)
->
"ExtVar("
^
(
string_of_int
(
Upool
.
int
id
))
^
", "
^
(
Encodings
.
Utf8
.
to_string
name
)
^
")"
|
Typed
.
Apply
(
e1
,
e2
)
->
"("
^
typed_to_string
e1
.
Typed
.
exp_descr
^
").("
^
(
typed_to_string
e2
.
Typed
.
exp_descr
)
^
")"
|
Typed
.
Apply
(
e1
,
e2
)
->
"("
^
typed_to_string
e1
^
").("
^
(
typed_to_string
e2
)
^
")"
|
Typed
.
Abstraction
(
abstr
)
->
"Abstraction("
^
(
abst
abstr
)
^
")"
|
Typed
.
Cst
(
cst
)
->
const
cst
|
Typed
.
Pair
(
e1
,
e2
)
->
"("
^
(
typed_to_string
e1
.
Typed
.
exp_descr
)
^
", "
^
(
typed_to_string
e2
.
Typed
.
exp_descr
)
^
")"
|
Typed
.
Pair
(
e1
,
e2
)
->
"("
^
(
typed_to_string
e1
)
^
", "
^
(
typed_to_string
e2
)
^
")"
|
Typed
.
String
(
_
,
_
,
s
,
_
)
->
"
\"
"
^
(
Encodings
.
Utf8
.
to_string
s
)
^
"
\"
"
|
Typed
.
Match
(
e
,
b
)
->
"Match("
^
(
typed_to_string
e
.
Typed
.
exp_descr
)
^
","
^
(
branches
b
)
^
")"
|
_
->
assert
false
|
Typed
.
Match
(
e
,
b
)
->
"Match("
^
(
typed_to_string
e
)
^
","
^
(
branches
b
)
^
")"
|
_
->
assert
false
)
^
"}"
and
const
cst
=
match
cst
with
|
Types
.
Integer
(
i
)
->
"Integer("
^
(
Intervals
.
V
.
to_string
i
)
^
")"
...
...
@@ -44,7 +45,7 @@ and abst abstr = (match abstr.Typed.fun_name with
|
Some
(
id
,
name
)
->
"name:("
^
(
string_of_int
(
Upool
.
int
id
))
^
", "
^
(
Encodings
.
Utf8
.
to_string
name
)
|
None
->
"name:<none>"
)
^
"),
\n
iface:["
^
(
iface
abstr
.
Typed
.
fun_iface
)
^
"]
\n
body:["
^
(
branches
abstr
.
Typed
.
fun_body
)
^
"], "
^
"]
,
\n
body:["
^
(
branches
abstr
.
Typed
.
fun_body
)
^
"], "
^
"typ:"
^
(
Types
.
Print
.
to_string
abstr
.
Typed
.
fun_typ
)
^
", fv:["
^
(
fv_to_string
abstr
.
Typed
.
fun_fv
)
^
"]"
...
...
@@ -56,7 +57,7 @@ and iface list = match list with
|
[]
->
""
and
branches
brs
=
"typ:"
^
(
Types
.
Print
.
to_string
brs
.
Typed
.
br_typ
)
^
", accept:"
^
(
Types
.
Print
.
to_string
brs
.
Typed
.
br_accept
)
^
", accept:"
^
(
Types
.
Print
.
to_string
brs
.
Typed
.
br_accept
)
^
", branches:"
^
(
branch
brs
.
Typed
.
br_branches
)
and
branch
brs
=
match
brs
with
...
...
@@ -64,17 +65,19 @@ and branch brs = match brs with
^
(
string_of_bool
br
.
Typed
.
br_ghost
)
^
"; br_vars_empty:["
^
(
fv_to_string
br
.
Typed
.
br_vars_empty
)
^
"];
\n
pat:{"
^
(
node
br
.
Typed
.
br_pat
)
^
"};
\n
body:"
^
(
typed_to_string
br
.
Typed
.
br_body
.
Typed
.
exp_descr
)
^
"}"
^
(
typed_to_string
br
.
Typed
.
br_body
)
^
"}"
|
br
::
rest
->
"
\n
{used:"
^
(
string_of_bool
br
.
Typed
.
br_used
)
^
"; ghost:"
^
(
string_of_bool
br
.
Typed
.
br_ghost
)
^
"; br_vars_empty:["
^
(
fv_to_string
br
.
Typed
.
br_vars_empty
)
^
"];
\n
pat:{"
^
(
node
br
.
Typed
.
br_pat
)
^
"};
\n
body:"
^
(
t
ype
d_
to_string
br
.
Typed
.
br_body
.
Typed
.
exp_
descr
)
^
"
}
, "
^
(
branch
rest
)
^
(
node
br
.
Typed
.
br_pat
)
^
"};
\n
body:
{typ:
"
^
(
T
ype
s
.
Print
.
to_string
br
.
Typed
.
br_body
.
Typed
.
exp_
typ
)
^
",
descr:
"
^
(
typed_to_string
br
.
Typed
.
br_body
)
^
"}},"
^
(
branch
rest
)
|
[]
->
""
and
node
node
=
"id:"
^
(
string_of_int
node
.
Patterns
.
id
)
^
"; descr:["
^
(
descr
node
.
Patterns
.
descr
)
^
"]; fv:["
^
(
descr
node
.
Patterns
.
descr
)
^
"]; accept:[id:"
^
(
string_of_int
(
Types
.
id
node
.
Patterns
.
accept
))
^
"; descr:"
^
(
Types
.
Print
.
to_string
(
Types
.
descr
node
.
Patterns
.
accept
))
^
"]; fv:["
^
(
fv_to_string
node
.
Patterns
.
fv
)
^
"]"
and
descr
(
t
,
fv
,
d
)
=
(
Types
.
Print
.
to_string
t
)
...
...
@@ -102,6 +105,24 @@ and fv_to_string fv = match fv with
^
(
Encodings
.
Utf8
.
to_string
name
)
^
"), "
^
(
fv_to_string
rest
)
|
[]
->
""
let
vloc_to_string
vloc
=
match
vloc
with
|
Lambda
.
Local
(
i
)
->
"Local("
^
(
string_of_int
i
)
^
")"
|
Lambda
.
Env
(
i
)
->
"Env("
^
(
string_of_int
i
)
^
")"
|
Lambda
.
Ext
(
_
,
i
)
->
"Ext(?, "
^
(
string_of_int
i
)
^
")"
|
Lambda
.
External
(
_
,
i
)
->
"External(?, "
^
(
string_of_int
i
)
^
")"
|
Lambda
.
Builtin
(
s
)
->
"Builtin("
^
s
^
")"
|
Lambda
.
Global
(
i
)
->
"Global("
^
(
string_of_int
i
)
^
")"
|
Lambda
.
Dummy
->
"Dummy"
let
print_binding
key
value
=
match
key
with
|
(
id
,
name
)
->
Printf
.
printf
"((%d, %s),"
(
Upool
.
int
id
)
(
Encodings
.
Utf8
.
to_string
name
);
Printf
.
printf
"%s"
(
vloc_to_string
value
);
Printf
.
printf
")
\n
"
let
print_env
env
=
match
Ident
.
Env
.
is_empty
env
with
|
true
->
Printf
.
printf
"<empty>
\n
"
|
false
->
Ident
.
Env
.
iter
print_binding
env
let
rec
print_value
v
=
match
v
with
|
Value
.
Pair
(
v1
,
v2
)
->
printf
"("
;
print_value
v1
;
printf
", "
;
print_value
v2
;
printf
")"
...
...
@@ -127,7 +148,7 @@ in
try
let
expr
=
ExprParser
.
of_string
str
file
in
let
env
,
texpr
=
Compute
.
to_typed
expr
in
eprintf
"%s
\n
"
(
typed_to_string
texpr
.
exp_descr
);
(*
eprintf "%s\n" (typed_to_string texpr);
*)
let
evalexpr
=
Compile
.
compile_eval_expr
env
texpr
in
print_value
evalexpr
;
printf
"
\n
"
with
...
...
tests/lambda/tests/eval/refs/match_medium.ref
View file @
a16f8fff
1
2
tests/lambda/tests/eval/refs/match_simple.ref
View file @
a16f8fff
3
1
File ./tests/eval/tests/match_simple.test, line 1, characters 28-46:
Warning: This branch is not used
tests/lambda/tests/eval/tests/match_medium.test
View file @
a16f8fff
(
fun
f
x
:
Int
:
Int
->
match
x
:
Int
with
|
1
->
0
|
x
:
Int
->
x
)
.
1
(
fun
f
x
:
Int
:
Int
->
match
x
:
Int
with
|
1
->
3
|
x
:
Int
->
x
)
.
2
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