Mercurial > hg > Members > atton > agda-proofs

annotate cbc/stack-subtype-sample.agda @ 60:bd428bd6b394

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define n-push/n-pop
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sat, 14 Jan 2017 00:00:40 +0000
parents ddcd652969e0
children 7af6c894f411
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
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.Nat
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Maybe
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Relation.Binary.PropositionalEquality
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import stack-subtype ℕ as S
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import subtype Context as N
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
9 open import subtype (Meta Context) as M
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
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 record Num : Set where
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 field
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 num : ℕ
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 instance
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 NumIsNormalDataSegment : N.DataSegment Num
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 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
19 ; 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
20 NumIsMetaDataSegment : M.DataSegment Num
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
21 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
22 ; 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
23
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 plus3 : Num -> Num
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 plus3 record { num = n } = record {num = n + 3}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 plus3CS : N.CodeSegment Num Num
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 plus3CS = N.cs plus3
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
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 setNext : {X Y : Set} {{x : N.DataSegment X}} {{y : N.DataSegment Y}}
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
33 -> (N.CodeSegment X Y) -> M.CodeSegment (Meta Context) (Meta Context)
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 setNext c = M.cs (\mc -> record mc {nextCS = liftContext c})
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
36 setElement : ℕ -> M.CodeSegment (Meta Context) (Meta Context)
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
37 setElement x = M.cs (\mc -> record mc {context = record (Meta.context mc) {element = just x}})
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
41 plus5AndPushWithPlus3 : {mc : Meta Context} {{_ : N.DataSegment Num}}
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
42 -> M.CodeSegment Num (Meta Context)
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 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
44 where
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
45 co = Meta.context mc
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 con : Num -> Context
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 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
48 st = Meta.stack mc
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
49
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
53 push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta Context
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 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
55 where
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 con = record { n = 4 ; element = just 0}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 code = N.cs (\c -> c)
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 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
62 ; stack = record { top = nothing}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 ; context = record { n = 9} }
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 push-sample-equiv = refl
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
67 pushed-sample : {m : Meta Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta Context
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 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
69 where
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 con = record { n = 4 ; element = just 0}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 code = N.cs (\c -> c)
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
73
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 pushed-sample-equiv : {m : Meta Context} ->
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
77 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
78 ; 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
79 ; context = record { n = 12} }
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 pushed-sample-equiv = refl
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
81
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
83
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
84 n-push : {{_ : M.DataSegment (Meta Context)}} -> Meta Context -> Meta Context
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
85 n-push m = M.csComp (pushSingleLinkedStackCS) (setElement ?)
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
86