Mercurial > hg > Members > atton > agda-proofs
annotate cbc/stack-subtype-sample.agda @ 56:ddcd652969e0
Add executable subtype-stack
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 11 Jan 2017 20:11:01 +0000 |
parents | |
children | bd428bd6b394 |
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 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import subtype (MetaContext Context) as M |
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 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 NumIsMetaDataSegment = record { get = (\m -> record {num = Context.n (MetaContext.context m)}) |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 ; set = (\m n -> record m {context = record (MetaContext.context m) {n = Num.num n}})} |
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}} |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 -> (N.CodeSegment X Y) -> M.CodeSegment (MetaContext Context) (MetaContext Context) |
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 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 setElement : ℕ -> M.CodeSegment (MetaContext Context) (MetaContext Context) |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 setElement x = M.cs (\mc -> record mc {context = record (MetaContext.context mc) {element = just x}}) |
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 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 plus5AndPushWithPlus3 : {mc : MetaContext Context} {{_ : N.DataSegment Num}} |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 -> M.CodeSegment Num (MetaContext Context) |
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 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 co = MetaContext.context mc |
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} |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 st = MetaContext.stack mc |
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 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> MetaContext Context |
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 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 pushed-sample : {m : MetaContext Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> MetaContext Context |
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 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 pushed-sample-equiv : {m : MetaContext Context} -> pushed-sample {m} ≡ record { nextCS = liftContext plus3CS |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
77 ; stack = record { top = just (cons 0 nothing) } |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 ; context = record { n = 12} } |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 pushed-sample-equiv = refl |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 |