{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}

#ifndef MIN_VERSION_GLASGOW_HASKELL
#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0
#endif
  -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10

#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0)
#else
{-# LANGUAGE OverlappingInstances #-}
#endif

-- | Generic representation of typed syntax trees
--
-- For details, see: A Generic Abstract Syntax Model for Embedded Languages
-- (ICFP 2012, <https://emilaxelsson.github.io/documents/axelsson2012generic.pdf>).

module Language.Syntactic.Syntax
    ( -- * Syntax trees
      AST (..)
    , ASTF
    , ASTFull (..)
    , Full (..)
    , (:->) (..)
    , SigRep (..)
    , Signature (..)
    , DenResult
    , Symbol (..)
    , size
      -- * Smart constructors
    , SmartFun
    , SmartSig
    , SmartSym
    , smartSym'
      -- * Open symbol domains
    , (:+:) (..)
    , Project (..)
    , (:<:) (..)
    , smartSym
    , smartSymTyped
    , Empty
      -- * Existential quantification
    , E (..)
    , liftE
    , liftE2
    , EF (..)
    , liftEF
    , liftEF2
      -- * Type casting expressions
    , Typed (..)
    , injT
    , castExpr
      -- * Misc.
    , NFData1 (..)
    , symType
    , prjP
    ) where



import Control.DeepSeq (NFData (..))
import Data.Typeable
#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0)
#else
import Data.Foldable (Foldable)
import Data.Proxy  -- Needed by GHC < 7.8
import Data.Traversable (Traversable)
#endif



--------------------------------------------------------------------------------
-- * Syntax trees
--------------------------------------------------------------------------------

-- | Generic abstract syntax tree, parameterized by a symbol domain
--
-- @(`AST` sym (a `:->` b))@ represents a partially applied (or unapplied)
-- symbol, missing at least one argument, while @(`AST` sym (`Full` a))@
-- represents a fully applied symbol, i.e. a complete syntax tree.
data AST sym sig
  where
    Sym  :: sym sig -> AST sym sig
    (:$) :: AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig

infixl 1 :$

-- | Fully applied abstract syntax tree
type ASTF sym a = AST sym (Full a)

-- | Fully applied abstract syntax tree
--
-- This type is like 'AST', but being a newtype, it is a proper type constructor
-- that can be partially applied.
newtype ASTFull sym a = ASTFull {ASTFull sym a -> ASTF sym a
unASTFull :: ASTF sym a}

instance Functor sym => Functor (AST sym)
  where
    fmap :: (a -> b) -> AST sym a -> AST sym b
fmap a -> b
f (Sym sym a
s)  = sym b -> AST sym b
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym ((a -> b) -> sym a -> sym b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f sym a
s)
    fmap a -> b
f (AST sym (a :-> a)
s :$ AST sym (Full a)
a) = ((a :-> a) -> a :-> b) -> AST sym (a :-> a) -> AST sym (a :-> b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> (a :-> a) -> a :-> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) AST sym (a :-> a)
s AST sym (a :-> b) -> AST sym (Full a) -> AST sym b
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST sym (Full a)
a

-- | Signature of a fully applied symbol
newtype Full a = Full { Full a -> a
result :: a }
  deriving (Full a -> Full a -> Bool
(Full a -> Full a -> Bool)
-> (Full a -> Full a -> Bool) -> Eq (Full a)
forall a. Eq a => Full a -> Full a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Full a -> Full a -> Bool
$c/= :: forall a. Eq a => Full a -> Full a -> Bool
== :: Full a -> Full a -> Bool
$c== :: forall a. Eq a => Full a -> Full a -> Bool
Eq, Int -> Full a -> ShowS
[Full a] -> ShowS
Full a -> String
(Int -> Full a -> ShowS)
-> (Full a -> String) -> ([Full a] -> ShowS) -> Show (Full a)
forall a. Show a => Int -> Full a -> ShowS
forall a. Show a => [Full a] -> ShowS
forall a. Show a => Full a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Full a] -> ShowS
$cshowList :: forall a. Show a => [Full a] -> ShowS
show :: Full a -> String
$cshow :: forall a. Show a => Full a -> String
showsPrec :: Int -> Full a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Full a -> ShowS
Show, Typeable, a -> Full b -> Full a
(a -> b) -> Full a -> Full b
(forall a b. (a -> b) -> Full a -> Full b)
-> (forall a b. a -> Full b -> Full a) -> Functor Full
forall a b. a -> Full b -> Full a
forall a b. (a -> b) -> Full a -> Full b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Full b -> Full a
$c<$ :: forall a b. a -> Full b -> Full a
fmap :: (a -> b) -> Full a -> Full b
$cfmap :: forall a b. (a -> b) -> Full a -> Full b
Functor)

-- | Signature of a partially applied (or unapplied) symbol
newtype a :-> sig = Partial (a -> sig)
  deriving (Typeable, a -> (a :-> b) -> a :-> a
(a -> b) -> (a :-> a) -> a :-> b
(forall a b. (a -> b) -> (a :-> a) -> a :-> b)
-> (forall a b. a -> (a :-> b) -> a :-> a) -> Functor ((:->) a)
forall a b. a -> (a :-> b) -> a :-> a
forall a b. (a -> b) -> (a :-> a) -> a :-> b
forall a a b. a -> (a :-> b) -> a :-> a
forall a a b. (a -> b) -> (a :-> a) -> a :-> b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> (a :-> b) -> a :-> a
$c<$ :: forall a a b. a -> (a :-> b) -> a :-> a
fmap :: (a -> b) -> (a :-> a) -> a :-> b
$cfmap :: forall a a b. (a -> b) -> (a :-> a) -> a :-> b
Functor)

infixr :->

-- | Witness of the arity of a symbol signature
data SigRep sig
  where
    SigFull :: SigRep (Full a)
    SigMore :: SigRep sig -> SigRep (a :-> sig)

-- | Valid symbol signatures
class Signature sig
  where
    signature :: SigRep sig

instance Signature (Full a)
  where
    signature :: SigRep (Full a)
signature = SigRep (Full a)
forall a. SigRep (Full a)
SigFull

instance Signature sig => Signature (a :-> sig)
  where
    signature :: SigRep (a :-> sig)
signature = SigRep sig -> SigRep (a :-> sig)
forall sig a. SigRep sig -> SigRep (a :-> sig)
SigMore SigRep sig
forall sig. Signature sig => SigRep sig
signature

-- | The result type of a symbol with the given signature
type family   DenResult sig
type instance DenResult (Full a)    = a
type instance DenResult (a :-> sig) = DenResult sig

-- | Valid symbols to use in an 'AST'
class Symbol sym
  where
    -- | Reify the signature of a symbol
    symSig :: sym sig -> SigRep sig

instance NFData1 sym => NFData (AST sym sig)
  where
    rnf :: AST sym sig -> ()
rnf (Sym sym sig
s)  = sym sig -> ()
forall (c :: * -> *) a. NFData1 c => c a -> ()
rnf1 sym sig
s
    rnf (AST sym (a :-> sig)
s :$ AST sym (Full a)
a) = AST sym (a :-> sig) -> ()
forall a. NFData a => a -> ()
rnf AST sym (a :-> sig)
s () -> () -> ()
`seq` AST sym (Full a) -> ()
forall a. NFData a => a -> ()
rnf AST sym (Full a)
a

-- | Count the number of symbols in an 'AST'
size :: AST sym sig -> Int
size :: AST sym sig -> Int
size (Sym sym sig
_)  = Int
1
size (AST sym (a :-> sig)
s :$ AST sym (Full a)
a) = AST sym (a :-> sig) -> Int
forall (sym :: * -> *) sig. AST sym sig -> Int
size AST sym (a :-> sig)
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ AST sym (Full a) -> Int
forall (sym :: * -> *) sig. AST sym sig -> Int
size AST sym (Full a)
a



--------------------------------------------------------------------------------
-- * Smart constructors
--------------------------------------------------------------------------------

-- | Maps a symbol signature to the type of the corresponding smart constructor:
--
-- > SmartFun sym (a :-> b :-> ... :-> Full x) = ASTF sym a -> ASTF sym b -> ... -> ASTF sym x
type family   SmartFun (sym :: * -> *) sig
type instance SmartFun sym (Full a)    = ASTF sym a
type instance SmartFun sym (a :-> sig) = ASTF sym a -> SmartFun sym sig

-- | Maps a smart constructor type to the corresponding symbol signature:
--
-- > SmartSig (ASTF sym a -> ASTF sym b -> ... -> ASTF sym x) = a :-> b :-> ... :-> Full x
type family   SmartSig f
type instance SmartSig (AST sym sig)     = sig
type instance SmartSig (ASTF sym a -> f) = a :-> SmartSig f

-- | Returns the symbol in the result of a smart constructor
type family   SmartSym f :: * -> *
type instance SmartSym (AST sym sig) = sym
type instance SmartSym (a -> f)      = SmartSym f

-- | Make a smart constructor of a symbol. 'smartSym'' has any type of the form:
--
-- > smartSym'
-- >     :: sym (a :-> b :-> ... :-> Full x)
-- >     -> (ASTF sym a -> ASTF sym b -> ... -> ASTF sym x)
smartSym' :: forall sig f sym
    .  ( Signature sig
       , f   ~ SmartFun sym sig
       , sig ~ SmartSig f
       , sym ~ SmartSym f
       )
    => sym sig -> f
smartSym' :: sym sig -> f
smartSym' sym sig
s = SigRep sig -> AST sym sig -> SmartFun sym sig
forall sig. SigRep sig -> AST sym sig -> SmartFun sym sig
go (SigRep sig
forall sig. Signature sig => SigRep sig
signature :: SigRep sig) (sym sig -> AST sym sig
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym sym sig
s)
  where
    go :: forall sig . SigRep sig -> AST sym sig -> SmartFun sym sig
    go :: SigRep sig -> AST sym sig -> SmartFun sym sig
go SigRep sig
SigFull AST sym sig
s       = SmartFun sym sig
AST sym sig
s
    go (SigMore SigRep sig
sig) AST sym sig
s = \AST sym (Full a)
a -> SigRep sig -> AST sym sig -> SmartFun sym sig
forall sig. SigRep sig -> AST sym sig -> SmartFun sym sig
go SigRep sig
sig (AST sym sig
AST sym (a :-> sig)
s AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
forall (sym :: * -> *) a sig.
AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
:$ AST sym (Full a)
a)



--------------------------------------------------------------------------------
-- * Open symbol domains
--------------------------------------------------------------------------------

-- | Direct sum of two symbol domains
data (sym1 :+: sym2) sig
  where
    InjL :: sym1 a -> (sym1 :+: sym2) a
    InjR :: sym2 a -> (sym1 :+: sym2) a
  deriving (a -> (:+:) sym1 sym2 b -> (:+:) sym1 sym2 a
(a -> b) -> (:+:) sym1 sym2 a -> (:+:) sym1 sym2 b
(forall a b. (a -> b) -> (:+:) sym1 sym2 a -> (:+:) sym1 sym2 b)
-> (forall a b. a -> (:+:) sym1 sym2 b -> (:+:) sym1 sym2 a)
-> Functor (sym1 :+: sym2)
forall a b. a -> (:+:) sym1 sym2 b -> (:+:) sym1 sym2 a
forall a b. (a -> b) -> (:+:) sym1 sym2 a -> (:+:) sym1 sym2 b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (sym1 :: * -> *) (sym2 :: * -> *) a b.
(Functor sym1, Functor sym2) =>
a -> (:+:) sym1 sym2 b -> (:+:) sym1 sym2 a
forall (sym1 :: * -> *) (sym2 :: * -> *) a b.
(Functor sym1, Functor sym2) =>
(a -> b) -> (:+:) sym1 sym2 a -> (:+:) sym1 sym2 b
<$ :: a -> (:+:) sym1 sym2 b -> (:+:) sym1 sym2 a
$c<$ :: forall (sym1 :: * -> *) (sym2 :: * -> *) a b.
(Functor sym1, Functor sym2) =>
a -> (:+:) sym1 sym2 b -> (:+:) sym1 sym2 a
fmap :: (a -> b) -> (:+:) sym1 sym2 a -> (:+:) sym1 sym2 b
$cfmap :: forall (sym1 :: * -> *) (sym2 :: * -> *) a b.
(Functor sym1, Functor sym2) =>
(a -> b) -> (:+:) sym1 sym2 a -> (:+:) sym1 sym2 b
Functor, (:+:) sym1 sym2 a -> Bool
(a -> m) -> (:+:) sym1 sym2 a -> m
(a -> b -> b) -> b -> (:+:) sym1 sym2 a -> b
(forall m. Monoid m => (:+:) sym1 sym2 m -> m)
-> (forall m a. Monoid m => (a -> m) -> (:+:) sym1 sym2 a -> m)
-> (forall m a. Monoid m => (a -> m) -> (:+:) sym1 sym2 a -> m)
-> (forall a b. (a -> b -> b) -> b -> (:+:) sym1 sym2 a -> b)
-> (forall a b. (a -> b -> b) -> b -> (:+:) sym1 sym2 a -> b)
-> (forall b a. (b -> a -> b) -> b -> (:+:) sym1 sym2 a -> b)
-> (forall b a. (b -> a -> b) -> b -> (:+:) sym1 sym2 a -> b)
-> (forall a. (a -> a -> a) -> (:+:) sym1 sym2 a -> a)
-> (forall a. (a -> a -> a) -> (:+:) sym1 sym2 a -> a)
-> (forall a. (:+:) sym1 sym2 a -> [a])
-> (forall a. (:+:) sym1 sym2 a -> Bool)
-> (forall a. (:+:) sym1 sym2 a -> Int)
-> (forall a. Eq a => a -> (:+:) sym1 sym2 a -> Bool)
-> (forall a. Ord a => (:+:) sym1 sym2 a -> a)
-> (forall a. Ord a => (:+:) sym1 sym2 a -> a)
-> (forall a. Num a => (:+:) sym1 sym2 a -> a)
-> (forall a. Num a => (:+:) sym1 sym2 a -> a)
-> Foldable (sym1 :+: sym2)
forall a. Eq a => a -> (:+:) sym1 sym2 a -> Bool
forall a. Num a => (:+:) sym1 sym2 a -> a
forall a. Ord a => (:+:) sym1 sym2 a -> a
forall m. Monoid m => (:+:) sym1 sym2 m -> m
forall a. (:+:) sym1 sym2 a -> Bool
forall a. (:+:) sym1 sym2 a -> Int
forall a. (:+:) sym1 sym2 a -> [a]
forall a. (a -> a -> a) -> (:+:) sym1 sym2 a -> a
forall m a. Monoid m => (a -> m) -> (:+:) sym1 sym2 a -> m
forall b a. (b -> a -> b) -> b -> (:+:) sym1 sym2 a -> b
forall a b. (a -> b -> b) -> b -> (:+:) sym1 sym2 a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2, Eq a) =>
a -> (:+:) sym1 sym2 a -> Bool
forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2, Num a) =>
(:+:) sym1 sym2 a -> a
forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2, Ord a) =>
(:+:) sym1 sym2 a -> a
forall (sym1 :: * -> *) (sym2 :: * -> *) m.
(Foldable sym1, Foldable sym2, Monoid m) =>
(:+:) sym1 sym2 m -> m
forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2) =>
(:+:) sym1 sym2 a -> Bool
forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2) =>
(:+:) sym1 sym2 a -> Int
forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2) =>
(:+:) sym1 sym2 a -> [a]
forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2) =>
(a -> a -> a) -> (:+:) sym1 sym2 a -> a
forall (sym1 :: * -> *) (sym2 :: * -> *) m a.
(Foldable sym1, Foldable sym2, Monoid m) =>
(a -> m) -> (:+:) sym1 sym2 a -> m
forall (sym1 :: * -> *) (sym2 :: * -> *) b a.
(Foldable sym1, Foldable sym2) =>
(b -> a -> b) -> b -> (:+:) sym1 sym2 a -> b
forall (sym1 :: * -> *) (sym2 :: * -> *) a b.
(Foldable sym1, Foldable sym2) =>
(a -> b -> b) -> b -> (:+:) sym1 sym2 a -> b
product :: (:+:) sym1 sym2 a -> a
$cproduct :: forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2, Num a) =>
(:+:) sym1 sym2 a -> a
sum :: (:+:) sym1 sym2 a -> a
$csum :: forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2, Num a) =>
(:+:) sym1 sym2 a -> a
minimum :: (:+:) sym1 sym2 a -> a
$cminimum :: forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2, Ord a) =>
(:+:) sym1 sym2 a -> a
maximum :: (:+:) sym1 sym2 a -> a
$cmaximum :: forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2, Ord a) =>
(:+:) sym1 sym2 a -> a
elem :: a -> (:+:) sym1 sym2 a -> Bool
$celem :: forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2, Eq a) =>
a -> (:+:) sym1 sym2 a -> Bool
length :: (:+:) sym1 sym2 a -> Int
$clength :: forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2) =>
(:+:) sym1 sym2 a -> Int
null :: (:+:) sym1 sym2 a -> Bool
$cnull :: forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2) =>
(:+:) sym1 sym2 a -> Bool
toList :: (:+:) sym1 sym2 a -> [a]
$ctoList :: forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2) =>
(:+:) sym1 sym2 a -> [a]
foldl1 :: (a -> a -> a) -> (:+:) sym1 sym2 a -> a
$cfoldl1 :: forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2) =>
(a -> a -> a) -> (:+:) sym1 sym2 a -> a
foldr1 :: (a -> a -> a) -> (:+:) sym1 sym2 a -> a
$cfoldr1 :: forall (sym1 :: * -> *) (sym2 :: * -> *) a.
(Foldable sym1, Foldable sym2) =>
(a -> a -> a) -> (:+:) sym1 sym2 a -> a
foldl' :: (b -> a -> b) -> b -> (:+:) sym1 sym2 a -> b
$cfoldl' :: forall (sym1 :: * -> *) (sym2 :: * -> *) b a.
(Foldable sym1, Foldable sym2) =>
(b -> a -> b) -> b -> (:+:) sym1 sym2 a -> b
foldl :: (b -> a -> b) -> b -> (:+:) sym1 sym2 a -> b
$cfoldl :: forall (sym1 :: * -> *) (sym2 :: * -> *) b a.
(Foldable sym1, Foldable sym2) =>
(b -> a -> b) -> b -> (:+:) sym1 sym2 a -> b
foldr' :: (a -> b -> b) -> b -> (:+:) sym1 sym2 a -> b
$cfoldr' :: forall (sym1 :: * -> *) (sym2 :: * -> *) a b.
(Foldable sym1, Foldable sym2) =>
(a -> b -> b) -> b -> (:+:) sym1 sym2 a -> b
foldr :: (a -> b -> b) -> b -> (:+:) sym1 sym2 a -> b
$cfoldr :: forall (sym1 :: * -> *) (sym2 :: * -> *) a b.
(Foldable sym1, Foldable sym2) =>
(a -> b -> b) -> b -> (:+:) sym1 sym2 a -> b
foldMap' :: (a -> m) -> (:+:) sym1 sym2 a -> m
$cfoldMap' :: forall (sym1 :: * -> *) (sym2 :: * -> *) m a.
(Foldable sym1, Foldable sym2, Monoid m) =>
(a -> m) -> (:+:) sym1 sym2 a -> m
foldMap :: (a -> m) -> (:+:) sym1 sym2 a -> m
$cfoldMap :: forall (sym1 :: * -> *) (sym2 :: * -> *) m a.
(Foldable sym1, Foldable sym2, Monoid m) =>
(a -> m) -> (:+:) sym1 sym2 a -> m
fold :: (:+:) sym1 sym2 m -> m
$cfold :: forall (sym1 :: * -> *) (sym2 :: * -> *) m.
(Foldable sym1, Foldable sym2, Monoid m) =>
(:+:) sym1 sym2 m -> m
Foldable, Functor (sym1 :+: sym2)
Foldable (sym1 :+: sym2)
Functor (sym1 :+: sym2)
-> Foldable (sym1 :+: sym2)
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> (:+:) sym1 sym2 a -> f ((:+:) sym1 sym2 b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    (:+:) sym1 sym2 (f a) -> f ((:+:) sym1 sym2 a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> (:+:) sym1 sym2 a -> m ((:+:) sym1 sym2 b))
-> (forall (m :: * -> *) a.
    Monad m =>
    (:+:) sym1 sym2 (m a) -> m ((:+:) sym1 sym2 a))
-> Traversable (sym1 :+: sym2)
(a -> f b) -> (:+:) sym1 sym2 a -> f ((:+:) sym1 sym2 b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
(:+:) sym1 sym2 (m a) -> m ((:+:) sym1 sym2 a)
forall (f :: * -> *) a.
Applicative f =>
(:+:) sym1 sym2 (f a) -> f ((:+:) sym1 sym2 a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> (:+:) sym1 sym2 a -> m ((:+:) sym1 sym2 b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (:+:) sym1 sym2 a -> f ((:+:) sym1 sym2 b)
forall (sym1 :: * -> *) (sym2 :: * -> *).
(Traversable sym1, Traversable sym2) =>
Functor (sym1 :+: sym2)
forall (sym1 :: * -> *) (sym2 :: * -> *).
(Traversable sym1, Traversable sym2) =>
Foldable (sym1 :+: sym2)
forall (sym1 :: * -> *) (sym2 :: * -> *) (m :: * -> *) a.
(Traversable sym1, Traversable sym2, Monad m) =>
(:+:) sym1 sym2 (m a) -> m ((:+:) sym1 sym2 a)
forall (sym1 :: * -> *) (sym2 :: * -> *) (f :: * -> *) a.
(Traversable sym1, Traversable sym2, Applicative f) =>
(:+:) sym1 sym2 (f a) -> f ((:+:) sym1 sym2 a)
forall (sym1 :: * -> *) (sym2 :: * -> *) (m :: * -> *) a b.
(Traversable sym1, Traversable sym2, Monad m) =>
(a -> m b) -> (:+:) sym1 sym2 a -> m ((:+:) sym1 sym2 b)
forall (sym1 :: * -> *) (sym2 :: * -> *) (f :: * -> *) a b.
(Traversable sym1, Traversable sym2, Applicative f) =>
(a -> f b) -> (:+:) sym1 sym2 a -> f ((:+:) sym1 sym2 b)
sequence :: (:+:) sym1 sym2 (m a) -> m ((:+:) sym1 sym2 a)
$csequence :: forall (sym1 :: * -> *) (sym2 :: * -> *) (m :: * -> *) a.
(Traversable sym1, Traversable sym2, Monad m) =>
(:+:) sym1 sym2 (m a) -> m ((:+:) sym1 sym2 a)
mapM :: (a -> m b) -> (:+:) sym1 sym2 a -> m ((:+:) sym1 sym2 b)
$cmapM :: forall (sym1 :: * -> *) (sym2 :: * -> *) (m :: * -> *) a b.
(Traversable sym1, Traversable sym2, Monad m) =>
(a -> m b) -> (:+:) sym1 sym2 a -> m ((:+:) sym1 sym2 b)
sequenceA :: (:+:) sym1 sym2 (f a) -> f ((:+:) sym1 sym2 a)
$csequenceA :: forall (sym1 :: * -> *) (sym2 :: * -> *) (f :: * -> *) a.
(Traversable sym1, Traversable sym2, Applicative f) =>
(:+:) sym1 sym2 (f a) -> f ((:+:) sym1 sym2 a)
traverse :: (a -> f b) -> (:+:) sym1 sym2 a -> f ((:+:) sym1 sym2 b)
$ctraverse :: forall (sym1 :: * -> *) (sym2 :: * -> *) (f :: * -> *) a b.
(Traversable sym1, Traversable sym2, Applicative f) =>
(a -> f b) -> (:+:) sym1 sym2 a -> f ((:+:) sym1 sym2 b)
$cp2Traversable :: forall (sym1 :: * -> *) (sym2 :: * -> *).
(Traversable sym1, Traversable sym2) =>
Foldable (sym1 :+: sym2)
$cp1Traversable :: forall (sym1 :: * -> *) (sym2 :: * -> *).
(Traversable sym1, Traversable sym2) =>
Functor (sym1 :+: sym2)
Traversable)

infixr :+:

instance (Symbol sym1, Symbol sym2) => Symbol (sym1 :+: sym2)
  where
    symSig :: (:+:) sym1 sym2 sig -> SigRep sig
symSig (InjL sym1 sig
s) = sym1 sig -> SigRep sig
forall (sym :: * -> *) sig. Symbol sym => sym sig -> SigRep sig
symSig sym1 sig
s
    symSig (InjR sym2 sig
s) = sym2 sig -> SigRep sig
forall (sym :: * -> *) sig. Symbol sym => sym sig -> SigRep sig
symSig sym2 sig
s

instance (NFData1 sym1, NFData1 sym2) => NFData1 (sym1 :+: sym2)
  where
    rnf1 :: (:+:) sym1 sym2 a -> ()
rnf1 (InjL sym1 a
s) = sym1 a -> ()
forall (c :: * -> *) a. NFData1 c => c a -> ()
rnf1 sym1 a
s
    rnf1 (InjR sym2 a
s) = sym2 a -> ()
forall (c :: * -> *) a. NFData1 c => c a -> ()
rnf1 sym2 a
s

-- | Symbol projection
--
-- The class is defined for /all pairs of types/, but 'prj' can only succeed if @sup@ is of the form
-- @(... `:+:` sub `:+:` ...)@.
class Project sub sup
  where
    -- | Partial projection from @sup@ to @sub@
    prj :: sup a -> Maybe (sub a)

instance Project sub sup => Project sub (AST sup)
  where
    prj :: AST sup a -> Maybe (sub a)
prj (Sym sup a
s) = sup a -> Maybe (sub a)
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj sup a
s
    prj AST sup a
_       = Maybe (sub a)
forall a. Maybe a
Nothing

instance {-# OVERLAPS #-} Project sym sym
  where
    prj :: sym a -> Maybe (sym a)
prj = sym a -> Maybe (sym a)
forall a. a -> Maybe a
Just

instance {-# OVERLAPS #-} Project sym1 (sym1 :+: sym2)
  where
    prj :: (:+:) sym1 sym2 a -> Maybe (sym1 a)
prj (InjL sym1 a
a) = sym1 a -> Maybe (sym1 a)
forall a. a -> Maybe a
Just sym1 a
a
    prj (:+:) sym1 sym2 a
_        = Maybe (sym1 a)
forall a. Maybe a
Nothing

instance {-# OVERLAPS #-} Project sym1 sym3 => Project sym1 (sym2 :+: sym3)
  where
    prj :: (:+:) sym2 sym3 a -> Maybe (sym1 a)
prj (InjR sym3 a
a) = sym3 a -> Maybe (sym1 a)
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj sym3 a
a
    prj (:+:) sym2 sym3 a
_        = Maybe (sym1 a)
forall a. Maybe a
Nothing


-- | Symbol injection
--
-- The class includes types @sub@ and @sup@ where @sup@ is of the form @(... `:+:` sub `:+:` ...)@.
class Project sub sup => sub :<: sup
  where
    -- | Injection from @sub@ to @sup@
    inj :: sub a -> sup a

instance {-# OVERLAPS #-} (sub :<: sup) => (sub :<: AST sup)
  where
    inj :: sub a -> AST sup a
inj = sup a -> AST sup a
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (sup a -> AST sup a) -> (sub a -> sup a) -> sub a -> AST sup a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sub a -> sup a
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj

instance {-# OVERLAPS #-} (sym :<: sym)
  where
    inj :: sym a -> sym a
inj = sym a -> sym a
forall a. a -> a
id

instance {-# OVERLAPS #-} (sym1 :<: (sym1 :+: sym2))
  where
    inj :: sym1 a -> (:+:) sym1 sym2 a
inj = sym1 a -> (:+:) sym1 sym2 a
forall (sym1 :: * -> *) a (sym2 :: * -> *).
sym1 a -> (:+:) sym1 sym2 a
InjL

instance {-# OVERLAPS #-} (sym1 :<: sym3) => (sym1 :<: (sym2 :+: sym3))
  where
    inj :: sym1 a -> (:+:) sym2 sym3 a
inj = sym3 a -> (:+:) sym2 sym3 a
forall (sym2 :: * -> *) a (sym1 :: * -> *).
sym2 a -> (:+:) sym1 sym2 a
InjR (sym3 a -> (:+:) sym2 sym3 a)
-> (sym1 a -> sym3 a) -> sym1 a -> (:+:) sym2 sym3 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym1 a -> sym3 a
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj

-- The reason for separating the `Project` and `(:<:)` classes is that there are
-- types that can be instances of the former but not the latter due to type
-- constraints on the `a` type.

-- | Make a smart constructor of a symbol. 'smartSym' has any type of the form:
--
-- > smartSym :: (sub :<: AST sup)
-- >     => sub (a :-> b :-> ... :-> Full x)
-- >     -> (ASTF sup a -> ASTF sup b -> ... -> ASTF sup x)
smartSym
    :: ( Signature sig
       , f   ~ SmartFun sup sig
       , sig ~ SmartSig f
       , sup ~ SmartSym f
       , sub :<: sup
       )
    => sub sig -> f
smartSym :: sub sig -> f
smartSym = sup sig -> f
forall sig f (sym :: * -> *).
(Signature sig, f ~ SmartFun sym sig, sig ~ SmartSig f,
 sym ~ SmartSym f) =>
sym sig -> f
smartSym' (sup sig -> f) -> (sub sig -> sup sig) -> sub sig -> f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sub sig -> sup sig
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj

-- | Make a smart constructor of a symbol. 'smartSymTyped' has any type of the
-- form:
--
-- > smartSymTyped :: (sub :<: AST (Typed sup), Typeable x)
-- >     => sub (a :-> b :-> ... :-> Full x)
-- >     -> (ASTF sup a -> ASTF sup b -> ... -> ASTF sup x)
smartSymTyped
    :: ( Signature sig
       , f         ~ SmartFun (Typed sup) sig
       , sig       ~ SmartSig f
       , Typed sup ~ SmartSym f
       , sub :<: sup
       , Typeable (DenResult sig)
       )
    => sub sig -> f
smartSymTyped :: sub sig -> f
smartSymTyped = Typed sup sig -> f
forall sig f (sym :: * -> *).
(Signature sig, f ~ SmartFun sym sig, sig ~ SmartSig f,
 sym ~ SmartSym f) =>
sym sig -> f
smartSym' (Typed sup sig -> f) -> (sub sig -> Typed sup sig) -> sub sig -> f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sup sig -> Typed sup sig
forall sig (sym :: * -> *).
Typeable (DenResult sig) =>
sym sig -> Typed sym sig
Typed (sup sig -> Typed sup sig)
-> (sub sig -> sup sig) -> sub sig -> Typed sup sig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sub sig -> sup sig
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj

-- | Empty symbol type
--
-- Can be used to make uninhabited 'AST' types. It can also be used as a terminator in co-product
-- lists (e.g. to avoid overlapping instances):
--
-- > (A :+: B :+: Empty)
data Empty :: * -> *



--------------------------------------------------------------------------------
-- * Existential quantification
--------------------------------------------------------------------------------

-- | Existential quantification
data E e
  where
    E :: e a -> E e

liftE :: (forall a . e a -> b) -> E e -> b
liftE :: (forall a. e a -> b) -> E e -> b
liftE forall a. e a -> b
f (E e a
a) = e a -> b
forall a. e a -> b
f e a
a

liftE2 :: (forall a b . e a -> e b -> c) -> E e -> E e -> c
liftE2 :: (forall a b. e a -> e b -> c) -> E e -> E e -> c
liftE2 forall a b. e a -> e b -> c
f (E e a
a) (E e a
b) = e a -> e a -> c
forall a b. e a -> e b -> c
f e a
a e a
b

-- | Existential quantification of 'Full'-indexed type
data EF e
  where
    EF :: e (Full a) -> EF e

liftEF :: (forall a . e (Full a) -> b) -> EF e -> b
liftEF :: (forall a. e (Full a) -> b) -> EF e -> b
liftEF forall a. e (Full a) -> b
f (EF e (Full a)
a) = e (Full a) -> b
forall a. e (Full a) -> b
f e (Full a)
a

liftEF2 :: (forall a b . e (Full a) -> e (Full b) -> c) -> EF e -> EF e -> c
liftEF2 :: (forall a b. e (Full a) -> e (Full b) -> c) -> EF e -> EF e -> c
liftEF2 forall a b. e (Full a) -> e (Full b) -> c
f (EF e (Full a)
a) (EF e (Full a)
b) = e (Full a) -> e (Full a) -> c
forall a b. e (Full a) -> e (Full b) -> c
f e (Full a)
a e (Full a)
b



--------------------------------------------------------------------------------
-- * Type casting expressions
--------------------------------------------------------------------------------

-- | \"Typed\" symbol. Using @`Typed` sym@ instead of @sym@ gives access to the
-- function 'castExpr' for casting expressions.
data Typed sym sig
  where
    Typed :: Typeable (DenResult sig) => sym sig -> Typed sym sig

instance Project sub sup => Project sub (Typed sup)
  where
    prj :: Typed sup a -> Maybe (sub a)
prj (Typed sup a
s) = sup a -> Maybe (sub a)
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj sup a
s

-- | Inject a symbol in an 'AST' with a 'Typed' domain
injT :: (sub :<: sup, Typeable (DenResult sig)) =>
    sub sig -> AST (Typed sup) sig
injT :: sub sig -> AST (Typed sup) sig
injT = Typed sup sig -> AST (Typed sup) sig
forall (sym :: * -> *) sig. sym sig -> AST sym sig
Sym (Typed sup sig -> AST (Typed sup) sig)
-> (sub sig -> Typed sup sig) -> sub sig -> AST (Typed sup) sig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sup sig -> Typed sup sig
forall sig (sym :: * -> *).
Typeable (DenResult sig) =>
sym sig -> Typed sym sig
Typed (sup sig -> Typed sup sig)
-> (sub sig -> sup sig) -> sub sig -> Typed sup sig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sub sig -> sup sig
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj

-- | Type cast an expression
castExpr :: forall sym a b
    .  ASTF (Typed sym) a  -- ^ Expression to cast
    -> ASTF (Typed sym) b  -- ^ Witness for typeability of result
    -> Maybe (ASTF (Typed sym) b)
castExpr :: ASTF (Typed sym) a
-> ASTF (Typed sym) b -> Maybe (ASTF (Typed sym) b)
castExpr ASTF (Typed sym) a
a ASTF (Typed sym) b
b = ASTF (Typed sym) a -> Maybe (ASTF (Typed sym) b)
forall sig.
(DenResult sig ~ a) =>
AST (Typed sym) sig -> Maybe (ASTF (Typed sym) b)
cast1 ASTF (Typed sym) a
a
  where
    cast1 :: (DenResult sig ~ a) => AST (Typed sym) sig -> Maybe (ASTF (Typed sym) b)
    cast1 :: AST (Typed sym) sig -> Maybe (ASTF (Typed sym) b)
cast1 (AST (Typed sym) (a :-> sig)
s :$ AST (Typed sym) (Full a)
_) = AST (Typed sym) (a :-> sig) -> Maybe (ASTF (Typed sym) b)
forall sig.
(DenResult sig ~ a) =>
AST (Typed sym) sig -> Maybe (ASTF (Typed sym) b)
cast1 AST (Typed sym) (a :-> sig)
s
    cast1 (Sym (Typed sym sig
_)) = ASTF (Typed sym) b -> Maybe (ASTF (Typed sym) b)
forall sig.
(DenResult sig ~ b) =>
AST (Typed sym) sig -> Maybe (ASTF (Typed sym) b)
cast2 ASTF (Typed sym) b
b
      where
        cast2 :: (DenResult sig ~ b) => AST (Typed sym) sig -> Maybe (ASTF (Typed sym) b)
        cast2 :: AST (Typed sym) sig -> Maybe (ASTF (Typed sym) b)
cast2 (AST (Typed sym) (a :-> sig)
s :$ AST (Typed sym) (Full a)
_)        = AST (Typed sym) (a :-> sig) -> Maybe (ASTF (Typed sym) b)
forall sig.
(DenResult sig ~ b) =>
AST (Typed sym) sig -> Maybe (ASTF (Typed sym) b)
cast2 AST (Typed sym) (a :-> sig)
s
        cast2 (Sym (Typed sym sig
_)) = ASTF (Typed sym) a -> Maybe (ASTF (Typed sym) b)
forall k (a :: k) (b :: k) (c :: k -> *).
(Typeable a, Typeable b) =>
c a -> Maybe (c b)
gcast ASTF (Typed sym) a
a
  -- Could be simplified using `simpleMatch`, but that would give an import
  -- cycle.
  --
  --     castExpr a b =
  --       simpleMatch
  --         (\(Typed _) _ -> simpleMatch
  --           (\(Typed _) _ -> gcast a
  --           ) b
  --         ) a



--------------------------------------------------------------------------------
-- * Misc.
--------------------------------------------------------------------------------

-- | Higher-kinded version of 'NFData'
class NFData1 c
  where
    -- | Force a symbol to normal form
    rnf1 :: c a -> ()
    rnf1 c a
s = c a
s c a -> () -> ()
`seq` ()

-- | Constrain a symbol to a specific type
symType :: Proxy sym -> sym sig -> sym sig
symType :: Proxy sym -> sym sig -> sym sig
symType Proxy sym
_ = sym sig -> sym sig
forall a. a -> a
id

-- | Projection to a specific symbol type
prjP :: Project sub sup => Proxy sub -> sup sig -> Maybe (sub sig)
prjP :: Proxy sub -> sup sig -> Maybe (sub sig)
prjP Proxy sub
_ = sup sig -> Maybe (sub sig)
forall (sub :: * -> *) (sup :: * -> *) a.
Project sub sup =>
sup a -> Maybe (sub a)
prj