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 Term : Set where
      *_      : Atom → Term
      _⟨_⟩    : Atom → Term → Term
      _,_     : Term → Term → Term
      _/\_    : Term → Term → Term
      _\/_    : Term → Term → Term
      ¬       : Term → Term 
      all_=>_ : Atom → Term → Term
      ∃_=>_   : Atom → Term → Term

  data Expr  : Term → Set  where
     var   : {v : Atom } → Var v → Expr (* v)
     func  : {x : Atom } { args : Term} → (f : Func x) → Expr args  → Expr ( x ⟨ args ⟩ )
     const : {c : Atom } → Const c → Expr (* c)
     args : {x y : Term} → (ex : Expr x) → (ey : Expr y) → Expr ( x , y )

  data Statement : Term → Set where
     atom  :  {x : Atom } → Pred x → Statement ( * x )
     predicate  :  {p : Atom } {args : Term } → Pred p → Expr args  → Statement ( p ⟨ args ⟩ )
     and  :  {x y : Term } → Statement x → Statement y  → Statement ( x /\ y )
     or   :  {x y : Term } → Statement x → Statement y  → Statement ( x \/ y )
     not   :  {x : Term } → Statement x → Statement ( ¬ x  )
     All    :  {x : Atom } { t : Term} → Var x → Statement t → Statement ( all x => t )
     Exist  :  {x : Atom } { t : Term} → Var x → Statement t → Statement ( ∃ x => t )

  Model : (ampa :  {x : Atom } → (px :  Pred x ) → Bool )
       →  (pmap : {p : Atom } { args : Term } → (px :  Pred p ) → Expr args  → Bool )
       →  (all0   :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool )
       →  (exist :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool )
       → {t : Term } → Statement t  → Bool
  Model amap pmap all0 exist s = model s where
      model : {t : Term} → Statement t → 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) = all0 x s
      model (Exist x s) = exist x s

data Atom : Set where
      X : Atom
      Y : Atom
      Z : Atom
      a : Atom
      b : Atom
      c : Atom
      f : Atom
      g : Atom
      h : Atom
      p : Atom
      q : Atom
      r : Atom


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

data Kinds : Atom → 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 : Atom → Set
Const x = Kinds x const

Func : Atom → Set
Func x = Kinds x func

Var : Atom → Set
Var x = Kinds x var

Pred : Atom → Set
Pred x = Kinds x pred

open Logic Atom Const Func Var Pred 

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

parse-arg : (t : Term ) → Maybe (Expr t )
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 t )
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 : {e xv : Term } { x : Atom } → Expr e → Var x → (value : Expr xv ) → Expr {!!}
subst-expr = {!!}

subst-prop : {xv t : Term } {x : Atom } (orig : Statement t ) → Var x → (value : Expr xv ) → Statement {!!}
subst-prop = {!!}

ampa :  {x : Atom } → (px :  Pred x ) → Bool 
ampa {p} px = false
ampa {q} px = true
ampa {r} px = false
pmap : {p : Atom } { args : Term } → (px :  Pred p ) → Expr args  → Bool 
pmap {p} px (Logic.func kf (Logic.const x)) = true
pmap {p} px (Logic.func kf _) = false
pmap {p}  px _ = false
pmap {q} {y} px _ = false
pmap {r} {y} px _ = false
all0   :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool 
all0   = {!!}
exist :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool 
exist = {!!}