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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102

; Substitution in lambda-calculus via S/K/I combinators. Extremely slow, as
; abstraction elimination does not pay attention to whether variables are free
; in an expression before introducing 'S'.
;
; Provides an example of how to implement substitution by embedding in a
; 'richer' data-type and then mapping back to syntax.

(datatype Expr
    (Var String :cost 100)
    (Abs String Expr)
    (If Expr Expr Expr)
    (N i64)
    (Add Expr Expr)
    (App Expr Expr))
(constructor TConst () Expr)
(let $T (TConst))
(constructor FConst () Expr)
(let $F (FConst))


; (\x. (if x then 0 else 1) + 2) false
(let $test
    (App 
        (Abs "x" (Add (If (Var "x") (N 0) (N 1)) (N 2))) $F))

(datatype CExpr
    (CVar String :cost 10000) ; (variables that haven't been eliminated yet)
    (CAbs String CExpr :cost 10000) ; (abstractions that haven't been eliminated yet)
    (CN i64)
    (CApp CExpr CExpr))
(constructor CTConst () CExpr)
(let $CT (CTConst))
(constructor CFConst () CExpr)
(let $CF (CFConst))
(constructor CIfConst () CExpr)
(let $CIf (CIfConst))
(constructor CAddConst () CExpr)
(let $CAdd (CAddConst))
(constructor SConst () CExpr)
(let $S (SConst))
(constructor KConst () CExpr)
(let $K (KConst))
(constructor IConst () CExpr)
(let $I (IConst))

;;;; Conversion functions
(constructor Comb (Expr) CExpr :cost 1000000)
(constructor Uncomb (CExpr) Expr)    
(rewrite (Comb (Uncomb cx)) cx)
(rewrite (Uncomb (Comb x)) x)

; Mechanical mappings back and forth.
; Note: we avoid resugaring S/K/I
(rule ((= x (N n))) ((union (Comb x) (CN n))))
(rule ((= cx (CN n))) ((union (Uncomb cx) (N n))))
(rule ((= x $T)) ((union (Comb x) $CT)))
(rule ((= cx $CT)) ((union (Uncomb cx) $T)))
(rule ((= x $F)) ((union (Comb x) $CF)))
(rule ((= cx $CF)) ((union (Uncomb cx) $F)))

(rule ((= x (If c t f)))
    ((union (Comb x) (CApp (CApp (CApp $CIf (Comb c)) (Comb t)) (Comb f)))))
(rule ((= cx (CApp (CApp (CApp $CIf cc) ct) cf)))
    ((union (Uncomb cx) (If (Uncomb cc) (Uncomb ct) (Uncomb cf)))))

(rule ((= x (Add l r)))
    ((union (Comb x) (CApp (CApp $CAdd (Comb l)) (Comb r)))))
(rule ((= cx (CApp (CApp $CAdd cl) cr)))
    ((union (Uncomb cx) (Add (Uncomb cl) (Uncomb cr)))))
(rule ((= x (App f a))) ((union (Comb x) (CApp (Comb f) (Comb a)))))

(rule ((= x (Var v))) ((union (Comb x) (CVar v))))
(rule ((= x (Abs v body))) ((union (Comb x) (CAbs v (Comb body)))))

;;;; Abstraction Elimination 
(rewrite (CAbs v (CVar v)) $I)
; Hacks, could be replaced by !free computation.
(rewrite (CAbs v1 (CVar v2)) (CApp $K (CVar v2)) 
    :when ((!= v1 v2)))
(rewrite (CAbs v (CN n)) (CApp $K (CN n)))
(rewrite (CAbs v $CT) (CApp $K $CT))
(rewrite (CAbs v $CF) (CApp $K $CF))
(rewrite (CAbs v $CIf) (CApp $K $CIf))
(rewrite (CAbs v $CAdd) (CApp $K $CAdd))
(rewrite (CAbs v (CApp x y)) (CApp (CApp $S (CAbs v x)) (CAbs v y)))
; May be needed for multiple nested variables
(rewrite (CAbs v (CApp $K (CVar v))) $K)

;;;; Primitive Evaluation rules (letd on "surface syntax")
(rewrite (If $T t f) t)
(rewrite (If $F t f) f)
(rewrite (Add (N n) (N m)) (N (+ n m)))

;;;; Substitution Rules (letd on the combinator representation)
(rewrite (CApp $I cx) cx)
(rewrite (CApp (CApp $K cx) cy) cx)
; Without demand, this can cause an explosion in DB size.
(rewrite (CApp (CApp (CApp $S cx) cy) cz) (CApp (CApp cx cz) (CApp cy cz)))

(run 11)
(extract (Comb $test))
(check (= $test (N 3)))