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
+
+
+