From dab051e89bbe904587a047d239e79610554d5c91 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 10 Mar 2014 08:17:41 +0100 Subject: implement a bff on a shaped source type Add IsShaped and Shaped records describing shapely types as in Jay95. Implement bff on Shaped and rewrite PartialVecVec to use the vector shape retaining all proofs on the vector implementation. --- Instances.agda | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 Instances.agda (limited to 'Instances.agda') diff --git a/Instances.agda b/Instances.agda new file mode 100644 index 0000000..faff6f8 --- /dev/null +++ b/Instances.agda @@ -0,0 +1,18 @@ +module Instances where + +open import Data.Nat using (ℕ) +open import Data.Vec using (Vec) +open import Function using (id) +open import Relation.Binary.PropositionalEquality using (refl) + +open import Structures using (Shaped) + +VecShaped : Shaped ℕ Vec +VecShaped = record + { arity = id + ; content = id + ; fill = λ _ → id + ; isShaped = record + { content-fill = λ _ → refl + ; fill-content = λ _ _ → refl + } } -- cgit v1.2.3 From 3532b34beabbaa6967fe660385c4b4036493a8f1 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 10 Mar 2014 09:31:57 +0100 Subject: port theorem-{1,2} to PartialShapeVec --- Bidir.agda | 147 +++++++++++++++++++++++++++++++++++++++------------------ Instances.agda | 30 ++++++++++-- 2 files changed, 127 insertions(+), 50 deletions(-) (limited to 'Instances.agda') diff --git a/Bidir.agda b/Bidir.agda index ae99c5a..1a661de 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -13,7 +13,7 @@ open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open import Data.List using (List) open import Data.List.All using (All) -open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map) renaming (lookup to lookupVec) +open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; allFin) renaming (lookup to lookupVec) open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Data.Vec.Properties using (lookup∘tabulate ; map-cong ; map-∘ ; map-lookup-allFin) open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) @@ -24,14 +24,16 @@ open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid) import Relation.Binary.EqReasoning as EqR +open import Structures using (Functor ; IsFunctor ; Shaped ; module Shaped) +open import Instances using (MaybeFunctor) import GetTypes -open GetTypes.PartialVecVec using (Get ; module Get) +open GetTypes.PartialShapeVec using (Get ; module Get) open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective) open import FinMap import CheckInsert open CheckInsert A import BFF -open BFF.PartialVecBFF A using (assoc ; enumerate ; enumeratel ; denumerate ; bff) +open BFF.PartialShapeBFF A using (assoc ; enumerate ; denumerate ; bff) open Setoid using () renaming (_≈_ to _∋_≈_) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) @@ -107,11 +109,24 @@ lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin just x ∷ map just xs ∎ where open EqR (VecISetoid (MaybeSetoid A.setoid) at _) -theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (map just s) +lemma-fmap-denumerate-enumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Shaped.fmap ShapeT (denumerate ShapeT c) (enumerate ShapeT s) ≡ c +lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin + fmap (denumerate ShapeT c) (fill s (allFin (arity s))) + ≡⟨ fill-fmap (denumerate ShapeT c) s (allFin (arity s)) ⟩ + fill s (map (flip lookupVec (content c)) (allFin (arity s))) + ≡⟨ cong (fill s) (map-lookup-allFin (content c)) ⟩ + fill s (content c) + ≡⟨ content-fill c ⟩ + c ∎ + where open ≡-Reasoning + open Shaped ShapeT + + +theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Get.Container G Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (Get.fmap G just s) theorem-1 G {i} s = begin bff G i s (get s) - ≡⟨ cong (bff G i s ∘ get) (sym (map-lookup-allFin s)) ⟩ - bff G i s (get (map f t)) + ≡⟨ cong (bff G i s ∘ get) (sym (lemma-fmap-denumerate-enumerate ShapeT s)) ⟩ + bff G i s (get (fmap f t)) ≡⟨ cong (bff G i s) (free-theorem f t) ⟩ bff G i s (map f (get t)) ≡⟨ refl ⟩ @@ -119,26 +134,26 @@ theorem-1 G {i} s = begin ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (get t)) ⟩ (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (toList (get t))) ≡⟨ cong just (begin - h′↦r (union (restrict f (toList (get t))) (reshape g′ (|gl₁| i))) + h′↦r (union (restrict f (toList (get t))) (reshape g′ (arity (|gl₁| i)))) ≡⟨ cong (h′↦r ∘ union (restrict f (toList (get t)))) (lemma-reshape-id g′) ⟩ h′↦r (union (restrict f (toList (get t))) g′) ≡⟨ cong h′↦r (lemma-disjoint-union f (get t)) ⟩ h′↦r (fromFunc f) ≡⟨ refl ⟩ - map (flip lookupM (fromFunc f)) t - ≡⟨ map-cong (lemma-lookupM-fromFunc f) t ⟩ - map (Maybe.just ∘ f) t - ≡⟨ map-∘ just f t ⟩ - map just (map f t) - ≡⟨ cong (map just) (map-lookup-allFin s) ⟩ - map just s ∎) ⟩ _ ∎ + fmap (flip lookupM (fromFunc f)) t + ≡⟨ IsFunctor.cong (isFunctor (|gl₁| i)) (lemma-lookupM-fromFunc f) t ⟩ + fmap (Maybe.just ∘ f) t + ≡⟨ IsFunctor.composition (isFunctor (|gl₁| i)) just f t ⟩ + fmap just (fmap f t) + ≡⟨ cong (fmap just) (lemma-fmap-denumerate-enumerate ShapeT s) ⟩ + fmap just s ∎) ⟩ _ ∎ where open ≡-Reasoning open Get G - t = enumeratel (|gl₁| i) - f = denumerate s + t = enumerate ShapeT (|gl₁| i) + f = denumerate ShapeT s g′ = delete-many (get t) (fromFunc f) - h↦h′ = flip union (reshape g′ (|gl₁| i)) - h′↦r = flip map t ∘ flip lookupM + h↦h′ = flip union (reshape g′ (arity (|gl₁| i))) + h′↦r = (λ f′ → fmap f′ t) ∘ flip lookupM lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a @@ -162,9 +177,21 @@ lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma lemma->>=-just (just a) p = a , refl lemma->>=-just nothing () -lemma-just-sequence : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v -lemma-just-sequence [] = refl -lemma-just-sequence (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequence xs) +lemma-just-sequenceV : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v +lemma-just-sequenceV [] = refl +lemma-just-sequenceV (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequenceV xs) + +lemma-just-sequence : (G : Get) → {A : Set} {i : Get.|I| G} → (c : Get.Container G A (Get.|gl₁| G i)) → Get.sequence G (Get.fmap G just c) ≡ just c +lemma-just-sequence G {i = i} c = begin + fill (|gl₁| i) <$> sequenceV (content (fmap just c)) + ≡⟨ cong (_<$>_ (fill (|gl₁| i)) ∘ sequenceV) (fmap-content just c) ⟩ + fill (|gl₁| i) <$> sequenceV (map just (content c)) + ≡⟨ cong (_<$>_ (fill (|gl₁| i))) (lemma-just-sequenceV (content c)) ⟩ + fill (|gl₁| i) <$> just (content c) + ≡⟨ cong just (content-fill c) ⟩ + just c ∎ + where open ≡-Reasoning + open Get G lemma-sequenceV-successful : {A : Set} {n : ℕ} → (v : Vec (Maybe A) n) → {r : Vec A n} → sequenceV v ≡ just r → v ≡ map just r lemma-sequenceV-successful [] {r = []} p = refl @@ -173,18 +200,44 @@ lemma-sequenceV-successful (just x ∷ xs) () | nothing | _ lemma-sequenceV-successful (just x ∷ xs) {r = .x ∷ .ys} refl | just ys | [ p′ ] = cong (_∷_ (just x)) (lemma-sequenceV-successful xs p′) lemma-sequenceV-successful (nothing ∷ xs) () -lemma-get-sequenceV : {A : Set} → (G : Get) → {i : Get.|I| G} {v : Vec (Maybe A) (Get.|gl₁| G i)} {r : Vec A (Get.|gl₁| G i)} → sequenceV v ≡ just r → Get.get G <$> sequenceV v ≡ sequenceV (Get.get G v) -lemma-get-sequenceV G {v = v} {r = r} p = begin - get <$> sequenceV v - ≡⟨ cong (_<$>_ get ∘ sequenceV) (lemma-sequenceV-successful v p) ⟩ - get <$> sequenceV (map just r) - ≡⟨ cong (_<$>_ get) (lemma-just-sequence r) ⟩ +lemma-sequence-successful : (G : Get) → {A : Set} {i : Get.|I| G} → (c : Get.Container G (Maybe A) (Get.|gl₁| G i)) → {r : Get.Container G A (Get.|gl₁| G i)} → Get.sequence G c ≡ just r → c ≡ Get.fmap G just r +lemma-sequence-successful G {i = i} c {r} p = just-injective (sym (begin + fill (|gl₁| i) <$> (map just <$> (content <$> just r)) + ≡⟨ cong (_<$>_ (fill (|gl₁| i)) ∘ _<$>_ (map just)) (begin + content <$> just r + ≡⟨ cong (_<$>_ content) (sym p) ⟩ + content <$> (fill (|gl₁| i) <$> sequenceV (content c)) + ≡⟨ sym (Functor.composition MaybeFunctor content (fill (|gl₁| i)) (sequenceV (content c))) ⟩ + content ∘ fill (|gl₁| i) <$> sequenceV (content c) + ≡⟨ Functor.cong MaybeFunctor (fill-content (|gl₁| i)) (sequenceV (content c)) ⟩ + id <$> sequenceV (content c) + ≡⟨ Functor.identity MaybeFunctor (sequenceV (content c)) ⟩ + sequenceV (content c) + ≡⟨ cong sequenceV (lemma-sequenceV-successful (content c) (proj₂ wp)) ⟩ + sequenceV (map just (proj₁ wp)) + ≡⟨ lemma-just-sequenceV (proj₁ wp) ⟩ + just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)) ∎) ⟩ + fill (|gl₁| i) <$> (map just <$> just (proj₁ (lemma-<$>-just (sequenceV (content c)) p))) + ≡⟨ cong (_<$>_ (fill (|gl₁| i)) ∘ just) (sym (lemma-sequenceV-successful (content c) (proj₂ wp))) ⟩ + fill (|gl₁| i) <$> just (content c) + ≡⟨ cong just (content-fill c) ⟩ + just c ∎)) + where open ≡-Reasoning + open Get G + wp = lemma-<$>-just (sequenceV (content c)) p + +lemma-get-sequence : {A : Set} → (G : Get) → {i : Get.|I| G} {v : Get.Container G (Maybe A) (Get.|gl₁| G i)} {r : Get.Container G A (Get.|gl₁| G i)} → Get.sequence G v ≡ just r → Get.get G <$> Get.sequence G v ≡ sequenceV (Get.get G v) +lemma-get-sequence G {v = v} {r = r} p = begin + get <$> sequence v + ≡⟨ cong (_<$>_ get ∘ sequence) (lemma-sequence-successful G v p) ⟩ + get <$> sequence (fmap just r) + ≡⟨ cong (_<$>_ get) (lemma-just-sequence G r) ⟩ get <$> just r - ≡⟨ sym (lemma-just-sequence (get r)) ⟩ + ≡⟨ sym (lemma-just-sequenceV (get r)) ⟩ sequenceV (map just (get r)) ≡⟨ cong sequenceV (sym (free-theorem just r)) ⟩ - sequenceV (get (map just r)) - ≡⟨ cong (sequenceV ∘ get) (sym (lemma-sequenceV-successful v p)) ⟩ + sequenceV (get (fmap just r)) + ≡⟨ cong (sequenceV ∘ get) (sym (lemma-sequence-successful G v p)) ⟩ sequenceV (get v) ∎ where open ≡-Reasoning open Get G @@ -198,16 +251,16 @@ sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _)) sequence-cong {S} (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ map just v -theorem-2 G j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G j))) <$> (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v)) p) -theorem-2 G j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v) ph′) -theorem-2 G j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩ +theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Get.Container G (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ map just v +theorem-2 G {i} j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G i))) (fromFunc (denumerate (Get.ShapeT G) s))) (Get.arity G (Get.|gl₁| G j)))) <$> (assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G j))) v)) p) +theorem-2 G {i} j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G j))) v) ph′) +theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩ get u ≡⟨ just-injective (trans (cong (_<$>_ get) (sym p)) (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph)) ⟩ get (h′↦r (h↦h′ h)) ≡⟨ refl ⟩ - get (map (flip lookupM (h↦h′ h)) t) + get (fmap (flip lookupM (h↦h′ h)) t) ≡⟨ free-theorem (flip lookupM (h↦h′ h)) t ⟩ map (flip lookupM (h↦h′ h)) (get t) ≡⟨ lemma-union-not-used h g′ (get t) (lemma-assoc-domain (get t) v h ph) ⟩ @@ -216,23 +269,23 @@ theorem-2 G j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid map just v ∎ where open SetoidReasoning open Get G - s′ = enumerate s - g = fromFunc (denumerate s) + s′ = enumerate ShapeT (|gl₁| i) + g = fromFunc (denumerate ShapeT s) g′ = delete-many (get s′) g - t = enumeratel (Get.|gl₁| G j) - h↦h′ = flip union (reshape g′ (Get.|gl₁| G j)) - h′↦r = flip map t ∘ flip lookupM + t = enumerate ShapeT (|gl₁| j) + h↦h′ = flip union (reshape g′ (arity (|gl₁| j))) + h′↦r = (λ f → fmap f t) ∘ flip lookupM -theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (map just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v +theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Get.Container G Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (Get.fmap G just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v theorem-2′ G j s v u p = drop-just (begin get <$> just u - ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence u)) ⟩ - get <$> sequenceV (map just u) - ≡⟨ lemma-get-sequenceV G (lemma-just-sequence u) ⟩ - sequenceV (get (map just u)) - ≈⟨ sequence-cong (theorem-2 G j s v (map just u) p) ⟩ + ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence G u)) ⟩ + get <$> sequence (fmap just u) + ≡⟨ lemma-get-sequence G (lemma-just-sequence G u) ⟩ + sequenceV (get (fmap just u)) + ≈⟨ sequence-cong (theorem-2 G j s v (fmap just u) p) ⟩ sequenceV (map just v) - ≡⟨ lemma-just-sequence v ⟩ + ≡⟨ lemma-just-sequenceV v ⟩ just v ∎) where open EqR (MaybeSetoid (VecISetoid A.setoid at _)) open Get G diff --git a/Instances.agda b/Instances.agda index faff6f8..b41b0a2 100644 --- a/Instances.agda +++ b/Instances.agda @@ -1,11 +1,35 @@ module Instances where +open import Category.Functor using (RawFunctor) +open import Data.Maybe as M using (Maybe) open import Data.Nat using (ℕ) open import Data.Vec using (Vec) -open import Function using (id) -open import Relation.Binary.PropositionalEquality using (refl) +open import Function using (_∘_ ; id) +open import Relation.Binary.PropositionalEquality as P using (_≗_ ; refl) -open import Structures using (Shaped) +open import Structures using (Functor ; Shaped) + +MaybeFunctor : Functor Maybe +MaybeFunctor = record + { rawfunctor = M.functor + ; isFunctor = record + { cong = cong + ; identity = identity + ; composition = composition + } } + where _<$>_ = RawFunctor._<$>_ M.functor + + cong : {α β : Set} {g h : α → β} → g ≗ h → _<$>_ g ≗ _<$>_ h + cong g≗h (M.just x) = P.cong M.just (g≗h x) + cong g≗h M.nothing = refl + + identity : {α : Set} → _<$>_ {α} id ≗ id + identity (M.just x) = refl + identity M.nothing = refl + + composition : {α β γ : Set} → (g : β → γ) → (h : α → β) → _<$>_ (g ∘ h) ≗ _<$>_ g ∘ _<$>_ h + composition g h (M.just x) = refl + composition g h M.nothing = refl VecShaped : Shaped ℕ Vec VecShaped = record -- cgit v1.2.3 From cb7f533f4119f044201df2f28838c96ee367b771 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 10 Mar 2014 16:11:15 +0100 Subject: also allow Shaped types for the view Albeit long, this commit is relatively boring. --- BFF.agda | 28 +++++----- Bidir.agda | 171 ++++++++++++++++++++++++++++++++------------------------- GetTypes.agda | 40 ++++++++++++++ Instances.agda | 49 ++++++++++++++--- Precond.agda | 42 +++++++------- 5 files changed, 211 insertions(+), 119 deletions(-) (limited to 'Instances.agda') diff --git a/BFF.agda b/BFF.agda index b78e2af..12524ca 100644 --- a/BFF.agda +++ b/BFF.agda @@ -18,10 +18,10 @@ open import Generic using (sequenceV ; ≡-to-Π) open import Structures using (Shaped ; module Shaped) open import Instances using (VecShaped) import CheckInsert -open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeVec) +open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeVec ; PartialShapeVec-to-PartialShapeShape) module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where - open GetTypes.PartialShapeVec public using (Get ; module Get) + open GetTypes.PartialShapeShape public using (Get ; module Get) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) open CheckInsert A @@ -36,19 +36,19 @@ module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Fin (Shaped.arity ShapeT s) → α denumerate ShapeT c = flip lookupV (Shaped.content ShapeT c) - bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.Container G Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Get.Container G (Maybe Carrier) (Get.|gl₁| G j)) - bff G {i} j s v = let s′ = enumerate ShapeT (|gl₁| i) + bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.SourceContainer G Carrier (Get.|gl₁| G i) → Get.ViewContainer G Carrier (Get.|gl₂| G j) → Maybe (Get.SourceContainer G (Maybe Carrier) (Get.|gl₁| G j)) + bff G {i} j s v = let s′ = enumerate SourceShapeT (|gl₁| i) t′ = get s′ - g = fromFunc (denumerate ShapeT s) - g′ = delete-many t′ g - t = enumerate ShapeT (|gl₁| j) - h = assoc (get t) v - h′ = (flip union (reshape g′ (arity (|gl₁| j)))) <$> h - in ((λ f → fmap f t) ∘ flip lookupM) <$> h′ + g = fromFunc (denumerate SourceShapeT s) + g′ = delete-many (Shaped.content ViewShapeT t′) g + t = enumerate SourceShapeT (|gl₁| j) + h = assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT v) + h′ = (flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j)))) <$> h + in ((λ f → fmapS f t) ∘ flip lookupM) <$> h′ where open Get G - sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.Container G Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Get.Container G Carrier (Get.|gl₁| G j)) - sbff G j s v = bff G j s v >>= Get.sequence G + sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.SourceContainer G Carrier (Get.|gl₁| G i) → Get.ViewContainer G Carrier (Get.|gl₂| G j) → Maybe (Get.SourceContainer G Carrier (Get.|gl₁| G j)) + sbff G j s v = bff G j s v >>= Shaped.sequence (Get.SourceShapeT G) module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where open GetTypes.PartialVecVec public using (Get) @@ -67,10 +67,10 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate = PartialShapeBFF.denumerate A VecShaped bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G j)) - bff G j s v = PartialShapeBFF.bff A (PartialVecVec-to-PartialShapeVec G) j s v + bff G j s v = PartialShapeBFF.bff A (PartialShapeVec-to-PartialShapeShape (PartialVecVec-to-PartialShapeVec G)) j s v sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j)) - sbff G j s v = PartialShapeBFF.sbff A (PartialVecVec-to-PartialShapeVec G) j s v + sbff G j s v = PartialShapeBFF.sbff A (PartialShapeVec-to-PartialShapeShape (PartialVecVec-to-PartialShapeVec G)) j s v module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where open GetTypes.VecVec public using (Get) diff --git a/Bidir.agda b/Bidir.agda index 9637f17..1513a17 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -25,9 +25,9 @@ open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid) import Relation.Binary.EqReasoning as EqR open import Structures using (Functor ; IsFunctor ; Shaped ; module Shaped) -open import Instances using (MaybeFunctor) +open import Instances using (MaybeFunctor ; ShapedISetoid) import GetTypes -open GetTypes.PartialShapeVec using (Get ; module Get) +open GetTypes.PartialShapeShape using (Get ; module Get) open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective) open import FinMap import CheckInsert @@ -122,38 +122,40 @@ lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin open Shaped ShapeT -theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Get.Container G Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (Get.fmap G just s) +theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (Get.fmapS G just s) theorem-1 G {i} s = begin bff G i s (get s) - ≡⟨ cong (bff G i s ∘ get) (sym (lemma-fmap-denumerate-enumerate ShapeT s)) ⟩ - bff G i s (get (fmap f t)) + ≡⟨ cong (bff G i s ∘ get) (sym (lemma-fmap-denumerate-enumerate SourceShapeT s)) ⟩ + bff G i s (get (fmapS f t)) ≡⟨ cong (bff G i s) (free-theorem f t) ⟩ - bff G i s (map f (get t)) + bff G i s (fmapV f (get t)) ≡⟨ refl ⟩ - h′↦r <$> (h↦h′ <$> (assoc (get t) (map f (get t)))) - ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (get t)) ⟩ - (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (toList (get t))) + h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT (fmapV f (get t))))) + ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′ ∘ assoc (Shaped.content ViewShapeT (get t))) (Shaped.fmap-content ViewShapeT f (get t)) ⟩ + h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (map f (Shaped.content ViewShapeT (get t))))) + ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (Shaped.content ViewShapeT (get t))) ⟩ + (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (toList (Shaped.content ViewShapeT (get t)))) ≡⟨ cong just (begin - h′↦r (union (restrict f (toList (get t))) (reshape g′ (arity (|gl₁| i)))) - ≡⟨ cong (h′↦r ∘ union (restrict f (toList (get t)))) (lemma-reshape-id g′) ⟩ - h′↦r (union (restrict f (toList (get t))) g′) - ≡⟨ cong h′↦r (lemma-disjoint-union f (get t)) ⟩ + h′↦r (union (restrict f (toList (Shaped.content ViewShapeT (get t)))) (reshape g′ (Shaped.arity SourceShapeT (|gl₁| i)))) + ≡⟨ cong (h′↦r ∘ union (restrict f (toList (Shaped.content ViewShapeT (get t))))) (lemma-reshape-id g′) ⟩ + h′↦r (union (restrict f (toList (Shaped.content ViewShapeT (get t)))) g′) + ≡⟨ cong h′↦r (lemma-disjoint-union f (Shaped.content ViewShapeT (get t))) ⟩ h′↦r (fromFunc f) ≡⟨ refl ⟩ - fmap (flip lookupM (fromFunc f)) t - ≡⟨ IsFunctor.cong (isFunctor (|gl₁| i)) (lemma-lookupM-fromFunc f) t ⟩ - fmap (Maybe.just ∘ f) t - ≡⟨ IsFunctor.composition (isFunctor (|gl₁| i)) just f t ⟩ - fmap just (fmap f t) - ≡⟨ cong (fmap just) (lemma-fmap-denumerate-enumerate ShapeT s) ⟩ - fmap just s ∎) ⟩ _ ∎ + fmapS (flip lookupM (fromFunc f)) t + ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (|gl₁| i)) (lemma-lookupM-fromFunc f) t ⟩ + fmapS (Maybe.just ∘ f) t + ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (|gl₁| i)) just f t ⟩ + fmapS just (fmapS f t) + ≡⟨ cong (fmapS just) (lemma-fmap-denumerate-enumerate SourceShapeT s) ⟩ + fmapS just s ∎) ⟩ _ ∎ where open ≡-Reasoning open Get G - t = enumerate ShapeT (|gl₁| i) - f = denumerate ShapeT s - g′ = delete-many (get t) (fromFunc f) - h↦h′ = flip union (reshape g′ (arity (|gl₁| i))) - h′↦r = (λ f′ → fmap f′ t) ∘ flip lookupM + t = enumerate SourceShapeT (|gl₁| i) + f = denumerate SourceShapeT s + g′ = delete-many (Shaped.content ViewShapeT (get t)) (fromFunc f) + h↦h′ = flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| i))) + h′↦r = (λ f′ → fmapS f′ t) ∘ flip lookupM lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a @@ -226,66 +228,85 @@ lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (sym (begin open Shaped ShapeT wp = lemma-<$>-just (sequenceV (content c)) p -lemma-get-sequence : {A : Set} → (G : Get) → {i : Get.|I| G} {v : Get.Container G (Maybe A) (Get.|gl₁| G i)} {r : Get.Container G A (Get.|gl₁| G i)} → Get.sequence G v ≡ just r → Get.get G <$> Get.sequence G v ≡ sequenceV (Get.get G v) +lemma-get-sequence : {A : Set} → (G : Get) → {i : Get.|I| G} {v : Get.SourceContainer G (Maybe A) (Get.|gl₁| G i)} {r : Get.SourceContainer G A (Get.|gl₁| G i)} → Shaped.sequence (Get.SourceShapeT G) v ≡ just r → Get.get G <$> Shaped.sequence (Get.SourceShapeT G) v ≡ Shaped.sequence (Get.ViewShapeT G) (Get.get G v) lemma-get-sequence G {v = v} {r = r} p = begin - get <$> sequence v - ≡⟨ cong (_<$>_ get ∘ sequence) (lemma-sequence-successful ShapeT v p) ⟩ - get <$> sequence (fmap just r) - ≡⟨ cong (_<$>_ get) (lemma-just-sequence ShapeT r) ⟩ + get <$> Shaped.sequence SourceShapeT v + ≡⟨ cong (_<$>_ get ∘ Shaped.sequence SourceShapeT) (lemma-sequence-successful SourceShapeT v p) ⟩ + get <$> Shaped.sequence SourceShapeT (fmapS just r) + ≡⟨ cong (_<$>_ get) (lemma-just-sequence SourceShapeT r) ⟩ get <$> just r - ≡⟨ sym (lemma-just-sequenceV (get r)) ⟩ - sequenceV (map just (get r)) - ≡⟨ cong sequenceV (sym (free-theorem just r)) ⟩ - sequenceV (get (fmap just r)) - ≡⟨ cong (sequenceV ∘ get) (sym (lemma-sequence-successful ShapeT v p)) ⟩ - sequenceV (get v) ∎ + ≡⟨ sym (lemma-just-sequence ViewShapeT (get r)) ⟩ + Shaped.sequence ViewShapeT (fmapV just (get r)) + ≡⟨ cong (Shaped.sequence ViewShapeT) (sym (free-theorem just r)) ⟩ + Shaped.sequence ViewShapeT (get (fmapS just r)) + ≡⟨ cong (Shaped.sequence ViewShapeT ∘ get) (sym (lemma-sequence-successful SourceShapeT v p)) ⟩ + Shaped.sequence ViewShapeT (get v) ∎ where open ≡-Reasoning open Get G -sequence-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂ -sequence-cong {S} VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequence-cong xs≈ys -sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (VecEq._∷-cong_ x≈y p) -sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | just sys | () -sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | nothing | () -sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -sequence-cong {S} (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _)) +sequenceV-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂ +sequenceV-cong {S} VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _)) +sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequenceV-cong xs≈ys +sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (VecEq._∷-cong_ x≈y p) +sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | just sys | () +sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | nothing | () +sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _)) +sequenceV-cong {S} (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Get.Container G (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ map just v -theorem-2 G {i} j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G i))) (fromFunc (denumerate (Get.ShapeT G) s))) (Get.arity G (Get.|gl₁| G j)))) <$> (assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G j))) v)) p) -theorem-2 G {i} j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G j))) v) ph′) -theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩ - get u - ≡⟨ just-injective (trans (cong (_<$>_ get) (sym p)) - (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph)) ⟩ - get (h′↦r (h↦h′ h)) +sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (EqSetoid S) ShapeT (MaybeSetoid α) at _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (EqSetoid S) ShapeT α at _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y +sequence-cong ShapeT α {x = x} {y = y} (shape≈ , content≈) with sequenceV (Shaped.content ShapeT x) | sequenceV (Shaped.content ShapeT y) | sequenceV-cong content≈ +sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | just {x} {y} x≈y = just (refl , (begin + content (fill s x) + ≡⟨ fill-content s x ⟩ + x + ≈⟨ x≈y ⟩ + y + ≡⟨ sym (fill-content s y) ⟩ + content (fill s y) ∎)) + where open EqR (VecISetoid α at _) + open Shaped ShapeT +sequence-cong ShapeT α (shape≈ , content≈) | .nothing | .nothing | nothing = nothing + +theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G j)) → (u : Get.SourceContainer G (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → ShapedISetoid (EqSetoid _) (Get.ViewShapeT G) (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ Get.fmapV G just v +theorem-2 G {i} j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G i)))) (fromFunc (denumerate (Get.SourceShapeT G) s))) (Shaped.arity (Get.SourceShapeT G) (Get.|gl₁| G j)))) <$> (assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G j)))) (Shaped.content (Get.ViewShapeT G) v))) p) +theorem-2 G {i} j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G j)))) (Shaped.content (Get.ViewShapeT G) v)) ph′) +theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = refl , (begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩ + content (get u) + ≡⟨ cong content (just-injective (trans (cong (_<$>_ get) (sym p)) + (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph))) ⟩ + content (get (h′↦r (h↦h′ h))) ≡⟨ refl ⟩ - get (fmap (flip lookupM (h↦h′ h)) t) - ≡⟨ free-theorem (flip lookupM (h↦h′ h)) t ⟩ - map (flip lookupM (h↦h′ h)) (get t) - ≡⟨ lemma-union-not-used h g′ (get t) (lemma-assoc-domain (get t) v h ph) ⟩ - map (flip lookupM h) (get t) - ≈⟨ lemma-2 (get t) v h ph ⟩ - map just v ∎ + content (get (fmapS (flip lookupM (h↦h′ h)) t)) + ≡⟨ cong content (free-theorem (flip lookupM (h↦h′ h)) t) ⟩ + content (fmapV (flip lookupM (h↦h′ h)) (get t)) + ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩ + map (flip lookupM (h↦h′ h)) (content (get t)) + ≡⟨ lemma-union-not-used h g′ (content (get t)) (lemma-assoc-domain (content (get t)) (content v) h ph) ⟩ + map (flip lookupM h) (content (get t)) + ≈⟨ lemma-2 (content (get t)) (content v) h ph ⟩ + map just (content v) + ≡⟨ sym (Shaped.fmap-content ViewShapeT just v) ⟩ + content (fmapV just v) ∎) where open SetoidReasoning open Get G - s′ = enumerate ShapeT (|gl₁| i) - g = fromFunc (denumerate ShapeT s) - g′ = delete-many (get s′) g - t = enumerate ShapeT (|gl₁| j) - h↦h′ = flip union (reshape g′ (arity (|gl₁| j))) - h′↦r = (λ f → fmap f t) ∘ flip lookupM + open Shaped ViewShapeT using (content) + s′ = enumerate SourceShapeT (|gl₁| i) + g = fromFunc (denumerate SourceShapeT s) + g′ = delete-many (Shaped.content ViewShapeT (get s′)) g + t = enumerate SourceShapeT (|gl₁| j) + h↦h′ = flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j))) + h′↦r = (λ f → fmapS f t) ∘ flip lookupM -theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Get.Container G Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (Get.fmap G just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v +theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G j)) → (u : Get.SourceContainer G Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (EqSetoid _) (Get.ViewShapeT G) A.setoid at _ ∋ Get.get G u ≈ v theorem-2′ G j s v u p = drop-just (begin get <$> just u - ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence ShapeT u)) ⟩ - get <$> sequence (fmap just u) - ≡⟨ lemma-get-sequence G (lemma-just-sequence ShapeT u) ⟩ - sequenceV (get (fmap just u)) - ≈⟨ sequence-cong (theorem-2 G j s v (fmap just u) p) ⟩ - sequenceV (map just v) - ≡⟨ lemma-just-sequenceV v ⟩ + ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence SourceShapeT u)) ⟩ + get <$> Shaped.sequence SourceShapeT (fmapS just u) + ≡⟨ lemma-get-sequence G (lemma-just-sequence SourceShapeT u) ⟩ + Shaped.sequence ViewShapeT (get (fmapS just u)) + ≈⟨ sequence-cong ViewShapeT A.setoid (theorem-2 G j s v (fmapS just u) p) ⟩ + Shaped.sequence ViewShapeT (fmapV just v) + ≡⟨ lemma-just-sequence ViewShapeT v ⟩ just v ∎) - where open EqR (MaybeSetoid (VecISetoid A.setoid at _)) - open Get G + where open Get G + open EqR (MaybeSetoid (ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _)) diff --git a/GetTypes.agda b/GetTypes.agda index 0db3f31..2812e2b 100644 --- a/GetTypes.agda +++ b/GetTypes.agda @@ -84,3 +84,43 @@ PartialVecVec-to-PartialShapeVec G = record ; get = get ; free-theorem = free-theorem } where open PartialVecVec.Get G + +module PartialShapeShape where + record Get : Set₁ where + field + SourceShape : Set + SourceContainer : Set → SourceShape → Set + SourceShapeT : Shaped SourceShape SourceContainer + + ViewShape : Set + ViewContainer : Set → ViewShape → Set + ViewShapeT : Shaped ViewShape ViewContainer + + I : Setoid ℓ₀ ℓ₀ + gl₁ : I ↪ EqSetoid SourceShape + gl₂ : I ⟶ EqSetoid ViewShape + + |I| = Setoid.Carrier I + |gl₁| = _⟨$⟩_ (to gl₁) + |gl₂| = _⟨$⟩_ gl₂ + + open Shaped SourceShapeT using () renaming (fmap to fmapS) + open Shaped ViewShapeT using () renaming (fmap to fmapV) + + field + get : {A : Set} {i : |I|} → SourceContainer A (|gl₁| i) → ViewContainer A (|gl₂| i) + free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get + + open Shaped SourceShapeT public using () renaming (fmap to fmapS) + open Shaped ViewShapeT public using () renaming (fmap to fmapV) + +PartialShapeVec-to-PartialShapeShape : PartialShapeVec.Get → PartialShapeShape.Get +PartialShapeVec-to-PartialShapeShape G = record + { SourceShapeT = ShapeT + ; ViewShapeT = VecShaped + ; I = I + ; gl₁ = gl₁ + ; gl₂ = gl₂ + ; get = get + ; free-theorem = free-theorem + } where open PartialShapeVec.Get G diff --git a/Instances.agda b/Instances.agda index b41b0a2..2e4ed3e 100644 --- a/Instances.agda +++ b/Instances.agda @@ -1,13 +1,22 @@ module Instances where +open import Level using () renaming (zero to ℓ₀) open import Category.Functor using (RawFunctor) open import Data.Maybe as M using (Maybe) open import Data.Nat using (ℕ) +open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂) open import Data.Vec using (Vec) +import Data.Vec.Equality +open Data.Vec.Equality.PropositionalEquality using () renaming (to-≡ to VecEq-to-≡) open import Function using (_∘_ ; id) -open import Relation.Binary.PropositionalEquality as P using (_≗_ ; refl) +open import Relation.Binary using (Setoid ; module Setoid) +open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) +open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; module ≡-Reasoning) -open import Structures using (Functor ; Shaped) +open Setoid using () renaming (_≈_ to _∋_≈_) + +open import Generic using (VecISetoid) +open import Structures using (Functor ; Shaped ; module Shaped) MaybeFunctor : Functor Maybe MaybeFunctor = record @@ -21,15 +30,15 @@ MaybeFunctor = record cong : {α β : Set} {g h : α → β} → g ≗ h → _<$>_ g ≗ _<$>_ h cong g≗h (M.just x) = P.cong M.just (g≗h x) - cong g≗h M.nothing = refl + cong g≗h M.nothing = P.refl identity : {α : Set} → _<$>_ {α} id ≗ id - identity (M.just x) = refl - identity M.nothing = refl + identity (M.just x) = P.refl + identity M.nothing = P.refl composition : {α β γ : Set} → (g : β → γ) → (h : α → β) → _<$>_ (g ∘ h) ≗ _<$>_ g ∘ _<$>_ h - composition g h (M.just x) = refl - composition g h M.nothing = refl + composition g h (M.just x) = P.refl + composition g h M.nothing = P.refl VecShaped : Shaped ℕ Vec VecShaped = record @@ -37,6 +46,28 @@ VecShaped = record ; content = id ; fill = λ _ → id ; isShaped = record - { content-fill = λ _ → refl - ; fill-content = λ _ _ → refl + { content-fill = λ _ → P.refl + ; fill-content = λ _ _ → P.refl } } + +ShapedISetoid : (S : Setoid ℓ₀ ℓ₀) {C : Set → (Setoid.Carrier S) → Set} → Shaped (Setoid.Carrier S) C → Setoid ℓ₀ ℓ₀ → ISetoid (Setoid.Carrier S) ℓ₀ ℓ₀ +ShapedISetoid S {C} ShapeT α = record + { Carrier = C (Setoid.Carrier α) + ; _≈_ = λ {s₁} {s₂} c₁ c₂ → S ∋ s₁ ≈ s₂ × ISetoid._≈_ (VecISetoid α) (content c₁) (content c₂) + ; isEquivalence = record + { refl = Setoid.refl S , ISetoid.refl (VecISetoid α) + ; sym = λ p → Setoid.sym S (proj₁ p) , ISetoid.sym (VecISetoid α) (proj₂ p) + ; trans = λ p q → Setoid.trans S (proj₁ p) (proj₁ q) , ISetoid.trans (VecISetoid α) (proj₂ p) (proj₂ q) + } } where open Shaped ShapeT + +Shaped≈-to-≡ : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Set) → {s : S} {x y : C α s} → ShapedISetoid (P.setoid S) ShapeT (P.setoid α) at s ∋ x ≈ y → x ≡ y +Shaped≈-to-≡ ShapeT α {s} {x} {y} (shape≈ , content≈) = begin + x + ≡⟨ P.sym (content-fill x) ⟩ + fill s (content x) + ≡⟨ P.cong (fill s) (VecEq-to-≡ content≈) ⟩ + fill s (content y) + ≡⟨ content-fill y ⟩ + y ∎ + where open ≡-Reasoning + open Shaped ShapeT diff --git a/Precond.agda b/Precond.agda index bc54cd5..85c955c 100644 --- a/Precond.agda +++ b/Precond.agda @@ -25,7 +25,7 @@ open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import Relation.Nullary using (yes ; no) -open import Structures using (IsFunctor) +open import Structures using (IsFunctor ; Shaped) open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id) import CheckInsert open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) @@ -33,7 +33,7 @@ import BFF import Bidir open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain) import GetTypes -open GetTypes.PartialShapeVec using (Get ; module Get) +open GetTypes.PartialShapeShape using (Get ; module Get) open BFF.PartialShapeBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff) lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.just (just a) ma ≡ Maybe.just (maybe′ id a ma) @@ -63,32 +63,32 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎ inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i) -assoc-enough : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → ∃ (λ h → assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G j))) v ≡ just h) → ∃ λ u → bff G j s v ≡ just u -assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmap f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (arity (|gl₁| j))))) p +assoc-enough : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G j)) → ∃ (λ h → assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G j)))) (Shaped.content (Get.ViewShapeT G) v) ≡ just h) → ∃ λ u → bff G j s v ≡ just u +assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j))))) p where open Get G - g′ = delete-many (get (enumerate ShapeT (|gl₁| i))) (fromFunc (denumerate ShapeT s)) - t = enumerate ShapeT (|gl₁| j) + g′ = delete-many (Shaped.content ViewShapeT (get (enumerate SourceShapeT (|gl₁| i)))) (fromFunc (denumerate SourceShapeT s)) + t = enumerate SourceShapeT (|gl₁| j) -assoc-enough′ : (G : Get) → {i : Get.|I| G} → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G i))) v ≡ just h) → ∃ λ u → bff G i s v ≡ just (Get.fmap G just u) +assoc-enough′ : (G : Get) → {i : Get.|I| G} → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G i)))) (Shaped.content (Get.ViewShapeT G) v) ≡ just h) → ∃ λ u → bff G i s v ≡ just (Get.fmapS G just u) assoc-enough′ G {i} s v (h , p) = _ , (begin bff G i s v ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩ - just (fmap (flip lookupM (union h (reshape g′ (arity (|gl₁| i))))) t) + just (fmapS (flip lookupM (union h (reshape g′ (Shaped.arity SourceShapeT (|gl₁| i))))) t) ≡⟨ cong just (begin _ - ≡⟨ cong ((λ f → fmap f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩ - fmap (flip lookupM (union h g′)) t - ≡⟨ cong ((λ f → fmap f t) ∘ flip lookupM) (proj₂ wp) ⟩ - fmap (flip lookupM (fromFunc (proj₁ wp))) t - ≡⟨ IsFunctor.cong (isFunctor (|gl₁| i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩ - fmap (Maybe.just ∘ proj₁ wp) t - ≡⟨ IsFunctor.composition (isFunctor (|gl₁| i)) just (proj₁ wp) t ⟩ - fmap Maybe.just (fmap (proj₁ wp) t) ∎) ⟩ _ ∎) + ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩ + fmapS (flip lookupM (union h g′)) t + ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩ + fmapS (flip lookupM (fromFunc (proj₁ wp))) t + ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (|gl₁| i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩ + fmapS (Maybe.just ∘ proj₁ wp) t + ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (|gl₁| i)) just (proj₁ wp) t ⟩ + fmapS Maybe.just (fmapS (proj₁ wp) t) ∎) ⟩ _ ∎) where open Get G - s′ = enumerate ShapeT (|gl₁| i) - g = fromFunc (denumerate ShapeT s) - g′ = delete-many (get s′) g - t = enumerate ShapeT (|gl₁| i) - wp = lemma-union-delete-fromFunc (lemma-assoc-domain (get t) v h p) + s′ = enumerate SourceShapeT (|gl₁| i) + g = fromFunc (denumerate SourceShapeT s) + g′ = delete-many (Shaped.content ViewShapeT (get s′)) g + t = enumerate SourceShapeT (|gl₁| i) + wp = lemma-union-delete-fromFunc (lemma-assoc-domain (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT v) h p) data All-different {A : Set} : List A → Set where different-[] : All-different [] -- cgit v1.2.3