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 ++++++--
 3 files changed, 18 insertions(+), 4 deletions(-)

(limited to 'src')

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 =
-- 
cgit