From d99b3aa7027a6d05d238f387fa2a629b91690ea9 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Wed, 28 Apr 2021 20:17:16 +0200
Subject: Solve a bug when reifying under a binder

---
 src/trace/smtAtom.ml             | 13 +++++++++++--
 src/trace/smtAtom.mli            |  1 +
 src/trace/smtCommands.ml         |  8 ++++++--
 unit-tests/Tests_verit_tactics.v | 14 ++++++++++++++
 4 files changed, 32 insertions(+), 4 deletions(-)

diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 62cbe99..ff6db6a 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -1096,6 +1096,8 @@ module Atom =
       Hashtbl.find op_coq_terms
 
 
+    exception UnknownUnderForall
+
     let of_coq ?eqsym:(eqsym=false) rt ro reify known_logic env sigma c =
       let op_tbl = Lazy.force op_tbl in
       let get_cst c =
@@ -1361,10 +1363,17 @@ module Atom =
                        let i = Structures.destRel c in
                        let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in
                        Some (Structures.string_of_name n)
-                     else
+                     else if Vars.closed0 c then
                        None
+                     else
+                       (* Uninterpreted expression depending on a quantified variable.
+                          We do not handle it for the moment.
+                          We leave for future work to have "dependent" constants.
+                        *)
+                       raise UnknownUnderForall
             in
-            Op.declare ro c targs tres os in
+            Op.declare ro c targs tres os
+        in
         (try
            let (i, _) = destruct "" op in
            Hashtbl.add op_coq_terms i c (* Chantal: I think we should move it to "Not_found" (otherwise it is already in the table) *)
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index 17a0cd0..37fcd88 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -140,6 +140,7 @@ module Atom :
       val print_atoms : reify_tbl -> string -> unit
 
       (** Given a coq term, build the corresponding atom *)
+      exception UnknownUnderForall
       val of_coq : ?eqsym:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
         reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t
 
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 31a6d9d..080d6c6 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -689,7 +689,7 @@ let gen_rel_name =
 
 let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
   let warn () =
-    Structures.warning "Lemma" ("Discarding the following lemma (axiom form unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr (Structures.extern_constr clemma))));
+    Structures.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr (Structures.extern_constr clemma))));
     None
   in
 
@@ -714,7 +714,11 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
   let core_smt =
     match core_f with
       | Some core_f ->
-         Some (Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env_lemma sigma) rf_quant core_f)
+         (try
+            Some (Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env_lemma sigma) rf_quant core_f)
+          with
+            | Atom.UnknownUnderForall -> warn ()
+         )
       | None -> None
   in
   let forall_args =
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index d1c57f4..7701753 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1249,3 +1249,17 @@ Section SearchApp.
       search x (l1 ++ l2 ++ l3) = search x (l3 ++ l2 ++ l1).
   Proof. verit. Qed.
 End SearchApp.
+
+
+Section UnknowUnderForall.
+  Variable H5 : forall H : Z, Some H = None -> False.
+  Variable H10 : @hd_error Z nil = None.
+  Variable H6 : forall H : list (list Z),
+      hd_error H = match H with
+                   | nil => None
+                   | x :: _ => Some x
+                   end.
+
+  Goal forall (l : list Z) (x : Z), hd_error l = Some x -> l <> nil.
+  Proof. verit. Qed.
+End UnknowUnderForall.
-- 
cgit