hd-rev-mklist-dependent.scm

(module list
  (provide
   [reverse ([l : (listof int?)]
             . -> .
             (and/c (listof int?)
                    (λ (r) (and (equal? (empty? l) (empty? r))
                                (equal? (cons? l) (cons? r))))))]
   [mk-list ([n : int?]
             . -> .
             (and/c (listof int?)
                    (λ (l) (if (zero? n) (empty? l) (cons? l)))))]
   [append ([l : (listof int?)]
            [r : (listof int?)]
            . -> .
            (and/c (listof int?)
                   (λ (a)
                     (cond
                       [(or (cons? l) (cons? r)) (cons? a)]
                       [(and (empty? l) (empty? r)) (empty? a)]
                       [else 'admit]))))])
  (define (reverse xs)
    (if (empty? xs) empty
        (append (reverse (cdr xs)) (cons (car xs) empty))))
  (define (mk-list n)
    (if (zero? n) empty
        (cons n (mk-list (- n 1)))))
  (define (append l r)
    (if (empty? l) r
        (cons (car l) (append (cdr l) r)))))

(module main
  (provide [main (int? . -> . int?)])
  (require list)
  (define (main len)
    (let [xs (mk-list len)]
      (if (positive? len)
          (car (reverse xs))
          0))))

(require main list)
(amb (reverse •)
     (mk-list •)
     (append • •))