# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1484361333 0
# Node ID c3afde46a41d9e31fa234d51a2f6644dff724768
# Parent  29b069a0c409ff8470d9568c612b81f54937cc89
Define n-pop

diff -r 29b069a0c409 -r c3afde46a41d cbc/stack-subtype-sample.agda
--- a/cbc/stack-subtype-sample.agda	Sat Jan 14 02:22:09 2017 +0000
+++ b/cbc/stack-subtype-sample.agda	Sat Jan 14 02:35:33 2017 +0000
@@ -88,6 +88,14 @@
 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)
 
+popOnce : Meta -> Meta
+popOnce m = M.exec popSingleLinkedStackCS m
+
+n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
+n-pop {{mm}} (zero)      = M.cs {{mm}} {{mm}} popOnce
+n-pop {m} {{mm}} (suc n) = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-pop {m} {{mm}} n) (M.cs {{mm}} {{mm}} popOnce)
+
+
 
 
 initMeta : ℕ -> N.CodeSegment Context Context -> Meta
@@ -106,3 +114,17 @@
                                                 ; stack   = record {top = just (cons 4 (just (cons 5 nothing)))}}
 n-push-cs-exec-equiv = refl
 
+
+n-pop-cs-exec = M.exec (n-pop {meta} 3) meta
+  where
+    meta = record { nextCS  = N.cs id
+                  ; context = record { n = 0 ; element = nothing}
+                  ; stack   = record {top = just (cons 9 (just (cons 8 (just (cons 7 (just (cons 6 (just (cons 5 nothing)))))))))}
+                  }
+
+n-pop-cs-exec-equiv : n-pop-cs-exec ≡ record { nextCS  = N.cs id
+                                              ; context = record { n = 0 ; element = just 6}
+                                              ; stack   = record { top = just (cons 5 nothing)}
+                                              }
+
+n-pop-cs-exec-equiv = refl