derive.eqb currently broken on int63

LPCIC · Feb 6, 2025 · 100d14e · 100d14e
1 parent 71e4b7d
commit 100d14e
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 7 deletions.
diff --git a/apps/derive/tests/test_eqbOK.v b/apps/derive/tests/test_eqbOK.v
@@ -30,7 +30,7 @@ Fail Elpi derive.eqbOK iota.
 (*
 Elpi derive.eqbOK large.
 *)
-Elpi derive.eqbOK prim_int.
+(* Elpi derive.eqbOK prim_int. *)
 Fail Elpi derive.eqbOK prim_float.
 Elpi derive.eqbOK fo_record.
 Elpi derive.eqbOK pa_record.

diff --git a/apps/derive/tests/test_eqbcorrect.v b/apps/derive/tests/test_eqbcorrect.v
@@ -35,7 +35,7 @@ Fail Elpi derive.eqbcorrect iota.
 (*
 Elpi derive.eqbcorrect large.
 *)
-Elpi derive.eqbcorrect prim_int.
+(* Elpi derive.eqbcorrect prim_int. *)
 Fail Elpi derive.eqbcorrect prim_float. (* Can not work, we don't have a syntaxtic test *)
 Elpi derive.eqbcorrect fo_record.
 Elpi derive.eqbcorrect pa_record.

diff --git a/apps/derive/theories/derive/eqbcorrect.v b/apps/derive/theories/derive/eqbcorrect.v
@@ -35,13 +35,15 @@ Ltac eqb_refl_on__solver :=
   repeat ((apply /andP; split) || reflexivity || assumption).
 End exports.
 
+(*
 Require Import Uint63Axioms.
 
 Lemma uint63_eqb_correct i : eqb_correct_on PrimInt63.eqb i.
 Proof. exact: eqb_correct. Qed.
 
 Lemma uint63_eqb_refl i : eqb_refl_on PrimInt63.eqb i.
 Proof. exact: eqb_refl. Qed.
+*)
 
 Elpi Db derive.eqbcorrect.db lp:{{
 
@@ -50,17 +52,17 @@ Elpi Db derive.eqbcorrect.db lp:{{
     o:constant, % correct
     o:constant. % reflexive
 
-  eqcorrect-for {{:gref PrimInt63.int }} C R :-
-    {{:gref uint63_eqb_correct}} = const C,
-    {{:gref uint63_eqb_refl}} = const R.
+%  eqcorrect-for {{:gref PrimInt63.int }} C R :-
+%    {{:gref uint63_eqb_correct}} = const C,
+%    {{:gref uint63_eqb_refl}} = const R.
 
   :index(2)
   pred correct-lemma-for i:term, o:term.
-  correct-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_correct }}.
+%  correct-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_correct }}.
 
   :index(2)
   pred refl-lemma-for i:term, o:term.
-  refl-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_refl }}.
+%  refl-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_refl }}.
 
 }}.