Mercurial > hg > Members > atton > agda-proofs

comparison cbc/variable-tuple.agda @ 22:84e3fbc662db

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define cs compose operator
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 22 Dec 2016 05:47:20 +0000
parents 4dd4400b48aa
children 0fcb7b35ba81
comparison
equal deleted inserted replaced
21:afb2304be45b 22:84e3fbc662db
39 39
40 triple : Format 40 triple : Format
41 triple = < String || ℕ || (List ℕ) > 41 triple = < String || ℕ || (List ℕ) >
42 42
43 43
44 DataSegment : {A : Set} -> Format -> Set 44 record CodeSegment : Set₁ where
45 DataSegment {A} FEnd = A 45 field
46 DataSegment {A} (FSet x f) = x -> (DataSegment {A} f) 46 IDS : Format
47 ODS : Format
47 48
49 cs : Format -> Format -> CodeSegment
50 cs i o = record { IDS = i ; ODS = o }
48 51
49 data CodeSegment : Set₁ where
50 cs : Format -> Format -> CodeSegment
51 52
52 csDouble : CodeSegment 53 csDouble : CodeSegment
53 csDouble = cs double double 54 csDouble = cs double double
54 55
56
55 ods : CodeSegment -> Set 57 ods : CodeSegment -> Set
56 ods (cs ids FEnd) = ⊤ 58 ods record { ODS = i } = ods' i
57 ods (cs ids (FSet s f)) = s × (ods (cs ids f)) 59 where
60 ods' : Format -> Set
61 ods' FEnd = ⊤
62 ods' (FSet s o) = s × (ods' o)
58 63
59 ods-double : ods csDouble 64 ods-double : ods csDouble
60 ods-double = "hoge" , zero , tt 65 ods-double = "hoge" , zero , tt
61 66
62 67
63 ids : {A : Set} -> CodeSegment -> Set 68
64 ids {A} (cs i o) = DataSegment {A} i 69 ids : {A : Set} -> CodeSegment -> Set
70 ids {A} record {IDS = IDS} = ids' IDS
71 where
72 ids' : Format -> Set
73 ids' FEnd = A
74 ids' (FSet x f) = x -> (ids' f)
75
65 76
66 ids-double : {A : Set} {a : A} -> ids {A} csDouble 77 ids-double : {A : Set} {a : A} -> ids {A} csDouble
67 ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a 78 ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a
68 79
69 80
70 executeCS : (cs : CodeSegment) -> Set 81 executeCS : (cs : CodeSegment) -> Set
71 executeCS c = ids {ods c} c 82 executeCS c = ids {ods c} c
72 83
84
85 _◎_ : {c1ods c2ids : Format} -> {equiv : c1ods ≡ c2ids} -> CodeSegment -> CodeSegment -> CodeSegment
86 record {IDS = i} ◎ (record {ODS = o}) = cs i o
87
88
89 compose-cs : CodeSegment
90 compose-cs = _◎_ {double} {double} {refl} csDouble csDouble
91
92
93