[Agda] Re: Issue 1050 in agda: how to reduce type check cost

[Sergei Meshveliani]

On Sun, 2014-02-09 at 07:20 +0000, agda at googlecode.com wrote:
> Comment #4 on issue 1050 by ulf.nor... at gmail.com: how to reduce type check  
> cost
> http://code.google.com/p/agda/issues/detail?id=1050
> 
> You can use C-c C-h to compute the type of a suitable function to use  
> instead of with. So for the |x-rem-x you'd do something like
> 
> ∣x-rem-x : ∀ x y → y ∣ (x - (eucRem x y))
> ∣x-rem-x x y = {! |x-rem-x-helper (y ≟ 0#) !}  -- hit C-c C-h in the hole
> 

I copy my reply to  agda at lists.chalmers.se
because 
* my replying (by the "Reply" button) to comments from the bug tracker
(via  agda at googlecode.com) usually are returned by
"your message is not a reply to ...", 
-- so that I prefer to insert a reply comment directly to the tracker, 

* I cannot add my reply to this #issue, because  #1050 is merged to
#1047,  and #1047 does not show the text from #1050
(I have only e-mails).

I try

  ∣x-rem-x x y = {! helper (y ≟ 0#) !} 

  C-c C-l   -- "loading" a module
  C-c C-h   -- see the hole type    

(right?). The interactive responds

-----------------------------------------
helper : ∀ {α α=} {upGCD : UpGCDRing α α=} { : PreEucRing}
           {x y
            : DecSetoid.Carrier
              (AlgClasses1.UpDSet.decSetoid
               (AlgClasses1.UpMagma.upDSet
                (AlgClasses1.UpSemigroup.upMagma
                 (AlgClasses2.UpMonoid.upSemigroup
                  (AlgClasses2.UpGroup.upMonoid
                   (UpCommutativeGroup.upGroup
                    (AlgClasses3.UpRingoid.+upCommGroup
                     (AlgClasses3.UpRing.upRingoid
                      (AlgClasses3.UpRingWithOne.upRing
                       (UpCommutativeRing.upRingWithOne
                        (UpIntegralRing.upCommutativeRing
                         (UpGCDRing.upIntegralRing upGCD))))))))))))}
           (w
            : Dec
              ((AlgClasses1.UpDSet.decSetoid
                (AlgClasses1.UpMagma.upDSet
                 (AlgClasses1.UpSemigroup.upMagma
                  (AlgClasses2.UpMonoid.upSemigroup
-------------------------

-- at this point the emacs lower window ends,
and I need to find in  emacs  of how to see it in full, how to switch to
the lower window ...

And there arises a question on a 13 record level trace in this report. 

In the code, this  Carrier  in the top line is obtained by 

  gR = UpGCDRing.gcdRing upGCD
  open GCDRing gR using (Carrier ...)

This is because each   Up<class>  exports  <class>,  and  <class> 
reexports by "open public" the export of all its nested classes.  

Now, the Agda interactive prints all the trace of this import chain, but
it chooses only the "Up" levels  
(this can be checked by looking into the records in AlgClasses*.agda). 

I doubt 
1) about the way Agda interactive prints the record import trace
   (has it an option for how to print the import trace?),
2) of whether I need to try another way of setting  "open public"  in 
   my algebra records.

Thanks,

------
Sergei