Mercurial > hg > Members > atton > agda-proofs

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module named-product where
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
3
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
4 open import Data.Bool
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Nat
45
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
6 open import Data.Nat.Show
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
7 open import Data.String hiding (_++_ ; show)
41
2abf1cd97f10 Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
8 open import Data.List
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
9 open import Relation.Binary.PropositionalEquality
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
10
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
40
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
12
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
13
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
14 record Context : Set where
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
15 field
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
16 cycle : ℕ
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
17 led : String
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
18 signature : String
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
19
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
20 record Datum (A : Set) : Set where
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
21 field
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
22 get : Context -> A
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
23 set : Context -> A -> Context
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
24 open Datum
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
25
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
26 record LoopCounter : Set where
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 field
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
28 count : ℕ
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
29 name : String
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
31 record SignatureWithNum : Set where
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 field
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 signature : String
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
34 num : ℕ
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
35
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 instance
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
37 contextHasLoopCounter : Datum LoopCounter
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
38 contextHasLoopCounter = record {get = (\c -> record {count = Context.cycle c ;
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
39 name = Context.led c });
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
40 set = (\c l -> record {cycle = LoopCounter.count l;
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
41 led = LoopCounter.name l;
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
42 signature = Context.signature c})}
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
43 contextHasSignatureWithNum : Datum SignatureWithNum
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
44 contextHasSignatureWithNum = record {get = (\c -> record { signature = Context.signature c
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
45 ; num = Context.cycle c})
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
46 ;set = (\c s -> record { cycle = SignatureWithNum.num s
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
47 ; led = Context.led c
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
48 ; signature = SignatureWithNum.signature s})
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
49 }
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
51
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
52 inc : LoopCounter -> LoopCounter
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
53 inc l = record l {count = suc (LoopCounter.count l)}
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 firstContext : Context
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
58
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
59 incContextCycle : {{_ : Datum LoopCounter }} -> Context -> Context
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
60 incContextCycle {{l}} c = Datum.set l c (inc (Datum.get l c))
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
61
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
63 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
64 equiv = refl
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
40
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
66
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
67
41
2abf1cd97f10 Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
68 data CodeSegment (A B : Set) : (List Set) -> Set where
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
69 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (B ∷ A ∷ l)
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
70
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
71 BasicCS : Set -> Set -> Set
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
72 BasicCS A B = CodeSegment A B (A ∷ B ∷ [])
43
0a780145c5ff Define compose operator using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
73
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
74 up : {A B : Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> Context -> B
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
75 up {{i}} {{o}} f c = f (Datum.get i c)
43
0a780145c5ff Define compose operator using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
76
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
77
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
78 csInc : BasicCS LoopCounter LoopCounter
44
72cf35fb82af Add composition sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
79 csInc = cs inc
40
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
80
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
81
42
f7916d13e2b1 Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
82 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
83 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (get i c))
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
84
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
85 --upCast : {A B : Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> (Datum A -> Datum B)
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
86 --upCast {{i}} {{o}} f a = record { get = (\c -> f (Datum.get a c))
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
87 -- ; set = (\c b -> Datum.set o c b)}
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
88
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
89 --downCast : {A B : Set} {{i : Datum A}} {{o : Datum B}} -> (Datum A -> Datum B) -> A -> B
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
90 --downCast {{i = record { get = get ; set = set }}} {{record { get = get₁ ; set = set₁ }}} f a = {!!}
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
91
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
92
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
93 apply : {A B : Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> Context -> B
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
94 apply {{i}} {{o}} f c = f (get i c)
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
95
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
96
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
97 _∘_ : {con : Context} -> {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}}
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
98 -> (C -> D) -> (A -> B) -> A -> D
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
99 _∘_ {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
100
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
101
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
102
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
103
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
104
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
105
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
106 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext
42
f7916d13e2b1 Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
107 equiv-exec = refl
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
108
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
109
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
110 _◎_ : {con : Context} {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}} {l ll : List Set}
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
111 -> CodeSegment C D (D ∷ C ∷ l) -> CodeSegment A B (B ∷ A ∷ ll) -> CodeSegment A D (D ∷ A ∷ C ∷ B ∷ (l ++ ll))
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
112 _◎_ {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} {l} {ll} (cs g) (cs f)
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
113 = cs {l = (C ∷ B ∷ (l ++ ll))} {{da}} {{dd}} (_∘_ {con} {{da}} {{db}} {{dc}} {{dd}} g f)
42
f7916d13e2b1 Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
114
f7916d13e2b1 Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
115
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
116 comp-sample : CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ [])
44
72cf35fb82af Add composition sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
117 comp-sample = csInc ◎ csInc
72cf35fb82af Add composition sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
118
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
119
44
72cf35fb82af Add composition sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
120 apply-sample : Context
72cf35fb82af Add composition sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
121 apply-sample = exec comp-sample firstContext
45
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
122
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
123 {-
45
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
124
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
125 updateSignature : SignatureWithNum -> SignatureWithNum
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
126 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num}
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
127
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
128 csUpdateSignature : basicCS SignatureWithNum SignatureWithNum
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
129 csUpdateSignature = cs updateSignature
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
130
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
131 --comp-sample-2 : CodeSegment LoopCounter SignatureWithNum ?
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
132 --comp-sample-2 = csUpdateSignature ◎ csInc
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
133 -}