Mercurial > hg > Members > atton > agda-proofs

comparison cbc/named-product.agda @ 40:e6b965df2137

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define type composition using subtype through DS
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 03 Jan 2017 07:52:43 +0000
parents d8312361afdc
children 2abf1cd97f10
comparison
equal deleted inserted replaced
39:d8312361afdc 40:e6b965df2137
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.List 7 open import Data.Vec
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 9
10 {-
11 record DataSegment (n : ℕ) : Set₁ where
12 field
13 name : String
14 ds : Vec (Set -> Set) (suc n)
15 10
16 ids : {A : Set} {n : ℕ} -> DataSegment n -> Set 11 data DataSegment {n : ℕ } : (Vec Set n) -> Set where
17 ids {a} {zero} record { name = name ; ds = (x ∷ []) } = x a 12 ds : (l : Vec Set n) -> DataSegment l
18 ids {a} {suc n} record { name = name ; ds = (x ∷ ds) } = x a -> ids {a} {n} record { name = name ; ds = ds } 13
19 -}
20 14
21 record Context : Set where 15 record Context : Set where
22 field 16 field
23 cycle : ℕ 17 cycle : ℕ
24 led : String 18 led : String
26 20
27 record Datum (A : Set) : Set where 21 record Datum (A : Set) : Set where
28 field 22 field
29 get : Context -> A 23 get : Context -> A
30 set : Context -> A -> Context 24 set : Context -> A -> Context
31
32
33 25
34 26
35 record LoopCounter : Set where 27 record LoopCounter : Set where
36 field 28 field
37 count : ℕ 29 count : ℕ
69 61
70 62
71 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" } 63 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
72 equiv = refl 64 equiv = refl
73 65
74 data CodeSegment (A B : Set) : (List Set) -> Set₁ where
75 cs : {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ [])
76 66
77 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context 67
68 data CodeSegment {n : ℕ} {l : Vec Set n} (A B : Set) : (DataSegment (A ∷ (B ∷ l))) -> Set where
69 cs : {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (ds (A ∷ (B ∷ l)))
70
71
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
78 exec {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c)) 73 exec {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c))
79 74
80 equiv-exec : incContextCycle firstContext ≡ exec (cs inc) firstContext 75
76 equiv-exec : {n : ℕ } {l : Vec Set n} -> incContextCycle firstContext ≡ exec (cs inc) firstContext
81 equiv-exec = refl 77 equiv-exec = refl
78 {-
82 79
83 80
84 --InputIsHead : {I : Set} (l : List Set) -> (cs : CodeSegment I _ l) -> I ≡ head l 81 InputIsHead : {n : ℕ} {I O : Set} {l : Vec Set (suc (suc n))} -> (cs : CodeSegment I O l) -> I ≡ head l
85 --InputIsHead = ? 82 InputIsHead (cs _) = refl
86 83
84 OutputIsLast : {n : ℕ} {I O : Set} {l : Vec Set (suc (suc n))} -> (cs : CodeSegment I O l) -> O ≡ last l
85 OutputIsLast {_} {_} {_} {l} (cs x) = {!!}
87 86
87 -}
88 88
89 89
90 90
91 --yoyo : DataSegment 91 --yoyo : DataSegment
92 --yoyo = record { name = "yoyo" ; ds = [ Yo ]} 92 --yoyo = record { name = "yoyo" ; ds = [ Yo ]}