Merge branch feature-get-record into feature-partial-getlen
[~helmut/bidiragda.git] / Bidir.agda
index e792b3a..cb29420 100644 (file)
@@ -18,6 +18,9 @@ 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₂)
 open import Function using (id ; _∘_ ; flip)
+open import Function.Equality using (_⟶_ ; _⟨$⟩_)
+open import Function.Injection using (module Injection) renaming (Injection to _↪_)
+open Injection using (to)
 open import Relation.Binary.Core using (refl ; _≡_)
 open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
 open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid ; module ≡-Reasoning) renaming (setoid to EqSetoid)
@@ -25,13 +28,13 @@ open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
 import Relation.Binary.EqReasoning as EqR
 
 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
 open CheckInsert A
 import BFF
-open BFF.VecBFF A using (assoc ; enumerate ; denumerate ; bff)
+open BFF.PartialVecBFF A using (assoc ; enumerate ; denumerate ; bff)
 open Setoid using () renaming (_≈_ to _∋_≈_)
 open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
 
@@ -125,7 +128,7 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin
   as ∎)
   where open ≡-Reasoning
 
-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)) ⟩
@@ -189,9 +192,8 @@ lemma-mapM-successful         (x ∷ xs) () | just y | nothing | _
 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} {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))
@@ -219,7 +221,7 @@ sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecE
 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 : (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 _) ⟩
@@ -228,7 +230,7 @@ theorem-2 G v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (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 (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′))