Mercurial > hg > Members > atton > agda-proofs

comparison cbc/variable-tuple.agda @ 24:0fcb7b35ba81

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add data version CodeSegment
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2016 01:57:13 +0000
parents 84e3fbc662db
children da78bb99d654
comparison
equal deleted inserted replaced
23:723532aa0592 24:0fcb7b35ba81
5 open import Data.List 5 open import Data.List
6 open import Data.Unit 6 open import Data.Unit
7 open import Data.Product 7 open import Data.Product
8 open import Function using (_∘_) 8 open import Function using (_∘_)
9 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality
10 open import Level hiding (zero)
10 11
11 data Format : Set₁ where 12 data Format : Set₁ where
12 FEnd : Format 13 FEnd : Format
13 FSet : Set -> Format -> Format 14 FSet : Set -> Format -> Format
14 15
38 double = < String || ℕ > 39 double = < String || ℕ >
39 40
40 triple : Format 41 triple : Format
41 triple = < String || ℕ || (List ℕ) > 42 triple = < String || ℕ || (List ℕ) >
42 43
44 data CodeSegment (A B : Set₁) : Set₁ where
45 -- cs : A -> B -> (A -> B) -> CodeSegment A B
46 cs : A -> B -> CodeSegment A B
43 47
44 record CodeSegment : Set₁ where 48 id : {l : Level} {A : Set l} -> A -> A
45 field 49 id a = a
46 IDS : Format
47 ODS : Format
48 50
49 cs : Format -> Format -> CodeSegment 51 CommonCodeSegment : Set₁
50 cs i o = record { IDS = i ; ODS = o } 52 CommonCodeSegment = CodeSegment Format Format
51 53
52 54 csDouble : CommonCodeSegment
53 csDouble : CodeSegment
54 csDouble = cs double double 55 csDouble = cs double double
55 56
56 57
57 ods : CodeSegment -> Set 58 ods : CommonCodeSegment -> Set
58 ods record { ODS = i } = ods' i 59 ods (cs i FEnd) = ⊤
59 where 60 ods (cs i (FSet s o)) = s × (ods (cs i o))
60 ods' : Format -> Set 61
61 ods' FEnd = ⊤
62 ods' (FSet s o) = s × (ods' o)
63 62
64 ods-double : ods csDouble 63 ods-double : ods csDouble
65 ods-double = "hoge" , zero , tt 64 ods-double = "hoge" , zero , tt
66 65
67 66
68 67 ids : {A : Set} -> CommonCodeSegment -> Set
69 ids : {A : Set} -> CodeSegment -> Set 68 ids {A} (cs FEnd o) = A
70 ids {A} record {IDS = IDS} = ids' IDS 69 ids {A} (cs (FSet s i) o) = s -> (ids {A} (cs i o))
71 where
72 ids' : Format -> Set
73 ids' FEnd = A
74 ids' (FSet x f) = x -> (ids' f)
75 70
76 71
77 ids-double : {A : Set} {a : A} -> ids {A} csDouble 72 ids-double : {A : Set} {a : A} -> ids {A} csDouble
78 ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a 73 ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a
79 74
80 75
81 executeCS : (cs : CodeSegment) -> Set 76
77 executeCS : (cs : CommonCodeSegment) -> Set
82 executeCS c = ids {ods c} c 78 executeCS c = ids {ods c} c
83 79
84 80
85 _◎_ : {c1ods c2ids : Format} -> {equiv : c1ods ≡ c2ids} -> CodeSegment -> CodeSegment -> CodeSegment 81 infixr 30 _◎_
86 record {IDS = i} ◎ (record {ODS = o}) = cs i o 82 _◎_ : {A B C : Set₁} -> CodeSegment A B -> CodeSegment B C -> CodeSegment A C
83 (cs i _) ◎ (cs _ o) = cs i o
87 84
88 85
89 compose-cs : CodeSegment 86 ◎-double : CommonCodeSegment
90 compose-cs = _◎_ {double} {double} {refl} csDouble csDouble 87 ◎-double = csDouble ◎ (cs (< String || ℕ >) <>) ◎ (cs <> triple)
91 88 -- ◎-double = csDouble ◎ (cs (< String || ℕ >) <>) ◎ (cs double triple) -- ...
92
93