Stefan pushed to branch master at Stefan / Typer Commits: 9853ee47 by Stefan Monnier at 2016-11-15T15:44:44-05:00 Fix some issues with case handling in lparse and eval * src/eval.ml (eval_case): Do add anonymous pattern args to context. Otherwise, deb-indices are wrong! * src/lparse.ml (fold_fun.add_branch.make_nctx): Don't take unrelated explicit pattern arg when we expect a normal pattern arg. Detect when we don't have enough pattern args. (infer_call.handle_fun_args): Allow (_ := ...) also for anonymous normal args. * tests/eval_test.ml ("Explicit field patterns"): Add more cases. - - - - - 3 changed files: - src/eval.ml - src/lparse.ml - tests/eval_test.ml Changes: ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -348,16 +348,17 @@ and eval_case ctx i loc target pat dflt = (* This is more robust *) let rec fold2 nctx pats args = match pats, args with - | (Some (_, name))::pats, arg::args -> - let nctx = add_rte_variable (Some name) arg nctx in - fold2 nctx pats args - | (None)::pats, arg::args -> fold2 nctx pats args - (* Errors: those should not happen but they might *) - (* List.fold2 would complain. we print more info *) - | _::_, [] -> warning loc "a) Eval::Case Pattern Error"; nctx - | [], _::_ -> warning loc "b) Eval::Case Pattern Error"; nctx - (* Normal case *) - | [], [] -> nctx in + | pat::pats, arg::args + -> let nctx = add_rte_variable (match pat with + | Some (_, name) -> Some name + | _ -> None) arg nctx in + fold2 nctx pats args + (* Errors: those should not happen but they might *) + (* List.fold2 would complain. we print more info *) + | _::_, [] -> warning loc "a) Eval::Case Pattern Error"; nctx + | [], _::_ -> warning loc "b) Eval::Case Pattern Error"; nctx + (* Normal case *) + | [], [] -> nctx in let nctx = fold2 ctx pat_args args in _eval exp nctx i ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -573,7 +573,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | [], [] -> ctx, List.rev acc | (_, pat)::_, [] -> lexp_error loc lctor - "Too many arguments to the constructor"; + "Too many pattern args to the constructor"; make_nctx ctx s [] [] pe acc | (_, Ppatcons (p, _))::pargs, cargs -> lexp_error (pexp_location p) lctor @@ -588,7 +588,7 @@ and check_case rtype (loc, target, ppatterns) ctx = ((ak, var)::acc) | ((ef, fpat)::pargs, (ak, _, fty)::cargs) when (match (ef, ak) with - | (Some (_, "_"), _) | (_, Aexplicit) -> true + | (Some (_, "_"), _) | (None, Aexplicit) -> true | _ -> false) -> let var = match fpat with Ppatsym v -> Some v | _ -> None in let nctx = ctx_extend ctx var Variable (mkSusp fty s) in @@ -600,8 +600,13 @@ and check_case rtype (loc, target, ppatterns) ctx = pexp_error l pctor ("Duplicate explicit field `" ^ fname ^ "`"); make_nctx ctx s pargs cargs (SMap.add fname var pe) acc - | pargs, (ak, _, fty)::cargs + | pargs, (ak, fname, fty)::cargs -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in + if ak = Aexplicit then + pexp_error loc pctor + ("Missing pattern for normal field" + ^ (match fname with Some (_,n) -> " `" ^ n ^ "`" + | _ -> "")); make_nctx nctx (ssink vdummy s) pargs cargs pe ((ak, None)::acc) in let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in @@ -672,8 +677,8 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = largs, ltp | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, - Arrow (ak, Some (_, aname'), arg_type, _, ret_type) - when (aname = aname' || aname = "_") + Arrow (ak, _, arg_type, _, ret_type) + when (aname = "_") (* Explicit-implicit argument. *) -> let parg = pexp_parse sarg in let larg = check parg arg_type ctx in ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -329,26 +329,29 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Metavars" "f : ?; - f x = 2 + f (1 + x);" + f x = 2 + f (1 + x); + %inf : ?; + %inf x = inf (1 + x); + test = 2;" "1" "1" let _ = test_eval_eqv_named "Explicit field patterns" "Triplet = inductive_ Triplet - (triplet (a ::: Int) (b :: Float) (c : String)); + (triplet (a ::: Int) (b :: Float) (c : String) (d :: Int)); triplet = inductive-cons Triplet triplet; - t = triplet (b := 5.0) (a := 3) (c := \"hello\");" + t = triplet (b := 5.0) (a := 3) (d := 7) (c := \"hello\");" "case t | triplet (b := bf) cf => cf; - case t | triplet (b := bf) cf => bf; + case t | triplet (b := bf) _ => bf; case t | triplet ( _ := bf) cf => cf; case t | triplet ( _ := af) ( _ := bf) ( _ := cf) => bf; case t | triplet ( _ := af) ( _ := bf) ( _ := cf) => cf; + case t | triplet ( _ := af) ( _ := bf) (d := df) cf => df; " - "\"hello\"; 5.0; \"hello\"; 5.0; \"hello\" - " + "\"hello\"; 5.0; \"hello\"; 5.0; \"hello\"; 7" let _ = test_eval_eqv_named "Implicit Arguments" View it on GitLab: https://gitlab.com/monnier/typer/commit/9853ee47600a6ff3aac7d8f9d8c2b1a7f072...