module Logic (Const Func Var Pred : Set)  where
open import Data.List hiding (all ; and ; or )
open import Data.Bool hiding ( not )

data Expr  : Set  where
   var   : Var → Expr 
   func  : Func → Expr → Expr 
   const : Const → Expr 
   _,_ : Expr → Expr → Expr 

data Statement : Set where
   pred       : Pred  → Statement 
   predx  : Pred  → Expr → Statement 
   _/\_   : Statement → Statement  → Statement 
   _\/_         : Statement → Statement  → Statement 
   ¬_         : Statement  → Statement 
   All_=>_        : Var → Statement → Statement 
   Exist_=>_      : Var → Statement → Statement 

subst-prop :  (e : Statement  ) → (sbst : Expr  → Var →  Expr  → Expr  )  → Var → Expr → Statement 
subst-prop (pred x) sbst xv v = pred x
subst-prop (predx x x₁) sbst xv v = predx x ( sbst x₁ xv v )
subst-prop (e /\ e₁) sbst xv v = ( subst-prop e sbst xv v ) /\ ( subst-prop e₁ sbst xv v )
subst-prop (e \/ e₁) sbst xv v = ( subst-prop e sbst xv v ) \/ ( subst-prop e₁ sbst xv v )
subst-prop (¬ e) sbst xv v = ¬ ( subst-prop e sbst xv v )
subst-prop (All x => e) sbst xv v = All x => ( subst-prop e sbst xv v )
subst-prop (Exist x => e) sbst xv v = Exist x => ( subst-prop e sbst xv v )

{-# TERMINATING #-} 
M : (amap :  Pred  → Bool ) (pmap :  Pred → Expr → Bool )
   →  (all-const   : List Expr )
   →  (subst-prop : Expr  → Var →  Expr  → Expr  )
   → Statement  → Bool
M amap pmap all0 sbst s = m s where
   m :  Statement  → Bool
   m (pred x) = amap x
   m (predx x x₁) = pmap x x₁
   m (s /\ s₁) = m s  ∧ m s₁ 
   m (s \/ s₁) = m s ∨ m s₁ 
   m (¬ s) = Data.Bool.not (m s )
   m (All x => s) = m-all all0 x s  where
     m-all :  List Expr → Var → Statement → Bool
     m-all [] vx s = true
     m-all (x ∷ t) vx s = m (subst-prop s sbst vx x ) ∧ m-all t vx s
   m (Exist x => s) = m-exist all0 x s  where
     m-exist :  List Expr → Var  → Statement → Bool
     m-exist [] vx s = false
     m-exist (x ∷ t) vx s = m (subst-prop s sbst vx x ) ∨ m-exist t vx s