## Base interfaces & classes
(jvm;interface Function
               (: apply (-> [java.lang.Object] java.lang.Object)))

(jvm;class Tuple0 java.lang.Object
           [])
(jvm;class Tuple1 java.lang.Object
           [[java.lang.Object _1]])
(jvm;class Tuple2 java.lang.Object
           [[java.lang.Object _1] [java.lang.Object _2]])
(jvm;class Tuple3 java.lang.Object
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3]])
(jvm;class Tuple4 java.lang.Object
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3] [java.lang.Object _4]])
(jvm;class Tuple5 java.lang.Object
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3] [java.lang.Object _4]
            [java.lang.Object _5]])
(jvm;class Tuple6 java.lang.Object
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3] [java.lang.Object _4]
            [java.lang.Object _5] [java.lang.Object _6]])
(jvm;class Tuple7 java.lang.Object
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3] [java.lang.Object _4]
            [java.lang.Object _5] [java.lang.Object _6]
            [java.lang.Object _7]])
(jvm;class Tuple8 java.lang.Object
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3] [java.lang.Object _4]
            [java.lang.Object _5] [java.lang.Object _6]
            [java.lang.Object _7] [java.lang.Object _8]])

(jvm;class Variant java.lang.Object
           [[java.lang.String tag]])
(jvm;class Variant0 lux.Variant
           [])
(jvm;class Variant1 lux.Variant
           [[java.lang.Object _1]])
(jvm;class Variant2 lux.Variant
           [[java.lang.Object _1] [java.lang.Object _2]])
(jvm;class Variant3 lux.Variant
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3]])
(jvm;class Variant4 lux.Variant
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3] [java.lang.Object _4]])
(jvm;class Variant5 lux.Variant
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3] [java.lang.Object _4]
            [java.lang.Object _5]])
(jvm;class Variant6 lux.Variant
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3] [java.lang.Object _4]
            [java.lang.Object _5] [java.lang.Object _6]])
(jvm;class Variant7 lux.Variant
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3] [java.lang.Object _4]
            [java.lang.Object _5] [java.lang.Object _6]
            [java.lang.Object _7]])
(jvm;class Variant8 lux.Variant
           [[java.lang.Object _1] [java.lang.Object _2]
            [java.lang.Object _3] [java.lang.Object _4]
            [java.lang.Object _5] [java.lang.Object _6]
            [java.lang.Object _7] [java.lang.Object _8]])

## Base functions & macros
(def' lambda
  (lambda' _ tokens
      (lambda' _ state
          (let' output (case' tokens
                              (#Cons (#Form (#Cons self (#Cons arg args'))) (#Cons body #Nil))
                              (#Form (#Cons (#Ident "lambda'")
                                            (#Cons self
                                                   (#Cons arg
                                                          (#Cons (case args'
                                                                   #Nil
                                                                   body

                                                                   _
                                                                   (#Form (#Cons (#Ident "lux;lambda")
                                                                                 (#Cons (#Form (#Cons (#Ident "_") args'))
                                                                                        (#Cons body #Nil)))))
                                                                 #Nil))))))
                [(#Cons output #Nil) state]))))
(declare-macro lambda)

(def' def
  (lambda (_ tokens state)
    (let' output (case' tokens
                        (#Cons (#Ident name) (#Cons body #Nil))
                        (#Form (#Cons (#Ident "def'")
                                      (#Cons (#Ident name)
                                             (#Cons body #Nil))))

                        (#Cons (#Form (#Cons (#Ident name) args))
                               (#Cons body #Nil))
                        (#Form (#Cons (#Ident "def'")
                                      (#Cons (#Ident name)
                                             (#Cons (#Form (#Cons (#Ident "lux:lambda")
                                                                  (#Cons (#Form (#Cons (#Ident name) args))
                                                                         (#Cons body #Nil))))
                                                    #Nil)))))
          [(#Cons output #Nil) state])))
(declare-macro def)

(def (+ x y)
  (jvm;iadd x y))

(def (id x)
  x)

(def (print x)
  (jvm;invokevirtual java.io.PrintStream "print" [Object]
                     (jvm;getstatic System out) [x]))

(def (println x)
  (jvm;invokevirtual java.io.PrintStream "println" [Object]
                     (jvm;getstatic System out) [x]))

(def (fold f init xs)
  (do (print "fold ") (print init) (print " ") (println xs)
      (case' xs
             #Nil
             init
             
             (#Cons x xs')
             (let' init' (f init x)
                   (do (print "init': ") (println init')
                       (fold f init' xs')))
             #((fold f (f init x) xs'))#
             )))

(def (reverse list)
  (do (print "reverse ") (println list)
      (let' reversed (fold (lambda [tail head]
                             (do (print "reverse/0 ") (print "tail: ") (print tail) (print " head: ") (println head)
                                 (#Cons head tail)))
                           #Nil
                           list)
            (do (print "!reversed ") (println reversed)
                reversed))))

(def (list xs state)
  (let' xs' (reverse xs)
        (let' output (fold (lambda [tail head]
                             (do (print "tail: ") (print tail) (print " head: ") (println head)
                                 (#Form (#Cons (#Tag "Cons")
                                               (#Cons head
                                                      (#Cons tail #Nil))))))
                           (#Tag "Nil")
                           (do (print "REVERSED: ") (println xs')
                               xs'))
              (do (print "output: ") (println output)
                  [(#Cons output #Nil) state]))))
(declare-macro list)

(def (list+ xs state)
  (case' (reverse xs)
    #Nil
    [#Nil state]

    (#Cons last init')
    (let' output (fold (lambda [tail head]
                         (#Form (#Cons (#Tag "Cons")
                                       (#Cons head tail))))
                       last
                       init')
          [(#Cons output #Nil) state])))
(declare-macro list+)

(def (->pairs xs)
  (case' xs
    (#Cons x (#Cons y xs'))
    (#Cons [x y] (->pairs xs'))

    _
    #Nil))

(def (let tokens state)
  (case' tokens
         (#Cons (#Tuple bindings) (#Cons body #Nil))
         (let' output (fold (lambda [body binding]
                              (case binding
                                [label value]
                                (#Form (list (#Ident "let'") label value body))))
                            body
                            (reverse (->pairs bindings)))
               [(list output) state])))
(declare-macro let)

(def (++-list xs ys)
  (case' xs
    #Nil
    ys

    (#Cons x xs*)
    (#Cons x (++-list xs* ys))))

(def (map-list f xs)
  (case' xs
    #Nil
    #Nil

    (#Cons x xs*)
    (#Cons (f x) (map-list f xs*))))

#(
(def (untemplate-list untemplate tokens)
(case tokens
#Nil
(#Tag "Nil")

(#Cons token tokens')
(#Form (list (#Tag "Cons") (untemplate token) (untemplate-list untemplate tokens')))))

(def (untemplate token)
(case token
(#Bool elem)
(#Form (list (#Tag "Bool") (#Bool elem)))

(#Int elem)
(#Form (list (#Tag "Int") (#Int elem)))

(#Real elem)
(#Form (list (#Tag "Real") (#Real elem)))

(#Char elem)
(#Form (list (#Tag "Char") (#Char elem)))

(#Text elem)
(#Form (list (#Tag "Text") (#Text elem)))

(#Tag elem)
(#Form (list (#Tag "Tag") (#Text elem)))

(#Ident elem)
(#Form (list (#Tag "Ident") (#Text elem)))

(#Form (#Cons (#Ident "~") (#Cons unquoted #Nil)))
unquoted

(#Tuple elems)
(#Form (list (#Tag "Tuple") (untemplate-list untemplate elems)))

(#Form elems)
(#Form (list (#Tag "Form") (untemplate-list untemplate elems)))
))


## I/O
(def (print x)
(jvm;invokevirtual java.io.PrintStream "print" [Object]
(jvm;getstatic System out) [x]))

(def (println x)
(jvm;invokevirtual java.io.PrintStream "println" [Object]
(jvm;getstatic System out) [x]))

(def (' form)
(case form
(#Cons token #Nil)
(untemplate token)))
(declare-macro ')

(def (+ x y)
(jvm;iadd x y))

(def inc (+ 1))

(def length (fold (lambda' l (lambda' x (inc l))) 0))

(def (rem dividend divisor)
(jvm;irem dividend divisor))

(def (= x y)
(jvm;invokevirtual Object "equals" [Object]
x [y]))

(def (pairs list)
(case list
(#Cons x (#Cons y list*))
(#Cons [x y] (pairs list*))

_
#Nil))

(def (show x)
(jvm;invokevirtual Object "toString" []
x []))

(def (concat t1 t2)
(jvm;invokevirtual String "concat" [String]
t1 [t2]))

(def (range from to)
(if (= from to)
#Nil
(#Cons from (range (inc from) to))))

(def (text->list text)
(let' length (jvm;invokevirtual String "length" []
text [])
(map (lambda' idx
(jvm;invokevirtual String "charAt" [int]
text [idx]))
(range 0 length))))

(def (enumerate list)
(case (fold (lambda' state
(lambda' x
(case state
[idx list']
[(inc idx) (#Cons [idx x] list')])))
[0 #Nil]
list)
[_ list']
(reverse list')))

(def list-map #Nil)

(def (put key val map)
(case map
#Nil
(#Cons [key val] map)

(#Cons [?key ?val] map')
(if (= key ?key)
(#Cons [?key val] map')
(#Cons [?key ?val] (put key val map')))))

(def (get key map)
(case map
#Nil
#None

(#Cons [?key ?val] map')
(if (= key ?key)
(#Some ?val)
(get key map'))))

(def (show-kv kv)
(case kv
[?key ?val]
(fold concat "" (list "#" ?key " " (show ?val)))))

(def (interpose elem list)
(case list
(#Cons x (#Cons y list'))
(list+ x elem y (interpose elem list'))

_
list))

(def (show-list xs)
(case xs
#Nil
"#Nil"

(#Cons x xs')
(fold concat "" (list "(#Cons " (show x) " " (show-list xs') ")"))))

(defsig (Equal x)
(: = (-> x x Bool)))

(deftype Equal (All [x r] {#= (-> x x Bool) & r}))
(deftype Equal (All [x] {#= (-> x x Bool)}))
(deftype Equal (All [x] (Exists [r] {#= (-> x x Bool) & r})))

(defimpl (Equal Bool)
(def (= x y)
(case [x y]
[ true  true] true
[false false] true
_             false)))

(def Equal_Bool
(struct {#= [(-> Bool Bool Bool)
(lambda [x y] ...)]}))

(: (~ g!Equal) (Equal Bool))
(: (~ g!Equal) {#= (-> Bool Bool Bool)})
(def (~ g!Equal)
{#= (lambda [x y] ...)})

(def Equal_List
(lambda [Equal_x]
(struct {#= })))

(: Equal_List
(All [x] (-> (Equal x) (Equal (List x)))))

(defimpl (All [x]
(=> [(Equal x)]
(Equal (List x))))
(def (= xs1 xs2)
(case [xs1 xs2]
[#Nil #Nil]
true

[(#Cons x1 xs1') (#Cons x2 xs2')]
(and (Equal_x x1 x2) (= xs1' xs2')))))

(All [x]
(-> (Equal x) (Equal (List x))))

(EqualList EqualBool) => {#= ...}

(: ops (List (Exists [a] [(-> Text a) (-> a [])])))
(def ops (list [(lambda [_] 10) (lambda [_] [])]
[(lambda [_] "") (lambda [_] [])]))

(case ops
#Nil
[]

(#Cons [f1 f2] ops')
(f2 (f1 "E")))

(defsig (Add x)
(: + (-> x x x)))

(defimpl AddInt (Add Int)
#defs
(def (+ x y)
(jvm;ladd x y)))

(defimpl (Add Int)
(def (+ x y)
(jvm;ladd x y)))

(: adder (All [x] (=> [(Add x)]
(-> x (-> x x)))))
(def (adder by)
(lambda [x] (+ by x)))

(adder AddInt 1) -> (lambda [x] ((get@ #+ AddInt) 1 x))
adder == (lambda [impl]
(case impl
{#+ +}
(lambda [x] (+ by x))))

(: calc (All [v]
(-> (-> v Int)
(| (#Add Int Int) (#Mul Int Int) & v)
Int)))
(def (calc backup expr)
(case expr
(#Add x y) (+ x y)
(#Mul x y) (* x y)
else       (backup else)))

(defsig Yolo
(: lol? (-> Text Bool))
(: foo Int))

(defimpl Meme [Yolo]
(def (lol? _) true)
(def foo 10))

(defimpl Nyan [Yolo]
Meme
(def foo 20))

(list 1 2 3) == (#Cons 1 (#Cons 2 (#Cons 3 #Nil)))
(list+ 1 2 (list 3))

(defsig (Monoid a)
(: empty a)
(: ++ (BinaryOp a)))

(: concat (All [a]
(=> [(Monoid a)]
(-> (List a) a))))
(def (concat mon
xs)
(fold (:: mon #++) (:: mon #empty) xs))

(defstruct (Monoid Text)
(def empty "")
(def (++ x y)
...))

(defstruct (All [a]
(Monoid (List a)))
(def empty (list))
(def (++ xs ys)
(case xs
#Nil
ys

(#Cons x xs')
(#Cons x (++ xs' ys)))))

(: map (All [a b] (-> (-> a b) (List a) (List b))))

(defsig (Collection c)
(: add    (All [x] (-> x (c x) (c x))))
(: length (All [x] (-> (c x) Int))))

(defclass (Stack s)
(: push (All [x] (-> x (s x) (s x))))
(: pop  (All [x] (-> (s x) (s x))))
(: peek (All [x] (-> (s x) (Maybe x)))))

(deftype (BinaryOp t)
(-> t t t))

(defclass (Number n)
(: + (BinaryOp n))
(: - (BinaryOp n))
(: * (BinaryOp n))
(: / (BinaryOp n)))

(def (flip f)
(lambda [x y]
(f y x)))

(def (concat' xss)
(case (reverse xss)
#Nil
#Nil

(#Cons xs xss')
(fold (flip ++) xs xss')))

n + n*m

(with [AddInt]
(+ 10 20))

(:: AddInt (+ 10 20)) == ((get@ AddInt #=) 10 20)

(defimpl (Stack List)
(def (push x xs)
(#Cons x xs))

(def (pop xs)
(case xs
#Nil          #Nil
(#Cons _ xs') xs'))

(def (peek xs)
(case xs
#Nil        #None
(#Cons x _) (#Some x))))

(defsig (Functor f)
(: map (All [a b] (-> (-> a b) (f a) (f b)))))

(def (Functor f)
{#map  (All [a b] (-> (-> a b) (f a) (f b)))})

(defimpl ListFunctor (Functor List)
(def (map func fa)
(case fa
#Nil
#Nil

(list a fa')
(list (func a) (map func fa')))))

(implicit ListFunctor
(map inc (list 1 2 3)))

(defsig (=> [(Functor m)]
(Monad m))
(: return (All [x] (-> x (m x))))
(: bind (All [a b] (-> (m a) (-> a (m b)) (m b)))))



(#User {#name Text #age Int})
(deftype User {#name Text #age Int})
(deftype User (& (#name Text)
(#age Int)))
(deftype User (All [r]
(& (#name Text)
(#age Int)
++ r)))
(def User (#Record (list ["name" Text] ["age" Int])))

(let [thunk (... (+ 5 6))]
(! thunk))

(Thunk Int)


(deftype Int&Bool [Int Bool])

(deftype (List a)
(| #Nil
(#Cons a (List a))))

(defclass (Equal a)
(: = (-> a a Bool)))
==
(deftype (Equal a)
{#= (-> a a Bool)})

(def Equals
(All [a] {#= (-> a a Bool)}))

(defimpl EqualBool [(Equal Bool)]
(def (= x y)
(if x
y
(not y))))

(def ... {#= (lambda [x y] (if x
y
(not y)))})

(def Class (All [I]
(Exists [S] (& (#state S)
(#methods (I S))))))

(definterface Vector
(: translate (BinaryOp Vector)))

(def Vector (Some [Vector]
(& (#translate (BinaryOp v)))))

(defclass Vector2D
{#x Real, #y Real}
(def (new-Vector2D x y)
{#x x, #y y})
Vector
(def (translate self offset)
(-> self
(update@ #x + (get@ offset #x))
(update@ #y + (get@ offset #y)))))

(def Vector2D
{#translate (: (lambda [self offset]
(-> self
(update@ #x +real (get@ offset #x))
(update@ #y +real (get@ offset #y))))
(BinaryOp {#x Real, #y Real}))})

(: new-Vector2D (-> Real Real [{#x Real, #y Real} (@class Vector2D)]))
(def (new-Vector2D x y)
[{#x x, #y y} Vector2D])

(defsig (Vector v)
(: translate (BinaryOp v))
(: scale (BinaryOp v)))

(def Vector (All Vector [v]
(& (#translate (BinaryOp v))
(#scale (BinaryOp v)))))

(defstruct Vector2D (Vector [Real Real])
(def (translate [x1 y1] [x2 y2])
[(+ x1 x2) (+ y1 y2)])
(def (scale [x1 y1] [x2 y2])
[(* x1 x2) (* y1 y2)]))

(def Vector2D (: {#translate (lambda [[x1 y1] [x2 y2]]
[(+real x1 x2) (+real y1 y2)])
#scale (lambda [[x1 y1] [x2 y2]]
[(*real x1 x2) (*real y1 y2)])}
(Vector [Real Real])))

(deftype (Stream a)
(| (#Cons a (Thunk (Stream a)))))

(: iterate (All [a] (-> (-> a a) a (Stream a))))
(def (iterate f init)
(list init (... (iterate f (f init)))))

(def (take n stream)
(if (<= n 0)
#Nil
(case stream
(#Cons x stream')
(#Cons x (take (dec n) stream')))))

(deftype (Stream a)
(All [b] (-> (-> a (Stream a b) b) b)))

(: iterate (All [a] (-> (-> a a) a (Stream a))))
(def (iterate f init)
(lambda [k]
(k init (iterate f (f init)))))

(def (repeat x)
(lambda [k] (k x (repeat x))))

(def (take n stream)
(if (<= n 0)
#Nil
(stream (lambda [x stream']
(#Cons x (take (dec n) stream'))))))

(defsig (Comonad w)
(: extract (All [a] (-> (w a) a)))
(: extend (All [a b] (-> (w a) (-> (w a) b) (w b)))))

(defstruct Stream (Comonad w)
(def (extract stream)
(stream (lambda [x _] x)))
(def (extend w f)
...))

(: fibonacci (Stream Int))
(def fibonacci ((lambda fibonacci [a b]
(lambda [k] (k a (fibonacci b (+ a b)))))
0 1))

(gen fibonacci [a 0 b 1]
(yield a (fibonacci b (+ a b))))

(defgen fibonacci [a 0 b 1]
(yield a (fibonacci b (+ a b))))

(gen fibonacci [a 0 b 1]
(yield a [b (+ a b)]))

## The dual of do-notation should be be-notation

(deftype (Stream a)
(| (#Cons a (Thunk (Stream a)))))

(defstruct (Functor Stream)
(def (map f s)
(lambda [k]
(stream (lambda [x stream']
(f s))))))

(deftype (Tape a)
(| (#Index (Thunk (Stream a)) a (Thunk (Stream a)))))

(deftype (Area a)
(| (#Cursor (Tape a) (Surreal a))))

(def (ints offset n)
(#Index (... (iterate (lambda [n'] (- n' offset)) n))
n
(... (iterate (+ offset) n))))

(def (reals offset x)
(#Cursor (ints offset x)
(reals (/ offset 10) 0)))
)#

#(
(deftype (Session i o s)
  (All [s' r]
       (-> (-> i s' r)
           (-> o s [i s'])
           r))
  
  (All [s' s''] (-> (-> c s' [p s''])
                    (-> [] s [c s']) (Session c p s)
                    [p s'']))
  (All [] (-> (-> c s p)
              (-> p [])))
  (All [r] (-> c (Session r p s) p)))

(Session Int [] (Session Int (Session [] Int <END>)))

(bind (session' [])
      (lambda [x session']
        (bind (session' [])
              (lambda [y session'']
                (session'' (+ x y))))))

(defstruct SessionMonad
  (Monad Session)
  (def (return v)
    (lambda [k session]
      (k v session)))
  (def (bind step m-value)
    (lambda [k session]
      (let [[v session'] (m-value [] session)]
        (k (step v) session')))))

## Not really "do"; but oh, well...

(deftype <NIL>
  (| #Nil))

(deftype (HList h t)
  (| (#Cons h t)))

(deftype (Session c p s)
  (All [r] (-> c (-> p s r) r)))

(deftype (Session c p s)
  (-> (-> p s c) c))

(deftype (? r s)
  (Session r [] s))

(deftype (! w s)
  (Session [] w s))

(deftype #rec <END>
  (Session [] [] <END>))

(def <<
  (lambda [k session]
    (k [] session)))

(def (>> val)
  (lambda [k session]
    (session val k)))

(<$> << (>> 5))

(def (<$> consumer producer)
  (producer [] consumer))

(HList Int (HList Int <NIL>))

(<.> (? Int) (? Int) (! Int) <END>)
(def fn-session
  (do [x <<
       y <<]
    (>> (+ x y))))

(<.> (! Int) (! Int) (? Int) <END>)
(def call-session
  (do [_ (>> 5)
       _ (>> 10)]
    <<))

(<$> fn-session call-session)

(def <<
  (lambda [chan]
    (chan (lambda []))))

(def (>> value)
  (lambda [chan]
    (chan value)))
)#

## (defsig (Equal a)
##   (: = (-> a a Bool)))

## (: not= (All [a] (-> (Equal a) a a Bool)))
## (def (not= &Equal
##            x x)
##   (not (:: &Equal (= x x))))

## (defstruct Int
##   []
##   (Equal Int)

##   (def (= x y)
##     (zero? (- x y))))

## (defsig (Show a)
##   (: show (-> a Text)))

## (defstruct (ListShow x)
##   [&show (Show a)]
##   (Show (List a))
  
##   (def (show xs)
##     (<> "(" (interpose ", " (map (:: &show show) xs)) ")")))

## (def ListShow
##   (: (lambda [&show]
##         {#show (lambda show [xs]
##                   (<> "(" (interpose ", " (map (:: &show show) xs)) ")"))})
##      (-> (Show a) (Show (List a)))))