Mercurial > hg > Members > atton > agda-proofs
changeset 22:84e3fbc662db
Define cs compose operator
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 22 Dec 2016 05:47:20 +0000 |
| parents | afb2304be45b |
| children | 723532aa0592 |
| files | cbc/variable-tuple.agda |
| diffstat | 1 files changed, 30 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/cbc/variable-tuple.agda Sun Dec 18 08:13:08 2016 +0000 +++ b/cbc/variable-tuple.agda Thu Dec 22 05:47:20 2016 +0000 @@ -41,27 +41,38 @@ triple = < String || ℕ || (List ℕ) > -DataSegment : {A : Set} -> Format -> Set -DataSegment {A} FEnd = A -DataSegment {A} (FSet x f) = x -> (DataSegment {A} f) +record CodeSegment : Set₁ where + field + IDS : Format + ODS : Format +cs : Format -> Format -> CodeSegment +cs i o = record { IDS = i ; ODS = o } -data CodeSegment : Set₁ where - cs : Format -> Format -> CodeSegment csDouble : CodeSegment csDouble = cs double double + ods : CodeSegment -> Set -ods (cs ids FEnd) = ⊤ -ods (cs ids (FSet s f)) = s × (ods (cs ids f)) +ods record { ODS = i } = ods' i + where + ods' : Format -> Set + ods' FEnd = ⊤ + ods' (FSet s o) = s × (ods' o) ods-double : ods csDouble ods-double = "hoge" , zero , tt -ids : {A : Set} -> CodeSegment -> Set -ids {A} (cs i o) = DataSegment {A} i + +ids : {A : Set} -> CodeSegment -> Set +ids {A} record {IDS = IDS} = ids' IDS + where + ids' : Format -> Set + ids' FEnd = A + ids' (FSet x f) = x -> (ids' f) + ids-double : {A : Set} {a : A} -> ids {A} csDouble ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a @@ -70,3 +81,13 @@ executeCS : (cs : CodeSegment) -> Set executeCS c = ids {ods c} c + +_◎_ : {c1ods c2ids : Format} -> {equiv : c1ods ≡ c2ids} -> CodeSegment -> CodeSegment -> CodeSegment +record {IDS = i} ◎ (record {ODS = o}) = cs i o + + +compose-cs : CodeSegment +compose-cs = _◎_ {double} {double} {refl} csDouble csDouble + + +