Mercurial > hg > Members > atton > agda-proofs

comparison cbc/named-product.agda @ 46:af1fe3bd9f1e

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:02:23 +0000
parents 08b695ca359c
children 49de29c12c7b
comparison
equal deleted inserted replaced
45:08b695ca359c 46:af1fe3bd9f1e
1 module named-product where 1 module named-product where
2 2
3 open import Function 3
4 open import Data.Bool 4 open import Data.Bool
5 open import Data.Nat 5 open import Data.Nat
6 open import Data.Nat.Show 6 open import Data.Nat.Show
7 open import Data.String hiding (_++_ ; show) 7 open import Data.String hiding (_++_ ; show)
8 open import Data.List 8 open import Data.List
19 19
20 record Datum (A : Set) : Set where 20 record Datum (A : Set) : Set where
21 field 21 field
22 get : Context -> A 22 get : Context -> A
23 set : Context -> A -> Context 23 set : Context -> A -> Context
24 24 open Datum
25 25
26 record LoopCounter : Set where 26 record LoopCounter : Set where
27 field 27 field
28 count : ℕ 28 count : ℕ
29 name : String 29 name : String
53 inc l = record l {count = suc (LoopCounter.count l)} 53 inc l = record l {count = suc (LoopCounter.count l)}
54 54
55 firstContext : Context 55 firstContext : Context
56 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" } 56 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
57 57
58
58 incContextCycle : {{_ : Datum LoopCounter }} -> Context -> Context 59 incContextCycle : {{_ : Datum LoopCounter }} -> Context -> Context
59 incContextCycle {{l}} c = Datum.set l c (inc (Datum.get l c)) 60 incContextCycle {{l}} c = Datum.set l c (inc (Datum.get l c))
60 61
61 62
62 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" } 63 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
63 equiv = refl 64 equiv = refl
64 65
65 66
66 67
67 data CodeSegment (A B : Set) : (List Set) -> Set where 68 data CodeSegment (A B : Set) : (List Set) -> Set where
68 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ l) 69 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (B ∷ A ∷ l)
69 70
70 basicCS : Set -> Set -> Set 71 BasicCS : Set -> Set -> Set
71 basicCS A B = CodeSegment A B (A ∷ B ∷ []) 72 BasicCS A B = CodeSegment A B (A ∷ B ∷ [])
72 73
73 csInc : basicCS LoopCounter LoopCounter 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
74 csInc = cs inc 79 csInc = cs inc
75 80
76 81
77 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context 82 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
78 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c)) 83 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (get i c))
84
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
89 --downCast : {A B : Set} {{i : Datum A}} {{o : Datum B}} -> (Datum A -> Datum B) -> A -> B
90 --downCast {{i = record { get = get ; set = set }}} {{record { get = get₁ ; set = set₁ }}} f a = {!!}
79 91
80 92
81 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec (cs {l = l} inc) firstContext 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
99 _∘_ {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
100
101
102
103
104
105
106 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext
82 equiv-exec = refl 107 equiv-exec = refl
83 108
84 109
85 _◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll : List Set} 110 _◎_ : {con : Context} {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}} {l ll : List Set}
86 -> CodeSegment B C (B ∷ C ∷ l) -> CodeSegment A B (A ∷ B ∷ ll) -> CodeSegment A C (A ∷ C ∷ B ∷ (l ++ ll)) 111 -> CodeSegment C D (D ∷ C ∷ l) -> CodeSegment A B (B ∷ A ∷ ll) -> CodeSegment A D (D ∷ A ∷ C ∷ B ∷ (l ++ ll))
87 _◎_ {A} {B} {C} {{da}} {{_}} {{dc}} {l} {ll} (cs g) (cs f) = cs {l = (B ∷ (l ++ ll))} {{da}} {{dc}} (g ∘ f) 112 _◎_ {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)
88 114
89 115
90 comp-sample : CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ []) 116 comp-sample : CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ [])
91 comp-sample = csInc ◎ csInc 117 comp-sample = csInc ◎ csInc
118
92 119
93 apply-sample : Context 120 apply-sample : Context
94 apply-sample = exec comp-sample firstContext 121 apply-sample = exec comp-sample firstContext
95 122
123 {-
96 124
97 updateSignature : SignatureWithNum -> SignatureWithNum 125 updateSignature : SignatureWithNum -> SignatureWithNum
98 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num} 126 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num}
99 127
100 csUpdateSignature : basicCS SignatureWithNum SignatureWithNum 128 csUpdateSignature : basicCS SignatureWithNum SignatureWithNum
101 csUpdateSignature = cs updateSignature 129 csUpdateSignature = cs updateSignature
102 130
103 comp-sample-2 : CodeSegment LoopCounter SignatureWithNum ? 131 --comp-sample-2 : CodeSegment LoopCounter SignatureWithNum ?
104 comp-sample-2 = csUpdateSignature ◎ csInc 132 --comp-sample-2 = csUpdateSignature ◎ csInc
133 -}