Mercurial > hg > Members > atton > agda-proofs
changeset 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 |
files | cbc/named-product.agda |
diffstat | 1 files changed, 9 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/cbc/named-product.agda Wed Jan 04 02:21:11 2017 +0000 +++ b/cbc/named-product.agda Wed Jan 04 02:26:58 2017 +0000 @@ -66,7 +66,11 @@ data CodeSegment (A B : Set) : (List Set) -> Set where cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ l) +basicCS : Set -> Set -> Set +basicCS A B = CodeSegment A B (A ∷ B ∷ []) +csInc : basicCS LoopCounter LoopCounter +csInc = cs inc exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context @@ -82,3 +86,8 @@ _◎_ {A} {B} {C} {{da}} {{_}} {{dc}} {l} {ll} (cs g) (cs f) = cs {l = (B ∷ (l ++ ll))} {{da}} {{dc}} (g ∘ f) +comp-sample : CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ []) +comp-sample = csInc ◎ csInc + +apply-sample : Context +apply-sample = exec comp-sample firstContext