gac/copy-list.scm

(define (mfilter p l)
  (cond ((null? l) '())
        ((p (car l))
         (cons (car l) (mfilter p (cdr l))))
        (else (mfilter p (cdr l)))))

(define (mfilter p l)
 (cond ((null? l) '())
       ((p (car l))
        (cons (car l) (mfilter p (cdr l))))
       (else (mfilter p (cdr l)))))

;; '(define (reverse l)
;;   (cond ((null? l) '())

(define (copy l)
   "copies the list l"
  (if (null? l) 
    '()
   (cons (car l) (copy (cdr l)))))

   "
   to copy a list l
we make a fresh cons that contains the head of l, and the copy of the tail of l.
if l is empty, the copy of l is '()

^- fully describing the algorithm.  Except we don't know yet whether `copy` works--since we haven't proven *before* that it works/exists, wer're doing that right now. We need to show that the above description is also complete from a coverage standpoint: does that cover all possible lengths of lists?

Can we show, that the use of `copy` will be less work, or in other words, *converge* towards a trivially solvable( or defined) case?

The process that's gonna happen will then only encounter cases that we have defined above.

So by logical deduction we know that the program will always work and give the right result.
   "


(define (reverse-append l l2)
  "copies the list l in reverse order, but adds l2 on the right
(y z) (x) -> (z y x)
() (x) -> (x)
(z) (y x) -> (z y x)
 l   l2
"
  (if (null? l)
      l2 ;; (begin (repl) l2)
      (reverse-append (rest l) (cons (first l) l2))))
"
reverse-append of the empty l is just l2 (nothing to be done).

reverse-append of a non-empty l is 
  the reverse of the rest of l, prepended to the first of l prepended to l2.

We cover all the cases:
- empty l
- non-empty l: since the recursive call is done with a shorter l it will hit the empty l case and is defined for non-empty case, thus,
reverse-append is defined for *all* lengths of l.

And it doesn't matter how long l2 is since we only ever add to it.
"

(define (reverse l)
  "copies the list l in reverse order"
  (reverse-append l '())))



;; (append (reverse l) l2)
;; (append-reverse l l2)