--- a/first-order.agda	Thu Aug 13 10:17:15 2020 +0900
+++ b/first-order.agda	Thu Aug 13 11:07:35 2020 +0900
@@ -2,6 +2,7 @@
 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 ( [_] )
 
 data Term : Set where
@@ -25,6 +26,23 @@
       all_=>_ :  Term → Term → Term
       ∃_=>_ :  Term → Term → Term
 
+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 )
+
 data Kind : Set where
       pred : Kind
       const : Kind
@@ -85,41 +103,77 @@
 Var : Term → Set
 Var x = Kinds x var
 
-Predicate : Term → Set
-Predicate x = Kinds x pred
+Pred : Term → Set
+Pred x = Kinds x pred
 
 ex1 : Term
 ex1 = ¬ ( p /\ ( all X => ( p ⟨ f ⟨ X ⟩ ⟩ )))
 
-module Logic (Const Func Var Pred : Term → Set)  where
+open Logic Const Func Var Pred 
 
-  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 )
+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
 
-  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 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
 
-  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 = {!!}
-
-
-
-
-
+  ex2 = parse ex1