From 907cb562f511e3bbd3f84011e5d3e101f00c4252 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Wed, 5 May 2021 16:06:38 +0200
Subject: Reify applied polymorphic terms with compdec

---
 src/PropToBool.v                 | 25 ++++++++++++++++++++++++-
 src/trace/smtAtom.ml             |  8 +++++++-
 src/trace/smtBtype.ml            |  2 +-
 unit-tests/Tests_verit_tactics.v | 31 +++++++++++++++++++++++++++++++
 4 files changed, 63 insertions(+), 3 deletions(-)

diff --git a/src/PropToBool.v b/src/PropToBool.v
index 1d85bb0..00cba37 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -210,10 +210,33 @@ Ltac prop2bool_hyp H :=
     try clear H; let H := fresh H in assert (H:=H'); clear H'
   ].
 
+
+Ltac remove_compdec_hyp H :=
+  let TH := type of H in
+  match TH with
+  | forall p : CompDec ?A, _ =>
+    match goal with
+    | [ p' : CompDec A |- _ ] =>
+      let H1 := fresh in
+      assert (H1 := H p'); clear H; assert (H := H1); clear H1;
+      remove_compdec_hyp H
+    | _ =>
+      idtac 1;
+      let c := fresh "c" in
+      assert (c : CompDec A);
+      [ auto with typeclass_instances
+      | let H1 := fresh in
+        assert (H1 := H c); clear H; assert (H := H1); clear H1;
+        remove_compdec_hyp H ]
+    end
+  | _ => idtac
+  end.
+
+
 Ltac prop2bool_hyps Hs :=
   lazymatch Hs with
   | (?Hs1, ?Hs2) => prop2bool_hyps Hs1; [ .. | prop2bool_hyps Hs2]
-  | ?H => try prop2bool_hyp H
+  | ?H => remove_compdec_hyp H; try prop2bool_hyp H
   end.
 
 
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index ff6db6a..f0a907a 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -1338,10 +1338,16 @@ module Atom =
         | _ -> assert false
 
       and mk_unknown c args ty =
+        (* Collecting types and CompDec allows to reify applied
+           polymorphic functions *)
         let rec collect_types = function
           | [] -> ([],[])
           | x::xs as l ->
-             if Constr.iskind (Structures.retyping_get_type_of env sigma x) then
+             let ty = Structures.retyping_get_type_of env sigma x in
+             if Constr.iskind ty ||
+                  let c, _ = Structures.decompose_app ty in
+                  Structures.eq_constr c (Lazy.force cCompDec)
+             then
                let (l1, l2) = collect_types xs in
                (x::l1, l2)
              else
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index 94339f6..1e05dc4 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -13,7 +13,7 @@
 open SmtMisc
 open CoqTerms
 
-(** Syntaxified version of Coq type *)
+(** Reified version of Coq type *)
 
 type uninterpreted_type =
   (* Uninterpreted type for which a CompDec is already known
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 7701753..bd4082f 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1263,3 +1263,34 @@ Section UnknowUnderForall.
   Goal forall (l : list Z) (x : Z), hd_error l = Some x -> l <> nil.
   Proof. verit. Qed.
 End UnknowUnderForall.
+
+
+Section CompDecHypotheses.
+  Variable A : Type.
+  Variable H : CompDec A.
+  Variable x : A.
+  Variable l2 : list A.
+  Hypothesis H1 : forall (x y : A) (x0 y0 : list A),
+      x :: x0 = y :: y0 -> y = x /\ y0 = x0.
+  Hypothesis H2 : forall (H : A) (H0 : list A), nil = H :: H0 -> False.
+  Hypothesis H7_bool : forall (H : bool) (H0 H1 : list bool),
+      ((H :: H0) ++ H1)%list = H :: H0 ++ H1.
+  Hypothesis H7_A : forall (H : A) (H0 H1 : list A),
+      ((H :: H0) ++ H1)%list = H :: H0 ++ H1.
+  Hypothesis H6_bool : forall H : list bool, (nil ++ H)%list = H.
+  Hypothesis H6_A : forall H : list A, (nil ++ H)%list = H.
+  Variable search : forall {A : Type} {H: CompDec A}, A -> list A -> bool.
+  Arguments search {_ _} _ _.
+  Hypothesis H5_bool : forall (H : CompDec bool) (H0 H1 : bool) (H2 : list bool),
+      search H0 (H1 :: H2) =
+      (if eqb_of_compdec H H0 H1 then true else search H0 H2).
+  Hypothesis H5_A : forall (H : CompDec A) (H0 H1 : A) (H2 : list A),
+      search H0 (H1 :: H2) =
+      (if eqb_of_compdec H H0 H1 then true else search H0 H2).
+  Hypothesis H4_bool : forall (H : CompDec bool) (H0 : bool), search H0 nil = false.
+  Hypothesis H4_A : forall (H : CompDec A) (H0 : A), search H0 nil = false.
+
+  Goal search x l2 = search x l2.
+  Proof. verit. Qed.
+
+End CompDecHypotheses.
-- 
cgit