egglog 2.0.0

egglog is a language that combines the benefits of equality saturation and datalog. It can be used for analysis, optimization, and synthesis of programs. It is the successor to the popular rust library egg.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

(datatype VarT)
(datatype Term)
(constructor App (Term Term) Term)
(constructor Lam (VarT Term) Term)
(constructor Var (VarT) Term)
(constructor Let (VarT Term Term) Term)
(constructor Add (Term Term) Term)
(constructor Num (i64) Term)
(constructor CaseSplit (Term Term Term) Term)
(constructor Cons (Term Term) Term)
(constructor Nil () Term)
(constructor 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))))
(constructor 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)