Merge pull request #784 from LPCIC/fix-780

derive: param1 support for is_true and primitive strings
LPCIC · Feb 26, 2025 · a130e2b · a130e2b
2 parents ab6881e + 5c4b3d0
commit a130e2b
Show file tree

Hide file tree

Showing 38 changed files with 304 additions and 104 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -27,6 +27,10 @@ jobs:
         with:
           opam_file: 'rocq-elpi.opam'
           custom_image: ${{ matrix.image }}
+          after_script: |
+            sudo chmod -R a+w .
+            make all-examples
+            make all-tests
           export: 'OPAMWITHTEST OPAMIGNORECONSTRAINTS OPAMVERBOSE'  # space-separated list of variables
         env:
           OPAMWITHTEST: 'true'

diff --git a/Changelog.md b/Changelog.md
@@ -1,3 +1,10 @@
+# UNRELEASED
+
+### APPS:
+- derive: support for primitive strings in `param1` and `param1_trivial`
+- derive: support for `is_true` in `param1_trivial` (based on pre-existing
+  special support for `is_eq` and `is_bool`)
+
 # [2.5.0] 18/2/2025
 
 Requires Elpi 2.0.7 and Coq 8.20 or Rocq 9.0.

diff --git a/_CoqProject b/_CoqProject
@@ -8,8 +8,8 @@
 
 # Theories
 
--Q theories elpi
--Q _build/default/theories elpi
+-R theories elpi
+-R _build/default/theories elpi
 -Q theories-stdlib elpi_stdlib
 -Q _build/default/theories-stdlib elpi_stdlib
 

diff --git a/apps/cs/tests/setup-project.sh b/apps/cs/tests/setup-project.sh
diff --git a/apps/derive/elpi/eqType.elpi b/apps/derive/elpi/eqType.elpi
@@ -63,7 +63,6 @@ translate-record-constructor (field _ ID _ _) _ (error S) :- S is "unsupported r
 pred self o:eqb.trm.
 
 pred valid i:eqb.trm, o:diagnostic.
-valid (eqb.global X) ok :- global X = {{ PrimInt63.int }}, !.
 valid (eqb.global GR) ok :- eqType GR _, !.
 valid (eqb.app GR A Args) D :- eqType GR EQT, !, valid-eqType EQT [A|Args] D.
 valid T (error S) :- S is "not an eqType: " ^ {std.any->string T}.
@@ -86,7 +85,7 @@ irrelevant? (app [{{ @eq }}, global EqType, A, B]) (eqb.app EQ EQTYPE [A1,B1]) D
   term->trm A A1,
   term->trm B B1,
 ].
-irrelevant? T R D :- whd1 T T1, coq.say "whd" T T1, irrelevant? T1 R D.
+irrelevant? T R D :- whd1 T T1, irrelevant? T1 R D.
 
 pred term->trm i:term, o:eqb.trm, o:diagnostic.
 term->trm (global GR) (eqb.global GR) ok :- !.

diff --git a/apps/derive/tests/test_bcongr.v b/apps/derive/tests/test_bcongr.v
@@ -29,6 +29,7 @@ Elpi derive.bcongr large.
 *)
 Elpi derive.bcongr prim_int.
 Elpi derive.bcongr prim_float.
+Elpi derive.bcongr prim_string.
 Elpi derive.bcongr fo_record.
 Elpi derive.bcongr pa_record.
 Elpi derive.bcongr pr_record.

diff --git a/apps/derive/tests/test_derive_corelib.v b/apps/derive/tests/test_derive_corelib.v
@@ -1,6 +1,6 @@
 (* Some standard data types using different features *)
-From elpi.core Require PrimInt63.
-From elpi.core Require PrimFloat.
+From elpi Require elpi.
+From elpi.core Require PrimInt63 PrimFloat PrimString.
 
 Module Coverage.
 
@@ -70,6 +70,7 @@ Inductive large :=
 
 Inductive prim_int := PI (i : PrimInt63.int).
 Inductive prim_float := PF (f : PrimFloat.float).
+Inductive prim_string := PS (s : lib:elpi.pstring).
 
 Record fo_record := { f1 : peano; f2 : unit; }.
 
@@ -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_eq.v b/apps/derive/tests/test_eq.v
@@ -23,6 +23,7 @@ Fail Elpi derive.eq iota.
 Elpi derive.eq large.
 Elpi derive.eq prim_int.
 Elpi derive.eq prim_float.
+Elpi derive.eq prim_string.
 Elpi derive.eq fo_record.
 Elpi derive.eq pa_record.
 Elpi derive.eq pr_record.

diff --git a/apps/derive/tests/test_eqK.v b/apps/derive/tests/test_eqK.v
@@ -37,6 +37,7 @@ Elpi derive.eqK large.
 *)
 Elpi derive.eqK prim_int.
 Elpi derive.eqK prim_float.
+Elpi derive.eqK prim_string.
 Elpi derive.eqK fo_record.
 Elpi derive.eqK pa_record.
 Elpi derive.eqK pr_record.

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.
 
@@ -31,6 +31,7 @@ Elpi derive.eqOK large.
 *)
 Elpi derive.eqOK prim_int.
 Fail Elpi derive.eqOK prim_float.
+Elpi derive.eqOK prim_string.
 Elpi derive.eqOK fo_record.
 Elpi derive.eqOK pa_record.
 Elpi derive.eqOK pr_record.

diff --git a/apps/derive/tests/test_eqType_ast.v b/apps/derive/tests/test_eqType_ast.v
@@ -24,6 +24,7 @@ Fail Elpi derive.eqType.ast iota.
 Elpi derive.eqType.ast large.
 Elpi derive.eqType.ast prim_int.
 Fail Elpi derive.eqType.ast prim_float.
+Elpi derive.eqType.ast prim_string.
 Elpi derive.eqType.ast fo_record.
 Elpi derive.eqType.ast pa_record.
 Elpi derive.eqType.ast pr_record.
@@ -32,6 +33,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
@@ -26,6 +26,7 @@ Elpi derive.eqb large.
 *)
 Elpi derive.eqb prim_int.
 Fail Elpi derive.eqb prim_float.
+Elpi derive.eqb prim_string.
 Elpi derive.eqb fo_record.
 Elpi derive.eqb pa_record.
 Elpi derive.eqb pr_record.
@@ -34,6 +35,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
@@ -32,6 +32,7 @@ Elpi derive.eqbOK large.
 *)
 Elpi derive.eqbOK prim_int.
 Fail Elpi derive.eqbOK prim_float.
+Elpi derive.eqbOK prim_string.
 Elpi derive.eqbOK fo_record.
 Elpi derive.eqbOK pa_record.
 Elpi derive.eqbOK pr_record.
@@ -40,6 +41,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
@@ -37,6 +37,7 @@ Elpi derive.eqbcorrect large.
 *)
 Elpi derive.eqbcorrect prim_int.
 Fail Elpi derive.eqbcorrect prim_float. (* Can not work, we don't have a syntaxtic test *)
+Elpi derive.eqbcorrect prim_string.
 Elpi derive.eqbcorrect fo_record.
 Elpi derive.eqbcorrect pa_record.
 Elpi derive.eqbcorrect pr_record.   
@@ -45,6 +46,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_eqcorrect.v b/apps/derive/tests/test_eqcorrect.v
@@ -32,6 +32,7 @@ Elpi derive.eqcorrect large.
 *)
 Elpi derive.eqcorrect prim_int.
 Fail Elpi derive.eqcorrect prim_float.
+Elpi derive.eqcorrect prim_string.
 Elpi derive.eqcorrect fo_record.
 Elpi derive.eqcorrect pa_record.
 Elpi derive.eqcorrect pr_record.

diff --git a/apps/derive/tests/test_fields.v b/apps/derive/tests/test_fields.v
@@ -24,6 +24,7 @@ Fail Elpi derive.fields iota.
 Elpi derive.fields large.
 Elpi derive.fields prim_int.
 Fail Elpi derive.fields prim_float.
+Elpi derive.fields prim_string.
 Elpi derive.fields fo_record.
 Elpi derive.fields pa_record.
 Elpi derive.fields pr_record.
@@ -32,6 +33,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
@@ -28,14 +28,15 @@ Elpi derive.induction iota.
 Elpi derive.induction large.
 Elpi derive.induction prim_int.
 Elpi derive.induction prim_float.
+Elpi derive.induction prim_string.
 Elpi derive.induction fo_record.
 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 +67,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_isK.v b/apps/derive/tests/test_isK.v
@@ -24,6 +24,7 @@ Elpi derive.isK iota.
 Elpi derive.isK large.
 Elpi derive.isK prim_int.
 Elpi derive.isK prim_float.
+Elpi derive.isK prim_string.
 Elpi derive.isK fo_record.
 Elpi derive.isK pa_record.
 Elpi derive.isK pr_record.

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
@@ -25,17 +25,19 @@ Elpi derive.param1 iota.
 Elpi derive.param1 large.
 Elpi derive.param1 prim_int.
 Elpi derive.param1 prim_float.
+Elpi derive.param1 prim_string.
 Elpi derive.param1 fo_record.
 Elpi derive.param1 pa_record.
 Elpi derive.param1 pr_record.
 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 +103,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
@@ -29,6 +29,7 @@ Elpi derive.param1.congr is_large. (* slow *)
 *)
 Elpi derive.param1.congr is_prim_int.
 Elpi derive.param1.congr is_prim_float.
+Elpi derive.param1.congr is_prim_string.
 Elpi derive.param1.congr is_fo_record.
 Elpi derive.param1.congr is_pa_record.
 Elpi derive.param1.congr is_pr_record.
@@ -37,6 +38,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.
@@ -26,14 +26,16 @@ Elpi derive.param1.functor is_iota.
 Elpi derive.param1.functor is_large.
 Elpi derive.param1.functor is_prim_int.
 Elpi derive.param1.functor is_prim_float.
+Elpi derive.param1.functor is_prim_string.
 Elpi derive.param1.functor is_fo_record.
 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
@@ -28,6 +28,7 @@ Fail Elpi derive.param1.trivial is_iota.
 Elpi derive.param1.trivial is_large.
 Elpi derive.param1.trivial is_prim_int.
 Elpi derive.param1.trivial is_prim_float.
+Elpi derive.param1.trivial is_prim_string.
 Elpi derive.param1.trivial is_fo_record.
 Elpi derive.param1.trivial is_pa_record.
 Elpi derive.param1.trivial is_pr_record.
@@ -38,6 +39,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.

diff --git a/apps/derive/tests/test_projK.v b/apps/derive/tests/test_projK.v
@@ -24,6 +24,7 @@ Elpi derive.projK iota.
 Elpi derive.projK large.
 Elpi derive.projK prim_int.
 Elpi derive.projK prim_float.
+Elpi derive.projK prim_string.
 Elpi derive.projK fo_record.
 Elpi derive.projK pa_record.
 Elpi derive.projK pr_record.

diff --git a/apps/derive/tests/test_tag.v b/apps/derive/tests/test_tag.v
@@ -25,6 +25,7 @@ Elpi derive.tag iota.
 Elpi derive.tag large.
 Elpi derive.tag prim_int.
 Elpi derive.tag prim_float.
+Elpi derive.tag prim_string.
 Elpi derive.tag fo_record.
 Elpi derive.tag pa_record.
 Elpi derive.tag pr_record.
@@ -33,6 +34,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.

diff --git a/apps/derive/theories/derive/eq.v b/apps/derive/theories/derive/eq.v
@@ -9,7 +9,7 @@ From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
 
-From elpi.core Require Import PrimInt63 PrimFloat.
+From elpi.core Require Import PrimInt63 PrimFloat PrimString.
 
 Register Coq.Numbers.Cyclic.Int63.PrimInt63.eqb as elpi.derive.eq_unit63.
 Register Coq.Floats.PrimFloat.eqb as elpi.derive.eq_float64.
@@ -20,6 +20,7 @@ Elpi Db derive.eq.db lp:{{
 type eq-db term -> term -> term -> prop.
 eq-db {{ lib:num.int63.type }} {{ lib:num.int63.type }} {{ lib:elpi.derive.eq_unit63 }} :- !.
 eq-db {{ lib:num.float.type }} {{ lib:num.float.type }} {{ lib:elpi.derive.eq_float64 }} :- !.
+eq-db {{ lib:elpi.pstring }} {{ lib:elpi.pstring }} {{ lib:elpi.pstring_eqb }} :- !.
 
 % quick access
 type eq-for inductive -> constant -> prop.