parent
ac406c7089
commit
4ff51e7901
@ -0,0 +1,15 @@
|
||||
open Test.CheckML
|
||||
|
||||
let test_ok filename =
|
||||
let (datatype_env, t) = from_file 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 ()
|
@ -1,4 +1,4 @@
|
||||
#use option.midml
|
||||
|
||||
let none =
|
||||
let _ =
|
||||
None
|
@ -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...
|
@ -1,2 +1,3 @@
|
||||
(lang dune 2.8)
|
||||
(using menhir 2.0)
|
||||
(cram enable)
|
Loading…
Reference in new issue