diff cbc/stack-subtype.agda @ 52:4880184e4ab5

Define push/pop using subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 10 Jan 2017 09:04:55 +0000
parents
children 6af88ee5c4ca
line wrap: on
line diff
--- /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
+