module first-order where
open import Data.List hiding (all ; and ; or )
open import Data.Maybe 
open import Data.Bool hiding ( not )
open import Relation.Nullary hiding (¬_)
open import Relation.Binary.PropositionalEquality hiding ( [_] )

module Logic (Atom : Set ) (Const Func Var Pred : Atom → Set)  where

  data Expr  : Set  where
     var   : {v : Atom } → Var v → Expr 
     func  : {x : Atom }  → (f : Func x) → Expr → Expr 
     const : {c : Atom } → Const c → Expr 
     args : Expr → Expr  → Expr 

  data Statement : Set where
     atom       : {x : Atom } → Pred x → Statement 
     predicate  : {p : Atom }  → Pred p → Expr → Statement 
     and        : Statement → Statement  → Statement 
     or         : Statement → Statement  → Statement 
     not        : Statement  → Statement 
     All        : {x : Atom } → Var x → Statement → Statement 
     Exist      : {x : Atom } → Var x → Statement → Statement 

  {-# TERMINATING #-} 
  Model : (ampa :  {x : Atom } → (px :  Pred x ) → Bool )
       →  (pmap : {p : Atom }  → (px :  Pred p ) → Expr → Bool )
       →  (all-const   : List Expr )
       → ( subst-prop :  {x : Atom } (e : Statement  ) → Var x → (value : Expr ) → Statement  )
       → Statement  → Bool
  Model amap pmap all0 sbst s = model s where
      model :  Statement  → Bool
      model (atom x) = amap x
      model (predicate x x₁) = pmap x x₁
      model (and s s₁) = model s  ∧ model s₁ 
      model (or s s₁) = model s ∨ model s₁ 
      model (not s) = Data.Bool.not (model s )
      model (All x s) = model-all all0 x s  where
          model-all :  List Expr → {x : Atom } → Var x → Statement → Bool
          model-all [] vx s = true
          model-all (x ∷ t) vx s = model (sbst s vx x ) ∧ model-all t vx s
      model (Exist x s) = model-exist all0 x s  where
          model-exist :  List Expr → {x : Atom } → Var x → Statement → Bool
          model-exist [] vx s = false
          model-exist (x ∷ t) vx s = model (sbst s vx x ) ∨ model-exist t vx s

data Term : Set where
      X : Term
      Y : Term
      Z : Term
      a : Term
      b : Term
      c : Term
      f : Term
      g : Term
      h : Term
      p : Term
      q : Term
      r : Term
      _⟨_⟩    : Term → Term → Term
      _,_     : Term → Term → Term
      _/\_    : Term → Term → Term
      _\/_    : Term → Term → Term
      ¬       : Term → Term 
      all_=>_ : Term → Term → Term
      ∃_=>_   : Term → Term → Term


data Kind : Set where
      pred : Kind
      const : Kind
      var  : Kind
      func : Kind
      conn : Kind
      arg  : Kind
      args : Kind

data Kinds : Term → Kind → Set where
      kX : Kinds X var
      kY : Kinds Y var
      kZ : Kinds Z var
      ka : Kinds a const
      kb : Kinds b const
      kc : Kinds c const
      kf : Kinds f func
      kg : Kinds g func
      kh : Kinds h func
      kp : Kinds p pred
      kq : Kinds q pred
      kr : Kinds r pred

Const : Term → Set
Const x = Kinds x const

Func : Term → Set
Func x = Kinds x func

Var : Term → Set
Var x = Kinds x var

Pred : Term → Set
Pred x = Kinds x pred

open Logic Term Const Func Var Pred 

ex1 : Term
ex1 = ¬ ( p  /\ ( all X => ( p ⟨ f ⟨ X ⟩ ⟩ )))

parse-arg : (t : Term ) → Maybe Expr 
parse-arg ( X) = just (var kX)
parse-arg ( Y) = just (var kY)
parse-arg ( Z) = just (var kZ)
parse-arg ( a) = just (const ka)
parse-arg ( b) = just (const kb)
parse-arg ( c) = just (const kc)
parse-arg (f ⟨ x ⟩) with parse-arg x
parse-arg (f ⟨ x ⟩) | just pt = just ( func kf pt )
parse-arg (f ⟨ x ⟩) | nothing = nothing
parse-arg (g ⟨ x ⟩) with parse-arg x
parse-arg (g ⟨ x ⟩) | just pt = just ( func kg pt )
parse-arg (g ⟨ x ⟩) | nothing = nothing
parse-arg (h ⟨ x ⟩) with parse-arg x
parse-arg (h ⟨ x ⟩) | just pt = just ( func kh pt )
parse-arg (h ⟨ x ⟩) | nothing = nothing
parse-arg (_ ⟨ x ⟩) = nothing
parse-arg (t , t₁) with parse-arg t | parse-arg t₁
... | just x | just y = just ( args x y )
... | _ | _ = nothing
parse-arg _ = nothing

parse : (t : Term ) → Maybe Statement 
parse ( p) = just ( atom kp )
parse ( q) = just ( atom kq )
parse ( r) = just ( atom kr )
parse (p ⟨ x ⟩) with parse-arg x
parse (p ⟨ x ⟩) | just y = just ( predicate kp y )
parse (p ⟨ x ⟩) | nothing = nothing
parse (q ⟨ x ⟩) with parse-arg x
parse (q ⟨ x ⟩) | just y = just ( predicate kq y )
parse (q ⟨ x ⟩) | nothing = nothing
parse (r ⟨ x ⟩) with parse-arg x
parse (r ⟨ x ⟩) | just y = just ( predicate kr y )
parse (r ⟨ x ⟩) | nothing = nothing
parse (_ ⟨ x ⟩) = nothing
parse (t /\ t₁) with parse t | parse t₁
parse (t /\ t₁) | just p₁ | just p₂ = just ( and p₁ p₂ )
parse (t /\ t₁) | _ | _ = nothing
parse (t \/ t₁) with parse t | parse t₁
parse (t \/ t₁) | just p₁ | just p₂ = just ( or p₁ p₂ )
parse (t \/ t₁) | _ | _ = nothing
parse (¬ t)  with parse t 
parse (¬ t)  | just tx = just ( not tx )
parse (¬ t)  | _ = nothing
parse (all X => t₁) with parse t₁
... | just tx = just ( All kX tx )
... | _ = nothing
parse (all Y => t₁) with parse t₁
... | just tx = just ( All kY tx )
... | _ = nothing
parse (all Z => t₁) with parse t₁
... | just tx = just ( All kZ tx )
... | _ = nothing
parse (∃ X => t₁) with parse t₁
... | just tx = just ( Exist kX tx )
... | _ = nothing
parse (∃ Y => t₁) with parse t₁
... | just tx = just ( Exist kY tx )
... | _ = nothing
parse (∃ Z => t₁) with parse t₁
... | just tx = just ( Exist kZ tx )
... | _ = nothing
parse _ = nothing

ex2 = parse ex1

subst-expr :  { x : Term } → Expr  → Var x → (value : Expr ) → Expr 
subst-expr  (var kX) kX v = v
subst-expr  (var kY) kX v = var kY
subst-expr  (var kZ) kX v = var kZ
subst-expr  (var kX) kY v = var kX
subst-expr  (var kY) kY v = v
subst-expr  (var kZ) kY v = var kZ
subst-expr  (var kX) kZ v = var kX
subst-expr  (var kY) kZ v = var kY
subst-expr  (var kZ) kZ v = v
subst-expr  (func f₁ e) xv v = func f₁ ( subst-expr e xv v ) 
subst-expr  (const x₁) xv v = (const x₁)
subst-expr  (args e e₁) xv v = args ( subst-expr e xv v ) ( subst-expr e₁ xv v ) 

subst-prop :  {x : Term } (e : Statement  ) → Var x → (value : Expr ) → Statement 
subst-prop (atom x) xv v = atom x
subst-prop (predicate x x₁) xv v = predicate x ( subst-expr x₁ xv v )
subst-prop (and e e₁) xv v = and ( subst-prop e xv v ) ( subst-prop e₁ xv v )
subst-prop (or e e₁) xv v =  or ( subst-prop e xv v ) ( subst-prop e₁ xv v )
subst-prop (not e) xv v = not ( subst-prop e xv v )
subst-prop (All x e) xv v = All x ( subst-prop e xv v )
subst-prop (Exist x e) xv v = Exist x ( subst-prop e xv v )

amap :  {x : Term } → (px :  Pred x ) → Bool 
amap {p} px = false
amap {q} px = true
amap {r} px = false
pmap : {p : Term } → (px :  Pred p ) → Expr → Bool 
pmap {p} px (Logic.const kc) = true
pmap {p}  px _ = false
pmap {q}  px _ = false
pmap {r}  px _ = false

all0   :  List Expr
all0 =  const ka ∷ const kb ∷ const kc ∷ []

test003 : Bool 
test003 with parse ( ∃ X => ( p  ⟨  X ⟩ ) )
test003 | just x = Model amap pmap all0 subst-prop x
test003 | nothing = false