Mercurial > hg > Members > atton > agda-proofs

comparison cbc/stack-subtype-sample.agda @ 61:7af6c894f411

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define n-push
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sat, 14 Jan 2017 02:10:28 +0000
parents bd428bd6b394
children 29b069a0c409
comparison
equal deleted inserted replaced
60:bd428bd6b394 61:7af6c894f411
1 module stack-subtype-sample where 1 module stack-subtype-sample where
2 2
3 open import Function
3 open import Data.Nat 4 open import Data.Nat
4 open import Data.Maybe 5 open import Data.Maybe
5 open import Relation.Binary.PropositionalEquality 6 open import Relation.Binary.PropositionalEquality
6 7
7 open import stack-subtype ℕ as S 8 open import stack-subtype ℕ as S
8 open import subtype Context as N 9 open import subtype Context as N
9 open import subtype (Meta Context) as M 10 open import subtype Meta as M
10 11
11 12
12 record Num : Set where 13 record Num : Set where
13 field 14 field
14 num : ℕ 15 num : ℕ
27 28
28 plus3CS : N.CodeSegment Num Num 29 plus3CS : N.CodeSegment Num Num
29 plus3CS = N.cs plus3 30 plus3CS = N.cs plus3
30 31
31 32
32 setNext : {X Y : Set} {{x : N.DataSegment X}} {{y : N.DataSegment Y}}
33 -> (N.CodeSegment X Y) -> M.CodeSegment (Meta Context) (Meta Context)
34 setNext c = M.cs (\mc -> record mc {nextCS = liftContext c})
35 33
36 setElement : ℕ -> M.CodeSegment (Meta Context) (Meta Context) 34 plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}}
37 setElement x = M.cs (\mc -> record mc {context = record (Meta.context mc) {element = just x}}) 35 -> M.CodeSegment Num (Meta)
38
39
40
41 plus5AndPushWithPlus3 : {mc : Meta Context} {{_ : N.DataSegment Num}}
42 -> M.CodeSegment Num (Meta Context)
43 plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} ) 36 plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} )
44 where 37 where
45 co = Meta.context mc 38 co = Meta.context mc
46 con : Num -> Context 39 con : Num -> Context
47 con record { num = num } = N.DataSegment.set nn co record {num = num + 5} 40 con record { num = num } = N.DataSegment.set nn co record {num = num + 5}
48 st = Meta.stack mc 41 st = Meta.stack mc
49 42
50 43
51 44
52 45
53 push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta Context 46 push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta
54 push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc 47 push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc
55 where 48 where
56 con = record { n = 4 ; element = just 0} 49 con = record { n = 4 ; element = just 0}
57 code = N.cs (\c -> c) 50 code = N.cs (\c -> c)
58 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code} 51 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
62 ; stack = record { top = nothing} 55 ; stack = record { top = nothing}
63 ; context = record { n = 9} } 56 ; context = record { n = 9} }
64 push-sample-equiv = refl 57 push-sample-equiv = refl
65 58
66 59
67 pushed-sample : {m : Meta Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta Context 60 pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta
68 pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc 61 pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc
69 where 62 where
70 con = record { n = 4 ; element = just 0} 63 con = record { n = 4 ; element = just 0}
71 code = N.cs (\c -> c) 64 code = N.cs (\c -> c)
72 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code} 65 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
73 66
74 67
75 68
76 pushed-sample-equiv : {m : Meta Context} -> 69 pushed-sample-equiv : {m : Meta} ->
77 pushed-sample {m} ≡ record { nextCS = liftContext plus3CS 70 pushed-sample {m} ≡ record { nextCS = liftContext plus3CS
78 ; stack = record { top = just (cons 0 nothing) } 71 ; stack = record { top = just (cons 0 nothing) }
79 ; context = record { n = 12} } 72 ; context = record { n = 12} }
80 pushed-sample-equiv = refl 73 pushed-sample-equiv = refl
81 74
82 75
83 76
84 n-push : {{_ : M.DataSegment (Meta Context)}} -> Meta Context -> Meta Context 77 pushNum : N.CodeSegment Context Context
85 n-push m = M.csComp (pushSingleLinkedStackCS) (setElement ?) 78 pushNum = N.cs pn
79 where
80 pn : Context -> Context
81 pn record { n = n } = record { n = n ; element = just n}
86 82
83 n-push : {{_ : N.DataSegment Num}} -> Meta -> Meta
84 n-push {{x}} record { context = record { n = zero ; element = el } ; stack = st ; nextCS = code} =
85 M.exec pushSingleLinkedStackCS record { context = record { n = zero ; element = el }
86 ; stack = st ; nextCS = code}
87 n-push {{x}} record { context = record { n = (suc n) ; element = el } ; stack = st ; nextCS = code} =
88 n-push {{x}} record {context = record {n = n ; element = e} ; stack = s ; nextCS = c}
89 where
90 pushedMeta = M.exec pushSingleLinkedStackCS record { context = record { n = (suc n) ; element = el}
91 ; stack = st ; nextCS = code}
92 e = Context.element (Meta.context pushedMeta)
93 s = Meta.stack pushedMeta
94 c = Meta.nextCS pushedMeta
95
96
97
98 n-push-cs : M.CodeSegment Meta Meta
99 n-push-cs = M.cs n-push
100
101
102 initMeta : ℕ -> N.CodeSegment Context Context -> Meta
103 initMeta n code = record { context = record { n = n ; element = nothing}
104 ; stack = emptySingleLinkedStack
105 ; nextCS = code
106 }
107
108 n-push-cs-exec = M.exec n-push-cs (initMeta 4 pushNum)
109
110
111 n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS = {!!}
112 ; context = {!!}
113 ; stack = record { top = {!!} }}
114 n-push-cs-exec-equiv = refl