annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Data.Maybe
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.Product
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Nat
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 module stack-subtype (A : Set) where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 -- data definitions
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 data Element (a : Set) : Set where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 cons : a -> Maybe (Element a) -> Element a
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 datum : {a : Set} -> Element a -> a
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 datum (cons a _) = a
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 next : {a : Set} -> Element a -> Maybe (Element a)
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 next (cons _ n) = n
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 record SingleLinkedStack (a : Set) : Set where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 field
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 top : Maybe (Element a)
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 open SingleLinkedStack
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 record Context : Set where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 field
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 stack : SingleLinkedStack A
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 element : Maybe A
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 n : ℕ
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 open import subtype Context
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 instance
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 yo : DataSegment Context
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 yo = record {get = (\x -> x) ; set = (\_ c -> c)}
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 -- definition based from Gears(209:5708390a9d88) src/parallel_execution
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 emptySingleLinkedStack : SingleLinkedStack A
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 emptySingleLinkedStack = record {top = nothing}
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 pushSingleLinkedStack : Context -> Context
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 pushSingleLinkedStack c = record c { stack = (push c) ; element = nothing}
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 push : Context -> SingleLinkedStack A
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 push record { stack = stack ; element = nothing } = stack
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 push record { stack = stack ; element = (just x) } = stack1
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 el = cons x (top stack)
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 stack1 = record {top = just el}
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 popSingleLinkedStack : Context -> Context
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 popSingleLinkedStack c = record c {element = (elem c) ; stack = (popdStack c)}
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 elem : Context -> Maybe A
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 elem record { stack = record { top = (just (cons x _)) } } = just x
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 elem record { stack = record { top = nothing } } = nothing
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 popdStack : Context -> SingleLinkedStack A
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 popdStack record { stack = record { top = (just (cons _ s)) } } = record { top = s }
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 popdStack record { stack = record { top = nothing } } = record { top = nothing }
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 -- sample
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 pushCS = cs pushSingleLinkedStack
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 popCS = cs popSingleLinkedStack
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
68
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
69
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 -- stack
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 record Stack {X Y : Set} (stackImpl : Set -> Set) : Set where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 field
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 stack : stackImpl A
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 push : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 pop : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
76