diff options
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 46 |
1 files changed, 24 insertions, 22 deletions
@@ -9,16 +9,18 @@ import Level import Category.Monad import Category.Functor open import Data.Maybe using (Maybe ; nothing ; just ; maybe′ ; drop-just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq) -open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) -open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) +import Data.Maybe.Categorical +open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_) +open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_) open import Data.List using (List) open import Data.List.All using (All) 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.Relation.Pointwise.Inductive using (Pointwise) open import Data.Vec.Properties using (lookup∘tabulate ; lookup∘update ; map-cong ; map-∘ ; map-lookup-allFin) open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) open import Function using (id ; _∘_ ; flip) -open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) +open import Relation.Binary.Indexed.Heterogeneous using () renaming (IndexedSetoid to ISetoid) +open import Relation.Binary.Indexed.Heterogeneous.Construct.At using (_atₛ_) open import Relation.Binary.PropositionalEquality as P using (_≡_ ; inspect ; [_] ; module ≡-Reasoning) open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid) import Relation.Binary.EqReasoning as EqR @@ -80,19 +82,19 @@ lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = (P.trans (lemma-lookupM-checkInsert j i h pl x ph) (P.sym pl)) (lemma-map-lookupM-assoc i x h ph js pj) -lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → VecISetoid (MaybeSetoid A.setoid) at _ ∋ map (flip lookupM h) is ≈ map just v +lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → VecISetoid (MaybeSetoid A.setoid) atₛ _ ∋ map (flip lookupM h) is ≈ map just v lemma-2 [] [] h p = ISetoid.refl (VecISetoid (MaybeSetoid A.setoid)) lemma-2 (i ∷ is) (x ∷ xs) h p with assoc is xs | inspect (assoc is) xs lemma-2 (i ∷ is) (x ∷ xs) h () | nothing | _ lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin lookupM i h ∷ map (flip lookupM h) is - ≈⟨ VecEq._∷-cong_ (lemma-lookupM-checkInserted i x h' p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩ + ≈⟨ Pointwise._∷_ (lemma-lookupM-checkInserted i x h' p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩ just x ∷ map (flip lookupM h) is ≡⟨ P.cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h' p is (lemma-assoc-domain is xs ir)) ⟩ just x ∷ map (flip lookupM h') is - ≈⟨ VecEq._∷-cong_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩ + ≈⟨ Pointwise._∷_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩ just x ∷ map just xs ∎ - where open EqR (VecISetoid (MaybeSetoid A.setoid) at _) + where open EqR (VecISetoid (MaybeSetoid A.setoid) atₛ _) 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 @@ -231,16 +233,16 @@ module _ (G : Get) where ≡⟨ P.cong (sequenceView ∘ get) (P.sym (lemma-sequence-successful SourceShapeT v p)) ⟩ sequenceView (get v) ∎ -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 S 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 _)) +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 Pointwise.[] = Setoid.refl (MaybeSetoid (VecISetoid S atₛ _)) +sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequenceV-cong S xs≈ys +sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (Pointwise._∷_ x≈y p) +sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | nothing | just sys | () +sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | just sxs | nothing | () +sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S atₛ _)) +sequenceV-cong S (Pointwise._∷_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S atₛ _)) -sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (P.setoid S) ShapeT (MaybeSetoid α) at _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (P.setoid S) ShapeT α at _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y +sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (P.setoid S) ShapeT (MaybeSetoid α) atₛ _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (P.setoid 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 (P.refl , (begin content (fill s x) @@ -250,7 +252,7 @@ sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | ju y ≡⟨ P.sym (fill-content s y) ⟩ content (fill s y) ∎)) - where open EqR (VecISetoid α at _) + where open EqR (VecISetoid α atₛ _) open Shaped ShapeT sequence-cong ShapeT α (shape≈ , content≈) | .nothing | .nothing | nothing = nothing @@ -259,7 +261,7 @@ module _ (G : Get) where open Shaped SourceShapeT using () renaming (arity to arityS) open Shaped ViewShapeT using () renaming (content to contentV) - theorem-2 : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer (Maybe Carrier) (gl₁ j)) → bff G j s v ≡ just u → ShapedISetoid (P.setoid _) ViewShapeT (MaybeSetoid A.setoid) at _ ∋ get u ≈ Get.fmapV G just v + theorem-2 : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer (Maybe Carrier) (gl₁ j)) → bff G j s v ≡ just u → ShapedISetoid (P.setoid _) ViewShapeT (MaybeSetoid A.setoid) atₛ _ ∋ get u ≈ Get.fmapV G just v theorem-2 {i} j s v u p with lemma-<$>-just ((flip union (reshape (delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))) (arityS (gl₁ j)))) <$> assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) p theorem-2 {i} j s v u p | h′ , ph′ with lemma-<$>-just (assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) ph′ theorem-2 {i} j s v u p | h′ , ph′ | h , ph = P.refl , (begin @@ -279,7 +281,7 @@ module _ (G : Get) where map just (contentV v) ≡⟨ P.sym (Shaped.fmap-content ViewShapeT just v) ⟩ contentV (fmapV just v) ∎) - where open EqR (VecISetoid (MaybeSetoid A.setoid) at _) + where open EqR (VecISetoid (MaybeSetoid A.setoid) atₛ _) s′ = enumerate SourceShapeT (gl₁ i) g = fromFunc (denumerate SourceShapeT s) g′ = delete-many (contentV (get s′)) g @@ -290,7 +292,7 @@ module _ (G : Get) where module _ (G : Get) where open Get G - theorem-2′ : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer Carrier (gl₁ j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (P.setoid _) ViewShapeT A.setoid at _ ∋ get u ≈ v + theorem-2′ : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer Carrier (gl₁ j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (P.setoid _) ViewShapeT A.setoid atₛ _ ∋ get u ≈ v theorem-2′ j s v u p = drop-just (begin get <$> just u ≡⟨ P.cong (_<$>_ get) (P.sym (lemma-just-sequence SourceShapeT u)) ⟩ @@ -301,4 +303,4 @@ module _ (G : Get) where Shaped.sequence ViewShapeT (fmapV just v) ≡⟨ lemma-just-sequence ViewShapeT v ⟩ just v ∎) - where open EqR (MaybeSetoid (ShapedISetoid (P.setoid _) ViewShapeT A.setoid at _)) + where open EqR (MaybeSetoid (ShapedISetoid (P.setoid _) ViewShapeT A.setoid atₛ _)) |