use subject-lifter instead of structure-op

Author: gares

HB/common/database.elpi

@@ -471,8 +471,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 _.
+pred is-subject-lifter i:term, o:int, o:classname.
+is-subject-lifter (global (const C)) N  Class :- exported-op M _ C, wrapper-mixin _ (const C) _, factory-nparams M N, mixin-first-class M Class.
+is-subject-lifter (app[global (const C)|_]) N Class :- exported-op M _ C, wrapper-mixin _ (const C) _, factory-nparams M N, mixin-first-class M Class.
+is-subject-lifter (global GR) N Class :- tag GR Class N, wrapper-mixin _ GR _.
+is-subject-lifter (app[global GR|_]) N Class :- tag GR Class N, wrapper-mixin _ GR _.

HB/common/utils.elpi

@@ -376,7 +376,7 @@ failsafe-structure-inference T T1 :-
       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,
+      is-subject-lifter Subject NP Class,
       coq.safe-dest-app Subject OP ArgsOp,
       std.nth NP ArgsOp S,
       (var S ; name S), % TODO: should be the subject of the structure, not a random name

HB/instance.elpi

@@ -85,7 +85,7 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
       private.declare-mixins-from-factory Factory TheType TheFactory ML TheMixins,
 
       % regular instance %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-      if (get-option "wrapper" ff ; not(is-structure-op-w-wrapper TheType _ _))
+      if (get-option "wrapper" ff ; not(is-subject-lifter TheType _ _))
         % regular subject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
           (private.declare-regular-inst TheType ML TheMixins TyWP SectionName CSL)  
         % wrapper %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

HB/structure.elpi

@@ -678,7 +678,7 @@ factory-on-some-structure-op? T VS F GR :- std.do! [
 
 kind factory-on-subject type.
 type factory-on-the-type w-args factoryname -> factory-on-subject.
-type factory-on-structure-op term -> factoryname -> gref -> factory-on-subject.
+type factory-on-subject-lifter 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 :- !,
@@ -688,10 +688,10 @@ product->triples  {{ lib:hb.prod lp:A lp:B  }} T L ClosureCheck :- !,
 product->triples {{ True }} _ [] tt :- !.
 product->triples {{ False }} _ [] ff :- !.
 product->triples A T [factory-on-the-type F] tt :- factory? A F, F = triple _ _ T, !.
-product->triples A _ [factory-on-structure-op A F OP] tt :- factory-on-some-structure-op? A [] F OP, !.
+product->triples A _ [factory-on-subject-lifter A F OP] tt :- factory-on-some-structure-op? A [] F OP, !.
 product->triples A T _ _ :-
   coq.error "HB: expecting a factory on" {coq.term->string T}
-    "or a factory on a structure operation. Got:" {coq.term->string A}.
+    "or a factory on a structure operation or tag. Got:" {coq.term->string A}.
 
 pred sigT->list-w-params i:term, o:w-params (list factory-on-subject), o:bool.
 sigT->list-w-params (fun N T B) L C :-
@@ -715,13 +715,13 @@ lift-to-the-subject (w-params.nil ID T Rest) (w-params.nil ID T Rest1) :-
 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 _ F OP|Rest] T [WF|Rest1] :-
+lift-to-the-subject.aux [factory-on-subject-lifter _ F OP|Rest] T [WF|Rest1] :-
   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,
   lift-to-the-subject.aux Rest T Rest1.
-lift-to-the-subject.aux [factory-on-structure-op Expr _ _|_] _ _ :-
+lift-to-the-subject.aux [factory-on-subject-lifter Expr _ _|_] _ _ :-
   coq.error "NYI: automatic wrapping for" {coq.term->string Expr}.
 
 

structures.v

@@ -1055,7 +1055,7 @@ Elpi Export HB.check.
 (** [HB.tag] declares a tag for mixin subjects
 
 [[
-HB.tag Definition N Params x := x
+HB.tag Definition N Params (x : S.type) : Type := x
 ]]
 
 *)
@@ -1095,7 +1095,7 @@ main [str G, str"|", int M] :- !,
   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>".
+main _ :- coq.error "Usage: HB.tag Definition <Name> ... <subject> := 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 _).