diff options
author | Sean Whitton <spwhitton@spwhitton.name> | 2018-11-23 17:29:46 -0700 |
---|---|---|
committer | Sean Whitton <spwhitton@spwhitton.name> | 2018-11-23 17:29:46 -0700 |
commit | 5a91775bd7c909bbaf3b3c8ee964136961a5146d (patch) | |
tree | cea89f085c1382f1567ff71a30b6f953708dc6a9 /src/Data/Maybe/Base.agda | |
parent | 5d2b156377dce5bdca65b14639306eaed3ac3a92 (diff) | |
parent | a19b25a865b2000bbd3acd909f5951a5407c1eec (diff) |
Merge tag 'upstream/0.17'
Upstream version 0.17
# gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST
# gpg: using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240
# gpg: issuer "spwhitton@spwhitton.name"
# gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate]
# Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4 753F 0F56 D055 3B6D 411B
# Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC 248B 695B 7AE4 BF06 6240
Diffstat (limited to 'src/Data/Maybe/Base.agda')
-rw-r--r-- | src/Data/Maybe/Base.agda | 52 |
1 files changed, 45 insertions, 7 deletions
diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda index 33317e5..b399444 100644 --- a/src/Data/Maybe/Base.agda +++ b/src/Data/Maybe/Base.agda @@ -17,12 +17,17 @@ data Maybe {a} (A : Set a) : Set a where {-# FOREIGN GHC type AgdaMaybe a b = Maybe b #-} {-# COMPILE GHC Maybe = data MAlonzo.Code.Data.Maybe.Base.AgdaMaybe (Just | Nothing) #-} +open import Function +open import Agda.Builtin.Equality using (_≡_ ; refl) + +just-injective : ∀ {a} {A : Set a} {a b} → (Maybe A ∋ just a) ≡ just b → a ≡ b +just-injective refl = refl + ------------------------------------------------------------------------ -- Some operations open import Data.Bool.Base using (Bool; true; false; not) open import Data.Unit.Base using (⊤) -open import Function open import Relation.Nullary boolToMaybe : Bool → Maybe ⊤ @@ -52,16 +57,23 @@ maybe j n nothing = n maybe′ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → B → Maybe A → B maybe′ = maybe +-- A defaulting mechanism + +fromMaybe : ∀ {a} {A : Set a} → A → Maybe A → A +fromMaybe = maybe′ id + -- A safe variant of "fromJust". If the value is nothing, then the -- return type is the unit type. -From-just : ∀ {a} (A : Set a) → Maybe A → Set a -From-just A (just _) = A -From-just A nothing = Lift ⊤ +module _ {a} {A : Set a} where -from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just A x -from-just (just x) = x -from-just nothing = _ + From-just : Maybe A → Set a + From-just (just _) = A + From-just nothing = Lift a ⊤ + + from-just : (x : Maybe A) → From-just x + from-just (just x) = x + from-just nothing = _ -- Functoriality: map. @@ -93,3 +105,29 @@ to-witness (just {x = p} _) = p to-witness-T : ∀ {p} {P : Set p} (m : Maybe P) → T (is-just m) → P to-witness-T (just p) _ = p to-witness-T nothing () + +------------------------------------------------------------------------ +-- Aligning and Zipping + +open import Data.These using (These; this; that; these) +open import Data.Product hiding (zip) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where + + alignWith : (These A B → C) → Maybe A → Maybe B → Maybe C + alignWith f (just a) (just b) = just (f (these a b)) + alignWith f (just a) nothing = just (f (this a)) + alignWith f nothing (just b) = just (f (that b)) + alignWith f nothing nothing = nothing + + zipWith : (A → B → C) → Maybe A → Maybe B → Maybe C + zipWith f (just a) (just b) = just (f a b) + zipWith _ _ _ = nothing + +module _ {a b} {A : Set a} {B : Set b} where + + align : Maybe A → Maybe B → Maybe (These A B) + align = alignWith id + + zip : Maybe A → Maybe B → Maybe (A × B) + zip = zipWith _,_ |