Merge branch feature-omit-sequence into master
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 5 Mar 2014 07:46:28 +0000 (08:46 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 5 Mar 2014 07:46:28 +0000 (08:46 +0100)
Beyond allowing default values during shape updates, this branch simplifies
working with shapes other than Vec.

1  2 
Bidir.agda

diff --combined Bidir.agda
@@@ -16,7 -16,7 +16,7 @@@ open import Data.List.All using (All
  open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; tabulate) renaming (lookup to lookupVec)
  open import Data.Vec.Equality using () renaming (module Equality to VecEq)
  open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate ; map-cong ; map-∘)
 -open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) renaming (map to map-Σ)
 +open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
  open import Function using (id ; _∘_ ; flip)
  open import Relation.Binary.Core using (refl ; _≡_)
  open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
@@@ -26,7 -26,7 +26,7 @@@ import Relation.Binary.EqReasoning as E
  
  import GetTypes
  open GetTypes.PartialVecVec using (Get ; module Get)
- open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid)
+ open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective)
  open import FinMap
  import CheckInsert
  open CheckInsert A
@@@ -123,7 -123,7 +123,7 @@@ lemma-map-denumerate-enumerate (a ∷ a
    as ∎)
    where open ≡-Reasoning
  
- theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just s
+ 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)
  theorem-1 G {i} s = begin
    bff G i s (get s)
      ≡⟨ cong (bff G i s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩
      ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩
    (h′↦r ∘ just) (fromFunc (denumerate s))
      ≡⟨ refl ⟩
-   mapMV (flip lookupM (fromFunc (denumerate s))) (enumerate s)
-     ≡⟨ mapMV-cong (lemma-lookupM-fromFunc (denumerate s)) (enumerate s) ⟩
-   mapMV (Maybe.just ∘ denumerate s) (enumerate s)
-     ≡⟨ mapMV-purity (denumerate s) (enumerate s) ⟩
-   just (map (denumerate s) (enumerate s))
-     ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩
-   just s ∎
+   just (map (flip lookupM (fromFunc (denumerate s))) (enumerate s))
+     ≡⟨ cong just (map-cong (lemma-lookupM-fromFunc (denumerate s)) (enumerate s)) ⟩
+   just (map (Maybe.just ∘ denumerate s) (enumerate s))
+     ≡⟨ cong just (map-∘ just (denumerate s) (enumerate s)) ⟩
+   just (map just (map (denumerate s) (enumerate s)))
+     ≡⟨ cong (Maybe.just ∘ map just) (lemma-map-denumerate-enumerate s) ⟩
+   just (map just s) ∎
      where open ≡-Reasoning
            open Get G
            h↦h′ = _<$>_ (flip union (reshape (delete-many (get (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G i)))
-           h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupM)
+           h′↦r = _<$>_ (flip map (enumerate s) ∘ flip lookupM)
  
  
  lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
Content-type: text/html Untitled Git - ~helmut/bidiragda.git/commitdiff


500 - Internal Server Error

panic: pp_match start/end pointers, i=3, start=31, end=72, s=55579f98344f, strend=55579f983477, len=41 at /etc/www/git/html/index.fcgi line 2487, <$fd> line 106.