Reify polymorphic terms

A polymorphic term is now reified as a whole of the term applied to one or many types. The same polymorphic term applied to different types is reified as different monomorphic terms.

3 files changed, 117 insertions, 9 deletions

diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index 55e689d..4ab111c 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -580,12 +580,95 @@ Section Int63.
 End Int63.
 
 
-Hint Resolve unit_ord bool_ord Z_ord Positive_ord BV_ord FArray_ord : typeclass_instances.
-Hint Resolve unit_eqbtype bool_eqbtype Z_eqbtype Positive_eqbtype BV_eqbtype FArray_eqbtype : typeclass_instances.
-Hint Resolve bool_dec Z_dec Positive_dec BV_dec FArray_dec : typeclass_instances.
-Hint Resolve unit_comp bool_comp Z_comp Positive_comp BV_comp FArray_comp : typeclass_instances.
-Hint Resolve unit_inh bool_inh Z_inh Positive_inh BV_inh FArray_inh : typeclass_instances.
-Hint Resolve unit_compdec bool_compdec Z_compdec Positive_compdec BV_compdec FArray_compdec : typeclass_instances.
-
-Hint Resolve int63_ord int63_inh int63_eqbtype int63_dec int63_comp int63_compdec
-  : typeclass_instances.
+Section option.
+
+  Generalizable Variable A.
+  Context `{HA : CompDec A}.
+
+
+  Definition option_eqb (x y : option A) : bool :=
+    match x, y with
+    | Some a, Some b => eqb a b
+    | None, None => true
+    | _, _ => false
+    end.
+
+
+  Lemma option_eqb_spec : forall (x y : option A), option_eqb x y = true <-> x = y.
+  Proof.
+    intros [a| ] [b| ]; simpl; split; try discriminate; auto.
+    - intro H. rewrite eqb_spec in H. now subst b.
+    - intros H. inversion H as [H1]. now rewrite eqb_spec.
+  Qed.
+
+
+  Instance option_eqbtype : EqbType (option A) := Build_EqbType _ _ option_eqb_spec.
+
+
+  Definition option_lt (x y : option A) : Prop :=
+    match x, y with
+    | Some a, Some b => lt a b
+    | Some _, None => True
+    | None, Some _ => False
+    | None, None => False
+    end.
+
+
+  Lemma option_lt_trans : forall (x y z : option A),
+      option_lt x y -> option_lt y z -> option_lt x z.
+  Proof.
+    intros [a| ] [b| ] [c| ]; simpl; auto.
+    - apply lt_trans.
+    - intros _ [].
+  Qed.
+
+
+  Lemma option_lt_not_eq : forall (x y : option A), option_lt x y -> x <> y.
+  Proof.
+    intros [a| ] [b| ]; simpl; auto.
+    - intros H1 H2. inversion H2 as [H3]. revert H3. now apply lt_not_eq.
+    - discriminate.
+  Qed.
+
+
+  Instance option_ord : OrdType (option A) :=
+    Build_OrdType _ _ option_lt_trans option_lt_not_eq.
+
+
+  Definition option_compare : forall (x y : option A), Compare option_lt Logic.eq x y.
+  Proof.
+    intros [a| ] [b| ]; simpl.
+    - case_eq (compare a b); intros l H.
+      + now apply LT.
+      + apply EQ. now subst b.
+      + now apply GT.
+    - now apply LT.
+    - now apply GT.
+    - now apply EQ.
+  Defined.
+
+
+  Instance option_comp : Comparable (option A) := Build_Comparable _ _ option_compare.
+
+
+  Instance option_inh : Inhabited (option A) := Build_Inhabited _ None.
+
+
+  Instance option_compdec : CompDec (option A) := {|
+    Eqb := option_eqbtype;
+    Ordered := option_ord;
+    Comp := option_comp;
+    Inh := option_inh
+  |}.
+
+End option.
+
+
+Hint Resolve unit_ord unit_eqbtype unit_comp unit_inh unit_compdec : typeclass_instances.
+Hint Resolve bool_ord bool_eqbtype bool_dec bool_comp bool_inh bool_compdec : typeclass_instances.
+Hint Resolve Z_ord Z_eqbtype Z_dec Z_comp Z_inh Z_compdec : typeclass_instances.
+Hint Resolve Positive_ord Positive_eqbtype Positive_dec Positive_comp Positive_inh Positive_compdec : typeclass_instances.
+Hint Resolve BV_ord BV_eqbtype BV_dec BV_comp BV_inh BV_compdec : typeclass_instances.
+Hint Resolve FArray_ord FArray_eqbtype FArray_dec FArray_comp FArray_inh FArray_compdec : typeclass_instances.
+Hint Resolve int63_ord int63_inh int63_eqbtype int63_dec int63_comp int63_compdec option_compdec : typeclass_instances.
+Hint Resolve option_ord option_eqbtype option_comp option_inh : typeclass_instances.
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index ae44b8d..121e705 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -1262,6 +1262,21 @@ module Atom =
         | _ -> assert false
 
       and mk_unknown c args ty =
+        let rec collect_types = function
+          | [] -> ([],[])
+          | x::xs as l ->
+             if Constr.iskind (Structures.retyping_get_type_of env sigma x) then
+               let (l1, l2) = collect_types xs in
+               (x::l1, l2)
+             else
+               ([], l)
+        in
+        let (args1, args2) = collect_types args in
+        let c, args =
+          match args1 with
+            | [] -> c, args
+            | _ -> Constr.mkApp (c, Array.of_list args1), args2
+        in
         let hargs = Array.of_list (List.map mk_hatom args) in
         let op =
           try Op.of_coq ro c
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 896c1bf..da7cb5a 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -994,3 +994,13 @@ Proof using.
   intros.
   verit.
 Qed.
+
+
+Section Polymorphism.
+  Goal forall (f : option Z -> Z) (a b : Z),
+      implb (Z.eqb a b) (Z.eqb (f (Some a)) (f (Some b))).
+  Proof. verit. auto with typeclass_instances. Qed.
+
+  Goal forall (f : option Z -> Z) (a b : Z), a = b -> f (Some a) = f (Some b).
+  Proof. verit. auto with typeclass_instances. Qed.
+End Polymorphism.