# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1484352040 0
# Node ID bd428bd6b3947c37c28a47ac74a65bee32b05cd4
# Parent  352e8a724829173e9630dab21d0be8539beef177
Trying define n-push/n-pop

diff -r 352e8a724829 -r bd428bd6b394 cbc/maybe-subtype-sample.agda
--- a/cbc/maybe-subtype-sample.agda	Thu Jan 12 02:48:09 2017 +0000
+++ b/cbc/maybe-subtype-sample.agda	Sat Jan 14 00:00:40 2017 +0000
@@ -1,30 +1,45 @@
 module maybe-subtype-sample (A : Set) where
 
 open import Level
+open import Data.Maybe
 open import Function using (id)
 open import Relation.Binary.PropositionalEquality
 
-
-
 open import maybe-subtype A
-open import subtype (Context A) as M
 open import subtype A as N
-
-return : {_ : Context A} {_ : Meta (Context A)} {{_ : N.DataSegment A}} {{_ : M.DataSegment A}} -> A -> Meta A
-return {c} {mc} {{nd}} {{md}} a = record {context = record {maybeElem = just a}}
+open import subtype (Meta A) as M
 
-fmap' : {B : Set} {{_ : M.DataSegment (Context A)}} {{_ : M.DataSegment (Context B)}} -> (A -> B) -> Context A -> Context B
-fmap' f record { maybeElem = (just x) } = record {maybeElem = just (f x)}
-fmap' f record { maybeElem = nothing }  = record {maybeElem = nothing}
-
-
-
-fmap : {c : Context A} {B : Set}
-       {{_ : N.DataSegment A}} {{_ : N.DataSegment B}} {{_ : M.DataSegment (Context A)}} {{_ : M.DataSegment (Context B)}}
-      -> N.CodeSegment A B -> M.CodeSegment (Context A) (Context B)
-fmap  {c} {B} {{na}} {{nb}} {{ma}} {{mb}} (N.cs f) = M.cs {{ma}} (fmap' {B} {{ma}} {{mb}} f)
+instance
+  MetaIsMetaDataSegment : {{_ : M.DataSegment A}} -> M.DataSegment (Meta A)
+  MetaIsMetaDataSegment    = record {get = (\mc -> mc) ; set = (\_ mc -> mc)}
+  ContextIsMetaDataSegment : M.DataSegment (Context)
+  ContextIsMetaDataSegment = record {get = Meta.context ; set = (\mc c -> record mc {context = c})}
 
 
 
 
 
+return : {X : Set} {_ : Context} {_ : Meta A} {{_ : N.DataSegment X}} {{_ : M.DataSegment X}} -> X -> Meta X
+return {c} {mc} {{nd}} {{md}} a = record {context = record {} ; maybeElem = just a}
+
+
+fmap' : {B : Set} -> (A -> B) -> Meta A -> Meta B
+fmap' f record { maybeElem = (just x) } = record {maybeElem = just (f x)}
+fmap' f record { maybeElem = nothing }  = record {maybeElem = nothing}
+
+
+fmap : {c : Context} {B : Set}
+       {{_ : M.DataSegment A}} {{_ : M.DataSegment B}} {{_ : M.DataSegment (Meta A)}}{{_ : M.DataSegment (Meta B)}}
+      -> M.CodeSegment A B -> M.CodeSegment (Meta A) (Meta B)
+fmap  {c} {B} {{na}} {{nb}} {{ma}}  (N.cs f) = M.cs {{ma}} (fmap' {B} f)
+
+
+liftMeta : {B : Set} {{_ : M.DataSegment A}} {{_ : M.DataSegment B}} -> N.CodeSegment A B -> M.CodeSegment A B
+liftMeta (N.cs f) = M.cs f
+
+
+fmap-preserve-id : {x : Meta A} {{nx : N.DataSegment A }}{{mx : M.DataSegment A}} {{mmx : M.DataSegment (Meta A)}}
+                 -> M.exec {{mmx}} {{mmx}} (fmap {{mx}} {{mx}} {{mmx}} {{mmx}} (M.cs id)) x ≡ M.exec (liftMeta (N.cs id)) x
+fmap-preserve-id = {!!}
+
+
diff -r 352e8a724829 -r bd428bd6b394 cbc/maybe-subtype.agda
--- a/cbc/maybe-subtype.agda	Thu Jan 12 02:48:09 2017 +0000
+++ b/cbc/maybe-subtype.agda	Sat Jan 14 00:00:40 2017 +0000
@@ -1,31 +1,19 @@
-module maybe-subtype (A : Set) where
-
 open import Level
+open import Data.Maybe
 open import Function using (id)
 open import Relation.Binary.PropositionalEquality
 
-data Maybe (A : Set) : Set where
-  nothing : Maybe A
-  just    : A -> Maybe A
+module maybe-subtype (A : Set)  where
 
 
-record Context (A : Set) : Set where
-  field
-    maybeElem : Maybe A
+record Context : Set where
 
-open import subtype (Context A) as N
+open import subtype Context as N
 
 
 record Meta (A : Set) : Set where
   field
-    context : Context A
+    context   : Context
+    maybeElem : Maybe A
 
 
-open import subtype (Meta A) as M
-
-instance
-  MetaIsMetaDataSegment : M.DataSegment (Meta A)
-  MetaIsMetaDataSegment = record {get = (\mc -> mc) ; set = (\_ mc -> mc)}
-  ContextIsMetaDataSegment : M.DataSegment (Context A)
-  ContextIsMetaDataSegment = record {get = Meta.context ; set = (\mc c -> record mc {context = c})}
-
diff -r 352e8a724829 -r bd428bd6b394 cbc/stack-product.agda
--- a/cbc/stack-product.agda	Thu Jan 12 02:48:09 2017 +0000
+++ b/cbc/stack-product.agda	Sat Jan 14 00:00:40 2017 +0000
@@ -108,7 +108,7 @@
   where
     push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A)
     push {A} {a} (zero  , s) = (zero , s)
-    push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , ? {- n-push -}) -- needs subtype
+    push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype
 
 
 {-
diff -r 352e8a724829 -r bd428bd6b394 cbc/stack-subtype-sample.agda
--- 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 ?)
+
diff -r 352e8a724829 -r bd428bd6b394 cbc/stack-subtype.agda
--- a/cbc/stack-subtype.agda	Thu Jan 12 02:48:09 2017 +0000
+++ b/cbc/stack-subtype.agda	Sat Jan 14 00:00:40 2017 +0000
@@ -23,10 +23,14 @@
 
 record Context : Set where
   field
+    -- fields for stack
     element : Maybe A
+    stack   : SingleLinkedStack A
+    -- fields for data segments
     n       : ℕ
 
 
+
 open import subtype Context as N
 
 instance
@@ -34,24 +38,22 @@
   ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)}
 
 
-record MetaContext (X : Set) {{_ : N.DataSegment X}} : Set₁ where
+record Meta  : Set₁ where
   field
     context : Context
-    stack   : SingleLinkedStack A
-    nextCS  : N.CodeSegment X X
-
+    nextCS  : N.CodeSegment Context Context
 
-
+    
 
-open import subtype (MetaContext Context) as M
+open import subtype Meta as M
 
 instance
-  MetaContextIncludeContext : M.DataSegment Context
-  MetaContextIncludeContext = record { get = MetaContext.context
-                                     ; set = (\m c -> record m {context = c}) }
+  MetaIncludeContext : M.DataSegment Context
+  MetaIncludeContext = record { get = Meta.context
+                              ; set = (\m c -> record m {context = c}) }
 
-  MetaContextIsMetaDataSegment : M.DataSegment (MetaContext Context)
-  MetaContextIsMetaDataSegment  = record { get = (\m -> m) ; set = (\_ m -> m) }
+  MetaIsMetaDataSegment : M.DataSegment Meta
+  MetaIsMetaDataSegment  = record { get = (\m -> m) ; set = (\_ m -> m) }
 
 
 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
@@ -66,42 +68,44 @@
 emptySingleLinkedStack = record {top = nothing}
 
 
-pushSingleLinkedStack :  MetaContext Context -> MetaContext Context
-pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
+pushSingleLinkedStack : Meta -> Meta
+pushSingleLinkedStack m = M.exec (liftMeta n) (record m {context = record c {stack = (push s e)}})
   where
-    n = MetaContext.nextCS m
-    e = Context.element (MetaContext.context m)
-    s = MetaContext.stack   m
+    c = (Meta.context m)
+    n = Meta.nextCS     m
+    e = Context.element c
+    s = Context.stack   c
     push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
     push s nothing  = s
     push s (just x) = record {top = just (cons x (top s))}
 
 
-
-popSingleLinkedStack : MetaContext Context -> MetaContext Context
-popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
+popSingleLinkedStack : Meta -> Meta
+popSingleLinkedStack m = M.exec (liftMeta n) (record m { context = record c { stack = (st c) ; element = (elem c)}})
   where
-    n = MetaContext.nextCS m
-    con  = MetaContext.context m
-    elem : MetaContext Context -> Maybe A
+    n = Meta.nextCS m
+    c = Meta.context m
+    elem : Context -> Maybe A
     elem record {stack = record { top = (just (cons x _)) }} = just x
-    elem record {stack = record { top = nothing           }} = nothing
-    st : MetaContext Context -> SingleLinkedStack A
+    elem record {stack = record { top = nothing } }          = nothing
+    st : Context -> SingleLinkedStack A
     st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
-    st record {stack = record { top = nothing           }} = record {top = nothing}
-    
-pushSingleLinkedStackCS : M.CodeSegment (MetaContext Context) (MetaContext Context)
+    st record {stack = record { top = nothing } }          = record {top = nothing}
+
+
+pushSingleLinkedStackCS : M.CodeSegment Meta Meta
 pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
 
-popSingleLinkedStackCS : M.CodeSegment (MetaContext Context) (MetaContext Context)
+popSingleLinkedStackCS : M.CodeSegment Meta Meta
 popSingleLinkedStackCS = M.cs popSingleLinkedStack
 
 
 -- for sample
 
 firstContext : Context
-firstContext = record { element = nothing ; n = 0}
+firstContext = record {stack = emptySingleLinkedStack ; element = nothing ; n = 0}
 
 
-firstMetaContext : MetaContext Context
-firstMetaContext = record {stack = emptySingleLinkedStack ; nextCS = (N.cs (\m -> m)) ; context = firstContext}
+firstMeta : Meta 
+firstMeta = record {nextCS = (N.cs (\m -> m)) ; context = firstContext}
+
diff -r 352e8a724829 -r bd428bd6b394 cbc/subtype.agda
--- a/cbc/subtype.agda	Thu Jan 12 02:48:09 2017 +0000
+++ b/cbc/subtype.agda	Sat Jan 14 00:00:40 2017 +0000
@@ -26,7 +26,7 @@
 comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
 
 csComp : {con : Context} -> {l1 l2 l3 l4 : Level}
-         {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
+        {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
          {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
        -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D
 csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f)