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

(limited to 'src')

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