; 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))
(function TConst () Expr)
(let T (TConst))
(function 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))
(function CTConst () CExpr)
(let CT (CTConst))
(function CFConst () CExpr)
(let CF (CFConst))
(function CIfConst () CExpr)
(let CIf (CIfConst))
(function CAddConst () CExpr)
(let CAdd (CAddConst))
(function SConst () CExpr)
(let S (SConst))
(function KConst () CExpr)
(let K (KConst))
(function IConst () CExpr)
(let I (IConst))

;;;; Conversion functions
(function Comb (Expr) CExpr :cost 1000000)
(function 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)
(query-extract (Comb test))
(check (= test (N 3)))