Stefan pushed to branch master at Stefan / Typer
Commits: 06bd99aa by Stefan Monnier at 2016-12-04T23:11:07-05:00 * src/lparse.ml: Fix handling of trailing explicit-implicit args
(infer_call.handle_fun_args): Fix handling of trailing explicit-implicit args.
* tests/eval_test.ml ("Equalities"): * btl/builtins.typer (Eq_comm): Remove unneeded explicit-implicits.
- - - - -
3 changed files:
- btl/builtins.typer - src/lparse.ml - tests/eval_test.ml
Changes:
===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -60,8 +60,7 @@ Eq_comm : (l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) ≡> (y : t) Eq_comm = lambda l t x y ≡> lambda p -> Eq_cast (f := lambda xy -> Eq (t := t) xy x) (p := p) - %% FIXME: Removing (l := l) gives bogus error! - (Eq_refl (l := l) (t := t) (x := x)); + Eq_refl;
% Basic operators _+_ = Built-in "Int.+" (Int -> Int -> Int);
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -658,19 +658,6 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = (SMap.remove aname' pending) (L.mkSusp ret_type (S.substitute larg))
- | [], _ - -> (if not (SMap.is_empty pending) then - let pending = SMap.bindings pending in - let loc = match pending with - | (_, sarg)::_ -> sexp_location sarg - | _ -> assert false in - pexp_error loc func - ("Explicit actual args `" - ^ String.concat ", " (List.map (fun (l, _) -> l) - pending) - ^ "` have no matching formal args")); - largs, ltp - | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, Arrow (ak, _, arg_type, _, ret_type) when (aname = "_") @@ -692,6 +679,31 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = ^ "(type = " ^ (lexp_string ltp) ^ ")"); handle_fun_args largs sargs pending ltp
+ (* Aerasable *) + | _, Arrow (Aerasable, v, arg_type, _, ret_type) + (* Don't instantiate after the last explicit arg: the rest is done, + * when needed in infer_and_check (via instantiate_implicit). *) + when not (sargs = [] && SMap.is_empty pending) + -> let larg = newMetavar (match sargs with + | [] -> pexp_location func + | sarg::_ -> sexp_location sarg) + (match v with Some (_, name) -> name | _ -> "v") + arg_type in + handle_fun_args ((Aerasable, larg) :: largs) sargs pending + (L.mkSusp ret_type (S.substitute larg)) + | [], _ + -> (if not (SMap.is_empty pending) then + let pending = SMap.bindings pending in + let loc = match pending with + | (_, sarg)::_ -> sexp_location sarg + | _ -> assert false in + pexp_error loc func + ("Explicit actual args `" + ^ String.concat ", " (List.map (fun (l, _) -> l) + pending) + ^ "` have no matching formal args")); + largs, ltp + | sarg :: sargs, Arrow (Aexplicit, _, arg_type, _, ret_type) -> let parg = pexp_parse sarg in let larg = check parg arg_type ctx in @@ -728,13 +740,6 @@ and infer_call (func: pexp) (sargs: sexp list) ctx =
handle_fun_args ((Aimplicit, larg) :: largs) (sarg::sargs) pending (L.mkSusp ret_type (S.substitute larg))) - (* Aerasable *) - | sarg :: sargs, Arrow (Aerasable, v, arg_type, _, ret_type) - -> let larg = newMetavar (sexp_location sarg) - (match v with Some (_, name) -> name | _ -> "v") - arg_type in - handle_fun_args ((Aerasable, larg) :: largs) (sarg::sargs) pending - (L.mkSusp ret_type (S.substitute larg))
| sarg :: sargs, t -> print_lexp_ctx (ectx_to_lctx ctx);
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -362,9 +362,7 @@ let _ = test_eval_eqv_named f = lambda α ≡> lambda p x -> Eq_cast (t := Type) (x := Int) (y := α) (f := (lambda v -> v)) (p := p) x"
- (* FIXME: If I remove the (l := ?) I get - * Explicit actual args `t, x` have no matching formal args *) - "f (Eq_refl (l := ?) (t := Type) (x := Int)) 3" + "f Eq_refl 3" "3"
(* run all tests *)
View it on GitLab: https://gitlab.com/monnier/typer/commit/06bd99aa9d591696690a9fb59c89223307b3...
Afficher les réponses par date