Re: Greetings

[Matthias Felleisen <matthias@ccs.neu.edu>]

Chris, 

Spidey is unable to prove the correctness of each data access because you
measure the null-ness of cur with (>= len n). Your len parameter for
choose-internal just keeps track of the length of avail and there is no
need for that. Just test whether you have elements left on your list: 

(define (choose m lst)
  (define choose-internal 
    (lambda (n  in-use  avail)
      (cond [(null? avail) nulp]
	[(= 1 n)
	 (visit (cons (car avail) in-use))
	 (choose-internal n in-use (cdr avail))]
	[else (let loop ([cur avail])
		(unless (pair? cur)
		  (choose-internal (sub1 n)
		    (cons (car cur) in-use)
		    (cdr cur))
		  (loop (cdr cur))))])))
  (if (> m 0)
      (choose-internal m null lst) 
      #f))

Now run Spidey and compare.

Your mistake is typical for someone who comes from a language where
everything is an array. The slogan is

 FORGET INDICES and LENGTHs!

They are hardly ever necessary. Note that n is NOT an index.

Furthermore, I suggest that you separate output and result. Just write a
function that creates a list of all the choices and then choose to print
them or choose to work with them in some other functions. Separate the
model from the view: 

(define (choose-new m lst)
  (letrec ([internal 
            (lambda (n  in-use  avail)
              (cond [(null? avail) null]
                    [(= 1 n)
                     (cons (cons (car avail) in-use)
                           (internal n in-use (cdr avail)))]
                    [else 
                     (let loop ([cur avail])
                       (if (pair? cur)
                           (append 
                            (internal (sub1 n)
			              (cons (car cur) in-use)
				      (cdr cur))
                            (loop (cdr cur)))
                           null))]))])
    (if (> m 0)
        (internal m null lst) 
        #f)))

(for-each visit (choose-new n l))

Finally, I'd like to think that the accumulator in-use is probably
something we can do recursively and properly, but I am running out
of time.

-- Matthias