changeset 61:7af6c894f411

Trying define n-push
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sat, 14 Jan 2017 02:10:28 +0000
parents bd428bd6b394
children 29b069a0c409
files cbc/stack-subtype-sample.agda cbc/stack-subtype.agda
diffstat 2 files changed, 73 insertions(+), 33 deletions(-) [+]
line wrap: on
line diff
--- a/cbc/stack-subtype-sample.agda	Sat Jan 14 00:00:40 2017 +0000
+++ b/cbc/stack-subtype-sample.agda	Sat Jan 14 02:10:28 2017 +0000
@@ -1,12 +1,13 @@
 module stack-subtype-sample where
 
+open import Function
 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 (Meta Context) as M
+open import subtype Context  as N
+open import subtype Meta     as M
 
 
 record Num : Set where
@@ -29,17 +30,9 @@
 plus3CS = N.cs plus3
 
 
-setNext : {X Y : Set} {{x : N.DataSegment X}} {{y : N.DataSegment Y}}
-        -> (N.CodeSegment X Y) -> M.CodeSegment (Meta Context) (Meta Context)
-setNext c = M.cs (\mc -> record mc {nextCS = liftContext c})
 
-setElement : ℕ -> M.CodeSegment (Meta Context) (Meta Context)
-setElement x = M.cs (\mc -> record mc {context = record (Meta.context mc) {element = just x}})
-
-
-
-plus5AndPushWithPlus3 : {mc : Meta Context} {{_ : N.DataSegment Num}}
-               -> M.CodeSegment Num (Meta Context)
+plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}}
+               -> M.CodeSegment Num (Meta)
 plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} )
   where
     co    = Meta.context mc
@@ -50,7 +43,7 @@
 
 
 
-push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  Meta Context
+push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  Meta
 push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc
   where
     con  = record { n = 4 ; element = just 0}
@@ -64,7 +57,7 @@
 push-sample-equiv = refl
 
 
-pushed-sample : {m : Meta Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  Meta Context
+pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  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}
@@ -73,7 +66,7 @@
 
 
 
-pushed-sample-equiv : {m : Meta Context} ->
+pushed-sample-equiv : {m : Meta} ->
                       pushed-sample {m} ≡ record { nextCS  = liftContext plus3CS
                                                   ; stack   = record { top = just (cons 0 nothing) }
                                                   ; context = record { n   = 12} }
@@ -81,6 +74,41 @@
 
 
 
-n-push : {{_ : M.DataSegment (Meta Context)}} -> Meta Context -> Meta Context
-n-push m = M.csComp (pushSingleLinkedStackCS) (setElement ?)
+pushNum : N.CodeSegment Context Context
+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
 
+
+
+n-push-cs : M.CodeSegment Meta Meta
+n-push-cs = M.cs n-push
+
+
+initMeta : ℕ -> N.CodeSegment Context Context -> Meta
+initMeta n code = record { context = record { n = n ; element = nothing}
+                         ; stack   = emptySingleLinkedStack
+                         ; nextCS  = code
+                         }
+
+n-push-cs-exec = M.exec n-push-cs (initMeta 4 pushNum)
+
+
+n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS  = {!!}
+                                                ; context = {!!}
+                                                ; stack   = record { top = {!!} }}
+n-push-cs-exec-equiv = refl
--- a/cbc/stack-subtype.agda	Sat Jan 14 00:00:40 2017 +0000
+++ b/cbc/stack-subtype.agda	Sat Jan 14 02:10:28 2017 +0000
@@ -2,6 +2,7 @@
 open import Data.Maybe
 open import Data.Product
 open import Data.Nat hiding (suc)
+open import Function
 
 module stack-subtype (A : Set) where
 
@@ -23,11 +24,12 @@
 
 record Context : Set where
   field
+    -- fields for concrete data segments
+    n       : ℕ 
     -- fields for stack
     element : Maybe A
-    stack   : SingleLinkedStack A
-    -- fields for data segments
-    n       : ℕ
+
+
 
 
 
@@ -40,8 +42,11 @@
 
 record Meta  : Set₁ where
   field
+    -- context as set of data segments
     context : Context
+    stack   : SingleLinkedStack A  
     nextCS  : N.CodeSegment Context Context
+    
 
     
 
@@ -69,28 +74,30 @@
 
 
 pushSingleLinkedStack : Meta -> Meta
-pushSingleLinkedStack m = M.exec (liftMeta n) (record m {context = record c {stack = (push s e)}})
+pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
   where
-    c = (Meta.context m)
-    n = Meta.nextCS     m
-    e = Context.element c
-    s = Context.stack   c
+    n = Meta.nextCS m
+    s = Meta.stack  m
+    e = Context.element (Meta.context m)
     push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
     push s nothing  = s
     push s (just x) = record {top = just (cons x (top s))}
 
 
+
 popSingleLinkedStack : Meta -> Meta
-popSingleLinkedStack m = M.exec (liftMeta n) (record m { context = record c { stack = (st c) ; element = (elem c)}})
+popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
   where
     n = Meta.nextCS m
-    c = Meta.context m
-    elem : Context -> Maybe A
+    con  = Meta.context m
+    elem : Meta -> Maybe A
     elem record {stack = record { top = (just (cons x _)) }} = just x
-    elem record {stack = record { top = nothing } }          = nothing
-    st : Context -> SingleLinkedStack A
+    elem record {stack = record { top = nothing           }} = nothing
+    st : Meta -> SingleLinkedStack A
     st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
-    st record {stack = record { top = nothing } }          = record {top = nothing}
+    st record {stack = record { top = nothing           }} = record {top = nothing}
+    
+
 
 
 pushSingleLinkedStackCS : M.CodeSegment Meta Meta
@@ -103,9 +110,14 @@
 -- for sample
 
 firstContext : Context
-firstContext = record {stack = emptySingleLinkedStack ; element = nothing ; n = 0}
+firstContext = record {element = nothing ; n = 0}
 
 
 firstMeta : Meta 
-firstMeta = record {nextCS = (N.cs (\m -> m)) ; context = firstContext}
+firstMeta = record { context = firstContext
+                   ; stack = emptySingleLinkedStack
+                   ; nextCS = (N.cs (\m -> m))
+                   }
 
+
+