module UVMHS.Core.Data.Pair where import UVMHS.Core.Init import UVMHS.Core.Classes import UVMHS.Core.Data.Arithmetic () instance (POrd a,POrd b) ⇒ POrd (a ∧ b) where (a x₁ :* b y₁) ⊑ :: (a ∧ b) -> (a ∧ b) -> 𝔹 ⊑ (a x₂ :* b y₂) = (a x₁ a -> a -> 𝔹 forall a. POrd a => a -> a -> 𝔹 ⊑ a x₂) 𝔹 -> 𝔹 -> 𝔹 ⩓ (b y₁ b -> b -> 𝔹 forall a. POrd a => a -> a -> 𝔹 ⊑ b y₂) instance (Bot a,Bot b) ⇒ Bot (a ∧ b) where bot :: a ∧ b bot = a forall a. Bot a => a bot a -> b -> a ∧ b forall a b. a -> b -> a ∧ b :* b forall a. Bot a => a bot instance (Join a,Join b) ⇒ Join (a ∧ b) where (a a₁ :* b b₁) ⊔ :: (a ∧ b) -> (a ∧ b) -> a ∧ b ⊔ (a a₂ :* b b₂) = (a a₁ a -> a -> a forall a. Join a => a -> a -> a ⊔ a a₂) a -> b -> a ∧ b forall a b. a -> b -> a ∧ b :* (b b₁ b -> b -> b forall a. Join a => a -> a -> a ⊔ b b₂) instance (Top a,Top b) ⇒ Top (a ∧ b) where top :: a ∧ b top = a forall a. Top a => a top a -> b -> a ∧ b forall a b. a -> b -> a ∧ b :* b forall a. Top a => a top instance (Meet a,Meet b) ⇒ Meet (a ∧ b) where (a a₁ :* b b₁) ⊓ :: (a ∧ b) -> (a ∧ b) -> a ∧ b ⊓ (a a₂ :* b b₂) = (a a₁ a -> a -> a forall a. Meet a => a -> a -> a ⊓ a a₂) a -> b -> a ∧ b forall a b. a -> b -> a ∧ b :* (b b₁ b -> b -> b forall a. Meet a => a -> a -> a ⊓ b b₂) instance (Dual a,Dual b) ⇒ Dual (a ∧ b) where dual :: (a ∧ b) -> a ∧ b dual (a a :* b b) = a -> a forall a. Dual a => a -> a dual a a a -> b -> a ∧ b forall a b. a -> b -> a ∧ b :* b -> b forall a. Dual a => a -> a dual b b instance (Difference a,Difference b) ⇒ Difference (a ∧ b) where (a a₁ :* b b₁) ⊟ :: (a ∧ b) -> (a ∧ b) -> a ∧ b ⊟ (a a₂ :* b b₂) = (a a₁ a -> a -> a forall a. Difference a => a -> a -> a ⊟ a a₂) a -> b -> a ∧ b forall a b. a -> b -> a ∧ b :* (b b₁ b -> b -> b forall a. Difference a => a -> a -> a ⊟ b b₂) instance (JoinLattice a,JoinLattice b) ⇒ JoinLattice (a ∧ b) instance (MeetLattice a,MeetLattice b) ⇒ MeetLattice (a ∧ b) instance (Lattice a,Lattice b) ⇒ Lattice (a ∧ b) instance (Null a,Null b) ⇒ Null (a ∧ b) where null :: a ∧ b null = (a forall a. Null a => a null a -> b -> a ∧ b forall a b. a -> b -> a ∧ b :* b forall a. Null a => a null) instance (Append a,Append b) ⇒ Append (a ∧ b) where (a x₁ :* b y₁) ⧺ :: (a ∧ b) -> (a ∧ b) -> a ∧ b ⧺ (a x₂ :* b y₂) = (a x₁ a -> a -> a forall a. Append a => a -> a -> a ⧺ a x₂) a -> b -> a ∧ b forall a b. a -> b -> a ∧ b :* (b y₁ b -> b -> b forall a. Append a => a -> a -> a ⧺ b y₂) instance (Monoid a,Monoid b) ⇒ Monoid (a ∧ b) instance Functor ((∧) a) where map :: forall a b. (a -> b) -> (a ∧ a) -> a ∧ b map a -> b f (a x :* a y) = a x a -> b -> a ∧ b forall a b. a -> b -> a ∧ b :* a -> b f a y instance (Null a) ⇒ Return ((∧) a) where return :: forall a. a -> a ∧ a return = a -> a -> a ∧ a forall a b. a -> b -> a ∧ b (:*) a forall a. Null a => a null instance (Append a) ⇒ Bind ((∧) a) where (a a :* a b) ≫= :: forall a b. (a ∧ a) -> (a -> a ∧ b) -> a ∧ b ≫= a -> a ∧ b f = let (a a' :* b c) = a -> a ∧ b f a b in (a a a -> a -> a forall a. Append a => a -> a -> a ⧺ a a') a -> b -> a ∧ b forall a b. a -> b -> a ∧ b :* b c instance (Monoid a) ⇒ Monad ((∧) a) instance FunctorM ((∧) a) where mapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> (a ∧ a) -> m (a ∧ b) mapM a -> m b f (a x :* a y) = (b -> a ∧ b) -> m b -> m (a ∧ b) forall a b. (a -> b) -> m a -> m b forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b map (a -> b -> a ∧ b forall a b. a -> b -> a ∧ b (:*) a x) (m b -> m (a ∧ b)) -> m b -> m (a ∧ b) forall a b. (a -> b) -> a -> b $ a -> m b f a y fst ∷ a ∧ b → a fst :: forall a b. (a ∧ b) -> a fst (a x :* b _) = a x snd ∷ a ∧ b → b snd :: forall a b. (a ∧ b) -> b snd (a _ :* b y) = b y swap ∷ a ∧ b → b ∧ a swap :: forall a b. (a ∧ b) -> b ∧ a swap (a x :* b y) = b y b -> a -> b ∧ a forall a b. a -> b -> a ∧ b :* a x mapPair ∷ (a₁ → a₂) → (b₁ → b₂) → a₁ ∧ b₁ → a₂ ∧ b₂ mapPair :: forall a₁ a₂ b₁ b₂. (a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∧ b₁) -> a₂ ∧ b₂ mapPair a₁ -> a₂ f b₁ -> b₂ g (a₁ x :* b₁ y) = a₁ -> a₂ f a₁ x a₂ -> b₂ -> a₂ ∧ b₂ forall a b. a -> b -> a ∧ b :* b₁ -> b₂ g b₁ y mapBoth ∷ (a → a') → a ∧ a → a' ∧ a' mapBoth :: forall a a'. (a -> a') -> (a ∧ a) -> a' ∧ a' mapBoth a -> a' f = (a -> a') -> (a -> a') -> (a ∧ a) -> a' ∧ a' forall a₁ a₂ b₁ b₂. (a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∧ b₁) -> a₂ ∧ b₂ mapPair a -> a' f a -> a' f mapFst ∷ (a₁ → a₂) → a₁ ∧ b → a₂ ∧ b mapFst :: forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b mapFst a₁ -> a₂ f = (a₁ -> a₂) -> (b -> b) -> (a₁ ∧ b) -> a₂ ∧ b forall a₁ a₂ b₁ b₂. (a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∧ b₁) -> a₂ ∧ b₂ mapPair a₁ -> a₂ f b -> b forall a. a -> a id mapSnd ∷ (b₁ → b₂) → a ∧ b₁ → a ∧ b₂ mapSnd :: forall b₁ b₂ a. (b₁ -> b₂) -> (a ∧ b₁) -> a ∧ b₂ mapSnd b₁ -> b₂ f = (a -> a) -> (b₁ -> b₂) -> (a ∧ b₁) -> a ∧ b₂ forall a₁ a₂ b₁ b₂. (a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∧ b₁) -> a₂ ∧ b₂ mapPair a -> a forall a. a -> a id b₁ -> b₂ f mapMPair ∷ (Monad m) ⇒ (a → m a') → (b → m b') → a ∧ b → m (a' ∧ b') mapMPair :: forall (m :: * -> *) a a' b b'. Monad m => (a -> m a') -> (b -> m b') -> (a ∧ b) -> m (a' ∧ b') mapMPair a -> m a' f b -> m b' g (a x :* b y) = do a' x' ← a -> m a' f a x b' y' ← b -> m b' g b y (a' ∧ b') -> m (a' ∧ b') forall a. a -> m a forall (m :: * -> *) a. Return m => a -> m a return ((a' ∧ b') -> m (a' ∧ b')) -> (a' ∧ b') -> m (a' ∧ b') forall a b. (a -> b) -> a -> b $ a' x' a' -> b' -> a' ∧ b' forall a b. a -> b -> a ∧ b :* b' y' mapMBoth ∷ (Monad m) ⇒ (a → m a) → a ∧ a → m (a ∧ a) mapMBoth :: forall (m :: * -> *) a. Monad m => (a -> m a) -> (a ∧ a) -> m (a ∧ a) mapMBoth a -> m a f = (a -> m a) -> (a -> m a) -> (a ∧ a) -> m (a ∧ a) forall (m :: * -> *) a a' b b'. Monad m => (a -> m a') -> (b -> m b') -> (a ∧ b) -> m (a' ∧ b') mapMPair a -> m a f a -> m a f mapMFst ∷ (Monad m) ⇒ (a → m a') → a ∧ b → m (a' ∧ b) mapMFst :: forall (m :: * -> *) a a' b. Monad m => (a -> m a') -> (a ∧ b) -> m (a' ∧ b) mapMFst = ((a -> m a') -> (b -> m b) -> (a ∧ b) -> m (a' ∧ b)) -> (b -> m b) -> (a -> m a') -> (a ∧ b) -> m (a' ∧ b) forall a b c. (a -> b -> c) -> b -> a -> c flip (a -> m a') -> (b -> m b) -> (a ∧ b) -> m (a' ∧ b) forall (m :: * -> *) a a' b b'. Monad m => (a -> m a') -> (b -> m b') -> (a ∧ b) -> m (a' ∧ b') mapMPair b -> m b forall a. a -> m a forall (m :: * -> *) a. Return m => a -> m a return mapMSnd ∷ (Monad m) ⇒ (b → m b') → a ∧ b → m (a ∧ b') mapMSnd :: forall (m :: * -> *) b b' a. Monad m => (b -> m b') -> (a ∧ b) -> m (a ∧ b') mapMSnd = (a -> m a) -> (b -> m b') -> (a ∧ b) -> m (a ∧ b') forall (m :: * -> *) a a' b b'. Monad m => (a -> m a') -> (b -> m b') -> (a ∧ b) -> m (a' ∧ b') mapMPair a -> m a forall a. a -> m a forall (m :: * -> *) a. Return m => a -> m a return