Stefan pushed to branch master at Stefan / Typer Commits: f49911fd by Stefan Monnier at 2016-09-29T00:41:49-04:00 * src/lparse.ml (_lexp_p_infer) <Parrow>: Also add anon vars to lctx * src/debruijn.ml (ectx_extend_anon): New function. * src/lparse.ml (_type_shift): Remove function. (_lexp_p_infer) <Parrow>: Also add anonymous vars to lctx. - - - - - 2 changed files: - src/debruijn.ml - src/lparse.ml Changes: ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -118,6 +118,9 @@ let lexp_ctx_cons (ctx : lexp_context) offset d v t = let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) = lexp_ctx_cons ctx 0 (Some def) v t +let ectx_extend_anon (ectx: elab_context) (t: lexp) : elab_context = + let ((n, map), lctx, f) = ectx in + ((n + 1, map), lexp_ctx_cons lctx 0 None Variable t, f) let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -75,14 +75,6 @@ type mdecl = | Ldecl of symbol * pexp option * pexp option | Lmcall of symbol * sexp list -(* This is used to make Type annotation and inferred type having the same index *) -(* since inferred type might need to parse a lambda var to infer the type *) - -let _type_shift tp i = - match tp with - | Var(v, idx) -> Var(v, idx) - | expr -> expr - let ctx_define (ctx: elab_context) var lxp ltype = let (_, cctx, _) = ctx in if OL.conv_p ltype (OL.check cctx lxp) then @@ -184,12 +176,11 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = (* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) -> let ltp, _ = lexp_infer tp ctx in - let nctx, sh = match ovar with - | None -> ctx, 0 - | Some var -> (env_extend ctx var Variable ltp), 1 in + let nctx = match ovar with + | None -> ectx_extend_anon ctx ltp + | Some var -> env_extend ctx var Variable ltp in let lxp, _ = lexp_infer expr nctx in - let lxp = _type_shift lxp sh in let v = Arrow(kind, ovar, ltp, tloc, lxp) in v, type0 @@ -225,8 +216,6 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = let nctx = env_extend ctx var Variable ltp in let lbody, lbtp = lexp_infer body nctx in - (* We added one variable in the ctx - let lbtp = _type_shift lbtp 1 in *) let lambda_type = Arrow(kind, None, ltp, tloc, lbtp) in Lambda(kind, var, ltp, lbody), lambda_type @@ -350,18 +339,16 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = (* make a list of all branches return type *) let texp = ref [] in - let ctx_len = get_size ctx in (* Read patterns one by one *) let fold_fun (merged, dflt) (pat, exp) = (* Create pattern context *) let (name, iloc, arg), nctx = lexp_read_pattern pat exp tlxp ctx in - let nctx_len = get_size nctx in (* parse using pattern context *) let exp, ltp = lexp_infer exp nctx in (* we added len(arg) variable int the context *) - texp := (_type_shift ltp (nctx_len - ctx_len))::!texp; + texp := ltp::!texp; (* Check ltp type. Must be similar to rtype *) (if type_check ltp then () @@ -569,6 +556,8 @@ and lexp_read_pattern pattern exp target ctx: ("`" ^ lexp_to_str (it) ^ "` is not an inductive type!") in + (* FIXME: Don't remove them, add them without names! *) + (* FIXME: Add support for explicit-implicit fields! *) (* Remove non explicit argument. *) let rec remove_nexplicit args acc = match args with View it on GitLab: https://gitlab.com/monnier/typer/commit/f49911fd102c1e9b11b43a743e5da2e44ba9...