[Git][monnier/typer][master] * src/lparse.ml (_lexp_rec_decl): Call lexp_p_infer with complete context
Stefan pushed to branch master at Stefan / Typer Commits: 8458627d by Stefan Monnier at 2016-09-29T10:51:32-04:00 * src/lparse.ml (_lexp_rec_decl): Call lexp_p_infer with complete context This fixes an assertion failure in "EVAL - Mutually Recursive Definition". - - - - - 2 changed files: - src/debruijn.ml - src/lparse.ml Changes: ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -109,9 +109,9 @@ let rec senv_lookup (name: string) (ctx: elab_context): int = 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 + 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 ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -808,9 +808,7 @@ and _lexp_rec_decl decls ctx i = * i.e let decl parsing *) (* to compute recursive offset *) - let n = (List.length decls) in let lst = ref [] in - (* print_int n; print_string "\n"; *) (* add all elements to the environment *) let tctx = List.fold_left (fun vctx decl -> @@ -826,23 +824,23 @@ and _lexp_rec_decl decls ctx i = lexp_fatal dloc "use lexp_decl_macro to parse macro decls") ctx decls in (* ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) *) - let i = ref 0 in + let i = ref (1 + List.length decls) in let ctx = List.fold_left (fun vctx decl -> - i := !i + 1; + i := !i - 1; match decl with (* +1 because we allow each definition to be recursive *) (* lexp infer *) | Ldecl ((l, s), Some pxp, None) -> let lxp, ltp = lexp_p_infer pxp tctx in lst := ((l, s), lxp, ltp)::!lst; - (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp) + (env_extend_rec (!i) vctx (l, s) (LetDef lxp) ltp) (* lexp check *) | Ldecl ((l, s), Some pxp, Some ptp) -> - let ltp, _ = lexp_p_infer ptp vctx in + let ltp, _ = lexp_p_infer ptp tctx in let lxp = lexp_p_check pxp ltp tctx in lst := ((l, s), lxp, ltp)::!lst; - (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp) + (env_extend_rec (!i) vctx (l, s) (LetDef lxp) ltp) (* macros *) | Lmcall (a, sargs) -> View it on GitLab: https://gitlab.com/monnier/typer/commit/8458627dcbd32d188256633bfe9220972b29...
Afficher les réponses par date
participants (1)
-
Stefan