wip

apps/derive/elpi/eqType.elpi

@@ -64,8 +64,8 @@ pred self o:trm.
 
 pred valid i:trm, o:diagnostic.
 valid {{ PrimInt63.int }} ok :- !.
-valid (global (indt I)) ok :- eqType I _, !.
-valid (app (indt I) A Args) D :- eqType I EQT, !, valid-eqType EQT [A|Args] D.
+valid (global GR) ok :- eqType GR _, !.
+valid (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}.
 
 pred valid-eqType i:eqType, i:list trm, o:diagnostic.
@@ -79,10 +79,10 @@ valid-eqType (value-param _ F) [_|TS] D :- std.do-ok! D [
 ].
 
 pred irrelevant? i:term, o:trm, o:diagnostic.
-irrelevant? (app [{{ @eq }}, global (indt EqType), A, B]) (app EQ EQTYPE [A1,B1]) D :- std.do-ok! D [
+irrelevant? (app [{{ @eq }}, global EqType, A, B]) (app EQ EQTYPE [A1,B1]) D :- std.do-ok! D [
   std.lift-ok (eqType EqType _) "Not an eqType", %eqb-for Bool Bool _,
   std.lift-ok ({{ @eq }} = global EQ) "",
-  term->trm (global (indt EqType)) EQTYPE,
+  term->trm (global EqType) EQTYPE,
   term->trm A A1,
   term->trm B B1,
 ].
@@ -138,7 +138,7 @@ pred main i:inductive, o:list prop.
 main I [C] :-
   std.assert-ok! (translate-indt I EQT) "derive.eqType.ast: translate",
   std.assert-ok! (validate-eqType EQT) "derive.eqType.ast: validate",
-  C = (eqType I EQT),
+  C = (eqType (indt I) EQT),
   coq.elpi.accumulate _ "derive.eqType.db" (clause _ _ C).
 
 }

apps/derive/elpi/eqb.elpi

@@ -9,7 +9,7 @@ macro @pi-trm N T F :-
 
 pred derive.eqb.main i:gref, i:string, o:list prop.
 derive.eqb.main (indt I) Prefix CL :- std.do! [
-  std.assert! (eqType I FI) "this inductive is not supported",
+  std.assert! (eqType (indt I) FI) "this inductive is not supported",
 
   derive.eqb.eqbf.main FI FI [] [] R,
   std.assert-ok! (coq.typecheck R Rty) "derive.eqbf generates illtyped term",

apps/derive/elpi/eqbOK.elpi

@@ -34,7 +34,7 @@ add-reflect (inductive _ _) Correct Refl {{iffP2 lp:Correct lp:Refl}}.
 
 pred main i:gref, i:string, o:list prop.
 main (indt I) Prefix [CL] :- std.do! [
-  std.assert! (eqType I FI) "this inductive is not supported",
+  std.assert! (eqType (indt I) FI) "this inductive is not supported",
   std.assert! (eqcorrect-for (indt I) Correct Refl) "run eqbcorrect before",
 
   add-reflect FI (global (const Correct)) (global (const Refl)) Breflect,

apps/derive/elpi/eqbcorrect.elpi

@@ -23,7 +23,7 @@ pred config  o:term,            o:term,               o:term,                 o:
 pred main i:gref, i:string, o:list prop.
 main (indt I) Prefix CLs :- std.do! [
 
-  std.assert! (eqType I FI) "this inductive is not supported",
+  std.assert! (eqType (indt I) FI) "this inductive is not supported",
 
   std.assert! (induction-db I Indu) "call derive.induction before",
 
@@ -102,11 +102,11 @@ main (indc _) _ _ :- stop "derive.eqbcorrect does not work on a constructor".
 
 pred search-eqcorrect-for i:term, o:term, o:term.
 search-eqcorrect-for (global (indt I)) (global (const C)) (global (const R)) :-
-  std.assert! (eqType I (inductive _ _)) "unknown or not applied enough type",
+  std.assert! (eqType (indt I) (inductive _ _)) "unknown or not applied enough type",
   eqcorrect-for (indt I) C R.
 
 search-eqcorrect-for (app[global (indt I)|Args]) CArgs RArgs :-
-  std.assert! (eqType I F) "unknown",
+  std.assert! (eqType (indt I) F) "unknown",
   eqcorrect-for (indt I) C R,
   search-eqcorrect-apply F Args (global (const C)) (global (const R)) CArgs RArgs.
 

apps/derive/elpi/fields.elpi

@@ -21,7 +21,7 @@ main I Prefix AllCL :- std.do! [
 
   std.assert! (tag-for I Tag) "no tag for this inductive, run that derivation first",
 
-  std.assert! (eqType I FI) "this inductive is not supported",
+  std.assert! (eqType(indt I) FI) "this inductive is not supported",
   coq.env.indt I _ _ _ Arity KS _,
 
   box (global (indt I)) KS FI CLB,

apps/derive/theories/derive/eqType_ast.v

@@ -24,10 +24,11 @@ type stop       trm -> arguments.
 type type-param         (trm -> eqType) -> eqType.
 type value-param trm -> (trm -> eqType) -> eqType.
 type inductive   inductive -> (trm -> list constructor) -> eqType.
+type axiom       eqType.
 
 type constructor constructor -> arguments -> constructor.
 
-pred eqType i:inductive, o:eqType.
+pred eqType i:gref, o:eqType.
 
 }}.
 
@@ -60,6 +61,6 @@ Elpi Accumulate derive File eqType.
 
 Elpi Accumulate derive lp:{{
 
-derivation (indt T) _ ff (derive "eqType_ast" (derive.eqType.ast.main T) (eqType T _)).
+derivation (indt T) _ ff (derive "eqType_ast" (derive.eqType.ast.main T) (eqType (indt T) _)).
 
 }}.

apps/derive/theories/derive/eqbOK.v

@@ -2,9 +2,9 @@
 
    license: GNU Lesser General Public License Version 2.1 or later           
    ------------------------------------------------------------------------- *)
-   
-Require Import eqb_core_defs.
-Require Import tag eqType_ast fields eqb eqbcorrect derive.
+
+From elpi.apps.derive Require Import eqb_core_defs.
+From elpi.apps.derive Require Import tag eqType_ast fields eqb eqbcorrect derive.
 
 From elpi.apps.derive.elpi Extra Dependency "eqbOK.elpi" as eqbOK.
 From elpi.apps.derive.elpi Extra Dependency "eqType.elpi" as eqType.
@@ -61,3 +61,44 @@ derivation (indt T) Prefix ff (derive "eqbOK" (derive.eqbOK.main (indt T) Prefix
 derivation (const T) Prefix ff (derive "eqbOK-alias" (derive.eqbOK.main (const T) Prefix) (eqbok-for (const T) _)).
 
 }}.
+
+
+Elpi Command derive.register_axiom.
+Elpi Accumulate Db derive.eqb.db.
+Elpi Accumulate Db derive.eqbcorrect.db.
+Elpi Accumulate Db derive.param1.db.
+Elpi Accumulate Db derive.param1.trivial.db.
+Elpi Accumulate Db derive.eqType.db.
+Elpi Accumulate lp:{{
+   main [str Type, str Eqb, str Correct, str Refl] :-
+     coq.locate Type GrType,
+     coq.locate Eqb GrEqb,
+     coq.locate Correct GrCorrect,
+     coq.locate Refl GrRefl,
+     GrRefl = const R,
+     GrCorrect = const C,
+     coq.elpi.accumulate _ "derive.eqb.db" (clause _ _ (eqb-done GrType)),
+     coq.elpi.accumulate _ "derive.eqb.db" (clause _ _ (eqb-for (global GrType) (global GrType) (global GrEqb))),
+     coq.elpi.accumulate _ "derive.eqbcorrect.db" (clause _ _ (eqcorrect-for GrType C R)),
+     coq.elpi.accumulate _ "derive.eqbcorrect.db" (clause _ _ (correct-lemma-for (global GrType) (global GrCorrect))),
+     coq.elpi.accumulate _ "derive.eqbcorrect.db" (clause _ _ (refl-lemma-for (global GrType) (global GrRefl))),
+     coq.elpi.accumulate _ "derive.eqType.db" (clause _ _ (eqType GrType axiom)),
+     coq.elpi.accumulate _ "derive.param1.db" (clause _ _ (reali-done GrType)), % HACK
+     coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "reali:fail") (reali (global GrType) {{ fun (x : lp:{{global GrType}}) => unit }} :- !)), % HACK
+     coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "realiR:fail") (realiR (global GrType) {{ fun (x : lp:{{global GrType}}) => unit }} :- !)), % HACK
+     coq.elpi.accumulate _ "derive.param1.trivial.db" (clause _ _ (param1-inhab-db {{ fun (x : lp:{{global GrType}}) => unit }} {{ fun (x : lp:{{global GrType}}) => tt }})).
+}}.
+Elpi Export derive.register_axiom.
+
+Axiom T : Type.
+Axiom eqb : T -> T -> bool.
+Axiom eqb_correct : forall x y,eqb x y -> x = y.
+Axiom eqb_refl : forall x, eqb x x = true.
+
+derive.register_axiom T eqb eqb_correct eqb_refl.
+
+Inductive foo := X : T -> foo.
+
+#[only(eqbOK)] derive foo.
+
+Print is_foo_inhab.