diff options
| -rw-r--r-- | BFF.agda | 28 | ||||
| -rw-r--r-- | Bidir.agda | 171 | ||||
| -rw-r--r-- | GetTypes.agda | 40 | ||||
| -rw-r--r-- | Instances.agda | 49 | ||||
| -rw-r--r-- | Precond.agda | 42 |
5 files changed, 211 insertions, 119 deletions
@@ -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) @@ -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 [] |