Merge branch feature-get-record into feature-partial-getlen
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 4 Feb 2014 09:32:34 +0000 (10:32 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 4 Feb 2014 09:32:34 +0000 (10:32 +0100)
These two features heavily interconnect. As such it makes sense to
integrate them properly. This non-trivial merge does that work. Compared
to feature-partial-getlen a few definitions moved from FreeTheorems.agda
to GetTypes.agda. Many types changed compared to both branches.

Conflicts:
BFF.agda
Bidir.agda
FreeTheorems.agda
Precond.agda
        conflict in GetTypes.agda not detected by merge

1  2 
BFF.agda
Bidir.agda
FreeTheorems.agda
GetTypes.agda
Precond.agda

diff --cc BFF.agda
+++ b/BFF.agda
@@@ -11,19 -11,15 +11,19 @@@ open Category.Functor.RawFunctor {Level
  open import Data.List using (List ; [] ; _∷_ ; map ; length)
  open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_)
  open import Function using (id ; _∘_ ; flip)
 -open import Relation.Binary using (DecSetoid ; module DecSetoid)
 +open import Function.Equality using (_⟶_ ; _⟨$⟩_)
 +open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪)
 +open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid)
 +open import Relation.Binary.PropositionalEquality using (cong) renaming (setoid to EqSetoid)
 +open Injection using (to)
  
  open import FinMap
 -open import Generic using (mapMV)
 +open import Generic using (mapMV ; ≡-to-Π)
  import CheckInsert
- import FreeTheorems
 -import GetTypes
++open import GetTypes using (VecVec-to-PartialVecVec)
  
 -module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
 -  open GetTypes.VecVec public using (Get)
 +module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
-   open FreeTheorems.PartialVecVec public using (get-type)
++  open GetTypes.PartialVecVec public using (Get)
    open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
    open CheckInsert A
  
    denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier
    denumerate = flip lookupV
  
-   bff : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ EqSetoid ℕ) → get-type gl₁ gl₂ → ({i : Setoid.Carrier I} → Vec Carrier (to gl₁ ⟨$⟩ i) → Vec Carrier (gl₂ ⟨$⟩ i) → Maybe (Vec Carrier (to gl₁ ⟨$⟩ i)))
-   bff gl₁ gl₂ get s v =
-                 let s′ = enumerate s
-                     t′ = get s′
 -  bff : (G : Get) → ({n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n))
++
++  bff : (G : Get) → ({i : Setoid.Carrier (Get.I G)} → Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i) → Vec Carrier ((Get.gl₂ G) ⟨$⟩ i) → Maybe (Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)))
+   bff G s v = let   s′ = enumerate s
+                     t′ = Get.get G s′
                      g  = fromFunc (denumerate s)
                      g′ = delete-many t′ g
                      h  = assoc t′ v
                      h′ = (flip union g′) <$> h
                  in h′ >>= flip mapMV s′ ∘ flip lookupV
-   open FreeTheorems.VecVec public using (get-type)
 +
 +module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
-   bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n))
-   bff {getlen} get s v = PartialVecBFF.bff A id↪ (≡-to-Π getlen) get {_} s v
++  open GetTypes.VecVec public using (Get)
 +  open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
 +  open CheckInsert A
 +
 +  open PartialVecBFF A public using (assoc ; enumerate ; denumerate)
 +
++  bff : (G : Get) → ({n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n))
++  bff G = PartialVecBFF.bff A (VecVec-to-PartialVecVec G)
diff --cc Bidir.agda
@@@ -27,8 -24,8 +27,8 @@@ open import Relation.Binary.Proposition
  open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
  import Relation.Binary.EqReasoning as EqR
  
- import FreeTheorems
- open FreeTheorems.PartialVecVec using (get-type ; free-theorem)
+ import GetTypes
 -open GetTypes.VecVec using (Get ; module Get)
++open GetTypes.PartialVecVec using (Get ; module Get)
  open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map ; VecISetoid)
  open import FinMap
  import CheckInsert
@@@ -128,13 -125,13 +128,13 @@@ lemma-map-denumerate-enumerate (a ∷ a
    as ∎)
    where open ≡-Reasoning
  
- theorem-1 : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → (get : get-type gl₁ gl₂) → {i : Setoid.Carrier I} → (s : Vec Carrier (to gl₁ ⟨$⟩ i)) → bff gl₁ gl₂ get s (get s) ≡ just s
- theorem-1 gl₁ gl₂ get s = begin
-   bff gl₁ gl₂ get s (get s)
-     ≡⟨ cong (bff gl₁ gl₂ get s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩
-   bff gl₁ gl₂ get s (get (map (denumerate s) (enumerate s)))
-     ≡⟨ cong (bff gl₁ gl₂ get s) (free-theorem gl₁ gl₂ get (denumerate s) (enumerate s)) ⟩
-   bff gl₁ gl₂ get s (map (denumerate s) (get (enumerate s)))
 -theorem-1 : (G : Get) → {m : ℕ} → (s : Vec Carrier m) → bff G s (Get.get G s) ≡ just s
++theorem-1 : (G : Get) → {i : Setoid.Carrier (Get.I G)} → (s : Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)) → bff G s (Get.get G s) ≡ just s
+ theorem-1 G s = begin
+   bff G s (get s)
+     ≡⟨ cong (bff G s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩
+   bff G s (get (map (denumerate s) (enumerate s)))
+     ≡⟨ cong (bff G s) (free-theorem (denumerate s) (enumerate s)) ⟩
+   bff G s (map (denumerate s) (get (enumerate s)))
      ≡⟨ refl ⟩
    (h′↦r ∘ h↦h′) (assoc (get (enumerate s)) (map (denumerate s) (get (enumerate s))))
      ≡⟨ cong (h′↦r ∘ h↦h′) (lemma-1 (denumerate s) (get (enumerate s))) ⟩
@@@ -191,9 -189,9 +192,8 @@@ lemma-mapM-successful         (x ∷ xs
  lemma-mapM-successful         (x ∷ xs) p  | just y | just ys | [ p′ ] with lemma-mapM-successful xs p′
  lemma-mapM-successful         (x ∷ xs) p  | just y | just ys | [ p′ ] | w , pw = y ∷ w , cong (_∷_ (just y)) pw
  
--
- lemma-get-mapMV : {A B : Set} {f : A → Maybe B} {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → {i : Setoid.Carrier I} {v : Vec A (to gl₁ ⟨$⟩ i)} {r : Vec B (to gl₁ ⟨$⟩ i)} → mapMV f v ≡ just r → (get : get-type gl₁ gl₂) → get <$> mapMV f v ≡ mapMV f (get v)
- lemma-get-mapMV {f = f} gl₁ gl₂ {v = v} p get = let w , pw = lemma-mapM-successful v p in begin
 -lemma-get-mapMV : {A B : Set} {f : A → Maybe B} {n : ℕ} {v : Vec A n} {r : Vec B n} → mapMV f v ≡ just r → (get : Get) → Get.get get <$> mapMV f v ≡ mapMV f (Get.get get v)
 -lemma-get-mapMV {f = f} {v = v} p G = let w , pw = lemma-mapM-successful v p in begin
++lemma-get-mapMV : {A B : Set} {f : A → Maybe B} → (G : Get) → {i : Setoid.Carrier (Get.I G)} {v : Vec A (to (Get.gl₁ G) ⟨$⟩ i)} {r : Vec B (to (Get.gl₁ G) ⟨$⟩ i)} → mapMV f v ≡ just r → Get.get G <$> mapMV f v ≡ mapMV f (Get.get G v)
++lemma-get-mapMV {f = f} G {v = v} p = let w , pw = lemma-mapM-successful v p in begin
    get <$> mapMV f v
      ≡⟨ cong (_<$>_ get) (sym (sequence-map f v)) ⟩
    get <$> (sequenceV (map f v))
@@@ -220,16 -219,16 +221,16 @@@ sequence-cong {S} {m₁ = just x ∷ xs
  sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
  sequence-cong {S}                                       (nothing VecEq.∷-cong xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
  
- theorem-2 : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → (get : get-type gl₁ gl₂) → {i : Setoid.Carrier I} → (v : Vec Carrier (gl₂ ⟨$⟩ i)) → (s u : Vec Carrier (to gl₁ ⟨$⟩ i)) → bff gl₁ gl₂ get s v ≡ just u → VecISetoid A.setoid at _ ∋ get u ≈ v
- theorem-2 gl₁ gl₂ get v s u p with (lemma->>=-just ((flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) <$> (assoc (get (enumerate s)) v)) p)
- theorem-2 gl₁ gl₂ get v s u p | h′ , ph′ with (lemma-<$>-just (assoc (get (enumerate s)) v) ph′)
- theorem-2 gl₁ gl₂ get v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩
 -theorem-2 : (G : Get) → {m : ℕ} → (v : Vec Carrier (Get.getlen G m)) → (s u : Vec Carrier m) → bff G s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
++theorem-2 : (G : Get) → {i : Setoid.Carrier (Get.I G)} → (v : Vec Carrier (Get.gl₂ G ⟨$⟩ i)) → (s u : Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)) → bff G s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
+ theorem-2 G v s u p with (lemma->>=-just ((flip union (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s)))) <$> (assoc (Get.get G (enumerate s)) v)) p)
+ theorem-2 G v s u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumerate s)) v) ph′)
+ theorem-2 G v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩
    get <$> (just u)
      ≡⟨ cong (_<$>_ get) (sym p) ⟩
-   get <$> (bff gl₁ gl₂ get s v)
+   get <$> (bff G s v)
      ≡⟨ cong (_<$>_ get ∘ flip _>>=_ h′↦r ∘ _<$>_ h↦h′) ph ⟩
    get <$> mapMV (flip lookupM (h↦h′ h)) s′
-     ≡⟨ lemma-get-mapMV gl₁ gl₂ (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) get ⟩
 -    ≡⟨ lemma-get-mapMV (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) G ⟩
++    ≡⟨ lemma-get-mapMV G (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) ⟩
    mapMV (flip lookupM (h↦h′ h)) (get s′)
      ≡⟨ sym (sequence-map (flip lookupM (h↦h′ h)) (get s′)) ⟩
    sequenceV (map (flip lookupM (h↦h′ h)) (get s′))
@@@ -5,14 -4,10 +5,16 @@@ open import Data.Nat using (ℕ
  open import Data.List using (List ; map)
  open import Data.Vec using (Vec) renaming (map to mapV)
  open import Function using (_∘_)
 -open import Relation.Binary.PropositionalEquality using (_≗_)
 +open import Function.Equality using (_⟶_ ; _⟨$⟩_)
 +open import Function.Injection using (module Injection) renaming (Injection to _↪_)
 +open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming (setoid to EqSetoid)
 +open import Relation.Binary using (Setoid)
 +open Injection using (to)
 +
 +open import Generic using (≡-to-Π)
  
+ import GetTypes
  module ListList where
    get-type : Set₁
    get-type = {A : Set} → List A → List A
@@@ -24,20 -24,10 +31,22 @@@ module VecVec wher
    get-type : (ℕ → ℕ) → Set₁
    get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
  
-   free-theorem-type : Set₁
-   free-theorem-type = {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
+   open GetTypes.VecVec public
  
    postulate
-     free-theorem : free-theorem-type
+     free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
+   assume-get : {getlen : ℕ → ℕ} → (get : get-type getlen) → Get
+   assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get }
 +
 +module PartialVecVec where
 +  get-type : {I : Setoid ℓ₀ ℓ₀} → (I ↪ (EqSetoid ℕ)) → (I ⟶ (EqSetoid ℕ)) → Set₁
 +  get-type {I} gl₁ gl₂ = {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
 +
++  open GetTypes.PartialVecVec public
++
 +  postulate
 +    free-theorem : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂)  → {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
 +
-   open VecVec using () renaming (free-theorem-type to VecVec-free-theorem-type)
-   VecVec-free-theorem : VecVec-free-theorem-type
-   VecVec-free-theorem {getlen} get = free-theorem Function.Injection.id (≡-to-Π getlen) get
++  assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂) → Get
++  assume-get {I} gl₁ gl₂ get = record { I = I; gl₁ = gl₁; gl₂ = gl₂; get = get; free-theorem = free-theorem gl₁ gl₂ get }
diff --cc GetTypes.agda
index 0000000,99675f9..a52ec24
mode 000000,100644..100644
--- /dev/null
@@@ -1,0 -1,20 +1,45 @@@
 -open import Relation.Binary.PropositionalEquality using (_≗_)
+ module GetTypes where
++open import Level using () renaming (zero to ℓ₀)
+ open import Data.Nat using (ℕ)
+ open import Data.List using (List ; map)
+ open import Data.Vec using (Vec) renaming (map to mapV)
+ open import Function using (_∘_)
++open import Function.Equality using (_⟶_ ; _⟨$⟩_)
++open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪)
++open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid)
++open import Relation.Binary using (Setoid)
++open Injection using (to)
++
++open import Generic using (≡-to-Π)
+ module ListList where
+   record Get : Set₁ where
+     field
+       get : {A : Set} → List A → List A
+       free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
+ module VecVec where
+   record Get : Set₁ where
+     field
+       getlen : ℕ → ℕ
+       get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
+       free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
++
++module PartialVecVec where
++  record Get : Set₁ where
++    field
++      I : Setoid ℓ₀ ℓ₀
++      gl₁ : I ↪ EqSetoid ℕ
++      gl₂ : I ⟶ EqSetoid ℕ
++      get : {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
++      free-theorem : {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
++
++VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
++VecVec-to-PartialVecVec G = record
++  { I = EqSetoid ℕ
++  ; gl₁ = id↪
++  ; gl₂ = ≡-to-Π getlen
++  ; get = get
++  ; free-theorem = free-theorem
++  } where open VecVec.Get G
diff --cc Precond.agda
@@@ -34,8 -30,9 +34,9 @@@ import CheckInser
  open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
  import BFF
  open import Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
- open BFF.PartialVecBFF (decSetoid deq) using (get-type ; assoc ; enumerate ; denumerate ; bff)
+ import GetTypes
 -open GetTypes.VecVec using (Get ; module Get)
 -open BFF.VecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
++open GetTypes.PartialVecVec using (Get ; module Get)
++open BFF.PartialVecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
  
  lemma-lookup-map-just : {n : ℕ} (f : Fin n) {A : Set} (v : Vec A n) → lookup f (map Maybe.just v) ≡ Maybe.just (lookup f v)
  lemma-lookup-map-just zero    (x ∷ xs) = refl
@@@ -73,9 -70,9 +74,9 @@@ lemma-union-delete-fromFunc {n = n} {i
            maybe′ just (lookupM i (delete-many is (map just g))) (lookup i h) ∎
          inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (map just g)) f≢i)
  
- assoc-enough : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → (get : get-type gl₁ gl₂) → {i : Setoid.Carrier I} → (s : Vec Carrier (to gl₁ ⟨$⟩ i)) → (v : Vec Carrier (gl₂ ⟨$⟩ i)) → ∃ (λ h → assoc (get (enumerate s)) v ≡ just h) → ∃ λ u → bff gl₁ gl₂ get s v ≡ just u
- assoc-enough gl₁ gl₂ get s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin
-   bff gl₁ gl₂ get s v
 -assoc-enough : (G : Get) → {m : ℕ} → (s : Vec Carrier m) → (v : Vec Carrier (Get.getlen G m)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G s v ≡ just u
++assoc-enough : (G : Get) → {i : Setoid.Carrier (Get.I G)} → (s : Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)) → (v : Vec Carrier (Get.gl₂ G ⟨$⟩ i)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G s v ≡ just u
+ assoc-enough G s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin
+   bff G s v
      ≡⟨ cong (flip _>>=_ (flip mapMV s′ ∘ flip lookupM) ∘ _<$>_ (flip union g′)) p ⟩
    mapMV (flip lookupM (union h g′)) s′
      ≡⟨ sym (sequence-map (flip lookupM (union h g′)) s′) ⟩