Mercurial > hg > GearsTemplate

comparison src/parallel_execution/stack.agda @ 427:07ccd411ad70

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix interface in agda
author ryokka
date Sat, 07 Oct 2017 18:22:31 +0900
parents 78b28c8ffff2
children c3202635c20a
comparison
equal deleted inserted replaced
426:02313bbfe900 427:07ccd411ad70
17 record Stack {a t : Set} (stackImpl : Set) : Set where 17 record Stack {a t : Set} (stackImpl : Set) : Set where
18 field 18 field
19 stack : stackImpl 19 stack : stackImpl
20 push : stackImpl -> a -> (stackImpl -> t) -> t 20 push : stackImpl -> a -> (stackImpl -> t) -> t
21 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t 21 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t
22
23 pushStack : {a t : Set} -> Stack -> a -> (Stack -> t) -> t
24 pushStack {a} {t} s0 d next = (stackImpl s0) (stack s0) d (\s1 -> next (record s0 {stack = s1;} ))
25
26 popStack : {a t : Set} -> Stack -> (Stack -> t) -> t
27 popStack {a} {t} s0 next = (stackImpl s0) (stack s0) (\s1 -> next s0)
28
22 29
23 data Element (a : Set) : Set where 30 data Element (a : Set) : Set where
24 cons : a -> Maybe (Element a) -> Element a 31 cons : a -> Maybe (Element a) -> Element a
25 32
26 datum : {a : Set} -> Element a -> a 33 datum : {a : Set} -> Element a -> a