[Gcl-devel] Re: Random noise

[Camm Maguire]

Greetings, and thanks!

Robert Boyer <address@hidden> writes:

> All of the following I'm sure you know.
> 
> ACL2 does not permit a user to define a function that
> sometimes returns 2 values and sometimes returns 1.  So,

Thanks!  Did not know this.

> ideally proclamation analysis for GCL will recognize that an
> ACL2 function has a known return arity and thereby avoid the
> necessity of passing around this number of values returned
> stuff altogether.  Just pass the values back trusting that
> whoever called knows how many to expect.
> 

OK, so here's the nub of the issue -- what return types can we use to
distinguish between the following two functions:

(defun foo (x y) (if x (values y y y) (values y y)))
(defun bar (x y) (values y y))

, and what are the results of the operations type-and and type-or upon
them?  

I see two possibilities:

foo -> (or (values t t t) (values t t))
bar -> (values t t)
 (or (values t t t) (values t t)) -> (or (values t t t) (values t t))
(and (values t t t) (values t t)) ->  nil

foo -> (values t t t)
bar -> (values t t)
 (or (values t t t)  (values t t)) ->  (values t t t)
(and (values t t t)  (values t t)) ->  (values t t)

We've winded up implementing latter for various reasons I can go into,
and which need not be final by any means.  But it appears that acl2
constrains itself in such a way as to fit into the former, which then
becomes more useful as it indicates exactly how many values are
returned, not just the maximum.  Given the latter semantics for the
sake of argument, might there be some other construct which could be
used to regain the exact arity, e.g.

(values t t t) = (or (arity) (arity t) (arity t t) (arity t t t))?

> > The callee must make sure to always set the maximum number of
> > values, otherwise junk will be left in MVloc.
> 
> Not true, if the callee knows that the caller is smart
> enough to know never to look at the "junk".
> 

Here's a bug I just fixed in the GCL debugger (not yet committed which
illustrates what I was trying to say:

(defun next-stack-frame (ihs  &aux line-info li i k na)
  (cond
   ((fb < ihs *ihs-base*) (mv-values nil nil nil nil nil))
   (t (let (fun)
        ;; next lower visible ihs
        (mv-setq (fun i) (get-next-visible-fun  ihs))
        (setq na fun)
        (cond
         ((and
           (setq line-info (get fun 'line-info))
           (do ((j (f + ihs 1) (f - j 1))
                (form ))
               ((<= j i) nil)
             (setq form (ihs-fun j))
             (cond ((setq li (get-line-of-form (ihs-fun j) line-info))
                    (return-from next-stack-frame 
                                 (mv-values
                                  i fun li
                                  ;; filename
                                  (car (aref line-info 0))
                                  ;;environment
                                  (list (vs (setq k (ihs-vs j)))
                                        (vs (1+ k))
                                        (vs (+ k 2)))
                                  )))))))
         ((special-form-p na) nil)
         ((get na 'dbl-invisible))
         ((fboundp na)
          (mv-values i na nil nil
                     (if (ihs-not-interpreted-env i)
                         nil
                       (let ((i (ihs-vs i)))
                         (list (vs i) (vs (1+ i)) (vs (f + i 2)))))))
         ((mv-values nil nil nil nil nil)))))))

I've just added the last branch, without which the caller to
next-stack-frame could and did read values set by some other
function. 

> > There is no way for the caller to tell how many values were set.
> 
> The caller knows exactly how many values will be set in the
> ACL2 case.
> 
> > This seems designed for the case where both the callee and
> > the caller know that exactly n values are placed in the
> > stack under all circumstances.
> 
> This is the only case that arises in ACL2.
> 

OK, but GCL has to both be optimal for ACL2 and float other lisp
programs as well.

> > one might want to support functions which might return
> > different numbers of values under different circumstances
> > in a general implementation.
> 
> Well obviously if one is going to support ANSI Common Lisp,
> such functions do exist and are nice in some cases.  But
> someone needs to pay for the lack of certainty about the
> number of return values in some cases, and it is not clear
> that everybody needs to pay that cost at all times.  It
> would be terribly sad, for example, if such primitives as
> 'car' were slowed down just to alert the world that
> precisely one value was returned.
> 

I'm thinking of inventing the arity type along the lines of your
earlier suggestion and have the compiler infer and propagate these.
In such a case of known 'arity' we might as well write shelter mv or
equivalent straight from the compiler.

> > One wants to avoid writes wherever possible.
> 
> It really depends so much on where you are writing to.  If

I meant ram.  Cache-line pollution is my guess for the dominant cost,
incurred in, for example, presetting all mv values to nil before
really setting what is to be set -- this is much worse than retrieving
the number of values set by the callee and only setting the remaining
to nil.

Take care,

> you are writing to a register, it can be done in a
> nanosecond, maybe in parallel with doing other things, hence
> really in no time at all.  If you are writing to a paper
> tape, you'll need to build a paper tape factory.
> 
> Bob
> 
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah