(datatype VarT)
(datatype Term)
(function App (Term Term) Term)
(function Lam (VarT Term) Term)
(function Var (VarT) Term)
(function Let (VarT Term Term) Term)
(function Add (Term Term) Term)
(function Num (i64) Term)
(function CaseSplit (Term Term Term) Term)
(function Cons (Term Term) Term)
(function Nil () Term)
(function V (String) VarT)
(sort StringSet (Set VarT))
(function freer (Term) StringSet :merge (set-intersect old new))

;;(rule ((= e (App e1 e2))
;;       (= (freer e1) fv1)
;;       (= (freer e2) fv2))
;;      ((set (freer e) (set-union fv1 fv2))))

(rule ((= e (App e1 e2))
       (= fvar1 (freer e1))
       (= fvar1 fv1)
       (= fvar2 (freer e2))
       (= fvar2 fv2))
     ((set (freer e) (set-union fv1 fv2))))
(rule ((= e (Var v))) ((set (freer e) (set-insert (set-empty) v))))
(function sum () Term :cost 1000)
(union (sum) (Lam (V "xs") (CaseSplit (Var (V "xs")) (Num 0) (Lam (V "x") (Lam (V "xs'") (Add (Var (V "x")) (App (sum) (Var (V "xs'")))))))))
(set (freer (sum)) (set-empty))
(run 100)