# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1484165461 0
# Node ID ddcd652969e071865c3988519a9064f781aceca5
# Parent  81c6779583b6ed17a1425615f15f846db4a4c4f8
Add executable subtype-stack

diff -r 81c6779583b6 -r ddcd652969e0 cbc/stack-subtype-sample.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/stack-subtype-sample.agda	Wed Jan 11 20:11:01 2017 +0000
@@ -0,0 +1,81 @@
+module stack-subtype-sample where
+
+open import Data.Nat
+open import Data.Maybe
+open import Relation.Binary.PropositionalEquality
+
+open import stack-subtype ℕ  as S
+open import subtype Context as N
+open import subtype (MetaContext Context) as M
+
+
+record Num : Set where
+  field
+    num : ℕ
+
+instance
+  NumIsNormalDataSegment : N.DataSegment Num
+  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}})}
+
+
+plus3 : Num -> Num
+plus3 record { num = n } = record {num = n + 3}
+
+plus3CS : N.CodeSegment Num Num
+plus3CS = N.cs plus3
+
+
+setNext : {X Y : Set} {{x : N.DataSegment X}} {{y : N.DataSegment Y}}
+        -> (N.CodeSegment X Y) -> M.CodeSegment (MetaContext Context) (MetaContext 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}})
+
+
+
+plus5AndPushWithPlus3 : {mc : MetaContext Context} {{_ : N.DataSegment Num}}
+               -> M.CodeSegment Num (MetaContext Context)
+plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} )
+  where
+    co    = MetaContext.context mc
+    con : Num -> Context
+    con record { num = num } = N.DataSegment.set nn co record {num = num + 5}
+    st    = MetaContext.stack mc
+
+
+
+
+push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  MetaContext Context
+push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc
+  where
+    con  = record { n = 4 ; element = just 0}
+    code = N.cs (\c -> c)
+    mc   = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
+
+
+push-sample-equiv : push-sample ≡ record { nextCS  = liftContext plus3CS
+                                          ; stack   = record { top = nothing}
+                                          ; context = record { n = 9} }
+push-sample-equiv = refl
+
+
+pushed-sample : {m : MetaContext Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  MetaContext 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}
+    code = N.cs (\c -> c)
+    mc   = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
+
+
+
+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 = refl
+
+
diff -r 81c6779583b6 -r ddcd652969e0 cbc/stack-subtype.agda
--- a/cbc/stack-subtype.agda	Wed Jan 11 13:37:23 2017 +0000
+++ b/cbc/stack-subtype.agda	Wed Jan 11 20:11:01 2017 +0000
@@ -97,49 +97,11 @@
 popSingleLinkedStackCS = M.cs popSingleLinkedStack
 
 
-
-
-
--- sample
-
-record Num : Set where
-  field
-    num : ℕ
+-- for sample
 
-instance
-  NumIsNormalDataSegment : N.DataSegment Num
-  NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c})
-                                  ; set = (\c n -> record c {n = Num.num n})}
-
-
-plus3 : Num -> Num
-plus3 record { num = n } = record {num = n + 3}
-
-plus3CS : N.CodeSegment Num Num
-plus3CS = N.cs plus3
+firstContext : Context
+firstContext = record { element = nothing ; n = 0}
 
 
-setNext : {X Y : Set} {{x : N.DataSegment X}} {{y : N.DataSegment Y}}
-        -> (N.CodeSegment X Y) -> M.CodeSegment (MetaContext Context) (MetaContext Context)
-setNext c = M.cs (\mc -> record mc {nextCS = liftContext c})
-
-setElement : A -> M.CodeSegment (MetaContext Context) (MetaContext Context)
-setElement x = M.cs (\mc -> record mc {context = record (MetaContext.context mc) {element = just x}})
-
-pushPlus3CS : {mc : MetaContext Context} -> M.CodeSegment (MetaContext Context) (MetaContext Context)
-pushPlus3CS {mc} = M.csComp {mc} pushSingleLinkedStackCS (setNext plus3CS)
-
-plus5AndPush : {mc : MetaContext Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}}
-               -> M.CodeSegment Num (MetaContext Context)
-plus5AndPush {mc} {{nn}} = M.cs (\n -> record {context = con ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} )
-  where
-    con  = MetaContext.context mc
-    st   = MetaContext.stack mc
-
-
-push-sample : {{_ : M.DataSegment Num}} -> MetaContext Context
-push-sample = M.exec (plus5AndPush {mc}) mc
-  where
-    con  = record { n = 4 ; element = nothing}
-    code = N.cs (\c -> c)
-    mc   = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
+firstMetaContext : MetaContext Context
+firstMetaContext = record {stack = emptySingleLinkedStack ; nextCS = (N.cs (\m -> m)) ; context = firstContext}