fix rebase

HB/common/synthesis.elpi

@@ -113,9 +113,10 @@ under-mixin-src-from-factory.do! TheType TheFactory LP :- std.do! [
 
 % Given TheType makes the provided list of mixins and instances
 % available for inference.
-pred under-these-mixin-src.do! i:term, i:list mixinname, i:list constant, i:list prop.
-under-these-mixin-src.do! TheType ML TheMixins LP :- std.do! [
+pred under-these-mixin-src.do! i:term, i:list mixinname, i:list constant, o:list prop, i:list prop.
+under-these-mixin-src.do! TheType ML TheMixins ClausesHas LP :- std.do! [
   std.map2 ML TheMixins (m\mi\c\ c = mixin-src TheType m (global (const mi))) MLClauses,
+  std.map-filter MLClauses mixin-src->has-mixin-instance ClausesHas,
   MLClauses => std.do! LP
 ].
 

HB/instance.elpi

@@ -87,16 +87,18 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
       % regular instance %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       if (get-option "wrapper" ff ; not(is-subject-lifter TheType _ _))
         % regular subject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-          (private.declare-regular-inst TheType ML TheMixins TyWP SectionName CSL)  
+          (private.declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL)  
         % wrapper %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-          (private.declare-wrapper-inst TheType ML TheMixins TyWP SectionName CSL)
+          (private.declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL)
       ,
 
       % shared to all branches
       if (get-option "export" tt)
          (coq.env.current-library File,
-              std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses)
-         (Clauses = []),
+              std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) ClausesExp)
+         (ClausesExp = []),
+
+      std.append ClausesHas ClausesExp Clauses,
   ]),
 
   % we accumulate clauses now that the section is over
@@ -416,13 +418,13 @@ declare-mixins-from-factory Factory T F ML TheMixins :- std.do! [
 
 % [declare-structure-instance-from-mixins T ML MLI] given mixins ML and
 % their implementation MLI declares all structure instances for T
-pred declare-structure-instance-from-mixins i:term, i:list mixinname, i:list constant, o:list (pair id constant).
-declare-structure-instance-from-mixins T ML TheMixins CL :- std.do! [
+pred declare-structure-instance-from-mixins i:term, i:list mixinname, i:list constant, o:list prop, o:list (pair id constant).
+declare-structure-instance-from-mixins T ML TheMixins ClausesHas CL :- std.do! [
   % The order of the following two "under...do!"  is crucial,
   % priority must be given to canonical mixins
   % as they are the ones which guarantee forgetful inheritance
   % hence we add these clauses last.
-  synthesis.under-these-mixin-src.do! T ML TheMixins [
+  synthesis.under-these-mixin-src.do! T ML TheMixins ClausesHas [
     synthesis.under-local-canonical-mixins-of.do! T [
       instance.declare-all T {findall-classes-for ML} CL,
     ]
@@ -436,9 +438,9 @@ close-section-if-has-params _ SectionName :-
   log.coq.env.end-section-name SectionName.
 
 pred declare-regular-inst i:term, i:list mixinname, i:list constant, i:arity, i:id,
-  o:list (pair id constant). 
-declare-regular-inst TheType ML TheMixins TyWP SectionName CSL :- std.do![
-  private.declare-structure-instance-from-mixins TheType ML TheMixins CCSL,
+  o:list prop, o:list (pair id constant). 
+declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL :- std.do![
+  private.declare-structure-instance-from-mixins TheType ML TheMixins ClausesHas CCSL,
 
   % TODO: share between the two cases and put just after declare-mixins-from-factory
   % since it talks about the unwrapped mixins
@@ -450,13 +452,13 @@ declare-regular-inst TheType ML TheMixins TyWP SectionName CSL :- std.do![
 ].
 
 pred declare-wrapper-inst i:term, i:list mixinname, i:list constant, i:arity, i:id,
-  o:list (pair id constant). 
-declare-wrapper-inst TheType ML TheMixins TyWP SectionName CSL :- std.do![
+  o:list prop, o:list (pair id constant). 
+declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL :- std.do![
   coq.safe-dest-app TheType TheTypeKey _,
   std.assert! (TheTypeKey = global TheTypeKeyGR) "The subject to be wrapped has no key",
   private.close-section-if-has-params TyWP SectionName,
   private.wrap-mixins TheTypeKeyGR ML TheMixins TheNewType WML TheWrappedMixins,
-  private.declare-structure-instance-from-mixins TheNewType WML TheWrappedMixins CSL,
+  private.declare-structure-instance-from-mixins TheNewType WML TheWrappedMixins ClausesHas CSL,
 ].
 
 pred derive-wrapper-instances i:term, i:mixinname, o:term, o:constant.

tests/hnf.v

@@ -14,5 +14,5 @@ Print HB_unnamed_mixin_8.
 
 HB.instance Definition _ := f.Build bool (3 + 2).
 Print Datatypes_bool__canonical__hnf_S.
-Print HB_unnamed_mixin_12.
+(* Print HB_unnamed_mixin_12. *)
 

tests/hnf.v.out

@@ -5,8 +5,5 @@ HB_unnamed_mixin_8 =
 {| M.x := f.y nat HB_unnamed_factory_6 + 1 |}
      : M.axioms_ nat
 Datatypes_bool__canonical__hnf_S =
-{| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |}
+{| S.sort := bool; S.class := {| S.hnf_M_mixin := hnf_f__to__hnf_M__11 |} |}
      : S.type
-HB_unnamed_mixin_12 =
-Builders_2.HB_unnamed_factory_4 bool HB_unnamed_factory_9
-     : M.axioms_ bool

tests/not_same_key.v.out

@@ -1,2 +1,3 @@
 The command has indeed failed with message:
-HB: all mixins must have the same key
+HB: expecting a factory on T 
+or a factory on a structure operation or tag. Got: B.phant_axioms T T1