iface: add many `Forall` instances

diff --git a/src/Symantic/Semantics/Forall.hs b/src/Symantic/Semantics/Forall.hs
index c959c5f341815ace63559fe69d492f7d9c3f1237..ae64ac394b3f405868364346efb3566601125a66 100644 (file)
--- a/src/Symantic/Semantics/Forall.hs
+++ b/src/Symantic/Semantics/Forall.hs
@@ -16,32 +16,58 @@ import Control.Applicative (Applicative (..))
 import Control.Monad (Monad (..))
 import Data.Bool (Bool (..))
 import Data.Eq (Eq (..))
 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.Functor (Functor (..))
 import Data.Kind (Type)

+import Data.Tuple qualified as Tuple

 import Text.Show (Show (..))
 import Unsafe.Coerce (unsafeCoerce)
 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)
 
 
 -- * 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
 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)
 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)
 instance
   ( forall sem. Syntaxes syns sem => Monad sem
   , Applicative (Forall syns)


@@ -49,11 +75,15 @@ instance
   (>>=) (Forall sa) f = Forall (sa >>= \a -> case f a of Forall sb -> sb)
   return = pure
   (>>) = (*>)
   (>>=) (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
 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
 instance
   ( forall sem. Syntaxes syns sem => Abstractable sem
   , forall sem. Syntaxes syns sem => Instantiable sem


@@ -72,6 +102,87 @@ instance
   (.) = Forall (.)
   flip = Forall flip
   ($) = Forall ($)
   (.) = 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
 
 -- * Type 'PerSyntax'
 data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where


@@ -86,8 +197,8 @@ instance
   ) =>
   Eq (PerSyntax (syn ': syns) a)
   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
   _ == _ = False
 
 instance Show (PerSyntax '[] a) where