diff --git a/lib/Haskell/Prim/Applicative.agda b/lib/Haskell/Prim/Applicative.agda index a88a6962..20c7aba2 100644 --- a/lib/Haskell/Prim/Applicative.agda +++ b/lib/Haskell/Prim/Applicative.agda @@ -41,43 +41,52 @@ record DefaultApplicative (f : Set → Set) : Set₁ where open Applicative ⦃...⦄ public {-# COMPILE AGDA2HS Applicative existing-class #-} -- ** instances -private - mkApplicative : DefaultApplicative t → Applicative t - mkApplicative x = record {DefaultApplicative x} instance open DefaultApplicative + iDefaultApplicativeList : DefaultApplicative List + iDefaultApplicativeList .pure x = x ∷ [] + iDefaultApplicativeList ._<*>_ fs xs = concatMap (λ f → map f xs) fs + iApplicativeList : Applicative List - iApplicativeList = mkApplicative λ where - .pure x → x ∷ [] - ._<*>_ fs xs → concatMap (λ f → map f xs) fs + iApplicativeList = record {DefaultApplicative iDefaultApplicativeList} + + iDefaultApplicativeMaybe : DefaultApplicative Maybe + iDefaultApplicativeMaybe .pure = Just + iDefaultApplicativeMaybe ._<*>_ (Just f) (Just x) = Just (f x) + iDefaultApplicativeMaybe ._<*>_ _ _ = Nothing iApplicativeMaybe : Applicative Maybe - iApplicativeMaybe = mkApplicative λ where - .pure → Just - ._<*>_ (Just f) (Just x) → Just (f x) - ._<*>_ _ _ → Nothing + iApplicativeMaybe = record {DefaultApplicative iDefaultApplicativeMaybe} + + iDefaultApplicativeEither : DefaultApplicative (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 = mkApplicative λ where - .pure → Right - ._<*>_ (Right f) (Right x) → Right (f x) - ._<*>_ (Left e) _ → Left e - ._<*>_ _ (Left e) → Left e + iApplicativeEither = record{DefaultApplicative iDefaultApplicativeEither} + + iDefaultApplicativeFun : DefaultApplicative (λ b → a → b) + iDefaultApplicativeFun .pure = const + iDefaultApplicativeFun ._<*>_ f g x = f x (g x) iApplicativeFun : Applicative (λ b → a → b) - iApplicativeFun = mkApplicative λ where - .pure → const - ._<*>_ f g x → f x (g x) + iApplicativeFun = record{DefaultApplicative iDefaultApplicativeFun} + + iDefaultApplicativeTuple₂ : ⦃ Monoid a ⦄ → DefaultApplicative (a ×_) + iDefaultApplicativeTuple₂ .pure x = mempty , x + iDefaultApplicativeTuple₂ ._<*>_ (a , f) (b , x) = a <> b , f x iApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_) - iApplicativeTuple₂ = mkApplicative λ where - .pure x → mempty , x - ._<*>_ (a , f) (b , x) → a <> b , f x + iApplicativeTuple₂ = record{DefaultApplicative iDefaultApplicativeTuple₂} + + iDefaultApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultApplicative (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₃ = mkApplicative λ where - .pure x → mempty , mempty , x - ._<*>_ (a , u , f) (b , v , x) → a <> b , u <> v , f x + iApplicativeTuple₃ = record{DefaultApplicative iDefaultApplicativeTuple₃} instance postulate iApplicativeIO : Applicative IO diff --git a/lib/Haskell/Prim/Enum.agda b/lib/Haskell/Prim/Enum.agda index f85c0cad..eafa83fc 100644 --- a/lib/Haskell/Prim/Enum.agda +++ b/lib/Haskell/Prim/Enum.agda @@ -122,82 +122,142 @@ instance iEnumInteger .enumFromTo = integerFromTo iEnumInteger .enumFromThenTo = integerFromThenTo -module _ (from : a → Integer) (to : Integer → a) where - private - fromTo : a → a → List a - fromTo a b = map to (enumFromTo (from a) (from b)) - - fromThenTo : (x x₁ : a) → @0 ⦃ IsFalse (fromEnum (from x) == fromEnum (from x₁)) ⦄ → a → List a - fromThenTo a a₁ b = map to (enumFromThenTo (from a) (from a₁) (from b)) - - unboundedEnumViaInteger : Enum a - unboundedEnumViaInteger .BoundedBelowEnum = Nothing - unboundedEnumViaInteger .BoundedAboveEnum = Nothing - unboundedEnumViaInteger .fromEnum = integerToInt ∘ from - unboundedEnumViaInteger .toEnum n = to (intToInteger n) - unboundedEnumViaInteger .succ x = to (from x + 1) - unboundedEnumViaInteger .pred x = to (from x - 1) - unboundedEnumViaInteger .enumFromTo a b = fromTo a b - unboundedEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b - - boundedBelowEnumViaInteger : ⦃ Ord a ⦄ → ⦃ BoundedBelow a ⦄ → Enum a - boundedBelowEnumViaInteger .BoundedBelowEnum = Just it - boundedBelowEnumViaInteger .BoundedAboveEnum = Nothing - boundedBelowEnumViaInteger .fromEnum = integerToInt ∘ from - boundedBelowEnumViaInteger .toEnum n = to (intToInteger n) - boundedBelowEnumViaInteger .succ x = to (from x + 1) - boundedBelowEnumViaInteger .pred x = to (from x - 1) - boundedBelowEnumViaInteger .enumFromTo a b = fromTo a b - boundedBelowEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b - - boundedAboveEnumViaInteger : ⦃ Ord a ⦄ → ⦃ BoundedAbove a ⦄ → Enum a - boundedAboveEnumViaInteger .BoundedBelowEnum = Nothing - boundedAboveEnumViaInteger .BoundedAboveEnum = Just it - boundedAboveEnumViaInteger .fromEnum = integerToInt ∘ from - boundedAboveEnumViaInteger .toEnum n = to (intToInteger n) - boundedAboveEnumViaInteger .succ x = to (from x + 1) - boundedAboveEnumViaInteger .pred x = to (from x - 1) - boundedAboveEnumViaInteger .enumFrom a = fromTo a maxBound - boundedAboveEnumViaInteger .enumFromTo a b = fromTo a b - boundedAboveEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b - - boundedEnumViaInteger : ⦃ Ord a ⦄ → ⦃ Bounded a ⦄ → Enum a - boundedEnumViaInteger .BoundedBelowEnum = Just it - boundedEnumViaInteger .BoundedAboveEnum = Just it - boundedEnumViaInteger .fromEnum = integerToInt ∘ from - boundedEnumViaInteger .toEnum n = to (intToInteger n) - boundedEnumViaInteger .succ x = to (from x + 1) - boundedEnumViaInteger .pred x = to (from x - 1) - boundedEnumViaInteger .enumFromTo a b = fromTo a b - boundedEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b - boundedEnumViaInteger .enumFrom a = fromTo a maxBound - boundedEnumViaInteger .enumFromThen a a₁ = - if a < a₁ then fromThenTo a a₁ maxBound - else fromThenTo a a₁ minBound +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 = boundedBelowEnumViaInteger pos unsafeIntegerToNat + 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 = boundedEnumViaInteger intToInteger integerToInt + 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 = boundedEnumViaInteger wordToInteger integerToWord + 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 = boundedEnumViaInteger (if_then 1 else 0) (_/= 0) + 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 = boundedEnumViaInteger (λ where LT → 0; EQ → 1; GT → 2) - (λ where (pos 0) → LT; (pos 1) → EQ; _ → GT) + 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 = boundedEnumViaInteger (λ _ → 0) λ _ → tt + 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 = boundedEnumViaInteger (pos ∘ c2n) - λ where (pos n) → primNatToChar n; _ → '_' + 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) diff --git a/lib/Haskell/Prim/Foldable.agda b/lib/Haskell/Prim/Foldable.agda index c5a30f56..c94cf66b 100644 --- a/lib/Haskell/Prim/Foldable.agda +++ b/lib/Haskell/Prim/Foldable.agda @@ -88,29 +88,35 @@ open Foldable ⦃...⦄ public {-# COMPILE AGDA2HS Foldable existing-class #-} -- ** instances -private - mkFoldable : DefaultFoldable t → Foldable t - mkFoldable x = record {DefaultFoldable x} - - foldMap=_ : (∀ {b a} → ⦃ Monoid b ⦄ → (a → b) → t a → b) → Foldable t - foldMap= x = record {DefaultFoldable (record {foldMap = x})} instance - iFoldableList : Foldable List - iFoldableList = foldMap= foldMapList + iDefaultFoldableList : DefaultFoldable List + iDefaultFoldableList .DefaultFoldable.foldMap = foldMapList where foldMapList : ⦃ Monoid b ⦄ → (a → b) → List a → b foldMapList f [] = mempty foldMapList f (x ∷ xs) = f x <> foldMapList f xs - iFoldableMaybe : Foldable Maybe - iFoldableMaybe = foldMap= λ where + iFoldableList : Foldable List + iFoldableList = record {DefaultFoldable iDefaultFoldableList} + + iDefaultFoldableMaybe : DefaultFoldable Maybe + iDefaultFoldableMaybe .DefaultFoldable.foldMap = λ where _ Nothing → mempty f (Just x) → f x - iFoldableEither : Foldable (Either a) - iFoldableEither = foldMap= λ where + iFoldableMaybe : Foldable Maybe + iFoldableMaybe = record {DefaultFoldable iDefaultFoldableMaybe} + + iDefaultFoldableEither : DefaultFoldable (Either a) + iDefaultFoldableEither .DefaultFoldable.foldMap = λ where _ (Left _) → mempty f (Right x) → f x + iFoldableEither : Foldable (Either a) + iFoldableEither = record {DefaultFoldable iDefaultFoldableEither} + + iDefaultFoldablePair : DefaultFoldable (a ×_) + iDefaultFoldablePair .DefaultFoldable.foldMap = λ f (_ , x) → f x + iFoldablePair : Foldable (a ×_) - iFoldablePair = foldMap= λ f (_ , x) → f x + iFoldablePair = record {DefaultFoldable iDefaultFoldablePair} diff --git a/lib/Haskell/Prim/Functor.agda b/lib/Haskell/Prim/Functor.agda index 96c065de..f14924bc 100644 --- a/lib/Haskell/Prim/Functor.agda +++ b/lib/Haskell/Prim/Functor.agda @@ -45,34 +45,45 @@ void = tt <$_ infixl 1 _<&>_ infixl 4 _<$>_ _$>_ --- ** instances -private - mkFunctor : DefaultFunctor t → Functor t - mkFunctor x = record {DefaultFunctor x} - - fmap=_ : (∀ {a b} → (a → b) → f a → f b) → Functor f - fmap= x = record {DefaultFunctor (record {fmap = x})} instance + iDefaultFunctorList : DefaultFunctor List + iDefaultFunctorList .DefaultFunctor.fmap = map + iFunctorList : Functor List - iFunctorList = fmap= map + iFunctorList = record{DefaultFunctor iDefaultFunctorList} - iFunctorMaybe : Functor Maybe - iFunctorMaybe = fmap= λ where + iDefaultFunctorMaybe : DefaultFunctor Maybe + iDefaultFunctorMaybe .DefaultFunctor.fmap = λ where f Nothing → Nothing f (Just x) → Just (f x) - iFunctorEither : Functor (Either a) - iFunctorEither = fmap= λ where + iFunctorMaybe : Functor Maybe + iFunctorMaybe = record{DefaultFunctor iDefaultFunctorMaybe} + + iDefaultFunctorEither : DefaultFunctor (Either a) + iDefaultFunctorEither .DefaultFunctor.fmap = λ where f (Left x) → Left x f (Right y) → Right (f y) + iFunctorEither : Functor (Either a) + iFunctorEither = record{DefaultFunctor iDefaultFunctorEither} + + iDefaultFunctorFun : DefaultFunctor (λ b → a → b) + iDefaultFunctorFun .DefaultFunctor.fmap = _∘_ + iFunctorFun : Functor (λ b → a → b) - iFunctorFun = fmap= _∘_ + iFunctorFun = record{DefaultFunctor iDefaultFunctorFun} + + iDefaultFunctorTuple₂ : DefaultFunctor (a ×_) + iDefaultFunctorTuple₂ .DefaultFunctor.fmap = λ f (x , y) → x , f y iFunctorTuple₂ : Functor (a ×_) - iFunctorTuple₂ = fmap= λ f (x , y) → x , f y + iFunctorTuple₂ = record{DefaultFunctor iDefaultFunctorTuple₂} + + iDefaultFunctorTuple₃ : DefaultFunctor (a × b ×_) + iDefaultFunctorTuple₃ .DefaultFunctor.fmap = λ where f (x , y , z) → x , y , f z iFunctorTuple₃ : Functor (a × b ×_) - iFunctorTuple₃ = fmap= λ where f (x , y , z) → x , y , f z + iFunctorTuple₃ = record{DefaultFunctor iDefaultFunctorTuple₃} instance postulate iFunctorIO : Functor IO diff --git a/lib/Haskell/Prim/Monad.agda b/lib/Haskell/Prim/Monad.agda index bfbeadd9..70dcd0cc 100644 --- a/lib/Haskell/Prim/Monad.agda +++ b/lib/Haskell/Prim/Monad.agda @@ -72,26 +72,44 @@ private bind=_ : ⦃ Applicative m ⦄ → (∀ {a b} → m a → (a → m b) → m b) → Monad m bind= x = record {DefaultMonad (record {_>>=_ = x})} instance + iDefaultMonadList : DefaultMonad List + iDefaultMonadList .DefaultMonad._>>=_ = flip concatMap + iMonadList : Monad List - iMonadList = bind= flip concatMap + iMonadList = record {DefaultMonad iDefaultMonadList} + + iDefaultMonadMaybe : DefaultMonad Maybe + iDefaultMonadMaybe .DefaultMonad._>>=_ = flip (maybe Nothing) iMonadMaybe : Monad Maybe - iMonadMaybe = bind= flip (maybe Nothing) + iMonadMaybe = record {DefaultMonad iDefaultMonadMaybe} + + iDefaultMonadEither : DefaultMonad (Either a) + iDefaultMonadEither .DefaultMonad._>>=_ = flip (either Left) iMonadEither : Monad (Either a) - iMonadEither = bind= flip (either Left) + iMonadEither = record {DefaultMonad iDefaultMonadEither} + + iDefaultMonadFun : DefaultMonad (λ b → a → b) + iDefaultMonadFun .DefaultMonad._>>=_ = λ f k r → k (f r) r iMonadFun : Monad (λ b → a → b) - iMonadFun = bind= λ f k r → k (f r) r + iMonadFun = record {DefaultMonad iDefaultMonadFun} + + iDefaultMonadTuple₂ : ⦃ Monoid a ⦄ → DefaultMonad (a ×_) + iDefaultMonadTuple₂ .DefaultMonad._>>=_ = λ (a , x) k → first (a <>_) (k x) iMonadTuple₂ : ⦃ Monoid a ⦄ → Monad (a ×_) - iMonadTuple₂ = bind= λ (a , x) k → first (a <>_) (k x) + iMonadTuple₂ = record {DefaultMonad iDefaultMonadTuple₂} - iMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_) - iMonadTuple₃ = bind= λ where + iDefaultMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonad (a × b ×_) + iDefaultMonadTuple₃ .DefaultMonad._>>=_ = λ 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₃} + instance postulate iMonadIO : Monad IO record MonadFail (m : Set → Set) : Set₁ where diff --git a/lib/Haskell/Prim/Monoid.agda b/lib/Haskell/Prim/Monoid.agda index 09e71b3a..b5e20631 100644 --- a/lib/Haskell/Prim/Monoid.agda +++ b/lib/Haskell/Prim/Monoid.agda @@ -70,50 +70,61 @@ record DefaultMonoid (a : Set) : Set where open Monoid ⦃...⦄ public {-# COMPILE AGDA2HS Monoid existing-class #-} -- ** instances -private - infix 0 mempty=_ - mempty=_ : ⦃ Semigroup a ⦄ → a → Monoid a - mempty= x = record {DefaultMonoid (record {mempty = x})} - - mkMonoid : DefaultMonoid a → Monoid a - mkMonoid x = record {DefaultMonoid x} instance + iDefaultMonoidList : DefaultMonoid (List a) + iDefaultMonoidList .DefaultMonoid.mempty = [] + iMonoidList : Monoid (List a) - iMonoidList = mempty= [] + iMonoidList = record{DefaultMonoid iDefaultMonoidList} + + iDefaultMonoidMaybe : ⦃ Semigroup a ⦄ → DefaultMonoid (Maybe a) + iDefaultMonoidMaybe .DefaultMonoid.mempty = Nothing iMonoidMaybe : ⦃ Semigroup a ⦄ → Monoid (Maybe a) - iMonoidMaybe = mempty= Nothing + iMonoidMaybe = record{DefaultMonoid iDefaultMonoidMaybe} + + iDefaultMonoidFun : ⦃ Monoid b ⦄ → DefaultMonoid (a → b) + iDefaultMonoidFun .DefaultMonoid.mempty = λ _ → mempty iMonoidFun : ⦃ Monoid b ⦄ → Monoid (a → b) - iMonoidFun = mempty= λ _ → mempty + iMonoidFun = record{DefaultMonoid iDefaultMonoidFun} + + iDefaultMonoidUnit : DefaultMonoid ⊤ + iDefaultMonoidUnit .DefaultMonoid.mempty = tt iMonoidUnit : Monoid ⊤ - iMonoidUnit = mempty= tt + iMonoidUnit = record{DefaultMonoid iDefaultMonoidUnit} + + iDefaultMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonoid (a × b) + iDefaultMonoidTuple₂ .DefaultMonoid.mempty = (mempty , mempty) iMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monoid (a × b) - iMonoidTuple₂ = mempty= (mempty , mempty) + iMonoidTuple₂ = record{DefaultMonoid iDefaultMonoidTuple₂} + + 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₃ = mempty= (mempty , mempty , mempty) + iMonoidTuple₃ = record{DefaultMonoid iDefaultMonoidTuple₃} open DefaultMonoid MonoidEndo : Monoid (a → a) -MonoidEndo = mkMonoid λ where - .mempty → id - .super ._<>_ → _∘_ +MonoidEndo = record {DefaultMonoid (λ where + .mempty → id + .super ._<>_ → _∘_)} MonoidEndoᵒᵖ : Monoid (a → a) -MonoidEndoᵒᵖ = mkMonoid λ where +MonoidEndoᵒᵖ = record {DefaultMonoid (λ where .mempty → id - .super ._<>_ → flip _∘_ + .super ._<>_ → flip _∘_) } MonoidConj : Monoid Bool -MonoidConj = mkMonoid λ where +MonoidConj = record {DefaultMonoid (λ where .mempty → True - .super ._<>_ → _&&_ + .super ._<>_ → _&&_)} MonoidDisj : Monoid Bool -MonoidDisj = mkMonoid λ where +MonoidDisj = record {DefaultMonoid (λ where .mempty → False - .super ._<>_ → _||_ + .super ._<>_ → _||_)} diff --git a/lib/Haskell/Prim/Ord.agda b/lib/Haskell/Prim/Ord.agda index 9f2403da..29e29e4b 100644 --- a/lib/Haskell/Prim/Ord.agda +++ b/lib/Haskell/Prim/Ord.agda @@ -51,37 +51,57 @@ record Ord (a : Set) : Set where infix 4 _<_ _>_ _<=_ _>=_ +record OrdFromCompare (a : Set) : Set where + field + compare : a → a → Ordering + overlap ⦃ super ⦄ : Eq a + + _<_ : a → a → Bool + x < y = compare x y == LT + + _>_ : a → a → Bool + x > y = compare x y == GT + + _>=_ : a → a → Bool + x >= y = compare x y /= LT + + _<=_ : a → a → Bool + x <= y = compare x y /= GT + + max : a → a → a + max x y = if compare x y == LT then y else x + + min : a → a → a + min x y = if compare x y == GT then y else x + +record OrdFromLessThan (a : Set) : Set where + field + _<_ : a → a → Bool + overlap ⦃ super ⦄ : Eq a + + compare : a → a → Ordering + compare x y = if x < y then LT else if x == y then EQ else GT + + _>_ : a → a → Bool + x > y = y < x + + _>=_ : a → a → Bool + x >= y = y < x || x == y + + _<=_ : a → a → Bool + x <= y = x < y || x == y + + max : a → a → a + max x y = if x < y then y else x + + min : a → a → a + min x y = if y < x then y else x + + open Ord ⦃...⦄ public {-# COMPILE AGDA2HS Ord existing-class #-} -ordFromCompare : ⦃ Eq a ⦄ → (a → a → Ordering) → Ord a -ordFromCompare cmp .compare = cmp -ordFromCompare cmp ._<_ x y = cmp x y == LT -ordFromCompare cmp ._>_ x y = cmp x y == GT -ordFromCompare cmp ._<=_ x y = cmp x y /= GT -ordFromCompare cmp ._>=_ x y = cmp x y /= LT -ordFromCompare cmp .max x y = if cmp x y == LT then y else x -ordFromCompare cmp .min x y = if cmp x y == GT then y else x - -ordFromLessThan : ⦃ Eq a ⦄ → (a → a → Bool) → Ord a -ordFromLessThan _<_ .compare x y = if x < y then LT else if x == y then EQ else GT -ordFromLessThan _<_ ._<_ x y = x < y -ordFromLessThan _<_ ._>_ x y = y < x -ordFromLessThan _<_ ._<=_ x y = x < y || x == y -ordFromLessThan _<_ ._>=_ x y = y < x || x == y -ordFromLessThan _<_ .max x y = if x < y then y else x -ordFromLessThan _<_ .min x y = if y < x then y else x - -ordFromLessEq : ⦃ Eq a ⦄ → (a → a → Bool) → Ord a -ordFromLessEq _<=_ .compare x y = if x == y then EQ else if x <= y then LT else GT -ordFromLessEq _<=_ ._<_ x y = x <= y && not (x == y) -ordFromLessEq _<=_ ._>_ x y = y <= x && not (x == y) -ordFromLessEq _<=_ ._<=_ x y = x <= y -ordFromLessEq _<=_ ._>=_ x y = y <= x -ordFromLessEq _<=_ .max x y = if y <= x then x else y -ordFromLessEq _<=_ .min x y = if x <= y then x else y - private compareFromLt : ⦃ Eq a ⦄ → (a → a → Bool) → a → a → Ordering compareFromLt _<_ x y = if x < y then LT else if x == y then EQ else GT @@ -98,44 +118,75 @@ private minNat (suc x) (suc y) = suc (minNat x y) instance + iOrdFromLessThanNat : OrdFromLessThan Nat + iOrdFromLessThanNat .OrdFromLessThan._<_ = ltNat + iOrdNat : Ord Nat - iOrdNat = record (ordFromLessThan ltNat) - { max = maxNat + iOrdNat = record + { OrdFromLessThan iOrdFromLessThanNat + ; max = maxNat ; min = minNat } + iOrdFromLessThanInteger : OrdFromLessThan Integer + iOrdFromLessThanInteger .OrdFromLessThan._<_ = ltInteger + iOrdInteger : Ord Integer - iOrdInteger = ordFromLessThan ltInteger + iOrdInteger = record {OrdFromLessThan iOrdFromLessThanInteger} + + iOrdFromLessThanInt : OrdFromLessThan Int + iOrdFromLessThanInt .OrdFromLessThan._<_ = ltInt iOrdInt : Ord Int - iOrdInt = ordFromLessThan ltInt + iOrdInt = record {OrdFromLessThan iOrdFromLessThanInt} + + iOrdFromLessThanWord : OrdFromLessThan Word + iOrdFromLessThanWord .OrdFromLessThan._<_ = ltWord iOrdWord : Ord Word - iOrdWord = ordFromLessThan ltWord + iOrdWord = record {OrdFromLessThan iOrdFromLessThanWord} + + iOrdFromLessThanDouble : OrdFromLessThan Double + iOrdFromLessThanDouble .OrdFromLessThan._<_ = primFloatLess iOrdDouble : Ord Double - iOrdDouble = ordFromLessThan primFloatLess + iOrdDouble = record {OrdFromLessThan iOrdFromLessThanDouble} + + iOrdFromLessThanChar : OrdFromLessThan Char + iOrdFromLessThanChar .OrdFromLessThan._<_ x y = c2n x < c2n y iOrdChar : Ord Char - iOrdChar = ordFromLessThan λ x y → c2n x < c2n y + iOrdChar = record {OrdFromLessThan iOrdFromLessThanChar} - iOrdBool : Ord Bool - iOrdBool = ordFromCompare λ where + 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 = ordFromCompare λ _ _ → EQ + iOrdUnit = record {OrdFromCompare iOrdFromCompareUnit} - iOrdTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (a × b) - iOrdTuple₂ = ordFromCompare λ where + 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 c ⦄ → Ord (a × b × c) - iOrdTuple₃ = ordFromCompare λ where + 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₃} + compareList : ⦃ Ord a ⦄ → List a → List a → Ordering compareList [] [] = EQ compareList [] (_ ∷ _) = LT @@ -143,25 +194,34 @@ compareList (_ ∷ _) [] = GT compareList (x ∷ xs) (y ∷ ys) = compare x y <> compareList xs ys instance + iOrdFromCompareList : ⦃ Ord a ⦄ → OrdFromCompare (List a) + iOrdFromCompareList .OrdFromCompare.compare = compareList + iOrdList : ⦃ Ord a ⦄ → Ord (List a) - iOrdList = ordFromCompare compareList + iOrdList = record {OrdFromCompare iOrdFromCompareList} - iOrdMaybe : ⦃ Ord a ⦄ → Ord (Maybe a) - iOrdMaybe = ordFromCompare λ where + 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 - iOrdEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (Either a b) - iOrdEither = ordFromCompare λ where + 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 - iOrdOrdering : Ord Ordering - iOrdOrdering = ordFromCompare λ where + 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 @@ -169,3 +229,6 @@ instance EQ GT → LT GT EQ → GT GT GT → EQ + + iOrdOrdering : Ord Ordering + iOrdOrdering = record {OrdFromCompare iOrdFromCompareOrdering} diff --git a/lib/Haskell/Prim/Show.agda b/lib/Haskell/Prim/Show.agda index 1d8a8c69..071e6d84 100644 --- a/lib/Haskell/Prim/Show.agda +++ b/lib/Haskell/Prim/Show.agda @@ -70,59 +70,90 @@ shows : ⦃ Show a ⦄ → a → ShowS shows = showsPrec 0 {-# COMPILE AGDA2HS Show existing-class #-} --- ** instances -private - infix 0 showsPrec=_ show=_ - showsPrec=_ : (Int → a → ShowS) → Show a - showsPrec=_ x = record {Show₁ (record {showsPrec = x})} - - show=_ : (a → String) → Show a - show= x = record {Show₂ (record {show = x})} +-- ** instances instance + iShow₂Nat : Show₂ Nat + iShow₂Nat .Show₂.show = primStringToList ∘ primShowNat + iShowNat : Show Nat - iShowNat = show= (primStringToList ∘ primShowNat) + iShowNat = record {Show₂ iShow₂Nat} + + iShow₂Integer : Show₂ Integer + iShow₂Integer .Show₂.show = showInteger iShowInteger : Show Integer - iShowInteger = show= showInteger + iShowInteger = record {Show₂ iShow₂Integer} + + iShow₂Int : Show₂ Int + iShow₂Int .Show₂.show = showInt iShowInt : Show Int - iShowInt = show= showInt + iShowInt = record{Show₂ iShow₂Int} + + iShow₂Word : Show₂ Word + iShow₂Word .Show₂.show = showWord iShowWord : Show Word - iShowWord = show= showWord + iShowWord = record{Show₂ iShow₂Word} + + iShow₂Double : Show₂ Double + iShow₂Double .Show₂.show = primStringToList ∘ primShowFloat iShowDouble : Show Double - iShowDouble = show= (primStringToList ∘ primShowFloat) + iShowDouble = record{Show₂ iShow₂Double} + + iShow₂Bool : Show₂ Bool + iShow₂Bool .Show₂.show = λ where False → "False"; True → "True" iShowBool : Show Bool - iShowBool = show= λ where False → "False"; True → "True" + iShowBool = record{Show₂ iShow₂Bool} + + iShow₁Char : Show₁ Char + iShow₁Char .Show₁.showsPrec _ = showString ∘ primStringToList ∘ primShowChar iShowChar : Show Char - iShowChar = showsPrec= λ _ → showString ∘ primStringToList ∘ primShowChar + iShowChar = record{Show₁ iShow₁Char} + + iShow₁List : ⦃ Show a ⦄ → Show₁ (List a) + iShow₁List .Show₁.showsPrec _ = showList iShowList : ⦃ Show a ⦄ → Show (List a) - iShowList = showsPrec= λ _ → showList + 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 + instance - iShowMaybe : ⦃ Show a ⦄ → Show (Maybe a) - iShowMaybe = showsPrec= λ where + iShow₁Maybe : ⦃ Show a ⦄ → Show₁ (Maybe a) + iShow₁Maybe .Show₁.showsPrec = λ where p Nothing → showString "Nothing" p (Just x) → showApp₁ p "Just" x - iShowEither : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (Either a b) - iShowEither = showsPrec= λ where + 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 + iShowEither : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (Either a b) + iShowEither = record{Show₁ iShow₁Either} + instance - iShowTuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (a × b) - iShowTuple₂ = showsPrec= λ _ → λ where + 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 c ⦄ → Show (a × b × c) - iShowTuple₃ = showsPrec= λ _ → λ where + 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 ")" + + iShowTuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show (a × b × c) + iShowTuple₃ = record{Show₁ iShow₁Tuple₃} diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs index a62f80a5..e43d1c8e 100644 --- a/src/Agda2Hs/Compile/Utils.hs +++ b/src/Agda2Hs/Compile/Utils.hs @@ -232,32 +232,42 @@ isInlinedFunction q = do _ -> return False checkInstance :: Term -> C () -checkInstance u | varOrDef u = liftTCM $ noConstraints $ do +checkInstance u = do reportSDoc "agda2hs.checkInstance" 12 $ text "checkInstance" <+> prettyTCM u - t <- infer u - reportSDoc "agda2hs.checkInstance" 15 $ text " inferred type:" <+> prettyTCM t - (m, v) <- newInstanceMeta "" t - reportSDoc "agda2hs.checkInstance" 15 $ text " instance meta:" <+> prettyTCM m - findInstance m Nothing - reportSDoc "agda2hs.checkInstance" 15 $ text " inferred instance:" <+> (prettyTCM =<< instantiate v) - reportSDoc "agda2hs.checkInstance" 65 $ text " inferred instance:" <+> (pure . P.pretty =<< instantiate v) - reportSDoc "agda2hs.checkInstance" 65 $ text " checking instance:" <+> (pure . P.pretty =<< instantiate u) - equalTerm t u v `catchError` \_ -> - genericDocError =<< text "illegal instance: " <+> prettyTCM u + reduce u >>= \case + Var x es -> do + unlessM (isInstance <$> domOfBV x) illegalInstance + checkInstanceElims es + Def f es -> do + unlessM (isJust . defInstance <$> getConstInfo f) illegalInstance + checkInstanceElims es + -- We need to compile applications of `fromNat`, `fromNeg`, and + -- `fromString` where the constraint type is ⊤ or IsTrue .... Ideally + -- this constraint would be marked as erased but this would involve + -- changing Agda builtins. + Con c _ _ + | prettyShow (conName c) == "Agda.Builtin.Unit.tt" || + prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" || + prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" -> return () + _ -> illegalInstance + where - varOrDef Var{} = True - varOrDef Def{} = True - varOrDef _ = False - --- We need to compile applications of `fromNat`, `fromNeg`, and --- `fromString` where the constraint type is ⊤ or IsTrue .... Ideally --- this constraint would be marked as erased but this would involve --- changing Agda builtins. -checkInstance u@(Con c _ _) - | prettyShow (conName c) == "Agda.Builtin.Unit.tt" || - prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" || - prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" = return () -checkInstance u = genericDocError =<< text "illegal instance: " <+> prettyTCM u + illegalInstance :: C () + illegalInstance = do + reportSDoc "agda2hs.checkInstance" 15 $ text "illegal instance: " <+> pretty u + genericDocError =<< text "illegal instance: " <+> prettyTCM u + + checkInstanceElims :: Elims -> C () + checkInstanceElims = mapM_ checkInstanceElim + + checkInstanceElim :: Elim -> C () + checkInstanceElim (Apply v) = case getHiding v of + Instance{} -> checkInstance $ unArg v + Hidden -> return () + NotHidden -> return () + checkInstanceElim IApply{} = illegalInstance + checkInstanceElim (Proj _ f) = + unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance compileLocal :: C a -> C a compileLocal = local $ \e -> e { compilingLocal = True } diff --git a/test/Issue301.agda b/test/Issue301.agda index 16793fc4..252555da 100644 --- a/test/Issue301.agda +++ b/test/Issue301.agda @@ -27,8 +27,9 @@ instance MyDataSemigroup ._<>_ = _><_ {-# COMPILE AGDA2HS MyDataSemigroup #-} -myDataDefaultMonoid : DefaultMonoid (MyData a) -DefaultMonoid.mempty myDataDefaultMonoid = Nuttin' +instance + myDataDefaultMonoid : DefaultMonoid (MyData a) + DefaultMonoid.mempty myDataDefaultMonoid = Nuttin' instance MyDataMonoid : Monoid (MyData a) diff --git a/test/golden/ExplicitInstance2.err b/test/golden/ExplicitInstance2.err index a635d6a8..2a4c6567 100644 --- a/test/golden/ExplicitInstance2.err +++ b/test/golden/ExplicitInstance2.err @@ -1,2 +1,2 @@ test/Fail/ExplicitInstance2.agda:13,1-5 -No instance of type HasDefault Bool was found in scope. +illegal instance: λ { .Fail.ExplicitInstance2.theDefault → True }