;;;;;;;;;;;;;;;;
;; Abstact Domain
;;;;;;;;;;;;;;;;

; Top means it can be an arbitrary value
(datatype Val (I i64))
(function TopConst () Val)
(let Top (TopConst))
(function TrueConst () Val)
(let True (TrueConst))
(function FalseConst () Val)
(let False (FalseConst))
(relation Bool (Val))
(Bool True)
(Bool False)

(function merge-val (Val Val) Val)

(rewrite (merge-val Top x) Top)
(rewrite (merge-val x Top) Top)
(rewrite (merge-val True  False) Top)
(rewrite (merge-val True  (I x))   Top)
(rewrite (merge-val False True)  Top)
(rewrite (merge-val False (I x))   Top)
(rewrite (merge-val (I x) (I y)) Top :when ((!= x y)))
(rewrite (merge-val x x) x)

(function add-val (Val Val) Val)

(rewrite (add-val Top x) Top)
(rewrite (add-val x Top) Top)
(rewrite (add-val True x) Top)
(rewrite (add-val False x) Top)
(rewrite (add-val x True) Top)
(rewrite (add-val x False) Top)
(rewrite (add-val (I x) (I y)) (I (+ x y)))

(function eq-val (Val Val) Val)

(rewrite (eq-val Top x) Top)
(rewrite (eq-val x Top) Top)
(rewrite (eq-val True False) False)
(rewrite (eq-val True (I x)) False)
(rewrite (eq-val False True) False)
(rewrite (eq-val False (I x)) False)
(rewrite (eq-val (I x) True) False)
(rewrite (eq-val (I x) False) False)
(rewrite (eq-val x x) True)

(datatype VarT (V String))
(datatype Loc (L i64))
(datatype Exp
    (Add VarT VarT)
    (Eq VarT VarT)
    (Var VarT)
    (Const Val))
(datatype ProgStmt
    (Ass VarT Exp)
    (If VarT Loc Loc)
    (Goto Loc)
    (Call VarT))
(function EndConst () ProgStmt)
(let End (EndConst))
(function Prog (Loc) ProgStmt)
(relation RProg (Loc ProgStmt))

(function const-prop (Loc VarT) Val :merge (merge-val old new))

;;;;;;;;;;;;;;;;
;; ASS Case
;;;;;;;;;;;;;;;;

;; PROPAGATION

; propagate x = k
(rule (
    (RProg (L li) (Ass x (Const k)))
)(
    (set (const-prop (L (+ li 1)) x) k)
))

; propagate x = a + b (non-constant)
(rule (
    (RProg l (Ass x (Add x1 x2)))
    (= v1 (const-prop l x1))
    (= v2 (const-prop l x2))
    (= l (L li))
)(
    (set (const-prop (L (+ li 1)) x) (add-val v1 v2))
))

; propagate x = a == b
(rule (
    (RProg l (Ass x (Eq x1 x2)))
    (= v1 (const-prop l x1))
    (= v2 (const-prop l x2))
    (= l (L li))
)(
    (set (const-prop (L (+ li 1)) x) (eq-val v1 v2))
))

; propagate other vars
(rule (
    (RProg (L li) (Ass (V x) e))
    (= val (const-prop (L li) (V y)))
    (!= x y)
)(
    (set (const-prop (L (+ li 1)) (V y)) val)
))

;; TRANSFORMATION 

; generate demand for biop
(rule (
    (= (Prog l) (Ass x (Add x1 x2)))
    (= v1 (const-prop l x1))
    (= v2 (const-prop l x2))
)(
    (add-val v1 v2)
))

(rule (
    (= (Prog l) (Ass x (Eq x1 x2)))
    (= v1 (const-prop l x1))
    (= v2 (const-prop l x2))
)(
    (eq-val v1 v2)
))

; replace x = a + b (constant)
(rule (
    (= (Prog l) (Ass x (Add x1 x2)))
    (= (I val) (add-val (const-prop l x1)
                        (const-prop l x2)))
)(
    (RProg l (Ass x (Const (I val))))
))

; replace x = a + b (non-contant)
(rule (
    (= (Prog l) (Ass x (Add x1 x2)))
    (= Top (add-val (const-prop l x1)
                      (const-prop l x2)))
)(
    (RProg l (Ass x (Add x1 x2)))
))

; replace x = a == b (constant)
(rule (
    (= (Prog l) (Ass x (Eq x1 x2)))
    (= b (eq-val (const-prop l x1) (const-prop l x2)))
    (Bool b)
)(
    (RProg l (Ass x (Const b)))
))

; replace x = a == b (non-constant)
(rule (
    (= (Prog l) (Ass x (Eq x1 x2)))
    (= Top (eq-val (const-prop l x1) (const-prop l x2)))
)(
    (RProg l (Ass x (Eq x1 x2)))
))

; replace x = k
(rule (
    (= (Prog l) (Ass x (Const val)))
)(
    (RProg l (Ass x (Const val)))
))

;;;;;;;;;;;;;;;;
;; CALL CASE
;;;;;;;;;;;;;;;;

;; PROPAGATION
(rule (
    (RProg l (Call f))
    (= val (const-prop l x))
    (= l (L li))
)(
    (set (const-prop (L (+ li 1)) x) val)
))

;; TRANSFORMATION
(rule (
    (= (Prog l) (Call f))
)(
    (RProg l (Call f))
))

;;;;;;;;;;;;;;;;
;; IF CASE
;;;;;;;;;;;;;;;;

;; PROPAGATION
(rule (
    (RProg l (If b l1 l2))
    (= val (const-prop l x))
)(
    (set (const-prop l1 x) val)
    (set (const-prop l2 x) val)
))

;; TRANSFORMATION

; replace if true
(rule (
    (= (Prog l) (If b l1 l2))
    (= True (const-prop l b))
)(
    (RProg l (Goto l1))
))

; replace if false
(rule (
    (= (Prog l) (If b l1 l2))
    (= False (const-prop l b))
)(
    (RProg l (Goto l2))
))

; replace if Top
(rule (
    (= (Prog l) (If b l1 l2))
    (= Top (const-prop l b))
)(
    (RProg l (If b l1 l2))
))

;;;;;;;;;;;;;;;;
;; GOTO CASE
;;;;;;;;;;;;;;;;

;; PROPAGATION
(rule (
    (RProg l1 (Goto l2))
    (= val (const-prop l1 x))
)(
    (set (const-prop l2 x) val)
))

;; TRANSFORMATION
(rule (
    (= (Prog l1) (Goto l2))
)(
    (RProg l1 (Goto l2))
))

;;;;;;;;;;;;;;;;
;; TEST
;;;;;;;;;;;;;;;;

(union (Prog (L 0)) (Ass (V "b") (Const Top)))
(union (Prog (L 1)) (Ass (V "ten") (Const (I 10))))
(union (Prog (L 2)) (Ass (V "one") (Const (I 1))))
(union (Prog (L 3)) (Ass (V "zero") (Const (I 0))))
; x := 10
(union (Prog (L 4)) (Ass (V "x") (Const (I 10))))
; while (...) {
(union (Prog (L 5)) (If (V "b") (L 6) (L 13)))
;     if (x == 10) {
(union (Prog (L 6)) (Ass (V "cond") (Eq (V "x") (V "ten"))))
(union (Prog (L 7)) (If (V "cond") (L 8) (L 10)))
;         DoSomething();
(union (Prog (L 8)) (Call (V "DoSomething")))
;     }
(union (Prog (L 9)) (Goto (L 12)))
;     else {
;         DoSomething();
(union (Prog (L 10)) (Call (V "DoSomethingElse")))
;         x := x + 1;
(union (Prog (L 11)) (Ass (V "x") (Add (V "x") (V "one"))))
;; (union (Prog (L 11)) (Call (V "DoSomethingElse")))
;     }
(union (Prog (L 12)) (Goto (L 5)))
; y := x
(union (Prog (L 13)) (Ass (V "y") (Add (V "x") (V "zero"))))
(union (Prog (L 14)) End)

(run 20)

(check (= (const-prop (L 14) (V "y")) (I 10)))