HB.check

Author: gares

HB/common/log.compat.current.elpi

@@ -35,7 +35,7 @@ log.private.log-vernac _.
 
 shorten log.private.coq.vernac.{ begin-module , end-module , begin-section, end-section }.
 shorten log.private.coq.vernac.{ import-module , export-module }.
-shorten log.private.coq.vernac.{ definition , variable , comment }.
+shorten log.private.coq.vernac.{ definition , variable , comment , check }.
 shorten log.private.coq.{ vernac.inductive , vernac.implicit }.
 shorten log.private.coq.vernac.{ canonical , abbreviation , notation , coercion }.
 shorten log.private.{ coq.vernac }.
@@ -100,6 +100,8 @@ coq.vernac->pp1 (vernac.implicit Local Name [L]) (box h [Locality, str "Argument
   std.intersperse spc PP1 PP.
 coq.vernac->pp1 (comment A) (box (hov 2) [str"(*", str S, str"*)"]) :-
   std.any->string A S.
+coq.vernac->pp1 (check T) (box (hov 2) [str"Check", spc, PPT, str"."]) :-
+  @holes! => coq.term->pp T PPT.
 
 pred local->locality i:bool, o:coq.pp.
 local->locality tt (str "Local ").

HB/common/log.elpi

@@ -125,6 +125,12 @@ log.coq.env.accumulate S DB CL :- std.do! [
   if-verbose (log.private.log-vernac (log.private.coq.vernac.comment CL)),
 ].
 
+pred log.coq.check i:term, o:term, o:term.
+log.coq.check Skel Ty T :- std.do! [
+  std.assert-ok! (coq.elaborate-skeleton Skel Ty T) "Check fails",
+  log.private.log-vernac (log.private.coq.vernac.check Skel),
+].
+
 namespace log.private {
 
 %%%%% Logging Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -160,6 +166,7 @@ type coq.vernac.coercion      string -> gref -> class       -> coq.vernac.
 type coq.vernac.canonical     string                        -> coq.vernac.
 type coq.vernac.implicit      bool -> string -> list (list implicit_kind)  -> coq.vernac.
 type coq.vernac.comment       A                             -> coq.vernac.
+type coq.vernac.check         term                          -> coq.vernac.
 
 }
 

HB/common/stdpp.elpi

@@ -133,7 +133,7 @@ pred copy-constructor i:indc-decl, o:indc-decl.
 copy-constructor (constructor ID A) (constructor ID A1) :- copy-arity A A1.
 
 % TODO: move to coq-elpi proper
-pred coq.gref.list->set i:list mixinname, o:coq.gref.set.
+pred coq.gref.list->set i:list gref, o:coq.gref.set.
 coq.gref.list->set L S :-
   std.fold L {coq.gref.set.empty} coq.gref.set.add S.
 

HB/common/utils.elpi

@@ -32,6 +32,7 @@ with-attributes P :-
     att "arg_sort" bool,
     att "log" bool,
     att "log.raw" bool,
+    att "skip" string,
   ] Opts, !,
   Opts => P.
 
@@ -86,7 +87,7 @@ nice-gref->string X Mod :-
 nice-gref->string X S :-
   coq.term->string (global X) S.
 
-pred gref->modname i:mixinname, o:id.
+pred gref->modname i:gref, o:id.
 gref->modname GR ModName :-
   coq.gref->path GR Path,
   if (std.rev Path [_,ModName|_]) true (coq.error "No enclosing module for " GR).

structures.v

@@ -599,6 +599,33 @@ Elpi Typecheck.
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 
+(** [HB.check T] acts like [Check T] but supports the attribute [#[skip="rex"]]
+    that skips the action on Coq version matches rex *)
+
+Elpi Command HB.check.
+Elpi Accumulate Db hb.db.
+Elpi Accumulate File "HB/common/stdpp.elpi".
+Elpi Accumulate File "HB/common/utils.elpi".
+Elpi Accumulate File "HB/common/log.elpi".
+Elpi Accumulate lp:{{
+main [trm Skel] :- !, with-attributes (with-logging (check-or-not Skel)).
+main _ :- coq.error "usage: HB.check (term).".
+
+pred check-or-not i:term.
+check-or-not Skel :-
+  coq.version VersionString _ _ _,
+  if (get-option "skip" R, rex_match R VersionString)
+     (coq.warn "Skipping test on Coq" VersionString "as requested")
+     (log.coq.check Skel Ty T,
+      coq.say {coq.term->string T} ":" {coq.term->string Ty}).
+}}.
+Elpi Typecheck.
+Elpi Export HB.check.
+
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+
 (** Technical notations from /Canonical Structures for the working Coq user/ *)
 Notation "`Error_cannot_unify: t1 'with' t2" := (unify t1 t2 None)
   (at level 0, format "`Error_cannot_unify:  t1  'with'  t2", only printing) :

tests/funclass.v

@@ -53,18 +53,6 @@ HB.mixin Record silly T := { xx : T }.
 #[infer(F = "_ -> _")]
 HB.structure Definition wp T (F : Monoid.type T) := { A of silly A }.
 
-Elpi Command CheckUnelssCoqVersion.
-Elpi Accumulate lp:{{
-main [int CV, trm Skel] :-
-  coq.version VersionString _ V _,
-  if (CV = V)
-     (coq.warn "Skipping test on Coq" VersionString)
-     (std.assert-ok! (coq.elaborate-ty-skeleton Skel _ T) "Check fails",
-      coq.say "Checked term:\n" {coq.term->string T}).
-}}.
-Elpi Typecheck.
-Elpi Export CheckUnelssCoqVersion.
-
-
-CheckUnelssCoqVersion 11 (forall w : wp.type _ mult, w = w).
+#[skip="8.11"]
+HB.check (forall w : wp.type _ mult, w = w).