HB.tag

Author: gares

HB/common/database.elpi

@@ -352,11 +352,14 @@ structure-nparams Structure NParams :-
   class-def (class Class Structure _),
   factory-nparams Class NParams.
 
+pred factory?-split i:term, o:factoryname, o:list term, o:term, o:list term.
+factory?-split (app[global GR|Args]) F [global GR|Params] T Rest :-
+  factory-alias->gref GR F, factory-nparams F NP, !,
+  std.split-at NP Args Params [T|Rest].
+
 pred factory? i:term, o:w-args factoryname.
 factory? S (triple F Params T) :-
-  not (var S), !,
-  safe-dest-app S (global GR) Args, factory-alias->gref GR F, factory-nparams F NP, !,
-  std.split-at NP Args Params [T|_].
+  factory?-split S F [_|Params] T _.
 
 % [find-max-classes Mixins Classes] states that Classes is a list of classes
 %   which contain all the mixins in Mixins.
@@ -376,3 +379,8 @@ find-max-classes [M|Mixins] [C|Classes] :-
   ].
 find-max-classes [M|_] _ :- coq.error "HB: cannot find a class containing mixin" M.
 
+pred is-structure-op-w-wrapper i:term, o:int, o:classname.
+is-structure-op-w-wrapper (global (const C)) N  Class :- exported-op M _ C, wrapper-mixin _ (const C) _, factory-nparams M N, mixin-first-class M Class.
+is-structure-op-w-wrapper (app[global (const C)|_]) N Class :- exported-op M _ C, wrapper-mixin _ (const C) _, factory-nparams M N, mixin-first-class M Class.
+is-structure-op-w-wrapper (global GR) N Class :- tag GR Class N, wrapper-mixin _ GR _.
+is-structure-op-w-wrapper (app[global GR|_]) N Class :- tag GR Class N, wrapper-mixin _ GR _.

HB/common/utils.elpi

@@ -371,13 +371,19 @@ re-enable-id-phant T T1 :-
 
 pred failsafe-structure-inference i:term, o:term.
 failsafe-structure-inference T T1 :-
-  (pi OP Args Args1 M Class NP S\
-    copy (app [global (const OP)|Args]) (app [global (const OP)| Args1]) :-
-      exported-op M _ OP, mixin-first-class M Class, factory-nparams Class NP,
-      std.nth NP Args S,
-      var S,
+  (pi T T2 F_Params F_Params1 Args Args1 Subject Subject1 NP ArgsOp ArgsOp1 OP S\
+    copy T T2 :-
+      factory?-split T _ F_Params Subject Args,
+      std.map F_Params copy F_Params1,
+      std.map Args copy Args1,
+      is-structure-op-w-wrapper Subject NP Class,
+      coq.safe-dest-app Subject OP ArgsOp,
+      std.nth NP ArgsOp S,
+      (var S ; name S),
       !,
-      eta-structure-record NP Class Args Args1) =>
+      eta-structure-record NP Class ArgsOp ArgsOp1,
+      coq.mk-app OP ArgsOp1 Subject1,
+      coq.mk-app (app F_Params1) [Subject1|Args1] T2) =>
   copy T T1.
 
 pred eta-structure-record i:int, i:classname, i:list term, o:list term.

HB/instance.elpi

@@ -88,7 +88,7 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
          % derived instance %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
          (private.declare-regular-inst TheType ML TheMixins TyWP SectionName CSL) 
          % regular instance %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-         (if (get-option "wrapper" ff ; not(private.is-structure-op-w-wrapper TheType))
+         (if (get-option "wrapper" ff ; not(is-structure-op-w-wrapper TheType _ _))
             % regular subject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
              (private.declare-regular-inst TheType ML TheMixins TyWP SectionName CSL)  
             % wrapper %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -400,10 +400,6 @@ declare-wrapper-inst TheType ML TheMixins TyWP SectionName CSL :- std.do![
   private.declare-structure-instance-from-mixins TheNewType WML TheWrappedMixins CSL,
 ].
 
-pred is-structure-op-w-wrapper i:term.
-is-structure-op-w-wrapper (global (const C)) :- exported-op _ _ C, wrapper-mixin _ (const C) _.
-is-structure-op-w-wrapper (app[global (const C)|_]) :- exported-op _ _ C, wrapper-mixin _ (const C) _.
-
 pred derive-wrapper-instances i:term, i:mixinname, o:term, o:constant.
 derive-wrapper-instances Instance WrapperMixin WrapperSubject C :- std.do! [
 

HB/structure.elpi

@@ -12,7 +12,6 @@ declare Module BSkel Sort :- std.do! [
   failsafe-structure-inference BSkelNoId BSkelNoIdX,
   std.assert-ok! (coq.elaborate-skeleton BSkelNoIdX _ BNoId) "illtyped structure definition",
   re-enable-id-phant BNoId B,
-  
   private.sigT->list-w-params B GRFSwP_or_ThingtoBeWrapped ClosureCheck,
 
   % do some work to go back to factories on a single subject
@@ -217,7 +216,6 @@ clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
   gref-deps (const Po) MLwP,
   w-params.nparams MLwP NParams,
   std.length {list-w-params_list MLwP} NMixins,
-
   (pi L L1 L2 Params Rest PoArgs\
     copy (app [global (const Po)| L]) (app [global (const C) | L2]) :-
       std.split-at NParams L Params [_|Rest],
@@ -658,19 +656,25 @@ if-coverage-not-good-error.one _ _. % new class is the first covering M
 %      hom belongs to Quiver, hence hom_isMon takes a "T of Quiver T"
 
 % checks if the term is forall A B C, Factory ... (Op A B C) ...
-pred factory-on-some-structure-op? i:term, i:list term, o:gref, o:constant.
+pred factory-on-some-structure-op? i:term, i:list term, o:gref, o:gref.
 factory-on-some-structure-op? (prod N Ty Bo) VS F OP :-
   @pi-decl N Ty x\
      factory-on-some-structure-op? (Bo x) [x|VS] F OP.
-factory-on-some-structure-op? T VS F OP :-
+factory-on-some-structure-op? T VS F (const OP) :-
   factory? T (triple F _ Subject),
   coq.safe-dest-app Subject (global (const OP)) Args,
   exported-op _ _ OP,
   std.appendR _ {std.rev VS} Args.
+factory-on-some-structure-op? T VS F GR :- std.do! [
+  factory? T (triple F _ Subject),
+  coq.safe-dest-app Subject (global GR) Args,
+  tag GR _ _,
+  std.appendR _ {std.rev VS} Args,
+].
 
 kind factory-on-subject type.
 type factory-on-the-type w-args factoryname -> factory-on-subject.
-type factory-on-structure-op term -> factoryname -> constant -> factory-on-subject.
+type factory-on-structure-op term -> factoryname -> gref -> factory-on-subject.
 
 pred product->triples i:term, i:term, o:list factory-on-subject, o:bool.
 product->triples  {{ lib:hb.prod lp:A lp:B  }} T L ClosureCheck :- !,
@@ -708,7 +712,7 @@ lift-to-the-subject.aux [] _ [].
 lift-to-the-subject.aux [factory-on-the-type F|Rest] T [F|Rest1] :-
   lift-to-the-subject.aux Rest T Rest1.
 lift-to-the-subject.aux [factory-on-structure-op Expr F OP|Rest] T [WF|Rest1] :-
-  wrapper-mixin Wrapper (const OP) F, !,
+  wrapper-mixin Wrapper OP F, !,
   factory-nparams Wrapper NParams,
   coq.mk-app {coq.env.global Wrapper} {std.append {coq.mk-n-holes NParams} [T]} W,
   factory? W WF,

_CoqProject.test-suite

@@ -52,7 +52,6 @@ examples/Coq2020_material/CoqWS_abstract.v
 examples/Coq2020_material/CoqWS_expansion/withHB.v
 examples/Coq2020_material/CoqWS_expansion/withoutHB.v
 
-examples/cat/cat.v
 tests/enriched_cat_case6.v
 
 tests/type_of_exported_ops.v
@@ -84,6 +83,7 @@ tests/fun_instance.v
 tests/issue284.v
 tests/issue287.v
 tests/monoid_enriched_cat.v
+tests/tag_wrap.v
 
 -R tests HB.tests
 -R examples HB.examples

structures.v

@@ -167,6 +167,11 @@ pred mixin-mem i:term, o:gref.
 %  wrapper-mixin (indt "hom_isMon") (const "hom") (indt "isMon").
 pred wrapper-mixin o:mixinname, o:gref, o:mixinname.
 
+% designated identity function for wrapping (sometimes you don't have a
+% structure op for it).
+% [tag GR Class NParams]
+pred tag o:gref, o:classname, o:int.
+
 %%%%%% Memory of exported mixins (HB.structure) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Operations (named mixin fields) need to be exported exactly once,
 % but the same mixin can be used in many structure, hence this memory
@@ -1002,6 +1007,68 @@ check-or-not Skel :-
 Elpi Typecheck.
 Elpi Export HB.check.
 
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+
+(** [HB.tag] declares a tag for mixin subjects
+
+[[
+HB.tag Definition N Params x := x
+]]
+
+*)
+
+#[arguments(raw)] Elpi Command HB.tag.
+Elpi Accumulate Db hb.db.
+Elpi Accumulate File "HB/common/stdpp.elpi".
+Elpi Accumulate File "HB/common/database.elpi".
+#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
+#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
+Elpi Accumulate File "HB/common/utils.elpi".
+Elpi Accumulate File "HB/common/log.elpi".
+Elpi Accumulate File "HB/common/synthesis.elpi".
+Elpi Accumulate File "HB/context.elpi".
+Elpi Accumulate File "HB/instance.elpi".
+Elpi Accumulate lp:{{
+
+main [const-decl Name (some BodySkel) AritySkel] :- !, std.do! [
+  std.assert-ok! (coq.elaborate-arity-skeleton AritySkel _ Arity) "HB: type illtyped",
+  coq.arity->nparams Arity N,
+  coq.arity->term Arity Ty,
+  std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "HB: body illtyped",
+  with-attributes (with-logging (std.do! [
+    log.coq.env.add-const-noimplicits Name Body Ty @transparent! C,
+    coq.arity->implicits Arity CImpls,
+    if (coq.any-implicit? CImpls)
+     (@global! => coq.arguments.set-implicit (const C) [CImpls])
+     true,
+  ])),
+  M is N - 1,
+  class-of-nth-arg M Ty Class,
+  acc-clause current (tag (const C) Class M),
+].
+main [str G, str"|", int M] :- !,
+  coq.locate G GR,
+  coq.env.typeof GR Ty,
+  class-of-nth-arg M Ty Class,
+  acc-clause current (tag GR Class M).
+
+main _ :- coq.error "Usage: HB.tag Definition <Name> := <Builder> T ...\nUsage: HB.tag <gref> | <nparams>".
+
+pred class-of-nth-arg i:int, i:term, o:classname.
+class-of-nth-arg 0 (prod _ (global S) _\_) Class :- class-def (class Class S _).
+class-of-nth-arg 0 (prod _ (app [global S|_]) _\_) Class :- class-def (class Class S _).
+class-of-nth-arg N (prod Name Ty Bo) Class :- N > 0, !, M is N - 1,
+  @pi-decl Name Ty x\ class-of-nth-arg M (Bo x) Class.
+class-of-nth-arg 0 T _ :- !,
+  coq.error "HB: the last parameter of a tag must be of a structure type:" {coq.term->string T}.
+class-of-nth-arg _ T _ :- !,
+  coq.error "HB: not enough argsuments:" {coq.term->string T}.
+
+}}.
+Elpi Typecheck.
+Elpi Export HB.tag.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)

tests/tag_wrap.v

@@ -0,0 +1,38 @@
+From HB Require Import structures.
+
+HB.mixin Record isSomething T := { clearly : True }.
+HB.structure Definition Something := { T of isSomething T }.
+
+HB.mixin Record isTerminal (T : Type) := { p : True }.
+
+HB.tag Definition this_one (T : Something.type) : Type := T.
+
+#[wrapper]
+HB.mixin Record this_one_isTerminal T of Something T := {
+  private : isTerminal (this_one T)
+}.
+
+HB.tag Definition this_other_one (T : Something.type) : Type := T.
+
+#[wrapper]
+HB.mixin Record this_other_one_isTerminal T of Something T := {
+  private : isTerminal (this_other_one T)
+}.
+(* This is a bug, maybe even in master. If I declare an instance on a mixin
+   which leads to no new structure instance, then the mixin is not use later
+   on *)
+HB.structure Definition magic1 := { T of
+  isSomething T &
+  isTerminal (this_one T)
+}.
+
+HB.structure Definition magic := { T of
+  isSomething T &
+  isTerminal (this_one T) &
+  isTerminal (this_other_one T)
+}.
+
+HB.instance Definition _ : isSomething nat := isSomething.Build nat I.
+HB.instance Definition _ : isTerminal (this_one nat) := isTerminal.Build nat I.
+HB.instance Definition _ : isTerminal (this_other_one nat) := isTerminal.Build nat I.
+Check nat : magic.type.