src/Symantic/Semantics/Forall.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE EmptyCase #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE QuantifiedConstraints #-}
   5 {-# LANGUAGE RankNTypes #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7
   8 -- | This module provides the 'Forall' semantic
   9 -- which preserves the polymorphism of the semantic.
  10 -- Useful when parsing the syntax from a text
  11 -- (ie. when the domain-specific language
  12 -- is not embedded into a Haskell file).
  13 module Symantic.Semantics.Forall where
  14
  15 import Control.Applicative (Applicative (..))
  16 import Control.Monad (Monad (..))
  17 import Data.Bool (Bool (..))
  18 import Data.Eq (Eq (..))
  19 import Data.Eq qualified as Eq
  20 import Data.Function qualified as Fun
  21 import Data.Functor (Functor (..))
  22 import Data.Kind (Type)
  23 import Data.Tuple qualified as Tuple
  24 import Text.Show (Show (..))
  25 import Unsafe.Coerce (unsafeCoerce)
  26
  27 import Symantic.Syntaxes.Classes
  28
  29 -- * Type 'Forall'
  30 newtype Forall (syns :: [Syntax]) (a :: Type)
  31   = Forall (forall sem. Syntaxes syns sem => sem a)
  32
  33 {-# INLINE forall1 #-}
  34 forall1 ::
  35   (forall sem. Syntaxes syns sem => sem a -> sem b) ->
  36   Forall syns a -> Forall syns b
  37 forall1 f (Forall a) = Forall (f a)
  38
  39 {-# INLINE forall2 #-}
  40 forall2 ::
  41   (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c) ->
  42   Forall syns a -> Forall syns b -> Forall syns c
  43 forall2 f (Forall a) (Forall b) = Forall (f a b)
  44
  45 {-# INLINE forall3 #-}
  46 forall3 ::
  47   (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c -> sem d) ->
  48   Forall syns a -> Forall syns b -> Forall syns c -> Forall syns d
  49 forall3 f (Forall a) (Forall b) (Forall c) = Forall (f a b c)
  50
  51 {-# INLINE forall4 #-}
  52 forall4 ::
  53   (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c -> sem d -> sem e) ->
  54   Forall syns a -> Forall syns b -> Forall syns c -> Forall syns d -> Forall syns e
  55 forall4 f (Forall a) (Forall b) (Forall c) (Forall d) = Forall (f a b c d)
  56
  57 instance
  58   ( forall sem. Syntaxes syns sem => Functor sem
  59   ) => Functor (Forall syns) where
  60   fmap f = forall1 (fmap f)
  61   (<$) a = forall1 (a <$)
  62 instance
  63   ( forall sem. Syntaxes syns sem => Applicative sem
  64   , Functor (Forall syns)
  65   ) => Applicative (Forall syns) where
  66   pure a = Forall (pure a)
  67   liftA2 f = forall2 (liftA2 f)
  68   (<*>) = forall2 (<*>)
  69   (<*)  = forall2 (<*)
  70   (*>)  = forall2 (*>)
  71 instance
  72   ( forall sem. Syntaxes syns sem => Monad sem
  73   , Applicative (Forall syns)
  74   ) => Monad (Forall syns) where
  75   (>>=) (Forall sa) f = Forall (sa >>= \a -> case f a of Forall sb -> sb)
  76   return = pure
  77   (>>) = (*>)
  78 instance
  79   ( forall sem. Syntaxes syns sem => Varable sem
  80   ) => Varable (Forall syns) where
  81   var = forall1 var
  82 instance
  83   (forall sem. Syntaxes syns sem => Instantiable sem) =>
  84   Instantiable (Forall syns)
  85   where
  86   (.@) = forall2 (.@)
  87 instance
  88   ( forall sem. Syntaxes syns sem => Abstractable sem
  89   , forall sem. Syntaxes syns sem => Instantiable sem
  90   ) => Abstractable (Forall syns) where
  91   lam f = Forall (lam (\a -> let Forall b = f (forallSem a) in b))
  92     where
  93       -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
  94       forallSem :: sem a -> Forall syns a
  95       forallSem a = Forall (unsafeCoerce a)
  96 instance
  97   ( forall sem. Syntaxes syns sem => Unabstractable sem
  98   ) => Unabstractable (Forall syns) where
  99   ap = Forall ap
 100   const = Forall const
 101   id = Forall id
 102   (.) = Forall (.)
 103   flip = Forall flip
 104   ($) = Forall ($)
 105 instance
 106   ( forall sem. Syntaxes syns sem => Constantable c sem
 107   ) => Constantable c (Forall syns) where
 108   constant c = Forall (constant c)
 109 instance
 110   ( forall sem. Syntaxes syns sem => Eitherable sem
 111   ) => Eitherable (Forall syns) where
 112   either = Forall either
 113   left = Forall left
 114   right = Forall right
 115 instance
 116   ( forall sem. Syntaxes syns sem => Equalable sem
 117   ) => Equalable (Forall syns) where
 118   equal = Forall equal
 119 instance
 120   ( forall sem. Syntaxes syns sem => IfThenElseable sem
 121   ) => IfThenElseable (Forall syns) where
 122   ifThenElse = forall3 ifThenElse
 123 instance
 124   ( forall sem. Syntaxes syns sem => Inferable c sem
 125   ) => Inferable c (Forall syns) where
 126   infer = Forall infer
 127 instance
 128   ( forall sem. Syntaxes syns sem => Listable sem
 129   ) => Listable (Forall syns) where
 130   cons = Forall cons
 131   nil = Forall nil
 132 instance
 133   ( forall sem. Syntaxes syns sem => Maybeable sem
 134   ) => Maybeable (Forall syns) where
 135   just = Forall just
 136   nothing = Forall nothing
 137 instance
 138   ( forall sem. Syntaxes syns sem => IsoFunctor sem
 139   ) => IsoFunctor (Forall syns) where
 140   (<%>) iso = forall1 (iso <%>)
 141 instance
 142   ( forall sem. Syntaxes syns sem => ProductFunctor sem
 143   , forall sem. Syntaxes syns sem => IsoFunctor sem
 144   , Syntaxes syns (Forall syns)
 145   ) => ProductFunctor (Forall syns) where
 146   (<.>) = forall2 (<.>)
 147   ra <. rb = Iso Tuple.fst (,()) <%> (ra <.> rb)
 148   ra .> rb = Iso Tuple.snd ((),) <%> (ra <.> rb)
 149 instance
 150   ( forall sem. Syntaxes syns sem => SumFunctor sem
 151   ) => SumFunctor (Forall syns) where
 152   (<+>) = forall2 (<+>)
 153 instance
 154   ( forall sem. Syntaxes syns sem => AlternativeFunctor sem
 155   ) => AlternativeFunctor (Forall syns) where
 156   (<|>) = forall2 (<|>)
 157 instance
 158   ( forall sem. Syntaxes syns sem => Dicurryable sem
 159   ) => Dicurryable (Forall syns) where
 160   dicurry args constr destr = forall1 (dicurry args constr destr)
 161 instance
 162   ( forall sem. Syntaxes syns sem => Emptyable sem
 163   ) => Emptyable (Forall syns) where
 164   empty = Forall empty
 165 instance
 166   ( forall sem. Syntaxes syns sem => Semigroupable sem
 167   ) => Semigroupable (Forall syns) where
 168   concat = Forall concat
 169 instance
 170   ( forall sem. Syntaxes syns sem => Optionable sem
 171   ) => Optionable (Forall syns) where
 172   optional = forall1 optional
 173 instance
 174   ( forall sem. Syntaxes syns sem => Repeatable sem
 175   ) => Repeatable (Forall syns) where
 176   many0 = forall1 many0
 177   many1 = forall1 many1
 178 instance
 179   ( forall sem. Syntaxes syns sem => Substractable sem
 180   ) => Substractable (Forall syns) where
 181   (<->) = forall2 (<->)
 182 instance
 183   ( forall sem. Syntaxes syns sem => Voidable sem
 184   ) => Voidable (Forall syns) where
 185   void a = forall1 (void a)
 186
 187 -- * Type 'PerSyntax'
 188 data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
 189   PerSyntaxZ :: a syn -> PerSyntax (syn ': syns) a
 190   PerSyntaxS :: PerSyntax syns a -> PerSyntax (skipSyn ': syns) a
 191
 192 instance Eq (PerSyntax '[] a) where
 193   (==) = \case {}
 194 instance
 195   ( Eq (a syn)
 196   , Eq (PerSyntax syns a)
 197   ) =>
 198   Eq (PerSyntax (syn ': syns) a)
 199   where
 200   PerSyntaxZ x == PerSyntaxZ y = x Eq.== y
 201   PerSyntaxS x == PerSyntaxS y = x Eq.== y
 202   _ == _ = False
 203
 204 instance Show (PerSyntax '[] a) where
 205   showsPrec _p = \case {}
 206 instance
 207   ( Show (a syn)
 208   , Show (PerSyntax syns a)
 209   ) =>
 210   Show (PerSyntax (syn ': syns) a)
 211   where
 212   showsPrec p = \case
 213     PerSyntaxZ a -> showsPrec p a
 214     PerSyntaxS s -> showsPrec p s
 215
 216 -- ** Class 'PerSyntaxable'
 217 class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
 218   perSyntax :: a syn -> PerSyntax syns a
 219 instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
 220   perSyntax = PerSyntaxZ
 221 instance PerSyntaxable syns syn => PerSyntaxable (skipSyn ': syns) syn where
 222   perSyntax = PerSyntaxS Fun.. perSyntax