Compare commits

...

5 Commits

@ -326,6 +326,17 @@ let convert_annot env ((flex_vars, ty) : ML.type_annotation)
(* -------------------------------------------------------------------------- *)
(* [get_pos t] returns the range of [t]. *)
let get_pos t =
match t with
| ML.Var (pos, _) | ML.Hole (pos, _) | ML.Abs (pos, _, _)
| ML.App (pos, _, _) | ML.Let (pos, _, _, _) | ML.Annot (pos, _, _)
| ML.Tuple (pos, _) | ML.LetProd (pos, _, _, _)
| ML.Variant (pos, _, _) | ML.Match (pos, _, _)
-> pos
(* -------------------------------------------------------------------------- *)
(* We will need a type environment to keep trace of term variables that must
be bound to solver variables during typechecking of patterns *)
@ -346,6 +357,8 @@ type type_env = (ML.tevar * variable) list
let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.nominal_term co
=
let rec hastype t w =
let pos = get_pos t in
correlate pos @@
match t with
(* Variable. *)
| ML.Var (pos, x) ->

@ -7,7 +7,7 @@
(library
(name client)
(libraries pprint alcotest qcheck-alcotest inferno)
(libraries pprint alcotest qcheck-alcotest menhirLib inferno)
(preprocess (pps ppx_compare))
(package inferno-sample-client)
)

@ -1,5 +1,7 @@
open Client
module LexUtil = MenhirLib.LexerUtil
(* -------------------------------------------------------------------------- *)
(* A wrapper over the client's [translate] function. We consider ill-typedness
@ -9,19 +11,26 @@ open Client
let print_type ty =
PPrint.(ToChannel.pretty 0.9 80 stdout (FPrinter.print_type ty ^^ hardline))
let translate ~rectypes e t =
let translate ~verbose ~rectypes e t =
try
Some (Infer.translate ~rectypes e t)
with
| Infer.Cycle (_range, ty) ->
if Config.verbose then begin
| Infer.Unbound (range, s) ->
Printf.eprintf "%!%sType error: unbound variable \"%s\".\n"
(LexUtil.range range) s;
None
| Infer.Cycle (range, ty) ->
if verbose then begin
Printf.eprintf "%!%sType error: cyclic type.\n"
(LexUtil.range range);
Printf.fprintf stdout "Type error: a cyclic type arose.\n";
print_type ty
end;
None
| Infer.Unify (_range, ty1, ty2) ->
if Config.verbose then begin
Printf.fprintf stdout "Type error: type mismatch.\n";
| Infer.Unify (range, ty1, ty2) ->
if verbose then begin
Printf.eprintf "%!%sType error: type mismatch.\n"
(LexUtil.range range);
Printf.fprintf stdout "Type error: mismatch between the type:\n";
print_type ty1;
Printf.fprintf stdout "and the type:\n";
@ -35,16 +44,25 @@ let equal_term t1 t2 =
(* -------------------------------------------------------------------------- *)
(* Main parsing function *)
let parse = MLParser.prog MLLexer.read
let wrap parser lexbuf =
let lexbuf = LexUtil.init "test" lexbuf in
try parser MLLexer.read lexbuf
with exn ->
let range = Lexing.(lexbuf.lex_start_p, lexbuf.lex_curr_p) in
Printf.eprintf "%!%sSyntax error.\n%!"
(LexUtil.range range);
raise exn
let parse_type_decls = MLParser.self_contained_type_decls MLLexer.read
(* Main parsing function *)
let term lexbuf = wrap MLParser.self_contained_term lexbuf
let program lexbuf = wrap MLParser.prog lexbuf
let type_decls lexbuf = wrap MLParser.self_contained_type_decls lexbuf
exception ParsingError
let ast_from_string s =
let lexbuf = Lexing.from_string s in
try parse lexbuf
try program lexbuf
with _ -> raise ParsingError
let letify xts =
@ -63,7 +81,7 @@ let open_uses filenames =
let on_file typedecl_env filename =
let ch = open_in filename in
let lexbuf = Lexing.from_channel ch in
let typedecl_env' = parse_type_decls lexbuf in
let typedecl_env' = type_decls lexbuf in
close_in ch;
Datatype.Env.union typedecl_env typedecl_env'
in
@ -79,18 +97,18 @@ let from_string typedecl s =
let from_file filename =
let ch = open_in filename in
let lexbuf = Lexing.from_channel ch in
try let (uses, typedecl_env, xts) = parse lexbuf in
close_in ch;
let typedecl_env' = open_uses uses in
let ast = letify xts in
(Datatype.Env.union typedecl_env typedecl_env', ast)
with _ -> raise ParsingError
let (uses, typedecl_env, xts) = program lexbuf in
close_in ch;
let typedecl_env' = open_uses uses in
let ast = letify xts in
(Datatype.Env.union typedecl_env typedecl_env', ast)
(* -------------------------------------------------------------------------- *)
(* Running all passes over a single ML term. *)
let test_with_args
?(verbose=Config.verbose)
~rectypes
~(success:int ref) ~(total:int ref) (env : ML.datatype_env) (t : ML.term)
: bool
@ -105,7 +123,7 @@ let test_with_args
ML2F.translate_env env in
print_endline "Type inference and translation to System F...";
let outcome =
translate ~rectypes env t
translate ~verbose ~rectypes env t
in
match outcome with
| None ->
@ -118,5 +136,5 @@ let test_with_args
incr success;
true
let test env t =
test_with_args ~success:(ref 0) ~total:(ref 0) env t
let test ?(verbose=Config.verbose) env t =
test_with_args ~verbose ~success:(ref 0) ~total:(ref 0) env t

@ -469,4 +469,4 @@ let test_suite =
]
let () =
Alcotest.run "ML test suite" test_suite
Alcotest.run ~verbose:false "ML test suite" test_suite

@ -1,15 +1,17 @@
open Test.CheckML
let test_ok filename =
let (datatype_env, t) = from_file filename in
let _ = Test.CheckML.test ~rectypes:false datatype_env t in ()
let test filename =
let (datatype_env, t) = Test.CheckML.from_file filename in
let _ = Test.CheckML.test ~verbose:true ~rectypes:false datatype_env t in ()
let parse_args () =
let usage_msg = "todo" in
let usage_msg = "Typecheck midml programs." in
let test_dir = ref "" in
let on_arg filename =
test_ok filename
test (Filename.concat !test_dir filename)
in
Arg.parse [] on_arg usage_msg
let speclist = [
("-I", Arg.Set_string test_dir, "Set a test directory")
] in
Arg.parse speclist on_arg usage_msg
let () =
parse_args ()

@ -24,6 +24,26 @@ Basics
Converting the System F term to de Bruijn style...
Type-checking the System F term...
$ cat wrong-id.midml
let id =
fun x -> y
$ ../TestMidML.exe wrong-id.midml
Type inference and translation to System F...
File "test", line 2, characters 11-12:
Type error: unbound variable "y".
$ cat wrong-id2.midml
let id =
(fun x -> x : some 'a. 'a -> 'a -> 'a)
$ ../TestMidML.exe wrong-id2.midml
Type inference and translation to System F...
Type error: a cyclic type arose.
mu a0. a0 -> a0
At an unknown location:
Type error: cyclic type.
$ cat hole.midml
let hole =
... []

@ -0,0 +1,2 @@
let id =
fun x -> y

@ -0,0 +1,2 @@
let id =
(fun x -> x : some 'a. 'a -> 'a -> 'a)
Loading…
Cancel
Save