Merge pull request #734 from LPCIC/derive-register

derive: ability to register an axiom

Author: gares

apps/derive/elpi/eqType.elpi

@@ -64,8 +64,8 @@ pred self o:eqb.trm.
 
 pred valid i:eqb.trm, o:diagnostic.
 valid (eqb.global X) ok :- global X = {{ PrimInt63.int }}, !.
-valid (eqb.global (indt I)) ok :- eqType I _, !.
-valid (eqb.app (indt I) A Args) D :- eqType I EQT, !, valid-eqType EQT [A|Args] D.
+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}.
 
 pred valid-eqType i:eqb.eqType, i:list eqb.trm, o:diagnostic.
@@ -79,10 +79,10 @@ valid-eqType (eqb.value-param _ F) [_|TS] D :- std.do-ok! D [
 ].
 
 pred irrelevant? i:term, o:eqb.trm, o:diagnostic.
-irrelevant? (app [{{ @eq }}, global (indt EqType), A, B]) (eqb.app EQ EQTYPE [A1,B1]) D :- std.do-ok! D [
+irrelevant? (app [{{ @eq }}, global EqType, A, B]) (eqb.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 (eqb.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 (eqb.inductive _ _)) "unknown or not applied enough type",
+  std.assert! (eqType (indt I) (eqb.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/tests-stdlib/test_derive.v

@@ -170,3 +170,21 @@ End derive_container.
 About wimpls.wimpls.
 About wimpls.Kwi.
 Redirect "tmp" Check Kwi _ (refl_equal 3).
+
+Section TestRegister.
+Variable T : Type.
+Definition is_T : T -> Type := fun x => True.
+Definition is_T_inhab : forall x : T, is_T x := fun x => I.
+Variable eqb : T -> T -> bool.
+Variable eqb_correct : forall x y,eqb x y = true -> x = y.
+Variable eqb_refl : forall x, eqb x x = true.
+
+derive.eqbOK.register_axiom T is_T is_T_inhab eqb eqb_correct eqb_refl.
+
+Inductive foo := X : T -> foo.
+
+#[only(eqbOK),verbose] derive foo.
+
+Redirect "tmp" Print foo_eqb_OK.
+
+End TestRegister.

apps/derive/theories/derive/eqType_ast.v

@@ -24,10 +24,11 @@ type eqb.stop       eqb.trm -> eqb.arguments.
 type eqb.type-param  (eqb.trm -> eqb.eqType) -> eqb.eqType.
 type eqb.value-param eqb.trm -> (eqb.trm -> eqb.eqType) -> eqb.eqType.
 type eqb.inductive   inductive -> (eqb.trm -> list eqb.constructor) -> eqb.eqType.
+type eqb.axiom       eqb.eqType.
 
 type eqb.constructor constructor -> eqb.arguments -> eqb.constructor.
 
-pred eqType i:inductive, o:eqb.eqType.
+pred eqType i:gref, o:eqb.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,35 @@ 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.eqbOK.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 File eqType.
+Elpi Accumulate lp:{{
+   main [str Type, str IsT, str IsTinhab, str Eqb, str Correct, str Refl] :- !,
+     coq.locate Type GrType,
+     coq.locate IsT GRisT,
+     coq.locate IsTinhab GRisTinhab,
+     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 eqb.axiom)),
+     coq.elpi.accumulate _ "derive.param1.db" (clause _ _ (reali-done GrType)),
+     coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "reali:fail") (reali (global GrType) (global GRisT) :- !)),
+     coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "realiR:fail") (realiR (global GrType) (global GRisT) :- !)),
+     coq.elpi.accumulate _ "derive.param1.trivial.db" (clause _ _ (param1-inhab-db (global GRisT) (global GRisTinhab))).
+  main _ :- coq.error "usage: derive.eqbOK.register_axiom T is_T is_T_inhab eqb eqb_correct eqb_refl.".
+}}.
+Elpi Export derive.eqbOK.register_axiom.