cleanup primitive strings

LPCIC · Feb 26, 2025 · 753638b · 753638b
1 parent 0667db3
commit 753638b
Show file tree

Hide file tree

Showing 23 changed files with 82 additions and 20 deletions.
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/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}.

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,7 +1,6 @@
 (* Some standard data types using different features *)
 From elpi Require elpi.
-From elpi.core Require PrimInt63.
-From elpi.core Require PrimFloat.
+From elpi.core Require PrimInt63 PrimFloat PrimString.
 
 Module Coverage.
 

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_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_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_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.

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.

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.

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.

diff --git a/apps/derive/theories/derive/eqType_ast.v b/apps/derive/theories/derive/eqType_ast.v
@@ -1,5 +1,5 @@
 From elpi Require Import elpi.
-From elpi.core Require Import PrimInt63 PrimFloat.
+From elpi.core Require Import PrimInt63 PrimFloat PrimString.
 From elpi.apps Require Import derive.
 
 From elpi.apps.derive.elpi Extra Dependency "eqType.elpi" as eqType.
@@ -29,6 +29,8 @@ type eqb.axiom       eqb.eqType.
 type eqb.constructor constructor -> eqb.arguments -> eqb.constructor.
 
 pred eqType i:gref, o:eqb.eqType.
+eqType {{:gref PrimInt63.int }} eqb.axiom :- !.
+eqType {{:gref lib:elpi.pstring }} eqb.axiom :- !.
 
 }}.
 

diff --git a/apps/derive/theories/derive/eqb.v b/apps/derive/theories/derive/eqb.v
@@ -31,6 +31,7 @@ Elpi Db derive.eqb.db lp:{{
 
   eqb-for {{ PrimFloat.float }} {{ PrimFloat.float }} {{ PrimFloat.eqb }}.
   eqb-for {{ PrimInt63.int }} {{ PrimInt63.int }} {{ PrimInt63.eqb }}.
+  eqb-for {{ lib:elpi.pstring }} {{ lib:elpi.pstring }} {{ lib:elpi.pstring_eqb }}.
 
   :name "eqb-for:whd"
   eqb-for T1 T2 X :- whd1 T1 T1', !, eqb-for T1' T2 X. 

diff --git a/apps/derive/theories/derive/eqbcorrect.v b/apps/derive/theories/derive/eqbcorrect.v
@@ -43,6 +43,19 @@ Proof. exact: Uint63Axioms.eqb_correct. Qed.
 Lemma uint63_eqb_refl i : eqb_refl_on PrimInt63.eqb i.
 Proof. exact: Uint63Axioms.eqb_refl. Qed.
 
+From elpi.core Require PrimString PrimStringAxioms.
+
+Lemma pstring_eqb_correct i : eqb_correct_on PrimString.eqb i.
+Proof.
+   move=> j; rewrite /PrimString.eqb; have [] := PrimStringAxioms.compare_ok i j.
+   by case: PrimString.compare => // /(_ erefl).
+Qed.
+
+Lemma pstring_eqb_refl i : eqb_refl_on PrimString.eqb i.
+Proof.
+   rewrite /PrimString.eqb /eqb_refl_on; have [] := PrimStringAxioms.compare_ok i i.
+   by case: PrimString.compare => // _ /(_ erefl).
+Qed.
 
 Elpi Db derive.eqbcorrect.db lp:{{
 
@@ -58,10 +71,12 @@ Elpi Db derive.eqbcorrect.db lp:{{
   :index(2)
   pred correct-lemma-for i:term, o:term.
   correct-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_correct }}.
+  correct-lemma-for {{ PrimString.string }} {{ @pstring_eqb_correct }}.
 
   :index(2)
   pred refl-lemma-for i:term, o:term.
   refl-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_refl }}.
+  refl-lemma-for {{ PrimString.string }} {{ @pstring_eqb_refl }}.
 
 }}.
 

diff --git a/apps/derive/theories/derive/eqcorrect.v b/apps/derive/theories/derive/eqcorrect.v
@@ -11,25 +11,39 @@ From elpi Require Import elpi.
 From elpi.apps Require Import derive.
 From elpi.apps Require Import  derive.eq derive.induction derive.eqK derive.param1.
 
-From elpi.core Require Import ssreflect PrimInt63.
-From elpi.core Require Uint63Axioms.
+From elpi.core Require Import ssreflect.
+
+From elpi.core Require PrimInt63 Uint63Axioms.
 
 Lemma uint63_eq_correct i : is_uint63 i -> eq_axiom_at PrimInt63.int PrimInt63.eqb i.
 Proof.
-move=> _ j; have [] : (eqb i j) = true <-> i = j.
+move=> _ j; have [] : (PrimInt63.eqb i j) = true <-> i = j.
   split; first exact: Uint63Axioms.eqb_correct.
   by move=> ->; rewrite Uint63Axioms.eqb_refl.
 by case: PrimInt63.eqb => [-> // _| _ abs]; constructor=> // /abs.
 Qed.
 Register uint63_eq_correct as elpi.derive.uint63_eq_correct.
 
+From elpi.core Require PrimString PrimStringAxioms.
+
+Lemma pstring_eq_correct i : is_pstring i -> eq_axiom_at PrimString.string PrimString.eqb i.
+Proof.
+  move=> _ j; have [] : (PrimString.eqb i j) = true <-> i = j.
+  rewrite /PrimString.eqb; have := PrimStringAxioms.compare_ok i j.
+   case: PrimString.compare => - [c r] //; split => //; [move=> _| by move=>/r ..].
+   by apply: c.
+by case: PrimString.eqb => [-> // _| _ abs]; constructor=> // /abs.
+Qed.
+Register pstring_eq_correct as elpi.derive.pstring_eq_correct.
+
 Elpi Db derive.eqcorrect.db lp:{{
   type eqcorrect-db gref -> term -> prop.
 }}.
 #[superglobal] Elpi Accumulate derive.eqcorrect.db File derive.lib.
 #[superglobal] Elpi Accumulate derive.eqcorrect.db lp:{{
 
-eqcorrect-db X {{ lib:elpi.derive.uint63_eq_correct }} :- {{ lib:num.int63.type }} = global X, !.
+eqcorrect-db {{:gref lib:num.int63.type }} {{ lib:elpi.derive.uint63_eq_correct }} :- !.
+eqcorrect-db {{:gref lib:elpi.pstring }} {{ lib:elpi.derive.pstring_eq_correct }} :- !.
 eqcorrect-db X _ :- {{ lib:num.float.type }} = global X, !, stop "float64 comparison is not syntactic".
 
 :name "eqcorrect-db:fail"

diff --git a/apps/derive/theories/derive/param1.v b/apps/derive/theories/derive/param1.v
@@ -41,15 +41,15 @@ Class reali {X : Type} {XR : X -> Type} (x : X) (xR : XR x) := Reali {}.
 
 Register store_reali as param1.store_reali.
 
-From elpi.core Require Import PrimInt63 PrimFloat.
+From elpi.core Require Import PrimInt63 PrimFloat PrimString.
 
 Inductive is_uint63 : PrimInt63.int -> Type := uint63 (i : PrimInt63.int) : is_uint63 i.
 Register is_uint63 as elpi.derive.is_uint63.
 
 Inductive is_float64 : PrimFloat.float -> Type := float64 (f : PrimFloat.float ) : is_float64 f.
 Register is_float64 as elpi.derive.is_float64.
 
-Inductive is_pstring : lib:elpi.pstring -> Type := pstring (s : lib:elpi.pstring) : is_pstring s.
+Inductive is_pstring : PrimString.string -> Type := pstring (s : PrimString.string) : is_pstring s.
 Register is_pstring as elpi.derive.is_pstring.
 
 (* Links a term (constant, inductive type, inductive constructor) with

diff --git a/tests/test_elaborator.v b/tests/test_elaborator.v
@@ -1,4 +1,4 @@
-From elpi.core Require Import PrimFloat.
+From elpi.core Require Import PrimInt63 PrimFloat PrimString.
 
 From elpi_elpi Extra Dependency "elpi_elaborator.elpi" as elab.
 

diff --git a/theories/core/PrimString.v.in b/theories/core/PrimString.v.in
@@ -0,0 +1,9 @@
+#[only="8.20"] From Coq Require PrimString.
+#[skip="8.20"] From Corelib Require PrimString.
+
+Register PrimString.string as elpi.pstring.
+
+Definition eqb (s1 s2 : PrimString.string) :=
+  match PrimString.compare s1 s2 with Eq => true | _ => false end.
+
+Register eqb as elpi.pstring_eqb.
diff --git a/theories/core/PrimStringAxioms.v.in b/theories/core/PrimStringAxioms.v.in
@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq Require Export PrimStringAxioms PString.
+#[skip="8.20"] From Corelib Require Export PrimStringAxioms PString.
+Definition compare_ok := compare_eq.
diff --git a/theories/core/dune b/theories/core/dune
@@ -49,6 +49,14 @@
   (with-stdout-to %{target}
    (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
 
+(rule
+ (target PrimString.v)
+ (deps
+  (glob_files PrimString.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
 (rule
  (target RelationClasses.v)
  (deps
@@ -73,6 +81,14 @@
   (with-stdout-to %{target}
    (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
 
+(rule
+ (target PrimStringAxioms.v)
+ (deps
+  (glob_files PrimStringAxioms.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
 (rule
  (target ssreflect.v)
  (deps

diff --git a/theories/elpi.v.in b/theories/elpi.v.in
@@ -51,9 +51,3 @@ Register Coq.Init.Datatypes.false as elpi.false.
 #[skip="8.20"] Register Corelib.Init.Datatypes.ReflectF as elpi.ReflectF.
 #[skip="8.20"] Register Corelib.Init.Datatypes.ReflectT as elpi.ReflectT.
 #[skip="8.20"] Register Corelib.Init.Datatypes.is_true as elpi.is_true.
-
-#[only="8.20"] From Coq Require PrimString.
-#[skip="8.20"] From Corelib Require PrimString.
-
-#[only="8.20"] Register Coq.Strings.PrimString.string as elpi.pstring.
-#[skip="8.20"] Register Corelib.Strings.PrimString.string as elpi.pstring.