Stefan pushed to branch master at Stefan / Typer
Commits: 77981fd4 by Stefan Monnier at 2021-02-09T18:04:24-05:00 * src/elab.ml (lexp_check_decls): Fix broken odd/even example.
* src/REPL.ml (main): Re-raise internal error, so OCAMLRUNPARAM=b gives a proper backtrace.
* samples/nat.typer (even1): Make it trickier to catch the previous error.
- - - - -
4 changed files:
- samples/nat.typer - src/REPL.ml - src/debruijn.ml - src/elab.ml
Changes:
===================================== samples/nat.typer ===================================== @@ -18,8 +18,14 @@ one = succ zero; two = succ one; three = succ two;
+%% `even1` is added just to have a more complex mutual-recursion, +%% where the order of declarations and definitions don't match at all. +even1 : Nat -> Int; even : Nat -> Int; odd : Nat -> Int; +even1 = lambda (n : Nat) -> case n + | zero => 1 + | succ y => (odd y); odd = lambda (n : Nat) -> case n | zero => 0 | succ y => (even y); @@ -29,6 +35,7 @@ even = lambda (n : Nat) -> case n | succ y => (odd y);
+ a = odd one; b = even one; c = odd two;
===================================== src/REPL.ml ===================================== @@ -1,6 +1,6 @@ (* REPL.ml --- Read Eval Print Loop (REPL)
-Copyright (C) 2016-2018 Free Software Foundation, Inc. +Copyright (C) 2016-2021 Free Software Foundation, Inc.
Author: Pierre Delaunay pierre.delaunay@hec.ca
@@ -315,8 +315,9 @@ let main () = with | Log.Stop_Compilation msg -> handle_stopped_compilation msg; exit 1 - | Log.Internal_error msg -> - handle_stopped_compilation ("Internal error: " ^ msg); exit 1 + | (Log.Internal_error msg) as e -> + handle_stopped_compilation ("Internal error: " ^ msg); + raise e | Log.User_error msg -> handle_stopped_compilation ("Fatal user error: " ^ msg); exit 1 ) in
===================================== src/debruijn.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2021 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types.
===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2021 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -1131,21 +1131,25 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let ectx = let (_, a, b, c) = ectx in let (grm, _, _, _) = nctx in (grm, a, b, c) in - let (declmap, nctx) + let (declmap) = List.fold_right - (fun ((l, vname), pexp) (map, nctx) -> + (fun ((l, vname), sexp) (map) -> let i = senv_lookup vname nctx in assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with | (v', ForwardRef, t) -> let adjusted_t = push_susp t (S.shift (i + 1)) in - let e = check pexp adjusted_t nctx in - let (grm, ec, lc, sl) = nctx in + (* We elab `sexp` within the original `nctx`, i.e. + * the context where the other vars don't have + * a definition yet. This is because we can't yet + * build the proper `nctx`: a partially filled + * mutually-recursive block would not have the + * proper format, e.g. for `lctx_view`! *) + let e = check sexp adjusted_t nctx in let d = (v', LetDef (i + 1, e), t) in - (IMap.add i ((l, Some vname), e, t) map, - (grm, ec, Myers.set_nth i d lc, sl)) + (IMap.add i ((l, Some vname), e, t) map) | _ -> Log.internal_error "Defining same slot!") - defs (IMap.empty, nctx) in + defs (IMap.empty) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in decls, ctx_define_rec ectx decls
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/77981fd4dc8bc6af20e1db5148a9fb14f4...