; Identifiers represented as strings, keep some newtypes around to aid clarity
(datatype ClassT (Class String))
(datatype FieldT (Field String))

(datatype Stmt
    (New String ClassT)
    ; Assign dst src
    (Assign String String)
    ; Store dst field src
    (Store String FieldT String)
    ; Load dst src field
    (Load String String FieldT))

(relation VarPointsTo (String ClassT))
(relation HeapPointsTo (ClassT FieldT ClassT))

; New variables point to classes they're initialized as
(rule ((= x (New a b))) ((VarPointsTo a b)))

; If I assign v1 <- v2 and v2 points to a class c2, then v1 points to class c2
; as well
(rule ((= x (Assign v1 v2)) (VarPointsTo v2 c2))
      ((VarPointsTo v1 c2)))

; If c1.f points to c2, and v2 points to class c1, then assigning v1 <- v2.f
; means v1 points to c2
(rule ((= x (Load v1 v2 f)) 
       (VarPointsTo v2 c1)
       (HeapPointsTo c1 f c2))
      ((VarPointsTo v1 c2)))

; If v1 points to class c1, and v2 to c2, and if v1.f <- v2, then c1.f points to
; c2
(rule ((= x (Store v1 f v2))
       (VarPointsTo v1 c1)
       (VarPointsTo v2 c2))
      ((HeapPointsTo c1 f c2)))

; Example in "From Datalog to Flix"
; l1: ClassA o1 = new ClassA();
; l2: ClassB o2 = new ClassB();
; l3: ClassB o3 = o2;
; l4: o2.f = o1;
; l5: Object r = o3.f;

(let A (Class "A"))
(let B (Class "B"))
(let f (Field "f"))

(let l1 (New "o1" A))
(let l2 (New "o2" B))
(let l3 (Assign "o3" "o2"))
(let l4 (Store "o2" f "o1"))
(let l5 (Load "r" "o3" f))

(run 3)

(check (VarPointsTo "o1" A))
(check (VarPointsTo "o2" B))

(check (VarPointsTo "o3" B))
(check (HeapPointsTo B f A))
(check (VarPointsTo "r" A))