Mercurial > hg > Members > atton > agda-proofs

annotate 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
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
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
8 open import Function using (_∘_ ; id)
17
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Binary.PropositionalEquality
24
0fcb7b35ba81 Add data version CodeSegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
10 open import Level hiding (zero)
17
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 data Format : Set₁ where
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 FEnd : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 FSet : Set -> Format -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 <> : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 <> = FEnd
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 infix 51 _>
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 _> : (Format -> Format) -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 _> f = f FEnd
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 infixl 52 _||_
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 _||_ : (Format -> Format) -> Set -> (Format -> Format)
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 _||_ f1 s = f1 ∘ (FSet s)
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
27 infix 53 <_
17
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 <_ : Set -> Format -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 <_ s = FSet s
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
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 unit : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 unit = <>
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 single : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 single = < ℕ >
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 double : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 double = < String || ℕ >
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 triple : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 triple = < String || ℕ || (List ℕ) >
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
43
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
44 data CodeSegment (I O : Set) : Set₁ where
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
45 cs : (I -> O) -> CodeSegment I O
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
46
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
47
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
48 twiceWithName : (String × ℕ ) -> (String × ℕ )
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
49 twiceWithName (s , n) = s , twice n
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
50 where
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
51 twice : ℕ -> ℕ
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
52 twice zero = zero
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
53 twice (ℕ.suc n₁) = (ℕ.suc (ℕ.suc (twice n₁)))
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
54
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
55 csDouble : CodeSegment (String × ℕ) (String × ℕ)
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
56 csDouble = cs twiceWithName
19
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
57
22
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
58
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
59 ods : {I O : Set} -> CodeSegment I O -> Set
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
60 ods {i} {o} c = o
19
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
61
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
62 ods-double : ods csDouble
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
63 ods-double = "hoge" , zero
19
853318ff55f9 Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
64
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
65
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
66 ids : {I O : Set} -> CodeSegment I O -> Set
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
67 ids {i} {o} c = i
22
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
68
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
69 ids-double : ids csDouble
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
70 ids-double = "fuga" , 3
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
71
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
72 --ids-double : {A : Set} {a : A} -> ids csDouble
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
73 --ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
74
20
4dd4400b48aa Define code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
75
24
0fcb7b35ba81 Add data version CodeSegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
76
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
77 executeCS : {A B : Set} -> CodeSegment A B -> (A -> B)
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
78 executeCS (cs b) = b
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
79
20
4dd4400b48aa Define code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
80
22
84e3fbc662db Define cs compose operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
81
24
0fcb7b35ba81 Add data version CodeSegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
82 infixr 30 _◎_
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
83 _◎_ : {A B C : Set} -> CodeSegment A B -> CodeSegment B C -> CodeSegment A C
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
84 (cs b1) ◎ (cs b2) = cs (b2 ∘ b1)
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
85
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
86
22
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
25
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
89 ◎-double : CodeSegment (String × ℕ) (String × ℕ )
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
90 --◎-double = csDouble ◎ csDouble ◎ csDouble -- ok
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
91 ◎-double = csDouble ◎ (cs (\s -> tt)) ◎ (cs (\t -> ("yo" , 100))) -- ok
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
92 --◎-double = csDouble ◎ (cs (\s -> tt)) ◎ csDouble -- ng (valid type check)
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
93
da78bb99d654 Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 24
diff changeset
94