fixes

Author: gares

apps/derive/elpi/derive.elpi

@@ -100,7 +100,7 @@ main T P CL :- get-option "recursive" tt, !,
 pred main.aux i:list gref, i:list prop, o:list prop.
 main.aux [] X X.
 main.aux [T|TS] Acc CL :-
-  /* (pi X\get-option "only" X :- !, fail) => */ Acc => main T tt CL1,
+  Acc => main T tt CL1,
   main.aux TS {std.append CL1 Acc} CL.
 
 main T P CL :- main1 T P CL.

apps/derive/elpi/eqb.elpi

@@ -190,12 +190,18 @@ fields.branch2 Args Args2 VarsA _ _ VarsB _ R :-
 fields.aux Args Args2 VarsA VarsB R.
 
 
+pred mk-eqb-for i:term, i:term, o:term.
+mk-eqb-for T1 T2 R :- eqb-for T1 T2 R, !.
+mk-eqb-for T1 _ _ :- 
+  Msg is "derive.eqb: missing boolean equality for " ^ {coq.term->string T1} ^ ", maybe use derive.eqb first",
+  stop Msg.
+
 pred fields.aux i:arguments, i:arguments, i:list term, i:list term, o:term.
 
 fields.aux (dependent TYX FX) (dependent TYY FY) [X|XS] [Y|YS] {{ lib:elpi.andb (lp:EQB lp:X lp:Y) lp:R1 }} :- 
   feqb.trm->term TYX TX,
   feqb.trm->term TYY TY,
-  std.assert! (eqb-for TX TY EQB) "??",
+  mk-eqb-for TX TY EQB,
   @pi-decl `p` TX n\ pi a\ (feqb.trm->term a n :- !) =>
   @pi-decl `p` TY m\ pi b\ (feqb.trm->term b m :- !) =>
     fields.aux (FX a) (FY b) XS YS (R n m),
@@ -204,7 +210,7 @@ fields.aux (dependent TYX FX) (dependent TYY FY) [X|XS] [Y|YS] {{ lib:elpi.andb
 fields.aux (regular TYX FX) (regular TYY FY)  [X|XS] [Y|YS] {{ lib:elpi.andb (lp:EQB lp:X lp:Y) lp:R }} :- 
   feqb.trm->term TYX TX,
   feqb.trm->term TYY TY,
-  std.assert! (eqb-for TX TY EQB) "??",
+  mk-eqb-for TX TY EQB,
   fields.aux FX FY XS YS R.
 
 fields.aux (irrelevant _ FX) (irrelevant _ FY) [_|XS] [_|YS] R :- fields.aux FX FY XS YS R.

apps/derive/elpi/eqbcorrect.elpi

@@ -431,11 +431,15 @@ apply-functor X [ff|Mask] [Y|YS] Rec R :- reali Y PY, apply-functor {coq.mk-app
 
 pred mk-reali i:term, o:term.
 mk-reali T R :- reali T R, !.
-mk-reali T _ :- coq.error {calc ("derive.eqbcorrect: no unary parametricity translation for " ^ {coq.term->string T} ^ ", use derive.param1 first")}.
+mk-reali T _ :-
+  Msg is "derive.eqbcorrect: no unary parametricity translation for " ^ {coq.term->string T} ^ ", use derive.param1 first",
+  stop Msg.
 
 pred mk-eqb-for i:term, o:term.
 mk-eqb-for T R :- eqb-for T T R, !.
-mk-eqb-for T _ :- coq.error {calc ("derive.eqbcorrect: boolean equality for " ^ {coq.term->string T} ^ ", maybe use derive.eqb first")}.
+mk-eqb-for T _ :- 
+  Msg is "derive.eqbcorrect: missing boolean equality for " ^ {coq.term->string T} ^ ", maybe use derive.eqb first",
+  stop Msg.
 
 }
 

apps/derive/examples/usage.v

@@ -68,7 +68,8 @@ Check Box._tag_contents_exchange : (* another one *)
   forall A (r : Box A) x y, set Box._tag x (set Box._contents y r) =
                             set Box._contents y (set Box._tag x r).
 
-(** Finally, one can derive an existing inductive typegenerated constants are
+(** Finally, one can derive an existing inductive type.
+    Generated constants are
     prefixed with nat_ but won't be in the right
     place, which is where the type is defined. This means that two users
     may run derive for the same type in different files, leading to

apps/derive/theories/derive/param1_trivial.v

@@ -149,19 +149,35 @@ Elpi Accumulate Db derive.param1.trivial.db.
 Elpi Accumulate File param1_inhab.
 Elpi Accumulate File param1_trivial.
 Elpi Accumulate lp:{{
-  main [str I, str O] :- !, coq.locate I (indt GR),
-    derive.param1.inhab.main GR O CL,
-    CL => derive.param1.trivial.main GR O _.
   main [str I] :- !, coq.locate I (indt GR),
     derive.param1.inhab.main GR "_witness" CL,
     CL => derive.param1.trivial.main GR "_trivial" _.
   main _ :- usage.
 
   usage :-
-    coq.error "Usage: derive.param1.trivial <inductive type name> [<output suffix>]".
+    coq.error "Usage: derive.param1.trivial <inductive type name>".
 }}.
 Elpi Typecheck.
 
+Elpi Command derive.param1.inhab.
+Elpi Accumulate File derive_hook.
+Elpi Accumulate File paramX.
+Elpi Accumulate File param1.
+Elpi Accumulate Db derive.param1.db.
+Elpi Accumulate Db derive.param1.congr.db.
+Elpi Accumulate Db derive.param1.trivial.db.
+Elpi Accumulate File param1_inhab.
+Elpi Accumulate lp:{{
+  main [str I] :- !, coq.locate I (indt GR),
+    derive.param1.inhab.main GR "_witness" _.
+  main _ :- usage.
+
+  usage :-
+    coq.error "Usage: derive.param1.inhab <inductive type name>".
+}}.
+Elpi Typecheck.
+
+
 (* hook into derive *)
 Elpi Accumulate derive Db derive.param1.trivial.db.
 Elpi Accumulate derive File param1_inhab.