From 88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 17 Dec 2013 08:49:24 +0100 Subject: refactor to get rid of FinMap without Maybe entirely The union was the only user of this type and now it uses only partial mappings. So drop remaining uses of FinMap and make everything work with FinMapMaybe instead. --- Bidir.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'Bidir.agda') diff --git a/Bidir.agda b/Bidir.agda index c74601a..1e65bab 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -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) -- cgit v1.2.3