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.Binary.PropositionalEquality hiding ( [_] )

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
      karg  : (x y : Term ) → Kinds (x ⟨ y  ⟩ ) arg
      kargs : (x y : Term ) → Kinds (x , y )  args
      kand  : (x y : Term ) → Kinds (x /\ y )  conn
      kor   : (x y : Term ) → Kinds (x \/ y ) conn
      knot  : (x : Term ) → Kinds  (¬ x ) conn
      kall_ : (x y : Term ) → Kinds (all x => y ) conn
      kexit : (x y : Term ) → Kinds (∃ x => y ) conn

kindOf : Term → Kind
kindOf X = var
kindOf Y = var
kindOf Z = var
kindOf a = const
kindOf b = const
kindOf c = const
kindOf f = func
kindOf g = func
kindOf h = func
kindOf p = pred
kindOf q = pred
kindOf r = pred
kindOf (t ⟨ t₁ ⟩) = arg
kindOf (t , t₁) = args
kindOf (t /\ t₁) = conn
kindOf (t \/ t₁) = conn
kindOf (¬ t) = conn
kindOf (all t => t₁) =  conn
kindOf (∃ t => t₁) = conn

Const : Term → Set
Const x = Kinds x const

Func : Term → Set
Func x = Kinds x func

Var : Term → Set
Var x = Kinds x var

Predicate : Term → Set
Predicate x = Kinds x pred

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

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

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

  data Statement : Term → Set where
     atom  :  {x : Term } → Pred x → Statement ( x )
     predicate  :  {p 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 t : Term} → Var x → Statement t → Statement ( all x => t )
     Exist  :  {x t : Term} → Var x → Statement t → Statement ( ∃ x => t )


  parse : (t : Term ) → Maybe (Statement t )
  parse t with kindOf t
  parse t | pred = {!!}
  parse t | const = {!!}
  parse t | var = {!!}
  parse t | func = {!!}
  parse t | conn = {!!}
  parse t | arg = {!!}
  parse t | args = {!!}