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
a909f7aa
Commit
a909f7aa
authored
May 16, 2014
by
Pietro Abate
Browse files
Consolidate lambda ant typing tests to share common code
parent
056bf345
Changes
21
Hide whitespace changes
Inline
Side-by-side
tests/lambda/Makefile
View file @
a909f7aa
...
...
@@ -3,10 +3,10 @@ ROOTDIR ?= ../..
SRCDIR
?=
src
EXTDIR
?=
$(SRCDIR)
/externals
INEXTFILES
=
misc/custom.ml misc/encodings.ml misc/upool.ml misc/ns.ml
\
INEXTFILES
=
misc/custom.ml misc/encodings.ml misc/upool.ml misc/ns.ml
\
types/sortedList.ml types/ident.ml misc/html.ml types/sequence.ml
\
types/patterns.ml parser/cduce_loc.mli parser/cduce_loc.ml typing/typed.ml
\
types/builtin_defs.ml parser/ast.ml typing/typepat.mli typing/typepat.ml
\
types/builtin_defs.ml parser/ast.ml
parser/parser.ml parser/ulexer.ml
typing/typepat.mli typing/typepat.ml
\
types/externals.mli types/externals.ml typing/typer.ml
\
runtime/run_dispatch.ml runtime/explain.ml schema/schema_pcre.ml
\
schema/schema_xml.mli schema/schema_xml.ml schema/schema_common.mli
\
...
...
@@ -19,11 +19,11 @@ INEXTFILES = misc/custom.ml misc/encodings.ml misc/upool.ml misc/ns.ml\
runtime/value.ml schema/schema_types.mli schema/schema_validator.mli
\
schema/schema_builtin.mli schema/schema_builtin.ml schema/schema_validator.ml
\
compile/lambda.ml
EXTFILES
=
$
(
INEXTFILES:%
=
$(ROOTDIR)
/%
)
EXTFILES
=
$
(
INEXTFILES:%
=
$(ROOTDIR)
/%
)
RM
?=
rm
-f
OUT
?=
main
.native
OUTDEBUG
?=
main
.byte
OUT
?=
lambdaTests.native typedTests
.native
OUTDEBUG
?=
lambdaTests.byte typedTests
.byte
.PHONY
:
clean _import tests
...
...
tests/lambda/_tags
View file @
a909f7aa
<src>: include
<src/parse*>: pp(camlp4orf.opt), package(camlp4.lib)
<src/compute*>: pp(camlp4orf.opt), package(camlp4.lib, unix, netsys, str)
<src/
main
*>: pp(camlp4orf.opt), package(camlp4.lib, unix, netsys, str, oUnit, pcre, ulex, num, netstring)
<src/
*Tests
*>: pp(camlp4orf.opt), package(camlp4.lib, unix, netsys, str, oUnit, pcre, ulex, num, netstring)
<src/externals>: include
<src/externals/schema_*>: package(pcre, netcgi2)
<src/externals/cduce_loc*>: package(ulex), syntax(camlp4o)
<src/externals/{ulexer,parser}.*>: syntax(camlp4o), package(ulex)
tests/lambda/src/
main
.ml
→
tests/lambda/src/
lambdaTests
.ml
View file @
a909f7aa
File moved
tests/
typed/src/main
.ml
→
tests/
lambda/src/typedTests
.ml
View file @
a909f7aa
...
...
@@ -68,41 +68,18 @@ let run_test_typer msg expected totest =
let
expected
=
(
parse_typed
expected
)
in
let
totest
=
(
parse_expr
totest
)
in
assert_equal
~
msg
:
msg
~
printer
:
(
fun
x
->
Printer
.
typed_to_string
x
)
expected
totest
(*
"match" >:: ( fun test_ctxt ->
assert_equal ~msg:"Test CDuce.runtime.match.hard failed"
~printer:(fun x -> x) (load_file "tests/match/hard.ref")
(run_test "(fun ((Int -> Int) -> Int) | f ->
(match f 0 with | 0 -> 0 | _ -> 1)) (fun (Int -> Int) | x -> x+2)");
assert_equal ~msg:"Test CDuce.runtime.match.medium failed"
~printer:(fun x -> x) (load_file "tests/match/medium.ref")
(run_test "(fun (Int -> Int) | x ->
(match x with | 1 -> 3 | x -> x)) 2");
assert_equal ~msg:"Test CDuce.runtime.match.simple failed"
~printer:(fun x -> x) (load_file "tests/match/simple.ref")
(run_test "(fun (Int -> Int) | x -> (match x with | _ -> x)) 2");
);
"list" >:: ( fun test_ctxt ->
assert_equal ~msg:"Test CDuce.runtime.list.fold failed"
~printer:(fun x -> x) (load_file "tests/list/fold.ref")
(run_test "fun (Int -> [Int*] -> [Int*])
| x -> (fun ([Int*] -> [Int*])
| y -> [x] @ y)");
assert_equal ~msg:"Test CDuce.runtime.list.is_empty failed"
~printer:(fun x -> x) (load_file "tests/list/is_empty.ref")
(run_test "fun ([Int*] -> Bool) | [] -> `true | _ -> `false");
assert_equal ~msg:"Test CDuce.runtime.list.tail failed"
~printer:(fun x -> x) (load_file "tests/list/tail.ref")
(run_test "fun ([Int*] -> [Int*]) | [_ (rest::(Int*)
)]
->
rest
|
[]
->
[]
");
);
*)
(* (message, typed expr - expected, cduce expr) *)
let
tests_typer_list
=
[
(*
"Test CDuce.typed.fun.const",
"
fun
f
x
:
Int
:
Int
->
2
",
"
fun
f
(
Int
->
Int
)
x
->
2
";
"fun f x : Int : Int -> x",
"fun f (Int -> Int) x&Int -> x";
*)
"Test CDuce.typed.fun.identity"
,
"fun f x : 'A[{}] : 'A[{}] -> x"
,
"fun f (`$A -> `$A) x -> x"
;
]
let
tests_typer
=
"CDuce type tests (Ast -> Typed)"
>:::
...
...
tests/typed/Makefile
deleted
100644 → 0
View file @
056bf345
COMPILER
?=
ocamlbuild
ROOTDIR
?=
../..
SRCDIR
?=
src
EXTDIR
?=
$(SRCDIR)
/externals
INEXTFILES
=
misc/custom.ml misc/encodings.ml misc/upool.ml misc/ns.ml
\
types/sortedList.ml types/ident.ml misc/html.ml types/sequence.ml
\
types/patterns.ml parser/cduce_loc.mli parser/cduce_loc.ml typing/typed.ml
\
types/builtin_defs.ml parser/ast.ml parser/parser.ml parser/ulexer.ml typing/typepat.mli typing/typepat.ml
\
types/externals.mli types/externals.ml typing/typer.ml
\
runtime/run_dispatch.ml runtime/explain.ml schema/schema_pcre.ml
\
schema/schema_xml.mli schema/schema_xml.ml schema/schema_common.mli
\
schema/schema_common.ml runtime/eval.mli runtime/eval.ml
\
compile/compile.ml types/compunit.mli types/compunit.ml types/var.ml
\
types/boolVar.ml misc/imap.ml types/atoms.ml types/intervals.ml
\
types/chars.mli types/chars.ml misc/bool.mli misc/bool.ml types/types.mli
\
misc/stats.mli misc/stats.ml types/normal.mli types/normal.ml misc/pretty.mli
\
misc/pretty.ml types/types.ml compile/auto_pat.mli runtime/value.mli
\
runtime/value.ml schema/schema_types.mli schema/schema_validator.mli
\
schema/schema_builtin.mli schema/schema_builtin.ml schema/schema_validator.ml
\
compile/lambda.ml
EXTFILES
=
$
(
INEXTFILES:%
=
$(ROOTDIR)
/%
)
RM
?=
rm
-f
OUT
?=
main.native
OUTDEBUG
?=
main.byte
.PHONY
:
clean check test _import
all
:
_import
$(COMPILER)
-use-ocamlfind
$(OUT)
debug
:
_import
$(COMPILER)
-use-ocamlfind
-tag
debug
$(OUTDEBUG)
_import
:
@
echo
-n
"Copying external files..."
@
test
-d
$(EXTDIR)
||
mkdir
$(EXTDIR)
@
cp
$(EXTFILES)
$(EXTDIR)
@
echo
"done"
clean
:
$(COMPILER)
-clean
test
$(EXTDIR)
=
"src"
||
test
$(EXTDIR)
=
"."
||
$(RM)
-r
$(EXTDIR)
tests/typed/_tags
deleted
100644 → 0
View file @
056bf345
<src>: include
<src/parse*>: pp(camlp4orf.opt), package(camlp4.lib)
<src/compute*>: pp(camlp4orf.opt), package(camlp4.lib, unix, netsys, str)
<src/main*>: pp(camlp4orf.opt), package(camlp4.lib, unix, netsys, str, oUnit, pcre, ulex, num, netstring)
<src/externals>: include
<src/externals/schema_*>: package(pcre, netcgi2)
<src/externals/cduce_loc*>: package(ulex), syntax(camlp4o)
<src/externals/{ulexer,parser}.*>: syntax(camlp4o), package(ulex)
tests/typed/src/compute.ml
deleted
100644 → 0
View file @
056bf345
open
Parse
open
Camlp4
.
PreCast
(* Gives a unique id for a name *)
module
Locals
=
Map
.
Make
(
String
)
(* To throw in case of an unbound name *)
exception
Error
let
type_of_string
s
=
match
s
with
|
"Int"
->
Types
.
interval
[
Intervals
.
Any
]
|
"String"
->
Sequence
.
string
|
"Char"
->
Types
.
char
Chars
.
any
|
"Bool"
->
Types
.
atom
(
Atoms
.
cup
(
Atoms
.
atom
(
Atoms
.
V
.
mk_ascii
"false"
))
(
Atoms
.
atom
(
Atoms
.
V
.
mk_ascii
"true"
)))
|
"Any"
->
Types
.
any
|
_
->
Types
.
empty
let
rec
_to_typed
env
l
expr
=
let
open
Typed
in
(* From Camlp4 locations to CDuce locations *)
let
loc
=
caml_loc_to_cduce
(
get_loc
expr
)
in
match
expr
with
|
Subst
(
_
,
e
,
s
)
->
let
_
,
_
,
e
=
_to_typed
env
l
e
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
e
.
exp_typ
;
exp_descr
=
(
Subst
(
e
,
make_sigma
s
))
}
|
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
.
Arrow
.
apply
(
Types
.
Arrow
.
get
e1
.
exp_typ
)
e2
.
exp_typ
);
exp_descr
=
Apply
(
e1
,
e2
)
}
|
Abstr
(
origloc
,
fun_name
,
iface
,
fv
,
body
)
->
let
fname
=
match
fun_name
with
|
"_"
->
None
|
_
->
Some
(
0
,
fun_name
)
in
parse_abstr
env
l
origloc
fname
iface
fv
body
|
Match
(
_
,
e
,
t
,
b
)
->
let
b
,
btype
=
parse_branches
env
l
t
[]
Types
.
empty
b
in
let
t
=
type_of_ptype
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
=
btype
;
exp_descr
=
Match
(
exp_descr
,
brs
)
}
|
Pair
(
_
,
e1
,
e2
)
->
let
_
,
_
,
e1
=
_to_typed
env
l
e1
in
let
_
,
_
,
e2
=
_to_typed
env
l
e2
in
let
t
=
Types
.
times
(
Types
.
cons
e1
.
exp_typ
)
(
Types
.
cons
e2
.
exp_typ
)
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
t
;
exp_descr
=
Pair
(
e1
,
e2
)
}
|
Op
(
_
,
op
,
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
=
type_of_string
"Int"
;
exp_descr
=
Op
(
op
,
0
,
[
e1
;
e2
])
}
|
Var
(
origloc
,
vname
)
->
let
line
=
Loc
.
start_line
origloc
in
let
cbegin
=
Loc
.
start_off
origloc
-
Loc
.
start_bol
origloc
in
let
cend
=
Loc
.
stop_off
origloc
-
Loc
.
start_bol
origloc
in
if
vname
=
"`nil"
then
let
nil_atom
=
Atoms
.
V
.
mk_ascii
"nil"
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
(
Types
.
atom
(
Atoms
.
atom
nil_atom
));
exp_descr
=
(
Cst
(
Types
.
Atom
nil_atom
))
}
else
if
vname
=
"_"
then
(
Printf
.
eprintf
"File %s, line %d, characters %d-%d:
\n
Error: Invalid reference to special variable %s
\n
"
(
Loc
.
file_name
origloc
)
line
cbegin
cend
vname
;
raise
Error
)
else
let
index
,
vtype
=
try
Locals
.
find
vname
l
with
Not_found
->
Printf
.
eprintf
"File %s, line %d, characters %d-%d:
\n
Error: Unbound identifier %s
\n
"
(
Loc
.
file_name
origloc
)
line
cbegin
cend
vname
;
raise
Error
in
let
v
=
if
Types
.
no_var
vtype
then
Var
(
index
,
vname
)
else
TVar
(
index
,
vname
)
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
vtype
;
exp_descr
=
v
}
|
Int
(
_
,
i
)
->
let
i
=
Big_int
.
big_int_of_int
i
in
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
(
type_of_string
"Int"
);
exp_descr
=
Cst
(
Types
.
Integer
i
)
}
|
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"
);
exp_descr
=
Cst
s
}
|
Bool
(
origloc
,
b
)
->
let
t
=
Types
.
atom
(
Atoms
.
atom
(
Atoms
.
V
.
mk_ascii
"true"
))
in
let
f
=
Types
.
atom
(
Atoms
.
atom
(
Atoms
.
V
.
mk_ascii
"false"
))
in
match
b
with
|
"true"
->
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
t
;
exp_descr
=
Cst
(
Types
.
Atom
(
Atoms
.
V
.
mk_ascii
"true"
))
}
|
"false"
->
env
,
l
,
{
exp_loc
=
loc
;
exp_typ
=
f
;
exp_descr
=
Cst
(
Types
.
Atom
(
Atoms
.
V
.
mk_ascii
"false"
))
}
|
_
->
let
line
=
Loc
.
start_line
origloc
in
let
cbegin
=
Loc
.
start_off
origloc
-
Loc
.
start_bol
origloc
in
let
cend
=
Loc
.
stop_off
origloc
-
Loc
.
start_bol
origloc
in
Printf
.
eprintf
"File %s, line %d, characters %d-%d:
\n
Error: Unknown special term %s
\n
"
(
Loc
.
file_name
origloc
)
line
cbegin
cend
b
;
raise
Error
and
make_sigma
s
=
let
rec
aux2
acc
=
function
|
(
name
,
ptype
)
::
rest
->
aux2
(
Types
.
Tallying
.
CS
.
E
.
add
(
Var
.
mk
name
)
(
type_of_ptype
ptype
)
acc
)
rest
|
[]
->
acc
in
let
rec
aux
acc
=
function
|
l
::
rest
->
aux
(
acc
@
[
aux2
Types
.
Tallying
.
CS
.
E
.
empty
l
])
rest
|
[]
->
acc
in
aux
[]
s
and
type_of_sigma
x
s
=
let
rec
aux2
x
acc
=
function
|
[]
->
acc
|
(
id
,
t2
)
::
rest
when
id
=
x
->
aux2
x
(
Types
.
cap
acc
(
type_of_ptype
t2
))
rest
|
_
::
rest
->
aux2
x
acc
rest
in
let
rec
aux
x
acc
=
function
|
[]
->
acc
|
l
::
rest
->
aux
x
(
Types
.
cup
acc
(
aux2
x
Types
.
any
l
))
rest
in
aux
x
Types
.
empty
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
)
and
first_param
loc
iface
=
let
rec
_first_param
loc
accu
=
function
|
TArrow
(
t1
,
t2
)
->
t1
,
accu
@
[
type_of_ptype
t1
,
type_of_ptype
t2
]
|
TUnion
(
t1
,
t2
)
->
let
t1
,
acc1
=
first_param
loc
t1
in
let
t2
,
acc2
=
first_param
loc
t2
in
TInter
(
t1
,
t2
)
,
acc1
@
acc2
|
TInter
(
t1
,
t2
)
->
let
t1
,
acc1
=
first_param
loc
t1
in
let
t2
,
acc2
=
first_param
loc
t2
in
TUnion
(
t1
,
t2
)
,
acc1
@
acc2
|
_
->
let
line
=
Loc
.
start_line
loc
in
let
cbegin
=
Loc
.
start_off
loc
-
Loc
.
start_bol
loc
in
let
cend
=
Loc
.
stop_off
loc
-
Loc
.
start_bol
loc
in
let
fname
=
Loc
.
file_name
loc
in
Printf
.
eprintf
"File %s, line %d, characters %d-%d:
\n
Error: This type should be an arrow type
\n
"
fname
line
cbegin
cend
;
raise
Error
in
_first_param
loc
[]
iface
and
parse_abstr
env
l
loc
fun_name
iface
fv
body
=
let
fun_typ
=
type_of_ptype
iface
in
let
ptype
,
iface
=
first_param
loc
iface
in
let
l
=
(
match
fun_name
with
|
None
->
l
|
Some
(
id
,
name
)
->
Locals
.
add
name
(
id
,
fun_typ
)
l
)
in
let
b
,
btype
=
parse_branches
env
l
ptype
[]
Types
.
empty
body
in
let
brs
=
{
Typed
.
br_typ
=
type_of_ptype
ptype
;
br_accept
=
Types
.
any
;
br_branches
=
b
}
in
let
abstr
=
{
Typed
.
fun_name
=
fun_name
;
fun_iface
=
iface
;
fun_body
=
brs
;
fun_typ
=
fun_typ
;
fun_fv
=
fv
}
in
env
,
l
,
{
Typed
.
exp_loc
=
caml_loc_to_cduce
loc
;
exp_typ
=
fun_typ
;
exp_descr
=
Typed
.
Abstraction
(
abstr
)
}
and
make_patterns
t
fv
d
=
incr
Patterns
.
counter
;
{
Patterns
.
id
=
(
!
Patterns
.
counter
);
descr
=
(
t
,
fv
,
d
);
accept
=
(
Types
.
cons
t
);
fv
=
fv
}
and
parse_branches
env
l
toptype
acc
btype
=
function
|
(
loc
,
p
,
e
)
::
rest
->
let
t
,
d
,
fv
,
br_locals
,
br_used
=
parse_match_value
env
l
[]
toptype
p
in
let
line
=
Loc
.
start_line
loc
in
let
cbegin
=
Loc
.
start_off
loc
-
Loc
.
start_bol
loc
in
let
cend
=
Loc
.
stop_off
loc
-
Loc
.
start_bol
loc
in
let
_
,
_
,
br_body
=
_to_typed
env
br_locals
e
in
let
fname
=
Loc
.
file_name
loc
in
let
tpat
=
if
not
br_used
then
begin
Printf
.
eprintf
"File %s, line %d, characters %d-%d:
\n
Warning: This branch is not used
\n
"
fname
line
cbegin
cend
;
make_patterns
t
[]
d
end
else
make_patterns
t
fv
d
in
let
b
=
{
Typed
.
br_loc
=
caml_loc_to_cduce
loc
;
br_used
=
br_used
;
br_ghost
=
false
;
br_vars_empty
=
[]
;
br_vars_poly
=
[]
;
br_pat
=
tpat
;
br_body
=
br_body
}
in
parse_branches
env
l
toptype
(
acc
@
[
b
])
(
Types
.
cup
btype
br_body
.
Typed
.
exp_typ
)
rest
|
[]
->
acc
,
btype
and
get_fv
brs
=
let
rec
_fv_of_patt
=
function
|
MPair
(
_
,
m1
,
m2
)
->
(
_fv_of_patt
m1
)
@
(
_fv_of_patt
m2
)
|
MVar
(
_
,
mname
,
_
)
->
[
0
,
mname
]
|
_
->
[]
in
let
rec
_get_fv
accu
=
function
|
(
_
,
p
,
_
)
::
rest
->
_get_fv
(
accu
@
(
_fv_of_patt
p
))
rest
|
[]
->
accu
in
_get_fv
[]
brs
and
parse_match_value
env
l
list
toptype
=
function
|
MPair
(
_
,
m1
,
m2
)
->
let
top1
,
top2
=
(
match
toptype
with
|
TPair
(
t1
,
t2
)
->
t1
,
t2
|
TSeq
(
t
)
->
t
,
TSeq
(
t
)
|
_
->
Type
(
"Empty"
)
,
Type
(
"Empty"
))
in
let
t1
,
d1
,
list1
,
l
,
b1
=
parse_match_value
env
l
list
top1
m1
in
let
t2
,
d2
,
list2
,
l
,
b2
=
parse_match_value
env
l
list
top2
m2
in
Types
.
times
(
Types
.
cons
t1
)
(
Types
.
cons
t2
)
,
Patterns
.
Times
(
make_patterns
t1
list1
d1
,
make_patterns
t2
list2
d2
)
,
(
list1
@
list2
)
,
l
,
b1
&&
b2
;
|
MVar
(
_
,
mname
,
mtype
)
->
if
mname
=
"`nil"
then
let
nil_atom
=
Atoms
.
V
.
mk_ascii
"nil"
in
let
t
=
Types
.
atom
(
Atoms
.
atom
nil_atom
)
in
(
t
,
Patterns
.
Constr
(
t
)
,
list
,
l
,
true
)
else
if
mname
=
"_"
then
let
t
=
type_of_ptype
mtype
in
(
t
,
Patterns
.
Constr
(
t
)
,
list
,
l
,
true
)
else
let
lsize
=
Locals
.
cardinal
l
in
let
l
=
Locals
.
add
mname
(
lsize
,
type_of_ptype
mtype
)
l
in
let
list
=
list
@
[
lsize
,
mname
]
in
let
d1
=
Types
.
any
,
list
,
Patterns
.
Capture
(
lsize
,
mname
)
in
let
t2
=
type_of_ptype
mtype
in
let
d2
=
t2
,
[]
,
Patterns
.
Constr
(
t2
)
in
let
is_subtype
=
Types
.
subtype
t2
(
type_of_ptype
toptype
)
in
(
t2
,
Patterns
.
Cap
(
d1
,
d2
)
,
list
,
l
,
is_subtype
)
|
MInt
(
_
,
i
)
->
let
t
=
Types
.
constant
(
Types
.
Integer
(
Big_int
.
big_int_of_int
i
))
in
let
is_subtype
=
Types
.
subtype
(
type_of_string
"Int"
)
(
type_of_ptype
toptype
)
in
(
t
,
Patterns
.
Constr
(
t
)
,
list
,
l
,
is_subtype
)
|
MString
(
_
,
s
)
->
let
zero
=
Types
.
Integer
(
Big_int
.
big_int_of_int
0
)
in
let
t
=
Types
.
constant
(
Types
.
String
(
0
,
String
.
length
s
-
1
,
s
,
zero
))
in
let
is_subtype
=
Types
.
subtype
(
type_of_string
"String"
)
(
type_of_ptype
toptype
)
in
(
t
,
Patterns
.
Constr
(
t
)
,
list
,
l
,
is_subtype
)
|
MBool
(
origloc
,
b
)
->
let
t
=
match
b
with
|
"true"
->
Types
.
atom
(
Atoms
.
atom
(
Atoms
.
V
.
mk_ascii
"true"
))
|
"false"
->
Types
.
atom
(
Atoms
.
atom
(
Atoms
.
V
.
mk_ascii
"false"
))
|
_
->
let
line
=
Loc
.
start_line
origloc
in
let
cbegin
=
Loc
.
start_off
origloc
-
Loc
.
start_bol
origloc
in
let
cend
=
Loc
.
stop_off
origloc
-
Loc
.
start_bol
origloc
in
Printf
.
eprintf
"File %s, line %d, characters %d-%d:
\n
Error: Unknown special term %s
\n
"
(
Loc
.
file_name
origloc
)
line
cbegin
cend
b
;
raise
Error
in
let
is_subtype
=
Types
.
subtype
t
(
type_of_ptype
toptype
)
in
(
t
,
Patterns
.
Constr
(
t
)
,
list
,
l
,
is_subtype
)
let
arith_op
f
=
function
|
Value
.
Integer
(
x
)
::
Value
.
Integer
(
y
)
::
[]
->
Value
.
Integer
(
Big_int
.
big_int_of_int
(
f
(
Big_int
.
int_of_big_int
x
)
(
Big_int
.
int_of_big_int
y
)))
|
_
->
raise
Error
let
equal
=
function
|
Value
.
Integer
(
x
)
::
Value
.
Integer
(
y
)
::
[]
->
let
b
=
if
Big_int
.
int_of_big_int
x
=
Big_int
.
int_of_big_int
y
then
"true"
else
"false"
in
Value
.
Atom
(
Atoms
.
V
.
mk_ascii
b
)
|
_
->
raise
Error
let
concat
=
let
rec
add_to_tail
y
=
function
|
Value
.
Pair
(
x
,
nil
,
s
)
->
if
nil
=
Value
.
Atom
(
Atoms
.
V
.
mk_ascii
"nil"
)
then
Value
.
Pair
(
x
,
y
,
s
)
else
Value
.
Pair
(
x
,
add_to_tail
y
nil
,
s
)
|
_
->
raise
Error
in
function
|
(
Value
.
Pair
(
_
,
_
,
_
)
as
x
)
::
(
Value
.
Pair
(
_
)
as
y
)
::
[]
->
add_to_tail
y
x
|
x
::
y
::
[]
->
if
x
=
Value
.
Atom
(
Atoms
.
V
.
mk_ascii
"nil"
)
then
y
else
if
y
=
Value
.
Atom
(
Atoms
.
V
.
mk_ascii
"nil"
)
then
x
else
raise
Error
|
_
->
raise
Error
let
to_typed
expr
=
Eval
.
register_op
"+"
(
arith_op
(
+
));
Eval
.
register_op
"-"
(
arith_op
(
-
));
Eval
.
register_op
"*"
(
arith_op
(
*
));
Eval
.
register_op
"/"
(
arith_op
(
/
));
Eval
.
register_op
"%"
(
arith_op
(
mod
));
Eval
.
register_op
"="
equal
;
Eval
.
register_op
"@"
concat
;
let
env
,
_
,
expr
=
_to_typed
Compile
.
empty_toplevel
Locals
.
empty
expr
in
env
,
expr
tests/typed/src/parse.ml
deleted
100644 → 0
View file @
056bf345
open
Printf
open
Camlp4
.
PreCast
type
expr
=
|
Subst
of
Loc
.
t
*
expr
*
(
string
*
ptype
)
list
list
|
Apply
of
Loc
.
t
*
expr
*
expr
|
Abstr
of
Loc
.
t
*
fun_name
*
ptype
*
fv
*
branches
|
Match
of
Loc
.
t
*
expr
*
ptype
*
branches
|
Pair
of
Loc
.
t
*
expr
*
expr
|
Op
of
Loc
.
t
*
string
*
expr
*
expr
|
Var
of
Loc
.
t
*
string
|
Int
of
Loc
.
t
*
int
|
String
of
Loc
.
t
*
string
|
Bool
of
Loc
.
t
*
string
and
fun_name
=
string
and
fv
=
(
int
*
string
)
list
and
branches
=
(
Loc
.
t
*
match_value
*
expr
)
list
and
match_value
=
|
MPair
of
Loc
.
t
*
match_value
*
match_value
|
MVar
of
Loc
.
t
*
string
*
ptype
|
MInt
of
Loc
.
t
*
int
|
MString
of
Loc
.
t
*
string
|
MBool
of
Loc
.
t
*
string
and
ptype
=
|
Type
of
string
|
PType
of
string
*
(
string
*
ptype
)
list
list
|
TPair
of
ptype
*
ptype
|
TUnion
of
ptype
*
ptype
|
TInter
of
ptype
*
ptype
|
TNot
of
ptype
|
TArrow
of
ptype
*
ptype
|
TSeq
of
ptype
module
ExprParser
=
struct
let
exp_eoi
=
Gram
.
Entry
.
mk
"exp_eoi"
EXTEND
Gram
GLOBAL
:
exp_eoi
;
exp_eoi
:
[[
e
=
expression
;
`EOI
->
e
]];
expression
:
[
"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
)
|
"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
])
|
"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
)
|
"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
)
|
"match"
;
e
=
SELF
;
":"
;
t
=
type_id
;
"with"
;
b
=
LIST1
branch
->
Match
(
_loc
,
e
,
t
,
b
)
]
|
"egal"
LEFTA
[
e1
=
SELF
;
"="
;
e2
=
SELF
->
Op
(
_loc
,
"="
,
e1
,
e2
)
]
|
"add"
LEFTA
[
e1
=
SELF
;
"+"
;
e2
=
SELF
->
Op
(
_loc
,
"+"
,
e1
,
e2
)
|
e1
=
SELF
;
"-"
;
e2
=
SELF
->
Op
(
_loc
,
"-"
,
e1
,
e2
)
]
|
"mult"
LEFTA
[
e1
=
SELF
;
"*"
;
e2
=
SELF
->
Op
(
_loc
,
"*"
,
e1
,
e2
)
|
e1
=
SELF
;
"/"
;
e2
=
SELF
->
Op
(
_loc
,
"/"
,
e1
,
e2
)
|
e1
=
SELF
;
"%"
;
e2
=
SELF
->
Op
(
_loc
,
"%"
,
e1
,
e2
)
]
|
"concat"
LEFTA
[
e1
=
SELF
;
"@"
;
e2
=
SELF
->
Op
(
_loc
,
"@"
,
e1
,
e2
)
]
|
"pair"
LEFTA
[
e1
=
SELF
;
","
;
e2
=
SELF
->
Pair
(
_loc
,
e1
,
e2
)
]
|
"apply"
[
e1
=
SELF
;
"."
;
e2
=
SELF
->
Apply
(
_loc
,
e1
,
e2
)
]
|
"list"
LEFTA
[
"["
;
le
=
LIST0
SELF
SEP
";"
;
"]"
->
let
rec
make_seq
res
=
function
|
e
::
rest
->
make_seq
(
Pair
(
_loc
,
e
,
res
))
rest
|
[]
->
res
in
make_seq
(
Var
(
_loc
,
"`nil"
))
(
List
.
rev
le
)
]
|
"paren"
[
"("
;
e
=
SELF
;
")"
->
e
]
|
"var"
[
x
=
LIDENT
->
Var
(
_loc
,
x
)
]
|
"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
)
]
];
sigma
:
[[
"{"
;
l
=
LIST0
subst
SEP
";"
;
"}"
->
l
]];
subst
:
[[
x
=
UIDENT
;
"/"
;
t
=
type_id
->
x
,
t
]];
param
:
[[
p
=
LIDENT
;
":"
;
t
=
type_id
->
_loc
,
p
,
t
]];
branch
:
[
"branch"
[
"|"
;
t
=
match_value
;
"->"
;
e
=
expression
->
_loc
,
t
,
e
]
];
match_value
:
[
"pair"
LEFTA
[
e1
=
SELF
;
","
;
e2
=
SELF
->
MPair
(
_loc
,
e1
,
e2
)
]
|
"headlist"
[
e1
=
SELF
;
"::"
;
e2
=
SELF
->
MPair
(
_loc
,
e1
,
e2
)
]
|
"paren"
[
"("
;
e
=
SELF
;
")"
->
e
]
|
"var"
[
x
=
LIDENT
;
":"
;
t
=
type_id
->
MVar
(
_loc
,
x
,
t
)
]
|
"int"
[
x
=
INT
->
MInt
(
_loc
,
int_of_string
x
)
]
|
"string"
[
x
=
STRING
->
MString
(
_loc
,
x
)
]
|
"bool"
[
"`"
;
x
=
LIDENT
->
MBool
(
_loc
,
x
)
]
|
"empty"
[
"["
;
"]"
->
MVar
(
_loc
,
"`nil"
,
Type
(
"Any"
))
]
];