CHANGES.md

 :x: marks a potential source of incompatibility
 
+Version 1.1.1, December 17, 2018
+--------------------------------
+
+Bug fixes
+  * prevented broken extraction of `any`
+  * fixed evaluation order when extracting nested mutators
+  * fixed extraction of nested recursive polymorphic functions
+  * fixed cloning of expressions raising exceptions
+
 Version 1.1.0, October 17, 2018
 -------------------------------
 
@@ -8,7 +17,7 @@ Core
   * coercions are now supported for `if` and `match` branches
   * `interrupt` command should now properly interrupt running provers.
   * clearer typing error messages thanks to printing qualified names
-  * fixed handling of prover upgrades, resurected the policy
+  * fixed handling of prover upgrades, resurrected the policy
     "duplicate" and added a policy "remove"
 
 API
@@ -25,7 +34,7 @@ Language
   * range types have now a default ordering to be used in `variant` clause
 
 Standard library
-  * library `Ieee_float`: floating-point operations can now be used in
+  * library `ieee_float`: floating-point operations can now be used in
     programs
 
 Transformations

Makefile.in

@@ -1576,7 +1576,7 @@ endif
 
 ALTERGODIR=src/trywhy3/alt-ergo
 
-JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -g -package js_of_ocaml.syntax \
+JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -g -package js_of_ocaml.ppx \
         -package ocplib-simplex -I src/trywhy3 \
 	-I $(ALTERGODIR)/lib/util \
 	-I $(ALTERGODIR)/lib/structures \
@@ -1700,8 +1700,6 @@ src/trywhy3/%.cmi: src/trywhy3/%.mli
 
 src/trywhy3/%.cmo: BFLAGS += -w -48
 
-src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo: BFLAGS += -syntax camlp4o
-
 clean::
 	rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte src/trywhy3/trywhy3.cm* \
 	 src/trywhy3/why3_worker.js src/trywhy3/why3_worker.byte src/trywhy3/why3_worker.cm* \

Version

-VERSION=1.1.0
+VERSION=1.1.1

bench/bench

@@ -98,6 +98,7 @@ drivers () {
 }
 
 valid_goals () {
+    bin/why3$suffix --list-provers | grep -q Alt-Ergo || return 0
     pgm="bin/why3prove$suffix"
     test -d $1 || exit 1
     for f in $1/*.mlw; do
@@ -113,6 +114,7 @@ valid_goals () {
 }
 
 invalid_goals () {
+    bin/why3$suffix --list-provers | grep -q Alt-Ergo || return 0
     pgm="bin/why3prove$suffix"
     test -d $1 || exit 1
     for f in $1/*.mlw; do
@@ -303,29 +305,6 @@ goods examples/prover "-L examples/prover --debug ignore_unused_vars"
 goods examples/in_progress
 echo ""
 
-echo "=== Checking replay (no prover) ==="
-replay bench/replay
-replay examples/stdlib --merging-only
-replay examples/bts --merging-only
-replay examples/tests --merging-only
-replay examples/tests-provers --merging-only
-replay examples/check-builtin --merging-only
-replay examples/logic --merging-only
-replay examples --merging-only
-replay examples/foveoos11-cm --merging-only
-replay examples/WP_revisited --merging-only
-replay examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps --merging-only"
-replay examples/bitvectors "-L examples/bitvectors --merging-only"
-replay examples/avl "-L examples/avl --merging-only"
-replay examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication --merging-only"
-replay examples/double_wp "-L examples/double_wp --merging-only"
-replay examples/in_progress/ring_decision "-L examples/in_progress/ring_decision --merging-only"
-replay examples/multiprecision "-L examples/multiprecision --merging-only"
-replay examples/prover "-L examples/prover --merging-only --debug ignore_unused_vars"
-#replay examples/in_progress --merging-only
-#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
-echo ""
-
 echo "=== Checking valid goals ==="
 valid_goals bench/valid
 echo ""
@@ -369,7 +348,6 @@ execute examples/vstte10_queens.mlw NQueens.test8
 # examples/residual.mlw Test.test_astar
 echo ""
 
-
 echo "=== Checking extraction to OCaml ==="
 extract_and_run examples/euler001 euler001.ml 1000000
 extract_and_run examples/gcd gcd.ml 6 15
@@ -385,6 +363,29 @@ extract_and_test_wmp examples/in_progress/multiprecision
 extract_and_test_wmp examples/multiprecision
 echo ""
 
+echo "=== Checking replay (no prover) ==="
+replay bench/replay
+replay examples/stdlib --merging-only
+replay examples/bts --merging-only
+replay examples/tests --merging-only
+replay examples/tests-provers --merging-only
+replay examples/check-builtin --merging-only
+replay examples/logic --merging-only
+replay examples --merging-only
+replay examples/foveoos11-cm --merging-only
+replay examples/WP_revisited --merging-only
+replay examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps --merging-only"
+replay examples/bitvectors "-L examples/bitvectors --merging-only"
+replay examples/avl "-L examples/avl --merging-only"
+replay examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication --merging-only"
+replay examples/double_wp "-L examples/double_wp --merging-only"
+replay examples/in_progress/ring_decision "-L examples/in_progress/ring_decision --merging-only"
+replay examples/multiprecision "-L examples/multiprecision --merging-only"
+replay examples/prover "-L examples/prover --merging-only --debug ignore_unused_vars"
+#replay examples/in_progress --merging-only
+#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
+echo ""
+
 echo "=== Checking --list-* ==="
 list_stuff --list-transforms
 list_stuff --list-printers

configure

 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.69 for Why3 1.1.0.
+# Generated by GNU Autoconf 2.69 for Why3 1.1.1.
 #
 #
 # Copyright (C) 1992-1996, 1998-2012 Free Software Foundation, Inc.
@@ -636,8 +636,8 @@ MAKEFLAGS=
 # Identity of this package.
 PACKAGE_NAME='Why3'
 PACKAGE_TARNAME='why3'
-PACKAGE_VERSION='1.1.0'
-PACKAGE_STRING='Why3 1.1.0'
+PACKAGE_VERSION='1.1.1'
+PACKAGE_STRING='Why3 1.1.1'
 PACKAGE_BUGREPORT=''
 PACKAGE_URL=''
 
@@ -1348,7 +1348,7 @@ if test "$ac_init_help" = "long"; then
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF
-\`configure' configures Why3 1.1.0 to adapt to many kinds of systems.
+\`configure' configures Why3 1.1.1 to adapt to many kinds of systems.
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
@@ -1410,7 +1410,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
-     short | recursive ) echo "Configuration of Why3 1.1.0:";;
+     short | recursive ) echo "Configuration of Why3 1.1.1:";;
    esac
   cat <<\_ACEOF
 
@@ -1515,7 +1515,7 @@ fi
 test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
-Why3 configure 1.1.0
+Why3 configure 1.1.1
 generated by GNU Autoconf 2.69
 
 Copyright (C) 2012 Free Software Foundation, Inc.
@@ -1570,7 +1570,7 @@ cat >config.log <<_ACEOF
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
-It was created by Why3 $as_me 1.1.0, which was
+It was created by Why3 $as_me 1.1.1, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   $ $0 $@
@@ -6002,7 +6002,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # report actual input values of CONFIG_FILES etc. instead of their
 # values after options handling.
 ac_log="
-This file was extended by Why3 $as_me 1.1.0, which was
+This file was extended by Why3 $as_me 1.1.1, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
@@ -6059,7 +6059,7 @@ _ACEOF
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
 ac_cs_version="\\
-Why3 config.status 1.1.0
+Why3 config.status 1.1.1
 configured by $0, generated by GNU Autoconf 2.69,
   with options \\"\$ac_cs_config\\"
 

debian/changelog

+why3 (1.1.1-1) unstable; urgency=medium
+
+  * New upstream version.
+  * Fix whitespace in debian/{control/changelog}
+
+ -- Ralf Treinen <treinen@debian.org>  Tue, 18 Dec 2018 04:50:38 +0100
+
 why3 (1.1.0-1) unstable; urgency=medium
 
   * New upstream version. Works with cvc4 version 1.6 (closes: #906001)
@@ -221,4 +228,3 @@ why3 (0.87.0-1) unstable; urgency=low
   * Initial Release (closes: #797696)
 
  -- Ralf Treinen <treinen@debian.org>  Sun, 20 Mar 2016 18:44:54 +0100
-

doc/manual.tex

@@ -118,7 +118,7 @@
 %BEGIN LATEX
 \begin{LARGE}
 %END LATEX
-  Version \whyversion{}, October 2018
+  Version \whyversion{}, December 2018
 %BEGIN LATEX
 \end{LARGE}
 %END LATEX

src/core/ident.ml

@@ -254,6 +254,12 @@ let create_ident_printer ?(sanitizer = same) sl =
     sanitizer = sanitizer;
     blacklist = sl }
 
+let duplicate_ident_printer id_printer =
+  {id_printer with
+   indices = Hstr.copy id_printer.indices;
+   values  = Hid.copy id_printer.values;
+  }
+
 let known_id printer id =
   try
     (let _ = Hid.find printer.values id in true)

src/core/ident.mli

@@ -115,6 +115,13 @@ val create_ident_printer :
   ?sanitizer : (string -> string) -> string list -> ident_printer
 (** start a new printer with a sanitizing function and a blacklist *)
 
+val duplicate_ident_printer: ident_printer -> ident_printer
+(** This is used to avoid editing the current (mutable) printer when raising
+    exception or printing information messages for the user.
+    This should be avoided for any other usage including display of the whole
+    task.
+*)
+
 val id_unique :
   ident_printer -> ?sanitizer : (string -> string) -> ident -> string
 (** use ident_printer to generate a unique name for ident

src/mlw/cakeml_printer.ml

@@ -243,8 +243,6 @@ module Print = struct
         forget_let_defn let_def
     | Eabsurd ->
         fprintf fmt (protect_on paren "assert false (* absurd *)")
-    | Ehole -> ()
-    | Eany _ -> assert false
     | Eapp (rs, []) when rs_equal rs rs_true ->
         fprintf fmt "true"
     | Eapp (rs, []) when rs_equal rs rs_false ->
@@ -432,6 +430,10 @@ module Print = struct
   let rec print_decl info fmt = function
     | Dlet ldef ->
         print_let_def info fmt ldef
+    | Dval ({pv_vs}, _) ->
+        let loc = pv_vs.vs_name.id_loc in
+        Loc.errorm ?loc "cannot extract top-level undefined constant %a@."
+          (print_lident info) pv_vs.vs_name
     | Dtype dl ->
         print_list newline (print_type_decl info) fmt dl
     | Dexn (xs, None) ->

src/mlw/compile.ml

@@ -280,6 +280,8 @@ module Translate = struct
         ML.e_let ld (expr info svar mask e2) (ML.I e.e_ity) mask eff attrs
     | Elet (LDsym (rs, _), ein) when rs_ghost rs ->
         expr info svar mask ein
+    | Elet (LDsym (_, {c_node = Cpur (_, _); _}), _) ->
+        assert false (* necessarily handled above *)
     | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
         Debug.dprintf debug_compile "compiling local function definition %s@."
           rs.rs_name.id_string;
@@ -309,6 +311,8 @@ module Translate = struct
         let ld = ML.sym_defn rsf res (params cty.cty_args) eapp in
         let ein = expr info svar mask ein in
         ML.e_let ld ein (ML.I e.e_ity) mask eff attrs
+    | Elet (LDsym (_, {c_node = Cany; _}), _) -> let loc = e.e_loc in
+        Loc.errorm ?loc "This expression cannot be extracted"
     | Elet (LDrec rdefl, ein) ->
         let rdefl = filter_out_ghost_rdef rdefl in
         List.iter
@@ -322,7 +326,7 @@ module Translate = struct
                 let args' = List.map (fun (_, ty, _) -> ty) args in
                 let svar  = List.fold_left add_tvar Stv.empty args' in
                 add_tvar svar res in
-              let new_svar = Stv.diff svar new_svar in
+              let new_svar = Stv.diff new_svar svar in
               let ef = expr info (Stv.union svar new_svar) ef.e_mask ef in
               { ML.rec_sym  = rs1; ML.rec_args = args; ML.rec_exp  = ef;
                 ML.rec_res  = res; ML.rec_svar = new_svar; }
@@ -369,8 +373,10 @@ module Translate = struct
         Debug.dprintf debug_compile "compiling a lambda expression@.";
         let ef = expr info svar e.e_mask ef in
         ML.e_fun (params cty.cty_args) ef (ML.I e.e_ity) mask eff attrs
-    | Eexec ({c_node = Cany}, _) ->
-        ML.mk_hole
+    | Eexec ({c_node = Cpur (_, _); _ }, _) ->
+        assert false (* necessarily ghost *)
+    | Eexec ({c_node = Cany}, _) -> let loc = e.e_loc in
+        Loc.errorm ?loc "This expression cannot be extracted"
     | Eabsurd ->
         ML.e_absurd (ML.I e.e_ity) mask eff attrs
     | Eassert _ ->
@@ -438,8 +444,6 @@ module Translate = struct
           let ty = if ity_equal xs.xs_ity ity_unit then None
             else Some (mlty_of_ity xs.xs_mask xs.xs_ity) in
         ML.mk_expr (ML.Eexn (xs, ty, e1)) (ML.I e.e_ity) mask eff attrs
-    | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _)
-    | Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole
 
   and ebranch info svar mask ({pp_pat = p; pp_mask = m}, e) =
     (* if the [case] expression is not ghost but there is (at least) one ghost
@@ -509,7 +513,7 @@ module Translate = struct
         Debug.dprintf debug_compile "compiling undifined constant %a@"
           print_pv pv;
         let ty = mlty_of_ity cty.cty_mask cty.cty_result in
-        [ML.Dlet (ML.Lvar (pv, ML.e_any ty cty))]
+        [ML.Dval (pv, ty)]
     | PDlet (LDvar (pv, e)) ->
         Debug.dprintf debug_compile "compiling top-level symbol %a@."
           print_pv pv;
@@ -610,10 +614,11 @@ module Transform = struct
   open Mltree
 
   let no_reads_writes_conflict spv spv_mreg =
-    let is_not_write {pv_ity = ity} = match ity.ity_node with
-      | Ityreg rho -> not (Mreg.mem rho spv_mreg)
-      | _ -> true in
-    Spv.for_all is_not_write spv
+    (* let is_not_write {pv_ity = ity} = match ity.ity_node with
+     *   | Ityreg rho -> not (Mreg.mem rho spv_mreg)
+     *   | _ -> true in
+     * Spv.for_all is_not_write spv *)
+    Spv.is_empty (pvs_affected spv_mreg spv)
 
   let mk_list_eb ebl f =
     let mk_acc e (e_acc, s_acc) =
@@ -691,7 +696,7 @@ module Transform = struct
         mk (Eraise (exn, Some e)), spv
     | Eassign _al ->
         e, Spv.empty
-    | Econst _ | Eabsurd | Ehole | Eany _ -> e, Spv.empty
+    | Econst _ | Eabsurd -> e, Spv.empty
     | Eignore e ->
         let e, spv = expr info subst e in
         mk (Eignore e), spv
@@ -719,7 +724,7 @@ module Transform = struct
     { r with rec_exp = rec_exp }, spv
 
   let rec pdecl info = function
-    | Dtype _ | Dexn _ as d -> d
+    | Dtype _ | Dexn _ | Dval _ as d -> d
     | Dmodule (id, dl) ->
         let dl = List.map (pdecl info) dl in Dmodule (id, dl)
     | Dlet def ->

src/mlw/cprinter.ml

@@ -1066,7 +1066,6 @@ module MLToC = struct
          | None, None -> raise (Unsupported ("assign not in driver")) in
        [], C.(Sexpr(Ebinop(Bassign, t, C.Evar v.pv_vs.vs_name)))
     | Eassign _ -> raise (Unsupported "assign")
-    | Ehole | Eany _ -> assert false
     | Eexn (_,_,e) -> expr info env e
     | Eignore e ->
        [], C.Sseq(C.Sblock(expr info {env with computes_return_value = false} e),

src/mlw/ity.ml

@@ -1231,6 +1231,17 @@ let eff_escape eff ity =
     Spv.fold add_fd fs esc in
   Mreg.fold add_write eff.eff_writes esc
 
+(* affected program variables by some writes effect *)
+
+let ity_affected wr ity =
+  Util.any ity_rch_fold (Mreg.contains wr) ity
+
+let pv_affected wr v = ity_affected wr v.pv_ity
+
+let pvs_affected wr pvs =
+  if Mreg.is_empty wr then Spv.empty
+  else Spv.filter (pv_affected wr) pvs
+
 (** specification *)
 
 type pre = term   (* precondition: pre_fmla *)

src/mlw/ity.mli

@@ -399,6 +399,18 @@ val mask_adjust : effect -> ity -> mask -> mask
 
 val eff_escape : effect -> ity -> Sity.t
 
+val ity_affected : 'a Mreg.t -> ity -> bool
+(** [ity_affected wr ity] returns [true] if the regions of [ity] are contained
+    in the effect described by [wr]. *)
+
+val pv_affected  : 'a Mreg.t -> pvsymbol -> bool
+(** [pv_affected wr pv] returns [true] if the regions of [pv] are contained in
+    the effect described by [wr]. *)
+
+val pvs_affected : 'a Mreg.t -> Spv.t -> Spv.t
+(** [pvs_affected wr pvs] returns the set of pvsymbols from [pvs] whose regions
+    are contained in the effect described by [wr]. *)
+
 (** {2 Computation types (higher-order types with effects)} *)
 
 type pre = term   (** precondition: pre_fmla *)

src/mlw/mlinterp.ml

@@ -776,10 +776,6 @@ let rec interp_expr info (e:Mltree.expr) : value =
                          raise CannotReduce
   | Eabsurd -> Debug.dprintf debug_interp "Eabsurd@.";
                raise CannotReduce
-  | Ehole -> Debug.dprintf debug_interp "Ehole@.";
-             raise CannotReduce
-  | Eany _ -> Debug.dprintf debug_interp "Eany@.";
-             raise CannotReduce
   | Ematch (e, l, bl) ->
      Debug.dprintf debug_interp "Ematch@.";
      begin match interp_expr info e with

src/mlw/mltree.ml

@@ -63,9 +63,7 @@ and expr_node =
   | Eraise  of xsymbol * expr option
   | Eexn    of xsymbol * ty option * expr
   | Eignore of expr
-  | Eany    of ty
   | Eabsurd
-  | Ehole
 
 and reg_branch = pat * expr
 
@@ -105,6 +103,7 @@ type its_defn = {
 type decl =
   | Dtype   of its_defn list
   | Dlet    of let_def
+  | Dval    of pvsymbol * ty (* top-level constants, of the form [val c: tau] *)
   | Dexn    of xsymbol * ty option
   | Dmodule of string * decl list
 
@@ -135,6 +134,7 @@ let rec get_decl_name = function
   | Dlet (Lvar ({pv_vs={vs_name=id}}, _))
   | Dlet (Lsym ({rs_name=id}, _, _, _))
   | Dlet (Lany ({rs_name=id}, _, _))
+  | Dval ({pv_vs={vs_name=id}}, _)
   | Dexn ({xs_name=id}, _) -> [id]
   | Dmodule (_, dl) -> List.concat (List.map get_decl_name dl)
 
@@ -184,7 +184,7 @@ and iter_deps_pat f = function
   | Pas (p, _) -> iter_deps_pat f p
 
 and iter_deps_expr f e = match e.e_node with
-  | Econst _ | Evar _ | Eabsurd | Ehole | Eany _ -> ()
+  | Econst _ | Evar _ | Eabsurd -> ()
   | Eapp (rs, exprl) ->
       f rs.rs_name; List.iter (iter_deps_expr f) exprl
   | Efun (args, e) ->
@@ -254,7 +254,7 @@ let rec iter_deps f = function
            iter_deps_expr f e; iter_deps_ty f res) rdef
   | Dlet (Lvar (_, e)) -> iter_deps_expr f e
   | Dexn (_, None) -> ()
-  | Dexn (_, Some ty) -> iter_deps_ty f ty
+  | Dexn (_, Some ty) | Dval (_, ty) -> iter_deps_ty f ty
   | Dmodule (_, dl) -> List.iter (iter_deps f) dl
 
 let ity_unit = I Ity.ity_unit
@@ -281,12 +281,6 @@ let is_unit = function
 
 let enope = Eblock []
 
-let e_any ty c =
-  mk_expr (Eany ty) (C c) MaskVisible Ity.eff_empty Sattr.empty
-
-let mk_hole =
-  mk_expr Ehole (I Ity.ity_unit) MaskVisible Ity.eff_empty Sattr.empty
-
 let mk_var id ty ghost = (id, ty, ghost)
 
 let mk_var_unit =
@@ -350,7 +344,7 @@ let e_absurd =
 
 let e_seq e1 e2 =
   let e = match e1.e_node, e2.e_node with
-    | (Eblock [] | Ehole), e | e, (Eblock [] | Ehole) -> e
+    | Eblock [], e | e, Eblock [] -> e
     | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
     | _, Eblock e2 -> Eblock (e1 :: e2)
     | Eblock e1, _ -> Eblock (e1 @ [e2])

src/mlw/ocaml_printer.ml

@@ -276,12 +276,12 @@ module Print = struct
     | Eapp (s, []) -> rs_equal s rs_false
     | _ -> false
 
-  let check_val_in_drv info ({rs_name = {id_loc = loc}} as rs) =
+  let check_val_in_drv info loc id =
     (* here [rs] refers to a [val] declaration *)
-    match query_syntax info.info_convert rs.rs_name,
-          query_syntax info.info_syn     rs.rs_name with
+    match query_syntax info.info_convert id,
+          query_syntax info.info_syn id with
     | None, None (* when info.info_flat *) ->
-        Loc.errorm ?loc "Function %a cannot be extracted" Expr.print_rs rs
+        Loc.errorm ?loc "Symbol %a cannot be extracted" (print_lident info) id
     | _ -> ()
 
   let is_mapped_to_int info ity =
@@ -389,9 +389,6 @@ module Print = struct
         (print_expr info) e
 
   and print_let_def ?(functor_arg=false) info fmt = function
-    | Lvar (pv, {e_node = Eany ty}) when functor_arg ->
-        fprintf fmt "@[<hov 2>val %a : %a@]"
-          (print_lident info) (pv_name pv) (print_ty info) ty;
     | Lvar (pv, e) ->
         fprintf fmt "@[<hov 2>let %a =@ %a@]"
           (print_lident info) (pv_name pv) (print_expr info) e
@@ -409,8 +406,7 @@ module Print = struct
                 (if fst then "let rec" else "and")
                 (print_lident info) rs1.rs_name
                 (print_fun_type_args info) (args, s, res, e);
-              forget_vars args
-        in
+              forget_vars args in
         print_list_next newline print_one fmt rdef;
     | Lany (rs, res, []) when functor_arg ->
         fprintf fmt "@[<hov 2>val %a : %a@]"
@@ -424,7 +420,7 @@ module Print = struct
           (print_list arrow (print_ty_arg info)) args
           (print_ty info) res;
         forget_vars args
-    | Lany (rs, _, _) -> check_val_in_drv info rs
+    | Lany ({rs_name}, _, _) -> check_val_in_drv info rs_name.id_loc rs_name
 
   and print_expr ?(paren=false) info fmt e =
     match e.e_node with
@@ -447,8 +443,6 @@ module Print = struct
         forget_let_defn let_def
     | Eabsurd ->
         fprintf fmt (protect_on paren "assert false (* absurd *)")
-    | Ehole -> ()
-    | Eany _ -> assert false
     | Eapp (rs, []) when rs_equal rs rs_true ->
         fprintf fmt "true"
     | Eapp (rs, []) when rs_equal rs rs_false ->
@@ -617,7 +611,7 @@ module Print = struct
   let rec is_signature_decl info = function
     | Dtype _ -> true
     | Dlet (Lany _) -> true
-    | Dlet (Lvar (_, {e_node = Eany _})) -> true
+    | Dval _ -> true
     | Dlet _ -> false
     | Dexn _ -> true
     | Dmodule (_, dl) -> is_signature info dl
@@ -634,9 +628,18 @@ module Print = struct
       | dl -> List.rev args, dl in
     extract [] dl
 
+  let print_top_val ?(functor_arg=false) info fmt ({pv_vs}, ty) =
+    if functor_arg then
+      fprintf fmt "@[<hov 2>val %a : %a@]"
+        (print_lident info) pv_vs.vs_name (print_ty info) ty
+    else
+      check_val_in_drv info pv_vs.vs_name.id_loc pv_vs.vs_name
+
   let rec print_decl ?(functor_arg=false) info fmt = function
     | Dlet ldef ->
         print_let_def info ~functor_arg fmt ldef
+    | Dval (pv, ty) ->
+        print_top_val info ~functor_arg fmt (pv, ty)
     | Dtype dl ->
         print_list_next newline (print_type_decl info) fmt dl
     | Dexn (xs, None) ->

src/mlw/pmodule.ml

@@ -793,8 +793,8 @@ let rec clone_expr cl sm e = e_attr_copy e (match e.e_node with
       e_for v'
         (e_var (sm_find_pv sm f)) dir (e_var (sm_find_pv sm t))
         i' (clone_invl cl ism invl) (clone_expr cl ism e)
-  | Eraise (xs, e) ->
-      e_raise (sm_find_xs sm xs) (clone_expr cl sm e) (clone_ity cl e.e_ity)
+  | Eraise (xs, e1) ->
+      e_raise (sm_find_xs sm xs) (clone_expr cl sm e1) (clone_ity cl e.e_ity)
   | Eexn ({xs_name = id; xs_mask = mask; xs_ity = ity} as xs, e) ->
       let xs' = create_xsymbol (id_clone id) ~mask (clone_ity cl ity) in
       e_exn xs' (clone_expr cl (sm_save_xs sm xs xs') e)