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...