--- a/cbc/stack-subtype-sample.agda	Thu Jan 12 02:48:09 2017 +0000
+++ b/cbc/stack-subtype-sample.agda	Sat Jan 14 00:00:40 2017 +0000
@@ -6,7 +6,7 @@
 
 open import stack-subtype ℕ  as S
 open import subtype Context as N
-open import subtype (MetaContext Context) as M
+open import subtype (Meta Context) as M
 
 
 record Num : Set where
@@ -18,8 +18,8 @@
   NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c})
                                   ; set = (\c n -> record c {n = Num.num n})}
   NumIsMetaDataSegment : M.DataSegment Num
-  NumIsMetaDataSegment = record { get = (\m -> record {num = Context.n (MetaContext.context m)})
-                                ; set = (\m n -> record m {context = record (MetaContext.context m) {n = Num.num n}})}
+  NumIsMetaDataSegment = record { get = (\m -> record {num = Context.n (Meta.context m)})
+                                ; set = (\m n -> record m {context = record (Meta.context m) {n = Num.num n}})}
 
 
 plus3 : Num -> Num
@@ -30,27 +30,27 @@
 
 
 setNext : {X Y : Set} {{x : N.DataSegment X}} {{y : N.DataSegment Y}}
-        -> (N.CodeSegment X Y) -> M.CodeSegment (MetaContext Context) (MetaContext Context)
+        -> (N.CodeSegment X Y) -> M.CodeSegment (Meta Context) (Meta Context)
 setNext c = M.cs (\mc -> record mc {nextCS = liftContext c})
 
-setElement : ℕ -> M.CodeSegment (MetaContext Context) (MetaContext Context)
-setElement x = M.cs (\mc -> record mc {context = record (MetaContext.context mc) {element = just x}})
+setElement : ℕ -> M.CodeSegment (Meta Context) (Meta Context)
+setElement x = M.cs (\mc -> record mc {context = record (Meta.context mc) {element = just x}})
 
 
 
-plus5AndPushWithPlus3 : {mc : MetaContext Context} {{_ : N.DataSegment Num}}
-               -> M.CodeSegment Num (MetaContext Context)
+plus5AndPushWithPlus3 : {mc : Meta Context} {{_ : N.DataSegment Num}}
+               -> M.CodeSegment Num (Meta Context)
 plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} )
   where
-    co    = MetaContext.context mc
+    co    = Meta.context mc
     con : Num -> Context
     con record { num = num } = N.DataSegment.set nn co record {num = num + 5}
-    st    = MetaContext.stack mc
+    st    = Meta.stack mc
 
 
 
 
-push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  MetaContext Context
+push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  Meta Context
 push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc
   where
     con  = record { n = 4 ; element = just 0}
@@ -64,7 +64,7 @@
 push-sample-equiv = refl
 
 
-pushed-sample : {m : MetaContext Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  MetaContext Context
+pushed-sample : {m : Meta Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  Meta Context
 pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc
   where
     con  = record { n = 4 ; element = just 0}
@@ -73,9 +73,14 @@
 
 
 
-pushed-sample-equiv : {m : MetaContext Context} -> pushed-sample {m} ≡ record { nextCS  = liftContext plus3CS
-                                                                               ; stack   = record { top = just (cons 0 nothing) }
-                                                                               ; context = record { n   = 12} }
+pushed-sample-equiv : {m : Meta Context} ->
+                      pushed-sample {m} ≡ record { nextCS  = liftContext plus3CS
+                                                  ; stack   = record { top = just (cons 0 nothing) }
+                                                  ; context = record { n   = 12} }
 pushed-sample-equiv = refl
 
 
+
+n-push : {{_ : M.DataSegment (Meta Context)}} -> Meta Context -> Meta Context
+n-push m = M.csComp (pushSingleLinkedStackCS) (setElement ?)
+