Stefan pushed to branch master at Stefan / Typer
Commits: 8dd054b6 by Stefan Monnier at 2016-11-08T10:57:37-05:00 * src/lparse.ml (_lexp_p_check): Check function arg type annotation.
- - - - -
1 changed file:
- src/lparse.ml
Changes:
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -371,10 +371,13 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = | Some def_arg_type -> let def_arg_type, lasort = _lexp_p_infer def_arg_type ctx trace in elab_check_sort ctx lasort (Some var) def_arg_type; - () (* FIXME: Check `conv_p def_arg_type given_arg_type`! *) + if not (OL.conv_p (ectx_to_lctx ctx) def_arg_type given_arg_type) then + lexp_error (lexp_location def_arg_type) def_arg_type + ("Type mismatch! Context expected `" + ^ lexp_string given_arg_type ^ "`\n") | _ -> () in
- let nctx = env_extend ctx var Variable latp in + let nctx = env_extend ctx var Variable given_arg_type in let lbody = lexp_check body given_body_type nctx in
mkLambda(kind, var, given_arg_type, lbody) @@ -600,7 +603,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* first list has all the arguments, second only holds explicit arguments *) let order, eorder = extract_order ltp [] [] in
- (*) + (* print_string "Type :"; lexp_print ltp; print_string "\n"; print_string "Order:"; List.iter (fun (_, b, _) -> print_string (b ^ " ")) (order); print_string "\n"; print_string "Sarg1: ";
View it on GitLab: https://gitlab.com/monnier/typer/commit/8dd054b6cae24bb8324e59596c02d2e49819...
Afficher les réponses par date