prelude.zfd

(data Bool
      False
      True)

(data (Maybe a)
      Nothing
      (Just a))

(data (Either a b)
      (Left a)
      (Right b))

(data (List a)
      Nil
      (Cons a (List a)))

(data Nat
      Z
      (S Nat))

(defn (id x)
  ((forall a) (-> [a] a))
  x)

(defn (-top-reverse xs ys)
  ((forall a b) (-> [a b] Any))
  (if (is-nil xs)
      (: ys Any)
      (-top-reverse (cdr xs) (cons (car xs) ys))))

(defn (top-reverse xs)
  ((forall a) (-> [a] Any))
  (-top-reverse xs ()))

(defn (top-concat . xs)
  (-> Any Any)
  (top-foldr top-append () xs))

(defn (not p)
  (-> [Bool] Bool)
  (if p False True))

(defn (-and y)
  (-> [Any] Any)
  (case y
    (() (: 'True Any))
    ((x) x)
    ((x . xs) `(if ,x
                   ,(-and xs)
                   False))))

(defmacro (and . x)
  (-> Any Any)
  (-and x))

(defn (-or y)
  (-> [Any] Any)
  (case y
    (() (: 'False Any))
    ((x) x)
    ((x . xs) `(if ,x
                   True
                   ,(-or xs)))))

(defmacro (or . x)
  (-> Any Any)
  (-or x))

(defn (unsafe-from-just m)
  ((forall a) (-> [(Maybe a)] a))
  (unsafe-coerce (cadr m)))

(defn (maybe d f m)
  ((forall a b) (-> [b (-> [a] b) (Maybe a)] b))
  (if (top-eq m Nothing)
      d
      (f (unsafe-from-just m))))

(defn (curry f x)
  ((forall a b c) (-> [(-> (cons b a) c) b]
                      (-> a c)))
  (lambda y (apply f (cons x y))))

(defn (unsafe-head l)
  ((forall a) (-> [(List a)] a))
  (unsafe-coerce (cadr l)))

(defn (unsafe-tail l)
  ((forall a) (-> [(List a)] (List a)))
  (unsafe-coerce (caddr l)))

(defn (nat-prev i)
  (-> [Nat] Nat)
  (if (top-eq i Z)
      i
      (unsafe-coerce (cadr i))))

(defn (unsafe-top-nth n l)
  (-> [Nat Any] Any)
  (if (top-eq n Z)
      (car l)
      (unsafe-top-nth (nat-prev n) (cdr l))))

(defn (-unsafe-top-nth n l)
  (-> [Nat Any] Any)
  (if (top-eq n Z)
      (: `(car ,l) Any)
      (-unsafe-top-nth (nat-prev n)
                       `(cdr ,l))))

(defn (-top-map-index f l i)
  (-> [(-> [Nat Any] Any) Any Nat] Any)
  (if (is-nil l)
      (: () Any)
      (cons (f i (car l))
            (-top-map-index f (cdr l) (S i)))))

(defn (top-map-index f l)
  (-> [(-> [Nat Any] Any) Any] Any)
  (-top-map-index f l Z))

(defn (top-zip xs ys)
  (-> [Any Any] Any)
  (if (or (is-nil xs) (is-nil ys))
      (: () Any)
      `((,(car xs) . ,(car ys))
        ,@(top-zip (cdr xs) (cdr ys)))))

(defn (-apply-alist f ns l)
  (-> [Any Any Any] Any)
  `(,f ,@(top-map (lambda (n) (car (alist-lookup n l))) ns)))

(defn (-record n ts c fs ks)
  (-> [Symbol Any Symbol Any Any] Any)
  (let ((ps (top-map data-arg-name ts))
        (mk-field (lambda (i f)
                    `(defn (,(car f) r)
                       ,(-forall ps
                                 `(-> [(,n ,@ps)] ,(cadr f)))
                       (unsafe-coerce ,(-unsafe-top-nth i '(cdr r))))))
        (xs (top-map cadr fs))
        (g (capture (symbol-concat '_ c )))
        (ks' (if (is-nil ks)
                 (top-map (lambda (f) (car f)) fs)
                 ks)))
    `(begin
       (data ,(cons n ts)
             ,(cons g xs))
       (defmacro (,c . l)
         (-> Any Any)
         (-apply-alist ',g ',ks' l))
       ,@(top-map-index mk-field fs))))

(def record
     (-> [(cons Symbol Any) (cons Symbol Any)] Any)
     (macro d
       (-record (fst (fst d))
                (snd (fst d))
                (fst (fst (snd d)))
                (snd (fst (snd d)))
                ())))

(defn (-class n ts fs)
  (-> [Symbol Any Any] Any)
  (let ((gs (unsafe-gensyms ts))
        (gm (top-zip (top-map car fs) gs))
        (ts' (top-map data-arg-name ts)))
    `(begin
       ,(-record n
                 ts
                 (capture (symbol-concat 'Mk n))
                 (top-map (lambda (f)
                            (cons (alist-lookup (car f) gm)
                                  (cdr f)))
                          fs)
                 (top-map (lambda (f) (car f)) fs))

       ,@(top-map
          (lambda (f)
            (let ((ps (unsafe-gensyms (cdadr f))))
              `(def ,(car f)
                    ,(-forall ts'
                              `(=> (,n ,@ts')
                                   ,(cadr f)))
                    (implicit r
                      (lambda ,ps
                        ((,(alist-lookup (car f) gm) r)
                         ,@ps))))))
          fs))))

(defmacro (class . d)
  (-> (cons (cons Symbol Any) Any) Any)
  (-class (fst (fst d)) (cdar d) (cdr d)))

(defn (-instance n t fs)
  (-> [Symbol Any Any] Any)
  `(def ,(unsafe-gensym)
        ,[n t]
        ,(cons (symbol-concat 'Mk n)
               fs)))

(defmacro (instance . d)
  (-> (cons [Symbol Any] Any) Any)
  (-instance (fst (fst d))
             (fst (snd (fst d)))
             (cdr d)))

(class (Eq a)
       (== (-> [a a] Bool)))

(instance (Eq ())
          (== (lambda (_ _) True)))

(instance (Eq Symbol)
          (== symbol-eq))