Stefan pushed to branch master at Stefan / Typer
Commits: 0a167d0a by Stefan Monnier at 2016-11-11T17:33:42-05:00 Instantiate implicit args when there's no function call
* src/lexp.ml (mkCall): Canonicalize. * src/lparse.ml (infer.target): Simplify accordingly. (instantiate_implicit): New function. (infer_and_check): Use it.
* src/opslexp.ml (check.call_split): No need for recursion.
* btl/types.typer (length, head, tail): Remove unneeded explicit args.
- - - - -
4 changed files:
- btl/types.typer - src/lexp.ml - src/lparse.ml - src/opslexp.ml
Changes:
===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -76,7 +76,7 @@ length = lambda a ≡> lambda xs -> case xs | nil => 0 - | cons hd tl => (1 + (length (a := a) tl)); + | cons hd tl => (1 + (length tl));
% ML's typical `head` function is not total, so can't be defined % as-is in Typer. There are several workarounds: @@ -87,14 +87,14 @@ head : (a : Type) ≡> List a -> Option a; head = lambda a ≡> lambda xs -> case xs - | nil => None (a := a) - | cons hd tl => Some (a := a) hd; + | nil => None + | cons hd tl => Some hd;
tail : (a : Type) ≡> List a -> List a; tail = lambda a ≡> lambda xs -> case xs - | nil => nil (a := a) + | nil => nil | cons hd tl => tl;
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -141,11 +141,15 @@ let mkVar v = hc (Var v) let mkLet (l, ds, e) = hc (Let (l, ds, e)) let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) -let mkCall (f, es) = hc (Call (f, es)) let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) let mkCons (t, n) = hc (Cons (t, n)) let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) let mkMetavar (n, s, v, t) = hc (Metavar (n, s, v, t)) +let mkCall (f, es) + = match f, es with + | Call (f', es'), _ -> hc (Call (f', es' @ es)) + | _, [] -> f + | _ -> hc (Call (f, es))
(********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp.
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -318,19 +318,16 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = [], [] in
(* Build Arrow type. *) - let target = if formal = [] then - push_susp idt (S.shift (List.length args)) - else - let targs, _ - = List.fold_right - (fun (ak, v, _) (targs, i) - -> ((ak, Var (v, i)) :: targs, - i - 1)) - formal - ([], List.length formal + List.length args - 1) in - mkCall (push_susp idt (S.shift (List.length formal - + List.length args)), - targs) in + let target = let targs, _ + = List.fold_right + (fun (ak, v, _) (targs, i) + -> ((ak, Var (v, i)) :: targs, + i - 1)) + formal + ([], List.length formal + List.length args - 1) in + mkCall (push_susp idt (S.shift (List.length formal + + List.length args)), + targs) in let cons_type = List.fold_left (fun ltp (kind, v, tp) -> mkArrow (kind, v, tp, loc, ltp)) @@ -354,6 +351,17 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = let lxp = check p t ctx in (lxp, t)
+(* Build the list of implicit arguments to instantiate. *) +and instantiate_implicit e t ctx = + let (meta_ctx, _) = !global_substitution in + let rec instantiate t args = + match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with + | Arrow ((Aerasable | Aimplicit) as ak, v, t1, _, t2) + -> let arg = newMetavar t1 in (* FIXME: Use `v` to make matevar name. *) + instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) + | _ -> (mkCall (e, List.rev args), t) + in instantiate t [] + 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 @@ -441,6 +449,10 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = and infer_and_check pexp ctx t = let (e, inferred_t) = infer pexp ctx in let subst, _ = !global_substitution in + let (e, inferred_t) = match OL.lexp_whnf t (ectx_to_lctx ctx) subst with + | Arrow ((Aerasable | Aimplicit), _, _, _, _) + -> (e, inferred_t) + | _ -> instantiate_implicit e inferred_t ctx in (match Unif.unify inferred_t t (ectx_to_lctx ctx) subst with | None -> lexp_error (pexp_location pexp) e @@ -603,7 +615,9 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = | [], _ -> (if not (SMap.is_empty pending) then let pending = SMap.bindings pending in - let loc = match pending with (_, sarg)::_ -> sexp_location sarg in + let loc = match pending with + | (_, sarg)::_ -> sexp_location sarg + | _ -> assert false in pexp_error loc func ("Explicit actual args `" ^ String.concat ", " (List.map (fun (l, _) -> l)
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -384,7 +384,7 @@ let rec check meta_ctx ctx e = let tct = arg_loop args ctx in tct | Case (l, e, ret, branches, default) - -> let rec call_split e = match e with + -> let call_split e = match e with | Call (f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (check ctx e) ctx meta_ctx in
View it on GitLab: https://gitlab.com/monnier/typer/commit/0a167d0a10034a4c4bddb0360b10d94f48ae...