Stefan pushed to branch master at Stefan / Typer

Commits: 222406c2 by Stefan Monnier at 2016-09-19T18:38:35-04:00 * src/debruijn.ml (lexp_ctx_cons): New fun. Test sanity of `offset`

(M): Alias for Myers, which we don't open any more. (lctx_extend, lctx_extend_rec): New functions. (env_extend): Use them. * src/opslexp.ml (check): Use lctx_extend(_rec).

- - - - -

2 changed files:

- src/debruijn.ml - src/opslexp.ml

Changes:

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -35,7 +35,7 @@ open Util open Lexp module L = Lexp -open Myers +module M = Myers open Fmt

module S = Subst @@ -61,7 +61,7 @@ type property_env = property_elem PropertyMap.t (* easier to debug with type annotations *) type env_elem = (int * vdef option * varbind * ltype) (* FIXME: This is the *lexp context*. *) -type lexp_context = env_elem myers +type lexp_context = env_elem M.myers

type db_idx = int (* DeBruijn index. *) type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *) @@ -85,7 +85,7 @@ let ectx_to_lctx (ectx : elab_context) : lexp_context =

let _make_scope = StringMap.empty let _make_senv_type = (0, _make_scope) -let _make_myers = nil +let _make_myers = M.nil let _get_env(ctx: elab_context): lexp_context = let (_, ev, _) = ctx in ev

(* Public methods: DO USE @@ -106,6 +106,16 @@ let rec senv_lookup (name: string) (ctx: elab_context): int = else *) raw_idx

+let lexp_ctx_cons (ctx : lexp_context) offset d v t = + assert (offset >= 0 && + (ctx = M.nil || + let (previous_offset, _, _, _) = M.car ctx in + previous_offset >= 0 && previous_offset <= 1 + offset)); + M.cons (offset, d, v, t) ctx + +let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) = + lexp_ctx_cons ctx 0 (Some def) v t + let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in let ((n, map), env, f) = ctx in @@ -113,9 +123,21 @@ let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = debruijn_warning loc ("Variable Shadowing " ^ name); with Not_found -> ()); let nmap = StringMap.add name n map in - ((n + 1, nmap), cons (0, Some def, v, t) env, f) + ((n + 1, nmap), + lexp_ctx_cons env 0 (Some def) v t, + f) + +let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) = + let (ctx, _) = + List.fold_left + (fun (ctx, recursion_offset) (def, e, t) -> + lexp_ctx_cons ctx recursion_offset (Some def) (LetDef e) t, + recursion_offset - 1) + (ctx, List.length defs) defs in + ctx

let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = + (* FIXME: Use lctx_extend_rec! *) List.fold_left (fun (ctx, recursion_offset) (def, e, t) -> let (loc, name) = def in @@ -124,7 +146,9 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = debruijn_warning loc ("Variable Shadowing " ^ name); with Not_found -> ()); let nmap = StringMap.add name n map in - ((n + 1, nmap), cons (recursion_offset, Some def, LetDef e, t) env, f), + ((n + 1, nmap), + lexp_ctx_cons env recursion_offset (Some def) (LetDef e) t, + f), recursion_offset - 1) (ctx, List.length defs) defs

@@ -174,17 +198,17 @@ let replace_by ctx name by = (* lookup and replace *) let rec replace_by' ctx by acc = match ctx with - | Mnil -> debruijn_error dummy_location + | M.Mnil -> debruijn_error dummy_location ("Replace error. This expression does not exist: " ^ name) - | Mcons((_, None, _, _) as elem, tl1, i, tl2) -> + | M.Mcons((_, None, _, _) as elem, tl1, i, tl2) -> (* Skip some elements if possible *) if idx <= i then replace_by' tl1 by (elem::acc) else replace_by' tl2 by (elem::acc) (* replace_by' tl1 by (elem::acc) *)

- | Mcons((_, Some (b, n), _, _) as elem, tl1, i, tl2) -> + | M.Mcons((_, Some (b, n), _, _) as elem, tl1, i, tl2) -> if n = name then - (cons by tl1), acc + (M.cons by tl1), acc else (* Skip some elements if possible *) if idx <= i then replace_by' tl1 by (elem::acc) @@ -193,7 +217,7 @@ let replace_by ctx name by =

let nenv, decls = replace_by' env by [] in (* add old declarations *) - let nenv = List.fold_left (fun ctx elem -> cons elem ctx) nenv decls in + let nenv = List.fold_left (fun ctx elem -> M.cons elem ctx) nenv decls in (a, nenv, b)

(* -------------------------------------------------------------------------- *)

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -223,24 +223,19 @@ let rec check ctx e = | Let (_, defs, e) -> let tmp_ctx = List.fold_left (fun ctx (v, e, t) - -> (match check ctx t with - | Sort (_, Stype _) -> () - | _ -> (U.msg_error "TC" (lexp_location t) - "Def type is not a type!"; ())); - Myers.cons (0, Some v, ForwardRef, t) ctx) - ctx defs in - let (new_ctx, _) = - List.fold_left (fun (ctx,recursion_offset) (v, e, t) - -> let t' = check tmp_ctx e in - assert_type e t t'; - (Myers.cons (recursion_offset, Some v, LetDef e, t) ctx, - recursion_offset - 1)) - (ctx, List.length defs) - defs in + -> (match check ctx t with + | Sort (_, Stype _) -> () + | _ -> (U.msg_error "TC" (lexp_location t) + "Def type is not a type!"; ())); + DB.lctx_extend ctx v ForwardRef t) + ctx defs in + let _ = List.iter (fun (v, e, t) -> assert_type e t (check tmp_ctx e)) + defs in + let new_ctx = DB.lctx_extend_rec ctx defs in check new_ctx e | Arrow (ak, v, t1, l, t2) -> (let k1 = check ctx t1 in - let k2 = check (Myers.cons (0, v, Variable, t1) ctx) t2 in + let k2 = check (DB.lexp_ctx_cons ctx 0 v Variable t1) t2 in match k1, k2 with | (Sort (_, s1), Sort (_, s2)) -> Sort (l, sort_compose l s1 s2) @@ -258,7 +253,7 @@ let rec check ctx e = Arrow (ak, Some v, t, l, (* FIXME: If ak is Aerasable, make sure the var only appears * in type annotations. *) - check (Myers.cons (0, Some v, Variable, t) ctx) e)) + check (DB.lctx_extend ctx v Variable t) e)) | Call (f, args) -> let ft = check ctx f in List.fold_left (fun ft (ak,arg) @@ -287,7 +282,7 @@ let rec check ctx e = Arrow (ak, Some v, t, lexp_location t, (* FIXME: `sort_compose` doesn't do what we want! *) arg_loop args (sort_compose l s s') - (Myers.cons (0, Some v, Variable, t) ctx)) in + (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args (Stype (SortLevel (SLn 0))) ctx in (* FIXME: Check cases! *) tct @@ -317,7 +312,8 @@ let rec check ctx e = (* FIXME: If ak is Aerasable, make sure the var only * appears in type annotations. *) | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes - -> mkctx (Myers.cons (0, vdef, Variable, mkSusp ftype s) ctx) + -> mkctx (DB.lexp_ctx_cons ctx 0 + vdef Variable (mkSusp ftype s)) (S.cons (Var ((match vdef with Some vd -> vd | None -> (l, "_")), 0)) s)

View it on GitLab: https://gitlab.com/monnier/typer/commit/222406c230ecab382880a7ec8804b3dec15f...