Mercurial > hg > Members > atton > agda-proofs

comparison cbc/named-product.agda @ 47:49de29c12c7b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define code segment compose operator using type -> ds cast!
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 05 Jan 2017 03:07:32 +0000
parents af1fe3bd9f1e
children fe5755744071
comparison
equal deleted inserted replaced
46:af1fe3bd9f1e 47:49de29c12c7b
62 62
63 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" } 63 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
64 equiv = refl 64 equiv = refl
65 65
66 66
67
68 data CodeSegment (A B : Set) : (List Set) -> Set where 67 data CodeSegment (A B : Set) : (List Set) -> Set where
69 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (B ∷ A ∷ l) 68 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (B ∷ A ∷ l)
70 69
71 BasicCS : Set -> Set -> Set 70 BasicCS : Set -> Set -> Set
72 BasicCS A B = CodeSegment A B (A ∷ B ∷ []) 71 BasicCS A B = CodeSegment A B (A ∷ B ∷ [])
73 72
74 up : {A B : Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> Context -> B
75 up {{i}} {{o}} f c = f (Datum.get i c)
76
77
78 csInc : BasicCS LoopCounter LoopCounter
79 csInc = cs inc
80 73
81 74
82 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context 75 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
83 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (get i c)) 76 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (get i c))
84 77
85 --upCast : {A B : Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> (Datum A -> Datum B)
86 --upCast {{i}} {{o}} f a = record { get = (\c -> f (Datum.get a c))
87 -- ; set = (\c b -> Datum.set o c b)}
88 78
89 --downCast : {A B : Set} {{i : Datum A}} {{o : Datum B}} -> (Datum A -> Datum B) -> A -> B 79 comp : {con : Context} -> {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}}
90 --downCast {{i = record { get = get ; set = set }}} {{record { get = get₁ ; set = set₁ }}} f a = {!!}
91
92
93 apply : {A B : Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> Context -> B
94 apply {{i}} {{o}} f c = f (get i c)
95
96
97 _∘_ : {con : Context} -> {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}}
98 -> (C -> D) -> (A -> B) -> A -> D 80 -> (C -> D) -> (A -> B) -> A -> D
99 _∘_ {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x))) 81 comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
100 82
101 83
84 csInc : BasicCS LoopCounter LoopCounter
85 csInc = cs inc
102 86
103 87
104 88
105 89
106 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext 90 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext
107 equiv-exec = refl 91 equiv-exec = refl
108 92
109 93
110 _◎_ : {con : Context} {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}} {l ll : List Set} 94 csComp : {con : Context} {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}} {l ll : List Set}
111 -> CodeSegment C D (D ∷ C ∷ l) -> CodeSegment A B (B ∷ A ∷ ll) -> CodeSegment A D (D ∷ A ∷ C ∷ B ∷ (l ++ ll)) 95 -> CodeSegment C D (D ∷ C ∷ l) -> CodeSegment A B (B ∷ A ∷ ll) -> CodeSegment A D (D ∷ A ∷ C ∷ B ∷ (l ++ ll))
112 _◎_ {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} {l} {ll} (cs g) (cs f) 96 csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} {l} {ll} (cs g) (cs f)
113 = cs {l = (C ∷ B ∷ (l ++ ll))} {{da}} {{dd}} (_∘_ {con} {{da}} {{db}} {{dc}} {{dd}} g f) 97 = cs {l = (C ∷ B ∷ (l ++ ll))} {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f)
114 98
115 99
116 comp-sample : CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ []) 100 comp-sample : {c : Context} -> CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ [])
117 comp-sample = csInc ◎ csInc 101 comp-sample {c} = (csComp {c} csInc csInc)
118 102
119 103
120 apply-sample : Context 104 apply-sample : Context
121 apply-sample = exec comp-sample firstContext 105 apply-sample = exec (comp-sample {firstContext}) firstContext
122 106
123 {- 107
124 108
125 updateSignature : SignatureWithNum -> SignatureWithNum 109 updateSignature : SignatureWithNum -> SignatureWithNum
126 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num} 110 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num}
127 111
128 csUpdateSignature : basicCS SignatureWithNum SignatureWithNum 112
113 csUpdateSignature : BasicCS SignatureWithNum SignatureWithNum
129 csUpdateSignature = cs updateSignature 114 csUpdateSignature = cs updateSignature
130 115
131 --comp-sample-2 : CodeSegment LoopCounter SignatureWithNum ? 116
132 --comp-sample-2 = csUpdateSignature ◎ csInc 117
133 -} 118 comp-sample-2 : {c : Context} -> CodeSegment LoopCounter SignatureWithNum (SignatureWithNum ∷ LoopCounter ∷ SignatureWithNum ∷ LoopCounter ∷ [])
119 comp-sample-2 {c} = csComp {c} csUpdateSignature csInc
120
121 apply-sample-2 : Context
122 apply-sample-2 = exec (comp-sample-2 {firstContext}) firstContext