tests

LPCIC · Feb 26, 2025 · de29538 · de29538
1 parent 57b2cb7
commit de29538
Show file tree

Hide file tree

Showing 15 changed files with 23 additions and 15 deletions.
diff --git a/apps/derive/tests/test_derive_corelib.v b/apps/derive/tests/test_derive_corelib.v
@@ -1,4 +1,5 @@
 (* Some standard data types using different features *)
+From elpi Require elpi.
 From elpi.core Require PrimInt63.
 From elpi.core Require PrimFloat.
 
@@ -91,6 +92,8 @@ Definition is_zero (n:peano) : bool :=
 
 Record sigma_bool := { depn : peano; depeq : is_zero depn = true }.
 
+Record sigma_bool2 := { depn2 : peano; depeq2 : lib:elpi.is_true (is_zero depn2) }.
+
 Fixpoint is_leq (n m:peano) : bool := 
   match n, m with 
   | Zero, _ => true 

diff --git a/apps/derive/tests/test_eqOK.v b/apps/derive/tests/test_eqOK.v
@@ -1,4 +1,4 @@
-From elpi.apps Require Import derive.eqOK.
+From elpi.apps Require Import derive.param1 derive.eqOK.
 
 From elpi.apps Require Import test_derive_corelib test_eqcorrect test_param1 test_param1_trivial.
 

diff --git a/apps/derive/tests/test_eqType_ast.v b/apps/derive/tests/test_eqType_ast.v
@@ -32,6 +32,7 @@ Elpi derive.eqType.ast enum.
 Elpi derive.eqType.ast bool.
 Fail Elpi derive.eqType.ast eq.
 Elpi derive.eqType.ast sigma_bool.
+Elpi derive.eqType.ast sigma_bool2.
 Elpi derive.eqType.ast ord.
 Elpi derive.eqType.ast ord2.
 Elpi derive.eqType.ast val.

diff --git a/apps/derive/tests/test_eqb.v b/apps/derive/tests/test_eqb.v
@@ -34,6 +34,7 @@ Elpi derive.eqb enum.
 Fail Elpi derive.eqb eq.
 Elpi derive.eqb bool.
 Elpi derive.eqb sigma_bool.
+Elpi derive.eqb sigma_bool2.
 Elpi derive.eqb ord.
 Elpi derive.eqb ord2.
 Elpi derive.eqb val.

diff --git a/apps/derive/tests/test_eqbOK.v b/apps/derive/tests/test_eqbOK.v
@@ -40,6 +40,7 @@ Elpi derive.eqbOK enum.
 Fail Elpi derive.eqbOK eq.
 Elpi derive.eqbOK bool.
 Elpi derive.eqbOK sigma_bool.
+Elpi derive.eqbOK sigma_bool2.
 Elpi derive.eqbOK ord.
 Elpi derive.eqbOK ord2.
 Elpi derive.eqbOK val.

diff --git a/apps/derive/tests/test_eqbcorrect.v b/apps/derive/tests/test_eqbcorrect.v
@@ -45,6 +45,7 @@ Elpi derive.eqbcorrect enum.
 Fail Elpi derive.eqbcorrect eq.
 Elpi derive.eqbcorrect bool.
 Elpi derive.eqbcorrect sigma_bool.
+Elpi derive.eqbcorrect sigma_bool2.
 Elpi derive.eqbcorrect ord.
 Elpi derive.eqbcorrect ord2.
 Elpi derive.eqbcorrect val.

diff --git a/apps/derive/tests/test_fields.v b/apps/derive/tests/test_fields.v
@@ -32,6 +32,7 @@ Elpi derive.fields enum.
 Elpi derive.fields bool.
 Fail Elpi derive.fields eq.
 Elpi derive.fields sigma_bool.
+Elpi derive.fields sigma_bool2.
 Elpi derive.fields ord.
 Elpi derive.fields ord2.
 Elpi derive.fields val.

diff --git a/apps/derive/tests/test_induction.v b/apps/derive/tests/test_induction.v
@@ -33,9 +33,9 @@ Elpi derive.induction pa_record.
 Elpi derive.induction pr_record.
 Elpi derive.induction dep_record.
 Elpi derive.induction enum.
-Elpi derive.induction eq.
-Elpi derive.induction bool.
 Elpi derive.induction sigma_bool.
+Elpi derive.induction bool.
+Elpi derive.induction sigma_bool2.
 Elpi derive.induction ord.
 Elpi derive.induction ord2.
 Elpi derive.induction val.
@@ -66,5 +66,6 @@ Redirect "tmp" Check pr_record_induction : forall A pr P, (forall x, is_peano x
 Redirect "tmp" Check dep_record_induction : forall P, (forall x (px : is_peano x) y, is_vect unit is_unit x px y -> P (Build_dep_record x y)) -> forall x, is_dep_record x -> P x.
 Redirect "tmp" Check enum_induction : forall P, (P E1) -> (P E2) -> (P E3) -> forall x, is_enum x -> P x.
 Redirect "tmp" Check sigma_bool_induction.
+Redirect "tmp" Check sigma_bool2_induction.
 Redirect "tmp" Check ord_induction : forall p Pp P, (forall n Pn l, is_eq bool is_bool (is_leq n p) (is_is_leq n Pn p Pp) true is_true l -> P (mkOrd p n l)) -> forall (o : ord p), is_ord p Pp o -> P o.
 Redirect "tmp" Check ord2_induction : forall p Pp P, (forall (o1 : ord p), is_ord p Pp o1 -> forall (o2 : ord p), is_ord p Pp o2 -> P (mkOrd2 p o1 o2)) -> forall (o : ord2 p), is_ord2 p Pp o -> P o.
diff --git a/apps/derive/tests/test_lens.v b/apps/derive/tests/test_lens.v
@@ -24,7 +24,7 @@ intros; unfold _pf3.
 match goal with
 | |- x = {| over := fun f r => {| pf3 := f (_ r); pf4 := _ r |} ;
             view := _ |}
-    => idtac "ok"
+    => idtac
 | |- _ => fail "not primitive"
 end.
 Abort.

diff --git a/apps/derive/tests/test_map.v b/apps/derive/tests/test_map.v
@@ -33,6 +33,7 @@ Elpi derive.map enum.
 Fail Elpi derive.map eq.
 Elpi derive.map bool.
 Elpi derive.map sigma_bool.
+Elpi derive.map sigma_bool2.
 Fail Elpi derive.map ord.
 Elpi derive.map val.
 End Coverage.

diff --git a/apps/derive/tests/test_param1.v b/apps/derive/tests/test_param1.v
@@ -32,10 +32,11 @@ Elpi derive.param1 dep_record.
 Elpi derive.param1 enum.
 (*
 Elpi derive.param1 eq. (* done in param1.v *)
+Elpi derive.param1 bool. (* done in param1.v *)
 *)
-Elpi derive.param1 bool.
 Elpi derive.param1 is_zero.
 Elpi derive.param1 sigma_bool.
+Elpi derive.param1 sigma_bool2.
 Elpi derive.param1 is_leq.
 Elpi derive.param1 ord.
 Elpi derive.param1 ord2.
@@ -101,15 +102,13 @@ Fixpoint vec_length (A : Type) n (v : vec A n) :=
 Elpi derive.param1 vec_length.
 Elpi derive.param1 list.
 Elpi derive.param1 is_list.
-Elpi derive.param1 eq.
 
 Fixpoint plus' m n := match n with 0 => m | S n => S (plus' m n) end.
 Elpi derive.param1 plus'.
 Elpi derive.param1 plus.
 Elpi derive.param1 prod.
 Elpi derive.param1 fst.
 Elpi derive.param1 snd.
-Elpi derive.param1 bool.
 Elpi derive.param1 Nat.divmod.
 Elpi derive.param1 Nat.div.
 

diff --git a/apps/derive/tests/test_param1_congr.v b/apps/derive/tests/test_param1_congr.v
@@ -37,6 +37,7 @@ Elpi derive.param1.congr is_enum.
 Elpi derive.param1.congr is_bool.
 Elpi derive.param1.congr is_eq.
 Elpi derive.param1.congr is_sigma_bool.
+Elpi derive.param1.congr is_sigma_bool2.
 Elpi derive.param1.congr is_ord.
 Elpi derive.param1.congr is_val.
 End Coverage.

diff --git a/apps/derive/tests/test_param1_functor.v b/apps/derive/tests/test_param1_functor.v
@@ -1,4 +1,4 @@
-From elpi.apps Require Import derive.param1_functor.
+From elpi.apps Require Import derive.param1 derive.param1_functor.
 
 From elpi.apps.derive.tests Require Import test_derive_corelib test_param1.
 Import test_derive_corelib.Coverage.
@@ -31,9 +31,10 @@ Elpi derive.param1.functor is_pa_record.
 Elpi derive.param1.functor is_pr_record.
 Elpi derive.param1.functor is_dep_record.
 Elpi derive.param1.functor is_enum.
-Fail Elpi derive.param1.functor param1.is_eq.
-Elpi derive.param1.functor is_bool.
+Fail Elpi derive.param1.functor derive.param1.exports.is_eq.
+Elpi derive.param1.functor derive.param1.exports.is_bool.
 Elpi derive.param1.functor is_sigma_bool.
+Elpi derive.param1.functor is_sigma_bool2.
 Elpi derive.param1.functor is_ord.
 Elpi derive.param1.functor is_ord2.
 Elpi derive.param1.functor is_val.

diff --git a/apps/derive/tests/test_param1_trivial.v b/apps/derive/tests/test_param1_trivial.v
@@ -38,6 +38,7 @@ Elpi derive.param1.trivial is_bool.
 Elpi derive.param1.trivial is_eq. (* ad-hoc *)
 *)
 Elpi derive.param1.trivial is_sigma_bool.
+Elpi derive.param1.trivial is_sigma_bool2.
 Elpi derive.param1.trivial is_ord.
 Elpi derive.param1.trivial is_ord2.
 Elpi derive.param1.trivial is_val.
@@ -104,8 +105,3 @@ Redirect "tmp" Check is_sigma_bool_inhab : full sigma_bool is_sigma_bool.
 Redirect "tmp" Check is_ord_inhab : forall p px, full (ord p) (is_ord p px).
 Redirect "tmp" Check is_ord2_inhab : forall p px, full (ord2 p) (is_ord2 p px).
 Redirect "tmp" Check is_val_inhab : full val is_val.
-
-Redirect "tmp" Record sigma_bool2 := { depn : peano; depeq : lib:elpi.is_true (is_zero depn) }.
-Redirect "tmp" Elpi derive.param1 sigma_bool2.
-Redirect "tmp" Elpi derive.param1.trivial is_sigma_bool2.
-Redirect "tmp" Check is_sigma_bool2_inhab.
diff --git a/apps/derive/tests/test_tag.v b/apps/derive/tests/test_tag.v
@@ -33,6 +33,7 @@ Elpi derive.tag enum.
 Elpi derive.tag eq.
 Elpi derive.tag bool.
 Elpi derive.tag sigma_bool.
+Elpi derive.tag sigma_bool2.
 Elpi derive.tag ord.
 Elpi derive.tag ord2.
 Elpi derive.tag val.