Mercurial > hg > Members > atton > agda-proofs

annotate cbc/variable-tuple.agda @ 18:782a11f3eea4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define input data segment
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 18 Dec 2016 06:41:39 +0000
parents 7bfae9affc84
children 853318ff55f9
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
17
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Function using (_∘_)
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Relation.Binary.PropositionalEquality
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 data Format : Set₁ where
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 FEnd : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 FSet : Set -> Format -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 <> : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 <> = FEnd
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 infix 51 _>
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 _> : (Format -> Format) -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 _> f = f FEnd
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 infixl 52 _||_
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 _||_ : (Format -> Format) -> Set -> (Format -> Format)
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 _||_ f1 s = f1 ∘ (FSet s)
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
25 infix 53 <_
17
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 <_ : Set -> Format -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 <_ s = FSet s
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
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 unit : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 unit = <>
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 single : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 single = < ℕ >
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 double : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 double = < String || ℕ >
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 triple : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 triple = < String || ℕ || (List ℕ) >
18
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
41
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 DataSegment : {A : Set} -> Format -> Set
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
44 DataSegment {A} FEnd = A
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
45 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
46
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 data CodeSegment : Set₁ where
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
49 cs : Format -> Format -> CodeSegment
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
50
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
51 ods : CodeSegment -> List Set
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
52 ods (cs ids FEnd) = []
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
53 ods (cs ids (FSet s f)) = s ∷ (ods (cs ids f))
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
54
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
55 ids : {A : Set} -> CodeSegment -> Set
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
56 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
57
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
58
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
59 ids-double : {A : Set} {a : A} -> ids {A} (cs double double)
782a11f3eea4 Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
60 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
61