[Git][monnier/typer][master] * src/elab.ml (lexp_check_decls): Fix broken odd/even example.
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... -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/77981fd4dc8bc6af20e1db5148a9fb14f4... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Stefan