Mercurial > hg > Members > kono > Proof > FirstOrder
changeset 2:08f8256a6b11
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 13 Aug 2020 10:17:15 +0900 (2020-08-13) |
parents | a087d3911b07 |
children | 9633bb018116 |
files | first-order.agda |
diffstat | 1 files changed, 81 insertions(+), 28 deletions(-) [+] |
line wrap: on
line diff
--- 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 = {!!} + + + + +