Stefan pushed to branch master at Stefan / Typer
Commits: eb54a39b by Stefan Monnier at 2016-11-15T10:07:37-05:00 * src/lparse.ml (fold_fun.add_branch): Support explicit field patterns
* tests/eval_test.ml ("Explicit field patterns"): New test. (bool_decl): Remove.
- - - - -
2 changed files:
- src/lparse.ml - tests/eval_test.ml
Changes:
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -505,9 +505,9 @@ and check_case rtype (loc, target, ppatterns) ctx = (* get target and its type *) let tlxp, tltp = infer target ctx in let meta_ctx, _ = !global_substitution in - (* FIXME: We need to be careful with whnf: while the output is equivalent - * to the input, it's not necessarily as readable. So try to reuse the - * "non-whnf" form whenever possible. *) + (* FIXME: We need to be careful with whnf: while the output is "equivalent" + * to the input, it's not necessarily as readable/efficient. + * So try to reuse the "non-whnf" form whenever possible. *) let call_split e = match (OL.lexp_whnf e (ectx_to_lctx ctx) meta_ctx) with | Call (f, args) -> (f, args) | _ -> (e,[]) in @@ -544,7 +544,7 @@ and check_case rtype (loc, target, ppatterns) ctx = ^ lexp_string it ^ "` but got `" ^ lexp_string it' ^ "`") in let _ = check_uniqueness pat cons_name lbranches in - let cons_args + let cargs = try SMap.find cons_name constructors with Not_found -> lexp_error loc lctor @@ -555,29 +555,56 @@ and check_case rtype (loc, target, ppatterns) ctx =
let subst = List.fold_right (fun (_, t) s -> S.cons t s) targs S.identity in - let rec make_nctx ctx fargs s pargs cargs = match pargs, cargs with - | [], [] -> ctx, List.rev fargs + let rec make_nctx ctx (* elab context. *) + s (* Pending substitution. *) + pargs (* Pattern arguments. *) + cargs (* Constructor arguments. *) + pe (* Pending explicit pattern args. *) + acc = (* Accumulated reult. *) + match (pargs, cargs) with + | (_, []) when not (SMap.is_empty pe) + -> let pending = SMap.bindings pe in + pexp_error loc pctor + ("Explicit pattern args `" + ^ String.concat ", " (List.map (fun (l, _) -> l) + pending) + ^ "` have no matching fields"); + make_nctx ctx s pargs cargs SMap.empty acc + | [], [] -> ctx, List.rev acc | (_, pat)::_, [] -> lexp_error loc lctor "Too many arguments to the constructor"; - make_nctx ctx fargs s [] [] - | (None, Ppatany _)::pargs, (Aexplicit, _, fty)::cargs - -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in - make_nctx nctx ((Aexplicit, None)::fargs) - (ssink vdummy s) pargs cargs - | (None, Ppatsym v)::pargs, (Aexplicit, _, fty)::cargs - -> let nctx = ctx_extend ctx (Some v) Variable (mkSusp fty s) in - make_nctx nctx ((Aexplicit, Some v)::fargs) - (ssink v s) pargs cargs + make_nctx ctx s [] [] pe acc | (_, Ppatcons (p, _))::pargs, cargs -> lexp_error (pexp_location p) lctor "Nested patterns not supported!"; - make_nctx ctx fargs s pargs cargs + make_nctx ctx s pargs cargs pe acc + | (_, (ak, Some (_, fname), fty)::cargs) + when SMap.mem fname pe + -> let var = SMap.find fname pe in + let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + make_nctx nctx (ssink (maybev var) s) pargs cargs + (SMap.remove fname pe) + ((ak, var)::acc) + | ((ef, fpat)::pargs, (ak, _, fty)::cargs) + when (match (ef, ak) with + | (Some (_, "_"), _) | (_, 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 + make_nctx nctx (ssink (maybev var) s) pargs cargs pe + ((ak, var)::acc) + | ((Some (l, fname), fpat)::pargs, cargs) + -> let var = match fpat with Ppatsym v -> Some v | _ -> None in + if SMap.mem fname pe then + pexp_error l pctor + ("Duplicate explicit field `" ^ fname ^ "`"); + make_nctx ctx s pargs cargs (SMap.add fname var pe) acc | pargs, (ak, _, fty)::cargs -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in - make_nctx nctx ((ak, None)::fargs) - (ssink vdummy s) pargs cargs in - let nctx, fargs = make_nctx ctx [] subst pargs cons_args in + 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 let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - M.length (ectx_to_lctx ctx))) in
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -169,11 +169,6 @@ let nat_decl = " | (succ y) => (1 + (to-num y)) | zero => 0;"
-let bool_decl = " - Bool = inductive (dBool) (true) (false); - false = inductive-cons Bool false; - true = inductive-cons Bool true;" - let _ = test_eval_eqv_named "Inductive::Recursive Call"
@@ -339,6 +334,23 @@ let _ = test_eval_eqv_named "Metavars" "1" "1"
let _ = test_eval_eqv_named + "Explicit field patterns" + "Triplet = inductive_ Triplet + (triplet (a ::: Int) (b :: Float) (c : String)); + triplet = inductive-cons Triplet triplet; + t = triplet (b := 5.0) (a := 3) (c := "hello");" + + "case t | triplet (b := bf) cf => cf; + case t | triplet (b := bf) cf => bf; + case t | triplet ( _ := bf) cf => cf; + case t | triplet ( _ := af) ( _ := bf) ( _ := cf) => bf; + case t | triplet ( _ := af) ( _ := bf) ( _ := cf) => cf; + " + + ""hello"; 5.0; "hello"; 5.0; "hello" + " + +let _ = test_eval_eqv_named "Implicit Arguments"
"default = new-attribute (Int -> Bool);
View it on GitLab: https://gitlab.com/monnier/typer/commit/eb54a39b5d76480f99d8a1d331af96b94ce7...