Mercurial > hg > Members > atton > agda-proofs
comparison cbc/variable-tuple.agda @ 25:da78bb99d654
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 |