instance.elpi: redirect-instances in progress, added call to declare-…

…instance, now working

HB/instance.elpi

@@ -528,20 +528,28 @@ declare-canonical-instances-from-factory Factory T F CSL :- std.do! [
     synthesis.under-local-canonical-mixins-of.do! T [
       list-w-params_list {factory-provides Factory} ML,
       coq.say "DCIFF!!!!!!! Ex ML (mixin names) = " ML,
+      %std.findall (mixin-src (sort _) _ _) YYY,
 
       % Clauses, MCSL and AllSubjects are outputs. currently, AllSubjects = [T]
-      add-all-mixins T Factory ML tt Clauses MCSL AllSubjects,
+      add-all-mixins T Factory ML tt ClausesFromF MCSL AllSubjects,
       coq.say "DCIFF!!!!!!!!!! Ex AllSubjects = " AllSubjects,  
       % old (Clauses not used)
       % instance.declare-all T {findall-classes-for ML} CCSL,  
-      % hcumul-forall AllSubjects (s \ instance.declare-all s {findall-classes-for ML}) CCSL,     
+      hcumul-forall AllSubjects (s \
+        instance.declare-all s {findall-classes-for ML}) CCSL,     
     ] 
   ],
 
   % Clauses => instance.declare-all T {findall-classes-for ML} CCSL,
   % new (should use Clauses and AllSubjects)
-  Clauses => hcumul-forall AllSubjects (s \ instance.declare-all s {findall-classes-for ML}) CCSL,     
-
+  %std.findall (mixin-src (sort _) _ _) XXX,
+  %coq.say "XXX" XXX,
+  %coq.say "Clauses" Clauses,
+  %coq.say "YYY dentro il under-*" YYY,
+  %std.spy(
+  %Clauses => hcumul-forall AllSubjects (s \
+  %  instance.declare-all s {findall-classes-for ML}) CCSL
+  %),
 /*
 %% New code: 
       % this should output all the candidate subjects too, as a new output argument.
@@ -712,11 +720,15 @@ derive-wrapper-instances Instance (wrapper-mixin WrapperMixin Subject Mixin)
         % name generation doesn't work because of dot occurrences  
         % mk_wrapper_instance_name Wrapper_Mixin Instance Nm,  
         % instance.declare-const "funq_instance_name" NewInstance {coq.term->arity Ty N0} _
+       coq.safe-dest-app Ty _Factory FArgs,
+       std.nth NParams FArgs WrapperSubject, 
        coq.say "REDIN!!!!!!!!!!!!!! OK", 
        coq.say "REDIN!!!!!!!!!!!!!! WrapperMixin = " WrapperMixin, 
        coq.say "REDIN!!!!!!!!!!!!!! NewInstance = " NewInstance, 
-
-       instance.declare-instance WrapperMixin _ NewInstance Clauses CSL
+       coq.say "REDIN!!!!!!!!!!!!!! WrapperSubject = " WrapperSubject, 
+
+
+       private.declare-instance WrapperMixin WrapperSubject NewInstance Clauses CSL
       )
 
 /*
@@ -739,9 +751,9 @@ derive-wrapper-instances Instance (wrapper-mixin WrapperMixin Subject Mixin)
 ].
 derive-wrapper-instances _ _ [] [].
 
-pred private.dec-inst-and-close i:factoryname, i:term, i:term, i:arity, i:id,
+pred dec-inst-and-close i:factoryname, i:term, i:term, i:arity, i:id,
   o:list prop, o:list (pair id constant). 
-private.dec-inst-and-close Factory TheType TheFactory TyWP SectionName Clauses CSL :- std.do! [
+dec-inst-and-close Factory TheType TheFactory TyWP SectionName Clauses CSL :- std.do! [
 
   private.declare-instance Factory TheType TheFactory Clauses CSL,
   % handle parameters via a section -- end
@@ -773,16 +785,18 @@ redirect-instances RealName Factory TheType TheFactory Body TyWP SectionName Cla
              if-verbose (coq.say {header} "closing instance section"),
              log.coq.env.end-section-name SectionName ),
           % we accumulate clauses now that the section is over
-          acc-clauses current Clauses0,
-          Clauses0 => private.derive-wrapper-instances Body W Clauses CSL
+          %acc-clauses current Clauses0,
+          %coq.say "REDIN!!!!!!! Clauses0 = " Clauses0,
+          %Clauses0 => 
+            private.derive-wrapper-instances TheFactory W Clauses CSL
           % private.declare-instance Factory TheType TheFactory Clauses CSL
         )  
         % there happens to be no wrapper, just treat it as a normal instance  
         (private.dec-inst-and-close Factory TheType TheFactory TyWP SectionName Clauses CSL)
      ]
     )
     % there can be no wrapper, just treat it as a normal instance  
-    (private.declare-instance Factory TheType TheFactory Clauses CSL)
+    (private.dec-inst-and-close Factory TheType TheFactory TyWP SectionName Clauses CSL)
    ) 
 ].