Mercurial > hg > Members > atton > agda-proofs

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
17
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module variable-tuple where
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.Nat hiding (_<_ ; _>_)
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.String
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Function using (_∘_)
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Binary.PropositionalEquality
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 data Format : Set₁ where
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 FEnd : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 FSet : Set -> Format -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 <> : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 <> = FEnd
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 infix 51 _>
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 _> : (Format -> Format) -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 _> f = f FEnd
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 infixl 52 _||_
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 _||_ : (Format -> Format) -> Set -> (Format -> Format)
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 _||_ f1 s = f1 ∘ (FSet s)
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
26 infix 53 <_
17
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 <_ : Set -> Format -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 <_ s = FSet s
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 unit : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 unit = <>
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 single : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 single = < ℕ >
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 double : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 double = < String || ℕ >
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 triple : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
22
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
44 record CodeSegment : Set₁ where
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
45 field
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
46 IDS : Format
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
47 ODS : Format
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
48
22
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
49 cs : Format -> Format -> CodeSegment
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
50 cs i o = record { IDS = i ; ODS = o }
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
51
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
52
19
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
53 csDouble : CodeSegment
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
54 csDouble = cs double double
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
55
22
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
56
19
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
57 ods : CodeSegment -> Set
22
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
58 ods record { ODS = i } = ods' i
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
59 where
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
60 ods' : Format -> Set
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
61 ods' FEnd = ⊤
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
62 ods' (FSet s o) = s × (ods' o)
19
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
63
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
64 ods-double : ods csDouble
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
65 ods-double = "hoge" , zero , tt
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
66
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
67
22
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
68
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
69 ids : {A : Set} -> CodeSegment -> Set
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
70 ids {A} record {IDS = IDS} = ids' IDS
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
71 where
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
72 ids' : Format -> Set
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
73 ids' FEnd = A
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
74 ids' (FSet x f) = x -> (ids' f)
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
75
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
76
19
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
77 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
78 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
79
20
4dd4400b48aa Define code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
80
4dd4400b48aa Define code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
81 executeCS : (cs : CodeSegment) -> Set
4dd4400b48aa Define code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
82 executeCS c = ids {ods c} c
4dd4400b48aa Define code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
83
22
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
84
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
85 _◎_ : {c1ods c2ids : Format} -> {equiv : c1ods ≡ c2ids} -> CodeSegment -> CodeSegment -> CodeSegment
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
86 record {IDS = i} ◎ (record {ODS = o}) = cs i o
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
87
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
88
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
89 compose-cs : CodeSegment
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
90 compose-cs = _◎_ {double} {double} {refl} csDouble csDouble
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
91
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
92
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
93