Mercurial > hg > Members > atton > agda-proofs

comparison cbc/named-product.agda @ 41:2abf1cd97f10

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define type composition using list of subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 03 Jan 2017 08:21:25 +0000
parents e6b965df2137
children f7916d13e2b1
comparison
equal deleted inserted replaced
40:e6b965df2137 41:2abf1cd97f10
2 2
3 open import Function 3 open import Function
4 open import Data.Bool 4 open import Data.Bool
5 open import Data.Nat 5 open import Data.Nat
6 open import Data.String 6 open import Data.String
7 open import Data.Vec 7 open import Data.List
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 9
10 10
11 data DataSegment {n : ℕ } : (Vec Set n) -> Set where
12 ds : (l : Vec Set n) -> DataSegment l
13 11
14 12
15 record Context : Set where 13 record Context : Set where
16 field 14 field
17 cycle : ℕ 15 cycle : ℕ
63 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" } 61 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
64 equiv = refl 62 equiv = refl
65 63
66 64
67 65
68 data CodeSegment {n : ℕ} {l : Vec Set n} (A B : Set) : (DataSegment (A ∷ (B ∷ l))) -> Set where 66 data CodeSegment (A B : Set) : (List Set) -> Set where
69 cs : {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (ds (A ∷ (B ∷ l))) 67 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ (B ∷ l))
70 68
71 69
72 exec : {n : ℕ } {I O : Set} -> {l : Vec Set (suc (suc n))} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O (ds (I ∷ O ∷ l)) -> Context -> Context 70 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
73 exec {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c)) 71 exec {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c))
74 72
75 73
76 equiv-exec : {n : ℕ } {l : Vec Set n} -> incContextCycle firstContext ≡ exec (cs inc) firstContext 74 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec (cs {l = l} inc) firstContext
77 equiv-exec = refl 75 equiv-exec = refl
76
78 {- 77 {-
79 78
80 79
81 InputIsHead : {n : ℕ} {I O : Set} {l : Vec Set (suc (suc n))} -> (cs : CodeSegment I O l) -> I ≡ head l 80 InputIsHead : {n : ℕ} {I O : Set} {l : Vec Set (suc (suc n))} -> (cs : CodeSegment I O l) -> I ≡ head l
82 InputIsHead (cs _) = refl 81 InputIsHead (cs _) = refl