[Axiom-developer] Re: defintrf bug

[Stephen Wilson]

Hello Tim,

address@hidden writes:
> Stephen,
> 
> (|Record|...) macroexpands into (|Record0|....)
> (|:|...) macroexpands into (CONS...)
> 
> 
> 
> 
> 
> in OPTPROB.nrlib/code.lsp
> 
>     (ELT (|Record| (|:| |lfn| 
>                         (|List| (|Expression| (|DoubleFloat|))))
>                    (|:| |init| (|List| (|DoubleFloat|)))))
> 
> was not expanded. Perhaps we need to do a macroexpand-all?

I noticed similar issue with D01AGNT.  But this case is more
interesting, as it is showing we can get these unquoted union/record
tags via different paths then just through mkUnionFunList.

> in DFINTTLS.nrlib/code.lsp, the source line in defintrf.spad, line 90
> where 
>   Z ==> Integer
>   Q ==> Fraction Z
>   B ==> Boolean
>   REC ==> Record(left:Q, right:Q)
>   keeprec? : (Q,REC) -> B
>    
>   keeprec?(a, rec)   == (a > rec.right) or (a < rec.left)
> 
> the code used to read:
> (|DFINTTLS;keeprec?|
>   (QCAR (PROG2 (LETT #0# (QREFELT $$ 3) NIL (QCDR #0#)
> 
> becomes
> 
> (|DFINTTLS;keeprec?|
>   (QCAR (PROG2 (LETT #0# (QREFELT $$ 1) NIL (QCDR #0#)
> 
> I have no idea why the index changed. And in the same file

Im at a loss to explain this as well.

> 
>    (|Record| 
>      (|:| (QREFELT $$ 2) (|Fraction| (|Integer|)))
>      (|:| (QREFELT $$ 1) (|Integer)))
> expands to
>    (|Record0|
>      (LIST (CONS '|endpoint|
>                  (|Fraction| (|Integer|)))
>            (CONS '|dir| (|Integer|))))
> 
> this seems like a bug in the algebra code to me.
> The function keeprec? expects a REC record with left and right indices
> but "endpoint" and "dir" are the indices of a REC2:
>   REC2 ==> Record(endpoint:Q, dir:Z)
> so it doesn't seem valid to call keeprec? on a REC2 construct.

Nice catch.  But is this a bug in the algebra?

The call:

      select_!(keeprec?(i.halfinf.endpoint, #1), l) 

Seems well typed. We have:

     keeprec?    : (Q, REC) -> B

     i.halfinf.endpoint is of type Q (Fraction Integer)

     "l" should have inferred to be of type List REC, given its
     definition "l := realZeros p" (which is comming from
     RealZeroPackage, I belive), and so the second argument type of
     keeprec? is satisfied.

Am I missing a step?  This looks like another compiler bug to me, that
REC2 is being confused for REC.

> Ultimately I think the algorithm is wrong. I think that even though
> the signature for keeprec? is properly matched in the call, and the
> shape of the record is the same yet the accessor names are wrong.
> 
> I'm still checking the other examples and they seem to be expanding
> correctly. I'm not sure that your patch is needed.

Given these insights, I feel the patch is not fully correct.  It
appears to solve the original bug, but not the general problem. 

Main issue remains: Types which involve (|:| field Type) terms like
Record and Union have `field' appear unquoted, foiling
compWithMappingMode.  

Perhaps the use of macroexpand-all at all points where these
expressions are generated would work as a general solution, but I have
doubts that such an experiment would suceed.

I will try again with my original idea to make compWithMappingMode
smarter, to lift only those identifiers which it can prove are bound.

Im not sure if the posting of a `patch for testing' was a worthwhile
activity.  Im certain I would have locally rejected the patch in time,
but your observations have been a great help.  Comments?

Do the documentation bits of the patch look OK to you? I can post a
revised patch containing a (possibly improved) chunk of documentation.


Thanks,
Steve