(datatype expr 
    (Num i64)
    (Add expr expr)
    (Max expr expr))
(rewrite (Add (Num a) (Num b)) (Num (+ a b)))
(rewrite (Max (Num a) (Num b)) (Num (max a b)))

; List of (weight, value) pairs
(datatype objects
    (Cons i64 i64 objects))
(function NilConst () objects)
(let Nil (NilConst))

; Given a capacity and a list of objects, finds the maximum value of a
; collection of objects whose total weight does not exceed the capacity.
(function Knap (i64 objects) expr)

(rule ((= f (Knap capacity (Cons weight val rest))) (<= weight capacity))
      ((union (Knap capacity (Cons weight val rest))
            (Max
                (Add (Num val) (Knap (- capacity weight) rest))
                (Knap capacity rest)))))

(rule ((= f (Knap capacity (Cons weight val rest))) (> weight capacity))
      ((union (Knap capacity (Cons weight val rest))
            (Knap capacity rest))))

(rule ((= f (Knap capacity Nil)))
      ((union (Knap capacity Nil) (Num 0))))

(let test1 (Knap 13 (Cons 5 5 (Cons 3 3 (Cons 12 12 (Cons 5 5 Nil))))))

(let test2 (Knap 5 (Cons 6 6 Nil)))

(let test3 (Knap 5 (Cons 1 1 (Cons 1 1 (Cons 1 1 Nil)))))

(let test4 (Knap 15 (Cons 12 40 (Cons 2 20 (Cons 1 20 (Cons 1 10 (Cons 4 100 Nil)))))))

; turn a (Num n) into n
(function Unwrap (expr) i64)
(rule ((= x (Num n))) ((set (Unwrap (Num n)) n)))

(run 100)

(check (= test1 (Num 13)))