Merge pull request #522 from Tragicus/uniq-mixin

Author: CohenCyril

HB/common/synthesis.elpi

@@ -86,13 +86,22 @@ assert!-infer-mixin T M B :-
 
 % Given TheType it looks all canonical structure instances on it and makes
 % all their mixins available for inference
-pred under-local-canonical-mixins-of.do! i:term, i:list prop.
-under-local-canonical-mixins-of.do! T P :- std.do! [
+pred local-canonical-mixins-of.aux i:term, i:list structure, o:list prop.
+local-canonical-mixins-of.aux _ [] [].
+local-canonical-mixins-of.aux T [S|Ss] MSL'' :- std.do! [
+  private.structure-instance->mixin-srcs T S MSL,
+	MSL => local-canonical-mixins-of.aux T Ss MSL',
+	std.append MSL MSL' MSL'',
+	].
+	
+pred local-canonical-mixins-of i:term, o:list prop.
+local-canonical-mixins-of T MSL :- std.do! [
   get-canonical-structures T CS,
-  std.map CS (private.structure-instance->mixin-srcs T) MSLL,
-  std.flatten MSLL MSL,
-  MSL => std.do! P
-].
+	std.map CS (s\c\ sigma w\ class-def (class c s w)) Cl,
+	toposort-classes Cl ClSorted,
+	std.map ClSorted (c\s\ sigma w\ class-def (class c s w)) CSSorted,
+	local-canonical-mixins-of.aux T CSSorted MSL,
+	].
 
 % Given TheType and a factory instance (on it), makes all the mixins provided by
 % the factory available for inference.
@@ -298,7 +307,7 @@ structure-instance->mixin-srcs.aux2 Params T Class (some P) M :-
   coq.mk-app (global (const P)) {std.append Params [T,Class]} M.
 structure-instance->mixin-srcs.aux T  F CL :-
   factory-instance->new-mixins [] F ML,
-  std.map ML (m\c\ c = mixin-src T m F) CL.
+  std.map-filter ML (m\c\ not (mixin-src T m _), c = mixin-src T m F) CL.
 
 % [factory-instance->new-mixins OldMixins FI MSL] find all the mixins
 % which can be generated by the factory instance FI which are not part of

HB/instance.elpi

@@ -391,8 +391,9 @@ declare-canonical-instances-from-factory Factory T F ClausesHas CFL CSL :- std.d
   % priority must be given to canonical mixins
   % as they are the ones which guarantee forgetful inheritance
   % hence we add these clauses last.
+	synthesis.local-canonical-mixins-of T MLCano,
   synthesis.under-mixin-src-from-factory.do! T F [
-    synthesis.under-local-canonical-mixins-of.do! T [
+    MLCano => std.do! [
       list-w-params_list {factory-provides Factory} ML,
       add-all-mixins T Factory ML tt Clauses CFL,
       std.map-filter Clauses (mixin-src->has-mixin-instance ) ClausesHas,

HB/pack.elpi

@@ -39,21 +39,21 @@ main Ty Args Instance :- std.do! [
 
 namespace private {
 
-pred synth-instance i:list term, i:gref, i:gref, i:term, i:term, i:list term, o:term.
-synth-instance Params KC KS T Tkey [Factory|Factories] Instance :-
+pred synth-instance.aux i:list term, i:gref, i:gref, i:term, i:term, i:list term, i:list prop, o:term.
+synth-instance.aux Params KC KS T Tkey [Factory|Factories] MLCano Instance :-
   synthesis.under-new-mixin-src-from-factory.do! Tkey Factory (_\
-    synth-instance Params KC KS T Tkey Factories Instance).
-synth-instance Params KC KS T Tkey [] Instance :- coq.safe-dest-app Tkey (global _) _, !,
-  synthesis.under-local-canonical-mixins-of.do! Tkey [
+    synth-instance.aux Params KC KS T Tkey Factories MLCano Instance).
+synth-instance.aux Params KC KS T Tkey [] MLCano Instance :-
+	MLCano => std.do! [
     std.assert-ok! (synthesis.infer-all-args-let Params Tkey KC ClassInstance) "HB.pack: cannot infer the instance",
     std.append Params [T, ClassInstance] InstanceArgs,
       Instance = app[global KS | InstanceArgs]
 ].
-synth-instance Params KC KS T Tkey [] Instance :- std.do! [
-  std.assert-ok! (synthesis.infer-all-args-let Params Tkey KC ClassInstance) "HB.pack: cannot infer the instance",
-  std.append Params [T, ClassInstance] InstanceArgs,
-    Instance = app[global KS | InstanceArgs]
-].
+
+pred synth-instance i:list term, i:gref, i:gref, i:term, i:term, i:list term, o:term.
+synth-instance Params KC KS T Tkey Factories Instance :-
+	if (coq.safe-dest-app Tkey (global _) _) (synthesis.local-canonical-mixins-of Tkey MLCano) (MLCano = []),
+	synth-instance.aux Params KC KS T Tkey Factories MLCano Instance.
 
 pred elab-factories i:list argument, i:term, o:list term.
 elab-factories [] _ [].