diff options
| -rw-r--r-- | BFF.agda | 2 | ||||
| -rw-r--r-- | Bidir.agda | 12 | ||||
| -rw-r--r-- | FinMap.agda | 49 | ||||
| -rw-r--r-- | Precond.agda | 2 |
4 files changed, 28 insertions, 37 deletions
@@ -35,7 +35,7 @@ module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n)) bff get s v = let s′ = enumerate s t′ = get s′ - g = partialize (fromFunc (denumerate s)) + g = fromFunc (denumerate s) g′ = delete-many t′ g h = assoc t′ v h′ = (flip union g′) <$> h @@ -113,20 +113,20 @@ theorem-1 get s = begin ≡⟨ cong (h′↦r ∘ h↦h′) (lemma-1 (denumerate s) (get (enumerate s))) ⟩ (h′↦r ∘ h↦h′ ∘ just) (restrict (denumerate s) (toList (get (enumerate s)))) ≡⟨ refl ⟩ - (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s))))) + (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩ - (h′↦r ∘ just) (partialize (fromFunc (denumerate s))) + (h′↦r ∘ just) (fromFunc (denumerate s)) ≡⟨ refl ⟩ - mapMV (flip lookupVec (partialize (fromFunc (denumerate s)))) (enumerate s) - ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-partialize-fromFunc (denumerate s)) ⟩ - mapMV (flip lookupVec (fromFunc (Maybe.just ∘ denumerate s))) (enumerate s) + mapMV (flip lookupVec (fromFunc (denumerate s))) (enumerate s) + ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-fromFunc-tabulate (denumerate s)) ⟩ + mapMV (flip lookupVec (tabulate (Maybe.just ∘ denumerate s))) (enumerate s) ≡⟨ mapMV-cong (lookup∘tabulate (Maybe.just ∘ 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 ∎ - where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s))))) + where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec) diff --git a/FinMap.agda b/FinMap.agda index 8cde5a6..c125c47 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -33,17 +33,11 @@ fromAscList : {A : Set} {n : ℕ} → List (Fin n × A) → FinMapMaybe n A fromAscList [] = empty fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs) -FinMap : ℕ → Set → Set -FinMap n A = Vec A n - -lookup : {A : Set} {n : ℕ} → Fin n → FinMap n A → A -lookup = lookupVec - -fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMap n A -fromFunc = tabulate +fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A +fromFunc = mapV just ∘ tabulate union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMapMaybe n A → FinMapMaybe n A -union m1 m2 = fromFunc (λ f → maybe′ just (lookupM f m2) (lookupM f m1)) +union m1 m2 = tabulate (λ f → maybe′ just (lookupM f m2) (lookupM f m1)) restrict : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A restrict f is = fromAscList (zip is (map f is)) @@ -54,9 +48,6 @@ delete i m = m [ i ]≔ nothing delete-many : {A : Set} {n m : ℕ} → Vec (Fin n) m → FinMapMaybe n A → FinMapMaybe n A delete-many = flip (foldr (const _) delete) -partialize : {A : Set} {n : ℕ} → FinMap n A → FinMapMaybe n A -partialize = mapV just - lemma-just≢nothing : {A Whatever : Set} {a : A} {ma : Maybe A} → ma ≡ just a → ma ≡ nothing → Whatever lemma-just≢nothing refl () @@ -99,9 +90,9 @@ lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → lemma-tabulate-∘ {zero} {_} {f} {g} f≗g = refl lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc)) -lemma-partialize-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → partialize (fromFunc f) ≡ fromFunc (just ∘ f) -lemma-partialize-fromFunc {zero} f = refl -lemma-partialize-fromFunc {suc _} f = cong (_∷_ (just (f zero))) (lemma-partialize-fromFunc (f ∘ suc)) +lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (just ∘ f) +lemma-fromFunc-tabulate {zero} f = refl +lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (f ∘ suc)) lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f lemma-lookupM-delete {i = zero} {j = zero} (_ ∷ _) p with p refl @@ -110,24 +101,24 @@ lemma-lookupM-delete {i = zero} {j = suc j} (_ ∷ _) p = refl lemma-lookupM-delete {i = suc i} {j = zero} (x ∷ xs) p = refl lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc) -lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f (toList t)) (delete-many t (partialize (fromFunc f))) ≡ partialize (fromFunc f) -lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (sym (lemma-partialize-fromFunc f)) - where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (partialize (fromFunc f)))) (lookupM x (restrict f (toList t))) ≡ just (f x) +lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f (toList t)) (delete-many t (fromFunc f)) ≡ fromFunc f +lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (sym (lemma-fromFunc-tabulate f)) + where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f (toList t))) ≡ just (f x) lemma-inner [] x = begin - maybe′ just (lookupM x (partialize (fromFunc f))) (lookupM x empty) - ≡⟨ cong (maybe′ just (lookupM x (partialize (fromFunc f)))) (lemma-lookupM-empty x) ⟩ - lookupM x (partialize (fromFunc f)) - ≡⟨ cong (lookupM x) (lemma-partialize-fromFunc f) ⟩ - lookupM x (fromFunc (just ∘ f)) + maybe′ just (lookupM x (fromFunc f)) (lookupM x empty) + ≡⟨ cong (maybe′ just (lookupM x (fromFunc f))) (lemma-lookupM-empty x) ⟩ + lookupM x (fromFunc f) + ≡⟨ cong (lookupM x) (lemma-fromFunc-tabulate f) ⟩ + lookupM x (tabulate (just ∘ f)) ≡⟨ lookup∘tabulate (just ∘ f) x ⟩ just (f x) ∎ lemma-inner (t ∷ ts) x with x ≟ t - lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (partialize (fromFunc f))))) (lemma-lookupM-insert x (f x) (restrict f (toList ts))) + lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (fromFunc f)))) (lemma-lookupM-insert x (f x) (restrict f (toList ts))) lemma-inner (t ∷ ts) x | no ¬p = begin - maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f)))) (lookupM x (restrict f (toList (t ∷ ts)))) - ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f))))) (sym (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p)) ⟩ - maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f)))) (lookupM x (restrict f (toList ts))) - ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (partialize (fromFunc f))) ¬p) ⟩ - maybe′ just (lookupM x (delete-many ts (partialize (fromFunc f)))) (lookupM x (restrict f (toList ts))) + maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList (t ∷ ts)))) + ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f)))) (sym (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p)) ⟩ + maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList ts))) + ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (fromFunc f)) ¬p) ⟩ + maybe′ just (lookupM x (delete-many ts (fromFunc f))) (lookupM x (restrict f (toList ts))) ≡⟨ lemma-inner ts x ⟩ just (f x) ∎ diff --git a/Precond.agda b/Precond.agda index 16e452b..40ffd79 100644 --- a/Precond.agda +++ b/Precond.agda @@ -20,7 +20,7 @@ open import Function using (flip ; _∘_) open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) -open import FinMap using (FinMap ; FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty) +open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty) import CheckInsert open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) import BFF |