スキーマ、タプル空間、タプルインスタンス、フィールド関数、テーブル
structure Schema where
fields : Type
typeAssig : fields → Type
def TupleSpace (S : Schema) := ((f : S.fields) → S.typeAssig f)
inductive NameAge where
| name : NameAge
| age : NameAge
deriving Repr
def Person : Schema := {
fields := NameAge
typeAssig := (λ| .name => String | .age => (Nat:Type))
}
#check TupleSpace Person
def personTaro : (TupleSpace Person) :=
(λ| .name => "Taro" | .age => (21 :Nat) )
#eval personTaro .age
def personAkane : (TupleSpace Person) :=
(λ| .name => "Akane" | .age => (25 :Nat) )
structure Person' where
name : String
age : Nat
def personTaro' : Person' := {
name := "Taro"
age := 21
}
#eval personTaro'.age
def getField (S : Schema ) (t : TupleSpace S) (f: S.fields) :
(S.typeAssig f) :=
t f
#eval getField Person personTaro NameAge.age
def Table (S : Schema) :Type := List (TupleSpace S)
def TaroAkane : Table Person := [
personTaro,
personAkane
]
#eval TaroAkane.map (λ p => p NameAge.age)文字列または番号の有限集合としての列挙型をどうする？
