# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1484360529 0
# Node ID 29b069a0c409ff8470d9568c612b81f54937cc89
# Parent  7af6c894f411a1d1ec870f9bacc736c1d8ffc1ba
Define n-push

diff -r 7af6c894f411 -r 29b069a0c409 cbc/stack-subtype-sample.agda
--- a/cbc/stack-subtype-sample.agda	Sat Jan 14 02:10:28 2017 +0000
+++ b/cbc/stack-subtype-sample.agda	Sat Jan 14 02:22:09 2017 +0000
@@ -78,25 +78,16 @@
 pushNum = N.cs pn
   where
     pn : Context -> Context
-    pn record { n = n } = record { n = n  ; element = just n}
-
-n-push : {{_ : N.DataSegment Num}} -> Meta -> Meta
-n-push {{x}} record { context = record { n = zero    ; element = el } ; stack = st ; nextCS = code} =
-  M.exec pushSingleLinkedStackCS record { context = record { n = zero ; element = el }
-                                        ; stack   = st ; nextCS  = code}
-n-push {{x}} record { context = record { n = (suc n) ; element = el } ; stack = st ; nextCS = code} =
-  n-push {{x}} record {context = record {n = n ; element = e} ; stack = s ; nextCS = c}
-    where
-      pushedMeta = M.exec pushSingleLinkedStackCS record { context = record { n = (suc n) ; element = el}
-                                                         ; stack = st ; nextCS = code}
-      e = Context.element (Meta.context pushedMeta)
-      s = Meta.stack pushedMeta
-      c = Meta.nextCS pushedMeta
+    pn record { n = n } = record { n = pred n  ; element = just n}
 
 
+pushOnce : Meta -> Meta
+pushOnce m = M.exec pushSingleLinkedStackCS m
 
-n-push-cs : M.CodeSegment Meta Meta
-n-push-cs = M.cs n-push
+n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
+n-push {{mm}} (zero)  = M.cs {{mm}} {{mm}} pushOnce
+n-push {m} {{mm}} (suc n)        = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-push {m} {{mm}} n) (M.cs {{mm}} {{mm}} pushOnce)
+
 
 
 initMeta : ℕ -> N.CodeSegment Context Context -> Meta
@@ -105,10 +96,13 @@
                          ; nextCS  = code
                          }
 
-n-push-cs-exec = M.exec n-push-cs (initMeta 4 pushNum)
+n-push-cs-exec = M.exec (n-push {meta} 2) meta
+  where
+    meta = (initMeta 5 pushNum)
 
 
-n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS  = {!!}
-                                                ; context = {!!}
-                                                ; stack   = record { top = {!!} }}
+n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS  = pushNum
+                                                ; context = record {n = 2 ; element = just 3}
+                                                ; stack   = record {top = just (cons 4 (just (cons 5 nothing)))}}
 n-push-cs-exec-equiv = refl
+