Mercurial > hg > Members > atton > agda-proofs

annotate cbc/maybe-subtype-sample.agda @ 77:a2e6f61d5f2b default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add modus-ponens
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 06:32:03 +0000
parents bd428bd6b394
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
59
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
1 module maybe-subtype-sample (A : Set) where
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
2
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
3 open import Level
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
4 open import Data.Maybe
59
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
5 open import Function using (id)
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
6 open import Relation.Binary.PropositionalEquality
58
b7493ee642de Trying define maybe-subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
59
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
8 open import maybe-subtype A
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
9 open import subtype A as N
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
10 open import subtype (Meta A) as M
59
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
11
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
12 instance
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
13 MetaIsMetaDataSegment : {{_ : M.DataSegment A}} -> M.DataSegment (Meta A)
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
14 MetaIsMetaDataSegment = record {get = (\mc -> mc) ; set = (\_ mc -> mc)}
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
15 ContextIsMetaDataSegment : M.DataSegment (Context)
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
16 ContextIsMetaDataSegment = record {get = Meta.context ; set = (\mc c -> record mc {context = c})}
59
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
17
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
18
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
19
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
20
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
21
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
22 return : {X : Set} {_ : Context} {_ : Meta A} {{_ : N.DataSegment X}} {{_ : M.DataSegment X}} -> X -> Meta X
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
23 return {c} {mc} {{nd}} {{md}} a = record {context = record {} ; maybeElem = just a}
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
24
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
25
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
26 fmap' : {B : Set} -> (A -> B) -> Meta A -> Meta B
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
27 fmap' f record { maybeElem = (just x) } = record {maybeElem = just (f x)}
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
28 fmap' f record { maybeElem = nothing } = record {maybeElem = nothing}
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
29
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
30
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
31 fmap : {c : Context} {B : Set}
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
32 {{_ : M.DataSegment A}} {{_ : M.DataSegment B}} {{_ : M.DataSegment (Meta A)}}{{_ : M.DataSegment (Meta B)}}
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
33 -> M.CodeSegment A B -> M.CodeSegment (Meta A) (Meta B)
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
34 fmap {c} {B} {{na}} {{nb}} {{ma}} (N.cs f) = M.cs {{ma}} (fmap' {B} f)
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
35
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
36
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
37 liftMeta : {B : Set} {{_ : M.DataSegment A}} {{_ : M.DataSegment B}} -> N.CodeSegment A B -> M.CodeSegment A B
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
38 liftMeta (N.cs f) = M.cs f
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
39
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
40
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
41 fmap-preserve-id : {x : Meta A} {{nx : N.DataSegment A }}{{mx : M.DataSegment A}} {{mmx : M.DataSegment (Meta A)}}
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
42 -> M.exec {{mmx}} {{mmx}} (fmap {{mx}} {{mx}} {{mmx}} {{mmx}} (M.cs id)) x ≡ M.exec (liftMeta (N.cs id)) x
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
43 fmap-preserve-id = {!!}
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
44
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
45