import Control.Monad (Monad (..))
import Data.Bool (Bool (..))
import Data.Eq (Eq (..))
+import Data.Eq qualified as Eq
+import Data.Function qualified as Fun
import Data.Functor (Functor (..))
import Data.Kind (Type)
+import Data.Tuple qualified as Tuple
import Text.Show (Show (..))
import Unsafe.Coerce (unsafeCoerce)
-import qualified Data.Function as Fun
-import Symantic.Syntaxes.Classes (Abstractable (..), Syntax, Syntaxes, Instantiable (..), Unabstractable (..))
+import Symantic.Syntaxes.Classes
-- * Type 'Forall'
newtype Forall (syns :: [Syntax]) (a :: Type)
= Forall (forall sem. Syntaxes syns sem => sem a)
+{-# INLINE forall1 #-}
+forall1 ::
+ (forall sem. Syntaxes syns sem => sem a -> sem b) ->
+ Forall syns a -> Forall syns b
+forall1 f (Forall a) = Forall (f a)
+
+{-# INLINE forall2 #-}
+forall2 ::
+ (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c) ->
+ Forall syns a -> Forall syns b -> Forall syns c
+forall2 f (Forall a) (Forall b) = Forall (f a b)
+
+{-# INLINE forall3 #-}
+forall3 ::
+ (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c -> sem d) ->
+ Forall syns a -> Forall syns b -> Forall syns c -> Forall syns d
+forall3 f (Forall a) (Forall b) (Forall c) = Forall (f a b c)
+
+{-# INLINE forall4 #-}
+forall4 ::
+ (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c -> sem d -> sem e) ->
+ Forall syns a -> Forall syns b -> Forall syns c -> Forall syns d -> Forall syns e
+forall4 f (Forall a) (Forall b) (Forall c) (Forall d) = Forall (f a b c d)
+
instance
( forall sem. Syntaxes syns sem => Functor sem
) => Functor (Forall syns) where
- fmap f (Forall sem) = Forall (fmap f sem)
- a <$ (Forall sem) = Forall (a <$ sem)
+ fmap f = forall1 (fmap f)
+ (<$) a = forall1 (a <$)
instance
( forall sem. Syntaxes syns sem => Applicative sem
, Functor (Forall syns)
) => Applicative (Forall syns) where
pure a = Forall (pure a)
- liftA2 f (Forall a) (Forall b) = Forall (liftA2 f a b)
- (<*>) (Forall f) (Forall a) = Forall ((<*>) f a)
- (<*) (Forall f) (Forall a) = Forall ((<*) f a)
- (*>) (Forall f) (Forall a) = Forall ((*>) f a)
+ liftA2 f = forall2 (liftA2 f)
+ (<*>) = forall2 (<*>)
+ (<*) = forall2 (<*)
+ (*>) = forall2 (*>)
instance
( forall sem. Syntaxes syns sem => Monad sem
, Applicative (Forall syns)
(>>=) (Forall sa) f = Forall (sa >>= \a -> case f a of Forall sb -> sb)
return = pure
(>>) = (*>)
+instance
+ ( forall sem. Syntaxes syns sem => Varable sem
+ ) => Varable (Forall syns) where
+ var = forall1 var
instance
(forall sem. Syntaxes syns sem => Instantiable sem) =>
Instantiable (Forall syns)
where
- Forall a2b .@ Forall a = Forall (a2b .@ a)
+ (.@) = forall2 (.@)
instance
( forall sem. Syntaxes syns sem => Abstractable sem
, forall sem. Syntaxes syns sem => Instantiable sem
(.) = Forall (.)
flip = Forall flip
($) = Forall ($)
+instance
+ ( forall sem. Syntaxes syns sem => Constantable c sem
+ ) => Constantable c (Forall syns) where
+ constant c = Forall (constant c)
+instance
+ ( forall sem. Syntaxes syns sem => Eitherable sem
+ ) => Eitherable (Forall syns) where
+ either = Forall either
+ left = Forall left
+ right = Forall right
+instance
+ ( forall sem. Syntaxes syns sem => Equalable sem
+ ) => Equalable (Forall syns) where
+ equal = Forall equal
+instance
+ ( forall sem. Syntaxes syns sem => IfThenElseable sem
+ ) => IfThenElseable (Forall syns) where
+ ifThenElse = forall3 ifThenElse
+instance
+ ( forall sem. Syntaxes syns sem => Inferable c sem
+ ) => Inferable c (Forall syns) where
+ infer = Forall infer
+instance
+ ( forall sem. Syntaxes syns sem => Listable sem
+ ) => Listable (Forall syns) where
+ cons = Forall cons
+ nil = Forall nil
+instance
+ ( forall sem. Syntaxes syns sem => Maybeable sem
+ ) => Maybeable (Forall syns) where
+ just = Forall just
+ nothing = Forall nothing
+instance
+ ( forall sem. Syntaxes syns sem => IsoFunctor sem
+ ) => IsoFunctor (Forall syns) where
+ (<%>) iso = forall1 (iso <%>)
+instance
+ ( forall sem. Syntaxes syns sem => ProductFunctor sem
+ , forall sem. Syntaxes syns sem => IsoFunctor sem
+ , Syntaxes syns (Forall syns)
+ ) => ProductFunctor (Forall syns) where
+ (<.>) = forall2 (<.>)
+ ra <. rb = Iso Tuple.fst (,()) <%> (ra <.> rb)
+ ra .> rb = Iso Tuple.snd ((),) <%> (ra <.> rb)
+instance
+ ( forall sem. Syntaxes syns sem => SumFunctor sem
+ ) => SumFunctor (Forall syns) where
+ (<+>) = forall2 (<+>)
+instance
+ ( forall sem. Syntaxes syns sem => AlternativeFunctor sem
+ ) => AlternativeFunctor (Forall syns) where
+ (<|>) = forall2 (<|>)
+instance
+ ( forall sem. Syntaxes syns sem => Dicurryable sem
+ ) => Dicurryable (Forall syns) where
+ dicurry args constr destr = forall1 (dicurry args constr destr)
+instance
+ ( forall sem. Syntaxes syns sem => Emptyable sem
+ ) => Emptyable (Forall syns) where
+ empty = Forall empty
+instance
+ ( forall sem. Syntaxes syns sem => Semigroupable sem
+ ) => Semigroupable (Forall syns) where
+ concat = Forall concat
+instance
+ ( forall sem. Syntaxes syns sem => Optionable sem
+ ) => Optionable (Forall syns) where
+ optional = forall1 optional
+instance
+ ( forall sem. Syntaxes syns sem => Repeatable sem
+ ) => Repeatable (Forall syns) where
+ many0 = forall1 many0
+ many1 = forall1 many1
+instance
+ ( forall sem. Syntaxes syns sem => Substractable sem
+ ) => Substractable (Forall syns) where
+ (<->) = forall2 (<->)
+instance
+ ( forall sem. Syntaxes syns sem => Voidable sem
+ ) => Voidable (Forall syns) where
+ void a = forall1 (void a)
-- * Type 'PerSyntax'
data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
) =>
Eq (PerSyntax (syn ': syns) a)
where
- PerSyntaxZ x == PerSyntaxZ y = x == y
- PerSyntaxS x == PerSyntaxS y = x == y
+ PerSyntaxZ x == PerSyntaxZ y = x Eq.== y
+ PerSyntaxS x == PerSyntaxS y = x Eq.== y
_ == _ = False
instance Show (PerSyntax '[] a) where