Don't Require PrimInt63 and PrimFloat by default

Author: proux01

apps/derive/theories/derive/eq.v

@@ -9,15 +9,17 @@ From Coq Require Import Bool.
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
 
+From Coq Require Import PrimInt63 PrimFloat.
+
 Register Coq.Numbers.Cyclic.Int63.PrimInt63.eqb as elpi.derive.eq_unit63.
 Register Coq.Floats.PrimFloat.eqb as elpi.derive.eq_float64.
 
 Elpi Db derive.eq.db lp:{{
 
 % full resolution (composes with eq functions for parameters)
 type eq-db term -> term -> term -> prop.
-eq-db {{ lib:elpi.uint63 }} {{ lib:elpi.uint63 }} {{ lib:elpi.derive.eq_unit63 }} :- !.
-eq-db {{ lib:elpi.float64 }} {{ lib:elpi.float64 }} {{ lib:elpi.derive.eq_float64 }} :- !.
+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 }} :- !.
 
 :name "eq-db:fail"
 eq-db A B F :-

apps/derive/theories/derive/eqType_ast.v

@@ -1,4 +1,5 @@
 From elpi Require Import elpi.
+From Coq Require Import PrimInt63 PrimFloat.
 From elpi.apps Require Import derive.
 
 From elpi.apps.derive Extra Dependency "eqType.elpi" as eqType.

apps/derive/theories/derive/eqcorrect.v

@@ -22,8 +22,8 @@ Register uint63_eq_correct as elpi.derive.uint63_eq_correct.
 Elpi Db derive.eqcorrect.db lp:{{
   type eqcorrect-db gref -> term -> prop.
 
-eqcorrect-db X {{ lib:elpi.derive.uint63_eq_correct }} :- {{ lib:elpi.uint63 }} = global X, !.
-eqcorrect-db X _ :- {{ lib:elpi.float64 }} = global X, !, stop "float64 comparison is not syntactic".
+eqcorrect-db X {{ lib:elpi.derive.uint63_eq_correct }} :- {{ lib:num.int63.type }} = global X, !.
+eqcorrect-db X _ :- {{ lib:num.float.type }} = global X, !, stop "float64 comparison is not syntactic".
 
 :name "eqcorrect-db:fail"
 eqcorrect-db T _ :-

apps/derive/theories/derive/param1.v

@@ -40,6 +40,8 @@ Class reali {X : Type} {XR : X -> Type} (x : X) (xR : XR x) := Reali {}.
 
 Register store_reali as param1.store_reali.
 
+From Coq Require Import PrimInt63 PrimFloat.
+
 Inductive is_uint63 : PrimInt63.int -> Type := uint63 (i : PrimInt63.int) : is_uint63 i.
 Register is_uint63 as elpi.derive.is_uint63.
 
@@ -55,8 +57,8 @@ pred reali-done i:gref.
 :index(3)
 pred reali i:term, o:term.
 
-reali {{ lib:elpi.uint63 }} {{ lib:elpi.derive.is_uint63 }} :- !.
-reali {{ lib:elpi.float64 }} {{ lib:elpi.derive.is_float64 }} :- !.
+reali {{ lib:num.int63.type }} {{ lib:elpi.derive.is_uint63 }} :- !.
+reali {{ lib:num.float.type }} {{ lib:elpi.derive.is_float64 }} :- !.
 
 :name "reali:fail"
 reali X _ :-
@@ -66,8 +68,8 @@ reali X _ :-
 
 type realiR term -> term -> prop.
 
-realiR {{ lib:elpi.uint63 }} {{ lib:elpi.derive.is_uint63 }} :- !.
-realiR {{ lib:elpi.float64 }} {{ lib:elpi.derive.is_float64 }} :- !.
+realiR {{ lib:num.int63.type }} {{ lib:elpi.derive.is_uint63 }} :- !.
+realiR {{ lib:num.float.type }} {{ lib:elpi.derive.is_float64 }} :- !.
 
 :name "realiR:fail"
 realiR T TR :-

elpi/elpi_elaborator.elpi

@@ -308,8 +308,8 @@ of (global GR as X) T X :- coq.env.typeof GR T1, unify-leq T1 T.
 of (pglobal GR I as X) T X :-
   @uinstance! I => coq.env.typeof GR T1, unify-leq T1 T.
 
-of (primitive (uint63 _) as X) T X :- unify-leq {{ lib:elpi.uint63 }} T.
-of (primitive (float64 _) as X) T X :- unify-leq {{ lib:elpi.float64 }} T.
+of (primitive (uint63 _) as X) T X :- unify-leq {{ lib:num.int63.type }} T.
+of (primitive (float64 _) as X) T X :- unify-leq {{ lib:num.float.type }} T.
 
 of (uvar as X) T Y :- !, evar X T Y.
 

tests/test_elaborator.v

@@ -1,5 +1,6 @@
 From unreleased Extra Dependency "elpi_elaborator.elpi" as elab.
 
+From Coq Require Import PrimInt63 PrimFloat.
 From elpi Require Import elpi.
 
 Elpi Command test.refiner.

theories/elpi.v

@@ -45,8 +45,3 @@ From Coq Require Bool.
 Register Coq.Bool.Bool.reflect  as elpi.reflect.
 Register Coq.Bool.Bool.ReflectF as elpi.ReflectF.
 Register Coq.Bool.Bool.ReflectT as elpi.ReflectT.
-
-From Coq Require PrimFloat PrimInt63.
-
-Register Coq.Floats.PrimFloat.float as elpi.float64.
-Register Coq.Numbers.Cyclic.Int63.PrimInt63.int as elpi.uint63.