;;; (C) 2008-2009 Dr. Gergo ERDI <http://gergo.erdi.hu/>

(in-package :alef)

(parse-and-run
 `(,@*library*

   (declare/virtual (+ a) () (a a a))
   (declare/virtual (= a) () (a a bool))
   (declare/virtual (< a) () (a a bool))

   (deftype nat ()
     zero
     (succ nat))

   (define/override (+ nat) (x zero)     x)
   (define/override (+ nat) (x (succ y)) (succ (+ x y)))
   
   (declare one () nat)
   (define one () (succ zero))
   (define two () (succ one))
   (define three () (succ two))
   
   (define/override (= nat) (zero     zero)     true)
   (define/override (= nat) ((succ x) (succ y)) (=/nat x y))
   (define/override (= nat) (_        _)        false)
   
   (define/override (< nat) (_        zero)     false)
   (define/override (< nat) (zero     _)        true)
   (define/override (< nat) ((succ x) (succ y)) (< x y))
   
   (declare length/nat (a) ((list a) nat))
   (define length/nat (nil)         zero)
   (define length/nat ((cons _ xs)) (succ (length/nat xs)))
   
   (declare take/nat (a) ((list a) nat (list a)))
   (define take/nat (zero     _)           nil)
   (define take/nat (_        nil)         nil)
   (define take/nat ((succ k) (cons x xs)) (cons x (take/nat k xs)))

   (declare start () (bool))
   (define start ()
     (let ((zeros (cons zero zeros)))
       (</nat two (length/nat zeros))))))