Stefan pushed to branch master at Stefan / Typer

Commits: b3b5b11f by Stefan Monnier at 2017-02-28T00:59:56-05:00 * src/lparse.ml (sform_lambda): New function

(parse_special_form): Pass `ot` to the special form. (elaborate): New function. (register_special_forms): Register it under all three names.

* src/pexp.ml (pexp): Remove Plambda.

- - - - -

3 changed files:

- src/lexp.ml - src/lparse.ml - src/pexp.ml

Changes:

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -376,8 +376,15 @@ let rec lexp_unparse lxp = | Var ((loc, name), _) -> Pimm (Symbol (loc, name)) | Cons (t, (l, name)) -> Pcall (pdatacons, [pexp_unparse (lexp_unparse t); Symbol (l, name)]) - | Lambda (kind, vdef, ltp, body) -> - Plambda(kind, vdef, Some (lexp_unparse ltp), lexp_unparse body) + | Lambda (kind, vdef, ltp, body) + -> let l = lexp_location lxp in + let st = pexp_unparse (lexp_unparse ltp) in + Pimm (Node (Symbol (l, match kind with + | Aexplicit -> "lambda_->_" + | Aimplicit -> "lambda_=>_" + | Aerasable -> "lambda_≡>_"), + [Node (Symbol (l, "_:_"), [Symbol vdef; st]); + pexp_unparse (lexp_unparse body)])) | Arrow (arg_kind, vdef, ltp1, loc, ltp2) -> let ut1 = pexp_unparse (lexp_unparse ltp1) in Pimm (Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_"

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -289,16 +289,6 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = (lexp_let_decls declss bdy nctx), mkSusp ltp s

- (* This case can be inferred. *) - | Plambda (kind, var, Some ptype, body) - -> let ltp = infer_type ptype ctx (Some var) in - - let nctx = env_extend ctx var Variable ltp in - let lbody, lbtp = infer body nctx in - - let lambda_type = mkArrow (kind, Some var, ltp, tloc, lbtp) in - mkLambda(kind, var, ltp, lbody), lambda_type - | Pcall (func, args) -> let (f, t) as ft = infer func ctx in let meta_ctx, _ = !global_substitution in @@ -312,7 +302,7 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = else infer_call ctx ft args

- | (Plambda _ | Pcase _ | Pimm (Symbol _)) + | (Pcase _ | Pimm (Symbol _)) -> let t = newMetatype (pexp_location p) in let lxp = check p t ctx in (lxp, t) @@ -334,7 +324,7 @@ and parse_special_form ctx f args ot = match OL.lexp_whnf f (ectx_to_lctx ctx) meta_ctx with | Builtin ((_, name), _, _) -> (* Special form. *) - let (e, ot') = (get_special_form name) ctx loc args None in + let (e, ot') = (get_special_form name) ctx loc args ot in (* `ot` is None if we're inferring and `Some t` if we're checking. *) (match (ot, ot') with | (Some t, Checked) -> (e, t) @@ -425,22 +415,15 @@ and lexp_let_decls declss (body: lexp) ctx = List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) declss body

-and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = - - let tloc = pexp_location p in - - (* Safe current trace in a global variable. If an error occur, - we will be able to retrieve the most recent trace and context *) - _global_lexp_ctx := ctx; - - let unify_with_arrow lxp kind var aty subst = +and unify_with_arrow ctx tloc lxp kind var aty = let body = newMetatype tloc in let arg = match aty with | None -> newMetatype tloc | Some laty -> laty in let l, _ = var in let arrow = mkArrow (kind, Some var, arg, l, body) in - match Unif.unify arrow lxp (ectx_to_lctx ctx) subst with + let meta_ctx, _ = !global_substitution in + match Unif.unify arrow lxp (ectx_to_lctx ctx) meta_ctx with | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp ^ " and " ^ lexp_string arrow @@ -454,39 +437,9 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = (mkDummy_type l, mkDummy_type l) | Some subst -> global_substitution := subst; arg, body

- in - let infer_lambda_body kind var def_arg_type body subst = - (* Check argument type annotation, if any. *) - let def_arg_type = match def_arg_type with - | Some def_arg_type - -> Some (infer_type def_arg_type ctx (Some var)) - | _ -> None in +and check (p : pexp) (t : ltype) (ctx : elab_context): lexp =

- (* Read var type from the provided type *) - let meta_ctx, _ = !global_substitution in - let given_arg_type, given_body_type = - match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with - | Arrow(kind, _, ltp, _, lbtp) - -> (match def_arg_type with - | None -> () - | Some def_arg_type - -> if not (OL.conv_p meta_ctx (ectx_to_lctx ctx) def_arg_type ltp) then - lexp_error (lexp_location def_arg_type) def_arg_type - ("Type mismatch! Context expected `" - ^ lexp_string ltp ^ "`")); - ltp, lbtp - | lxp -> unify_with_arrow lxp kind var def_arg_type subst in - - let nctx = env_extend ctx var Variable given_arg_type in - let lbody = check body given_body_type nctx in - mkLambda (kind, var, given_arg_type, lbody) - - in - let subst, _ = !global_substitution in match p with - | Plambda (kind, var, def_arg_type, body) - -> infer_lambda_body kind var def_arg_type body subst - | Pcase (loc, target, branches) -> check_case t (loc, target, branches) ctx

@@ -1202,6 +1155,71 @@ let sform_arrow kind ctx loc sargs ot = | _ -> sexp_error loc "##_->_ takes two arguments"; sform_dummy_ret loc

+(* Infer or check, as the case may be. *) +let elaborate ctx pe ot = + match ot with + | Some t -> (check pe t ctx, Checked) + | None -> let (le, lt) = infer pe ctx in + (le, Inferred lt) + +let sform_lambda kind ctx loc sargs ot' = + match sargs with + | [sargs; sbody] + -> let sargs = sexp_p_list sargs ["_:_"] in + let pbody = pexp_parse sbody in + + let rec do_all_args sargs ctx ot = match sargs with + | [] -> elaborate ctx pbody 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 (pexp_parse 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' + | _ -> sexp_error loc "##lambda_->_ takes two arguments"; + sform_dummy_ret loc + (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) * But it would be less efficient (such a lambda can't be passed as argument @@ -1243,6 +1261,9 @@ let register_special_forms () = ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); + ("lambda_->_", sform_lambda Aexplicit); + ("lambda_=>_", sform_lambda Aimplicit); + ("lambda_≡>_", sform_lambda Aerasable); ("_->_", sform_arrow Aexplicit); ("_=>_", sform_arrow Aimplicit); ("_≡>_", sform_arrow Aerasable);

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -40,7 +40,6 @@ type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) | Plet of location * pdecl list * pexp - | Plambda of arg_kind * pvar * pexp option * pexp | Pcall of pexp * sexp list (* Curried call. *) (* The symbols are only used so that we can distinguish two * otherwise isomorphic types. *) @@ -64,7 +63,6 @@ let rec pexp_location e = (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s | Plet (l, _, _) -> l - | Plambda (_,(l,_), _, _) -> l | Pcall (f, _) -> pexp_location f | Pcase (l, _, _) -> l

@@ -72,7 +70,6 @@ let pexp_name e = match e with | Pimm _ -> "Pimm" | Plet (_, _, _) -> "Plet" - | Plambda (_,(_,_), _, _) -> "Plambda" | Pcall (_, _) -> "Pcall" | Pcase (_, _, _) -> "Pcase"

@@ -93,26 +90,6 @@ let rec pexp_parse (s : sexp) : pexp = -> Plet (start, pexp_p_decls decls, pexp_parse body) | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) -> pexp_error start "Unrecognized let expression"; Pimm (Symbol (start, "?")) - (* lambda *) - | Node (Symbol (start,(("lambda_->_" | "lambda_=>_" | "lambda_≡>_") as arw)), - [arg; body]) - -> let kind = match arw with - | "lambda_->_" -> Aexplicit | "lambda_=>_" -> Aimplicit - | _ -> Aerasable in - List.fold_right - (fun arg pbody - -> let (v, t) = match arg with - | Symbol v -> (v, None) - | Node (Symbol (_, "_:_"), [Symbol v; t]) - -> (v, Some (pexp_parse t)) - | _ -> pexp_error start "Unrecognized lambda argument"; - ((dummy_location, "unrecognized_arg"), None) - in Plambda (kind, v, t, pbody)) - (sexp_p_list arg ["_:_"]) - (pexp_parse body) - | Node (Symbol (start, "lambda_"), _) - -> pexp_error start "Unrecognized lambda expression"; - Pimm (Symbol (start, "?")) (* cases analysis *) | Node (Symbol (start, "case_"), [Node (Symbol (_, "_|_"), e :: cases)]) @@ -228,15 +205,12 @@ and pexp_p_decls e: pdecl list = -> List.concat (List.map pexp_p_decls decls) | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, pexp_parse t)] | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr(s, pexp_parse t)] - | Node (Symbol (_, "_=_"), [Node (Symbol s, args); t]) -> - let rec mkfun args = - match args with - | [] -> pexp_parse t (* Plambda of arg_kind * pvar * pexp option * pexp *) - | (Symbol s :: args) -> Plambda(Aexplicit, s, None, mkfun args) - | (arg :: args) -> pexp_error (sexp_location arg) - "Unknown argument format"; - mkfun args - in [Pexpr(s, mkfun args)] + | Node (Symbol (l, "_=_"), [Node (Symbol s, args) as d; t]) -> + [Pexpr(s, Pcall (Pimm (Symbol (sexp_location d, "lambda_->_")), + [(match args with + | [] -> Sexp.dummy_epsilon + | arg::args -> Node (arg, args)); + t]))] (* everything else is considered a macro * An error will be produced during lexp_parsing if the macro does not exist * once expanded the Pmcall macro will produce a list of pdecl *) @@ -253,15 +227,6 @@ and pexp_unparse (e : pexp) : sexp = | Plet (start, decls, body) -> Node (Symbol (start, "let_in_"), [pexp_u_decls decls; pexp_unparse body]) - | Plambda (ak, v, t, body) -> - Node (Symbol (dummy_location, match ak with - | Aexplicit -> "lambda_->_" - | Aimplicit -> "lambda_=>_" - | Aerasable -> "lambda_≡>_"), - [(match t with None -> Symbol v - | Some t -> Node (Symbol (dummy_location, "_:_"), - [Symbol v; pexp_unparse t])); - pexp_unparse body]) | Pcall (f, args) -> Node (pexp_unparse f, args) | Pcase (start, e, branches) -> Node (Symbol (start, "case_"),

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