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/09844e1e7f7a643f79bfa27c2c641c1a5a0β¦
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/09844e1e7f7a643f79bfa27c2c641c1a5a0β¦
You're receiving this email because of your account on gitlab.com.