# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1484141843 0
# Node ID 81c6779583b6ed17a1425615f15f846db4a4c4f8
# Parent  fa95e30701387327b8f4d9edf5ef702595c56c3e
Add push-sample

diff -r fa95e3070138 -r 81c6779583b6 cbc/stack-subtype.agda
--- a/cbc/stack-subtype.agda	Wed Jan 11 10:56:13 2017 +0000
+++ b/cbc/stack-subtype.agda	Wed Jan 11 13:37:23 2017 +0000
@@ -123,9 +123,23 @@
         -> (N.CodeSegment X Y) -> M.CodeSegment (MetaContext Context) (MetaContext Context)
 setNext c = M.cs (\mc -> record mc {nextCS = liftContext c})
 
-
-
-
+setElement : A -> M.CodeSegment (MetaContext Context) (MetaContext Context)
+setElement x = M.cs (\mc -> record mc {context = record (MetaContext.context mc) {element = just x}})
 
 pushPlus3CS : {mc : MetaContext Context} -> M.CodeSegment (MetaContext Context) (MetaContext Context)
 pushPlus3CS {mc} = M.csComp {mc} pushSingleLinkedStackCS (setNext plus3CS)
+
+plus5AndPush : {mc : MetaContext Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}}
+               -> M.CodeSegment Num (MetaContext Context)
+plus5AndPush {mc} {{nn}} = M.cs (\n -> record {context = con ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} )
+  where
+    con  = MetaContext.context mc
+    st   = MetaContext.stack mc
+
+
+push-sample : {{_ : M.DataSegment Num}} -> MetaContext Context
+push-sample = M.exec (plus5AndPush {mc}) mc
+  where
+    con  = record { n = 4 ; element = nothing}
+    code = N.cs (\c -> c)
+    mc   = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
diff -r fa95e3070138 -r 81c6779583b6 cbc/subtype.agda
--- a/cbc/subtype.agda	Wed Jan 11 10:56:13 2017 +0000
+++ b/cbc/subtype.agda	Wed Jan 11 13:37:23 2017 +0000
@@ -14,7 +14,8 @@
   cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B
 
 
-exec : {I O : Set} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context
+exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}}
+     -> CodeSegment I O -> Context -> Context
 exec {l} {{i}} {{o}}  (cs b) c = set o c (b (get i c))