Mercurial > hg > Members > atton > agda-proofs
annotate cbc/variable-tuple.agda @ 19:853318ff55f9
Trying define output data segment
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 18 Dec 2016 07:59:51 +0000 |
parents | 782a11f3eea4 |
children | 4dd4400b48aa |
rev | line source |
---|---|
17 | 1 module variable-tuple where |
2 | |
3 open import Data.Nat hiding (_<_ ; _>_) | |
4 open import Data.String | |
5 open import Data.List | |
18
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
6 open import Data.Unit |
19
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
7 open import Data.Product |
17 | 8 open import Function using (_∘_) |
9 open import Relation.Binary.PropositionalEquality | |
10 | |
11 data Format : Set₁ where | |
12 FEnd : Format | |
13 FSet : Set -> Format -> Format | |
14 | |
15 <> : Format | |
16 <> = FEnd | |
17 | |
18 infix 51 _> | |
19 _> : (Format -> Format) -> Format | |
20 _> f = f FEnd | |
21 | |
22 infixl 52 _||_ | |
23 _||_ : (Format -> Format) -> Set -> (Format -> Format) | |
24 _||_ f1 s = f1 ∘ (FSet s) | |
25 | |
18
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
26 infix 53 <_ |
17 | 27 <_ : Set -> Format -> Format |
28 <_ s = FSet s | |
29 | |
30 | |
31 unit : Format | |
32 unit = <> | |
33 | |
34 single : Format | |
35 single = < ℕ > | |
36 | |
37 double : Format | |
38 double = < String || ℕ > | |
39 | |
40 triple : Format | |
41 triple = < String || ℕ || (List ℕ) > | |
18
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
42 |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
43 |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
44 DataSegment : {A : Set} -> Format -> Set |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
45 DataSegment {A} FEnd = A |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
46 DataSegment {A} (FSet x f) = x -> (DataSegment {A} f) |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
47 |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
48 |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
49 data CodeSegment : Set₁ where |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
50 cs : Format -> Format -> CodeSegment |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
51 |
19
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
52 csDouble : CodeSegment |
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
53 csDouble = cs double double |
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
54 |
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
55 ods : CodeSegment -> Set |
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
56 ods (cs ids FEnd) = ⊤ |
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
57 ods (cs ids (FSet s f)) = s × (ods (cs ids f)) |
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
58 |
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
59 ods-double : ods csDouble |
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
60 ods-double = "hoge" , zero , tt |
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
61 |
18
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
62 |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
63 ids : {A : Set} -> CodeSegment -> Set |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
64 ids {A} (cs i o) = DataSegment {A} i |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
65 |
19
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
66 ids-double : {A : Set} {a : A} -> ids {A} csDouble |
18
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
67 ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a |
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
68 |