Mercurial > hg > Members > atton > agda-proofs

comparison cbc/stack-subtype.agda @ 54:fa95e3070138

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define SingleLinkedStack using subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 11 Jan 2017 10:56:13 +0000
parents 6af88ee5c4ca
children 81c6779583b6
comparison
equal deleted inserted replaced
53:6af88ee5c4ca 54:fa95e3070138
1 open import Level 1 open import Level hiding (lift)
2 open import Data.Maybe 2 open import Data.Maybe
3 open import Data.Product 3 open import Data.Product
4 open import Data.Nat 4 open import Data.Nat hiding (suc)
5 5
6 module stack-subtype (A : Set) where 6 module stack-subtype (A : Set) where
7 7
8 -- data definitions 8 -- data definitions
9 9
21 top : Maybe (Element a) 21 top : Maybe (Element a)
22 open SingleLinkedStack 22 open SingleLinkedStack
23 23
24 record Context : Set where 24 record Context : Set where
25 field 25 field
26 stack : SingleLinkedStack A
27 element : Maybe A 26 element : Maybe A
28 n : ℕ 27 n : ℕ
29 28
30 open import subtype Context 29
30 open import subtype Context as N
31 31
32 instance 32 instance
33 ContextIsDataSegment : DataSegment Context 33 ContextIsDataSegment : N.DataSegment Context
34 ContextIsDataSegment = record {get = (\x -> x) ; set = (\_ c -> c)} 34 ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)}
35
36
37 record MetaContext (X : Set) {{_ : N.DataSegment X}} : Set₁ where
38 field
39 context : Context
40 stack : SingleLinkedStack A
41 nextCS : N.CodeSegment X X
35 42
36 43
37 44
45
46 open import subtype (MetaContext Context) as M
47
48 instance
49 MetaContextIncludeContext : M.DataSegment Context
50 MetaContextIncludeContext = record { get = MetaContext.context
51 ; set = (\m c -> record m {context = c}) }
52
53 MetaContextIsMetaDataSegment : M.DataSegment (MetaContext Context)
54 MetaContextIsMetaDataSegment = record { get = (\m -> m) ; set = (\_ m -> m) }
55
56
57 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
58 liftMeta (N.cs f) = M.cs f
59
60 liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
61 liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c)))
62
38 -- definition based from Gears(209:5708390a9d88) src/parallel_execution 63 -- definition based from Gears(209:5708390a9d88) src/parallel_execution
39 64
40 emptySingleLinkedStack : SingleLinkedStack A 65 emptySingleLinkedStack : SingleLinkedStack A
41 emptySingleLinkedStack = record {top = nothing} 66 emptySingleLinkedStack = record {top = nothing}
42 67
43 pushSingleLinkedStack : Context -> Context 68
44 pushSingleLinkedStack c = record c { stack = (push c) ; element = nothing} 69 pushSingleLinkedStack : MetaContext Context -> MetaContext Context
70 pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
45 where 71 where
46 push : Context -> SingleLinkedStack A 72 n = MetaContext.nextCS m
47 push record { stack = stack ; element = nothing } = stack 73 e = Context.element (MetaContext.context m)
48 push record { stack = stack ; element = (just x) } = stack1 74 s = MetaContext.stack m
49 where 75 push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
50 el = cons x (top stack) 76 push s nothing = s
51 stack1 = record {top = just el} 77 push s (just x) = record {top = just (cons x (top s))}
52 78
53 popSingleLinkedStack : Context -> Context 79
54 popSingleLinkedStack c = record c {element = (elem c) ; stack = (popdStack c)} 80
81 popSingleLinkedStack : MetaContext Context -> MetaContext Context
82 popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
55 where 83 where
56 elem : Context -> Maybe A 84 n = MetaContext.nextCS m
57 elem record { stack = record { top = (just (cons x _)) } } = just x 85 con = MetaContext.context m
58 elem record { stack = record { top = nothing } } = nothing 86 elem : MetaContext Context -> Maybe A
59 popdStack : Context -> SingleLinkedStack A 87 elem record {stack = record { top = (just (cons x _)) }} = just x
60 popdStack record { stack = record { top = (just (cons _ s)) } } = record { top = s } 88 elem record {stack = record { top = nothing }} = nothing
61 popdStack record { stack = record { top = nothing } } = record { top = nothing } 89 st : MetaContext Context -> SingleLinkedStack A
90 st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
91 st record {stack = record { top = nothing }} = record {top = nothing}
92
93 pushSingleLinkedStackCS : M.CodeSegment (MetaContext Context) (MetaContext Context)
94 pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
95
96 popSingleLinkedStackCS : M.CodeSegment (MetaContext Context) (MetaContext Context)
97 popSingleLinkedStackCS = M.cs popSingleLinkedStack
98
99
100
101
62 102
63 -- sample 103 -- sample
64 104
105 record Num : Set where
106 field
107 num : ℕ
65 108
66 pushCS = cs pushSingleLinkedStack 109 instance
67 popCS = cs popSingleLinkedStack 110 NumIsNormalDataSegment : N.DataSegment Num
111 NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c})
112 ; set = (\c n -> record c {n = Num.num n})}
68 113
69 114
70 -- stack 115 plus3 : Num -> Num
71 record Stack {X Y : Set} (stackImpl : Set -> Set) : Set where 116 plus3 record { num = n } = record {num = n + 3}
72 field
73 stack : stackImpl A
74 push : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y
75 pop : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y
76 117
118 plus3CS : N.CodeSegment Num Num
119 plus3CS = N.cs plus3
120
121
122 setNext : {X Y : Set} {{x : N.DataSegment X}} {{y : N.DataSegment Y}}
123 -> (N.CodeSegment X Y) -> M.CodeSegment (MetaContext Context) (MetaContext Context)
124 setNext c = M.cs (\mc -> record mc {nextCS = liftContext c})
125
126
127
128
129
130 pushPlus3CS : {mc : MetaContext Context} -> M.CodeSegment (MetaContext Context) (MetaContext Context)
131 pushPlus3CS {mc} = M.csComp {mc} pushSingleLinkedStackCS (setNext plus3CS)