# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1484039095 0
# Node ID 4880184e4ab5de10ba8037685f7f64f0b22e695f
# Parent  16e27df74ec5ee6a69826d81bbb55fc4bcd95826
Define push/pop using subtype

diff -r 16e27df74ec5 -r 4880184e4ab5 cbc/stack-subtype.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/stack-subtype.agda	Tue Jan 10 09:04:55 2017 +0000
@@ -0,0 +1,76 @@
+open import Level
+open import Data.Maybe
+open import Data.Product
+open import Data.Nat
+
+module stack-subtype (A : Set) where
+
+-- data definitions
+
+data Element (a : Set) : Set where
+  cons : a -> Maybe (Element a) -> Element a
+
+datum : {a : Set} -> Element a -> a
+datum (cons a _) = a
+
+next : {a : Set} -> Element a -> Maybe (Element a)
+next (cons _ n) = n
+
+record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+open SingleLinkedStack
+
+record Context : Set where
+  field
+    stack   : SingleLinkedStack A
+    element : Maybe A
+    n       : ℕ 
+
+open import subtype Context
+
+instance
+  yo : DataSegment Context
+  yo = record {get = (\x -> x) ; set = (\_ c -> c)}
+
+
+
+-- definition based from Gears(209:5708390a9d88) src/parallel_execution
+
+emptySingleLinkedStack : SingleLinkedStack A
+emptySingleLinkedStack = record {top = nothing}
+
+pushSingleLinkedStack : Context -> Context
+pushSingleLinkedStack c = record c { stack = (push c) ; element = nothing}
+  where
+    push : Context -> SingleLinkedStack A
+    push record { stack = stack ; element = nothing }  = stack
+    push record { stack = stack ; element = (just x) } = stack1
+      where
+        el = cons x (top stack)
+        stack1 = record {top = just el}
+
+popSingleLinkedStack : Context -> Context
+popSingleLinkedStack c = record c {element = (elem c) ; stack =  (popdStack c)}
+  where
+    elem : Context -> Maybe A
+    elem record { stack = record { top = (just (cons x _)) } } = just x
+    elem record { stack = record { top = nothing } }           = nothing
+    popdStack : Context -> SingleLinkedStack A
+    popdStack record { stack = record { top = (just (cons _ s)) } } = record { top = s }
+    popdStack record { stack = record { top = nothing } }           = record { top = nothing }
+
+-- sample
+
+
+pushCS = cs pushSingleLinkedStack
+popCS  = cs popSingleLinkedStack
+
+
+-- stack
+record Stack {X Y : Set} (stackImpl : Set -> Set) : Set where
+  field
+    stack : stackImpl A
+    push  : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y
+    pop   : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y
+
diff -r 16e27df74ec5 -r 4880184e4ab5 cbc/subtype-sample.agda
--- a/cbc/subtype-sample.agda	Tue Jan 10 02:04:55 2017 +0000
+++ b/cbc/subtype-sample.agda	Tue Jan 10 09:04:55 2017 +0000
@@ -15,6 +15,8 @@
     signature : String
     
 open import subtype Context
+
+
 record LoopCounter : Set where
   field
     count : ℕ
diff -r 16e27df74ec5 -r 4880184e4ab5 cbc/subtype.agda
--- a/cbc/subtype.agda	Tue Jan 10 02:04:55 2017 +0000
+++ b/cbc/subtype.agda	Tue Jan 10 09:04:55 2017 +0000
@@ -1,27 +1,28 @@
-module subtype (Context : Set) where
-
+open import Level
 open import Relation.Binary.PropositionalEquality
 
+module subtype {l : Level} (Context : Set l) where
 
-record DataSegment (A : Set) : Set where
+
+record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where
   field
     get : Context -> A
     set : Context -> A -> Context
 open DataSegment
 
-data CodeSegment (A B : Set) : Set where
+data CodeSegment {ll : Level} (A B : Set ll) : Set (l ⊔ ll) where
   cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B
 
 
-exec : {I O : Set} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context
-exec {l} {{i}} {{o}}  (cs b) c = DataSegment.set o c (b (get i c))
+exec : {I O : Set l} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context
+exec {l} {{i}} {{o}}  (cs b) c = set o c (b (get i c))
 
 
-comp : {con : Context} -> {A B C D : Set} {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
+comp : {con : Context} -> {A B C D : Set l} {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
        -> (C -> D) -> (A -> B) -> A -> D
 comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
 
-csComp : {con : Context} {A B C D : Set}
+csComp : {con : Context} {A B C D : Set l}
          {{_ : 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)
@@ -29,7 +30,7 @@
 
 
 
-comp-associative : {A B C D E F : Set} {con : Context}
+comp-associative : {A B C D E F : Set l} {con : Context}
                    {{da : DataSegment A}} {{db : DataSegment B}} {{dc : DataSegment C}}
                    {{dd : DataSegment D}} {{de : DataSegment E}} {{df : DataSegment F}}
                    -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)