|
57
|
1 module maybe-subtype (A : Set) where
|
|
|
2
|
|
|
3 open import Level
|
|
|
4 open import Function using (id)
|
|
|
5 open import Relation.Binary.PropositionalEquality
|
|
|
6
|
|
|
7 data Maybe (A : Set) : Set where
|
|
|
8 nothing : Maybe A
|
|
|
9 just : A -> Maybe A
|
|
|
10
|
|
|
11
|
|
|
12 record Context (A : Set) : Set where
|
|
|
13 field
|
|
|
14 maybeElem : Maybe A
|
|
|
15
|
|
|
16 open import subtype (Context A) as N
|
|
|
17
|
|
|
18
|
|
|
19 record Meta (A : Set) : Set where
|
|
|
20 field
|
|
|
21 context : Context A
|
|
|
22
|
|
|
23
|
|
|
24 open import subtype (Meta A) as M
|
|
|
25
|
|
|
26 instance
|
|
|
27 MetaIsMetaDataSegment : M.DataSegment (Meta A)
|
|
|
28 MetaIsMetaDataSegment = record {get = (\mc -> mc) ; set = (\_ mc -> mc)}
|
|
|
29 ContextIsMetaDataSegment : M.DataSegment (Context A)
|
|
|
30 ContextIsMetaDataSegment = record {get = Meta.context ; set = (\mc c -> record mc {context = c})}
|
|
|
31
|
|
|
32 return : {_ : Context A} {_ : Meta (Context A)} {{_ : N.DataSegment A}} {{_ : M.DataSegment A}} -> A -> Meta A
|
|
|
33 return {c} {mc} {{nd}} {{md}} a = record {context = record {maybeElem = just a}}
|
|
|
34
|
|
|
35 fmap' : {B : Set} {{_ : M.DataSegment (Context A)}} {{_ : M.DataSegment (Context B)}} -> (A -> B) -> Context A -> Context B
|
|
|
36 fmap' f record { maybeElem = (just x) } = record {maybeElem = just (f x)}
|
|
|
37 fmap' f record { maybeElem = nothing } = record {maybeElem = nothing}
|
|
|
38
|
|
|
39
|
|
|
40
|
|
|
41 fmap : {c : Context A} {B : Set}
|
|
|
42 {{_ : N.DataSegment A}} {{_ : N.DataSegment B}} {{_ : M.DataSegment (Context A)}} {{_ : M.DataSegment (Context B)}}
|
|
|
43 -> N.CodeSegment A B -> M.CodeSegment (Context A) (Context B)
|
|
|
44 fmap {c} {B} {{na}} {{nb}} {{ma}} {{mb}} (N.cs f) = M.cs {{ma}} (fmap' {B} {{ma}} {{mb}} f)
|
|
|
45
|
|
|
46
|
|
|
47
|
|
|
48 open ≡-Reasoning
|
|
|
49
|
|
|
50 exec-id : (x : Meta A) -> M.exec (M.cs {zero} {zero} {Context A} id) x ≡ x
|
|
|
51 exec-id record { context = context } = refl
|
|
|
52
|
|
|
53
|
|
|
54 maybe-preserve-id : {{na : N.DataSegment A}} {{ma : M.DataSegment A}} {{mx : M.DataSegment (Context A)}}
|
|
|
55 -> (x : Context A)
|
|
|
56 -> M.exec {{mx}} {{mx}} (fmap {x} {{na}}{{na}}{{mx}}{{mx}} (N.cs id)) (record {context = x})
|
|
|
57 ≡
|
|
|
58 M.exec {{mx}} {{mx}} (M.cs {{mx}} {{mx}} id) (record {context = x})
|
|
|
59
|
|
|
60 maybe-preserve-id {{na}} {{ma}} {{mx}} record { maybeElem = nothing } = begin
|
|
|
61 M.exec {{mx}} {{mx}} (fmap {record { maybeElem = nothing }} {{na}}{{na}}{{mx}}{{mx}} (N.cs id)) (record {context = record { maybeElem = nothing }})
|
|
|
62 ≡⟨ refl ⟩
|
|
|
63 M.DataSegment.set mx (record { context = record { maybeElem = nothing } }) ((fmap' {{mx}} {{mx}} id) (M.DataSegment.get mx (record { context = record { maybeElem = nothing } })))
|
|
|
64 ≡⟨ {!!} ⟩
|
|
|
65 record {context = record { maybeElem = nothing }}
|
|
|
66 ≡⟨ sym (exec-id (record {context = record {maybeElem = nothing}})) ⟩
|
|
|
67 M.exec {{mx}} {{mx}} (M.cs {{mx}} {{mx}} id) (record {context = record { maybeElem = nothing }})
|
|
|
68 ∎
|
|
|
69 maybe-preserve-id record { maybeElem = (just x) } = {!!}
|
|
|
70 {-
|
|
|
71 maybe-preserve-id {{na}} {{ma}} {{mx}} record { maybeElem = nothing } = begin
|
|
|
72 M.exec (fmap {record {maybeElem = nothing}} (N.cs id)) record {context = record { maybeElem = nothing}}
|
|
|
73 ≡⟨ refl ⟩
|
|
|
74 M.exec (M.cs (fmap' id)) record {context = record {maybeElem = nothing}}
|
|
|
75 ≡⟨ refl ⟩
|
|
|
76 M.DataSegment.set mx (record { context = record { maybeElem = nothing } }) ((fmap' id) (M.DataSegment.get mx (record { context = record { maybeElem = nothing } })))
|
|
|
77 ≡⟨ {!!} ⟩
|
|
|
78 record { context = record { maybeElem = nothing }}
|
|
|
79 ≡⟨ {!!} ⟩
|
|
|
80 M.exec {zero} {zero} {A} {A} (M.cs id) (record { context = record { maybeElem = nothing } })
|
|
|
81 ∎
|
|
|
82 maybe-preserve-id record { maybeElem = (just x) } = {!!}
|
|
|
83
|
|
|
84
|
|
|
85 -}
|
