Mercurial > hg > Members > atton > agda-proofs

comparison cbc/variable-tuple.agda @ 25:da78bb99d654

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Embed function body to codesegment
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2016 02:36:46 +0000
parents 0fcb7b35ba81
children d503a73186ce
comparison
equal deleted inserted replaced
24:0fcb7b35ba81 25:da78bb99d654
3 open import Data.Nat hiding (_<_ ; _>_) 3 open import Data.Nat hiding (_<_ ; _>_)
4 open import Data.String 4 open import Data.String
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 (_∘_ ; id)
9 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality
10 open import Level hiding (zero) 10 open import Level hiding (zero)
11 11
12 data Format : Set₁ where 12 data Format : Set₁ where
13 FEnd : Format 13 FEnd : Format
39 double = < String || ℕ > 39 double = < String || ℕ >
40 40
41 triple : Format 41 triple : Format
42 triple = < String || ℕ || (List ℕ) > 42 triple = < String || ℕ || (List ℕ) >
43 43
44 data CodeSegment (A B : Set₁) : Set₁ where 44 data CodeSegment (I O : Set) : Set₁ where
45 -- cs : A -> B -> (A -> B) -> CodeSegment A B 45 cs : (I -> O) -> CodeSegment I O
46 cs : A -> B -> CodeSegment A B
47
48 id : {l : Level} {A : Set l} -> A -> A
49 id a = a
50
51 CommonCodeSegment : Set₁
52 CommonCodeSegment = CodeSegment Format Format
53
54 csDouble : CommonCodeSegment
55 csDouble = cs double double
56 46
57 47
58 ods : CommonCodeSegment -> Set 48 twiceWithName : (String × ℕ ) -> (String × ℕ )
59 ods (cs i FEnd) = ⊤ 49 twiceWithName (s , n) = s , twice n
60 ods (cs i (FSet s o)) = s × (ods (cs i o)) 50 where
51 twice : ℕ -> ℕ
52 twice zero = zero
53 twice (ℕ.suc n₁) = (ℕ.suc (ℕ.suc (twice n₁)))
54
55 csDouble : CodeSegment (String × ℕ) (String × ℕ)
56 csDouble = cs twiceWithName
61 57
62 58
59 ods : {I O : Set} -> CodeSegment I O -> Set
60 ods {i} {o} c = o
61
63 ods-double : ods csDouble 62 ods-double : ods csDouble
64 ods-double = "hoge" , zero , tt 63 ods-double = "hoge" , zero
65 64
66 65
67 ids : {A : Set} -> CommonCodeSegment -> Set 66 ids : {I O : Set} -> CodeSegment I O -> Set
68 ids {A} (cs FEnd o) = A 67 ids {i} {o} c = i
69 ids {A} (cs (FSet s i) o) = s -> (ids {A} (cs i o))
70 68
69 ids-double : ids csDouble
70 ids-double = "fuga" , 3
71 71
72 ids-double : {A : Set} {a : A} -> ids {A} csDouble 72 --ids-double : {A : Set} {a : A} -> ids csDouble
73 ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a 73 --ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a
74 74
75 75
76 76
77 executeCS : (cs : CommonCodeSegment) -> Set 77 executeCS : {A B : Set} -> CodeSegment A B -> (A -> B)
78 executeCS c = ids {ods c} c 78 executeCS (cs b) = b
79
79 80
80 81
81 infixr 30 _◎_ 82 infixr 30 _◎_
82 _◎_ : {A B C : Set₁} -> CodeSegment A B -> CodeSegment B C -> CodeSegment A C 83 _◎_ : {A B C : Set} -> CodeSegment A B -> CodeSegment B C -> CodeSegment A C
83 (cs i _) ◎ (cs _ o) = cs i o 84 (cs b1) ◎ (cs b2) = cs (b2 ∘ b1)
84 85
85 86
86 ◎-double : CommonCodeSegment 87
87 ◎-double = csDouble ◎ (cs (< String || ℕ >) <>) ◎ (cs <> triple) 88
88 -- ◎-double = csDouble ◎ (cs (< String || ℕ >) <>) ◎ (cs double triple) -- ... 89 ◎-double : CodeSegment (String × ℕ) (String × ℕ )
90 --◎-double = csDouble ◎ csDouble ◎ csDouble -- ok
91 ◎-double = csDouble ◎ (cs (\s -> tt)) ◎ (cs (\t -> ("yo" , 100))) -- ok
92 --◎-double = csDouble ◎ (cs (\s -> tt)) ◎ csDouble -- ng (valid type check)
93
94