Mercurial > hg > Members > atton > agda-proofs
comparison cbc/named-product.agda @ 44:72cf35fb82af
Add composition sample
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 04 Jan 2017 02:26:58 +0000 |
parents | 0a780145c5ff |
children | 08b695ca359c |
comparison
equal
deleted
inserted
replaced
43:0a780145c5ff | 44:72cf35fb82af |
---|---|
64 | 64 |
65 | 65 |
66 data CodeSegment (A B : Set) : (List Set) -> Set where | 66 data CodeSegment (A B : Set) : (List Set) -> Set where |
67 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ l) | 67 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ l) |
68 | 68 |
69 basicCS : Set -> Set -> Set | |
70 basicCS A B = CodeSegment A B (A ∷ B ∷ []) | |
69 | 71 |
72 csInc : basicCS LoopCounter LoopCounter | |
73 csInc = cs inc | |
70 | 74 |
71 | 75 |
72 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context | 76 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context |
73 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c)) | 77 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c)) |
74 | 78 |
80 _◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll : List Set} | 84 _◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll : List Set} |
81 -> CodeSegment B C (B ∷ C ∷ l) -> CodeSegment A B (A ∷ B ∷ ll) -> CodeSegment A C (A ∷ C ∷ B ∷ (l ++ ll)) | 85 -> CodeSegment B C (B ∷ C ∷ l) -> CodeSegment A B (A ∷ B ∷ ll) -> CodeSegment A C (A ∷ C ∷ B ∷ (l ++ ll)) |
82 _◎_ {A} {B} {C} {{da}} {{_}} {{dc}} {l} {ll} (cs g) (cs f) = cs {l = (B ∷ (l ++ ll))} {{da}} {{dc}} (g ∘ f) | 86 _◎_ {A} {B} {C} {{da}} {{_}} {{dc}} {l} {ll} (cs g) (cs f) = cs {l = (B ∷ (l ++ ll))} {{da}} {{dc}} (g ∘ f) |
83 | 87 |
84 | 88 |
89 comp-sample : CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ []) | |
90 comp-sample = csInc ◎ csInc | |
91 | |
92 apply-sample : Context | |
93 apply-sample = exec comp-sample firstContext |