; Resolution theorem proving
; 
; Traditional resolution theorem provers maintain a clause database
; of formulas in Conjunction Normal Form (CNF a big And of Ors).
; Each clause is a set of positive and negative literals
; The prover saturates this set by taking two clauses 
; {a}\/c1  {not a}\/c2 and creating a new clause c1 \/ c2.
; Clauses also are pruned by simplications, unit propagation,
; and subsumption.
; These systems use sophisticated term indexing to find matching clauses

; A natural question is whether egglog's saturation and term indexing gives
; a leg up towards building one of these systems. A programmable one even,
; with built in support for equality reasoning

; Resolution is provided by a join
; unit propagation is an equation solving process and egraph substitution
; Clause Simplification is provided by rewrite rules

; This encoding seems about right but is unsatisfying
; Using AC to encode the set nature of clauses is inefficient

; An important aspect of these provers that seems challenging to encode shallowly
; is that the match also occurs modulo _unification_.
; The unification variables of each clause are not globally scoped, really
; they are scoped outside the body of each clase in an implicit \forall
; This encoding as it stands really only supports ground atoms modulo equality

(datatype Bool)
(function TrueConst () Bool)
(let True (TrueConst))
(function FalseConst () Bool)
(let False (FalseConst))
(function myor (Bool Bool) Bool)
(function negate (Bool) Bool)

; clauses are assumed in the normal form (or a (or b (or c False)))

(union (negate False) True)
(union (negate True) False)

; "Solving" negation equations
(rule ((= (negate p) True)) ((union p False)))
(rule ((= (negate p) False)) ((union p True)))

; canonicalize associtivity. "append" for clauses
; terminate with false
(rewrite (myor (myor a  b) c) (myor a (myor b c)))
; commutativity
(rewrite (myor a (myor b c)) (myor b (myor a c)))

;absorption
(rewrite (myor a (myor a b)) (myor a b))
(rewrite (myor a (myor (negate a) b)) True)

; simplification
(rewrite (myor False a) a)
(rewrite (myor a False) a)
(rewrite (myor True a) True)
(rewrite (myor a True) True)

; unit propagation
; This is kind of interesting actually.
; Looks a bit like equation solving

; The following is not valid egglog but could be?
;(rewrite p True    
;    :when ((= True (or p False))))

(rule ((= True (myor p False))) ((union p True)))

; resolution
; This counts on commutativity to bubble everything possible up to the front of the clause.
(rule ((= True (myor a as)) (= True (myor (negate a) bs)))
      ((union (myor as bs) True)))

; example predicate
(function p (i64) Bool)
(let p0 (p 0))
(let p1 (p 1))
(let p2 (p 2))
;(union (or p0 (or p1 (or p2 False))) True)
;(union (or (negate p0) (or p1 (or (negate p2) False))) True)
(union (myor p1 (myor (negate p2) False)) True)
(union (myor p2 (myor (negate p0) False)) True)
(union (myor p0 (myor (negate p1) False)) True)
(union p1 False)
(union (myor (negate p0) (myor p1 (myor p2 False))) True)
(run 10)


(check (!= True False))
(check (= p0 False))
(check (= p2 False))

; we could turn the original axioms into _patterns_  in all possible directions.
; Which is kind of compelling
; (rule ((or (pat x)))  )
; or let a unification expansion happen and use thos