Mercurial > hg > Members > atton > agda-proofs

comparison 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
comparison
equal deleted inserted replaced
17:7bfae9affc84 18:782a11f3eea4
1 module variable-tuple where 1 module variable-tuple where
2 2
3 open import Data.Nat hiding (_<_ ; _>_) 3 open import Data.Nat hiding (_<_ ; _>_)
4 open import Data.String 4 open import Data.String
5 open import Data.List 5 open import Data.List
6 open import Data.Unit
6 open import Function using (_∘_) 7 open import Function using (_∘_)
7 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
8 9
9 data Format : Set₁ where 10 data Format : Set₁ where
10 FEnd : Format 11 FEnd : Format
11 FSet : Set -> Format -> Format 12 FSet : Set -> Format -> Format
12 13
13 <> : Format 14 <> : Format
14 <> = FEnd 15 <> = FEnd
15 16
16 {-
17 begin_ : ∀{x y : A} → x ≡ y → x ≡ y
18 begin_ x≡y = x≡y
19
20 _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
21 _ ≡⟨⟩ x≡y = x≡y
22
23 _≡⟨_⟩_ : ∀ (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
24 _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
25
26 _≅⟨_⟩_ : ∀ (x {y z} : A) → x ≅ y → y ≡ z → x ≡ z
27 _ ≅⟨ x≅y ⟩ y≡z = trans (H.≅-to-≡ x≅y) y≡z
28
29 _∎ : ∀ (x : A) → x ≡ x
30 _∎ _ = refl
31 -}
32
33 infix 51 _> 17 infix 51 _>
34 _> : (Format -> Format) -> Format 18 _> : (Format -> Format) -> Format
35 _> f = f FEnd 19 _> f = f FEnd
36 20
37 infixl 52 _||_ 21 infixl 52 _||_
38 _||_ : (Format -> Format) -> Set -> (Format -> Format) 22 _||_ : (Format -> Format) -> Set -> (Format -> Format)
39 _||_ f1 s = f1 ∘ (FSet s) 23 _||_ f1 s = f1 ∘ (FSet s)
40 24
41 infix 54 <_ 25 infix 53 <_
42 <_ : Set -> Format -> Format 26 <_ : Set -> Format -> Format
43 <_ s = FSet s 27 <_ s = FSet s
44 28
45 29
46 unit : Format 30 unit : Format
52 double : Format 36 double : Format
53 double = < String || ℕ > 37 double = < String || ℕ >
54 38
55 triple : Format 39 triple : Format
56 triple = < String || ℕ || (List ℕ) > 40 triple = < String || ℕ || (List ℕ) >
41
42
43 DataSegment : {A : Set} -> Format -> Set
44 DataSegment {A} FEnd = A
45 DataSegment {A} (FSet x f) = x -> (DataSegment {A} f)
46
47
48 data CodeSegment : Set₁ where
49 cs : Format -> Format -> CodeSegment
50
51 ods : CodeSegment -> List Set
52 ods (cs ids FEnd) = []
53 ods (cs ids (FSet s f)) = s ∷ (ods (cs ids f))
54
55 ids : {A : Set} -> CodeSegment -> Set
56 ids {A} (cs i o) = DataSegment {A} i
57
58
59 ids-double : {A : Set} {a : A} -> ids {A} (cs double double)
60 ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a
61