annotate cbc/variable-tuple.agda @ 17:7bfae9affc84

Add variable-tuple
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 18 Dec 2016 01:35:31 +0000
parents
children 782a11f3eea4
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
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Function using (_∘_)
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Relation.Binary.PropositionalEquality
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 data Format : Set₁ where
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 FEnd : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 FSet : Set -> Format -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 <> : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 <> = FEnd
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 {-
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 begin_ : ∀{x y : A} → x ≡ y → x ≡ y
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 begin_ x≡y = x≡y
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 _ ≡⟨⟩ x≡y = x≡y
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 _≡⟨_⟩_ : ∀ (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 _≅⟨_⟩_ : ∀ (x {y z} : A) → x ≅ y → y ≡ z → x ≡ z
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 _ ≅⟨ x≅y ⟩ y≡z = trans (H.≅-to-≡ x≅y) y≡z
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 _∎ : ∀ (x : A) → x ≡ x
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 _∎ _ = refl
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
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 infix 51 _>
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 _> : (Format -> Format) -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 _> f = f FEnd
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 infixl 52 _||_
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 _||_ : (Format -> Format) -> Set -> (Format -> Format)
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 _||_ f1 s = f1 ∘ (FSet s)
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 infix 54 <_
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 <_ : Set -> Format -> Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 <_ s = FSet s
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 unit : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 unit = <>
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
48
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 single : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 single = < ℕ >
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 double : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 double = < String || ℕ >
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 triple : Format
7bfae9affc84 Add variable-tuple
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 triple = < String || ℕ || (List ℕ) >