SMT: do not raise an exception on inner let recs, just encode them imprecisely

Fixes #3991

Author: mtzguido

src/smtencoding/FStarC.SMTEncoding.Encode.fst

@@ -849,6 +849,7 @@ let encode_top_level_let :
         let toks_fvbs = List.rev toks in
         let decls = List.rev decls |> List.flatten in
         (*
+         * GM: Not accurate any more.
          * AR: decls are the declarations for the top-level lets
          *     if one of the let body contains a let rec (inner let rec), we simply return decls at that point, inner let recs are not encoded to the solver yet (see Inner_let_rec below)
          *     the way it is implemented currently is that, the call to encode the let body throws an exception Inner_let_rec which is caught below in this function
@@ -1154,30 +1155,12 @@ let encode_top_level_let :
                                                   is_smt_reifiable_function env.tcenv t))
         then decls, env_decls
         else
-          try
-            if not is_rec
-            then
-              (* Encoding non-recursive definitions *)
-              encode_non_rec_lbdef bindings typs toks_fvbs env
-            else
-              encode_rec_lbdefs bindings typs toks_fvbs env
-          with
-            | Inner_let_rec names ->
-              let plural = List.length names > 1 in
-              let r = List.hd names |> snd in
-              FStarC.TypeChecker.Err.add_errors
-                env.tcenv
-                [(Errors.Warning_DefinitionNotTranslated,
-                  // FIXME
-                  [Errors.text <| Format.fmt3
-                    "Definitions of inner let-rec%s %s and %s enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types"
-                    (if plural then "s" else "")
-                    (List.map fst names |> String.concat ",")
-                    (if plural then "their" else "its")],
-                  r,
-                  Errors.get_ctx () // TODO: fix this, leaking abstraction
-                  )];
-              decls, env_decls  //decls are type declarations for the lets, if there is an inner let rec, only those are encoded to the solver
+          if not is_rec
+          then
+            (* Encoding non-recursive definitions *)
+            encode_non_rec_lbdef bindings typs toks_fvbs env
+          else
+            encode_rec_lbdefs bindings typs toks_fvbs env
 
     with Let_rec_unencodeable ->
       let msg = bindings |> List.map (fun lb -> show lb.lbname) |> String.concat " and " in

src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst

@@ -1465,21 +1465,26 @@ and encode_term (t:typ) (env:env_t) : (term         (* encoding of t, expects t
                 f, decls@decls'@decls''@(mk_decls fsym tkey_hash f_decls (decls@decls'@decls''))
           end
 
+      // Inr means a top-level name
       | Tm_let {lbs=(_, {lbname=Inr _}::_)} ->
         failwith "Impossible: already handled by encoding of Sig_let"
 
+      // A single non-recursive local let
       | Tm_let {lbs=(false, [{lbname=Inl x; lbtyp=t1; lbdef=e1}]); body=e2} ->
         encode_let x t1 e1 e2 env encode_term
 
       | Tm_let {lbs=(false, _::_)} ->
         failwith "Impossible: non-recursive let with multiple bindings"
 
-      | Tm_let {lbs=(_, lbs)} ->
-        let names = lbs |> List.map (fun lb ->
-                                        let {lbname = lbname} = lb in
-                                        let x = Inl?.v lbname in (* has to be Inl *)
-                                        (Ident.string_of_id x.ppname, S.range_of_bv x)) in
-        raise (Inner_let_rec names)
+      // A recursive local let. We encode this imprecisely, just generating a
+      // fresh variable.
+      | Tm_let {lbs=(true, lbs)} ->
+        let f = varops.fresh env.current_module_name "inner_let_rec" in
+        let decl = Term.DeclFun (f, [], Term_sort, Some "Inner let rec") in
+        mkFreeV <| mk_fv (f, Term_sort), [decl] |> mk_decls_trivial
+
+      | Tm_let _ ->
+        failwith "Impossible: all cases handled above (encode_term)."
 
       | Tm_match {scrutinee=e; brs=pats} ->
         encode_match e pats mk_Term_unit env encode_term

src/smtencoding/FStarC.SMTEncoding.Env.fst

@@ -33,8 +33,6 @@ open FStarC.Class.Show
 
 let dbg_PartialApp = Debug.get_toggle "PartialApp"
 
-exception Inner_let_rec of list (string & Range.t) //name of the inner let-rec(s) and their locations
-
 let add_fuel x tl = if (Options.unthrottle_inductives()) then tl else x::tl
 let withenv c (a, b) = (a,b,c)
 let vargs args = List.filter (function (Inl _, _) -> false | _ -> true) args

src/smtencoding/FStarC.SMTEncoding.Solver.fst

@@ -1424,33 +1424,17 @@ let encode_and_ask (can_split:bool) (is_retry:bool) use_env_msg tcenv q : (list
 
 (* Asks the solver and reports errors. Does quake if needed. *)
 let do_solve (can_split:bool) (is_retry:bool) use_env_msg tcenv q : unit =
-  let ans_opt =
-    try Some (encode_and_ask can_split is_retry use_env_msg tcenv q) with
-    (* Each (potentially splitted) query can fail with this error, raise by encode_query.
-     * Note, even though this is a log_issue, the error cannot be turned into a warning
-     * nor ignored. *)
-    | FStarC.SMTEncoding.Env.Inner_let_rec names ->
-      FStarC.TypeChecker.Err.log_issue
-        tcenv tcenv.range
-        (Errors.Error_NonTopRecFunctionNotFullyEncoded, [
-          Errors.text <|
-         Format.fmt1
-           "Could not encode the query since F* does not support precise smtencoding of inner let-recs yet (in this case %s)"
-           (String.concat "," (List.map fst names))]);
-       None
-  in
+  let ans_opt = encode_and_ask can_split is_retry use_env_msg tcenv q in
   match ans_opt with
-  | Some (default_settings::_, ans) when not ans.ok ->
+  | default_settings::_, ans when not ans.ok ->
     report tcenv default_settings ans
 
-  | Some (_, ans) when ans.ok ->
+  | _, ans when ans.ok ->
     () (* trivial or succeeded *)
 
-  | Some ([], ans) when not ans.ok ->
+  | [], ans when not ans.ok ->
     failwith "impossible: bad answer from encode_and_ask"
 
-  | None -> () (* already logged an error *)
-
 let split_and_solve (retrying:bool) use_env_msg tcenv q : unit =
   if retrying && (Debug.any () || Options.query_stats ()) then begin
     Format.print1 "(%s)\tQuery-stats splitting query because retrying failed query\n"

tests/bug-reports/closed/Bug1622.fst

@@ -9,8 +9,12 @@ let pred (args: list bool) : sprop =
   | a::q -> let out:sprop = fun s0 -> out s0 in aux q out
   in aux args (fun _ -> True)
 
-[@@(expect_failure [142])]  //could not encode the query since an inner let-rec aux appears in it
 let lemma_pred (args:list bool) : Lemma (pred args true) =
   match args with
   | [] -> assert_norm (pred args true)
   | _ -> admit()
+
+let lemma_pred' (args:list bool) : Lemma (pred args true) =
+  match args with
+  | [] -> assert_norm (pred [] true)
+  | _ -> admit()

tests/bug-reports/closed/Bug2876.fst

@@ -1,8 +1,6 @@
 module Bug2876
 
-// Fails since we cannot currently encode inner let-recs.
-// The original issue was that this crashed, though, so we are indeed
-// testing that we get a proper error.
-[@@expect_failure [142]]
+// Fails since we encode inner let-recs imprecisely.
+[@@expect_failure [19]]
 let test () =
   assert ((let rec f (x:nat) : Dv nat = f x in f) == (let rec f (x:nat) : Dv nat = f x in f))

tests/bug-reports/closed/Bug3991.fst

@@ -0,0 +1,10 @@
+module Bug3991
+
+noeq
+type mytc (#a:Type0) (s:a) = | X
+
+let mytc_let_rec : mytc (let rec f x = x in ()) = X
+
+let rec foo (x:int) : int = x
+
+let _ = assert (forall x. 1 + x > x)