--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/stack-subtype-sample.agda.replaced	Tue Sep 08 18:38:08 2020 +0900
@@ -0,0 +1,212 @@
+module stack-subtype-sample where
+
+open import Level renaming (suc to S ; zero to O)
+open import Function
+open import Data.Nat
+open import Data.Maybe
+open import Relation.Binary.PropositionalEquality
+
+open import stack-subtype @$\mathbb{N}$@
+open import subtype Context  as N
+open import subtype Meta     as M
+
+
+record Num : Set where
+  field
+    num : @$\mathbb{N}$@
+
+instance
+  NumIsNormalDataSegment : N.DataSegment Num
+  NumIsNormalDataSegment = record { get = (\c @$\rightarrow$@ record { num = Context.n c})
+                                  ; set = (\c n @$\rightarrow$@ record c {n = Num.num n})}
+  NumIsMetaDataSegment : M.DataSegment Num
+  NumIsMetaDataSegment = record { get = (\m @$\rightarrow$@ record {num = Context.n (Meta.context m)})
+                                ; set = (\m n @$\rightarrow$@ record m {context = record (Meta.context m) {n = Num.num n}})}
+
+
+plus3 : Num @$\rightarrow$@ Num
+plus3 record { num = n } = record {num = n + 3}
+
+plus3CS : N.CodeSegment Num Num
+plus3CS = N.cs plus3
+
+
+
+plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}}
+               @$\rightarrow$@ M.CodeSegment Num (Meta)
+plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n @$\rightarrow$@ record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} )
+  where
+    co    = Meta.context mc
+    con : Num @$\rightarrow$@ Context
+    con record { num = num } = N.DataSegment.set nn co record {num = num + 5}
+    st    = Meta.stack mc
+
+
+
+
+push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} @$\rightarrow$@  Meta
+push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc
+  where
+    con  = record { n = 4 ; element = just 0}
+    code = N.cs (\c @$\rightarrow$@ c)
+    mc   = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
+
+
+push-sample-equiv : push-sample @$\equiv$@ record { nextCS  = liftContext plus3CS
+                                          ; stack   = record { top = nothing}
+                                          ; context = record { n = 9} }
+push-sample-equiv = refl
+
+
+pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} @$\rightarrow$@  Meta
+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}
+    code = N.cs (\c @$\rightarrow$@ c)
+    mc   = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
+
+
+
+pushed-sample-equiv : {m : Meta} @$\rightarrow$@
+                      pushed-sample {m} @$\equiv$@ record { nextCS  = liftContext plus3CS
+                                                  ; stack   = record { top = just (cons 0 nothing) }
+                                                  ; context = record { n   = 12} }
+pushed-sample-equiv = refl
+
+
+
+pushNum : N.CodeSegment Context Context
+pushNum = N.cs pn
+  where
+    pn : Context @$\rightarrow$@ Context
+    pn record { n = n } = record { n = pred n  ; element = just n}
+
+
+pushOnce : Meta @$\rightarrow$@ Meta
+pushOnce m = M.exec pushSingleLinkedStackCS m
+
+n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : @$\mathbb{N}$@) @$\rightarrow$@ M.CodeSegment Meta Meta
+n-push {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
+n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m @$\rightarrow$@ M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m))
+
+popOnce : Meta @$\rightarrow$@ Meta
+popOnce m = M.exec popSingleLinkedStackCS m
+
+n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : @$\mathbb{N}$@) @$\rightarrow$@ M.CodeSegment Meta Meta
+n-pop {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
+n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m @$\rightarrow$@ M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m))
+
+
+
+initMeta : @$\mathbb{N}$@  @$\rightarrow$@ Maybe @$\mathbb{N}$@ @$\rightarrow$@ N.CodeSegment Context Context @$\rightarrow$@ Meta
+initMeta n mn code = record { context = record { n = n ; element = mn}
+                         ; stack   = emptySingleLinkedStack
+                         ; nextCS  = code
+                         }
+
+n-push-cs-exec = M.exec (n-push {meta} 3) meta
+  where
+    meta = (initMeta 5 (just 9) pushNum)
+
+
+n-push-cs-exec-equiv : n-push-cs-exec @$\equiv$@ record { nextCS  = pushNum
+                                                ; context = record {n = 2 ; element = just 3}
+                                                ; stack   = record {top = just (cons 4 (just (cons 5 (just (cons 9 nothing)))))}}
+n-push-cs-exec-equiv = refl
+
+
+n-pop-cs-exec = M.exec (n-pop {meta} 4) 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 @$\equiv$@ 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
+
+
+open @$\equiv$@-Reasoning
+
+id-meta : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Meta
+id-meta n e s = record { context = record {n = n ; element = just e}
+                       ; nextCS = (N.cs id) ; stack = s}
+
+exec-comp : (f g : M.CodeSegment Meta Meta) (m : Meta) @$\rightarrow$@ M.exec (M.csComp {m} f g) m @$\equiv$@ M.exec f (M.exec g m)
+exec-comp (M.cs x) (M.cs _) m = refl
+
+
+push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@  @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Element @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@
+push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta @$\equiv$@ meta
+  where
+    meta = id-meta n e record {top = just (cons x (just s))}
+
+push-pop : (n e x : @$\mathbb{N}$@) @$\rightarrow$@ (s : Element @$\mathbb{N}$@) @$\rightarrow$@  push-pop-type n e x s
+push-pop n e x s = refl
+
+
+
+pop-n-push-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@
+pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta
+                         @$\equiv$@ M.exec (n-push {meta} n) meta
+  where
+    meta = id-meta cn ce s
+
+pop-n-push : (n cn ce : @$\mathbb{N}$@) @$\rightarrow$@ (s : SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ pop-n-push-type n cn ce s
+
+pop-n-push zero cn ce s    = refl
+pop-n-push (suc n) cn ce s = begin
+  M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc (suc n)))) (id-meta cn ce s)
+  @$\equiv$@@$\langle$@ refl @$\rangle$@
+  M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce))) (id-meta cn ce s)
+  @$\equiv$@@$\langle$@ exec-comp (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s) @$\rangle$@                        
+  M.exec (M.cs popOnce) (M.exec (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s))
+  @$\equiv$@@$\langle$@ cong (\x @$\rightarrow$@ M.exec (M.cs popOnce) x) (exec-comp (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce) (id-meta cn ce s)) @$\rangle$@
+  M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s)))
+  @$\equiv$@@$\langle$@ refl @$\rangle$@                                                                                                          
+  M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})))
+  @$\equiv$@@$\langle$@ sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) @$\rangle$@
+  M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
+  @$\equiv$@@$\langle$@ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) @$\rangle$@
+  M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
+  @$\equiv$@@$\langle$@ refl @$\rangle$@
+  M.exec (n-push n) (pushOnce (id-meta cn ce s))
+  @$\equiv$@@$\langle$@ refl @$\rangle$@
+  M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s))
+  @$\equiv$@@$\langle$@ refl @$\rangle$@
+  M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)
+  @$\blacksquare$@
+
+
+
+n-push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@  @$\mathbb{N}$@  @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@
+n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta @$\equiv$@ meta
+  where
+    meta = id-meta cn ce st
+
+n-push-pop : (n cn ce : @$\mathbb{N}$@) @$\rightarrow$@ (s : SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ n-push-pop-type n cn ce s
+n-push-pop zero    cn ce s = refl
+n-push-pop (suc n) cn ce s = begin
+  M.exec (M.csComp {id-meta cn ce s} (n-pop {id-meta cn ce s}  (suc n)) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)
+  @$\equiv$@@$\langle$@ refl @$\rangle$@
+  M.exec (M.csComp  {id-meta cn ce s}  (M.cs (\m @$\rightarrow$@ M.exec (n-pop {id-meta cn ce s} n) (popOnce m))) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)
+  @$\equiv$@@$\langle$@ exec-comp (M.cs (\m @$\rightarrow$@ M.exec (n-pop n) (popOnce m))) (n-push {id-meta cn ce s}  (suc n))  (id-meta cn ce s) @$\rangle$@
+  M.exec (M.cs (\m @$\rightarrow$@ M.exec (n-pop  {id-meta cn ce s}  n) (popOnce m))) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))
+  @$\equiv$@@$\langle$@ refl @$\rangle$@
+  M.exec (n-pop n) (popOnce (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)))
+  @$\equiv$@@$\langle$@ refl @$\rangle$@
+  M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)))
+  @$\equiv$@@$\langle$@ cong (\x @$\rightarrow$@ M.exec (n-pop  {id-meta cn ce s}  n) x) (sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce s}  (suc n)) (id-meta cn ce s))) @$\rangle$@
+  M.exec (n-pop n) (M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s))
+  @$\equiv$@@$\langle$@ cong (\x @$\rightarrow$@ M.exec (n-pop {id-meta cn ce s}  n) x) (pop-n-push n cn ce s) @$\rangle$@
+  M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s))
+  @$\equiv$@@$\langle$@ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) @$\rangle$@
+  M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s)
+  @$\equiv$@@$\langle$@ n-push-pop n cn ce s @$\rangle$@
+  id-meta cn ce s
+  @$\blacksquare$@
+