Add support for cram tests.

This commit is contained in:
Olivier 2021-12-07 17:03:33 +01:00
parent 0be36b2b32
commit 55c0c2e7b1
20 changed files with 230 additions and 4 deletions

View File

@ -60,7 +60,7 @@ let letify xts =
aux xts
let suite_dir =
"../../../../client/test/suite/"
"../../../../client/test/suite.t/"
let open_uses ?(suite_dir=suite_dir) filenames =
let on_file typedecl_env filename =

View File

@ -503,7 +503,7 @@ let test_some () =
test_ok "some.midml" some
let test_some_pair () =
test_ok "some_pair.midml"
test_ok "some-pair.midml"
(ML.Variant (dummy_pos,
Datatype.Label "Some",
Some (ML.Tuple (dummy_pos, [id;id]))))
@ -518,7 +518,7 @@ let test_conscons () =
test_ok "conscons.midml" conscons
let test_match_tuple () =
test_ok "match_tuple.midml"
test_ok "match-tuple.midml"
(ML.Match
(dummy_pos,
ML.Tuple (dummy_pos, [id;unit]),

15
client/test/TestMidML.ml Normal file
View File

@ -0,0 +1,15 @@
open Test.CheckML
let test_ok filename =
let (datatype_env, t) = from_file ~suite_dir:"" filename in
let _ = Test.CheckML.test datatype_env t in ()
let parse_args () =
let usage_msg = "todo" in
let on_arg filename =
test_ok filename
in
Arg.parse [] on_arg usage_msg
let () =
parse_args ()

View File

@ -25,3 +25,11 @@
(modules TestMLRandom)
(package inferno-sample-client)
)
(executable
(name TestMidML)
(libraries client test)
(modules TestMidML))
(cram
(deps ./TestMidML.exe))

View File

@ -1,4 +1,4 @@
#use option.midml
let none =
let _ =
None

202
client/test/suite.t/run.t Normal file
View File

@ -0,0 +1,202 @@
Basics
$ cat id.midml
let id =
fun x -> x
$ ../TestMidML.exe id.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 -> fun (x : some . a0) -> x
Converting the System F term to de Bruijn style...
Type-checking the System F term...
$ cat idid.midml
let idid =
(fun x -> x) (fun x -> x)
$ ../TestMidML.exe idid.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 -> (fun (x : some . a0 -> a0) -> x) (fun (x : some . a0) -> x)
Converting the System F term to de Bruijn style...
Type-checking the System F term...
$ cat hole.midml
let hole =
... []
$ ../TestMidML.exe hole.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 -> <a0>...[]
Converting the System F term to de Bruijn style...
Type-checking the System F term...
Option type
$ cat none.midml
#use option.midml
let _ =
None
$ ../TestMidML.exe none.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 -> None<option a0> ()
Converting the System F term to de Bruijn style...
Type-checking the System F term...
$ cat some.midml
#use option.midml
let _ =
Some (fun x -> x)
$ ../TestMidML.exe some.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 -> Some<option (a0 -> a0)> (fun (x : some . a0) -> x)
Converting the System F term to de Bruijn style...
Type-checking the System F term...
$ cat some-pair.midml
#use option.midml
let _ =
Some (fun x -> x, fun x -> x)
$ ../TestMidML.exe some-pair.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 ->
FUN a1 ->
Some<option {a1 -> a1*a0 -> a0}> (
fun (x : some . a1) -> x,
fun (x : some . a0) -> x
)
Converting the System F term to de Bruijn style...
Type-checking the System F term...
List type
$ cat nil.midml
#use list.midml
let _ =
Nil
$ ../TestMidML.exe nil.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 -> Nil<list a0> ()
Converting the System F term to de Bruijn style...
Type-checking the System F term...
$ cat cons.midml
#use list.midml
let _ =
Cons (fun x -> x, Nil)
$ ../TestMidML.exe cons.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 ->
Cons<list (a0 -> a0)> (
fun (x : some . a0) -> x,
Nil<list (a0 -> a0)> ()
)
Converting the System F term to de Bruijn style...
Type-checking the System F term...
$ cat conscons.midml
#use list.midml
let _ =
Cons (
fun x -> x,
Cons (
fun x -> x,
Nil
)
)
$ ../TestMidML.exe conscons.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 ->
Cons<list (a0 -> a0)> (
fun (x : some . a0) -> x,
Cons<list (a0 -> a0)> (
fun (x : some . a0) -> x,
Nil<list (a0 -> a0)> ()
)
)
Converting the System F term to de Bruijn style...
Type-checking the System F term...
$ cat some-nil.midml
#use option.midml
#use list.midml
let _ =
Some Nil
$ ../TestMidML.exe some-nil.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 -> Some<option (list a0)> (Nil<list a0> ())
Converting the System F term to de Bruijn style...
Type-checking the System F term...
Pattern-matching
$ cat match-tuple.midml
let _ =
match (fun x -> x, ()) with (f, ()) -> f end
$ ../TestMidML.exe match-tuple.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 ->
match<a0 -> a0> (fun (x : some . a0) -> x, ()) with
| (f, ()) -> f
end
Converting the System F term to de Bruijn style...
Type-checking the System F term...
$ cat match-some-annotated.midml
#use option.midml
let _ =
match Some (fun x -> x) with
| None -> None
| (Some _ : some 'a. option 'a) -> None
end
$ ../TestMidML.exe match-some-annotated.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 ->
FUN a1 ->
match<option a0> Some<option (a1 -> a1)> (fun (x : some . a1) -> x) with
| None<option (a1 -> a1)> () -> None<option a0> ()
| (Some<option (a1 -> a1)> _ : some . option (a1 -> a1)) ->
None<option a0> ()
end
Converting the System F term to de Bruijn style...
Type-checking the System F term...

View File

@ -1,2 +1,3 @@
(lang dune 2.8)
(using menhir 2.0)
(cram enable)