Don't constant-fold undefined_X functions in monomorphisation

These should be preserved for prover backends.

3 files changed, 36 insertions, 18 deletions

diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index 3ae46657..ea0e50f9 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -298,13 +298,25 @@ let is_env_inconsistent env ksubsts =
     Env.add_constraint (nc_eq (nvar k) nexp) env) ksubsts env in
   prove __POS__ env nc_false
 
+module StringSet = Set.Make(String)
+module StringMap = Map.Make(String)
 
 let const_props defs ref_vars =
   let const_fold exp =
+    (* Constant-fold function applications with constant arguments *)
+    let interpreter_istate =
+      (* Do not interpret undefined_X functions *)
+      let open Interpreter in
+      let undefined_builtin_ids = ids_of_defs (Defs Initial_check.undefined_builtin_val_specs) in
+      let remove_primop id = StringMap.remove (string_of_id id) in
+      let remove_undefined_primops = IdSet.fold remove_primop undefined_builtin_ids in
+      let (lstate, gstate) = Constant_fold.initial_state defs in
+      (lstate, { gstate with primops = remove_undefined_primops gstate.primops })
+    in
     try
       strip_exp exp
       |> infer_exp (env_of exp)
-      |> Constant_fold.rewrite_exp_once (Constant_fold.initial_state defs)
+      |> Constant_fold.rewrite_exp_once interpreter_istate
       |> keep_undef_typ
     with
     | _ -> exp
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 691acd81..dca42c7b 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -834,30 +834,31 @@ let undefined_typschm id typq =
 
 let have_undefined_builtins = ref false
 
+let undefined_builtin_val_specs =
+  [extern_of_string (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}";
+   extern_of_string (mk_id "undefined_bool") "unit -> bool effect {undef}";
+   extern_of_string (mk_id "undefined_bit") "unit -> bit effect {undef}";
+   extern_of_string (mk_id "undefined_int") "unit -> int effect {undef}";
+   extern_of_string (mk_id "undefined_nat") "unit -> nat effect {undef}";
+   extern_of_string (mk_id "undefined_real") "unit -> real effect {undef}";
+   extern_of_string (mk_id "undefined_string") "unit -> string effect {undef}";
+   extern_of_string (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
+   extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
+   extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
+   (* Only used with lem_mwords *)
+   extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
+   extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"]
+
 let generate_undefineds vs_ids (Defs defs) =
-  let gen_vs id str =
-    if (IdSet.mem id vs_ids) then [] else [extern_of_string id str]
-  in
   let undefined_builtins =
     if !have_undefined_builtins then
       []
     else
       begin
         have_undefined_builtins := true;
-        List.concat
-          [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}";
-           gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}";
-           gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}";
-           gen_vs (mk_id "undefined_int") "unit -> int effect {undef}";
-           gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}";
-           gen_vs (mk_id "undefined_real") "unit -> real effect {undef}";
-           gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
-           gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
-           gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
-           gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
-           (* Only used with lem_mwords *)
-           gen_vs (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
-           gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
+        List.filter
+          (fun def -> IdSet.is_empty (IdSet.inter vs_ids (ids_of_def def)))
+          undefined_builtin_val_specs
       end
   in
   let undefined_tu = function
diff --git a/src/initial_check.mli b/src/initial_check.mli
index b41b1818..59c8f0b6 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -87,6 +87,11 @@ val opt_enum_casts : bool ref
    all the loaded files. *)
 val have_undefined_builtins : bool ref
 
+(** Val specs of undefined functions for builtin types that get added to
+    the AST if opt_undefined_gen is set (minus those functions that already
+    exist in the AST). *)
+val undefined_builtin_val_specs : unit def list
+
 (** {2 Desugar and process AST } *)
 
 (** If the generate flag is false, then we won't generate any