module maybe-subtype (A : Set) where open import Level open import Function using (id) open import Relation.Binary.PropositionalEquality data Maybe (A : Set) : Set where nothing : Maybe A just : A -> Maybe A record Context (A : Set) : Set where field maybeElem : Maybe A open import subtype (Context A) as N record Meta (A : Set) : Set where field context : Context A open import subtype (Meta A) as M instance MetaIsMetaDataSegment : M.DataSegment (Meta A) MetaIsMetaDataSegment = record {get = (\mc -> mc) ; set = (\_ mc -> mc)} ContextIsMetaDataSegment : M.DataSegment (Context A) ContextIsMetaDataSegment = record {get = Meta.context ; set = (\mc c -> record mc {context = c})} return : {_ : Context A} {_ : Meta (Context A)} {{_ : N.DataSegment A}} {{_ : M.DataSegment A}} -> A -> Meta A return {c} {mc} {{nd}} {{md}} a = record {context = record {maybeElem = just a}} fmap' : {B : Set} {{_ : M.DataSegment (Context A)}} {{_ : M.DataSegment (Context B)}} -> (A -> B) -> Context A -> Context B fmap' f record { maybeElem = (just x) } = record {maybeElem = just (f x)} fmap' f record { maybeElem = nothing } = record {maybeElem = nothing} fmap : {c : Context A} {B : Set} {{_ : N.DataSegment A}} {{_ : N.DataSegment B}} {{_ : M.DataSegment (Context A)}} {{_ : M.DataSegment (Context B)}} -> N.CodeSegment A B -> M.CodeSegment (Context A) (Context B) fmap {c} {B} {{na}} {{nb}} {{ma}} {{mb}} (N.cs f) = M.cs {{ma}} (fmap' {B} {{ma}} {{mb}} f) open ≡-Reasoning exec-id : (x : Meta A) -> M.exec (M.cs {zero} {zero} {Context A} id) x ≡ x exec-id record { context = context } = refl maybe-preserve-id : {{na : N.DataSegment A}} {{ma : M.DataSegment A}} {{mx : M.DataSegment (Context A)}} -> (x : Context A) -> M.exec {{mx}} {{mx}} (fmap {x} {{na}}{{na}}{{mx}}{{mx}} (N.cs id)) (record {context = x}) ≡ M.exec {{mx}} {{mx}} (M.cs {{mx}} {{mx}} id) (record {context = x}) maybe-preserve-id {{na}} {{ma}} {{mx}} record { maybeElem = nothing } = begin M.exec {{mx}} {{mx}} (fmap {record { maybeElem = nothing }} {{na}}{{na}}{{mx}}{{mx}} (N.cs id)) (record {context = record { maybeElem = nothing }}) ≡⟨ refl ⟩ M.DataSegment.set mx (record { context = record { maybeElem = nothing } }) ((fmap' {{mx}} {{mx}} id) (M.DataSegment.get mx (record { context = record { maybeElem = nothing } }))) ≡⟨ {!!} ⟩ record {context = record { maybeElem = nothing }} ≡⟨ sym (exec-id (record {context = record {maybeElem = nothing}})) ⟩ M.exec {{mx}} {{mx}} (M.cs {{mx}} {{mx}} id) (record {context = record { maybeElem = nothing }}) ∎ maybe-preserve-id record { maybeElem = (just x) } = {!!} {- maybe-preserve-id {{na}} {{ma}} {{mx}} record { maybeElem = nothing } = begin M.exec (fmap {record {maybeElem = nothing}} (N.cs id)) record {context = record { maybeElem = nothing}} ≡⟨ refl ⟩ M.exec (M.cs (fmap' id)) record {context = record {maybeElem = nothing}} ≡⟨ refl ⟩ M.DataSegment.set mx (record { context = record { maybeElem = nothing } }) ((fmap' id) (M.DataSegment.get mx (record { context = record { maybeElem = nothing } }))) ≡⟨ {!!} ⟩ record { context = record { maybeElem = nothing }} ≡⟨ {!!} ⟩ M.exec {zero} {zero} {A} {A} (M.cs id) (record { context = record { maybeElem = nothing } }) ∎ maybe-preserve-id record { maybeElem = (just x) } = {!!} -}