Mercurial > hg > Members > atton > agda-proofs

annotate cbc/stack-subtype-sample.agda @ 63:c3afde46a41d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define n-pop
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sat, 14 Jan 2017 02:35:33 +0000
parents 29b069a0c409
children 44d448a978d3
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module stack-subtype-sample where
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
3 open import Function
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Nat
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Maybe
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Relation.Binary.PropositionalEquality
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import stack-subtype ℕ as S
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
9 open import subtype Context as N
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
10 open import subtype Meta as M
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 record Num : Set where
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 field
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 num : ℕ
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 instance
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 NumIsNormalDataSegment : N.DataSegment Num
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c})
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 ; set = (\c n -> record c {n = Num.num n})}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 NumIsMetaDataSegment : M.DataSegment Num
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
22 NumIsMetaDataSegment = record { get = (\m -> record {num = Context.n (Meta.context m)})
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
23 ; set = (\m n -> record m {context = record (Meta.context m) {n = Num.num n}})}
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 plus3 : Num -> Num
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 plus3 record { num = n } = record {num = n + 3}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 plus3CS : N.CodeSegment Num Num
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 plus3CS = N.cs plus3
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
34 plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}}
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
35 -> M.CodeSegment Num (Meta)
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} )
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 where
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
38 co = Meta.context mc
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 con : Num -> Context
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 con record { num = num } = N.DataSegment.set nn co record {num = num + 5}
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
41 st = Meta.stack mc
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
46 push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 where
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 con = record { n = 4 ; element = just 0}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 code = N.cs (\c -> c)
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 push-sample-equiv : push-sample ≡ record { nextCS = liftContext plus3CS
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 ; stack = record { top = nothing}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 ; context = record { n = 9} }
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 push-sample-equiv = refl
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
60 pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 where
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 con = record { n = 4 ; element = just 0}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 code = N.cs (\c -> c)
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
67
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
68
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
69 pushed-sample-equiv : {m : Meta} ->
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
70 pushed-sample {m} ≡ record { nextCS = liftContext plus3CS
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
71 ; stack = record { top = just (cons 0 nothing) }
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
72 ; context = record { n = 12} }
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 pushed-sample-equiv = refl
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
75
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
76
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
77 pushNum : N.CodeSegment Context Context
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
78 pushNum = N.cs pn
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
79 where
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
80 pn : Context -> Context
62
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
81 pn record { n = n } = record { n = pred n ; element = just n}
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
82
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
83
62
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
84 pushOnce : Meta -> Meta
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
85 pushOnce m = M.exec pushSingleLinkedStackCS m
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
86
62
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
87 n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
88 n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} pushOnce
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
89 n-push {m} {{mm}} (suc n) = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-push {m} {{mm}} n) (M.cs {{mm}} {{mm}} pushOnce)
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
90
63
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
91 popOnce : Meta -> Meta
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
92 popOnce m = M.exec popSingleLinkedStackCS m
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
93
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
94 n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
95 n-pop {{mm}} (zero) = M.cs {{mm}} {{mm}} popOnce
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
96 n-pop {m} {{mm}} (suc n) = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-pop {m} {{mm}} n) (M.cs {{mm}} {{mm}} popOnce)
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
97
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
98
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
99
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
100
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
101 initMeta : ℕ -> N.CodeSegment Context Context -> Meta
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
102 initMeta n code = record { context = record { n = n ; element = nothing}
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
103 ; stack = emptySingleLinkedStack
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
104 ; nextCS = code
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
105 }
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
106
62
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
107 n-push-cs-exec = M.exec (n-push {meta} 2) meta
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
108 where
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
109 meta = (initMeta 5 pushNum)
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
110
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
111
62
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
112 n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS = pushNum
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
113 ; context = record {n = 2 ; element = just 3}
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
114 ; stack = record {top = just (cons 4 (just (cons 5 nothing)))}}
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
115 n-push-cs-exec-equiv = refl
62
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
116
63
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
117
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
118 n-pop-cs-exec = M.exec (n-pop {meta} 3) meta
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
119 where
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
120 meta = record { nextCS = N.cs id
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
121 ; context = record { n = 0 ; element = nothing}
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
122 ; stack = record {top = just (cons 9 (just (cons 8 (just (cons 7 (just (cons 6 (just (cons 5 nothing)))))))))}
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
123 }
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
124
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
125 n-pop-cs-exec-equiv : n-pop-cs-exec ≡ record { nextCS = N.cs id
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
126 ; context = record { n = 0 ; element = just 6}
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
127 ; stack = record { top = just (cons 5 nothing)}
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
128 }
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
129
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
130 n-pop-cs-exec-equiv = refl