Stefan pushed to branch tp/ift6172-2019 at Stefan / Typer

Commits: 09844e1e by Stefan Monnier at 2019-12-11T14:57:16Z * src/elab.ml (elaborate): Improve/fix comments

(elab_call.handle_fun_args): Remove `pending`, always empty.

- - - - -

1 changed file:

- src/elab.ml

Changes:

===================================== src/elab.ml ===================================== @@ -342,18 +342,12 @@ and elab_special_form ctx f args ot = sform_dummy_ret ctx loc

and infer_type pexp ectx var = - (* We could also use lexp_check with an argument of the form - * Sort (?s), but in most cases the metavar would be allocated - * unnecessarily. *) + (* We could also use lexp_check with an argument of the form Sort (...), + * except that we don't know which universe level it will be. *) let t, s = infer pexp ectx in (match OL.lexp_whnf s (ectx_to_lctx ectx) with | Sort (_, _) -> () (* All clear! *) - (* FIXME: We could automatically coerce Type levels to Sorts, so we - * could write `(a : TypeLevel) -> a -> a` instead of - * `(a : TypeLevel) -> Type_ a -> Type_ a` *) | _ -> - (* FIXME: Here we rule out TypeLevel/TypeOmega. - * Maybe it's actually correct?! *) let lexp_string e = lexp_string (L.clean e) in let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with @@ -501,29 +495,11 @@ and elab_macro_call ctx func args ot = (* Identify Call Type and return processed call. *) and elab_call ctx (func, ltp) (sargs: sexp list) =

- let rec handle_fun_args largs sargs pending ltp = + let rec handle_fun_args largs sargs ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in match sargs, ltp' with - | _, Arrow ((_, 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 (larg :: largs) sargs - (SMap.remove aname 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 + -> largs, ltp

| sarg :: sargs, _ -> let (arg_type, ret_type) = match ltp' with @@ -532,10 +508,10 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | _ -> unify_with_arrow ctx (sexp_location sarg) ltp' (dloc, None) None in let larg = check sarg arg_type ctx in - handle_fun_args (larg :: largs) sargs pending + handle_fun_args (larg :: largs) sargs (L.mkSusp ret_type (S.substitute larg)) in

- let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in + let (largs, ret_type) = handle_fun_args [] sargs ltp in (mkCall (func, List.rev largs), Inferred ret_type)

(* Parse inductive type definition. *)

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