Stefan pushed to branch master at Stefan / Typer

Commits: 5c157c20 by Stefan Monnier at 2017-08-03T15:36:36-04:00 * src/elab.ml: Make `elaborate` the core function

(elaborate): Rewrite, using code from `infer` and `check`. (infer): Rewrite, delegating to `elaborate`. (check): Rewrite, delegating to `elaborate`. (elab_varref): Rename from `infer_varref` and adjust return type. (elab_special_form): Rename from `parse_special_form`; adjust return type. (elab_macro_call): Rename from `handle_macro_call`; adjust return type. (elab_call): Rename from `infer_call`; adjust return type. (sform_lambda): Adjust now that `elaborate` can return Lazy.

- - - - - f36cbd42 by Stefan Monnier at 2017-08-03T15:49:39-04:00 * src/elab.ml (sform_immediate): New special form

(register_special_forms): Register it. (elaborate): Use it for immediates.

- - - - -

1 changed file:

- src/elab.ml

Changes:

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -88,11 +88,11 @@ let lexp_warning = debug_message warning lexp_name lexp_string let lexp_error = debug_message error lexp_name lexp_string let value_fatal = debug_message fatal value_name value_string

-(** Builtin Macros i.e, special forms. *) +(** Type info returned by elaboration. *) type sform_type = - | Inferred of ltype - | Checked - | Lazy + | Checked (* Checked that the expression has the requested type. *) + | Inferred of ltype (* Hasn't looked as the requested type. *) + | Lazy (* Hasn't looked as the requested type, nor inferred a type. *)

type special_forms_map = (elab_context -> location -> sexp list -> ltype option @@ -251,62 +251,57 @@ let mkDummy_infer ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in (mkDummy_check ctx loc t, t)

-let infer_varref ctx ((loc, name) as id) +let elab_varref ctx ((loc, name) as id) = let idx = senv_lookup name ctx in let lxp = make_var name idx loc in let ltp = env_lookup_type ctx (id, idx) in - (lxp, ltp) - -let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = - - match p with - | Symbol ((loc, name) as id) - -> if not (name = "typer-identifier") then - infer (Node (Symbol (loc, "typer-identifier"), [p])) ctx - (* Break the inf-recursion! *) - else infer_varref ctx id - - | Node (se, []) -> infer se ctx - - | Node (func, args) - -> let (f, t) as ft = infer func ctx in - if (OL.conv_p (ectx_to_lctx ctx) t type_special_form) then - parse_special_form ctx f args None - else if (OL.conv_p (ectx_to_lctx ctx) t - (BI.get_predef "Macro" ctx)) then - let t = newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - (sexp_location func) in - let lxp = handle_macro_call ctx f args t in - (lxp, t) - else - infer_call ctx ft args - - (* Block/String/Integer/Float. *) - | Integer _ -> (mkImm (p), DB.type_int) - | Float _ -> (mkImm (p), DB.type_float) - | String _ -> (mkImm (p), DB.type_string) - | Block _ -> infer (Node (Symbol (sexp_location p, "typer-block"), [p])) - ctx - -and parse_special_form ctx f args ot = + (lxp, Inferred ltp) + +(* Infer or check, as the case may be. *) +let rec elaborate ctx se ot = + match se with + (* Rewrite SYM to `typr-identifier SYM`. *) + | Symbol ((loc, name) as id) + -> if not (name = "typer-identifier") then + elaborate ctx (Node (Symbol (loc, "typer-identifier"), [se])) ot + (* Break the inf-recursion! *) + else elab_varref ctx id + + (* Rewrite BLOCK to `typer-block BLOCK`. *) + | Block (l,_,_) -> elaborate ctx (Node (Symbol (l, "typer-block"), [se])) ot + + (* Rewrite IMM to `typer-immediate IMM`. *) + | (Integer _ | Float _ | String _) + -> let l = sexp_location se in + elaborate ctx (Node (Symbol (l, "typer-immediate"), [se])) ot + + | Node (se, []) -> elaborate ctx se ot + + | Node (func, args) + -> let (f, t) as ft = infer func ctx in + if (OL.conv_p (ectx_to_lctx ctx) t type_special_form) then + elab_special_form ctx f args ot + else if (OL.conv_p (ectx_to_lctx ctx) t + (BI.get_predef "Macro" ctx)) then + elab_macro_call ctx f args ot + else + elab_call ctx ft args + +and infer (p : sexp) (ctx : elab_context): lexp * ltype = + match elaborate ctx p None with + | (_, Checked) -> fatal (sexp_location p) "`infer` got Checked!" + | (e, Lazy) -> (e, OL.get_type (ectx_to_lctx ctx) e) + | (e, Inferred t) -> (e, t) + +and elab_special_form ctx f args ot = let loc = lexp_location f in match OL.lexp_whnf f (ectx_to_lctx ctx) with | Builtin ((_, name), _, _) -> (* Special form. *) - 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) - | _ -> let inferred_t = match ot' with - | Inferred t -> t - | _ -> OL.get_type (ectx_to_lctx ctx) e in - match ot with - | None -> (e, inferred_t) - | Some t -> let e = check_inferred ctx e inferred_t t in - (e, t)) + (get_special_form name) ctx loc args ot

| _ -> lexp_error loc f ("Unknown special-form: " ^ lexp_string f); - mkDummy_infer ctx loc + sform_dummy_ret ctx loc

(* Make up an argument of type `t` when none is provided. *) and get_implicit_arg ctx loc name t = @@ -413,29 +408,12 @@ and unify_with_arrow ctx tloc lxp kind var aty | Some [] -> arg, body

and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = - - match p with - | Symbol (l,name) - -> check (Node (Symbol (l, "typer-identifier"), [p])) t ctx - - | Node (se, []) -> check se t ctx - - | Node (func, args) - -> let (f, ft) = infer func ctx in - if (OL.conv_p (ectx_to_lctx ctx) ft type_special_form) then - let (e, _) = parse_special_form ctx f args (Some t) in e - else if (OL.conv_p (ectx_to_lctx ctx) ft - (BI.get_predef "Macro" ctx)) then - handle_macro_call ctx f args t - else - let (e, inferred_t) = infer_call ctx (f, ft) args in - check_inferred ctx e inferred_t t - - | _ -> infer_and_check p ctx t - -and infer_and_check pexp ctx t = - let (e, inferred_t) = infer pexp ctx in - check_inferred ctx e inferred_t t + let (e, ot) = elaborate ctx p (Some t) in + match ot with + | Checked -> e + | _ -> let inferred_t = match ot with Inferred t -> t + | _ -> OL.get_type (ectx_to_lctx ctx) e in + check_inferred ctx e inferred_t t

(* This is a crucial function: take an expression `e` of type `inferred_t` * and convert it into something of type `t`. Currently the only conversion @@ -613,93 +591,92 @@ and check_case rtype (loc, target, ppatterns) ctx =

mkCase (loc, tlxp, rtype, lpattern, dflt)

-and handle_macro_call ctx func args t = +and elab_macro_call ctx func args ot = + let t + = match ot with + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) + (lexp_location func) + | Some t -> t in let sxp = match lexp_expand_macro (lexp_location func) func args ctx (Some t) with | Vsexp (sxp) -> sxp | v -> value_fatal (lexp_location func) v "Macros should return a Sexp" in - - check sxp t ctx + elaborate ctx sxp ot

(* Identify Call Type and return processed call. *) -and infer_call ctx (func, ltp) (sargs: sexp list) = - let loc = lexp_location func in - - (* Vanilla : sqr is inferred and (lambda x -> x * x) is returned - * Macro : sqr is returned - * Constructor : a constructor is returned - * Anonymous : lambda *) - - let rec handle_fun_args largs sargs pending ltp = - let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in - match sargs, ltp' with - | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type) - when SMap.mem aname pending - -> let sarg = SMap.find aname pending in - let larg = check sarg arg_type ctx in - handle_fun_args ((ak, larg) :: largs) sargs - (SMap.remove aname pending) - (L.mkSusp ret_type (S.substitute larg)) - - | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, - Arrow (ak, _, arg_type, _, ret_type) - when (aname = "_") - (* Explicit-implicit argument. *) - -> let larg = check sarg arg_type ctx in - handle_fun_args ((ak, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) - - | (Node (Symbol (_, "_:=_"), [Symbol (l, aname); sarg])) :: sargs, - Arrow _ - -> if SMap.mem aname pending then - sexp_error l ("Duplicate explicit arg `" ^ aname ^ "`"); - handle_fun_args largs sargs (SMap.add aname sarg pending) ltp - - | (Node (Symbol (_, "_:=_"), Symbol (l, aname) :: _)) :: sargs, _ - -> sexp_error l - ("Explicit arg `" ^ aname ^ "` to non-function " - ^ "(type = " ^ (lexp_string ltp) ^ ")"); - handle_fun_args largs sargs pending ltp - - (* Aerasable *) - | _, Arrow ((Aerasable | Aimplicit) as ak, 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 = get_implicit_arg - ctx (match sargs with - | [] -> loc - | sarg::_ -> sexp_location sarg) - (match v with Some (_, name) -> name | _ -> "v") - arg_type in - handle_fun_args ((ak, 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 - lexp_error loc func - ("Explicit actual args `" - ^ String.concat ", " (List.map (fun (l, _) -> l) - pending) - ^ "` have no matching formal args")); - largs, ltp - - | sarg :: sargs, _ - -> let (arg_type, ret_type) = match ltp' with - | Arrow (ak, _, arg_type, _, ret_type) - -> assert (ak = Aexplicit); (arg_type, ret_type) - | _ -> unify_with_arrow ctx (sexp_location sarg) - ltp' Aexplicit (dloc, "<anon>") None in - let larg = check sarg arg_type ctx in - handle_fun_args ((Aexplicit, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) in - - let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in - mkCall (func, List.rev largs), ret_type +and elab_call ctx (func, ltp) (sargs: sexp list) = + let loc = lexp_location func in + + let rec handle_fun_args largs sargs pending ltp = + let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in + match sargs, ltp' with + | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type) + when SMap.mem aname pending + -> let sarg = SMap.find aname pending in + let larg = check sarg arg_type ctx in + handle_fun_args ((ak, larg) :: largs) sargs + (SMap.remove aname pending) + (L.mkSusp ret_type (S.substitute larg)) + + | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, + Arrow (ak, _, arg_type, _, ret_type) + when (aname = "_") + (* Explicit-implicit argument. *) + -> let larg = check sarg arg_type ctx in + handle_fun_args ((ak, larg) :: largs) sargs pending + (L.mkSusp ret_type (S.substitute larg)) + + | (Node (Symbol (_, "_:=_"), [Symbol (l, aname); sarg])) :: sargs, + Arrow _ + -> if SMap.mem aname pending then + sexp_error l ("Duplicate explicit arg `" ^ aname ^ "`"); + handle_fun_args largs sargs (SMap.add aname sarg pending) ltp + + | (Node (Symbol (_, "_:=_"), Symbol (l, aname) :: _)) :: sargs, _ + -> sexp_error l + ("Explicit arg `" ^ aname ^ "` to non-function " + ^ "(type = " ^ (lexp_string ltp) ^ ")"); + handle_fun_args largs sargs pending ltp + + (* Aerasable *) + | _, Arrow ((Aerasable | Aimplicit) as ak, 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 = get_implicit_arg + ctx (match sargs with + | [] -> loc + | sarg::_ -> sexp_location sarg) + (match v with Some (_, name) -> name | _ -> "v") + arg_type in + handle_fun_args ((ak, 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 + lexp_error loc func + ("Explicit actual args `" + ^ String.concat ", " (List.map (fun (l, _) -> l) + pending) + ^ "` have no matching formal args")); + largs, ltp + + | sarg :: sargs, _ + -> let (arg_type, ret_type) = match ltp' with + | Arrow (ak, _, arg_type, _, ret_type) + -> assert (ak = Aexplicit); (arg_type, ret_type) + | _ -> unify_with_arrow ctx (sexp_location sarg) + ltp' Aexplicit (dloc, "<anon>") None in + let larg = check sarg arg_type ctx in + handle_fun_args ((Aexplicit, larg) :: largs) sargs pending + (L.mkSusp ret_type (S.substitute larg)) in + + let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in + (mkCall (func, List.rev largs), Inferred ret_type)

(* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = @@ -1121,6 +1098,19 @@ let sform_arrow kind ctx loc sargs ot = | _ -> sexp_error loc "##_->_ takes two arguments"; sform_dummy_ret ctx loc

+let sform_immediate ctx loc sargs ot = + match sargs with + | [(String _) as se] -> mkImm (se), Inferred DB.type_string + | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int + | [(Float _) as se] -> mkImm (se), Inferred DB.type_float + | [se] + -> (sexp_error loc ("Non-immediate passed to ##typer-immediate"); + sform_dummy_ret ctx loc) + | _ + -> (sexp_error loc ("Too many args to ##typer-immediate"); + sform_dummy_ret ctx loc) + + let sform_identifier ctx loc sargs ot = match sargs with | [Symbol (l,name)] @@ -1161,9 +1151,7 @@ let sform_identifier ctx loc sargs ot =

(* Normal identifier. *) | [Symbol id] - -> (try let (e, t) = infer_varref ctx id in - (e, Inferred t) - + -> (try elab_varref ctx id with Not_found -> (let (loc, name) = id in sexp_error loc ("The variable: `" ^ name ^ "` was not declared"); @@ -1177,13 +1165,6 @@ let sform_identifier ctx loc sargs ot = -> (sexp_error loc ("Too many args to ##typer-identifier"); sform_dummy_ret ctx 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 var_of_ovar l ov = match ov with | None -> (l, "<anon>") | Some v -> v @@ -1207,10 +1188,8 @@ let rec sform_lambda kind ctx loc sargs ot = let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with - | Lazy -> Lazy (* FIXME: Impossible! *) - | Checked -> Checked - | Inferred lt2 - -> Inferred (mkArrow (kind, Some arg, lt1, loc, lt2))) in + | Inferred lt2 -> Inferred (mkArrow (kind, Some arg, lt1, loc, lt2)) + | _ -> alt) in

(match ot with | None -> mklam (match olt1 with @@ -1231,11 +1210,11 @@ let rec sform_lambda kind ctx loc sargs ot = ^ lexp_string lt1 ^ "`")); mklam lt1 (Some lt2)

- | Arrow (ak2, v, lt1, _, lt2) when kind = Aexplicit + | Arrow (ak2, ov, lt1, _, lt2) when kind = Aexplicit (* `t` is an implicit arrow and `kind` is Aexplicit, * so auto-add a corresponding Lambda wrapper! * FIXME: This should be moved to a macro. *) - -> let v = var_of_ovar loc v in + -> let v = var_of_ovar loc ov in (* FIXME: Here we end up adding a local variable `v` whose * name is lot lexically present, so there's a risk of * name capture. We should make those vars anonymous? *) @@ -1243,8 +1222,10 @@ let rec sform_lambda kind ctx loc sargs ot = (* FIXME: Don't go back to sform_lambda, but use an internal * loop to avoid re-computing olt1 each time. *) let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in - assert (alt == Checked); - (mkLambda (ak2, v, lt1, lam), Checked) + (mkLambda (ak2, v, lt1, lam), + match alt with + | Inferred lt2' -> Inferred (mkArrow (ak2, ov, lt1, loc, lt2')) + | _ -> alt)

| lt -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 @@ -1325,6 +1306,7 @@ let register_special_forms () = [ ("Built-in", sform_built_in); ("typer-identifier", sform_identifier); + ("typer-immediate", sform_immediate); ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype);

View it on GitLab: https://gitlab.com/monnier/typer/compare/27dd27dc9e57f84a56a06c830a470201127...

--- View it on GitLab: https://gitlab.com/monnier/typer/compare/27dd27dc9e57f84a56a06c830a470201127... You're receiving this email because of your account on gitlab.com.