Stefan pushed to branch master at Stefan / Typer
Commits: 42ae69a5 by Stefan Monnier at 2016-12-05T09:34:31-05:00 * src/lparse.ml (lexp_check_decls): Provide previous defs during elab
* src/myers.ml (set_nth): New function. * src/opslexp.ml (check'): Check `Let` defs within themselves!
- - - - -
3 changed files:
- src/lparse.ml - src/myers.ml - src/opslexp.ml
Changes:
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -866,13 +866,21 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) (defs : (vdef * pexp * ltype) list) : (vdef * lexp * ltype) list * elab_context = - let declmap = List.fold_right - (fun ((_, vname) as v, pexp, ltp) map -> + let (declmap, nctx) + = List.fold_right + (fun ((_, vname) as v, pexp, ltp) (map, nctx) -> let i = senv_lookup vname nctx in - let adjusted_ltp = push_susp ltp (S.shift (i + 1)) in - IntMap.add i (v, check pexp adjusted_ltp nctx, ltp) - map) - defs IntMap.empty in + assert (i < List.length defs); + match Myers.nth i (ectx_to_lctx nctx) with + | (o, v', ForwardRef, t) + -> let adjusted_ltp = push_susp ltp (S.shift (i + 1)) in + assert (t == ltp); + let e = check pexp adjusted_ltp nctx in + let (ec, lc) = nctx in + (IntMap.add i (v, e, ltp) map, + (ec, Myers.set_nth i (o, v', LetDef e, t) lc)) + | _ -> U.internal_error "Defining same slot!") + defs (IntMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IntMap.bindings declmap)) in decls, ctx_define_rec ectx decls
===================================== src/myers.ml ===================================== --- a/src/myers.ml +++ b/src/myers.ml @@ -75,6 +75,17 @@ let rec nthcdr n l =
let nth n l = car (nthcdr n l)
+(* While `nth` is O(log N), `set_nth` is O(N)! :-( *) +let rec set_nth n v l = match (n, l) with + | 0, Mcons (_, cdr, s, tail) -> Mcons (v, cdr, s, tail) + | n, Mcons (v', cdr, _, _) + -> cons v' (set_nth (n - 1) v cdr) + (* We can't set_nth past the end in general because we'd need to + * magically fill the intermediate entries with something of the right type. + * But we *can* set_nth just past the end. *) + | 0, Mnil -> Mcons (v, Mnil, 1, Mnil) + | _, Mnil -> raise Not_found + (* This operation would be more efficient using Myers's choice of keeping * the length (instead of the skip-distance) in each node. *) let length l =
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -396,20 +396,21 @@ let rec check' meta_ctx erased ctx e = lookup_type ctx v | Susp (e, s) -> check erased ctx (push_susp e s) | Let (l, defs, e) - -> let tmp_ctx = + -> let _ = List.fold_left (fun ctx (v, e, t) -> (let _ = check_type DB.set_empty ctx t in DB.lctx_extend ctx (Some v) ForwardRef t)) ctx defs in let nerased = DB.set_sink (List.length defs) erased in + let nctx = DB.lctx_extend_rec ctx defs in + (* FIXME: Termination checking! Positivity-checker! *) let _ = List.fold_left (fun n (v, e, t) - -> assert_type tmp_ctx e + -> assert_type nctx e (push_susp t (S.shift n)) - (check nerased tmp_ctx e); + (check nerased nctx e); n - 1) (List.length defs) defs in - let new_ctx = DB.lctx_extend_rec ctx defs in - mkSusp (check nerased new_ctx e) + mkSusp (check nerased nctx e) (lexp_defs_subst l S.identity defs) | Arrow (ak, v, t1, l, t2) -> (let k1 = check_type erased ctx t1 in
View it on GitLab: https://gitlab.com/monnier/typer/commit/42ae69a5a5402665c4e423018a2d9d25e890...
Afficher les réponses par date