module simple-logic where
open import Data.Bool

data Var : Set where
   X : Var
   Y : Var
   Z : Var

data Expr : Set where
   var : Var → Expr
   a : Expr
   b : Expr
   c : Expr
   f : Expr → Expr
   g : Expr → Expr
   h : Expr → Expr
   _,_ : Expr → Expr → Expr

data Statement : Set where
   p : Expr → Statement
   q : Statement
   r : Statement
   _/\_    :  Statement → Statement → Statement
   _\/_    :  Statement → Statement → Statement
   ¬       :  Statement → Statement 
   all_=>_ :  Var → Statement → Statement
   ∃_=>_   :  Var → Statement → Statement

test002 : Statement
test002 = ¬ ( q /\ ( all X => p ( f ( var X  ))))

subst-expr : Expr → Var → (value : Expr ) → Expr
subst-expr (var X ) X v = v 
subst-expr (var Y ) Y v = v 
subst-expr (var Z ) Z v = v 
subst-expr (f x ) n v = f (subst-expr x n v) 
subst-expr (x , y ) n v = (subst-expr x n v) , (subst-expr y n v) 
subst-expr x  n v = x 

subst-prop : (orig : Statement ) → Var → (value : Expr ) → Statement
subst-prop (p x ) n v = p ( subst-expr x n v )
subst-prop q n v = q
subst-prop r n v = r
subst-prop (x /\ y) n v = subst-prop x n v /\ subst-prop x n v
subst-prop (x \/ y) n v = subst-prop x n v \/ subst-prop x n v
subst-prop (¬ x) n v = ¬ (subst-prop x n v )
subst-prop (all x => y) n v = all x => subst-prop y n v 
subst-prop (∃ x => y) n v =  ∃ x => subst-prop y n v 

{-# TERMINATING #-} 
M0 : Statement → Bool
M0 q = true
M0 r = false
M0 (p  a ) = true
M0 (x /\ y) = M0 x ∧ M0 y
M0 (x \/ y) = M0 x ∨ M0 y
M0 (¬ x) = not (M0 x)
-- we only try simple constant, it may contains arbitrary complex functional value
M0 (all x => y) = M0 ( subst-prop y x a ) ∧ M0 ( subst-prop y x b ) ∧ M0 ( subst-prop y x c ) 
M0 (∃ x => y)   = M0 ( subst-prop y x a ) ∨ M0 ( subst-prop y x b ) ∨ M0 ( subst-prop y x c ) 
M0 _ = false

test003 : Bool 
test003 = M0 ( ∃ X => p ( var X ))