Stefan pushed to branch master at Stefan / Typer

Commits: 48b06933 by Stefan Monnier at 2017-07-07T15:49:10-04:00 * src/elab.ml (sform_lambda): Only handle a single arg

- - - - -

1 changed file:

- src/elab.ml

Changes:

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -1154,60 +1154,54 @@ let elaborate ctx pe ot = | None -> let (le, lt) = infer pe ctx in (le, Inferred lt)

-let sform_lambda kind ctx loc sargs ot' = +let sform_lambda kind ctx loc sargs ot = match sargs with - | [sargs; sbody] - -> let sargs = sexp_p_list sargs ["_:_"] in - - let rec do_all_args sargs ctx ot = match sargs with - | [] -> elaborate ctx sbody ot - | sarg :: sargs - -> let (arg, ost1) = match sarg with - | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (arg, Some st) - | Symbol arg -> (arg, None) - | _ -> sexp_error (sexp_location sarg) - "Unrecognized lambda argument"; - ((dummy_location, "_"), None) in - - let olt1 = match ost1 with - | Some st -> Some (infer_type st ctx (Some arg)) - | _ -> None in - - let lt1, olt2 = - match ot with - | None -> ((match olt1 with - | Some lt1 -> lt1 - | None -> newMetatype loc), - None) - (* Read var type from the provided type *) - | Some t - -> let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with - | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind - -> (match olt1 with - | None -> () - | Some lt1' - -> if not (OL.conv_p meta_ctx (ectx_to_lctx ctx) lt1 lt1') - then lexp_error (lexp_location lt1') lt1' - ("Type mismatch! Context expected `" - ^ lexp_string lt1 ^ "`")); - (lt1, Some lt2) - (* FIXME: If `t` is an implicit arrow and `kind` is Aexplicit, - * then auto-add a corresponding Lambda wrapper! *) - | lt - -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 - in (lt1, Some lt2) in - - let nctx = env_extend ctx arg Variable lt1 in - let (lbody, alt) = do_all_args sargs nctx olt2 in - (mkLambda (kind, arg, lt1, lbody), - match alt with - | Lazy -> Lazy - | Checked -> Checked - | Inferred lt2 - -> Inferred (mkArrow (kind, Some arg, lt1, loc, lt2))) in - - do_all_args sargs ctx ot' + | [sarg; sbody] + -> let (arg, ost1) = match sarg with + | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (arg, Some st) + | Symbol arg -> (arg, None) + | _ -> sexp_error (sexp_location sarg) + "Unrecognized lambda argument"; + ((dummy_location, "_"), None) in + + let olt1 = match ost1 with + | Some st -> Some (infer_type st ctx (Some arg)) + | _ -> None in + + let lt1, olt2 = + match ot with + | None -> ((match olt1 with + | Some lt1 -> lt1 + | None -> newMetatype loc), + None) + (* Read var type from the provided type *) + | Some t + -> let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with + | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind + -> (match olt1 with + | None -> () + | Some lt1' + -> if not (OL.conv_p meta_ctx (ectx_to_lctx ctx) lt1 lt1') + then lexp_error (lexp_location lt1') lt1' + ("Type mismatch! Context expected `" + ^ lexp_string lt1 ^ "`")); + (lt1, Some lt2) + (* FIXME: If `t` is an implicit arrow and `kind` is Aexplicit, + * then auto-add a corresponding Lambda wrapper! *) + | lt + -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 + in (lt1, Some lt2) in + + let nctx = env_extend ctx arg Variable lt1 in + let (lbody, alt) = elaborate nctx sbody olt2 in + (mkLambda (kind, arg, lt1, lbody), + match alt with + | Lazy -> Lazy + | Checked -> Checked + | Inferred lt2 + -> Inferred (mkArrow (kind, Some arg, lt1, loc, lt2))) + | _ -> sexp_error loc "##lambda_->_ takes two arguments"; sform_dummy_ret loc

View it on GitLab: https://gitlab.com/monnier/typer/commit/48b069332bd73e6d1a22ef1f7a68363ea876...

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/48b069332bd73e6d1a22ef1f7a68363ea876... You're receiving this email because of your account on gitlab.com.