Mercurial > hg > Members > atton > agda-proofs

comparison cbc/named-product.agda @ 43:0a780145c5ff

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define compose operator using list of subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 04 Jan 2017 02:21:11 +0000
parents f7916d13e2b1
children 72cf35fb82af
comparison
equal deleted inserted replaced
42:f7916d13e2b1 43:0a780145c5ff
62 equiv = refl 62 equiv = refl
63 63
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 l 67 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ l)
68
69
68 70
69 71
70 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context 72 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
71 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c)) 73 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c))
72 74
73 75
74 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec (cs {l = l} inc) firstContext 76 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec (cs {l = l} inc) firstContext
75 equiv-exec = refl 77 equiv-exec = refl
76 78
77 79
78 _◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll : List Set} 80 _◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll : List Set}
79 -> CodeSegment B C l -> CodeSegment A B ll -> CodeSegment A C (l ++ ll) 81 -> CodeSegment B C (B ∷ C ∷ l) -> CodeSegment A B (A ∷ B ∷ ll) -> CodeSegment A C (A ∷ C ∷ B ∷ (l ++ ll))
80 _◎_ {{da}} {{_}} {{dc}} {l = l} {ll = ll} (cs g) (cs f) = cs {l = l ++ ll} {{da}} {{dc}} (g ∘ f) 82 _◎_ {A} {B} {C} {{da}} {{_}} {{dc}} {l} {ll} (cs g) (cs f) = cs {l = (B ∷ (l ++ ll))} {{da}} {{dc}} (g ∘ f)
81 83
82 84