Mercurial > hg > Members > atton > agda-proofs

comparison cbc/variable-tuple.agda @ 19:853318ff55f9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define output data segment
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 18 Dec 2016 07:59:51 +0000
parents 782a11f3eea4
children 4dd4400b48aa
comparison
equal deleted inserted replaced
18:782a11f3eea4 19:853318ff55f9
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 Data.Unit
7 open import Data.Product
7 open import Function using (_∘_) 8 open import Function using (_∘_)
8 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality
9 10
10 data Format : Set₁ where 11 data Format : Set₁ where
11 FEnd : Format 12 FEnd : Format
46 47
47 48
48 data CodeSegment : Set₁ where 49 data CodeSegment : Set₁ where
49 cs : Format -> Format -> CodeSegment 50 cs : Format -> Format -> CodeSegment
50 51
51 ods : CodeSegment -> List Set 52 csDouble : CodeSegment
52 ods (cs ids FEnd) = [] 53 csDouble = cs double double
53 ods (cs ids (FSet s f)) = s ∷ (ods (cs ids f)) 54
55 ods : CodeSegment -> Set
56 ods (cs ids FEnd) = ⊤
57 ods (cs ids (FSet s f)) = s × (ods (cs ids f))
58
59 ods-double : ods csDouble
60 ods-double = "hoge" , zero , tt
61
54 62
55 ids : {A : Set} -> CodeSegment -> Set 63 ids : {A : Set} -> CodeSegment -> Set
56 ids {A} (cs i o) = DataSegment {A} i 64 ids {A} (cs i o) = DataSegment {A} i
57 65
58 66 ids-double : {A : Set} {a : A} -> ids {A} csDouble
59 ids-double : {A : Set} {a : A} -> ids {A} (cs double double)
60 ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a 67 ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a
61 68