# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1482048788 0
# Node ID afb2304be45b8e904aa194593627baa6079c84a6
# Parent  4dd4400b48aa7a23deb4646386c219462376bba3# Parent  d924de5deb70224483e98aaf544dffce3ca80953
Merge 20:d924de5deb70

diff -r d924de5deb70 -r afb2304be45b cbc/tuple.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/tuple.agda	Sun Dec 18 08:13:08 2016 +0000
@@ -0,0 +1,51 @@
+module tuple where
+
+open import Level
+
+
+
+_×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
+_×_ {l} U V = {X : Set  l} -> (U -> V -> X) -> X
+
+<_,_> : {l : Level} {A B : Set l} -> A -> B -> A × B
+<_,_> {l} {A} {B} a b = \{X : Set l} -> \(x : A -> B -> X) -> x a b
+
+
+CodeSegment : {l : Level} -> Set l -> Set l -> Set l -> Set l -> Set (suc l)
+CodeSegment A B C D  = (A × B) -> (C × D)
+
+
+data Nat : Set where
+  O : Nat
+  S : Nat -> Nat
+
+data Unit : Set where
+  unit : Unit
+
+
+fst : {l : Level} {A B : Set l} -> A × B  -> A
+fst x = x (\a b -> a)
+
+snd : {l : Level} {A B : Set l} -> A × B -> B
+snd x = x (\a b -> b)
+
+
+
+plus1 : CodeSegment Nat Unit Nat Unit
+plus1 a = < (S (fst a)) , unit >
+
+
+twice' : Nat -> Nat
+twice' O     = O
+twice' (S n) = (S (S (twice' n)))
+
+twice : CodeSegment Nat Unit Nat Unit
+twice a = < (twice' (fst a)) , unit >
+
+
+_∘_ : {l : Level} {A B C D E F : Set l} -> CodeSegment C D E F -> CodeSegment A B C D -> CodeSegment A B E F
+_∘_ cs2 cs1 x = cs2 (cs1 x)
+
+
+hoge : CodeSegment Nat Unit Nat Unit
+hoge = ((plus1 ∘ twice) ∘ twice)
diff -r d924de5deb70 -r afb2304be45b cbc/variable-tuple.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/variable-tuple.agda	Sun Dec 18 08:13:08 2016 +0000
@@ -0,0 +1,72 @@
+module variable-tuple where
+
+open import Data.Nat hiding (_<_ ; _>_)
+open import Data.String
+open import Data.List
+open import Data.Unit
+open import Data.Product
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality
+
+data Format : Set₁ where
+  FEnd : Format
+  FSet : Set -> Format -> Format
+
+<> : Format
+<> = FEnd
+
+infix  51 _>
+_> : (Format -> Format) -> Format
+_> f = f FEnd
+
+infixl 52 _||_
+_||_ : (Format -> Format) -> Set -> (Format -> Format)
+_||_ f1 s = f1 ∘ (FSet s)
+
+infix 53 <_
+<_ : Set -> Format -> Format
+<_ s = FSet s
+
+
+unit : Format
+unit = <>
+
+single : Format
+single = < ℕ  >
+
+double : Format
+double = < String || ℕ  >
+
+triple : Format
+triple = < String || ℕ  || (List ℕ) >
+
+
+DataSegment : {A : Set} -> Format -> Set
+DataSegment {A} FEnd       = A
+DataSegment {A} (FSet x f) = x -> (DataSegment {A} f)
+
+
+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-double : ods csDouble
+ods-double = "hoge" , zero , tt
+
+
+ids : {A : Set} -> CodeSegment ->  Set
+ids {A} (cs i o) = DataSegment {A} i
+
+ids-double : {A : Set} {a : A} -> ids {A} csDouble
+ids-double {_} {a}  =  \(s : String) -> \(n : ℕ) -> a
+
+
+executeCS : (cs : CodeSegment) -> Set
+executeCS c = ids {ods c} c
+