From 2bba3c5e454e87bb19ce1a19c040232196e9d310 Mon Sep 17 00:00:00 2001 From: Lukas Rohde Date: Sat, 14 Mar 2026 23:03:37 +0100 Subject: [PATCH 1/8] Refactor base library structure and port additional Haskell functions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This commit reorganizes large parts of the Agda2Hs base library to separate primitive type class definitions from higher-level utility functions and to align the module structure more closely with the corresponding hierarchy in Haskell. Key changes include: • Utility functions previously defined in Prim modules (e.g. Prim.String, Prim.Functor, Prim.Foldable, Prim.Monad, Prim.List) were moved to new modules in the Data and Control namespaces. • Introduced new modules mirroring the Haskell ecosystem, including: - Data.String - Data.Functor - Data.Foldable - Data.Traversable - Data.List - Control.Applicative - Control.Monad • Refactored several primitive modules so they now primarily contain class definitions and minimal core functionality. • Reworked the IO instances for Functor, Applicative, and Monad to define them explicitly in terms of bindIO and returnIO. • Added missing type classes and instances: - Alternative - MonadFail - MonadPlus • Expanded several modules with additional functions ported from Haskell’s base library. • Updated imports and reexports throughout the codebase to reflect the new module structure. Due to the tight dependencies between these changes, they are grouped into a single commit. This change is intended to make the library structure more consistent with Haskell and simplify future additions of standard functions. --- lib/base/Haskell/Control/Applicative.agda | 29 ++ lib/base/Haskell/Control/Monad.agda | 138 +++++++- lib/base/Haskell/Data/Foldable.agda | 85 +++++ lib/base/Haskell/Data/Functor.agda | 25 ++ lib/base/Haskell/Data/List.agda | 382 +++++++++++++++++----- lib/base/Haskell/Data/String.agda | 40 +++ lib/base/Haskell/Data/Traversable.agda | 101 ++++++ lib/base/Haskell/Extra/Refinement.agda | 6 +- lib/base/Haskell/Law/List.agda | 4 +- lib/base/Haskell/Prelude.agda | 152 ++++----- lib/base/Haskell/Prim.agda | 12 +- lib/base/Haskell/Prim/Absurd.agda | 4 +- lib/base/Haskell/Prim/Alternative.agda | 39 +++ lib/base/Haskell/Prim/Applicative.agda | 73 +++-- lib/base/Haskell/Prim/Foldable.agda | 127 ++++--- lib/base/Haskell/Prim/Functor.agda | 41 +-- lib/base/Haskell/Prim/IO.agda | 7 + lib/base/Haskell/Prim/List.agda | 116 +------ lib/base/Haskell/Prim/Monad.agda | 58 +--- lib/base/Haskell/Prim/MonadFail.agda | 29 ++ lib/base/Haskell/Prim/MonadPlus.agda | 58 ++++ lib/base/Haskell/Prim/Monoid.agda | 31 +- lib/base/Haskell/Prim/String.agda | 37 +-- lib/base/Haskell/Prim/Traversable.agda | 14 +- 24 files changed, 1128 insertions(+), 480 deletions(-) create mode 100644 lib/base/Haskell/Control/Applicative.agda create mode 100644 lib/base/Haskell/Data/Foldable.agda create mode 100644 lib/base/Haskell/Data/Functor.agda create mode 100644 lib/base/Haskell/Data/String.agda create mode 100644 lib/base/Haskell/Data/Traversable.agda create mode 100644 lib/base/Haskell/Prim/Alternative.agda create mode 100644 lib/base/Haskell/Prim/MonadFail.agda create mode 100644 lib/base/Haskell/Prim/MonadPlus.agda diff --git a/lib/base/Haskell/Control/Applicative.agda b/lib/base/Haskell/Control/Applicative.agda new file mode 100644 index 00000000..0126c992 --- /dev/null +++ b/lib/base/Haskell/Control/Applicative.agda @@ -0,0 +1,29 @@ +module Haskell.Control.Applicative where + +open import Haskell.Prim +open import Haskell.Prim.Maybe + +open import Haskell.Prim.Applicative public +open import Haskell.Prim.Alternative public +open import Haskell.Data.Functor public using (_<$>_) +open import Haskell.Data.Foldable public using (asum) + + +infixl 4 _<**>_ +_<**>_ : ⦃ Applicative f ⦄ → f a → f (a → b) → f b +_<**>_ = liftA2 (λ a f → f a) + +liftA : ⦃ Applicative f ⦄ → (a → b) → f a → f b +liftA f a = pure f <*> a + +liftA3 : ⦃ Applicative f ⦄ → (a → b → c → d) → f a → f b → f c → f d +liftA3 f a b c = liftA2 f a b <*> c + +optional : ⦃ Alternative f ⦄ → f a → f (Maybe a) +optional v = Just <$> v <|> pure Nothing + +-- Omitted for now: +-- - 'newtype Const a (b :: k) = Const { getConst :: a }' +-- - 'newtype WrappedMonad (m :: Type -> Type) a = WrapMonad { unwrapMonad :: m a }' +-- - 'newtype WrappedArrow (a :: Type -> Type -> Type) b c = WrapArrow { unwrapArrow :: a b c }' +-- - 'newtype ZipList a = ZipList { getZipList :: [a] }' \ No newline at end of file diff --git a/lib/base/Haskell/Control/Monad.agda b/lib/base/Haskell/Control/Monad.agda index f42f3813..05189234 100644 --- a/lib/base/Haskell/Control/Monad.agda +++ b/lib/base/Haskell/Control/Monad.agda @@ -2,10 +2,138 @@ module Haskell.Control.Monad where open import Haskell.Prim open import Haskell.Prim.Bool -open import Haskell.Prim.Monad -open import Haskell.Prim.String +open import Haskell.Prim.Int +open import Haskell.Prim.Tuple +open import Haskell.Prim.Applicative +open import Haskell.Prim.Alternative +open import Haskell.Prim.Traversable +open import Haskell.Prim.Foldable +open import Haskell.Data.Foldable using (sequenceA₋; foldlM) +open import Haskell.Data.List using (unzip; zipWith) open import Haskell.Extra.Erase -guard : {{ MonadFail m }} → (b : Bool) → m (Erase (b ≡ True)) -guard True = return (Erased refl) -guard False = fail "Guard was not True" +open import Haskell.Prim.Functor public +open import Haskell.Prim.Monad public +open import Haskell.Prim.MonadFail public +open import Haskell.Prim.MonadPlus public +open import Haskell.Prim.Traversable public using (mapM; sequence) +open import Haskell.Data.Traversable public using (forM) +open import Haskell.Data.Foldable public using (mapM₋; forM₋; sequence₋; msum) +open import Haskell.Data.Functor public using (void) + + +variable a1 a2 a3 a4 a5 r : Type + +infixr 1 _=<<_ _>=>_ _<=<_ +_=<<_ : ⦃ Monad m ⦄ → (a → m b) → m a → m b +_=<<_ = flip _>>=_ + +_>=>_ : ⦃ Monad m ⦄ → (a → m b) → (b → m c) → a → m c +f >=> g = λ x → f x >>= g + +_<=<_ : ⦃ Monad m ⦄ → (b → m c) → (a → m b) → a → m c +_<=<_ = flip _>=>_ + + +join : ⦃ Monad m ⦄ → m (m a) → m a +join x = x >>= id + +mfilter : ⦃ MonadPlus m ⦄ → (a → Bool) → m a → m a +mfilter p ma = do + a ← ma + if p a then return a else mzero + +filterM : ⦃ Applicative m ⦄ → (a → m Bool) → (List a) → m (List a) +filterM p = foldr (λ x → liftA2 (λ b → if b then (x ∷_) else id) (p x)) (pure []) + +mapAndUnzipM : ⦃ Applicative m ⦄ → (a → m (b × c)) → (List a) → m (List b × List c) +mapAndUnzipM f xs = fmap unzip (traverse f xs) + +zipWithM : ⦃ Applicative m ⦄ → (a → b → m c) → (List a) → (List b) → m (List c) +zipWithM f xs ys = sequenceA (zipWith f xs ys) + +zipWithM₋ : ⦃ Applicative m ⦄ → (a → b → m c) → (List a) → (List b) → m ⊤ +zipWithM₋ f xs ys = sequenceA₋ (zipWith f xs ys) + +foldM : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (b → a → m b) → b → t a → m b +foldM = foldlM + +foldM₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (b → a → m b) → b → t a → m ⊤ +foldM₋ f a xs = foldlM f a xs >> return tt + +replicateMNat : ⦃ Applicative m ⦄ → Nat → m a → m (List a) +replicateMNat zero _ = pure [] +replicateMNat (suc n) f = liftA2 _∷_ f (replicateMNat n f) + +replicateM : ⦃ Applicative m ⦄ → (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → m a → m (List a) +replicateM cnt f = replicateMNat (intToNat cnt) f + +replicateMNat₋ : ⦃ Applicative m ⦄ → Nat → m a → m ⊤ +replicateMNat₋ zero _ = pure tt +replicateMNat₋ (suc n) f = f *> replicateMNat₋ n f + +replicateM₋ : ⦃ Applicative m ⦄ → (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → m a → m ⊤ +replicateM₋ cnt f = replicateMNat₋ (intToNat cnt) f + + +guard : ⦃ Alternative f ⦄ → (b : Bool) → f (Erase (b ≡ True)) +guard True = pure (Erased refl) +guard False = empty + +when : ⦃ Applicative f ⦄ → (b : Bool) → ({@0 p : b ≡ True} → f ⊤) → f ⊤ +when True f = f {refl} +when False _ = pure tt + +unless : ⦃ Applicative f ⦄ → (b : Bool) → ({@0 p : b ≡ False} → f ⊤) → f ⊤ +unless True _ = pure tt +unless False f = f {refl} + + +liftM : ⦃ Monad m ⦄ → (a1 → r) → m a1 → m r +liftM f m1 = do + x1 ← m1 + return (f x1) + +liftM2 : ⦃ Monad m ⦄ → (a1 → a2 → r) → m a1 → m a2 → m r +liftM2 f m1 m2 = do + x1 ← m1 + x2 ← m2 + return (f x1 x2) + +liftM3 : ⦃ Monad m ⦄ → (a1 → a2 → a3 → r) → m a1 → m a2 → m a3 → m r +liftM3 f m1 m2 m3 = do + x1 ← m1 + x2 ← m2 + x3 ← m3 + return (f x1 x2 x3) + +liftM4 : ⦃ Monad m ⦄ → (a1 -> a2 -> a3 -> a4 -> r) → m a1 → m a2 → m a3 → m a4 → m r +liftM4 f m1 m2 m3 m4 = do + x1 ← m1 + x2 ← m2 + x3 ← m3 + x4 ← m4 + return (f x1 x2 x3 x4) + +liftM5 : ⦃ Monad m ⦄ → (a1 → a2 → a3 → a4 → a5 → r) → m a1 → m a2 → m a3 → m a4 → m a5 → m r +liftM5 f m1 m2 m3 m4 m5 = do + x1 ← m1 + x2 ← m2 + x3 ← m3 + x4 ← m4 + x5 ← m5 + return (f x1 x2 x3 x4 x5) + +ap : ⦃ Monad m ⦄ → m (a → b) → m a → m b +ap m1 m2 = do + f ← m1 + x ← m2 + return (f x) + +infixl 4 _<$!>_ +_<$!>_ : ⦃ Monad m ⦄ → (a → b) → m a → m b +_<$!>_ = fmap + + +-- Omitted for now: +-- - 'forever :: Applicative => f -> f a -> f b' diff --git a/lib/base/Haskell/Data/Foldable.agda b/lib/base/Haskell/Data/Foldable.agda new file mode 100644 index 00000000..47bb5d28 --- /dev/null +++ b/lib/base/Haskell/Data/Foldable.agda @@ -0,0 +1,85 @@ +module Haskell.Data.Foldable where + +open import Haskell.Prim +open import Haskell.Prim.Monad +open import Haskell.Prim.Applicative +open import Haskell.Prim.Alternative +open import Haskell.Prim.MonadPlus +open import Haskell.Prim.Monoid +open import Haskell.Prim.Eq +open import Haskell.Prim.Ord +open import Haskell.Prim.Bool +open import Haskell.Prim.Maybe + +open import Haskell.Prim.Foldable public + + +foldrM : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (a → b → m b) → b → t a → m b +foldrM f z0 xs = foldl (λ k x z → f x z >>= k) return xs z0 + +foldlM : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (b → a → m b) → b → t a → m b +foldlM f z0 xs = foldr (λ x k z → f z x >>= k) return xs z0 + +traverse₋ : ⦃ Foldable t ⦄ → ⦃ Applicative f ⦄ → (a → f b) → t a → f ⊤ +traverse₋ f = foldr (λ x m → f x *> m) (pure tt) + +for₋ : ⦃ Foldable t ⦄ → ⦃ Applicative f ⦄ → t a → (a → f b) → f ⊤ +for₋ = flip traverse₋ + +mapM₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (a → m b) → t a → m ⊤ +mapM₋ f = foldr (λ x m → f x >> m) (pure tt) + +forM₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → t a → (a → m b) → m ⊤ +forM₋ = flip mapM₋ + +sequenceA₋ : ⦃ Foldable t ⦄ → ⦃ Applicative f ⦄ → t (f a) → f ⊤ +sequenceA₋ = foldr (λ mx my → mx *> my) (pure tt) + +sequence₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → t (m a) → m ⊤ +sequence₋ = foldr (λ mx my → mx >> my) (pure tt) + +asum : ⦃ Foldable t ⦄ → ⦃ Alternative f ⦄ → t (f a) → f a +asum = foldr _<|>_ empty + +msum : ⦃ Foldable t ⦄ → ⦃ MonadPlus m ⦄ → t (m a) → m a +msum = asum + +concat : ⦃ Foldable t ⦄ → t (List a) → List a +concat = fold + +concatMap : ⦃ Foldable t ⦄ → (a → List b) → t a → List b +concatMap = foldMap + +any : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool +any ⦃ i ⦄ = foldMap ⦃ i ⦄ ⦃ MonoidDisj ⦄ + +all : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool +all ⦃ i ⦄ = foldMap ⦃ i ⦄ ⦃ MonoidConj ⦄ + +and : ⦃ Foldable t ⦄ → t Bool → Bool +and = all id + +or : ⦃ Foldable t ⦄ → t Bool → Bool +or = any id + +maximumBy : ⦃ _ : Foldable t ⦄ → (a → a → Ordering) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a +maximumBy {a = a} cmp = foldr1 max' + where + max' : a → a → a + max' x y with cmp x y + ... | GT = x + ... | _ = y + +minimumBy : ⦃ _ : Foldable t ⦄ → (a → a → Ordering) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a +minimumBy {a = a} cmp = foldr1 min' + where + min' : a → a → a + min' x y with cmp x y + ... | GT = y + ... | _ = x + +notElem : ⦃ Foldable t ⦄ → ⦃ Eq a ⦄ → a → t a → Bool +notElem x t = not (elem x t) + +find : ⦃ Foldable t ⦄ → (a → Bool) → t a → Maybe a +find ⦃ i ⦄ p = foldMap ⦃ i ⦄ ⦃ MonoidFirst ⦄ (λ x → if p x then Just x else Nothing) \ No newline at end of file diff --git a/lib/base/Haskell/Data/Functor.agda b/lib/base/Haskell/Data/Functor.agda new file mode 100644 index 00000000..ab48834d --- /dev/null +++ b/lib/base/Haskell/Data/Functor.agda @@ -0,0 +1,25 @@ +module Haskell.Data.Functor where + +open import Haskell.Prim +open import Haskell.Prim.Tuple + +open import Haskell.Prim.Functor public + + +infixl 4 _$>_ +_$>_ : ⦃ Functor f ⦄ → f a → (@0 ⦃ a ⦄ → b) → f b +_$>_ = flip _<$_ + +infixl 4 _<$>_ +_<$>_ : ⦃ Functor f ⦄ → (a → b) → f a → f b +_<$>_ = fmap + +infixl 1 _<&>_ +_<&>_ : ⦃ Functor f ⦄ → f a → (a → b) → f b +m <&> f = fmap f m + +unzip : ⦃ Functor f ⦄ → f (a × b) -> (f a × f b) +unzip xs = fst <$> xs , snd <$> xs + +void : ⦃ Functor f ⦄ → f a → f ⊤ +void = tt <$_ diff --git a/lib/base/Haskell/Data/List.agda b/lib/base/Haskell/Data/List.agda index 00cbff80..a620c739 100644 --- a/lib/base/Haskell/Data/List.agda +++ b/lib/base/Haskell/Data/List.agda @@ -1,90 +1,310 @@ module Haskell.Data.List where -open import Haskell.Prelude +open import Haskell.Prim +open import Haskell.Prim.Bool +open import Haskell.Prim.Tuple +open import Haskell.Prim.Int +open import Haskell.Prim.Maybe +open import Haskell.Prim.Ord +open import Haskell.Prim.Num +open import Haskell.Prim.Eq -open import Haskell.Data.Ord using (comparing) +open import Haskell.Prim.List public +open import Haskell.Prim.Foldable public using (Foldable) +open Foldable ⦃ ... ⦄ public + using (null; length; foldl; foldl'; foldl1; foldr; foldr1; sum; product; maximum; minimum; elem) +open import Haskell.Data.Foldable public + using (concat; concatMap; and; or; any; all; maximumBy; minimumBy; notElem; find) +open import Haskell.Data.Traversable public using (mapAccumL; mapAccumR) +open import Haskell.Data.String public using (lines; words; unlines; unwords) -open import Haskell.Law.Eq -open import Haskell.Law.Equality -{----------------------------------------------------------------------------- - Operations -------------------------------------------------------------------------------} +variable i : Type + +uncons : List a → Maybe (a × List a) +uncons [] = Nothing +uncons (x ∷ xs) = Just (x , xs) + +unsnoc : List a → Maybe (List a × a) +unsnoc = foldr (λ x → Just ∘ maybe ([] , x) (λ (a , b) → x ∷ a , b)) Nothing + +singleton : a → List a +singleton = _∷ [] + +compareLength : List a → Int → Ordering +compareLength xs n = + if n < 0 then GT + else foldr (λ _ f m → if m > 0 then f (m - 1) else GT) (λ m → if m > 0 then LT else EQ) xs n + +foldl1' : (a → a → a) → (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a +foldl1' f (x ∷ xs) = foldl f x xs + +scanl : (b → a → b) → b → List a → List b +scanl f z [] = z ∷ [] +scanl f z (x ∷ xs) = z ∷ scanl f (f z x) xs + +scanl' : (b → a → b) → b → List a → List b +scanl' = scanl + +scanl1 : (a → a → a) → List a → List a +scanl1 f [] = [] +scanl1 f (x ∷ xs) = scanl f x xs + +scanr : (a → b → b) → b → List a → List b +scanr f z [] = z ∷ [] +scanr f z (x ∷ xs) = case scanr f z xs of λ where + [] → [] -- impossible + qs@(q ∷ _) → f x q ∷ qs + +scanr1 : (a → a → a) → List a → List a +scanr1 f [] = [] +scanr1 f (x ∷ xs) = case scanr1 f xs of λ where + [] → x ∷ [] + qs@(q ∷ _) → f x q ∷ qs + +replicateNat : Nat → a → List a +replicateNat zero _ = [] +replicateNat (suc n) x = x ∷ replicateNat n x + +replicate : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → a → List a +replicate n = replicateNat (intToNat n) + +takeNat : Nat → List a → List a +takeNat n [] = [] +takeNat zero xs = [] +takeNat (suc n) (x ∷ xs) = x ∷ takeNat n xs + +take : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a +take n xs = takeNat (intToNat n) xs + +dropNat : Nat → List a → List a +dropNat n [] = [] +dropNat zero xs = xs +dropNat (suc n) (_ ∷ xs) = dropNat n xs + +drop : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a +drop n xs = dropNat (intToNat n) xs + +splitAtNat : (n : Nat) → List a → List a × List a +splitAtNat _ [] = [] , [] +splitAtNat 0 xs = [] , xs +splitAtNat (suc n) (x ∷ xs) = first (x ∷_) (splitAtNat n xs) + +splitAt : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a × List a +splitAt n xs = splitAtNat (intToNat n) xs + +takeWhile : (a → Bool) → List a → List a +takeWhile p [] = [] +takeWhile p (x ∷ xs) = if p x then x ∷ takeWhile p xs else [] + +dropWhile : (a → Bool) → List a → List a +dropWhile p [] = [] +dropWhile p (x ∷ xs) = if p x then dropWhile p xs else x ∷ xs + +dropWhileEnd : (a → Bool) → List a → List a +dropWhileEnd p = foldr (λ x xs → if p x && null xs then [] else x ∷ xs) [] + +span : (a → Bool) → List a → List a × List a +span p [] = [] , [] +span p (x ∷ xs) = if p x then first (x ∷_) (span p xs) + else ([] , x ∷ xs) + +break : (a → Bool) → List a → List a × List a +break p = span (not ∘ p) + +stripPrefix : ⦃ Eq a ⦄ → List a → List a → Maybe (List a) +stripPrefix [] ys = Just ys +stripPrefix _ [] = Nothing +stripPrefix (x ∷ xs) (y ∷ ys) = if x == y then stripPrefix xs ys else Nothing + +reverse : List a → List a +reverse = foldl (flip _∷_) [] + +inits : List a → List (List a) +inits = map reverse ∘ scanl (flip _∷_) [] + +tails : List a → List (List a) +tails [] = singleton [] +tails xs@(_ ∷ xs') = xs ∷ tails xs' + +isPrefixOf : ⦃ Eq a ⦄ → List a → List a → Bool +isPrefixOf [] _ = True +isPrefixOf _ [] = False +isPrefixOf (x ∷ xs) (y ∷ ys) = x == y && isPrefixOf xs ys + +isSuffixOf : ⦃ Eq a ⦄ → List a → List a → Bool +isSuffixOf xs ys = isPrefixOf (reverse xs) (reverse ys) + +isInfixOf : ⦃ Eq a ⦄ → List a → List a → Bool +isInfixOf xs ys = any (isPrefixOf xs) (tails ys) + +isSubsequenceOf : ⦃ Eq a ⦄ → List a → List a → Bool +isSubsequenceOf [] _ = True +isSubsequenceOf _ [] = False +isSubsequenceOf xs@(x ∷ xs') (y ∷ ys) = if x == y then isSubsequenceOf xs' ys + else isSubsequenceOf xs ys + +lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b +lookup _ [] = Nothing +lookup k ((x , y) ∷ xys) = if k == x then Just y else lookup k xys + +filter : (a → Bool) → List a → List a +filter p [] = [] +filter p (x ∷ xs) = if p x then x ∷ filter p xs else filter p xs partition : (a → Bool) → List a → (List a × List a) partition p xs = (filter p xs , filter (not ∘ p) xs) --- | Delete all occurrences of an item. --- Not part of 'Data.List'. -deleteAll : ⦃ _ : Eq a ⦄ → @0 ⦃ IsLawfulEq a ⦄ → a → List a → List a -deleteAll x = filter (not ∘ (x ==_)) - --- | These semantics of 'nub' assume that the 'Eq' instance --- is lawful. --- These semantics are inefficient, but good for proofs. -nub : ⦃ _ : Eq a ⦄ → @0 ⦃ IsLawfulEq a ⦄ → List a → List a -nub [] = [] -nub (x ∷ xs) = x ∷ deleteAll x (nub xs) - -postulate - sortBy : (a → a → Ordering) → List a → List a - -sort : ⦃ Ord a ⦄ → List a → List a -sort = sortBy compare - -sortOn : ⦃ Ord b ⦄ → (a → b) → List a → List a -sortOn f = - map snd - ∘ sortBy (comparing fst) - ∘ map (λ x → let y = f x in seq y (y , x)) - -{----------------------------------------------------------------------------- - Properties -------------------------------------------------------------------------------} - --- | A deleted item is no longer an element. --- -prop-elem-deleteAll - : ∀ ⦃ _ : Eq a ⦄ ⦃ _ : IsLawfulEq a ⦄ - (x y : a) (zs : List a) - → elem x (deleteAll y zs) - ≡ (if x == y then False else elem x zs) --- -prop-elem-deleteAll x y [] - with x == y -... | False = refl -... | True = refl -prop-elem-deleteAll x y (z ∷ zs) - with recurse ← prop-elem-deleteAll x y zs - with y == z in eqyz -... | True - with x == z in eqxz -... | True - rewrite equality' _ _ (trans (equality x z eqxz) (sym (equality y z eqyz))) - = recurse -... | False - = recurse -prop-elem-deleteAll x y (z ∷ zs) - | False - with x == z in eqxz -... | True - rewrite equality x z eqxz | eqSymmetry y z | eqyz - = refl -... | False - = recurse - --- | An item is an element of the 'nub' iff it is --- an element of the original list. --- -prop-elem-nub - : ∀ ⦃ _ : Eq a ⦄ ⦃ _ : IsLawfulEq a ⦄ - (x : a) (ys : List a) - → elem x (nub ys) - ≡ elem x ys --- -prop-elem-nub x [] = refl -prop-elem-nub x (y ∷ ys) - rewrite prop-elem-deleteAll x y (nub ys) - with x == y -... | True = refl -... | False = prop-elem-nub x ys +infixl 9 _!?_ +_!?_ : List a → Int → Maybe a +[] !? _ = Nothing +(x ∷ xs) !? n = case compare n 0 of λ where + LT → Nothing + EQ → Just x + GT → xs !? (n - 1) + +infixl 9 _!!ᴺ_ +_!!ᴺ_ : (xs : List a) (n : Nat) → @0 ⦃ IsTrue (n < lengthNat xs) ⦄ → a +(x ∷ xs) !!ᴺ zero = x +(x ∷ xs) !!ᴺ suc n = xs !!ᴺ n + +infixl 9 _!!_ +_!!_ : (xs : List a) (n : Int) + → ⦃ @0 _ : IsNonNegativeInt n ⦄ + → ⦃ @0 _ : IsTrue (intToNat n < lengthNat xs) ⦄ → a +xs !! n = xs !!ᴺ intToNat n + +findIndices : (a → Bool) → List a → List Int +findIndices p xs = let go x r k = if p x then k ∷ r (k + 1) else r (k + 1) + in foldr go (const []) xs 0 + +findIndex : (a → Bool) → List a → Maybe Int +findIndex p xs = case findIndices p xs of λ where + [] → Nothing + (x ∷ _) → Just x + +elemIndices : ⦃ Eq a ⦄ → a → List a → List Int +elemIndices x = findIndices (x ==_) + +elemIndex : ⦃ Eq a ⦄ → a → List a → Maybe Int +elemIndex x = findIndex (x ==_) + +zipWith : (a → b → c) → List a → List b → List c +zipWith f [] _ = [] +zipWith f _ [] = [] +zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys + +zipWith3 : (a → b → c → d) → List a → List b → List c → List d +zipWith3 f [] _ _ = [] +zipWith3 f _ [] _ = [] +zipWith3 f _ _ [] = [] +zipWith3 f (x ∷ xs) (y ∷ ys) (z ∷ zs) = f x y z ∷ zipWith3 f xs ys zs + +zip : List a → List b → List (a × b) +zip = zipWith _,_ + +zip3 : List a → List b → List c → List (a × b × c) +zip3 = zipWith3 _,_,_ + +unzip : List (a × b) → List a × List b +unzip [] = [] , [] +unzip ((x , y) ∷ xys) = (x ∷_) *** (y ∷_) $ unzip xys + +unzip3 : List (a × b × c) → List a × List b × List c +unzip3 [] = [] , [] , [] +unzip3 ((x , y , z) ∷ xyzs) = case unzip3 xyzs of λ where + (xs , ys , zs) → x ∷ xs , y ∷ ys , z ∷ zs + +intersperse : a → List a → List a +intersperse _ [] = [] +intersperse sep (x ∷ xs) = x ∷ prependToAll sep xs + where + prependToAll : a → List a → List a + prependToAll _ [] = [] + prependToAll sep (x ∷ xs) = sep ∷ x ∷ prependToAll sep xs + +intercalate : List a → List (List a) → List a +intercalate xs xss = concat (intersperse xs xss) + +subsequences : List a → List (List a) +subsequences xs = [] ∷ nonEmptySubsequences xs + where + nonEmptySubsequences : List a → List (List a) + nonEmptySubsequences [] = [] + nonEmptySubsequences (x ∷ xs) = let f ys r = ys ∷ (x ∷ ys) ∷ r + in singleton x ∷ foldr f [] (nonEmptySubsequences xs) + +nubBy : (a → a → Bool) → List a → List a +nubBy eq [] = [] +nubBy eq (x ∷ xs) = x ∷ filter (not ∘ eq x) (nubBy eq xs) + +nub : ⦃ Eq a ⦄ → List a → List a +nub = nubBy _==_ + +deleteBy : (a → a → Bool) → a → List a → List a +deleteBy _ _ [] = [] +deleteBy eq x (x' ∷ xs) = if eq x x' then xs else x' ∷ deleteBy eq x xs + +delete : ⦃ Eq a ⦄ → a → List a → List a +delete = deleteBy _==_ + +deleteFirstsBy : (a → a → Bool) → List a → List a → List a +deleteFirstsBy eq = foldl (flip (deleteBy eq)) + +infix 5 _\\_ +_\\_ : ⦃ Eq a ⦄ → List a → List a → List a +_\\_ = deleteFirstsBy _==_ + +unionBy : (a → a → Bool) → List a → List a → List a +unionBy eq xs ys = xs ++ deleteFirstsBy eq (nubBy eq ys) xs + +union : ⦃ Eq a ⦄ → List a → List a → List a +union = unionBy _==_ + +intersectBy : (a → a → Bool) → List a → List a → List a +intersectBy eq xs ys = filter (λ x → any (eq x) ys) xs + +intersect : ⦃ Eq a ⦄ → List a → List a → List a +intersect = intersectBy _==_ + +insertBy : (a → a → Ordering) → a → List a → List a +insertBy _ x [] = singleton x +insertBy cmp x ys@(y ∷ ys') = case cmp x y of λ where + GT → y ∷ insertBy cmp x ys' + _ → x ∷ ys + +insert : ⦃ Ord a ⦄ → a → List a → List a +insert = insertBy compare + + +-- Omitted for now: +-- [obviously non-terminating] +-- - 'iterate :: (a -> a) -> a -> [a]' +-- - 'iterate' :: (a -> a) -> a -> [a]' +-- - 'repeat :: a -> [a]' +-- - 'cycle :: [a] -> [a]' +-- - 'unfoldr :: (b -> Maybe (a, b)) -> b -> [a] + +-- [hard to prove termination] +-- - 'groupBy :: (a -> a -> Bool) -> [a] -> [[a]]' +-- - 'group :: Eq a => [a] -> [[a]]' +-- - 'transpose :: [[a]] -> [[a]]' +-- - 'permutations :: [a] -> [[a]]' +-- - 'sortBy :: (a -> a -> Ordering) -> [a] -> [a]' +-- - 'sort :: Ord a => [a] -> [a]' +-- - 'sortOn :: Ord b => (a -> b) -> [a] -> [a] + +-- [type signature includes currently not supported (?) `NonEmpty` type] +-- - 'inits1 :: [a] -> [NonEmpty a]' +-- - 'tails1 :: [a] -> [NonEmpty a]' + +-- - 'zipWith4', 'zipWith5', 'zipWith6', 'zipWith7' +-- - 'zip4', 'zip5', 'zip6', 'zip7' +-- - 'unzip4', 'unzip5', 'unzip6', 'unzip7' + +-- - 'genericLength :: Num i => [a] -> i' +-- - 'genericTake :: Integral i => i -> [a] -> [a]' +-- - 'genericDrop :: Integral i => i -> [a] -> [a]' +-- - 'genericSplitAt :: Integral i => i -> [a] -> ([a], [a])' +-- - 'genericIndex :: Integral i => [a] -> i -> a' +-- - 'genericReplicate :: Integral i => i -> a -> [a]' diff --git a/lib/base/Haskell/Data/String.agda b/lib/base/Haskell/Data/String.agda new file mode 100644 index 00000000..450bb45d --- /dev/null +++ b/lib/base/Haskell/Data/String.agda @@ -0,0 +1,40 @@ +module Haskell.Data.String where + +open import Haskell.Prim +open import Haskell.Prim.List +open import Haskell.Prim.Foldable +open import Haskell.Data.Foldable + +open import Haskell.Prim.String public + + +private + cons : Char → List String → List String + cons c [] = (c ∷ []) ∷ [] + cons c (s ∷ ss) = (c ∷ s) ∷ ss + + mutual + space : String → List String + space [] = [] + space (c ∷ s) = if primIsSpace c then space s else cons c (word s) + + word : String → List String + word [] = [] + word (c ∷ s) = if primIsSpace c then [] ∷ space s else cons c (word s) + +lines : String → List String +lines [] = [] +lines ('\n' ∷ s) = [] ∷ lines s +lines (c ∷ s) = cons c (lines s) + +words : String → List String +words [] = [] +words s@(c ∷ s₁) = if primIsSpace c then space s₁ else word s + +unlines : List String → String +unlines = concatMap (_++ "\n") + +unwords : List String → String +unwords [] = "" +unwords (w ∷ []) = w +unwords (w ∷ ws) = w ++ ' ' ∷ unwords ws \ No newline at end of file diff --git a/lib/base/Haskell/Data/Traversable.agda b/lib/base/Haskell/Data/Traversable.agda new file mode 100644 index 00000000..1330eef7 --- /dev/null +++ b/lib/base/Haskell/Data/Traversable.agda @@ -0,0 +1,101 @@ +module Haskell.Data.Traversable where + +open import Haskell.Prim hiding (s) +open import Haskell.Prim.Functor +open import Haskell.Prim.Applicative +open import Haskell.Prim.Monad +open import Haskell.Prim.Tuple + +open import Haskell.Prim.Traversable public + + +variable s : Type + +for : ⦃ Traversable t ⦄ → ⦃ Applicative f ⦄ → t a → (a → f b) → f (t b) +for = flip traverse + +forM : ⦃ Traversable t ⦄ → ⦃ Monad m ⦄ → t a → (a → m b) → m (t b) +forM = flip mapM + +private + record State (s a : Type) : Type where + constructor mkState + pattern + field run : s → s × a + + record StateT (s : Type) (m : Type → Type) (a : Type) : Type where + constructor mkStateT + pattern + field run : s → m (s × a) + + instance + open DefaultFunctor + open ApplicativeFrom<*> + + iDefaultFunctorState : DefaultFunctor (State s) + iDefaultFunctorState .fmap f (mkState k) = mkState $ λ s → let s' , v = k s in s' , f v + + iFunctorState : Functor (State s) + iFunctorState = record { DefaultFunctor iDefaultFunctorState } + + iDefaultApplicativeStateL : ApplicativeFrom<*> (State s) + iDefaultApplicativeStateL .pure x = mkState (λ s → s , x) + iDefaultApplicativeStateL ._<*>_ (mkState kf) (mkState kx) = mkState $ λ s → + let s' , f = kf s + s'' , x = kx s' + in s'' , f x + + iApplicativeStateL : Applicative (State s) + iApplicativeStateL = record { ApplicativeFrom<*> iDefaultApplicativeStateL } + + iDefaultApplicativeStateR : ApplicativeFrom<*> (State s) + iDefaultApplicativeStateR .pure x = mkState (λ s → s , x) + iDefaultApplicativeStateR ._<*>_ (mkState kf) (mkState kx) = mkState $ λ s → + let s' , x = kx s + s'' , f = kf s' + in s'' , f x + + iApplicativeStateR : Applicative (State s) + iApplicativeStateR = record { ApplicativeFrom<*> iDefaultApplicativeStateR } + + iDefaultFunctorStateT : ⦃ Monad m ⦄ → DefaultFunctor (StateT s m) + iDefaultFunctorStateT .fmap f (mkStateT kx) = mkStateT $ λ s → do + s' , x ← kx s + return (s' , f x) + + iFunctorStateT : ⦃ Monad m ⦄ → Functor (StateT s m) + iFunctorStateT = record { DefaultFunctor iDefaultFunctorStateT } + + iDefaultApplicativeStateT : ⦃ Monad m ⦄ → ApplicativeFrom<*> (StateT s m) + iDefaultApplicativeStateT .pure x = mkStateT (λ s → return (s , x)) + iDefaultApplicativeStateT ._<*>_ (mkStateT kf) (mkStateT kx) = mkStateT $ λ s → do + s' , f ← kf s + s'' , x ← kx s' + return (s'' , f x) + + iApplicativeStateT : ⦃ Monad m ⦄ → Applicative (StateT s m) + iApplicativeStateT = record { ApplicativeFrom<*> iDefaultApplicativeStateT} + + iDefaultMonadStateT : ⦃ Monad m ⦄ → DefaultMonad (StateT s m) + iDefaultMonadStateT .DefaultMonad._>>=_ m k = mkStateT $ λ s → do + s' , x ← StateT.run m s + StateT.run (k x) s' + + iMonadStateT : ⦃ Monad m ⦄ → Monad (StateT s m) + iMonadStateT = record { DefaultMonad iDefaultMonadStateT } + +mapAccumL : ⦃ Traversable t ⦄ → (s → a → s × b) → s → t a → s × t b +mapAccumL ⦃ iTraversable ⦄ f s t = State.run (traverse ⦃ iTraversable ⦄ ⦃ iApplicativeStateL ⦄ (mkState ∘ flip f) t) s + +mapAccumR : ⦃ Traversable t ⦄ → (s → a → s × b) → s → t a → s × t b +mapAccumR ⦃ iTraversable ⦄ f s t = State.run (traverse ⦃ iTraversable ⦄ ⦃ iApplicativeStateR ⦄ (mkState ∘ flip f) t) s + +mapAccumM : ⦃ Monad m ⦄ → ⦃ Traversable t ⦄ → (s → a → m (s × b)) → s → t a → m (s × t b) +mapAccumM f s t = StateT.run (mapM (mkStateT ∘ flip f) t) s + +forAccumM : ⦃ Monad m ⦄ → ⦃ Traversable t ⦄ → s → t a → (s → a → m (s × b)) → m (s × t b) +forAccumM s t f = mapAccumM f s t + +-- Omitted for now: +-- - 'fmapDefault :: Traversable t => (a -> b) -> t a -> t b' +-- - 'foldMapDefault :: (Traversable t, Monoid m) => (a -> m) -> t a -> m' \ No newline at end of file diff --git a/lib/base/Haskell/Extra/Refinement.agda b/lib/base/Haskell/Extra/Refinement.agda index d8621f6a..4d0a4b7a 100644 --- a/lib/base/Haskell/Extra/Refinement.agda +++ b/lib/base/Haskell/Extra/Refinement.agda @@ -1,10 +1,12 @@ module Haskell.Extra.Refinement where -open import Haskell.Prelude +open import Haskell.Prim +open import Haskell.Prim.Maybe open import Agda.Primitive + private variable - ℓ ℓ′ : Level + ℓ′ : Level record ∃ (a : Type ℓ) (@0 P : a → Type ℓ′) : Type (ℓ ⊔ ℓ′) where constructor _⟨⟩ diff --git a/lib/base/Haskell/Law/List.agda b/lib/base/Haskell/Law/List.agda index 377b91be..7a613cbc 100644 --- a/lib/base/Haskell/Law/List.agda +++ b/lib/base/Haskell/Law/List.agda @@ -2,9 +2,11 @@ module Haskell.Law.List where open import Haskell.Law.Equality open import Haskell.Prim renaming (addNat to _+ₙ_) -open import Haskell.Prim.Foldable open import Haskell.Prim.List open import Haskell.Prim.Applicative +open import Haskell.Prim.Foldable +open import Haskell.Data.Foldable + []≠∷ : ∀ x (xs : List a) → [] ≠ x ∷ xs []≠∷ x xs () diff --git a/lib/base/Haskell/Prelude.agda b/lib/base/Haskell/Prelude.agda index dbe4b34e..f02bc79c 100644 --- a/lib/base/Haskell/Prelude.agda +++ b/lib/base/Haskell/Prelude.agda @@ -1,49 +1,67 @@ {-# OPTIONS --no-auto-inline #-} + module Haskell.Prelude where -open import Haskell.Prim -open Haskell.Prim public using - ( Type; - Bool; True; False; Char; Integer; - List; []; _∷_; Nat; zero; suc; ⊤; tt; - TypeError; ⊥; iNumberNat; lengthNat; - IsTrue; IsFalse; NonEmpty; - All; allNil; allCons; - Any; anyHere; anyThere; - id; _∘_; _$_; flip; const; - if_then_else_; case_of_; - Number; fromNat; Negative; fromNeg; - IsString; fromString; - _≡_; refl; - a; b; c; d; e; f; m; s; t ) - -open import Haskell.Prim.Absurd public -open import Haskell.Prim.Applicative public -open import Haskell.Prim.Bool public -open import Haskell.Prim.Bounded public -open import Haskell.Prim.Char public -open import Haskell.Prim.Double public -open import Haskell.Prim.Either public -open import Haskell.Prim.Enum public -open import Haskell.Prim.Eq public -open import Haskell.Prim.Foldable public -open import Haskell.Prim.Functor public -open import Haskell.Prim.Int public -open import Haskell.Prim.Integer public -open import Haskell.Prim.IO public -open import Haskell.Prim.List public -open import Haskell.Prim.Maybe public -open import Haskell.Prim.Monad public -open import Haskell.Prim.Monoid public -open import Haskell.Prim.Num public -open import Haskell.Prim.Ord public -open import Haskell.Prim.Show public -open import Haskell.Prim.String public -open import Haskell.Prim.Traversable public -open import Haskell.Prim.Tuple public hiding (first; second; _***_) -open import Haskell.Prim.Word public - --- Problematic features +open import Haskell.Prim public + using (Type; + Bool; True; False; Char; Integer; + List; []; _∷_; Nat; zero; suc; ⊤; tt; + TypeError; ⊥; iNumberNat; + IsTrue; IsFalse; NonEmpty; + All; allNil; allCons; + Any; anyHere; anyThere; + id; _∘_; _$_; flip; const; + if_then_else_; case_of_; + Number; fromNat; Negative; fromNeg; + IsString; fromString; + _≡_; refl; + a; b; c; d; e; f; m; s; t) + +open import Haskell.Prim.Absurd public +open import Haskell.Prim.Bool public +open import Haskell.Prim.Bounded public +open import Haskell.Prim.Char public +open import Haskell.Prim.Double public +open import Haskell.Prim.Either public +open import Haskell.Prim.Enum public +open import Haskell.Prim.Eq public +open import Haskell.Prim.Int public +open import Haskell.Prim.Integer public +open import Haskell.Prim.IO public + hiding (returnIO; bindIO; failIO; mplusIO) +open import Haskell.Prim.Maybe public +open import Haskell.Prim.Monoid public +open import Haskell.Prim.MonadFail public +open import Haskell.Prim.Num public +open import Haskell.Prim.Ord public +open import Haskell.Prim.Show public +open import Haskell.Prim.Tuple public hiding (first; second; _***_) +open import Haskell.Prim.Word public +open import Haskell.Prim.String public +open import Haskell.Prim.Functor public +open import Haskell.Prim.Applicative public +open import Haskell.Prim.Monad public +open import Haskell.Prim.Traversable public +open import Haskell.Prim.Foldable public + hiding (fold; foldMap'; foldr'; toList; null; length) + +open import Haskell.Data.String public + using (lines; words; unlines; unwords) +open import Haskell.Data.List public + using (_++_; map; reverse; lengthNat; length; + head; last; tail; init; + _!!ᴺ_; _!!_; splitAt; lookup; null; + scanl; scanl1; scanr; scanr1; + replicateNat; replicate; + take; drop; takeWhile; dropWhile; + filter; span; break; + zip; zip3; zipWith; zipWith3; unzip; unzip3; + and; or; any; all; concat; concatMap; notElem) +open import Haskell.Data.Functor public using (_<$>_) +open import Haskell.Control.Monad public using (_=<<_; mapM₋; sequence₋) + + +-- Problematic features: -- - [Partial]: Could pass implicit/instance arguments to prove totality. -- - [Float]: Or Float (Agda floats are Doubles) -- - [Infinite]: Define colists and map to Haskell lists? @@ -51,6 +69,7 @@ open import Haskell.Prim.Word public -- Missing from the Haskell Prelude: -- -- Float [Float] +-- -- Rational -- -- Real(toRational), @@ -61,31 +80,23 @@ open import Haskell.Prim.Word public -- RealFrac(properFraction, truncate, round, ceiling, floor), -- RealFloat(floatRadix, floatDigits, floatRange, decodeFloat, -- encodeFloat, exponent, significand, scaleFloat, isNaN, --- isInfinite, isDenormalized, isIEEE, isNegativeZero, atan2), +-- isInfinite, isDenormalized, isIEEE, isNegativeZero, atan2) -- -- subtract, even, odd, gcd, lcm, (^), (^^), --- fromIntegral, realToFrac, --- --- foldr1, foldl1, maximum, minimum [Partial] +-- fromIntegral, realToFrac -- -- until [Partial] -- -- iterate, repeat, cycle [Infinite] -- -- ReadS, Read(readsPrec, readList), --- reads, readParen, read, lex, +-- reads, readParen, read, lex -- --- IO, putChar, putStr, putStrLn, print, --- getChar, getLine, getContents, interact, --- FilePath, readFile, writeFile, appendFile, readIO, readLn, --- IOError, ioError, userError, - +-- readIO, readLn, +-- IOError, ioError, userError --------------------------------------------------- --- Functions infixr 0 _$!_ - _$!_ : (a → b) → a → b _$!_ = _$_ @@ -104,37 +115,10 @@ error {i = ()} err errorWithoutStackTrace : {@0 @(tactic absurd) i : ⊥} → String → a errorWithoutStackTrace {i = ()} err -------------------------------------------------- --- More List functions --- These uses Eq, Ord, or Foldable, so can't go in Prim.List without --- turning those dependencies around. - -reverse : List a → List a -reverse = foldl (flip _∷_) [] - -infixl 9 _!!_ _!!ᴺ_ - -_!!ᴺ_ : (xs : List a) (n : Nat) → @0 ⦃ IsTrue (n < lengthNat xs) ⦄ → a -(x ∷ xs) !!ᴺ zero = x -(x ∷ xs) !!ᴺ suc n = xs !!ᴺ n - -_!!_ : (xs : List a) (n : Int) - → ⦃ @0 nn : IsNonNegativeInt n ⦄ - → ⦃ @0 _ : IsTrue (intToNat n {{nn}} < lengthNat xs) ⦄ → a -xs !! n = xs !!ᴺ intToNat n - -lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b -lookup x [] = Nothing -lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs - - -------------------------------------------------- --- Unsafe functions coerce : @0 a ≡ b → a → b coerce refl x = x IsJust : Maybe a → Type IsJust Nothing = ⊥ -IsJust (Just _) = ⊤ - +IsJust (Just _) = ⊤ \ No newline at end of file diff --git a/lib/base/Haskell/Prim.agda b/lib/base/Haskell/Prim.agda index 43b52006..295af905 100644 --- a/lib/base/Haskell/Prim.agda +++ b/lib/base/Haskell/Prim.agda @@ -22,6 +22,7 @@ open import Agda.Builtin.Word public renaming (primWord64ToNat to w2n; pri open import Agda.Builtin.Strict public open import Agda.Builtin.List public + variable @0 ℓ : Level a b c d e : Type @@ -65,6 +66,7 @@ if True then x else y = x the : (@0 a : Type ℓ) -> a -> a the _ x = x + -------------------------------------------------- -- Agda strings @@ -83,14 +85,6 @@ instance iNumberNat .fromNat n = n --------------------------------------------------- --- Lists - -lengthNat : List a → Nat -lengthNat [] = 0 -lengthNat (_ ∷ xs) = addNat 1 (lengthNat xs) - - -------------------------------------------------- -- Proof things @@ -99,7 +93,7 @@ data ⊥ : Type where magic : {A : Type} → ⊥ → A magic () ---principle of explosion +-- Principle of explosion exFalso : {x : Bool} → (x ≡ True) → (x ≡ False) → ⊥ exFalso {False} () b exFalso {True} a () diff --git a/lib/base/Haskell/Prim/Absurd.agda b/lib/base/Haskell/Prim/Absurd.agda index 349955dc..1fd4003d 100644 --- a/lib/base/Haskell/Prim/Absurd.agda +++ b/lib/base/Haskell/Prim/Absurd.agda @@ -1,12 +1,12 @@ - module Haskell.Prim.Absurd where open import Haskell.Prim +open import Haskell.Prim.List using (lengthNat) open import Agda.Builtin.Reflection renaming (bindTC to _>>=_; absurd to absurdP) -private +private pattern vArg x = arg (arg-info visible (modality relevant quantity-ω)) x refute : Nat → Term diff --git a/lib/base/Haskell/Prim/Alternative.agda b/lib/base/Haskell/Prim/Alternative.agda new file mode 100644 index 00000000..5e43a49b --- /dev/null +++ b/lib/base/Haskell/Prim/Alternative.agda @@ -0,0 +1,39 @@ +module Haskell.Prim.Alternative where + +open import Haskell.Prim +open import Haskell.Prim.Applicative +open import Haskell.Prim.IO +open import Haskell.Prim.List +open import Haskell.Prim.Maybe +open import Haskell.Prim.String + + +-------------------------------------------------------------------------------- +-- Alternative + +-- ** base +record Alternative (f : Type → Type) : Type₁ where + infixl 3 _<|>_ + field + empty : f a + _<|>_ : f a → f a → f a + overlap ⦃ super ⦄ : Applicative f + +-- ** export +open Alternative ⦃...⦄ public +{-# COMPILE AGDA2HS Alternative existing-class #-} + +-- ** instances +instance + iAlternativeList : Alternative List + iAlternativeList .empty = [] + iAlternativeList ._<|>_ = _++_ + + iAlternativeMaybe : Alternative Maybe + iAlternativeMaybe .empty = Nothing + iAlternativeMaybe ._<|>_ (Just x) _ = Just x + iAlternativeMaybe ._<|>_ Nothing y = y + + iAlternativeIO : Alternative IO + iAlternativeIO .empty = failIO "mzero" + iAlternativeIO ._<|>_ = mplusIO diff --git a/lib/base/Haskell/Prim/Applicative.agda b/lib/base/Haskell/Prim/Applicative.agda index 2629f90e..5d41fa76 100644 --- a/lib/base/Haskell/Prim/Applicative.agda +++ b/lib/base/Haskell/Prim/Applicative.agda @@ -11,20 +11,39 @@ open import Haskell.Prim.Monoid open import Haskell.Prim.Tuple --------------------------------------------------- +-------------------------------------------------------------------------------- -- Applicative -- ** base record Applicative (f : Type → Type) : Type₁ where infixl 4 _<*>_ _<*_ _*>_ field - pure : a → f a - _<*>_ : f (a → b) → f a → f b + pure : a → f a + _<*>_ : f (a → b) → f a → f b + liftA2 : (a → b → c) → f a → f b → f c overlap ⦃ super ⦄ : Functor f _<*_ : f a → f b → f a _*>_ : f a → f b → f b + -- ** defaults -record DefaultApplicative (f : Type → Type) : Type₁ where +record ApplicativeFromLiftA2 (f : Type → Type) : Type₁ where + constructor mk + infixl 4 _<*>_ _<*_ _*>_ + field + pure : a → f a + liftA2 : (a → b → c) → f a → f b → f c + overlap ⦃ super ⦄ : Functor f + + _<*>_ : f (a → b) → f a → f b + _<*>_ = liftA2 id + + _<*_ : f a → f b → f a + _<*_ = liftA2 const + + _*>_ : f a → f b → f b + x *> y = (id <$ x) <*> y + +record ApplicativeFrom<*> (f : Type → Type) : Type₁ where constructor mk infixl 4 _<*>_ _<*_ _*>_ field @@ -32,61 +51,71 @@ record DefaultApplicative (f : Type → Type) : Type₁ where _<*>_ : f (a → b) → f a → f b overlap ⦃ super ⦄ : Functor f + liftA2 : (a → b → c) → f a → f b → f c + liftA2 f x y = fmap f x <*> y + _<*_ : f a → f b → f a - x <* y = const <$> x <*> y + x <* y = fmap const x <*> y _*>_ : f a → f b → f b - x *> y = const id <$> x <*> y + x *> y = fmap (const id) x <*> y + -- ** export open Applicative ⦃...⦄ public {-# COMPILE AGDA2HS Applicative existing-class #-} + -- ** instances instance - open DefaultApplicative + open ApplicativeFrom<*> - iDefaultApplicativeList : DefaultApplicative List + iDefaultApplicativeList : ApplicativeFrom<*> List iDefaultApplicativeList .pure x = x ∷ [] - iDefaultApplicativeList ._<*>_ fs xs = concatMap (λ f → map f xs) fs + iDefaultApplicativeList ._<*>_ fs xs = foldMap (λ f → map f xs) fs iApplicativeList : Applicative List - iApplicativeList = record {DefaultApplicative iDefaultApplicativeList} + iApplicativeList = record {ApplicativeFrom<*> iDefaultApplicativeList} - iDefaultApplicativeMaybe : DefaultApplicative Maybe + iDefaultApplicativeMaybe : ApplicativeFrom<*> Maybe iDefaultApplicativeMaybe .pure = Just iDefaultApplicativeMaybe ._<*>_ (Just f) (Just x) = Just (f x) iDefaultApplicativeMaybe ._<*>_ _ _ = Nothing iApplicativeMaybe : Applicative Maybe - iApplicativeMaybe = record {DefaultApplicative iDefaultApplicativeMaybe} + iApplicativeMaybe = record {ApplicativeFrom<*> iDefaultApplicativeMaybe} - iDefaultApplicativeEither : DefaultApplicative (Either a) + iDefaultApplicativeEither : ApplicativeFrom<*> (Either a) iDefaultApplicativeEither .pure = Right iDefaultApplicativeEither ._<*>_ (Right f) (Right x) = Right (f x) iDefaultApplicativeEither ._<*>_ (Left e) _ = Left e iDefaultApplicativeEither ._<*>_ _ (Left e) = Left e iApplicativeEither : Applicative (Either a) - iApplicativeEither = record{DefaultApplicative iDefaultApplicativeEither} + iApplicativeEither = record{ApplicativeFrom<*> iDefaultApplicativeEither} - iDefaultApplicativeFun : DefaultApplicative (λ b → a → b) + iDefaultApplicativeFun : ApplicativeFrom<*> (λ b → a → b) iDefaultApplicativeFun .pure = const iDefaultApplicativeFun ._<*>_ f g x = f x (g x) iApplicativeFun : Applicative (λ b → a → b) - iApplicativeFun = record{DefaultApplicative iDefaultApplicativeFun} + iApplicativeFun = record{ApplicativeFrom<*> iDefaultApplicativeFun} - iDefaultApplicativeTuple₂ : ⦃ Monoid a ⦄ → DefaultApplicative (a ×_) + iDefaultApplicativeTuple₂ : ⦃ Monoid a ⦄ → ApplicativeFrom<*> (a ×_) iDefaultApplicativeTuple₂ .pure x = mempty , x iDefaultApplicativeTuple₂ ._<*>_ (a , f) (b , x) = a <> b , f x iApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_) - iApplicativeTuple₂ = record{DefaultApplicative iDefaultApplicativeTuple₂} + iApplicativeTuple₂ = record{ApplicativeFrom<*> iDefaultApplicativeTuple₂} - iDefaultApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultApplicative (a × b ×_) + iDefaultApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ApplicativeFrom<*> (a × b ×_) iDefaultApplicativeTuple₃ .pure x = mempty , mempty , x iDefaultApplicativeTuple₃ ._<*>_ (a , u , f) (b , v , x) = a <> b , u <> v , f x iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_) - iApplicativeTuple₃ = record{DefaultApplicative iDefaultApplicativeTuple₃} - -instance postulate iApplicativeIO : Applicative IO + iApplicativeTuple₃ = record{ApplicativeFrom<*> iDefaultApplicativeTuple₃} + + iDefaultApplicativeIO : ApplicativeFrom<*> IO + iDefaultApplicativeIO .pure = returnIO + iDefaultApplicativeIO ._<*>_ m1 m2 = bindIO m1 (λ f → bindIO m2 (λ x → returnIO (f x))) + + iApplicativeIO : Applicative IO + iApplicativeIO = record{ApplicativeFrom<*> iDefaultApplicativeIO} diff --git a/lib/base/Haskell/Prim/Foldable.agda b/lib/base/Haskell/Prim/Foldable.agda index 3de5cc27..84e80837 100644 --- a/lib/base/Haskell/Prim/Foldable.agda +++ b/lib/base/Haskell/Prim/Foldable.agda @@ -1,9 +1,9 @@ - module Haskell.Prim.Foldable where open import Haskell.Prim open import Haskell.Prim.Num hiding (abs) open import Haskell.Prim.Eq +open import Haskell.Prim.Ord open import Haskell.Prim.List open import Haskell.Prim.Int open import Haskell.Prim.Bool @@ -12,85 +12,106 @@ open import Haskell.Prim.Either open import Haskell.Prim.Tuple open import Haskell.Prim.Monoid --------------------------------------------------- + +-------------------------------------------------------------------------------- -- Foldable -- ** base record Foldable (t : Type → Type) : Type₁ where field - foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b - foldr : (a → b → b) → b → t a → b - foldl : (b → a → b) → b → t a → b - any : (a → Bool) → t a → Bool - all : (a → Bool) → t a → Bool - and : t Bool → Bool - null : t a → Bool - or : t Bool → Bool - concat : t (List a) → List a - concatMap : (a → List b) → t a → List b - elem : ⦃ Eq a ⦄ → a → t a → Bool - notElem : ⦃ Eq a ⦄ → a → t a → Bool - toList : t a → List a - sum : ⦃ iNum : Num a ⦄ → t a → a - product : ⦃ iNum : Num a ⦄ → t a → a - length : t a → Int + fold : ⦃ Monoid b ⦄ → t b → b + foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b + foldMap' : ⦃ Monoid b ⦄ → (a → b) → t a → b + foldr : (a → b → b) → b → t a → b + foldr' : (a → b → b) → b → t a → b + foldl : (b → a → b) → b → t a → b + foldl' : (b → a → b) → b → t a → b + toList : t a → List a + foldr1 : (a → a → a) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a + foldl1 : (a → a → a) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a + null : t a → Bool + length : t a → Int + elem : ⦃ Eq a ⦄ → a → t a → Bool + maximum : ⦃ Ord a ⦄ → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a + minimum : ⦃ Ord a ⦄ → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a + sum : ⦃ Num a ⦄ → t a → a + product : ⦃ Num a ⦄ → t a → a + -- ** defaults record DefaultFoldable (t : Type → Type) : Type₁ where - module M = Foldable {t = t} field foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b + fold : ⦃ Monoid b ⦄ → t b → b + fold = foldMap id + foldr : (a → b → b) → b → t a → b foldr f z t = foldMap ⦃ MonoidEndo ⦄ f t z + foldr' : (a → b → b) → b → t a → b + foldr' = foldr + foldl : (b → a → b) → b → t a → b foldl f z t = foldMap ⦃ MonoidEndoᵒᵖ ⦄ (flip f) t z - any : (a → Bool) → t a → Bool - any = foldMap ⦃ MonoidDisj ⦄ - - all : (a → Bool) → t a → Bool - all = foldMap ⦃ MonoidConj ⦄ + foldl' : (b → a → b) → b → t a → b + foldl' = foldl - and : t Bool → Bool - and = all id - - or : t Bool → Bool - or = any id + foldMap' : ⦃ Monoid b ⦄ → (a → b) → t a → b + foldMap' f = foldl' (λ acc a → acc <> f a) mempty + toList : t a → List a + toList = foldr _∷_ [] + + foldr1 : (a → a → a) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a + foldr1 f s = let l = toList s + xs , x = init l , last l + in foldrList f x xs + where + foldrList : (a → b → b) → b → List a → b + foldrList f z = λ where + [] → z + (x ∷ xs) → f x (foldrList f z xs) + + foldl1 : (a → a → a) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a + foldl1 f s with toList s + ... | x ∷ xs = foldlList f x xs + where + foldlList : (b → a → b) → b → List a → b + foldlList f z = λ where + [] → z + (x ∷ xs) → foldlList f (f z x) xs + null : t a → Bool - null = all (const False) - - concat : t (List a) → List a - concat = foldMap id - - concatMap : (a → List b) → t a → List b - concatMap = foldMap - + null = foldMap ⦃ MonoidConj ⦄ (const False) + + length : t a → Int + length = foldMap ⦃ MonoidSum ⦄ (const 1) + elem : ⦃ Eq a ⦄ → a → t a → Bool elem x = foldMap ⦃ MonoidDisj ⦄ (x ==_) - notElem : ⦃ Eq a ⦄ → a → t a → Bool - notElem x t = not (elem x t) + maximum : ⦃ Ord a ⦄ → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a + maximum = foldr1 max - toList : t a → List a - toList = foldr _∷_ [] + minimum : ⦃ Ord a ⦄ → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a + minimum = foldr1 min + + sum : ⦃ Num a ⦄ → t a → a + sum = fold ⦃ MonoidSum ⦄ + + product : ⦃ Num a ⦄ → t a → a + product = fold ⦃ MonoidProduct ⦄ - sum : ⦃ iNum : Num a ⦄ → t a → a - sum = foldMap ⦃ MonoidSum ⦄ id - - product : ⦃ iNum : Num a ⦄ → t a → a - product = foldMap ⦃ MonoidProduct ⦄ id - - length : t a → Int - length = foldMap ⦃ MonoidSum ⦄ (const 1) -- ** export open Foldable ⦃...⦄ public {-# COMPILE AGDA2HS Foldable existing-class #-} -- ** instances instance + open DefaultFoldable + iDefaultFoldableList : DefaultFoldable List - iDefaultFoldableList .DefaultFoldable.foldMap = foldMapList + iDefaultFoldableList .foldMap = foldMapList where foldMapList : ⦃ Monoid b ⦄ → (a → b) → List a → b foldMapList f [] = mempty @@ -100,7 +121,7 @@ instance iFoldableList = record {DefaultFoldable iDefaultFoldableList} iDefaultFoldableMaybe : DefaultFoldable Maybe - iDefaultFoldableMaybe .DefaultFoldable.foldMap = λ where + iDefaultFoldableMaybe .foldMap = λ where _ Nothing → mempty f (Just x) → f x @@ -108,7 +129,7 @@ instance iFoldableMaybe = record {DefaultFoldable iDefaultFoldableMaybe} iDefaultFoldableEither : DefaultFoldable (Either a) - iDefaultFoldableEither .DefaultFoldable.foldMap = λ where + iDefaultFoldableEither .foldMap = λ where _ (Left _) → mempty f (Right x) → f x @@ -116,7 +137,7 @@ instance iFoldableEither = record {DefaultFoldable iDefaultFoldableEither} iDefaultFoldablePair : DefaultFoldable (a ×_) - iDefaultFoldablePair .DefaultFoldable.foldMap = λ f (_ , x) → f x + iDefaultFoldablePair .foldMap = λ f (_ , x) → f x iFoldablePair : Foldable (a ×_) iFoldablePair = record {DefaultFoldable iDefaultFoldablePair} diff --git a/lib/base/Haskell/Prim/Functor.agda b/lib/base/Haskell/Prim/Functor.agda index c0847503..25dcc045 100644 --- a/lib/base/Haskell/Prim/Functor.agda +++ b/lib/base/Haskell/Prim/Functor.agda @@ -8,7 +8,8 @@ open import Haskell.Prim.List open import Haskell.Prim.Maybe open import Haskell.Prim.Tuple --------------------------------------------------- + +-------------------------------------------------------------------------------- -- Functor -- ** base @@ -17,12 +18,12 @@ record Functor (f : Type → Type) : Type₁ where field fmap : (a → b) → f a → f b _<$_ : (@0 {{ b }} → a) → f b → f a + -- ** defaults record DefaultFunctor (f : Type → Type) : Type₁ where field fmap : (a → b) → f a → f b infixl 4 _<$_ - _<$_ : (@0 {{ b }} → a) → f b → f a x <$ m = fmap (λ b → x {{b}}) m @@ -30,30 +31,18 @@ record DefaultFunctor (f : Type → Type) : Type₁ where open Functor ⦃...⦄ public {-# COMPILE AGDA2HS Functor existing-class #-} -_<$>_ : {{Functor f}} → (a → b) → f a → f b -_<$>_ = fmap - -_<&>_ : {{Functor f}} → f a → (a → b) → f b -m <&> f = fmap f m - -_$>_ : {{Functor f}} → f a → (@0 {{ a }} → b) → f b -m $> x = x <$ m - -void : {{Functor f}} → f a → f ⊤ -void = tt <$_ - -infixl 1 _<&>_ -infixl 4 _<$>_ _$>_ - +-- ** instances instance + open DefaultFunctor + iDefaultFunctorList : DefaultFunctor List - iDefaultFunctorList .DefaultFunctor.fmap = map + iDefaultFunctorList .fmap = map iFunctorList : Functor List iFunctorList = record{DefaultFunctor iDefaultFunctorList} iDefaultFunctorMaybe : DefaultFunctor Maybe - iDefaultFunctorMaybe .DefaultFunctor.fmap = λ where + iDefaultFunctorMaybe .fmap = λ where f Nothing → Nothing f (Just x) → Just (f x) @@ -61,7 +50,7 @@ instance iFunctorMaybe = record{DefaultFunctor iDefaultFunctorMaybe} iDefaultFunctorEither : DefaultFunctor (Either a) - iDefaultFunctorEither .DefaultFunctor.fmap = λ where + iDefaultFunctorEither .fmap = λ where f (Left x) → Left x f (Right y) → Right (f y) @@ -69,21 +58,25 @@ instance iFunctorEither = record{DefaultFunctor iDefaultFunctorEither} iDefaultFunctorFun : DefaultFunctor (λ b → a → b) - iDefaultFunctorFun .DefaultFunctor.fmap = _∘_ + iDefaultFunctorFun .fmap = _∘_ iFunctorFun : Functor (λ b → a → b) iFunctorFun = record{DefaultFunctor iDefaultFunctorFun} iDefaultFunctorTuple₂ : DefaultFunctor (a ×_) - iDefaultFunctorTuple₂ .DefaultFunctor.fmap = λ f (x , y) → x , f y + iDefaultFunctorTuple₂ .fmap = λ f (x , y) → x , f y iFunctorTuple₂ : Functor (a ×_) iFunctorTuple₂ = record{DefaultFunctor iDefaultFunctorTuple₂} iDefaultFunctorTuple₃ : DefaultFunctor (a × b ×_) - iDefaultFunctorTuple₃ .DefaultFunctor.fmap = λ where f (x , y , z) → x , y , f z + iDefaultFunctorTuple₃ .fmap = λ where f (x , y , z) → x , y , f z iFunctorTuple₃ : Functor (a × b ×_) iFunctorTuple₃ = record{DefaultFunctor iDefaultFunctorTuple₃} -instance postulate iFunctorIO : Functor IO + iDefaultFunctorIO : DefaultFunctor IO + iDefaultFunctorIO .fmap = λ f x → bindIO x (returnIO ∘ f) + + iFunctorIO : Functor IO + iFunctorIO = record{DefaultFunctor iDefaultFunctorIO} diff --git a/lib/base/Haskell/Prim/IO.agda b/lib/base/Haskell/Prim/IO.agda index b653e3c4..31b88ccc 100644 --- a/lib/base/Haskell/Prim/IO.agda +++ b/lib/base/Haskell/Prim/IO.agda @@ -4,6 +4,7 @@ open import Haskell.Prim open import Haskell.Prim.Show open import Haskell.Prim.String + postulate IO : ∀{a} → Type a → Type a FilePath = String @@ -25,3 +26,9 @@ postulate readFile : FilePath → IO String writeFile : FilePath → String → IO ⊤ appendFile : FilePath → String → IO ⊤ + + -- For instance definitions + returnIO : a → IO a + bindIO : IO a → (a → IO b) → IO b + failIO : String → IO a + mplusIO : IO a → IO a → IO a diff --git a/lib/base/Haskell/Prim/List.agda b/lib/base/Haskell/Prim/List.agda index 8343eb61..9979d4cb 100644 --- a/lib/base/Haskell/Prim/List.agda +++ b/lib/base/Haskell/Prim/List.agda @@ -2,127 +2,33 @@ module Haskell.Prim.List where open import Haskell.Prim -open import Haskell.Prim.Bool -open import Haskell.Prim.Tuple -open import Haskell.Prim.Int - -------------------------------------------------- -- List -map : (a → b) → List a → List b -map f [] = [] -map f (x ∷ xs) = f x ∷ map f xs - infixr 5 _++_ _++_ : ∀ {@0 ℓ} {@0 a : Type ℓ} → List a → List a → List a [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ xs ++ ys -filter : (a → Bool) → List a → List a -filter p [] = [] -filter p (x ∷ xs) = if p x then x ∷ filter p xs else filter p xs - -scanl : (b → a → b) → b → List a → List b -scanl f z [] = z ∷ [] -scanl f z (x ∷ xs) = z ∷ scanl f (f z x) xs - -scanr : (a → b → b) → b → List a → List b -scanr f z [] = z ∷ [] -scanr f z (x ∷ xs) = - case scanr f z xs of λ where - [] → [] -- impossible - qs@(q ∷ _) → f x q ∷ qs - -scanl1 : (a → a → a) → List a → List a -scanl1 f [] = [] -scanl1 f (x ∷ xs) = scanl f x xs - -scanr1 : (a → a → a) → List a → List a -scanr1 f [] = [] -scanr1 f (x ∷ []) = x ∷ [] -scanr1 f (x ∷ xs) = - case scanr1 f xs of λ where - [] → [] -- impossible - qs@(q ∷ _) → f x q ∷ qs - -takeWhile : (a → Bool) → List a → List a -takeWhile p [] = [] -takeWhile p (x ∷ xs) = if p x then x ∷ takeWhile p xs else [] - -dropWhile : (a → Bool) → List a → List a -dropWhile p [] = [] -dropWhile p (x ∷ xs) = if p x then dropWhile p xs else x ∷ xs - -span : (a → Bool) → List a → List a × List a -span p [] = [] , [] -span p (x ∷ xs) = if p x then first (x ∷_) (span p xs) - else ([] , x ∷ xs) - -break : (a → Bool) → List a → List a × List a -break p = span (not ∘ p) - -zipWith : (a → b → c) → List a → List b → List c -zipWith f [] _ = [] -zipWith f _ [] = [] -zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys - -zip : List a → List b → List (a × b) -zip = zipWith _,_ - -zipWith3 : (a → b → c → d) → List a → List b → List c → List d -zipWith3 f [] _ _ = [] -zipWith3 f _ [] _ = [] -zipWith3 f _ _ [] = [] -zipWith3 f (x ∷ xs) (y ∷ ys) (z ∷ zs) = f x y z ∷ zipWith3 f xs ys zs - -zip3 : List a → List b → List c → List (a × b × c) -zip3 = zipWith3 _,_,_ - -unzip : List (a × b) → List a × List b -unzip [] = [] , [] -unzip ((x , y) ∷ xys) = (x ∷_) *** (y ∷_) $ unzip xys - -unzip3 : List (a × b × c) → List a × List b × List c -unzip3 [] = [] , [] , [] -unzip3 ((x , y , z) ∷ xyzs) = - case unzip3 xyzs of λ where - (xs , ys , zs) → x ∷ xs , y ∷ ys , z ∷ zs - -takeNat : Nat → List a → List a -takeNat n [] = [] -takeNat zero xs = [] -takeNat (suc n) (x ∷ xs) = x ∷ takeNat n xs - -take : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a -take n xs = takeNat (intToNat n) xs - -dropNat : Nat → List a → List a -dropNat n [] = [] -dropNat zero xs = xs -dropNat (suc n) (_ ∷ xs) = dropNat n xs - -drop : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a -drop n xs = dropNat (intToNat n) xs - -splitAtNat : (n : Nat) → List a → List a × List a -splitAtNat _ [] = [] , [] -splitAtNat 0 xs = [] , xs -splitAtNat (suc n) (x ∷ xs) = first (x ∷_) (splitAtNat n xs) - -splitAt : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a × List a -splitAt n xs = splitAtNat (intToNat n) xs - head : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a head (x ∷ _) = x -tail : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a -tail (_ ∷ xs) = xs - last : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a last (x ∷ []) = x last (_ ∷ xs@(_ ∷ _)) = last xs +tail : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a +tail (_ ∷ xs) = xs + init : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a init (x ∷ []) = [] init (x ∷ xs@(_ ∷ _)) = x ∷ init xs + +map : (a → b) → List a → List b +map f [] = [] +map f (x ∷ xs) = f x ∷ map f xs + +lengthNat : List a → Nat +lengthNat [] = 0 +lengthNat (_ ∷ xs) = addNat 1 (lengthNat xs) \ No newline at end of file diff --git a/lib/base/Haskell/Prim/Monad.agda b/lib/base/Haskell/Prim/Monad.agda index bff504d7..05cf30e8 100644 --- a/lib/base/Haskell/Prim/Monad.agda +++ b/lib/base/Haskell/Prim/Monad.agda @@ -1,4 +1,3 @@ - module Haskell.Prim.Monad where open import Haskell.Prim @@ -10,10 +9,10 @@ open import Haskell.Prim.IO open import Haskell.Prim.List open import Haskell.Prim.Maybe open import Haskell.Prim.Monoid -open import Haskell.Prim.String open import Haskell.Prim.Tuple -------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- -- Monad module Do where @@ -25,6 +24,7 @@ module Do where overlap ⦃ super ⦄ : Applicative m return : a → m a _>>_ : m a → (@0 {{ a }} → m b) → m b + -- ** defaults record DefaultMonad (m : Type → Type) : Type₁ where field @@ -54,84 +54,50 @@ module Dont where open Do public -_=<<_ : {{Monad m}} → (a → m b) → m a → m b -_=<<_ = flip _>>=_ - -mapM₋ : ⦃ Monad m ⦄ → ⦃ Foldable t ⦄ → (a → m b) → t a → m ⊤ -mapM₋ f = foldr (λ x k → f x >> k) (pure tt) - -sequence₋ : ⦃ Monad m ⦄ → ⦃ Foldable t ⦄ → t (m a) → m ⊤ -sequence₋ = foldr (λ mx my → mx >> my) (pure tt) - -- ** instances instance + open DefaultMonad + iDefaultMonadList : DefaultMonad List - iDefaultMonadList .DefaultMonad._>>=_ = flip concatMap + iDefaultMonadList ._>>=_ = flip foldMap iMonadList : Monad List iMonadList = record {DefaultMonad iDefaultMonadList} iDefaultMonadMaybe : DefaultMonad Maybe - iDefaultMonadMaybe .DefaultMonad._>>=_ = flip (maybe Nothing) + iDefaultMonadMaybe ._>>=_ = flip (maybe Nothing) iMonadMaybe : Monad Maybe iMonadMaybe = record {DefaultMonad iDefaultMonadMaybe} iDefaultMonadEither : DefaultMonad (Either a) - iDefaultMonadEither .DefaultMonad._>>=_ = flip (either Left) + iDefaultMonadEither ._>>=_ = flip (either Left) iMonadEither : Monad (Either a) iMonadEither = record {DefaultMonad iDefaultMonadEither} iDefaultMonadFun : DefaultMonad (λ b → a → b) - iDefaultMonadFun .DefaultMonad._>>=_ = λ f k r → k (f r) r + iDefaultMonadFun ._>>=_ = λ f k r → k (f r) r iMonadFun : Monad (λ b → a → b) iMonadFun = record {DefaultMonad iDefaultMonadFun} iDefaultMonadTuple₂ : ⦃ Monoid a ⦄ → DefaultMonad (a ×_) - iDefaultMonadTuple₂ .DefaultMonad._>>=_ = λ (a , x) k → first (a <>_) (k x) + iDefaultMonadTuple₂ ._>>=_ = λ (a , x) k → first (a <>_) (k x) iMonadTuple₂ : ⦃ Monoid a ⦄ → Monad (a ×_) iMonadTuple₂ = record {DefaultMonad iDefaultMonadTuple₂} iDefaultMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonad (a × b ×_) - iDefaultMonadTuple₃ .DefaultMonad._>>=_ = λ where + iDefaultMonadTuple₃ ._>>=_ = λ where (a , b , x) k → case k x of λ where (a₁ , b₁ , y) → a <> a₁ , b <> b₁ , y iMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_) iMonadTuple₃ = record {DefaultMonad iDefaultMonadTuple₃} --- For 'Monad IO', we only postulate the '_>>=_' operation, --- and construct the instance via 'DefaultMonad' as usual. --- This is necessary to ensure that the existing 'Applicative IO' --- instance is picked for the 'super' instance field. -postulate - bindIO : IO a → (a → IO b) → IO b - -instance iDefaultMonadIO : DefaultMonad IO - iDefaultMonadIO .DefaultMonad._>>=_ = bindIO + iDefaultMonadIO ._>>=_ = bindIO iMonadIO : Monad IO iMonadIO = record {DefaultMonad iDefaultMonadIO} - -------------------------------------------------------------------------------- --- MonadFail class - -record MonadFail (m : Type → Type) : Type₁ where - field - fail : String → m a - overlap ⦃ super ⦄ : Monad m - -open MonadFail ⦃...⦄ public - -{-# COMPILE AGDA2HS MonadFail existing-class #-} - -instance - MonadFailList : MonadFail List - MonadFailList .fail _ = [] - - MonadFailMaybe : MonadFail Maybe - MonadFailMaybe .fail _ = Nothing diff --git a/lib/base/Haskell/Prim/MonadFail.agda b/lib/base/Haskell/Prim/MonadFail.agda new file mode 100644 index 00000000..65f569b4 --- /dev/null +++ b/lib/base/Haskell/Prim/MonadFail.agda @@ -0,0 +1,29 @@ +module Haskell.Prim.MonadFail where + +open import Haskell.Prim +open import Haskell.Prim.String +open import Haskell.Prim.Monad +open import Haskell.Prim.Maybe +open import Haskell.Prim.IO + + +-------------------------------------------------------------------------------- +-- MonadFail + +record MonadFail (m : Type → Type) : Type₁ where + field + fail : String → m a + overlap ⦃ super ⦄ : Monad m + +open MonadFail ⦃...⦄ public +{-# COMPILE AGDA2HS MonadFail existing-class #-} + +instance + MonadFailList : MonadFail List + MonadFailList .fail _ = [] + + MonadFailMaybe : MonadFail Maybe + MonadFailMaybe .fail _ = Nothing + + iMonadFailIO : MonadFail IO + iMonadFailIO .fail = failIO \ No newline at end of file diff --git a/lib/base/Haskell/Prim/MonadPlus.agda b/lib/base/Haskell/Prim/MonadPlus.agda new file mode 100644 index 00000000..3f925f8e --- /dev/null +++ b/lib/base/Haskell/Prim/MonadPlus.agda @@ -0,0 +1,58 @@ +module Haskell.Prim.MonadPlus where + +open import Haskell.Prim +open import Haskell.Prim.Alternative +open import Haskell.Prim.Monad +open import Haskell.Prim.IO +open import Haskell.Prim.List +open import Haskell.Prim.Maybe + + +-------------------------------------------------------------------------------- +-- MonadPlus + +-- ** base +record MonadPlus (m : Type → Type) : Type₁ where + field + overlap ⦃ super₁ ⦄ : Alternative m + overlap ⦃ super₂ ⦄ : Monad m + mzero : m a + mplus : m a → m a → m a + +-- ** default +record DefaultMonadPlus (m : Type → Type) : Type₁ where + field + overlap ⦃ super₁ ⦄ : Alternative m + overlap ⦃ super₂ ⦄ : Monad m + + mzero : m a + mzero = empty + + mplus : m a → m a → m a + mplus = _<|>_ + +-- ** export +open MonadPlus ⦃...⦄ public +{-# COMPILE AGDA2HS MonadPlus existing-class #-} + +-- ** instances +instance + open DefaultMonadPlus + + iDefaultMonadPlusList : DefaultMonadPlus List + iDefaultMonadPlusList = record {} + + iMonadPlusList : MonadPlus List + iMonadPlusList = record {DefaultMonadPlus iDefaultMonadPlusList} + + iDefaultMonadPlusMaybe : DefaultMonadPlus Maybe + iDefaultMonadPlusMaybe = record {} + + iMonadPlusMaybe : MonadPlus Maybe + iMonadPlusMaybe = record {DefaultMonadPlus iDefaultMonadPlusMaybe} + + iDefaultMonadPlusIO : DefaultMonadPlus IO + iDefaultMonadPlusIO = record {} + + iMonadPlusIO : MonadPlus IO + iMonadPlusIO = record {DefaultMonadPlus iDefaultMonadPlusIO} diff --git a/lib/base/Haskell/Prim/Monoid.agda b/lib/base/Haskell/Prim/Monoid.agda index a011cd11..90ef8e61 100644 --- a/lib/base/Haskell/Prim/Monoid.agda +++ b/lib/base/Haskell/Prim/Monoid.agda @@ -1,4 +1,3 @@ - module Haskell.Prim.Monoid where open import Haskell.Prim @@ -8,15 +7,20 @@ open import Haskell.Prim.Maybe open import Haskell.Prim.Either open import Haskell.Prim.Tuple --------------------------------------------------- + +-------------------------------------------------------------------------------- -- Semigroup +-- ** base record Semigroup (a : Type) : Type where infixr 6 _<>_ field _<>_ : a → a → a + +-- ** export open Semigroup ⦃...⦄ public {-# COMPILE AGDA2HS Semigroup existing-class #-} +-- ** instances instance iSemigroupList : Semigroup (List a) iSemigroupList ._<>_ = _++_ @@ -44,7 +48,7 @@ instance iSemigroupTuple₃ ._<>_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ <> x₂ , y₁ <> y₂ , z₁ <> z₂ --------------------------------------------------- +-------------------------------------------------------------------------------- -- Monoid -- ** base @@ -54,6 +58,7 @@ record Monoid (a : Type) : Type where overlap ⦃ super ⦄ : Semigroup a mappend : a → a → a mconcat : List a → a + -- ** defaults record DefaultMonoid (a : Type) : Type where field @@ -66,9 +71,11 @@ record DefaultMonoid (a : Type) : Type where mconcat : List a → a mconcat [] = mempty mconcat (x ∷ xs) = x <> mconcat xs + -- ** export open Monoid ⦃...⦄ public {-# COMPILE AGDA2HS Monoid existing-class #-} + -- ** instances instance iDefaultMonoidList : DefaultMonoid (List a) @@ -111,8 +118,8 @@ open DefaultMonoid MonoidEndo : Monoid (a → a) MonoidEndo = record {DefaultMonoid (λ where - .mempty → id - .super ._<>_ → _∘_)} + .mempty → id + .super ._<>_ → _∘_)} MonoidEndoᵒᵖ : Monoid (a → a) MonoidEndoᵒᵖ = record {DefaultMonoid (λ where @@ -128,3 +135,17 @@ MonoidDisj : Monoid Bool MonoidDisj = record {DefaultMonoid (λ where .mempty → False .super ._<>_ → _||_)} + +MonoidFirst : Monoid (Maybe a) +MonoidFirst = record {DefaultMonoid (λ where + .mempty → Nothing + .super ._<>_ → λ where + Nothing b → b + a _ → a)} + +MonoidLast : Monoid (Maybe a) +MonoidLast = record {DefaultMonoid (λ where + .mempty → Nothing + .super ._<>_ → λ where + a Nothing → a + _ b → b)} diff --git a/lib/base/Haskell/Prim/String.agda b/lib/base/Haskell/Prim/String.agda index 8024ce07..d5e80f22 100644 --- a/lib/base/Haskell/Prim/String.agda +++ b/lib/base/Haskell/Prim/String.agda @@ -2,51 +2,18 @@ module Haskell.Prim.String where open import Haskell.Prim -open import Haskell.Prim.List -open import Haskell.Prim.Foldable + -------------------------------------------------- -- String + -- This is _not_ the builtin String type of Agda -- which is defined by postulates. -- `fromString` can be used to convert back -- to builtin Agda strings. - String = List Char instance iIsStringString : IsString String iIsStringString .IsString.Constraint _ = ⊤ iIsStringString .fromString s = primStringToList s - -private - cons : Char → List String → List String - cons c [] = (c ∷ []) ∷ [] - cons c (s ∷ ss) = (c ∷ s) ∷ ss - -lines : String → List String -lines [] = [] -lines ('\n' ∷ s) = [] ∷ lines s -lines (c ∷ s) = cons c (lines s) - -private - mutual - space : String → List String - space [] = [] - space (c ∷ s) = if primIsSpace c then space s else cons c (word s) - - word : String → List String - word [] = [] - word (c ∷ s) = if primIsSpace c then [] ∷ space s else cons c (word s) - -words : String → List String -words [] = [] -words s@(c ∷ s₁) = if primIsSpace c then space s₁ else word s - -unlines : List String → String -unlines = concatMap (_++ "\n") - -unwords : List String → String -unwords [] = "" -unwords (w ∷ []) = w -unwords (w ∷ ws) = w ++ ' ' ∷ unwords ws diff --git a/lib/base/Haskell/Prim/Traversable.agda b/lib/base/Haskell/Prim/Traversable.agda index 0c97fbe7..51c324ae 100644 --- a/lib/base/Haskell/Prim/Traversable.agda +++ b/lib/base/Haskell/Prim/Traversable.agda @@ -1,5 +1,3 @@ - - module Haskell.Prim.Traversable where open import Haskell.Prim @@ -12,7 +10,8 @@ open import Haskell.Prim.Maybe open import Haskell.Prim.Either open import Haskell.Prim.Tuple --------------------------------------------------- + +-------------------------------------------------------------------------------- -- Traversable -- ** base @@ -25,6 +24,7 @@ record Traversable (t : Type → Type) : Type₁ where sequenceA : ⦃ Applicative f ⦄ → t (f a) → f (t a) mapM : ⦃ Monad m ⦄ → (a → m b) → t a → m (t b) sequence : ⦃ Monad m ⦄ → t (m a) → m (t a) + -- ** defaults record DefaultTraversable (t : Type → Type) : Type₁ where field @@ -40,9 +40,11 @@ record DefaultTraversable (t : Type → Type) : Type₁ where sequence : ⦃ Monad m ⦄ → t (m a) → m (t a) sequence = sequenceA + -- ** export open Traversable ⦃...⦄ public {-# COMPILE AGDA2HS Traversable existing-class #-} + -- ** instances private mkTraversable : DefaultTraversable t → Traversable t @@ -66,13 +68,13 @@ instance iTraversableMaybe : Traversable Maybe iTraversableMaybe = traverse= λ where f Nothing → pure Nothing - f (Just x) → Just <$> f x + f (Just x) → fmap Just (f x) iTraversableEither : Traversable (Either a) iTraversableEither = traverse= λ where f (Left x) → pure (Left x) - f (Right y) → Right <$> f y + f (Right y) → fmap Right (f y) iTraversablePair : Traversable (a ×_) iTraversablePair = traverse= λ - f (x , y) → (x ,_) <$> f y + f (x , y) → fmap (x ,_) (f y) From e67238c6cdc011a6aa51615749da24728bc3b1a1 Mon Sep 17 00:00:00 2001 From: Lukas Rohde Date: Wed, 18 Mar 2026 14:41:29 +0100 Subject: [PATCH 2/8] Fix: whitespace --- lib/base/Haskell/Control/Applicative.agda | 2 +- lib/base/Haskell/Control/Monad.agda | 2 +- lib/base/Haskell/Data/Foldable.agda | 2 +- lib/base/Haskell/Data/String.agda | 2 +- lib/base/Haskell/Data/Traversable.agda | 20 ++++++++++---------- lib/base/Haskell/Prelude.agda | 2 +- lib/base/Haskell/Prim/Applicative.agda | 2 +- lib/base/Haskell/Prim/Foldable.agda | 12 ++++++------ lib/base/Haskell/Prim/List.agda | 2 +- lib/base/Haskell/Prim/Monad.agda | 2 +- lib/base/Haskell/Prim/MonadFail.agda | 2 +- lib/base/Haskell/Prim/MonadPlus.agda | 6 +++--- 12 files changed, 28 insertions(+), 28 deletions(-) diff --git a/lib/base/Haskell/Control/Applicative.agda b/lib/base/Haskell/Control/Applicative.agda index 0126c992..a55a2c61 100644 --- a/lib/base/Haskell/Control/Applicative.agda +++ b/lib/base/Haskell/Control/Applicative.agda @@ -26,4 +26,4 @@ optional v = Just <$> v <|> pure Nothing -- - 'newtype Const a (b :: k) = Const { getConst :: a }' -- - 'newtype WrappedMonad (m :: Type -> Type) a = WrapMonad { unwrapMonad :: m a }' -- - 'newtype WrappedArrow (a :: Type -> Type -> Type) b c = WrapArrow { unwrapArrow :: a b c }' --- - 'newtype ZipList a = ZipList { getZipList :: [a] }' \ No newline at end of file +-- - 'newtype ZipList a = ZipList { getZipList :: [a] }' diff --git a/lib/base/Haskell/Control/Monad.agda b/lib/base/Haskell/Control/Monad.agda index 05189234..b2f0778f 100644 --- a/lib/base/Haskell/Control/Monad.agda +++ b/lib/base/Haskell/Control/Monad.agda @@ -90,7 +90,7 @@ unless False f = f {refl} liftM : ⦃ Monad m ⦄ → (a1 → r) → m a1 → m r -liftM f m1 = do +liftM f m1 = do x1 ← m1 return (f x1) diff --git a/lib/base/Haskell/Data/Foldable.agda b/lib/base/Haskell/Data/Foldable.agda index 47bb5d28..0f420072 100644 --- a/lib/base/Haskell/Data/Foldable.agda +++ b/lib/base/Haskell/Data/Foldable.agda @@ -82,4 +82,4 @@ notElem : ⦃ Foldable t ⦄ → ⦃ Eq a ⦄ → a → t a → Bool notElem x t = not (elem x t) find : ⦃ Foldable t ⦄ → (a → Bool) → t a → Maybe a -find ⦃ i ⦄ p = foldMap ⦃ i ⦄ ⦃ MonoidFirst ⦄ (λ x → if p x then Just x else Nothing) \ No newline at end of file +find ⦃ i ⦄ p = foldMap ⦃ i ⦄ ⦃ MonoidFirst ⦄ (λ x → if p x then Just x else Nothing) diff --git a/lib/base/Haskell/Data/String.agda b/lib/base/Haskell/Data/String.agda index 450bb45d..00954ad7 100644 --- a/lib/base/Haskell/Data/String.agda +++ b/lib/base/Haskell/Data/String.agda @@ -37,4 +37,4 @@ unlines = concatMap (_++ "\n") unwords : List String → String unwords [] = "" unwords (w ∷ []) = w -unwords (w ∷ ws) = w ++ ' ' ∷ unwords ws \ No newline at end of file +unwords (w ∷ ws) = w ++ ' ' ∷ unwords ws diff --git a/lib/base/Haskell/Data/Traversable.agda b/lib/base/Haskell/Data/Traversable.agda index 1330eef7..ec88f100 100644 --- a/lib/base/Haskell/Data/Traversable.agda +++ b/lib/base/Haskell/Data/Traversable.agda @@ -22,39 +22,39 @@ private constructor mkState pattern field run : s → s × a - + record StateT (s : Type) (m : Type → Type) (a : Type) : Type where constructor mkStateT pattern field run : s → m (s × a) - + instance open DefaultFunctor open ApplicativeFrom<*> - + iDefaultFunctorState : DefaultFunctor (State s) iDefaultFunctorState .fmap f (mkState k) = mkState $ λ s → let s' , v = k s in s' , f v iFunctorState : Functor (State s) iFunctorState = record { DefaultFunctor iDefaultFunctorState } - + iDefaultApplicativeStateL : ApplicativeFrom<*> (State s) iDefaultApplicativeStateL .pure x = mkState (λ s → s , x) iDefaultApplicativeStateL ._<*>_ (mkState kf) (mkState kx) = mkState $ λ s → let s' , f = kf s s'' , x = kx s' in s'' , f x - + iApplicativeStateL : Applicative (State s) iApplicativeStateL = record { ApplicativeFrom<*> iDefaultApplicativeStateL } - + iDefaultApplicativeStateR : ApplicativeFrom<*> (State s) iDefaultApplicativeStateR .pure x = mkState (λ s → s , x) iDefaultApplicativeStateR ._<*>_ (mkState kf) (mkState kx) = mkState $ λ s → let s' , x = kx s s'' , f = kf s' in s'' , f x - + iApplicativeStateR : Applicative (State s) iApplicativeStateR = record { ApplicativeFrom<*> iDefaultApplicativeStateR } @@ -72,7 +72,7 @@ private s' , f ← kf s s'' , x ← kx s' return (s'' , f x) - + iApplicativeStateT : ⦃ Monad m ⦄ → Applicative (StateT s m) iApplicativeStateT = record { ApplicativeFrom<*> iDefaultApplicativeStateT} @@ -80,7 +80,7 @@ private iDefaultMonadStateT .DefaultMonad._>>=_ m k = mkStateT $ λ s → do s' , x ← StateT.run m s StateT.run (k x) s' - + iMonadStateT : ⦃ Monad m ⦄ → Monad (StateT s m) iMonadStateT = record { DefaultMonad iDefaultMonadStateT } @@ -98,4 +98,4 @@ forAccumM s t f = mapAccumM f s t -- Omitted for now: -- - 'fmapDefault :: Traversable t => (a -> b) -> t a -> t b' --- - 'foldMapDefault :: (Traversable t, Monoid m) => (a -> m) -> t a -> m' \ No newline at end of file +-- - 'foldMapDefault :: (Traversable t, Monoid m) => (a -> m) -> t a -> m' diff --git a/lib/base/Haskell/Prelude.agda b/lib/base/Haskell/Prelude.agda index f02bc79c..17023ade 100644 --- a/lib/base/Haskell/Prelude.agda +++ b/lib/base/Haskell/Prelude.agda @@ -121,4 +121,4 @@ coerce refl x = x IsJust : Maybe a → Type IsJust Nothing = ⊥ -IsJust (Just _) = ⊤ \ No newline at end of file +IsJust (Just _) = ⊤ diff --git a/lib/base/Haskell/Prim/Applicative.agda b/lib/base/Haskell/Prim/Applicative.agda index 5d41fa76..b7382423 100644 --- a/lib/base/Haskell/Prim/Applicative.agda +++ b/lib/base/Haskell/Prim/Applicative.agda @@ -116,6 +116,6 @@ instance iDefaultApplicativeIO : ApplicativeFrom<*> IO iDefaultApplicativeIO .pure = returnIO iDefaultApplicativeIO ._<*>_ m1 m2 = bindIO m1 (λ f → bindIO m2 (λ x → returnIO (f x))) - + iApplicativeIO : Applicative IO iApplicativeIO = record{ApplicativeFrom<*> iDefaultApplicativeIO} diff --git a/lib/base/Haskell/Prim/Foldable.agda b/lib/base/Haskell/Prim/Foldable.agda index 84e80837..bab4482b 100644 --- a/lib/base/Haskell/Prim/Foldable.agda +++ b/lib/base/Haskell/Prim/Foldable.agda @@ -61,7 +61,7 @@ record DefaultFoldable (t : Type → Type) : Type₁ where toList : t a → List a toList = foldr _∷_ [] - + foldr1 : (a → a → a) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a foldr1 f s = let l = toList s xs , x = init l , last l @@ -80,13 +80,13 @@ record DefaultFoldable (t : Type → Type) : Type₁ where foldlList f z = λ where [] → z (x ∷ xs) → foldlList f (f z x) xs - + null : t a → Bool null = foldMap ⦃ MonoidConj ⦄ (const False) - + length : t a → Int length = foldMap ⦃ MonoidSum ⦄ (const 1) - + elem : ⦃ Eq a ⦄ → a → t a → Bool elem x = foldMap ⦃ MonoidDisj ⦄ (x ==_) @@ -95,10 +95,10 @@ record DefaultFoldable (t : Type → Type) : Type₁ where minimum : ⦃ Ord a ⦄ → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a minimum = foldr1 min - + sum : ⦃ Num a ⦄ → t a → a sum = fold ⦃ MonoidSum ⦄ - + product : ⦃ Num a ⦄ → t a → a product = fold ⦃ MonoidProduct ⦄ diff --git a/lib/base/Haskell/Prim/List.agda b/lib/base/Haskell/Prim/List.agda index 9979d4cb..87d2cc5b 100644 --- a/lib/base/Haskell/Prim/List.agda +++ b/lib/base/Haskell/Prim/List.agda @@ -31,4 +31,4 @@ map f (x ∷ xs) = f x ∷ map f xs lengthNat : List a → Nat lengthNat [] = 0 -lengthNat (_ ∷ xs) = addNat 1 (lengthNat xs) \ No newline at end of file +lengthNat (_ ∷ xs) = addNat 1 (lengthNat xs) diff --git a/lib/base/Haskell/Prim/Monad.agda b/lib/base/Haskell/Prim/Monad.agda index 05cf30e8..84f1b3b9 100644 --- a/lib/base/Haskell/Prim/Monad.agda +++ b/lib/base/Haskell/Prim/Monad.agda @@ -24,7 +24,7 @@ module Do where overlap ⦃ super ⦄ : Applicative m return : a → m a _>>_ : m a → (@0 {{ a }} → m b) → m b - + -- ** defaults record DefaultMonad (m : Type → Type) : Type₁ where field diff --git a/lib/base/Haskell/Prim/MonadFail.agda b/lib/base/Haskell/Prim/MonadFail.agda index 65f569b4..00c26b75 100644 --- a/lib/base/Haskell/Prim/MonadFail.agda +++ b/lib/base/Haskell/Prim/MonadFail.agda @@ -26,4 +26,4 @@ instance MonadFailMaybe .fail _ = Nothing iMonadFailIO : MonadFail IO - iMonadFailIO .fail = failIO \ No newline at end of file + iMonadFailIO .fail = failIO diff --git a/lib/base/Haskell/Prim/MonadPlus.agda b/lib/base/Haskell/Prim/MonadPlus.agda index 3f925f8e..1557731c 100644 --- a/lib/base/Haskell/Prim/MonadPlus.agda +++ b/lib/base/Haskell/Prim/MonadPlus.agda @@ -24,7 +24,7 @@ record DefaultMonadPlus (m : Type → Type) : Type₁ where field overlap ⦃ super₁ ⦄ : Alternative m overlap ⦃ super₂ ⦄ : Monad m - + mzero : m a mzero = empty @@ -50,9 +50,9 @@ instance iMonadPlusMaybe : MonadPlus Maybe iMonadPlusMaybe = record {DefaultMonadPlus iDefaultMonadPlusMaybe} - + iDefaultMonadPlusIO : DefaultMonadPlus IO iDefaultMonadPlusIO = record {} - + iMonadPlusIO : MonadPlus IO iMonadPlusIO = record {DefaultMonadPlus iDefaultMonadPlusIO} From 54597331222a34ada0cc5525fbbd85dea235c400 Mon Sep 17 00:00:00 2001 From: Lukas Rohde Date: Wed, 18 Mar 2026 23:32:30 +0100 Subject: [PATCH 3/8] Fix: test with invalid reference to renamed symbol --- test/Succeed/Issue421.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/test/Succeed/Issue421.agda b/test/Succeed/Issue421.agda index 250cf454..bc61acb7 100644 --- a/test/Succeed/Issue421.agda +++ b/test/Succeed/Issue421.agda @@ -18,12 +18,12 @@ instance iFunctorIdentity : Functor Identity iFunctorIdentity = record {DefaultFunctor iDefaultFunctorIdentity} - iDefaultApplicativeIdentity : DefaultApplicative Identity - iDefaultApplicativeIdentity .DefaultApplicative.pure = MkIdentity - iDefaultApplicativeIdentity .DefaultApplicative._<*>_ (MkIdentity f) (MkIdentity x) = MkIdentity (f x) + iDefaultApplicativeIdentity : ApplicativeFrom<*> Identity + iDefaultApplicativeIdentity .ApplicativeFrom<*>.pure = MkIdentity + iDefaultApplicativeIdentity .ApplicativeFrom<*>._<*>_ (MkIdentity f) (MkIdentity x) = MkIdentity (f x) iApplicativeIdentity : Applicative Identity - iApplicativeIdentity = record {DefaultApplicative iDefaultApplicativeIdentity} + iApplicativeIdentity = record {ApplicativeFrom<*> iDefaultApplicativeIdentity} {-# COMPILE AGDA2HS iFunctorIdentity #-} {-# COMPILE AGDA2HS iApplicativeIdentity #-} -- generates pure and (<*>) multiple times From b66a5eea550f4747ced94e443f2a1d3f77fa8bdb Mon Sep 17 00:00:00 2001 From: Lukas Rohde Date: Thu, 19 Mar 2026 21:36:43 +0100 Subject: [PATCH 4/8] Mark some variables as private to avoid polluting the namespace --- lib/base/Haskell/Control/Monad.agda | 10 +++++----- lib/base/Haskell/Data/Traversable.agda | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lib/base/Haskell/Control/Monad.agda b/lib/base/Haskell/Control/Monad.agda index b2f0778f..de841724 100644 --- a/lib/base/Haskell/Control/Monad.agda +++ b/lib/base/Haskell/Control/Monad.agda @@ -22,7 +22,7 @@ open import Haskell.Data.Foldable public using (mapM₋; forM₋; sequence₋; m open import Haskell.Data.Functor public using (void) -variable a1 a2 a3 a4 a5 r : Type +private variable a1 a2 a3 a4 a5 r : Type infixr 1 _=<<_ _>=>_ _<=<_ _=<<_ : ⦃ Monad m ⦄ → (a → m b) → m a → m b @@ -43,16 +43,16 @@ mfilter p ma = do a ← ma if p a then return a else mzero -filterM : ⦃ Applicative m ⦄ → (a → m Bool) → (List a) → m (List a) +filterM : ⦃ Applicative m ⦄ → (a → m Bool) → List a → m (List a) filterM p = foldr (λ x → liftA2 (λ b → if b then (x ∷_) else id) (p x)) (pure []) -mapAndUnzipM : ⦃ Applicative m ⦄ → (a → m (b × c)) → (List a) → m (List b × List c) +mapAndUnzipM : ⦃ Applicative m ⦄ → (a → m (b × c)) → List a → m (List b × List c) mapAndUnzipM f xs = fmap unzip (traverse f xs) -zipWithM : ⦃ Applicative m ⦄ → (a → b → m c) → (List a) → (List b) → m (List c) +zipWithM : ⦃ Applicative m ⦄ → (a → b → m c) → List a → List b → m (List c) zipWithM f xs ys = sequenceA (zipWith f xs ys) -zipWithM₋ : ⦃ Applicative m ⦄ → (a → b → m c) → (List a) → (List b) → m ⊤ +zipWithM₋ : ⦃ Applicative m ⦄ → (a → b → m c) → List a → List b → m ⊤ zipWithM₋ f xs ys = sequenceA₋ (zipWith f xs ys) foldM : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (b → a → m b) → b → t a → m b diff --git a/lib/base/Haskell/Data/Traversable.agda b/lib/base/Haskell/Data/Traversable.agda index ec88f100..93ccc529 100644 --- a/lib/base/Haskell/Data/Traversable.agda +++ b/lib/base/Haskell/Data/Traversable.agda @@ -9,7 +9,7 @@ open import Haskell.Prim.Tuple open import Haskell.Prim.Traversable public -variable s : Type +private variable s : Type for : ⦃ Traversable t ⦄ → ⦃ Applicative f ⦄ → t a → (a → f b) → f (t b) for = flip traverse From e604278fbf1aa47afb7a83b5544898bcec2b782b Mon Sep 17 00:00:00 2001 From: Lukas Rohde Date: Wed, 25 Mar 2026 12:04:45 +0100 Subject: [PATCH 5/8] Expose some private definitions through helper submodules --- lib/base/Haskell/Data/String.agda | 4 +++- lib/base/Haskell/Data/Traversable.agda | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/lib/base/Haskell/Data/String.agda b/lib/base/Haskell/Data/String.agda index 00954ad7..89544bbf 100644 --- a/lib/base/Haskell/Data/String.agda +++ b/lib/base/Haskell/Data/String.agda @@ -8,7 +8,7 @@ open import Haskell.Data.Foldable open import Haskell.Prim.String public -private +module Helpers where cons : Char → List String → List String cons c [] = (c ∷ []) ∷ [] cons c (s ∷ ss) = (c ∷ s) ∷ ss @@ -21,6 +21,8 @@ private word : String → List String word [] = [] word (c ∷ s) = if primIsSpace c then [] ∷ space s else cons c (word s) + +open Helpers lines : String → List String lines [] = [] diff --git a/lib/base/Haskell/Data/Traversable.agda b/lib/base/Haskell/Data/Traversable.agda index 93ccc529..4e83c401 100644 --- a/lib/base/Haskell/Data/Traversable.agda +++ b/lib/base/Haskell/Data/Traversable.agda @@ -17,7 +17,7 @@ for = flip traverse forM : ⦃ Traversable t ⦄ → ⦃ Monad m ⦄ → t a → (a → m b) → m (t b) forM = flip mapM -private +module Helpers where record State (s a : Type) : Type where constructor mkState pattern @@ -84,6 +84,8 @@ private iMonadStateT : ⦃ Monad m ⦄ → Monad (StateT s m) iMonadStateT = record { DefaultMonad iDefaultMonadStateT } +open Helpers + mapAccumL : ⦃ Traversable t ⦄ → (s → a → s × b) → s → t a → s × t b mapAccumL ⦃ iTraversable ⦄ f s t = State.run (traverse ⦃ iTraversable ⦄ ⦃ iApplicativeStateL ⦄ (mkState ∘ flip f) t) s From 822285b4d2e25a47324b2ad5eaa23ea08334ae0b Mon Sep 17 00:00:00 2001 From: Lukas Rohde Date: Wed, 25 Mar 2026 12:52:23 +0100 Subject: [PATCH 6/8] Fix: whitespace --- lib/base/Haskell/Data/String.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/base/Haskell/Data/String.agda b/lib/base/Haskell/Data/String.agda index 89544bbf..bb29fe51 100644 --- a/lib/base/Haskell/Data/String.agda +++ b/lib/base/Haskell/Data/String.agda @@ -21,7 +21,7 @@ module Helpers where word : String → List String word [] = [] word (c ∷ s) = if primIsSpace c then [] ∷ space s else cons c (word s) - + open Helpers lines : String → List String From 80f58c28a089ac35ffd2b5d2674ebad83bcd292c Mon Sep 17 00:00:00 2001 From: Lukas Rohde Date: Fri, 27 Mar 2026 11:02:35 +0100 Subject: [PATCH 7/8] Introduce submodules for instances of type classes and extract `Semigroup` into its own module --- lib/base/Haskell/Control/Applicative.agda | 2 + lib/base/Haskell/Control/Monad.agda | 21 +- lib/base/Haskell/Data/Foldable.agda | 31 +- lib/base/Haskell/Data/Functor.agda | 1 + lib/base/Haskell/Data/List.agda | 16 +- lib/base/Haskell/Data/String.agda | 4 +- lib/base/Haskell/Data/Traversable.agda | 15 +- lib/base/Haskell/Law/Monoid/Def.agda | 3 + lib/base/Haskell/Law/Semigroup/Def.agda | 2 +- lib/base/Haskell/Law/Semigroup/Either.agda | 2 +- lib/base/Haskell/Law/Semigroup/List.agda | 2 +- lib/base/Haskell/Law/Semigroup/Maybe.agda | 2 +- lib/base/Haskell/Prelude.agda | 29 +- lib/base/Haskell/Prim/Alternative.agda | 29 +- lib/base/Haskell/Prim/Applicative.agda | 93 ++--- lib/base/Haskell/Prim/Bounded.agda | 115 ++++--- lib/base/Haskell/Prim/Enum.agda | 377 +++++++++++---------- lib/base/Haskell/Prim/Eq.agda | 81 ++--- lib/base/Haskell/Prim/Foldable.agda | 80 +++-- lib/base/Haskell/Prim/Functor.agda | 70 ++-- lib/base/Haskell/Prim/Monad.agda | 78 +++-- lib/base/Haskell/Prim/MonadFail.agda | 19 +- lib/base/Haskell/Prim/MonadPlus.agda | 32 +- lib/base/Haskell/Prim/Monoid.agda | 94 ++--- lib/base/Haskell/Prim/Num.agda | 151 +++++---- lib/base/Haskell/Prim/Ord.agda | 238 ++++++------- lib/base/Haskell/Prim/Semigroup.agda | 48 +++ lib/base/Haskell/Prim/Show.agda | 135 ++++---- lib/base/Haskell/Prim/Traversable.agda | 75 ++-- 29 files changed, 996 insertions(+), 849 deletions(-) create mode 100644 lib/base/Haskell/Prim/Semigroup.agda diff --git a/lib/base/Haskell/Control/Applicative.agda b/lib/base/Haskell/Control/Applicative.agda index a55a2c61..2e44047b 100644 --- a/lib/base/Haskell/Control/Applicative.agda +++ b/lib/base/Haskell/Control/Applicative.agda @@ -4,7 +4,9 @@ open import Haskell.Prim open import Haskell.Prim.Maybe open import Haskell.Prim.Applicative public + renaming (module Instances to ApplicativeInstances) open import Haskell.Prim.Alternative public + renaming (module Instances to AlternativeInstances) open import Haskell.Data.Functor public using (_<$>_) open import Haskell.Data.Foldable public using (asum) diff --git a/lib/base/Haskell/Control/Monad.agda b/lib/base/Haskell/Control/Monad.agda index de841724..463271b5 100644 --- a/lib/base/Haskell/Control/Monad.agda +++ b/lib/base/Haskell/Control/Monad.agda @@ -4,19 +4,30 @@ open import Haskell.Prim open import Haskell.Prim.Bool open import Haskell.Prim.Int open import Haskell.Prim.Tuple -open import Haskell.Prim.Applicative -open import Haskell.Prim.Alternative -open import Haskell.Prim.Traversable -open import Haskell.Prim.Foldable +open import Haskell.Prim.Applicative hiding (module Instances) +open import Haskell.Prim.Alternative hiding (module Instances) +open import Haskell.Prim.Traversable hiding (module Instances) +open import Haskell.Prim.Foldable hiding (module Instances) open import Haskell.Data.Foldable using (sequenceA₋; foldlM) open import Haskell.Data.List using (unzip; zipWith) open import Haskell.Extra.Erase open import Haskell.Prim.Functor public + renaming (module Instances to FunctorInstances) +open import Haskell.Prim.Applicative public + using () renaming (module Instances to ApplicativeInstances) +open import Haskell.Prim.Alternative public + using () renaming (module Instances to AlternativeInstances) open import Haskell.Prim.Monad public + renaming (module Instances to MonadInstances) open import Haskell.Prim.MonadFail public + renaming (module Instances to MonadFailInstances) open import Haskell.Prim.MonadPlus public -open import Haskell.Prim.Traversable public using (mapM; sequence) + renaming (module Instances to MonadPlusInstances) +open import Haskell.Prim.Traversable public + using (mapM; sequence) renaming (module Instances to TraversableInstances) +open import Haskell.Prim.Foldable public + using () renaming (module Instances to FoldableInstances) open import Haskell.Data.Traversable public using (forM) open import Haskell.Data.Foldable public using (mapM₋; forM₋; sequence₋; msum) open import Haskell.Data.Functor public using (void) diff --git a/lib/base/Haskell/Data/Foldable.agda b/lib/base/Haskell/Data/Foldable.agda index 0f420072..9de1012c 100644 --- a/lib/base/Haskell/Data/Foldable.agda +++ b/lib/base/Haskell/Data/Foldable.agda @@ -1,17 +1,32 @@ module Haskell.Data.Foldable where open import Haskell.Prim -open import Haskell.Prim.Monad -open import Haskell.Prim.Applicative -open import Haskell.Prim.Alternative -open import Haskell.Prim.MonadPlus -open import Haskell.Prim.Monoid -open import Haskell.Prim.Eq -open import Haskell.Prim.Ord open import Haskell.Prim.Bool open import Haskell.Prim.Maybe - +open import Haskell.Prim.Eq hiding (module Instances) +open import Haskell.Prim.Ord hiding (module Instances) +open import Haskell.Prim.Monoid hiding (module Instances) +open import Haskell.Prim.Applicative hiding (module Instances) +open import Haskell.Prim.Alternative hiding (module Instances) +open import Haskell.Prim.Monad hiding (module Instances) +open import Haskell.Prim.MonadPlus hiding (module Instances) + +open import Haskell.Prim.Eq public + using () renaming (module Instances to EqInstances) +open import Haskell.Prim.Ord public + using () renaming (module Instances to OrdInstances) +open import Haskell.Prim.Monoid public + using () renaming (module Instances to MonoidInstances) +open import Haskell.Prim.Applicative public + using () renaming (module Instances to ApplicativeInstances) +open import Haskell.Prim.Alternative public + using () renaming (module Instances to AlternativeInstances) +open import Haskell.Prim.Monad public + using () renaming (module Instances to MonadInstances) +open import Haskell.Prim.MonadPlus public + using () renaming (module Instances to MonadPlusInstances) open import Haskell.Prim.Foldable public + renaming (module Instances to FoldableInstances) foldrM : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (a → b → m b) → b → t a → m b diff --git a/lib/base/Haskell/Data/Functor.agda b/lib/base/Haskell/Data/Functor.agda index ab48834d..9f7ae4e3 100644 --- a/lib/base/Haskell/Data/Functor.agda +++ b/lib/base/Haskell/Data/Functor.agda @@ -4,6 +4,7 @@ open import Haskell.Prim open import Haskell.Prim.Tuple open import Haskell.Prim.Functor public + renaming (module Instances to FunctorInstances) infixl 4 _$>_ diff --git a/lib/base/Haskell/Data/List.agda b/lib/base/Haskell/Data/List.agda index a620c739..84f86991 100644 --- a/lib/base/Haskell/Data/List.agda +++ b/lib/base/Haskell/Data/List.agda @@ -5,14 +5,20 @@ open import Haskell.Prim.Bool open import Haskell.Prim.Tuple open import Haskell.Prim.Int open import Haskell.Prim.Maybe -open import Haskell.Prim.Ord -open import Haskell.Prim.Num -open import Haskell.Prim.Eq +open import Haskell.Prim.Eq hiding (module Instances) +open import Haskell.Prim.Ord hiding (module Instances) +open import Haskell.Prim.Num hiding (module Instances) open import Haskell.Prim.List public -open import Haskell.Prim.Foldable public using (Foldable) -open Foldable ⦃ ... ⦄ public +open import Haskell.Prim.Eq public + using () renaming (module Instances to EqInstances) +open import Haskell.Prim.Ord public + using () renaming (module Instances to OrdInstances) +open import Haskell.Prim.Num public + using () renaming (module Instances to NumInstances) +open import Haskell.Prim.Foldable public using (null; length; foldl; foldl'; foldl1; foldr; foldr1; sum; product; maximum; minimum; elem) + renaming (module Instances to FoldableInstances) open import Haskell.Data.Foldable public using (concat; concatMap; and; or; any; all; maximumBy; minimumBy; notElem; find) open import Haskell.Data.Traversable public using (mapAccumL; mapAccumR) diff --git a/lib/base/Haskell/Data/String.agda b/lib/base/Haskell/Data/String.agda index bb29fe51..d807e704 100644 --- a/lib/base/Haskell/Data/String.agda +++ b/lib/base/Haskell/Data/String.agda @@ -2,10 +2,12 @@ module Haskell.Data.String where open import Haskell.Prim open import Haskell.Prim.List -open import Haskell.Prim.Foldable +open import Haskell.Prim.Foldable hiding (module Instances) open import Haskell.Data.Foldable open import Haskell.Prim.String public +open import Haskell.Prim.Foldable public + using () renaming (module Instances to FoldableInstances) module Helpers where diff --git a/lib/base/Haskell/Data/Traversable.agda b/lib/base/Haskell/Data/Traversable.agda index 4e83c401..569f8623 100644 --- a/lib/base/Haskell/Data/Traversable.agda +++ b/lib/base/Haskell/Data/Traversable.agda @@ -1,12 +1,19 @@ module Haskell.Data.Traversable where open import Haskell.Prim hiding (s) -open import Haskell.Prim.Functor -open import Haskell.Prim.Applicative -open import Haskell.Prim.Monad open import Haskell.Prim.Tuple - +open import Haskell.Prim.Functor hiding (module Instances) +open import Haskell.Prim.Applicative hiding (module Instances) +open import Haskell.Prim.Monad hiding (module Instances) + +open import Haskell.Prim.Functor public + using () renaming (module Instances to FunctorInstances) +open import Haskell.Prim.Applicative public + using () renaming (module Instances to ApplicativeInstances) +open import Haskell.Prim.Monad public + using () renaming (module Instances to MonadInstances) open import Haskell.Prim.Traversable public + renaming (module Instances to TraversableInstances) private variable s : Type diff --git a/lib/base/Haskell/Law/Monoid/Def.agda b/lib/base/Haskell/Law/Monoid/Def.agda index 880d8e93..bf88e06e 100644 --- a/lib/base/Haskell/Law/Monoid/Def.agda +++ b/lib/base/Haskell/Law/Monoid/Def.agda @@ -4,7 +4,10 @@ open import Haskell.Prim open import Haskell.Prim.Tuple open import Haskell.Prim.Foldable +open import Haskell.Prim.Semigroup + renaming (module Instances to SemigroupInstances) open import Haskell.Prim.Monoid + renaming (module Instances to MonoidInstances) open import Haskell.Law.Semigroup.Def diff --git a/lib/base/Haskell/Law/Semigroup/Def.agda b/lib/base/Haskell/Law/Semigroup/Def.agda index d743fcee..34c54fdf 100644 --- a/lib/base/Haskell/Law/Semigroup/Def.agda +++ b/lib/base/Haskell/Law/Semigroup/Def.agda @@ -3,7 +3,7 @@ module Haskell.Law.Semigroup.Def where open import Haskell.Prim open import Haskell.Prim.Tuple -open import Haskell.Prim.Monoid +open import Haskell.Prim.Semigroup record IsLawfulSemigroup (a : Type) ⦃ iSemigroupA : Semigroup a ⦄ : Type₁ where field diff --git a/lib/base/Haskell/Law/Semigroup/Either.agda b/lib/base/Haskell/Law/Semigroup/Either.agda index 084f3926..7540e274 100644 --- a/lib/base/Haskell/Law/Semigroup/Either.agda +++ b/lib/base/Haskell/Law/Semigroup/Either.agda @@ -3,7 +3,7 @@ module Haskell.Law.Semigroup.Either where open import Haskell.Prim open import Haskell.Prim.Either -open import Haskell.Prim.Monoid +open import Haskell.Prim.Semigroup open import Haskell.Law.Equality open import Haskell.Law.Semigroup.Def diff --git a/lib/base/Haskell/Law/Semigroup/List.agda b/lib/base/Haskell/Law/Semigroup/List.agda index b5518bdb..53dcb1f2 100644 --- a/lib/base/Haskell/Law/Semigroup/List.agda +++ b/lib/base/Haskell/Law/Semigroup/List.agda @@ -3,7 +3,7 @@ module Haskell.Law.Semigroup.List where open import Haskell.Prim open import Haskell.Prim.List -open import Haskell.Prim.Monoid +open import Haskell.Prim.Semigroup open import Haskell.Law.Equality open import Haskell.Law.List diff --git a/lib/base/Haskell/Law/Semigroup/Maybe.agda b/lib/base/Haskell/Law/Semigroup/Maybe.agda index 7387d3a4..0757c634 100644 --- a/lib/base/Haskell/Law/Semigroup/Maybe.agda +++ b/lib/base/Haskell/Law/Semigroup/Maybe.agda @@ -3,7 +3,7 @@ module Haskell.Law.Semigroup.Maybe where open import Haskell.Prim open import Haskell.Prim.Maybe -open import Haskell.Prim.Monoid +open import Haskell.Prim.Semigroup open import Haskell.Law.Equality open import Haskell.Law.Semigroup.Def diff --git a/lib/base/Haskell/Prelude.agda b/lib/base/Haskell/Prelude.agda index 17023ade..710dfd8a 100644 --- a/lib/base/Haskell/Prelude.agda +++ b/lib/base/Haskell/Prelude.agda @@ -20,30 +20,45 @@ open import Haskell.Prim public open import Haskell.Prim.Absurd public open import Haskell.Prim.Bool public open import Haskell.Prim.Bounded public + renaming (module Instances to BoundedInstances) open import Haskell.Prim.Char public open import Haskell.Prim.Double public open import Haskell.Prim.Either public open import Haskell.Prim.Enum public -open import Haskell.Prim.Eq public + renaming (module Instances to EnumInstances) open import Haskell.Prim.Int public open import Haskell.Prim.Integer public open import Haskell.Prim.IO public hiding (returnIO; bindIO; failIO; mplusIO) open import Haskell.Prim.Maybe public -open import Haskell.Prim.Monoid public -open import Haskell.Prim.MonadFail public -open import Haskell.Prim.Num public -open import Haskell.Prim.Ord public -open import Haskell.Prim.Show public open import Haskell.Prim.Tuple public hiding (first; second; _***_) open import Haskell.Prim.Word public open import Haskell.Prim.String public +open import Haskell.Prim.Eq public + renaming (module Instances to EqInstances) +open import Haskell.Prim.Ord public + renaming (module Instances to OrdInstances) +open import Haskell.Prim.Num public + renaming (module Instances to NumInstances) +open import Haskell.Prim.Show public + renaming (module Instances to ShowInstances) +open import Haskell.Prim.Semigroup public + renaming (module Instances to SemigroupInstances) +open import Haskell.Prim.Monoid public + renaming (module Instances to MonoidInstances) open import Haskell.Prim.Functor public + renaming (module Instances to FunctorInstances) open import Haskell.Prim.Applicative public + renaming (module Instances to ApplicativeInstances) open import Haskell.Prim.Monad public -open import Haskell.Prim.Traversable public + renaming (module Instances to MonadInstances) +open import Haskell.Prim.MonadFail public + renaming (module Instances to MonadFailInstances) open import Haskell.Prim.Foldable public hiding (fold; foldMap'; foldr'; toList; null; length) + renaming (module Instances to FoldableInstances) +open import Haskell.Prim.Traversable public + renaming (module Instances to TraversableInstances) open import Haskell.Data.String public using (lines; words; unlines; unwords) diff --git a/lib/base/Haskell/Prim/Alternative.agda b/lib/base/Haskell/Prim/Alternative.agda index 5e43a49b..74f740d5 100644 --- a/lib/base/Haskell/Prim/Alternative.agda +++ b/lib/base/Haskell/Prim/Alternative.agda @@ -2,6 +2,7 @@ module Haskell.Prim.Alternative where open import Haskell.Prim open import Haskell.Prim.Applicative + renaming (module Instances to ApplicativeInstances) open import Haskell.Prim.IO open import Haskell.Prim.List open import Haskell.Prim.Maybe @@ -24,16 +25,18 @@ open Alternative ⦃...⦄ public {-# COMPILE AGDA2HS Alternative existing-class #-} -- ** instances -instance - iAlternativeList : Alternative List - iAlternativeList .empty = [] - iAlternativeList ._<|>_ = _++_ - - iAlternativeMaybe : Alternative Maybe - iAlternativeMaybe .empty = Nothing - iAlternativeMaybe ._<|>_ (Just x) _ = Just x - iAlternativeMaybe ._<|>_ Nothing y = y - - iAlternativeIO : Alternative IO - iAlternativeIO .empty = failIO "mzero" - iAlternativeIO ._<|>_ = mplusIO +module Instances where + instance + iAlternativeList : Alternative List + iAlternativeList .empty = [] + iAlternativeList ._<|>_ = _++_ + + iAlternativeMaybe : Alternative Maybe + iAlternativeMaybe .empty = Nothing + iAlternativeMaybe ._<|>_ (Just x) _ = Just x + iAlternativeMaybe ._<|>_ Nothing y = y + + iAlternativeIO : Alternative IO + iAlternativeIO .empty = failIO "mzero" + iAlternativeIO ._<|>_ = mplusIO +open Instances public diff --git a/lib/base/Haskell/Prim/Applicative.agda b/lib/base/Haskell/Prim/Applicative.agda index b7382423..9e4efccb 100644 --- a/lib/base/Haskell/Prim/Applicative.agda +++ b/lib/base/Haskell/Prim/Applicative.agda @@ -1,13 +1,18 @@ module Haskell.Prim.Applicative where open import Haskell.Prim -open import Haskell.Prim.Either -open import Haskell.Prim.Foldable +open import Haskell.Prim.Semigroup + renaming (module Instances to SemigroupInstances) +open import Haskell.Prim.Monoid + renaming (module Instances to MonoidInstances) open import Haskell.Prim.Functor + renaming (module Instances to FunctorInstances) +open import Haskell.Prim.Foldable + renaming (module Instances to FoldableInstances) +open import Haskell.Prim.Either open import Haskell.Prim.IO open import Haskell.Prim.List open import Haskell.Prim.Maybe -open import Haskell.Prim.Monoid open import Haskell.Prim.Tuple @@ -65,57 +70,59 @@ open Applicative ⦃...⦄ public {-# COMPILE AGDA2HS Applicative existing-class #-} -- ** instances -instance - open ApplicativeFrom<*> +module Instances where + instance + open ApplicativeFrom<*> - iDefaultApplicativeList : ApplicativeFrom<*> List - iDefaultApplicativeList .pure x = x ∷ [] - iDefaultApplicativeList ._<*>_ fs xs = foldMap (λ f → map f xs) fs + iDefaultApplicativeList : ApplicativeFrom<*> List + iDefaultApplicativeList .pure x = x ∷ [] + iDefaultApplicativeList ._<*>_ fs xs = foldMap (λ f → map f xs) fs - iApplicativeList : Applicative List - iApplicativeList = record {ApplicativeFrom<*> iDefaultApplicativeList} + iApplicativeList : Applicative List + iApplicativeList = record {ApplicativeFrom<*> iDefaultApplicativeList} - iDefaultApplicativeMaybe : ApplicativeFrom<*> Maybe - iDefaultApplicativeMaybe .pure = Just - iDefaultApplicativeMaybe ._<*>_ (Just f) (Just x) = Just (f x) - iDefaultApplicativeMaybe ._<*>_ _ _ = Nothing + iDefaultApplicativeMaybe : ApplicativeFrom<*> Maybe + iDefaultApplicativeMaybe .pure = Just + iDefaultApplicativeMaybe ._<*>_ (Just f) (Just x) = Just (f x) + iDefaultApplicativeMaybe ._<*>_ _ _ = Nothing - iApplicativeMaybe : Applicative Maybe - iApplicativeMaybe = record {ApplicativeFrom<*> iDefaultApplicativeMaybe} + iApplicativeMaybe : Applicative Maybe + iApplicativeMaybe = record {ApplicativeFrom<*> iDefaultApplicativeMaybe} - iDefaultApplicativeEither : ApplicativeFrom<*> (Either a) - iDefaultApplicativeEither .pure = Right - iDefaultApplicativeEither ._<*>_ (Right f) (Right x) = Right (f x) - iDefaultApplicativeEither ._<*>_ (Left e) _ = Left e - iDefaultApplicativeEither ._<*>_ _ (Left e) = Left e + iDefaultApplicativeEither : ApplicativeFrom<*> (Either a) + iDefaultApplicativeEither .pure = Right + iDefaultApplicativeEither ._<*>_ (Right f) (Right x) = Right (f x) + iDefaultApplicativeEither ._<*>_ (Left e) _ = Left e + iDefaultApplicativeEither ._<*>_ _ (Left e) = Left e - iApplicativeEither : Applicative (Either a) - iApplicativeEither = record{ApplicativeFrom<*> iDefaultApplicativeEither} + iApplicativeEither : Applicative (Either a) + iApplicativeEither = record{ApplicativeFrom<*> iDefaultApplicativeEither} - iDefaultApplicativeFun : ApplicativeFrom<*> (λ b → a → b) - iDefaultApplicativeFun .pure = const - iDefaultApplicativeFun ._<*>_ f g x = f x (g x) + iDefaultApplicativeFun : ApplicativeFrom<*> (λ b → a → b) + iDefaultApplicativeFun .pure = const + iDefaultApplicativeFun ._<*>_ f g x = f x (g x) - iApplicativeFun : Applicative (λ b → a → b) - iApplicativeFun = record{ApplicativeFrom<*> iDefaultApplicativeFun} + iApplicativeFun : Applicative (λ b → a → b) + iApplicativeFun = record{ApplicativeFrom<*> iDefaultApplicativeFun} - iDefaultApplicativeTuple₂ : ⦃ Monoid a ⦄ → ApplicativeFrom<*> (a ×_) - iDefaultApplicativeTuple₂ .pure x = mempty , x - iDefaultApplicativeTuple₂ ._<*>_ (a , f) (b , x) = a <> b , f x + iDefaultApplicativeTuple₂ : ⦃ Monoid a ⦄ → ApplicativeFrom<*> (a ×_) + iDefaultApplicativeTuple₂ .pure x = mempty , x + iDefaultApplicativeTuple₂ ._<*>_ (a , f) (b , x) = a <> b , f x - iApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_) - iApplicativeTuple₂ = record{ApplicativeFrom<*> iDefaultApplicativeTuple₂} + iApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_) + iApplicativeTuple₂ = record{ApplicativeFrom<*> iDefaultApplicativeTuple₂} - iDefaultApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ApplicativeFrom<*> (a × b ×_) - iDefaultApplicativeTuple₃ .pure x = mempty , mempty , x - iDefaultApplicativeTuple₃ ._<*>_ (a , u , f) (b , v , x) = a <> b , u <> v , f x + iDefaultApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ApplicativeFrom<*> (a × b ×_) + iDefaultApplicativeTuple₃ .pure x = mempty , mempty , x + iDefaultApplicativeTuple₃ ._<*>_ (a , u , f) (b , v , x) = a <> b , u <> v , f x - iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_) - iApplicativeTuple₃ = record{ApplicativeFrom<*> iDefaultApplicativeTuple₃} + iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_) + iApplicativeTuple₃ = record{ApplicativeFrom<*> iDefaultApplicativeTuple₃} - iDefaultApplicativeIO : ApplicativeFrom<*> IO - iDefaultApplicativeIO .pure = returnIO - iDefaultApplicativeIO ._<*>_ m1 m2 = bindIO m1 (λ f → bindIO m2 (λ x → returnIO (f x))) + iDefaultApplicativeIO : ApplicativeFrom<*> IO + iDefaultApplicativeIO .pure = returnIO + iDefaultApplicativeIO ._<*>_ m1 m2 = bindIO m1 (λ f → bindIO m2 (λ x → returnIO (f x))) - iApplicativeIO : Applicative IO - iApplicativeIO = record{ApplicativeFrom<*> iDefaultApplicativeIO} + iApplicativeIO : Applicative IO + iApplicativeIO = record{ApplicativeFrom<*> iDefaultApplicativeIO} +open Instances public diff --git a/lib/base/Haskell/Prim/Bounded.agda b/lib/base/Haskell/Prim/Bounded.agda index bd9ae0d5..515526a4 100644 --- a/lib/base/Haskell/Prim/Bounded.agda +++ b/lib/base/Haskell/Prim/Bounded.agda @@ -3,13 +3,16 @@ module Haskell.Prim.Bounded where open import Haskell.Prim open import Haskell.Prim.Eq + renaming (module Instances to EqInstances) +open import Haskell.Prim.Ord + renaming (module Instances to OrdInstances) open import Haskell.Prim.Int open import Haskell.Prim.Maybe -open import Haskell.Prim.Ord open import Haskell.Prim.Tuple open import Haskell.Prim.Word --------------------------------------------------- + +-------------------------------------------------------------------------------- -- Bounded record BoundedBelow (a : Type) : Type where @@ -30,59 +33,61 @@ record Bounded (a : Type) : Type where open BoundedBelow ⦃...⦄ public open BoundedAbove ⦃...⦄ public -instance - iBounded : ⦃ BoundedBelow a ⦄ → ⦃ BoundedAbove a ⦄ → Bounded a - iBounded .Bounded.below = it - iBounded .Bounded.above = it - -instance - iBoundedBelowNat : BoundedBelow Nat - iBoundedBelowNat .minBound = 0 - - iBoundedBelowWord : BoundedBelow Word - iBoundedBelowWord .minBound = 0 - iBoundedAboveWord : BoundedAbove Word - iBoundedAboveWord .maxBound = 18446744073709551615 - - iBoundedBelowInt : BoundedBelow Int - iBoundedBelowInt .minBound = -9223372036854775808 - iBoundedAboveInt : BoundedAbove Int - iBoundedAboveInt .maxBound = 9223372036854775807 - - iBoundedBelowBool : BoundedBelow Bool - iBoundedBelowBool .minBound = False - iBoundedAboveBool : BoundedAbove Bool - iBoundedAboveBool .maxBound = True - - iBoundedBelowChar : BoundedBelow Char - iBoundedBelowChar .minBound = '\0' - iBoundedAboveChar : BoundedAbove Char - iBoundedAboveChar .maxBound = '\1114111' - - iBoundedBelowUnit : BoundedBelow ⊤ - iBoundedBelowUnit .minBound = tt - - iBoundedAboveUnit : BoundedAbove ⊤ - iBoundedAboveUnit .maxBound = tt - - iBoundedBelowTuple₂ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄ - → BoundedBelow (a × b) - iBoundedBelowTuple₂ .minBound = minBound , minBound - iBoundedAboveTuple₂ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄ - → BoundedAbove (a × b) - iBoundedAboveTuple₂ .maxBound = maxBound , maxBound - - iBoundedBelowTuple₃ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄ → ⦃ BoundedBelow c ⦄ - → BoundedBelow (a × b × c) - iBoundedBelowTuple₃ .minBound = minBound , minBound , minBound - iBoundedAboveTuple₃ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄ → ⦃ BoundedAbove c ⦄ - → BoundedAbove (a × b × c) - iBoundedAboveTuple₃ .maxBound = maxBound , maxBound , maxBound - - iBoundedBelowOrdering : BoundedBelow Ordering - iBoundedBelowOrdering .minBound = LT - iBoundedAboveOrdering : BoundedAbove Ordering - iBoundedAboveOrdering .maxBound = GT +module Instances where + instance + iBounded : ⦃ BoundedBelow a ⦄ → ⦃ BoundedAbove a ⦄ → Bounded a + iBounded .Bounded.below = it + iBounded .Bounded.above = it + + instance + iBoundedBelowNat : BoundedBelow Nat + iBoundedBelowNat .minBound = 0 + + iBoundedBelowWord : BoundedBelow Word + iBoundedBelowWord .minBound = 0 + iBoundedAboveWord : BoundedAbove Word + iBoundedAboveWord .maxBound = 18446744073709551615 + + iBoundedBelowInt : BoundedBelow Int + iBoundedBelowInt .minBound = -9223372036854775808 + iBoundedAboveInt : BoundedAbove Int + iBoundedAboveInt .maxBound = 9223372036854775807 + + iBoundedBelowBool : BoundedBelow Bool + iBoundedBelowBool .minBound = False + iBoundedAboveBool : BoundedAbove Bool + iBoundedAboveBool .maxBound = True + + iBoundedBelowChar : BoundedBelow Char + iBoundedBelowChar .minBound = '\0' + iBoundedAboveChar : BoundedAbove Char + iBoundedAboveChar .maxBound = '\1114111' + + iBoundedBelowUnit : BoundedBelow ⊤ + iBoundedBelowUnit .minBound = tt + + iBoundedAboveUnit : BoundedAbove ⊤ + iBoundedAboveUnit .maxBound = tt + + iBoundedBelowTuple₂ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄ + → BoundedBelow (a × b) + iBoundedBelowTuple₂ .minBound = minBound , minBound + iBoundedAboveTuple₂ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄ + → BoundedAbove (a × b) + iBoundedAboveTuple₂ .maxBound = maxBound , maxBound + + iBoundedBelowTuple₃ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄ → ⦃ BoundedBelow c ⦄ + → BoundedBelow (a × b × c) + iBoundedBelowTuple₃ .minBound = minBound , minBound , minBound + iBoundedAboveTuple₃ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄ → ⦃ BoundedAbove c ⦄ + → BoundedAbove (a × b × c) + iBoundedAboveTuple₃ .maxBound = maxBound , maxBound , maxBound + + iBoundedBelowOrdering : BoundedBelow Ordering + iBoundedBelowOrdering .minBound = LT + iBoundedAboveOrdering : BoundedAbove Ordering + iBoundedAboveOrdering .maxBound = GT +open Instances public -- Sanity checks diff --git a/lib/base/Haskell/Prim/Enum.agda b/lib/base/Haskell/Prim/Enum.agda index 344d73af..a4ae3e62 100644 --- a/lib/base/Haskell/Prim/Enum.agda +++ b/lib/base/Haskell/Prim/Enum.agda @@ -2,22 +2,27 @@ module Haskell.Prim.Enum where open import Haskell.Prim -open import Haskell.Prim.Bool -open import Haskell.Prim.Bounded -open import Haskell.Prim.Either open import Haskell.Prim.Eq + renaming (module Instances to EqInstances) +open import Haskell.Prim.Ord + renaming (module Instances to OrdInstances) +open import Haskell.Prim.Num + renaming (module Instances to NumInstances) +open import Haskell.Prim.Bounded + renaming (module Instances to BoundedInstances) open import Haskell.Prim.Functor + renaming (module Instances to FunctorInstances) +open import Haskell.Prim.Bool +open import Haskell.Prim.Either open import Haskell.Prim.Int open import Haskell.Prim.Integer open import Haskell.Prim.List open import Haskell.Prim.Maybe -open import Haskell.Prim.Num -open import Haskell.Prim.Ord open import Haskell.Prim.Tuple open import Haskell.Prim.Word --------------------------------------------------- +-------------------------------------------------------------------------------- -- Enum -- Assumptions: unbounded enums have no constraints on their -- operations and bounded enums should work on all values between @@ -82,182 +87,184 @@ open Enum ⦃...⦄ public {-# COMPILE AGDA2HS Enum existing-class #-} -private - divNat : Nat → Nat → Nat - divNat a 0 = 0 - divNat a (suc b) = div-helper 0 b a b - - diff : Integer → Integer → Maybe Nat - diff a b = - case a - b of λ where - (pos n) → Just n - (negsuc _) → Nothing - - unsafeIntegerToNat : Integer → Nat - unsafeIntegerToNat (pos n) = n - unsafeIntegerToNat (negsuc _) = 0 - - integerFromCount : Integer → Integer → Nat → List Integer - integerFromCount a step 0 = [] - integerFromCount a step (suc n) = a ∷ integerFromCount (a + step) step n - - integerFromTo : Integer → Integer → List Integer - integerFromTo a b = maybe [] (integerFromCount a 1 ∘ suc) (diff b a) - - integerFromThenTo : (a a₁ : Integer) → @0 ⦃ IsFalse (integerToInt a == integerToInt a₁) ⦄ → Integer → List Integer - integerFromThenTo a a₁ b = - case compare a a₁ of λ where - LT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a₁ - a))))) (diff b a) - EQ → [] -- impossible - GT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a - a₁))))) (diff a b) - -instance - iEnumInteger : Enum Integer - iEnumInteger .BoundedBelowEnum = Nothing - iEnumInteger .BoundedAboveEnum = Nothing - iEnumInteger .fromEnum = integerToInt - iEnumInteger .toEnum n = intToInteger n - iEnumInteger .succ = _+ 1 - iEnumInteger .pred = _- 1 - iEnumInteger .enumFromTo = integerFromTo - iEnumInteger .enumFromThenTo = integerFromThenTo - -private - fromTo : (from : a → Integer) (to : Integer → a) - → a → a → List a - fromTo from to a b = map to (enumFromTo (from a) (from b)) - - fromThenTo : (from : a → Integer) (to : Integer → a) - → (x x₁ : a) → @0 ⦃ IsFalse (fromEnum (from x) == fromEnum (from x₁)) ⦄ → a → List a - fromThenTo from to a a₁ b = map to (enumFromThenTo (from a) (from a₁) (from b)) - - -instance - iEnumNat : Enum Nat - iEnumNat .BoundedBelowEnum = Just it - iEnumNat .BoundedAboveEnum = Nothing - iEnumNat .fromEnum = integerToInt ∘ pos - iEnumNat .toEnum n = unsafeIntegerToNat (intToInteger n) - iEnumNat .succ n = suc n - iEnumNat .pred (suc n) = n - iEnumNat .enumFromTo = fromTo pos unsafeIntegerToNat - iEnumNat .enumFromThenTo = fromThenTo pos unsafeIntegerToNat - - iEnumInt : Enum Int - iEnumInt .BoundedBelowEnum = Just it - iEnumInt .BoundedAboveEnum = Just it - iEnumInt .fromEnum = integerToInt ∘ intToInteger - iEnumInt .toEnum n = integerToInt (intToInteger n) - iEnumInt .succ x = integerToInt (intToInteger x + 1) - iEnumInt .pred x = integerToInt (intToInteger x - 1) - iEnumInt .enumFromTo a b = fromTo intToInteger integerToInt a b - iEnumInt .enumFromThenTo a a₁ b = fromThenTo intToInteger integerToInt a a₁ b - iEnumInt .enumFrom a = fromTo intToInteger integerToInt a maxBound - iEnumInt .enumFromThen a a₁ = - if a < a₁ then fromThenTo intToInteger integerToInt a a₁ maxBound - else fromThenTo intToInteger integerToInt a a₁ minBound - - iEnumWord : Enum Word - iEnumWord .BoundedBelowEnum = Just it - iEnumWord .BoundedAboveEnum = Just it - iEnumWord .fromEnum = integerToInt ∘ wordToInteger - iEnumWord .toEnum n = integerToWord (intToInteger n) - iEnumWord .succ x = integerToWord (wordToInteger x + 1) - iEnumWord .pred x = integerToWord (wordToInteger x - 1) - iEnumWord .enumFromTo a b = fromTo wordToInteger integerToWord a b - iEnumWord .enumFromThenTo a a₁ b = fromThenTo wordToInteger integerToWord a a₁ b - iEnumWord .enumFrom a = fromTo wordToInteger integerToWord a maxBound - iEnumWord .enumFromThen a a₁ = - if a < a₁ then fromThenTo wordToInteger integerToWord a a₁ maxBound - else fromThenTo wordToInteger integerToWord a a₁ minBound - -private - fromBool : Bool → Integer - fromBool = if_then 1 else 0 - - toBool : Integer → Bool - toBool = _/= 0 - -instance - iEnumBool : Enum Bool - iEnumBool .BoundedBelowEnum = Just it - iEnumBool .BoundedAboveEnum = Just it - iEnumBool .fromEnum = integerToInt ∘ fromBool - iEnumBool .toEnum n = toBool (intToInteger n) - iEnumBool .succ x = toBool (fromBool x + 1) - iEnumBool .pred x = toBool (fromBool x - 1) - iEnumBool .enumFromTo a b = fromTo fromBool toBool a b - iEnumBool .enumFromThenTo a a₁ b = fromThenTo fromBool toBool a a₁ b - iEnumBool .enumFrom a = fromTo fromBool toBool a maxBound - iEnumBool .enumFromThen a a₁ = - if a < a₁ then fromThenTo fromBool toBool a a₁ maxBound - else fromThenTo fromBool toBool a a₁ minBound - -private - fromOrdering : Ordering → Integer - fromOrdering = λ where LT → 0; EQ → 1; GT → 2 - - toOrdering : Integer → Ordering - toOrdering = λ where (pos 0) → LT; (pos 1) → EQ; _ → GT - -instance - iEnumOrdering : Enum Ordering - iEnumOrdering .BoundedBelowEnum = Just it - iEnumOrdering .BoundedAboveEnum = Just it - iEnumOrdering .fromEnum = integerToInt ∘ fromOrdering - iEnumOrdering .toEnum n = toOrdering (intToInteger n) - iEnumOrdering .succ x = toOrdering (fromOrdering x + 1) - iEnumOrdering .pred x = toOrdering (fromOrdering x - 1) - iEnumOrdering .enumFromTo a b = fromTo fromOrdering toOrdering a b - iEnumOrdering .enumFromThenTo a a₁ b = fromThenTo fromOrdering toOrdering a a₁ b - iEnumOrdering .enumFrom a = fromTo fromOrdering toOrdering a maxBound - iEnumOrdering .enumFromThen a a₁ = - if a < a₁ then fromThenTo fromOrdering toOrdering a a₁ maxBound - else fromThenTo fromOrdering toOrdering a a₁ minBound - -private - fromUnit : ⊤ → Integer - fromUnit _ = 0 - - toUnit : Integer → ⊤ - toUnit _ = tt - -instance - iEnumUnit : Enum ⊤ - iEnumUnit .BoundedBelowEnum = Just it - iEnumUnit .BoundedAboveEnum = Just it - iEnumUnit .fromEnum = integerToInt ∘ fromUnit - iEnumUnit .toEnum n = toUnit (intToInteger n) - iEnumUnit .succ x = toUnit (fromUnit x + 1) - iEnumUnit .pred x = toUnit (fromUnit x - 1) - iEnumUnit .enumFromTo a b = fromTo fromUnit toUnit a b - iEnumUnit .enumFromThenTo a a₁ b = fromThenTo fromUnit toUnit a a₁ b - iEnumUnit .enumFrom a = fromTo fromUnit toUnit a maxBound - iEnumUnit .enumFromThen a a₁ = - if a < a₁ then fromThenTo fromUnit toUnit a a₁ maxBound - else fromThenTo fromUnit toUnit a a₁ minBound - -private - fromChar : Char → Integer - fromChar = pos ∘ c2n - - toChar : Integer → Char - toChar = λ where (pos n) → primNatToChar n; _ → '_' - -instance - iEnumChar : Enum Char - iEnumChar .BoundedBelowEnum = Just it - iEnumChar .BoundedAboveEnum = Just it - iEnumChar .fromEnum = integerToInt ∘ fromChar - iEnumChar .toEnum n = toChar (intToInteger n) - iEnumChar .succ x = toChar (fromChar x + 1) - iEnumChar .pred x = toChar (fromChar x - 1) - iEnumChar .enumFromTo a b = fromTo fromChar toChar a b - iEnumChar .enumFromThenTo a a₁ b = fromThenTo fromChar toChar a a₁ b - iEnumChar .enumFrom a = fromTo fromChar toChar a maxBound - iEnumChar .enumFromThen a a₁ = - if a < a₁ then fromThenTo fromChar toChar a a₁ maxBound - else fromThenTo fromChar toChar a a₁ minBound - - -- Missing: - -- Enum Double (can't go via Integer) +module Instances where + private + divNat : Nat → Nat → Nat + divNat a 0 = 0 + divNat a (suc b) = div-helper 0 b a b + + diff : Integer → Integer → Maybe Nat + diff a b = + case a - b of λ where + (pos n) → Just n + (negsuc _) → Nothing + + unsafeIntegerToNat : Integer → Nat + unsafeIntegerToNat (pos n) = n + unsafeIntegerToNat (negsuc _) = 0 + + integerFromCount : Integer → Integer → Nat → List Integer + integerFromCount a step 0 = [] + integerFromCount a step (suc n) = a ∷ integerFromCount (a + step) step n + + integerFromTo : Integer → Integer → List Integer + integerFromTo a b = maybe [] (integerFromCount a 1 ∘ suc) (diff b a) + + integerFromThenTo : (a a₁ : Integer) → @0 ⦃ IsFalse (integerToInt a == integerToInt a₁) ⦄ → Integer → List Integer + integerFromThenTo a a₁ b = + case compare a a₁ of λ where + LT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a₁ - a))))) (diff b a) + EQ → [] -- impossible + GT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a - a₁))))) (diff a b) + + instance + iEnumInteger : Enum Integer + iEnumInteger .BoundedBelowEnum = Nothing + iEnumInteger .BoundedAboveEnum = Nothing + iEnumInteger .fromEnum = integerToInt + iEnumInteger .toEnum n = intToInteger n + iEnumInteger .succ = _+ 1 + iEnumInteger .pred = _- 1 + iEnumInteger .enumFromTo = integerFromTo + iEnumInteger .enumFromThenTo = integerFromThenTo + + private + fromTo : (from : a → Integer) (to : Integer → a) + → a → a → List a + fromTo from to a b = map to (enumFromTo (from a) (from b)) + + fromThenTo : (from : a → Integer) (to : Integer → a) + → (x x₁ : a) → @0 ⦃ IsFalse (fromEnum (from x) == fromEnum (from x₁)) ⦄ → a → List a + fromThenTo from to a a₁ b = map to (enumFromThenTo (from a) (from a₁) (from b)) + + + instance + iEnumNat : Enum Nat + iEnumNat .BoundedBelowEnum = Just it + iEnumNat .BoundedAboveEnum = Nothing + iEnumNat .fromEnum = integerToInt ∘ pos + iEnumNat .toEnum n = unsafeIntegerToNat (intToInteger n) + iEnumNat .succ n = suc n + iEnumNat .pred (suc n) = n + iEnumNat .enumFromTo = fromTo pos unsafeIntegerToNat + iEnumNat .enumFromThenTo = fromThenTo pos unsafeIntegerToNat + + iEnumInt : Enum Int + iEnumInt .BoundedBelowEnum = Just it + iEnumInt .BoundedAboveEnum = Just it + iEnumInt .fromEnum = integerToInt ∘ intToInteger + iEnumInt .toEnum n = integerToInt (intToInteger n) + iEnumInt .succ x = integerToInt (intToInteger x + 1) + iEnumInt .pred x = integerToInt (intToInteger x - 1) + iEnumInt .enumFromTo a b = fromTo intToInteger integerToInt a b + iEnumInt .enumFromThenTo a a₁ b = fromThenTo intToInteger integerToInt a a₁ b + iEnumInt .enumFrom a = fromTo intToInteger integerToInt a maxBound + iEnumInt .enumFromThen a a₁ = + if a < a₁ then fromThenTo intToInteger integerToInt a a₁ maxBound + else fromThenTo intToInteger integerToInt a a₁ minBound + + iEnumWord : Enum Word + iEnumWord .BoundedBelowEnum = Just it + iEnumWord .BoundedAboveEnum = Just it + iEnumWord .fromEnum = integerToInt ∘ wordToInteger + iEnumWord .toEnum n = integerToWord (intToInteger n) + iEnumWord .succ x = integerToWord (wordToInteger x + 1) + iEnumWord .pred x = integerToWord (wordToInteger x - 1) + iEnumWord .enumFromTo a b = fromTo wordToInteger integerToWord a b + iEnumWord .enumFromThenTo a a₁ b = fromThenTo wordToInteger integerToWord a a₁ b + iEnumWord .enumFrom a = fromTo wordToInteger integerToWord a maxBound + iEnumWord .enumFromThen a a₁ = + if a < a₁ then fromThenTo wordToInteger integerToWord a a₁ maxBound + else fromThenTo wordToInteger integerToWord a a₁ minBound + + private + fromBool : Bool → Integer + fromBool = if_then 1 else 0 + + toBool : Integer → Bool + toBool = _/= 0 + + instance + iEnumBool : Enum Bool + iEnumBool .BoundedBelowEnum = Just it + iEnumBool .BoundedAboveEnum = Just it + iEnumBool .fromEnum = integerToInt ∘ fromBool + iEnumBool .toEnum n = toBool (intToInteger n) + iEnumBool .succ x = toBool (fromBool x + 1) + iEnumBool .pred x = toBool (fromBool x - 1) + iEnumBool .enumFromTo a b = fromTo fromBool toBool a b + iEnumBool .enumFromThenTo a a₁ b = fromThenTo fromBool toBool a a₁ b + iEnumBool .enumFrom a = fromTo fromBool toBool a maxBound + iEnumBool .enumFromThen a a₁ = + if a < a₁ then fromThenTo fromBool toBool a a₁ maxBound + else fromThenTo fromBool toBool a a₁ minBound + + private + fromOrdering : Ordering → Integer + fromOrdering = λ where LT → 0; EQ → 1; GT → 2 + + toOrdering : Integer → Ordering + toOrdering = λ where (pos 0) → LT; (pos 1) → EQ; _ → GT + + instance + iEnumOrdering : Enum Ordering + iEnumOrdering .BoundedBelowEnum = Just it + iEnumOrdering .BoundedAboveEnum = Just it + iEnumOrdering .fromEnum = integerToInt ∘ fromOrdering + iEnumOrdering .toEnum n = toOrdering (intToInteger n) + iEnumOrdering .succ x = toOrdering (fromOrdering x + 1) + iEnumOrdering .pred x = toOrdering (fromOrdering x - 1) + iEnumOrdering .enumFromTo a b = fromTo fromOrdering toOrdering a b + iEnumOrdering .enumFromThenTo a a₁ b = fromThenTo fromOrdering toOrdering a a₁ b + iEnumOrdering .enumFrom a = fromTo fromOrdering toOrdering a maxBound + iEnumOrdering .enumFromThen a a₁ = + if a < a₁ then fromThenTo fromOrdering toOrdering a a₁ maxBound + else fromThenTo fromOrdering toOrdering a a₁ minBound + + private + fromUnit : ⊤ → Integer + fromUnit _ = 0 + + toUnit : Integer → ⊤ + toUnit _ = tt + + instance + iEnumUnit : Enum ⊤ + iEnumUnit .BoundedBelowEnum = Just it + iEnumUnit .BoundedAboveEnum = Just it + iEnumUnit .fromEnum = integerToInt ∘ fromUnit + iEnumUnit .toEnum n = toUnit (intToInteger n) + iEnumUnit .succ x = toUnit (fromUnit x + 1) + iEnumUnit .pred x = toUnit (fromUnit x - 1) + iEnumUnit .enumFromTo a b = fromTo fromUnit toUnit a b + iEnumUnit .enumFromThenTo a a₁ b = fromThenTo fromUnit toUnit a a₁ b + iEnumUnit .enumFrom a = fromTo fromUnit toUnit a maxBound + iEnumUnit .enumFromThen a a₁ = + if a < a₁ then fromThenTo fromUnit toUnit a a₁ maxBound + else fromThenTo fromUnit toUnit a a₁ minBound + + private + fromChar : Char → Integer + fromChar = pos ∘ c2n + + toChar : Integer → Char + toChar = λ where (pos n) → primNatToChar n; _ → '_' + + instance + iEnumChar : Enum Char + iEnumChar .BoundedBelowEnum = Just it + iEnumChar .BoundedAboveEnum = Just it + iEnumChar .fromEnum = integerToInt ∘ fromChar + iEnumChar .toEnum n = toChar (intToInteger n) + iEnumChar .succ x = toChar (fromChar x + 1) + iEnumChar .pred x = toChar (fromChar x - 1) + iEnumChar .enumFromTo a b = fromTo fromChar toChar a b + iEnumChar .enumFromThenTo a a₁ b = fromThenTo fromChar toChar a a₁ b + iEnumChar .enumFrom a = fromTo fromChar toChar a maxBound + iEnumChar .enumFromThen a a₁ = + if a < a₁ then fromThenTo fromChar toChar a a₁ maxBound + else fromThenTo fromChar toChar a a₁ minBound + + -- Missing: + -- Enum Double (can't go via Integer) +open Instances public diff --git a/lib/base/Haskell/Prim/Eq.agda b/lib/base/Haskell/Prim/Eq.agda index 4f844c75..54e61d50 100644 --- a/lib/base/Haskell/Prim/Eq.agda +++ b/lib/base/Haskell/Prim/Eq.agda @@ -12,7 +12,8 @@ open import Haskell.Prim.Tuple open import Haskell.Prim.Maybe open import Haskell.Prim.Either --------------------------------------------------- + +-------------------------------------------------------------------------------- -- Eq record Eq (a : Type) : Type where @@ -29,54 +30,56 @@ x /= y = not (x == y) infix 4 _/=_ -instance - iEqNat : Eq Nat - iEqNat ._==_ = eqNat +module Instances where + instance + iEqNat : Eq Nat + iEqNat ._==_ = eqNat - iEqInteger : Eq Integer - iEqInteger ._==_ = eqInteger + iEqInteger : Eq Integer + iEqInteger ._==_ = eqInteger - iEqInt : Eq Int - iEqInt ._==_ = eqInt + iEqInt : Eq Int + iEqInt ._==_ = eqInt - iEqWord : Eq Word - iEqWord ._==_ = eqWord + iEqWord : Eq Word + iEqWord ._==_ = eqWord - iEqDouble : Eq Double - iEqDouble ._==_ = primFloatEquality + iEqDouble : Eq Double + iEqDouble ._==_ = primFloatEquality - iEqBool : Eq Bool - iEqBool ._==_ False False = True - iEqBool ._==_ True True = True - iEqBool ._==_ _ _ = False + iEqBool : Eq Bool + iEqBool ._==_ False False = True + iEqBool ._==_ True True = True + iEqBool ._==_ _ _ = False - iEqChar : Eq Char - iEqChar ._==_ = eqChar + iEqChar : Eq Char + iEqChar ._==_ = eqChar - iEqUnit : Eq ⊤ - iEqUnit ._==_ _ _ = True + iEqUnit : Eq ⊤ + iEqUnit ._==_ _ _ = True - iEqTuple₂ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (a × b) - iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₁ == y₂ + iEqTuple₂ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (a × b) + iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₁ == y₂ - iEqTuple₃ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → ⦃ Eq c ⦄ → Eq (a × b × c) - iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₁ == y₂ && z₁ == z₂ + iEqTuple₃ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → ⦃ Eq c ⦄ → Eq (a × b × c) + iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₁ == y₂ && z₁ == z₂ - iEqList : ⦃ Eq a ⦄ → Eq (List a) - iEqList {a} ._==_ = eqList - where - eqList : List a → List a → Bool - eqList [] [] = True - eqList (x ∷ xs) (y ∷ ys) = x == y && eqList xs ys - eqList _ _ = False + iEqList : ⦃ Eq a ⦄ → Eq (List a) + iEqList {a} ._==_ = eqList + where + eqList : List a → List a → Bool + eqList [] [] = True + eqList (x ∷ xs) (y ∷ ys) = x == y && eqList xs ys + eqList _ _ = False - iEqMaybe : ⦃ Eq a ⦄ → Eq (Maybe a) - iEqMaybe ._==_ Nothing Nothing = True - iEqMaybe ._==_ (Just x) (Just y) = x == y - iEqMaybe ._==_ _ _ = False + iEqMaybe : ⦃ Eq a ⦄ → Eq (Maybe a) + iEqMaybe ._==_ Nothing Nothing = True + iEqMaybe ._==_ (Just x) (Just y) = x == y + iEqMaybe ._==_ _ _ = False - iEqEither : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (Either a b) - iEqEither ._==_ (Left x) (Left y) = x == y - iEqEither ._==_ (Right x) (Right y) = x == y - iEqEither ._==_ _ _ = False + iEqEither : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (Either a b) + iEqEither ._==_ (Left x) (Left y) = x == y + iEqEither ._==_ (Right x) (Right y) = x == y + iEqEither ._==_ _ _ = False +open Instances public diff --git a/lib/base/Haskell/Prim/Foldable.agda b/lib/base/Haskell/Prim/Foldable.agda index bab4482b..b91f9474 100644 --- a/lib/base/Haskell/Prim/Foldable.agda +++ b/lib/base/Haskell/Prim/Foldable.agda @@ -1,16 +1,22 @@ module Haskell.Prim.Foldable where open import Haskell.Prim -open import Haskell.Prim.Num hiding (abs) +open import Haskell.Prim.Num + hiding (abs) renaming (module Instances to NumInstances) open import Haskell.Prim.Eq + renaming (module Instances to EqInstances) open import Haskell.Prim.Ord + renaming (module Instances to OrdInstances) +open import Haskell.Prim.Semigroup + renaming (module Instances to SemigroupInstances) +open import Haskell.Prim.Monoid + renaming (module Instances to MonoidInstances) open import Haskell.Prim.List open import Haskell.Prim.Int open import Haskell.Prim.Bool open import Haskell.Prim.Maybe open import Haskell.Prim.Either open import Haskell.Prim.Tuple -open import Haskell.Prim.Monoid -------------------------------------------------------------------------------- @@ -107,37 +113,39 @@ open Foldable ⦃...⦄ public {-# COMPILE AGDA2HS Foldable existing-class #-} -- ** instances -instance - open DefaultFoldable - - iDefaultFoldableList : DefaultFoldable List - iDefaultFoldableList .foldMap = foldMapList - where - foldMapList : ⦃ Monoid b ⦄ → (a → b) → List a → b - foldMapList f [] = mempty - foldMapList f (x ∷ xs) = f x <> foldMapList f xs - - iFoldableList : Foldable List - iFoldableList = record {DefaultFoldable iDefaultFoldableList} - - iDefaultFoldableMaybe : DefaultFoldable Maybe - iDefaultFoldableMaybe .foldMap = λ where - _ Nothing → mempty - f (Just x) → f x - - iFoldableMaybe : Foldable Maybe - iFoldableMaybe = record {DefaultFoldable iDefaultFoldableMaybe} - - iDefaultFoldableEither : DefaultFoldable (Either a) - iDefaultFoldableEither .foldMap = λ where - _ (Left _) → mempty - f (Right x) → f x - - iFoldableEither : Foldable (Either a) - iFoldableEither = record {DefaultFoldable iDefaultFoldableEither} - - iDefaultFoldablePair : DefaultFoldable (a ×_) - iDefaultFoldablePair .foldMap = λ f (_ , x) → f x - - iFoldablePair : Foldable (a ×_) - iFoldablePair = record {DefaultFoldable iDefaultFoldablePair} +module Instances where + instance + open DefaultFoldable + + iDefaultFoldableList : DefaultFoldable List + iDefaultFoldableList .foldMap = foldMapList + where + foldMapList : ⦃ Monoid b ⦄ → (a → b) → List a → b + foldMapList f [] = mempty + foldMapList f (x ∷ xs) = f x <> foldMapList f xs + + iFoldableList : Foldable List + iFoldableList = record {DefaultFoldable iDefaultFoldableList} + + iDefaultFoldableMaybe : DefaultFoldable Maybe + iDefaultFoldableMaybe .foldMap = λ where + _ Nothing → mempty + f (Just x) → f x + + iFoldableMaybe : Foldable Maybe + iFoldableMaybe = record {DefaultFoldable iDefaultFoldableMaybe} + + iDefaultFoldableEither : DefaultFoldable (Either a) + iDefaultFoldableEither .foldMap = λ where + _ (Left _) → mempty + f (Right x) → f x + + iFoldableEither : Foldable (Either a) + iFoldableEither = record {DefaultFoldable iDefaultFoldableEither} + + iDefaultFoldablePair : DefaultFoldable (a ×_) + iDefaultFoldablePair .foldMap = λ f (_ , x) → f x + + iFoldablePair : Foldable (a ×_) + iFoldablePair = record {DefaultFoldable iDefaultFoldablePair} +open Instances public diff --git a/lib/base/Haskell/Prim/Functor.agda b/lib/base/Haskell/Prim/Functor.agda index 25dcc045..4df971d2 100644 --- a/lib/base/Haskell/Prim/Functor.agda +++ b/lib/base/Haskell/Prim/Functor.agda @@ -32,51 +32,53 @@ open Functor ⦃...⦄ public {-# COMPILE AGDA2HS Functor existing-class #-} -- ** instances -instance - open DefaultFunctor +module Instances where + instance + open DefaultFunctor - iDefaultFunctorList : DefaultFunctor List - iDefaultFunctorList .fmap = map + iDefaultFunctorList : DefaultFunctor List + iDefaultFunctorList .fmap = map - iFunctorList : Functor List - iFunctorList = record{DefaultFunctor iDefaultFunctorList} + iFunctorList : Functor List + iFunctorList = record{DefaultFunctor iDefaultFunctorList} - iDefaultFunctorMaybe : DefaultFunctor Maybe - iDefaultFunctorMaybe .fmap = λ where - f Nothing → Nothing - f (Just x) → Just (f x) + iDefaultFunctorMaybe : DefaultFunctor Maybe + iDefaultFunctorMaybe .fmap = λ where + f Nothing → Nothing + f (Just x) → Just (f x) - iFunctorMaybe : Functor Maybe - iFunctorMaybe = record{DefaultFunctor iDefaultFunctorMaybe} + iFunctorMaybe : Functor Maybe + iFunctorMaybe = record{DefaultFunctor iDefaultFunctorMaybe} - iDefaultFunctorEither : DefaultFunctor (Either a) - iDefaultFunctorEither .fmap = λ where - f (Left x) → Left x - f (Right y) → Right (f y) + iDefaultFunctorEither : DefaultFunctor (Either a) + iDefaultFunctorEither .fmap = λ where + f (Left x) → Left x + f (Right y) → Right (f y) - iFunctorEither : Functor (Either a) - iFunctorEither = record{DefaultFunctor iDefaultFunctorEither} + iFunctorEither : Functor (Either a) + iFunctorEither = record{DefaultFunctor iDefaultFunctorEither} - iDefaultFunctorFun : DefaultFunctor (λ b → a → b) - iDefaultFunctorFun .fmap = _∘_ + iDefaultFunctorFun : DefaultFunctor (λ b → a → b) + iDefaultFunctorFun .fmap = _∘_ - iFunctorFun : Functor (λ b → a → b) - iFunctorFun = record{DefaultFunctor iDefaultFunctorFun} + iFunctorFun : Functor (λ b → a → b) + iFunctorFun = record{DefaultFunctor iDefaultFunctorFun} - iDefaultFunctorTuple₂ : DefaultFunctor (a ×_) - iDefaultFunctorTuple₂ .fmap = λ f (x , y) → x , f y + iDefaultFunctorTuple₂ : DefaultFunctor (a ×_) + iDefaultFunctorTuple₂ .fmap = λ f (x , y) → x , f y - iFunctorTuple₂ : Functor (a ×_) - iFunctorTuple₂ = record{DefaultFunctor iDefaultFunctorTuple₂} + iFunctorTuple₂ : Functor (a ×_) + iFunctorTuple₂ = record{DefaultFunctor iDefaultFunctorTuple₂} - iDefaultFunctorTuple₃ : DefaultFunctor (a × b ×_) - iDefaultFunctorTuple₃ .fmap = λ where f (x , y , z) → x , y , f z + iDefaultFunctorTuple₃ : DefaultFunctor (a × b ×_) + iDefaultFunctorTuple₃ .fmap = λ where f (x , y , z) → x , y , f z - iFunctorTuple₃ : Functor (a × b ×_) - iFunctorTuple₃ = record{DefaultFunctor iDefaultFunctorTuple₃} + iFunctorTuple₃ : Functor (a × b ×_) + iFunctorTuple₃ = record{DefaultFunctor iDefaultFunctorTuple₃} - iDefaultFunctorIO : DefaultFunctor IO - iDefaultFunctorIO .fmap = λ f x → bindIO x (returnIO ∘ f) + iDefaultFunctorIO : DefaultFunctor IO + iDefaultFunctorIO .fmap = λ f x → bindIO x (returnIO ∘ f) - iFunctorIO : Functor IO - iFunctorIO = record{DefaultFunctor iDefaultFunctorIO} + iFunctorIO : Functor IO + iFunctorIO = record{DefaultFunctor iDefaultFunctorIO} +open Instances public diff --git a/lib/base/Haskell/Prim/Monad.agda b/lib/base/Haskell/Prim/Monad.agda index 84f1b3b9..88357014 100644 --- a/lib/base/Haskell/Prim/Monad.agda +++ b/lib/base/Haskell/Prim/Monad.agda @@ -1,14 +1,20 @@ module Haskell.Prim.Monad where open import Haskell.Prim +open import Haskell.Prim.Semigroup + renaming (module Instances to SemigroupInstances) +open import Haskell.Prim.Monoid + renaming (module Instances to MonoidInstances) +open import Haskell.Prim.Functor + renaming (module Instances to FunctorInstances) open import Haskell.Prim.Applicative -open import Haskell.Prim.Either + renaming (module Instances to ApplicativeInstances) open import Haskell.Prim.Foldable -open import Haskell.Prim.Functor + renaming (module Instances to FoldableInstances) +open import Haskell.Prim.Either open import Haskell.Prim.IO open import Haskell.Prim.List open import Haskell.Prim.Maybe -open import Haskell.Prim.Monoid open import Haskell.Prim.Tuple @@ -55,49 +61,51 @@ module Dont where open Do public -- ** instances -instance - open DefaultMonad +module Instances where + instance + open DefaultMonad - iDefaultMonadList : DefaultMonad List - iDefaultMonadList ._>>=_ = flip foldMap + iDefaultMonadList : DefaultMonad List + iDefaultMonadList ._>>=_ = flip foldMap - iMonadList : Monad List - iMonadList = record {DefaultMonad iDefaultMonadList} + iMonadList : Monad List + iMonadList = record {DefaultMonad iDefaultMonadList} - iDefaultMonadMaybe : DefaultMonad Maybe - iDefaultMonadMaybe ._>>=_ = flip (maybe Nothing) + iDefaultMonadMaybe : DefaultMonad Maybe + iDefaultMonadMaybe ._>>=_ = flip (maybe Nothing) - iMonadMaybe : Monad Maybe - iMonadMaybe = record {DefaultMonad iDefaultMonadMaybe} + iMonadMaybe : Monad Maybe + iMonadMaybe = record {DefaultMonad iDefaultMonadMaybe} - iDefaultMonadEither : DefaultMonad (Either a) - iDefaultMonadEither ._>>=_ = flip (either Left) + iDefaultMonadEither : DefaultMonad (Either a) + iDefaultMonadEither ._>>=_ = flip (either Left) - iMonadEither : Monad (Either a) - iMonadEither = record {DefaultMonad iDefaultMonadEither} + iMonadEither : Monad (Either a) + iMonadEither = record {DefaultMonad iDefaultMonadEither} - iDefaultMonadFun : DefaultMonad (λ b → a → b) - iDefaultMonadFun ._>>=_ = λ f k r → k (f r) r + iDefaultMonadFun : DefaultMonad (λ b → a → b) + iDefaultMonadFun ._>>=_ = λ f k r → k (f r) r - iMonadFun : Monad (λ b → a → b) - iMonadFun = record {DefaultMonad iDefaultMonadFun} + iMonadFun : Monad (λ b → a → b) + iMonadFun = record {DefaultMonad iDefaultMonadFun} - iDefaultMonadTuple₂ : ⦃ Monoid a ⦄ → DefaultMonad (a ×_) - iDefaultMonadTuple₂ ._>>=_ = λ (a , x) k → first (a <>_) (k x) + iDefaultMonadTuple₂ : ⦃ Monoid a ⦄ → DefaultMonad (a ×_) + iDefaultMonadTuple₂ ._>>=_ = λ (a , x) k → first (a <>_) (k x) - iMonadTuple₂ : ⦃ Monoid a ⦄ → Monad (a ×_) - iMonadTuple₂ = record {DefaultMonad iDefaultMonadTuple₂} + iMonadTuple₂ : ⦃ Monoid a ⦄ → Monad (a ×_) + iMonadTuple₂ = record {DefaultMonad iDefaultMonadTuple₂} - iDefaultMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonad (a × b ×_) - iDefaultMonadTuple₃ ._>>=_ = λ where - (a , b , x) k → case k x of λ where - (a₁ , b₁ , y) → a <> a₁ , b <> b₁ , y + iDefaultMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonad (a × b ×_) + iDefaultMonadTuple₃ ._>>=_ = λ where + (a , b , x) k → case k x of λ where + (a₁ , b₁ , y) → a <> a₁ , b <> b₁ , y - iMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_) - iMonadTuple₃ = record {DefaultMonad iDefaultMonadTuple₃} + iMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_) + iMonadTuple₃ = record {DefaultMonad iDefaultMonadTuple₃} - iDefaultMonadIO : DefaultMonad IO - iDefaultMonadIO ._>>=_ = bindIO + iDefaultMonadIO : DefaultMonad IO + iDefaultMonadIO ._>>=_ = bindIO - iMonadIO : Monad IO - iMonadIO = record {DefaultMonad iDefaultMonadIO} + iMonadIO : Monad IO + iMonadIO = record {DefaultMonad iDefaultMonadIO} +open Instances public diff --git a/lib/base/Haskell/Prim/MonadFail.agda b/lib/base/Haskell/Prim/MonadFail.agda index 00c26b75..293ab9a4 100644 --- a/lib/base/Haskell/Prim/MonadFail.agda +++ b/lib/base/Haskell/Prim/MonadFail.agda @@ -1,8 +1,9 @@ module Haskell.Prim.MonadFail where open import Haskell.Prim -open import Haskell.Prim.String open import Haskell.Prim.Monad + renaming (module Instances to MonadInstances) +open import Haskell.Prim.String open import Haskell.Prim.Maybe open import Haskell.Prim.IO @@ -18,12 +19,14 @@ record MonadFail (m : Type → Type) : Type₁ where open MonadFail ⦃...⦄ public {-# COMPILE AGDA2HS MonadFail existing-class #-} -instance - MonadFailList : MonadFail List - MonadFailList .fail _ = [] +module Instances where + instance + MonadFailList : MonadFail List + MonadFailList .fail _ = [] - MonadFailMaybe : MonadFail Maybe - MonadFailMaybe .fail _ = Nothing + MonadFailMaybe : MonadFail Maybe + MonadFailMaybe .fail _ = Nothing - iMonadFailIO : MonadFail IO - iMonadFailIO .fail = failIO + iMonadFailIO : MonadFail IO + iMonadFailIO .fail = failIO +open Instances public diff --git a/lib/base/Haskell/Prim/MonadPlus.agda b/lib/base/Haskell/Prim/MonadPlus.agda index 1557731c..21d9aa66 100644 --- a/lib/base/Haskell/Prim/MonadPlus.agda +++ b/lib/base/Haskell/Prim/MonadPlus.agda @@ -2,7 +2,9 @@ module Haskell.Prim.MonadPlus where open import Haskell.Prim open import Haskell.Prim.Alternative + renaming (module Instances to AlternativeInstances) open import Haskell.Prim.Monad + renaming (module Instances to MonadInstances) open import Haskell.Prim.IO open import Haskell.Prim.List open import Haskell.Prim.Maybe @@ -36,23 +38,25 @@ open MonadPlus ⦃...⦄ public {-# COMPILE AGDA2HS MonadPlus existing-class #-} -- ** instances -instance - open DefaultMonadPlus +module Instances where + instance + open DefaultMonadPlus - iDefaultMonadPlusList : DefaultMonadPlus List - iDefaultMonadPlusList = record {} + iDefaultMonadPlusList : DefaultMonadPlus List + iDefaultMonadPlusList = record {} - iMonadPlusList : MonadPlus List - iMonadPlusList = record {DefaultMonadPlus iDefaultMonadPlusList} + iMonadPlusList : MonadPlus List + iMonadPlusList = record {DefaultMonadPlus iDefaultMonadPlusList} - iDefaultMonadPlusMaybe : DefaultMonadPlus Maybe - iDefaultMonadPlusMaybe = record {} + iDefaultMonadPlusMaybe : DefaultMonadPlus Maybe + iDefaultMonadPlusMaybe = record {} - iMonadPlusMaybe : MonadPlus Maybe - iMonadPlusMaybe = record {DefaultMonadPlus iDefaultMonadPlusMaybe} + iMonadPlusMaybe : MonadPlus Maybe + iMonadPlusMaybe = record {DefaultMonadPlus iDefaultMonadPlusMaybe} - iDefaultMonadPlusIO : DefaultMonadPlus IO - iDefaultMonadPlusIO = record {} + iDefaultMonadPlusIO : DefaultMonadPlus IO + iDefaultMonadPlusIO = record {} - iMonadPlusIO : MonadPlus IO - iMonadPlusIO = record {DefaultMonadPlus iDefaultMonadPlusIO} + iMonadPlusIO : MonadPlus IO + iMonadPlusIO = record {DefaultMonadPlus iDefaultMonadPlusIO} +open Instances public diff --git a/lib/base/Haskell/Prim/Monoid.agda b/lib/base/Haskell/Prim/Monoid.agda index 90ef8e61..f56d99c2 100644 --- a/lib/base/Haskell/Prim/Monoid.agda +++ b/lib/base/Haskell/Prim/Monoid.agda @@ -1,6 +1,8 @@ module Haskell.Prim.Monoid where open import Haskell.Prim +open import Haskell.Prim.Semigroup + renaming (module Instances to SemigroupInstances) open import Haskell.Prim.Bool open import Haskell.Prim.List open import Haskell.Prim.Maybe @@ -8,46 +10,6 @@ open import Haskell.Prim.Either open import Haskell.Prim.Tuple --------------------------------------------------------------------------------- --- Semigroup - --- ** base -record Semigroup (a : Type) : Type where - infixr 6 _<>_ - field _<>_ : a → a → a - --- ** export -open Semigroup ⦃...⦄ public -{-# COMPILE AGDA2HS Semigroup existing-class #-} - --- ** instances -instance - iSemigroupList : Semigroup (List a) - iSemigroupList ._<>_ = _++_ - - iSemigroupMaybe : ⦃ Semigroup a ⦄ → Semigroup (Maybe a) - iSemigroupMaybe ._<>_ Nothing m = m - iSemigroupMaybe ._<>_ m Nothing = m - iSemigroupMaybe ._<>_ (Just x) (Just y) = Just (x <> y) - - iSemigroupEither : Semigroup (Either a b) - iSemigroupEither ._<>_ (Left _) e = e - iSemigroupEither ._<>_ e _ = e - - iSemigroupFun : ⦃ Semigroup b ⦄ → Semigroup (a → b) - iSemigroupFun ._<>_ f g x = f x <> g x - - iSemigroupUnit : Semigroup ⊤ - iSemigroupUnit ._<>_ _ _ = tt - - - iSemigroupTuple₂ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → Semigroup (a × b) - iSemigroupTuple₂ ._<>_ (x₁ , y₁) (x₂ , y₂) = x₁ <> x₂ , y₁ <> y₂ - - iSemigroupTuple₃ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → ⦃ Semigroup c ⦄ → Semigroup (a × b × c) - iSemigroupTuple₃ ._<>_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ <> x₂ , y₁ <> y₂ , z₁ <> z₂ - - -------------------------------------------------------------------------------- -- Monoid @@ -77,42 +39,44 @@ open Monoid ⦃...⦄ public {-# COMPILE AGDA2HS Monoid existing-class #-} -- ** instances -instance - iDefaultMonoidList : DefaultMonoid (List a) - iDefaultMonoidList .DefaultMonoid.mempty = [] +module Instances where + instance + iDefaultMonoidList : DefaultMonoid (List a) + iDefaultMonoidList .DefaultMonoid.mempty = [] - iMonoidList : Monoid (List a) - iMonoidList = record{DefaultMonoid iDefaultMonoidList} + iMonoidList : Monoid (List a) + iMonoidList = record{DefaultMonoid iDefaultMonoidList} - iDefaultMonoidMaybe : ⦃ Semigroup a ⦄ → DefaultMonoid (Maybe a) - iDefaultMonoidMaybe .DefaultMonoid.mempty = Nothing + iDefaultMonoidMaybe : ⦃ Semigroup a ⦄ → DefaultMonoid (Maybe a) + iDefaultMonoidMaybe .DefaultMonoid.mempty = Nothing - iMonoidMaybe : ⦃ Semigroup a ⦄ → Monoid (Maybe a) - iMonoidMaybe = record{DefaultMonoid iDefaultMonoidMaybe} + iMonoidMaybe : ⦃ Semigroup a ⦄ → Monoid (Maybe a) + iMonoidMaybe = record{DefaultMonoid iDefaultMonoidMaybe} - iDefaultMonoidFun : ⦃ Monoid b ⦄ → DefaultMonoid (a → b) - iDefaultMonoidFun .DefaultMonoid.mempty = λ _ → mempty + iDefaultMonoidFun : ⦃ Monoid b ⦄ → DefaultMonoid (a → b) + iDefaultMonoidFun .DefaultMonoid.mempty = λ _ → mempty - iMonoidFun : ⦃ Monoid b ⦄ → Monoid (a → b) - iMonoidFun = record{DefaultMonoid iDefaultMonoidFun} + iMonoidFun : ⦃ Monoid b ⦄ → Monoid (a → b) + iMonoidFun = record{DefaultMonoid iDefaultMonoidFun} - iDefaultMonoidUnit : DefaultMonoid ⊤ - iDefaultMonoidUnit .DefaultMonoid.mempty = tt + iDefaultMonoidUnit : DefaultMonoid ⊤ + iDefaultMonoidUnit .DefaultMonoid.mempty = tt - iMonoidUnit : Monoid ⊤ - iMonoidUnit = record{DefaultMonoid iDefaultMonoidUnit} + iMonoidUnit : Monoid ⊤ + iMonoidUnit = record{DefaultMonoid iDefaultMonoidUnit} - iDefaultMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonoid (a × b) - iDefaultMonoidTuple₂ .DefaultMonoid.mempty = (mempty , mempty) + iDefaultMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonoid (a × b) + iDefaultMonoidTuple₂ .DefaultMonoid.mempty = (mempty , mempty) - iMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monoid (a × b) - iMonoidTuple₂ = record{DefaultMonoid iDefaultMonoidTuple₂} + iMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monoid (a × b) + iMonoidTuple₂ = record{DefaultMonoid iDefaultMonoidTuple₂} - iDefaultMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → DefaultMonoid (a × b × c) - iDefaultMonoidTuple₃ .DefaultMonoid.mempty = (mempty , mempty , mempty) + iDefaultMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → DefaultMonoid (a × b × c) + iDefaultMonoidTuple₃ .DefaultMonoid.mempty = (mempty , mempty , mempty) - iMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → Monoid (a × b × c) - iMonoidTuple₃ = record{DefaultMonoid iDefaultMonoidTuple₃} + iMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → Monoid (a × b × c) + iMonoidTuple₃ = record{DefaultMonoid iDefaultMonoidTuple₃} +open Instances public open DefaultMonoid diff --git a/lib/base/Haskell/Prim/Num.agda b/lib/base/Haskell/Prim/Num.agda index c7c6bb60..cec6a7b4 100644 --- a/lib/base/Haskell/Prim/Num.agda +++ b/lib/base/Haskell/Prim/Num.agda @@ -3,15 +3,21 @@ module Haskell.Prim.Num where open import Haskell.Prim +open import Haskell.Prim.Eq + renaming (module Instances to EqInstances) +open import Haskell.Prim.Ord + renaming (module Instances to OrdInstances) +open import Haskell.Prim.Semigroup + renaming (module Instances to SemigroupInstances) +open import Haskell.Prim.Monoid + renaming (module Instances to MonoidInstances) open import Haskell.Prim.Word open import Haskell.Prim.Int open import Haskell.Prim.Integer open import Haskell.Prim.Double -open import Haskell.Prim.Eq -open import Haskell.Prim.Ord -open import Haskell.Prim.Monoid --------------------------------------------------- + +-------------------------------------------------------------------------------- -- Num record Num (a : Type) : Type₁ where @@ -33,88 +39,87 @@ record Num (a : Type) : Type₁ where overlap ⦃ numOne ⦄ : number .Number.Constraint 1 open Num ⦃...⦄ public hiding (FromIntegerOK; number) - {-# COMPILE AGDA2HS Num existing-class #-} -instance - iNumNat : Num Nat - iNumNat .MinusOK n m = IsFalse (ltNat n m) - iNumNat .NegateOK 0 = ⊤ - iNumNat .NegateOK (suc _) = ⊥ - iNumNat .Num.FromIntegerOK (negsuc _) = ⊥ - iNumNat .Num.FromIntegerOK (pos _) = ⊤ - iNumNat ._+_ n m = addNat n m - iNumNat ._-_ n m = monusNat n m - iNumNat ._*_ n m = mulNat n m - iNumNat .negate n = n - iNumNat .abs n = n - iNumNat .signum 0 = 0 - iNumNat .signum (suc n) = 1 - iNumNat .fromInteger (pos n) = n - iNumNat .fromInteger (negsuc _) ⦃ () ⦄ +module Instances where + instance + iNumNat : Num Nat + iNumNat .MinusOK n m = IsFalse (ltNat n m) + iNumNat .NegateOK 0 = ⊤ + iNumNat .NegateOK (suc _) = ⊥ + iNumNat .Num.FromIntegerOK (negsuc _) = ⊥ + iNumNat .Num.FromIntegerOK (pos _) = ⊤ + iNumNat ._+_ n m = addNat n m + iNumNat ._-_ n m = monusNat n m + iNumNat ._*_ n m = mulNat n m + iNumNat .negate n = n + iNumNat .abs n = n + iNumNat .signum 0 = 0 + iNumNat .signum (suc n) = 1 + iNumNat .fromInteger (pos n) = n + iNumNat .fromInteger (negsuc _) ⦃ () ⦄ - iNumInt : Num Int - iNumInt .MinusOK _ _ = ⊤ - iNumInt .NegateOK _ = ⊤ - iNumInt .Num.FromIntegerOK _ = ⊤ - iNumInt ._+_ x y = addInt x y - iNumInt ._-_ x y = subInt x y - iNumInt ._*_ x y = mulInt x y - iNumInt .negate x = negateInt x - iNumInt .abs x = absInt x - iNumInt .signum x = signInt x - iNumInt .fromInteger n = integerToInt n + iNumInt : Num Int + iNumInt .MinusOK _ _ = ⊤ + iNumInt .NegateOK _ = ⊤ + iNumInt .Num.FromIntegerOK _ = ⊤ + iNumInt ._+_ x y = addInt x y + iNumInt ._-_ x y = subInt x y + iNumInt ._*_ x y = mulInt x y + iNumInt .negate x = negateInt x + iNumInt .abs x = absInt x + iNumInt .signum x = signInt x + iNumInt .fromInteger n = integerToInt n - iNumInteger : Num Integer - iNumInteger .MinusOK _ _ = ⊤ - iNumInteger .NegateOK _ = ⊤ - iNumInteger .Num.FromIntegerOK _ = ⊤ - iNumInteger ._+_ x y = addInteger x y - iNumInteger ._-_ x y = subInteger x y - iNumInteger ._*_ x y = mulInteger x y - iNumInteger .negate x = negateInteger x - iNumInteger .abs x = absInteger x - iNumInteger .signum x = signInteger x - iNumInteger .fromInteger n = n + iNumInteger : Num Integer + iNumInteger .MinusOK _ _ = ⊤ + iNumInteger .NegateOK _ = ⊤ + iNumInteger .Num.FromIntegerOK _ = ⊤ + iNumInteger ._+_ x y = addInteger x y + iNumInteger ._-_ x y = subInteger x y + iNumInteger ._*_ x y = mulInteger x y + iNumInteger .negate x = negateInteger x + iNumInteger .abs x = absInteger x + iNumInteger .signum x = signInteger x + iNumInteger .fromInteger n = n - iNumWord : Num Word - iNumWord .MinusOK _ _ = ⊤ - iNumWord .NegateOK _ = ⊤ - iNumWord .Num.FromIntegerOK _ = ⊤ - iNumWord ._+_ x y = addWord x y - iNumWord ._-_ x y = subWord x y - iNumWord ._*_ x y = mulWord x y - iNumWord .negate x = negateWord x - iNumWord .abs x = x - iNumWord .signum x = if x == 0 then 0 else 1 - iNumWord .fromInteger n = integerToWord n + iNumWord : Num Word + iNumWord .MinusOK _ _ = ⊤ + iNumWord .NegateOK _ = ⊤ + iNumWord .Num.FromIntegerOK _ = ⊤ + iNumWord ._+_ x y = addWord x y + iNumWord ._-_ x y = subWord x y + iNumWord ._*_ x y = mulWord x y + iNumWord .negate x = negateWord x + iNumWord .abs x = x + iNumWord .signum x = if x == 0 then 0 else 1 + iNumWord .fromInteger n = integerToWord n - iNumDouble : Num Double - iNumDouble .MinusOK _ _ = ⊤ - iNumDouble .NegateOK _ = ⊤ - iNumDouble .Num.FromIntegerOK _ = ⊤ - iNumDouble ._+_ x y = primFloatPlus x y - iNumDouble ._-_ x y = primFloatMinus x y - iNumDouble ._*_ x y = primFloatTimes x y - iNumDouble .negate x = primFloatMinus 0.0 x - iNumDouble .abs x = if x < 0.0 then primFloatMinus 0.0 x else x - iNumDouble .signum x = case compare x 0.0 of λ where - LT → -1.0 - EQ → x - GT → 1.0 - iNumDouble .fromInteger (pos n) = fromNat n - iNumDouble .fromInteger (negsuc n) = fromNeg (suc n) + iNumDouble : Num Double + iNumDouble .MinusOK _ _ = ⊤ + iNumDouble .NegateOK _ = ⊤ + iNumDouble .Num.FromIntegerOK _ = ⊤ + iNumDouble ._+_ x y = primFloatPlus x y + iNumDouble ._-_ x y = primFloatMinus x y + iNumDouble ._*_ x y = primFloatTimes x y + iNumDouble .negate x = primFloatMinus 0.0 x + iNumDouble .abs x = if x < 0.0 then primFloatMinus 0.0 x else x + iNumDouble .signum x = case compare x 0.0 of λ where + LT → -1.0 + EQ → x + GT → 1.0 + iNumDouble .fromInteger (pos n) = fromNat n + iNumDouble .fromInteger (negsuc n) = fromNeg (suc n) +open Instances public open DefaultMonoid MonoidSum : ⦃ iNum : Num a ⦄ → Monoid a MonoidSum = record {DefaultMonoid (λ where .mempty → 0 - .super ._<>_ → _+_ - )} + .super ._<>_ → _+_)} MonoidProduct : ⦃ iNum : Num a ⦄ → Monoid a MonoidProduct = record {DefaultMonoid (λ where .mempty → 1 - .super ._<>_ → _*_ - )} + .super ._<>_ → _*_)} diff --git a/lib/base/Haskell/Prim/Ord.agda b/lib/base/Haskell/Prim/Ord.agda index beda7476..d3f5eaa9 100644 --- a/lib/base/Haskell/Prim/Ord.agda +++ b/lib/base/Haskell/Prim/Ord.agda @@ -3,18 +3,23 @@ module Haskell.Prim.Ord where open import Haskell.Prim open import Haskell.Prim.Eq + renaming (module Instances to EqInstances) +open import Haskell.Prim.Semigroup + renaming (module Instances to SemigroupInstances) +open import Haskell.Prim.Monoid + renaming (module Instances to MonoidInstances) open import Haskell.Prim.Bool open import Haskell.Prim.Int open import Haskell.Prim.Word open import Haskell.Prim.Integer open import Haskell.Prim.Double open import Haskell.Prim.Tuple -open import Haskell.Prim.Monoid open import Haskell.Prim.List open import Haskell.Prim.Maybe open import Haskell.Prim.Either --------------------------------------------------- + +-------------------------------------------------------------------------------- -- Ordering data Ordering : Type where @@ -35,7 +40,8 @@ instance iMonoidOrdering : Monoid Ordering iMonoidOrdering = record {DefaultMonoid (record {mempty = EQ})} --------------------------------------------------- + +-------------------------------------------------------------------------------- -- Ord record Ord (a : Type) : Type where @@ -97,9 +103,7 @@ record OrdFromLessThan (a : Type) : Type where min : a → a → a min x y = if y < x then y else x - open Ord ⦃...⦄ public - {-# COMPILE AGDA2HS Ord existing-class #-} private @@ -117,118 +121,120 @@ private minNat (suc x) zero = zero minNat (suc x) (suc y) = suc (minNat x y) -instance - iOrdFromLessThanNat : OrdFromLessThan Nat - iOrdFromLessThanNat .OrdFromLessThan._<_ = ltNat - - iOrdNat : Ord Nat - iOrdNat = record - { OrdFromLessThan iOrdFromLessThanNat - ; max = maxNat - ; min = minNat - } - - iOrdFromLessThanInteger : OrdFromLessThan Integer - iOrdFromLessThanInteger .OrdFromLessThan._<_ = ltInteger - - iOrdInteger : Ord Integer - iOrdInteger = record {OrdFromLessThan iOrdFromLessThanInteger} - - iOrdFromLessThanInt : OrdFromLessThan Int - iOrdFromLessThanInt .OrdFromLessThan._<_ = ltInt - - iOrdInt : Ord Int - iOrdInt = record {OrdFromLessThan iOrdFromLessThanInt} - - iOrdFromLessThanWord : OrdFromLessThan Word - iOrdFromLessThanWord .OrdFromLessThan._<_ = ltWord - - iOrdWord : Ord Word - iOrdWord = record {OrdFromLessThan iOrdFromLessThanWord} - - iOrdFromLessThanDouble : OrdFromLessThan Double - iOrdFromLessThanDouble .OrdFromLessThan._<_ = primFloatLess - - iOrdDouble : Ord Double - iOrdDouble = record {OrdFromLessThan iOrdFromLessThanDouble} - - iOrdFromLessThanChar : OrdFromLessThan Char - iOrdFromLessThanChar .OrdFromLessThan._<_ x y = c2n x < c2n y - - iOrdChar : Ord Char - iOrdChar = record {OrdFromLessThan iOrdFromLessThanChar} - - iOrdFromCompareBool : OrdFromCompare Bool - iOrdFromCompareBool .OrdFromCompare.compare = λ where - False True → LT - True False → GT - _ _ → EQ - - iOrdBool : Ord Bool - iOrdBool = record {OrdFromCompare iOrdFromCompareBool} - - iOrdFromCompareUnit : OrdFromCompare ⊤ - iOrdFromCompareUnit .OrdFromCompare.compare = λ _ _ → EQ - - iOrdUnit : Ord ⊤ - iOrdUnit = record {OrdFromCompare iOrdFromCompareUnit} - - iOrdFromCompareTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → OrdFromCompare (a × b) - iOrdFromCompareTuple₂ .OrdFromCompare.compare = λ where - (x₁ , y₁) (x₂ , y₂) → compare x₁ x₂ <> compare y₁ y₂ - - iOrdTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (a × b) - iOrdTuple₂ = record {OrdFromCompare iOrdFromCompareTuple₂} +private + compareList : ⦃ Ord a ⦄ → List a → List a → Ordering + compareList [] [] = EQ + compareList [] (_ ∷ _) = LT + compareList (_ ∷ _) [] = GT + compareList (x ∷ xs) (y ∷ ys) = compare x y <> compareList xs ys - iOrdFromCompareTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → OrdFromCompare (a × b × c) - iOrdFromCompareTuple₃ .OrdFromCompare.compare = λ where - (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) → compare x₁ x₂ <> compare y₁ y₂ <> compare z₁ z₂ +module Instances where + instance + iOrdFromLessThanNat : OrdFromLessThan Nat + iOrdFromLessThanNat .OrdFromLessThan._<_ = ltNat - iOrdTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → Ord (a × b × c) - iOrdTuple₃ = record {OrdFromCompare iOrdFromCompareTuple₃} + iOrdNat : Ord Nat + iOrdNat = record + { OrdFromLessThan iOrdFromLessThanNat + ; max = maxNat + ; min = minNat + } + + iOrdFromLessThanInteger : OrdFromLessThan Integer + iOrdFromLessThanInteger .OrdFromLessThan._<_ = ltInteger + + iOrdInteger : Ord Integer + iOrdInteger = record {OrdFromLessThan iOrdFromLessThanInteger} + + iOrdFromLessThanInt : OrdFromLessThan Int + iOrdFromLessThanInt .OrdFromLessThan._<_ = ltInt + + iOrdInt : Ord Int + iOrdInt = record {OrdFromLessThan iOrdFromLessThanInt} + + iOrdFromLessThanWord : OrdFromLessThan Word + iOrdFromLessThanWord .OrdFromLessThan._<_ = ltWord + + iOrdWord : Ord Word + iOrdWord = record {OrdFromLessThan iOrdFromLessThanWord} + + iOrdFromLessThanDouble : OrdFromLessThan Double + iOrdFromLessThanDouble .OrdFromLessThan._<_ = primFloatLess + + iOrdDouble : Ord Double + iOrdDouble = record {OrdFromLessThan iOrdFromLessThanDouble} + + iOrdFromLessThanChar : OrdFromLessThan Char + iOrdFromLessThanChar .OrdFromLessThan._<_ x y = c2n x < c2n y + + iOrdChar : Ord Char + iOrdChar = record {OrdFromLessThan iOrdFromLessThanChar} + + iOrdFromCompareBool : OrdFromCompare Bool + iOrdFromCompareBool .OrdFromCompare.compare = λ where + False True → LT + True False → GT + _ _ → EQ + + iOrdBool : Ord Bool + iOrdBool = record {OrdFromCompare iOrdFromCompareBool} + + iOrdFromCompareUnit : OrdFromCompare ⊤ + iOrdFromCompareUnit .OrdFromCompare.compare = λ _ _ → EQ + + iOrdUnit : Ord ⊤ + iOrdUnit = record {OrdFromCompare iOrdFromCompareUnit} + + iOrdFromCompareTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → OrdFromCompare (a × b) + iOrdFromCompareTuple₂ .OrdFromCompare.compare = λ where + (x₁ , y₁) (x₂ , y₂) → compare x₁ x₂ <> compare y₁ y₂ + + iOrdTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (a × b) + iOrdTuple₂ = record {OrdFromCompare iOrdFromCompareTuple₂} + + iOrdFromCompareTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → OrdFromCompare (a × b × c) + iOrdFromCompareTuple₃ .OrdFromCompare.compare = λ where + (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) → compare x₁ x₂ <> compare y₁ y₂ <> compare z₁ z₂ + + iOrdTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → Ord (a × b × c) + iOrdTuple₃ = record {OrdFromCompare iOrdFromCompareTuple₃} + + iOrdFromCompareList : ⦃ Ord a ⦄ → OrdFromCompare (List a) + iOrdFromCompareList .OrdFromCompare.compare = compareList + + iOrdList : ⦃ Ord a ⦄ → Ord (List a) + iOrdList = record {OrdFromCompare iOrdFromCompareList} + + iOrdFromCompareMaybe : ⦃ Ord a ⦄ → OrdFromCompare (Maybe a) + iOrdFromCompareMaybe .OrdFromCompare.compare = λ where + Nothing Nothing → EQ + Nothing (Just _) → LT + (Just _) Nothing → GT + (Just x) (Just y) → compare x y + + iOrdMaybe : ⦃ Ord a ⦄ → Ord (Maybe a) + iOrdMaybe = record {OrdFromCompare iOrdFromCompareMaybe} + + iOrdFromCompareEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → OrdFromCompare (Either a b) + iOrdFromCompareEither .OrdFromCompare.compare = λ where + (Left x) (Left y) → compare x y + (Left _) (Right _) → LT + (Right _) (Left _) → GT + (Right x) (Right y) → compare x y + + iOrdEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (Either a b) + iOrdEither = record {OrdFromCompare iOrdFromCompareEither} -compareList : ⦃ Ord a ⦄ → List a → List a → Ordering -compareList [] [] = EQ -compareList [] (_ ∷ _) = LT -compareList (_ ∷ _) [] = GT -compareList (x ∷ xs) (y ∷ ys) = compare x y <> compareList xs ys + iOrdFromCompareOrdering : OrdFromCompare Ordering + iOrdFromCompareOrdering .OrdFromCompare.compare = λ where + LT LT → EQ + LT _ → LT + _ LT → GT + EQ EQ → EQ + EQ GT → LT + GT EQ → GT + GT GT → EQ -instance - iOrdFromCompareList : ⦃ Ord a ⦄ → OrdFromCompare (List a) - iOrdFromCompareList .OrdFromCompare.compare = compareList - - iOrdList : ⦃ Ord a ⦄ → Ord (List a) - iOrdList = record {OrdFromCompare iOrdFromCompareList} - - iOrdFromCompareMaybe : ⦃ Ord a ⦄ → OrdFromCompare (Maybe a) - iOrdFromCompareMaybe .OrdFromCompare.compare = λ where - Nothing Nothing → EQ - Nothing (Just _) → LT - (Just _) Nothing → GT - (Just x) (Just y) → compare x y - - iOrdMaybe : ⦃ Ord a ⦄ → Ord (Maybe a) - iOrdMaybe = record {OrdFromCompare iOrdFromCompareMaybe} - - iOrdFromCompareEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → OrdFromCompare (Either a b) - iOrdFromCompareEither .OrdFromCompare.compare = λ where - (Left x) (Left y) → compare x y - (Left _) (Right _) → LT - (Right _) (Left _) → GT - (Right x) (Right y) → compare x y - - iOrdEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (Either a b) - iOrdEither = record {OrdFromCompare iOrdFromCompareEither} - - iOrdFromCompareOrdering : OrdFromCompare Ordering - iOrdFromCompareOrdering .OrdFromCompare.compare = λ where - LT LT → EQ - LT _ → LT - _ LT → GT - EQ EQ → EQ - EQ GT → LT - GT EQ → GT - GT GT → EQ - - iOrdOrdering : Ord Ordering - iOrdOrdering = record {OrdFromCompare iOrdFromCompareOrdering} + iOrdOrdering : Ord Ordering + iOrdOrdering = record {OrdFromCompare iOrdFromCompareOrdering} +open Instances public diff --git a/lib/base/Haskell/Prim/Semigroup.agda b/lib/base/Haskell/Prim/Semigroup.agda new file mode 100644 index 00000000..25bcbf5e --- /dev/null +++ b/lib/base/Haskell/Prim/Semigroup.agda @@ -0,0 +1,48 @@ +module Haskell.Prim.Semigroup where + +open import Haskell.Prim +open import Haskell.Prim.List +open import Haskell.Prim.Maybe +open import Haskell.Prim.Either +open import Haskell.Prim.Tuple + + +-------------------------------------------------------------------------------- +-- Semigroup + +-- ** base +record Semigroup (a : Type) : Type where + infixr 6 _<>_ + field _<>_ : a → a → a + +-- ** export +open Semigroup ⦃...⦄ public +{-# COMPILE AGDA2HS Semigroup existing-class #-} + +-- ** instances +module Instances where + instance + iSemigroupList : Semigroup (List a) + iSemigroupList ._<>_ = _++_ + + iSemigroupMaybe : ⦃ Semigroup a ⦄ → Semigroup (Maybe a) + iSemigroupMaybe ._<>_ Nothing m = m + iSemigroupMaybe ._<>_ m Nothing = m + iSemigroupMaybe ._<>_ (Just x) (Just y) = Just (x <> y) + + iSemigroupEither : Semigroup (Either a b) + iSemigroupEither ._<>_ (Left _) e = e + iSemigroupEither ._<>_ e _ = e + + iSemigroupFun : ⦃ Semigroup b ⦄ → Semigroup (a → b) + iSemigroupFun ._<>_ f g x = f x <> g x + + iSemigroupUnit : Semigroup ⊤ + iSemigroupUnit ._<>_ _ _ = tt + + iSemigroupTuple₂ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → Semigroup (a × b) + iSemigroupTuple₂ ._<>_ (x₁ , y₁) (x₂ , y₂) = x₁ <> x₂ , y₁ <> y₂ + + iSemigroupTuple₃ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → ⦃ Semigroup c ⦄ → Semigroup (a × b × c) + iSemigroupTuple₃ ._<>_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ <> x₂ , y₁ <> y₂ , z₁ <> z₂ +open Instances public diff --git a/lib/base/Haskell/Prim/Show.agda b/lib/base/Haskell/Prim/Show.agda index 601512b1..01f26b26 100644 --- a/lib/base/Haskell/Prim/Show.agda +++ b/lib/base/Haskell/Prim/Show.agda @@ -2,22 +2,25 @@ module Haskell.Prim.Show where open import Haskell.Prim +open import Haskell.Prim.Eq + renaming (module Instances to EqInstances) +open import Haskell.Prim.Ord + renaming (module Instances to OrdInstances) +open import Haskell.Prim.Foldable + renaming (module Instances to FoldableInstances) open import Haskell.Prim.String open import Haskell.Prim.List open import Haskell.Prim.Word open import Haskell.Prim.Double open import Haskell.Prim.Maybe -open import Haskell.Prim.Eq open import Haskell.Prim.Tuple -open import Haskell.Prim.Ord open import Haskell.Prim.Either open import Haskell.Prim.Integer open import Haskell.Prim.Bool open import Haskell.Prim.Int -open import Haskell.Prim.Foldable --------------------------------------------------- +-------------------------------------------------------------------------------- -- Show ShowS : Type @@ -72,88 +75,90 @@ shows = showsPrec 0 {-# COMPILE AGDA2HS Show existing-class #-} -- ** instances -instance - iShow₂Nat : Show₂ Nat - iShow₂Nat .Show₂.show = primStringToList ∘ primShowNat +module Instances where + instance + iShow₂Nat : Show₂ Nat + iShow₂Nat .Show₂.show = primStringToList ∘ primShowNat - iShowNat : Show Nat - iShowNat = record {Show₂ iShow₂Nat} + iShowNat : Show Nat + iShowNat = record {Show₂ iShow₂Nat} - iShow₂Integer : Show₂ Integer - iShow₂Integer .Show₂.show = showInteger + iShow₂Integer : Show₂ Integer + iShow₂Integer .Show₂.show = showInteger - iShowInteger : Show Integer - iShowInteger = record {Show₂ iShow₂Integer} + iShowInteger : Show Integer + iShowInteger = record {Show₂ iShow₂Integer} - iShow₂Int : Show₂ Int - iShow₂Int .Show₂.show = showInt + iShow₂Int : Show₂ Int + iShow₂Int .Show₂.show = showInt - iShowInt : Show Int - iShowInt = record{Show₂ iShow₂Int} + iShowInt : Show Int + iShowInt = record{Show₂ iShow₂Int} - iShow₂Word : Show₂ Word - iShow₂Word .Show₂.show = showWord + iShow₂Word : Show₂ Word + iShow₂Word .Show₂.show = showWord - iShowWord : Show Word - iShowWord = record{Show₂ iShow₂Word} + iShowWord : Show Word + iShowWord = record{Show₂ iShow₂Word} - iShow₂Double : Show₂ Double - iShow₂Double .Show₂.show = primStringToList ∘ primShowFloat + iShow₂Double : Show₂ Double + iShow₂Double .Show₂.show = primStringToList ∘ primShowFloat - iShowDouble : Show Double - iShowDouble = record{Show₂ iShow₂Double} + iShowDouble : Show Double + iShowDouble = record{Show₂ iShow₂Double} - iShow₂Bool : Show₂ Bool - iShow₂Bool .Show₂.show = λ where False → "False"; True → "True" + iShow₂Bool : Show₂ Bool + iShow₂Bool .Show₂.show = λ where False → "False"; True → "True" - iShowBool : Show Bool - iShowBool = record{Show₂ iShow₂Bool} + iShowBool : Show Bool + iShowBool = record{Show₂ iShow₂Bool} - iShow₁Char : Show₁ Char - iShow₁Char .Show₁.showsPrec _ = showString ∘ primStringToList ∘ primShowChar + iShow₁Char : Show₁ Char + iShow₁Char .Show₁.showsPrec _ = showString ∘ primStringToList ∘ primShowChar - iShowChar : Show Char - iShowChar = record{Show₁ iShow₁Char} + iShowChar : Show Char + iShowChar = record{Show₁ iShow₁Char} - iShow₁List : ⦃ Show a ⦄ → Show₁ (List a) - iShow₁List .Show₁.showsPrec _ = showList + iShow₁List : ⦃ Show a ⦄ → Show₁ (List a) + iShow₁List .Show₁.showsPrec _ = showList - iShowList : ⦃ Show a ⦄ → Show (List a) - iShowList = record{Show₁ iShow₁List} + iShowList : ⦃ Show a ⦄ → Show (List a) + iShowList = record{Show₁ iShow₁List} -private - showApp₁ : ⦃ Show a ⦄ → Int → String → a → ShowS - showApp₁ p tag x = showParen (p > 10) $ - showString tag ∘ showString " " ∘ showsPrec 11 x + private + showApp₁ : ⦃ Show a ⦄ → Int → String → a → ShowS + showApp₁ p tag x = showParen (p > 10) $ + showString tag ∘ showString " " ∘ showsPrec 11 x -instance - iShow₁Maybe : ⦃ Show a ⦄ → Show₁ (Maybe a) - iShow₁Maybe .Show₁.showsPrec = λ where - p Nothing → showString "Nothing" - p (Just x) → showApp₁ p "Just" x + instance + iShow₁Maybe : ⦃ Show a ⦄ → Show₁ (Maybe a) + iShow₁Maybe .Show₁.showsPrec = λ where + p Nothing → showString "Nothing" + p (Just x) → showApp₁ p "Just" x - iShowMaybe : ⦃ Show a ⦄ → Show (Maybe a) - iShowMaybe = record{Show₁ iShow₁Maybe} + iShowMaybe : ⦃ Show a ⦄ → Show (Maybe a) + iShowMaybe = record{Show₁ iShow₁Maybe} - iShow₁Either : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show₁ (Either a b) - iShow₁Either .Show₁.showsPrec = λ where - p (Left x) → showApp₁ p "Left" x - p (Right y) → showApp₁ p "Right" y + iShow₁Either : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show₁ (Either a b) + iShow₁Either .Show₁.showsPrec = λ where + p (Left x) → showApp₁ p "Left" x + p (Right y) → showApp₁ p "Right" y - iShowEither : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (Either a b) - iShowEither = record{Show₁ iShow₁Either} + iShowEither : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (Either a b) + iShowEither = record{Show₁ iShow₁Either} -instance - iShow₁Tuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show₁ (a × b) - iShow₁Tuple₂ .Show₁.showsPrec = λ _ → λ where - (x , y) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ")" + instance + iShow₁Tuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show₁ (a × b) + iShow₁Tuple₂ .Show₁.showsPrec = λ _ → λ where + (x , y) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ")" - iShowTuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (a × b) - iShowTuple₂ = record{Show₁ iShow₁Tuple₂} + iShowTuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (a × b) + iShowTuple₂ = record{Show₁ iShow₁Tuple₂} - iShow₁Tuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show₁ (a × b × c) - iShow₁Tuple₃ .Show₁.showsPrec = λ _ → λ where - (x , y , z) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ", " ∘ shows z ∘ showString ")" + iShow₁Tuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show₁ (a × b × c) + iShow₁Tuple₃ .Show₁.showsPrec = λ _ → λ where + (x , y , z) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ", " ∘ shows z ∘ showString ")" - iShowTuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show (a × b × c) - iShowTuple₃ = record{Show₁ iShow₁Tuple₃} + iShowTuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show (a × b × c) + iShowTuple₃ = record{Show₁ iShow₁Tuple₃} +open Instances public diff --git a/lib/base/Haskell/Prim/Traversable.agda b/lib/base/Haskell/Prim/Traversable.agda index 51c324ae..d4749c74 100644 --- a/lib/base/Haskell/Prim/Traversable.agda +++ b/lib/base/Haskell/Prim/Traversable.agda @@ -1,10 +1,14 @@ module Haskell.Prim.Traversable where open import Haskell.Prim -open import Haskell.Prim.Applicative open import Haskell.Prim.Functor -open import Haskell.Prim.Foldable + renaming (module Instances to FunctorInstances) +open import Haskell.Prim.Applicative + renaming (module Instances to ApplicativeInstances) open import Haskell.Prim.Monad + renaming (module Instances to MonadInstances) +open import Haskell.Prim.Foldable + renaming (module Instances to FoldableInstances) open import Haskell.Prim.List open import Haskell.Prim.Maybe open import Haskell.Prim.Either @@ -46,35 +50,38 @@ open Traversable ⦃...⦄ public {-# COMPILE AGDA2HS Traversable existing-class #-} -- ** instances -private - mkTraversable : DefaultTraversable t → Traversable t - mkTraversable x = record {DefaultTraversable x} - - infix 0 traverse=_ - traverse=_ : ⦃ Functor t ⦄ → ⦃ Foldable t ⦄ - → (∀ {f a b} → ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b)) - → Traversable t - traverse= x = record {DefaultTraversable (record {traverse = x})} -instance - open DefaultTraversable - - iTraversableList : Traversable List - iTraversableList = traverse= traverseList - where - traverseList : ⦃ Applicative f ⦄ → (a → f b) → List a → f (List b) - traverseList f [] = pure [] - traverseList f (x ∷ xs) = ⦇ f x ∷ traverseList f xs ⦈ - - iTraversableMaybe : Traversable Maybe - iTraversableMaybe = traverse= λ where - f Nothing → pure Nothing - f (Just x) → fmap Just (f x) - - iTraversableEither : Traversable (Either a) - iTraversableEither = traverse= λ where - f (Left x) → pure (Left x) - f (Right y) → fmap Right (f y) - - iTraversablePair : Traversable (a ×_) - iTraversablePair = traverse= λ - f (x , y) → fmap (x ,_) (f y) +module Instances where + private + mkTraversable : DefaultTraversable t → Traversable t + mkTraversable x = record {DefaultTraversable x} + + infix 0 traverse=_ + traverse=_ : ⦃ Functor t ⦄ → ⦃ Foldable t ⦄ + → (∀ {f a b} → ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b)) + → Traversable t + traverse= x = record {DefaultTraversable (record {traverse = x})} + + instance + open DefaultTraversable + + iTraversableList : Traversable List + iTraversableList = traverse= traverseList + where + traverseList : ⦃ Applicative f ⦄ → (a → f b) → List a → f (List b) + traverseList f [] = pure [] + traverseList f (x ∷ xs) = ⦇ f x ∷ traverseList f xs ⦈ + + iTraversableMaybe : Traversable Maybe + iTraversableMaybe = traverse= λ where + f Nothing → pure Nothing + f (Just x) → fmap Just (f x) + + iTraversableEither : Traversable (Either a) + iTraversableEither = traverse= λ where + f (Left x) → pure (Left x) + f (Right y) → fmap Right (f y) + + iTraversablePair : Traversable (a ×_) + iTraversablePair = traverse= λ + f (x , y) → fmap (x ,_) (f y) +open Instances public From 9f7a89020247fac38ab6d70506924f2b16bf5833 Mon Sep 17 00:00:00 2001 From: Lukas Rohde Date: Sat, 28 Mar 2026 11:19:06 +0100 Subject: [PATCH 8/8] Replace most Prelude reexports by introducing explicit alias definitions to work around #126 --- lib/base/Haskell/Prelude.agda | 292 ++++++++++++++++++++++++++++++---- 1 file changed, 263 insertions(+), 29 deletions(-) diff --git a/lib/base/Haskell/Prelude.agda b/lib/base/Haskell/Prelude.agda index 710dfd8a..c071a92e 100644 --- a/lib/base/Haskell/Prelude.agda +++ b/lib/base/Haskell/Prelude.agda @@ -16,7 +16,6 @@ open import Haskell.Prim public IsString; fromString; _≡_; refl; a; b; c; d; e; f; m; s; t) - open import Haskell.Prim.Absurd public open import Haskell.Prim.Bool public open import Haskell.Prim.Bounded public @@ -33,7 +32,6 @@ open import Haskell.Prim.IO public open import Haskell.Prim.Maybe public open import Haskell.Prim.Tuple public hiding (first; second; _***_) open import Haskell.Prim.Word public -open import Haskell.Prim.String public open import Haskell.Prim.Eq public renaming (module Instances to EqInstances) open import Haskell.Prim.Ord public @@ -46,34 +44,270 @@ open import Haskell.Prim.Semigroup public renaming (module Instances to SemigroupInstances) open import Haskell.Prim.Monoid public renaming (module Instances to MonoidInstances) -open import Haskell.Prim.Functor public - renaming (module Instances to FunctorInstances) -open import Haskell.Prim.Applicative public - renaming (module Instances to ApplicativeInstances) -open import Haskell.Prim.Monad public - renaming (module Instances to MonadInstances) -open import Haskell.Prim.MonadFail public - renaming (module Instances to MonadFailInstances) -open import Haskell.Prim.Foldable public + +-- Explicitly reexport definitions from Haskell.Data.Functor (update these +-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed): +import Haskell.Data.Functor + +module Functor = Haskell.Data.Functor.Functor +module DefaultFunctor = Haskell.Data.Functor.DefaultFunctor +module FunctorInstances = Haskell.Data.Functor.FunctorInstances + +open Functor ⦃ ... ⦄ public + +Functor : (f : Type → Type) → Type₁ +Functor = Haskell.Data.Functor.Functor + +DefaultFunctor : (f : Type → Type) → Type₁ +DefaultFunctor = Haskell.Data.Functor.DefaultFunctor + +infixl 4 _<$>_ +_<$>_ : ⦃ Haskell.Data.Functor.Functor f ⦄ → (a → b) → f a → f b +_<$>_ = Haskell.Data.Functor._<$>_ + +-- Explicitly reexport definitions from Haskell.Control.Applicative (update these +-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed): +import Haskell.Control.Applicative + +module Applicative = Haskell.Control.Applicative.Applicative +module ApplicativeFrom<*> = Haskell.Control.Applicative.ApplicativeFrom<*> +module ApplicativeFromLiftA2 = Haskell.Control.Applicative.ApplicativeFromLiftA2 +module ApplicativeInstances = Haskell.Control.Applicative.ApplicativeInstances + +open Applicative ⦃ ... ⦄ public + +Applicative : (f : Type → Type) → Type₁ +Applicative = Haskell.Control.Applicative.Applicative + +ApplicativeFrom<*> : (f : Type → Type) → Type₁ +ApplicativeFrom<*> = Haskell.Control.Applicative.ApplicativeFrom<*> + +ApplicativeFromLiftA2 : (f : Type → Type) → Type₁ +ApplicativeFromLiftA2 = Haskell.Control.Applicative.ApplicativeFromLiftA2 + +-- Explicitly reexport definitions from Haskell.Control.Monad (update these +-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed): +import Haskell.Control.Monad + +module Monad = Haskell.Control.Monad.Monad +module DefaultMonad = Haskell.Control.Monad.DefaultMonad +module MonadInstances = Haskell.Control.Monad.MonadInstances +module Dont = Haskell.Control.Monad.Dont + +module MonadFail = Haskell.Control.Monad.MonadFail +module MonadFailInstances = Haskell.Control.Monad.MonadFailInstances + +open Monad ⦃ ... ⦄ public +open MonadFail ⦃ ... ⦄ public + +Monad : (m : Type → Type) → Type₁ +Monad = Haskell.Control.Monad.Monad + +DefaultMonad : (m : Type → Type) → Type₁ +DefaultMonad = Haskell.Control.Monad.DefaultMonad + +MonadFail : (m : Type → Type) → Type₁ +MonadFail = Haskell.Control.Monad.MonadFail + +infixr 1 _=<<_ +_=<<_ : ⦃ Monad m ⦄ → (a → m b) → m a → m b +_=<<_ = Haskell.Control.Monad._=<<_ + +-- Explicitly reexport definitions from Haskell.Data.Foldable (update these +-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed): +import Haskell.Data.Foldable + +module Foldable = Haskell.Data.Foldable.Foldable hiding (fold; foldMap'; foldr'; toList; null; length) - renaming (module Instances to FoldableInstances) -open import Haskell.Prim.Traversable public - renaming (module Instances to TraversableInstances) - -open import Haskell.Data.String public - using (lines; words; unlines; unwords) -open import Haskell.Data.List public - using (_++_; map; reverse; lengthNat; length; - head; last; tail; init; - _!!ᴺ_; _!!_; splitAt; lookup; null; - scanl; scanl1; scanr; scanr1; - replicateNat; replicate; - take; drop; takeWhile; dropWhile; - filter; span; break; - zip; zip3; zipWith; zipWith3; unzip; unzip3; - and; or; any; all; concat; concatMap; notElem) -open import Haskell.Data.Functor public using (_<$>_) -open import Haskell.Control.Monad public using (_=<<_; mapM₋; sequence₋) +module DefaultFoldable = Haskell.Data.Foldable.DefaultFoldable +module FoldableInstances = Haskell.Data.Foldable.FoldableInstances + +open Foldable ⦃ ... ⦄ public + +Foldable : (t : Type → Type) → Type₁ +Foldable = Haskell.Data.Foldable.Foldable + +DefaultFoldable : (t : Type → Type) → Type₁ +DefaultFoldable = Haskell.Data.Foldable.DefaultFoldable + +mapM₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (a → m b) → t a → m ⊤ +mapM₋ = Haskell.Data.Foldable.mapM₋ + +sequence₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → t (m a) → m ⊤ +sequence₋ = Haskell.Data.Foldable.sequence₋ + +-- Explicitly reexport definitions from Haskell.Data.Traversable (update these +-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed): +import Haskell.Data.Traversable + +module Traversable = Haskell.Data.Traversable.Traversable +module DefaultTraversable = Haskell.Data.Traversable.DefaultTraversable +module TraversableInstances = Haskell.Data.Traversable.TraversableInstances + +open Traversable ⦃ ... ⦄ public + +Traversable : (t : Type → Type) → Type₁ +Traversable = Haskell.Data.Traversable.Traversable + +-- Explicitly reexport definitions from Haskell.Data.String (update these +-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed): +import Haskell.Data.String + +String : Type +String = Haskell.Data.String.String + +instance iIsStringString : IsString String +iIsStringString = Haskell.Data.String.iIsStringString + +lines : String → List String +lines = Haskell.Data.String.lines + +words : String → List String +words = Haskell.Data.String.words + +unlines : List String → String +unlines = Haskell.Data.String.unlines + +unwords : List String → String +unwords = Haskell.Data.String.unwords + +-- Explicitly reexport definitions from Haskell.Data.List (update these +-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed): +import Haskell.Data.List + +infixr 5 _++_ +_++_ : List a → List a → List a +_++_ = Haskell.Data.List._++_ + +map : (a → b) → List a → List b +map = Haskell.Data.List.map + +reverse : List a → List a +reverse = Haskell.Data.List.reverse + +lengthNat : List a → Nat +lengthNat = Haskell.Data.List.lengthNat + +length : ⦃ Foldable t ⦄ → t a → Int +length = Haskell.Data.List.length + +head : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a +head = Haskell.Data.List.head + +last : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a +last = Haskell.Data.List.last + +tail : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a +tail = Haskell.Data.List.tail + +init : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a +init = Haskell.Data.List.init + +infixl 9 _!!ᴺ_ +_!!ᴺ_ : (xs : List a) (n : Nat) → @0 ⦃ IsTrue (n < lengthNat xs) ⦄ → a +_!!ᴺ_ = Haskell.Data.List._!!ᴺ_ + +infixl 9 _!!_ +_!!_ : (xs : List a) (n : Int) + → ⦃ @0 _ : IsNonNegativeInt n ⦄ + → ⦃ @0 _ : IsTrue (intToNat n < lengthNat xs) ⦄ → a +_!!_ = Haskell.Data.List._!!_ + +splitAtNat : (n : Nat) → List a → List a × List a +splitAtNat = Haskell.Data.List.splitAtNat + +splitAt : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a × List a +splitAt = Haskell.Data.List.splitAt + +lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b +lookup = Haskell.Data.List.lookup + +null : ⦃ Foldable t ⦄ → t a → Bool +null = Haskell.Data.List.null + +scanl : (b → a → b) → b → List a → List b +scanl = Haskell.Data.List.scanl + +scanl1 : (a → a → a) → List a → List a +scanl1 = Haskell.Data.List.scanl1 + +scanr : (a → b → b) → b → List a → List b +scanr = Haskell.Data.List.scanr + +scanr1 : (a → a → a) → List a → List a +scanr1 = Haskell.Data.List.scanr1 + +replicateNat : Nat → a → List a +replicateNat = Haskell.Data.List.replicateNat + +replicate : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → a → List a +replicate = Haskell.Data.List.replicate + +takeNat : Nat → List a → List a +takeNat = Haskell.Data.List.takeNat + +take : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a +take = Haskell.Data.List.take + +dropNat : Nat → List a → List a +dropNat = Haskell.Data.List.dropNat + +drop : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a +drop = Haskell.Data.List.drop + +takeWhile : (a → Bool) → List a → List a +takeWhile = Haskell.Data.List.takeWhile + +dropWhile : (a → Bool) → List a → List a +dropWhile = Haskell.Data.List.dropWhile + +filter : (a → Bool) → List a → List a +filter = Haskell.Data.List.filter + +span : (a → Bool) → List a → List a × List a +span = Haskell.Data.List.span + +break : (a → Bool) → List a → List a × List a +break = Haskell.Data.List.break + +zip : List a → List b → List (a × b) +zip = Haskell.Data.List.zip + +zip3 : List a → List b → List c → List (a × b × c) +zip3 = Haskell.Data.List.zip3 + +zipWith : (a → b → c) → List a → List b → List c +zipWith = Haskell.Data.List.zipWith + +zipWith3 : (a → b → c → d) → List a → List b → List c → List d +zipWith3 = Haskell.Data.List.zipWith3 + +unzip : List (a × b) → List a × List b +unzip = Haskell.Data.List.unzip + +unzip3 : List (a × b × c) → List a × List b × List c +unzip3 = Haskell.Data.List.unzip3 + +and : ⦃ Foldable t ⦄ → t Bool → Bool +and = Haskell.Data.List.and + +or : ⦃ Foldable t ⦄ → t Bool → Bool +or = Haskell.Data.List.or + +any : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool +any = Haskell.Data.List.any + +all : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool +all = Haskell.Data.List.all + +concat : ⦃ Foldable t ⦄ → t (List a) → List a +concat = Haskell.Data.List.concat + +concatMap : ⦃ Foldable t ⦄ → (a → List b) → t a → List b +concatMap = Haskell.Data.List.concatMap + +notElem : ⦃ Foldable t ⦄ → ⦃ Eq a ⦄ → a → t a → Bool +notElem = Haskell.Data.List.notElem -- Problematic features: