--- a/first-order.agda	Thu Aug 13 09:26:06 2020 +0900
+++ b/first-order.agda	Thu Aug 13 10:17:15 2020 +0900
@@ -1,7 +1,7 @@
 module first-order where
 open import Data.List hiding (all ; and ; or )
 open import Data.Maybe 
-open import Data.Bool hiding ( and ; or ; not )
+open import Data.Bool hiding ( not )
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 
 data Term : Set where
@@ -25,48 +25,101 @@
       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 Var : Term → Set where
-   varX : Var X
-   varY : Var Y
-   varZ : Var Z
+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
 
-data Func : Term → Set where
-   funcf : Func f
-   funcg : Func g
-   funch : Func h
+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
 
-data Const : Term → Set where
-   ca : Const a
-   cb : Const b
-   cc : Const c
+Const : Term → Set
+Const x = Kinds x const
+
+Func : Term → Set
+Func x = Kinds x func
 
-data Predicate  : Term → Set where
-   pp : Predicate p
-   pq : Predicate q
-   pr : Predicate r
+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 : Term → Set)  where
+module Logic (Const Func Var Pred : Term → Set)  where
 
-  data Expr  : Set 
-  data Args  : List Expr  → Set  where
-     last : (last : Expr ) → Args [ last ]
-     next : (h : Expr ) → {t : List Expr  } → Args   t   → Args  ( h ∷ t )
-
-  data Expr  where
-     var   : {v : Term} → Var v → Expr 
-     func  : {x : Term} → (f : Func x) → {args : List Expr } → Args  args → Expr 
-     const : {c : Term} → Const c → Expr 
+  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 = {!!}
+  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 = {!!}
+
+
+
+
+