{-# LANGUAGE EmptyDataDecls       #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE Rank2Types           #-}
{-# LANGUAGE TypeSynonymInstances #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Term
-- Copyright   :  (c) 2010-2011 Patrick Bahr, Tom Hvitved
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module defines the central notion of /terms/ and its
-- generalisation to contexts.
--
--------------------------------------------------------------------------------

module Data.Comp.Term
    (Cxt (..),
     Hole,
     NoHole,
     Context,
     Term,
     PTerm,
     Const,
     unTerm,
     simpCxt,
     toCxt,
     constTerm
     ) where

import Control.Applicative hiding (Const)
import Control.Monad hiding (mapM, sequence)

import Data.Kind
import Data.Foldable
import Data.Traversable
import Unsafe.Coerce

import Prelude hiding (foldl, foldl1, foldr, foldr1, mapM, sequence)


{-|  -}
type Const f = f ()

{-| This function converts a constant to a term. This assumes that the
argument is indeed a constant, i.e. does not have a value for the
argument type of the functor @f@. -}

constTerm :: (Functor f) => Const f -> Term f
constTerm :: forall (f :: * -> *). Functor f => Const f -> Term f
constTerm = forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const forall a. HasCallStack => a
undefined)

{-| This data type represents contexts over a signature. Contexts are
terms containing zero or more holes. The first type parameter is
supposed to be one of the phantom types 'Hole' and 'NoHole'. The
second parameter is the signature of the context. The third parameter
is the type of the holes. -}

data Cxt :: Type -> (Type -> Type) -> Type -> Type where
            Term :: f (Cxt h f a) -> Cxt h f a
            Hole :: a -> Cxt Hole f a


{-| Phantom type that signals that a 'Cxt' might contain holes.  -}

data Hole

{-| Phantom type that signals that a 'Cxt' does not contain holes.
-}

data NoHole

type Context = Cxt Hole

{-| Convert a functorial value into a context.  -}
simpCxt :: Functor f => f a -> Context f a
{-# INLINE simpCxt #-}
simpCxt :: forall (f :: * -> *) a. Functor f => f a -> Context f a
simpCxt = forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (f :: * -> *). a -> Cxt Hole f a
Hole


{-| Cast a term over a signature to a context over the same signature. -}
toCxt :: Functor f => Term f -> Cxt h f a
{-# INLINE toCxt #-}
toCxt :: forall (f :: * -> *) h a. Functor f => Term f -> Cxt h f a
toCxt = forall a b. a -> b
unsafeCoerce
-- equivalent to @Term . (fmap toCxt) . unTerm@

{-| A term is a context with no holes.  -}
type Term f = Cxt NoHole f ()

-- | Polymorphic definition of a term. This formulation is more
-- natural than 'Term', it leads to impredicative types in some cases,
-- though.
type PTerm f = forall h a . Cxt h f a

instance Functor f => Functor (Cxt h f) where
    fmap :: forall a b. (a -> b) -> Cxt h f a -> Cxt h f b
fmap a -> b
f = Cxt h f a -> Cxt h f b
run
        where run :: Cxt h f a -> Cxt h f b
run (Hole a
v) = forall a (f :: * -> *). a -> Cxt Hole f a
Hole (a -> b
f a
v)
              run (Term f (Cxt h f a)
t) = forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cxt h f a -> Cxt h f b
run f (Cxt h f a)
t)

instance Functor f => Applicative (Context f) where
    pure :: forall a. a -> Context f a
pure = forall a (f :: * -> *). a -> Cxt Hole f a
Hole
    <*> :: forall a b. Context f (a -> b) -> Context f a -> Context f b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (Functor f) => Monad (Context f) where
    Context f a
m >>= :: forall a b. Context f a -> (a -> Context f b) -> Context f b
>>= a -> Context f b
f = Context f a -> Context f b
run Context f a
m
        where run :: Context f a -> Context f b
run (Hole a
v) = a -> Context f b
f a
v
              run (Term f (Context f a)
t) = forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Context f a -> Context f b
run f (Context f a)
t)

instance (Foldable f) => Foldable (Cxt h f) where
    foldr :: forall a b. (a -> b -> b) -> b -> Cxt h f a -> b
foldr a -> b -> b
op b
c Cxt h f a
a = Cxt h f a -> b -> b
run Cxt h f a
a b
c
        where run :: Cxt h f a -> b -> b
run (Hole a
a) b
e = a
a a -> b -> b
`op` b
e
              run (Term f (Cxt h f a)
t) b
e = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Cxt h f a -> b -> b
run b
e f (Cxt h f a)
t

    foldl :: forall b a. (b -> a -> b) -> b -> Cxt h f a -> b
foldl b -> a -> b
op = b -> Cxt h f a -> b
run
        where run :: b -> Cxt h f a -> b
run b
e (Hole a
a) = b
e b -> a -> b
`op` a
a
              run b
e (Term f (Cxt h f a)
t) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> Cxt h f a -> b
run b
e f (Cxt h f a)
t

    fold :: forall m. Monoid m => Cxt h f m -> m
fold (Hole m
a) = m
a
    fold (Term f (Cxt h f m)
t) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold f (Cxt h f m)
t

    foldMap :: forall m a. Monoid m => (a -> m) -> Cxt h f a -> m
foldMap a -> m
f = Cxt h f a -> m
run
        where run :: Cxt h f a -> m
run (Hole a
a) = a -> m
f a
a
              run (Term f (Cxt h f a)
t) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Cxt h f a -> m
run f (Cxt h f a)
t

instance (Traversable f) => Traversable (Cxt h f) where
    traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Cxt h f a -> f (Cxt h f b)
traverse a -> f b
f = Cxt h f a -> f (Cxt h f b)
run
        where run :: Cxt h f a -> f (Cxt h f b)
run (Hole a
a) = forall a (f :: * -> *). a -> Cxt Hole f a
Hole forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
a
              run (Term f (Cxt h f a)
t) = forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Cxt h f a -> f (Cxt h f b)
run f (Cxt h f a)
t

    sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Cxt h f (f a) -> f (Cxt h f a)
sequenceA (Hole f a
a) = forall a (f :: * -> *). a -> Cxt Hole f a
Hole forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
a
    sequenceA (Term f (Cxt h f (f a))
t) = forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA f (Cxt h f (f a))
t

    mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Cxt h f a -> m (Cxt h f b)
mapM a -> m b
f = Cxt h f a -> m (Cxt h f b)
run
        where run :: Cxt h f a -> m (Cxt h f b)
run (Hole a
a) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a (f :: * -> *). a -> Cxt Hole f a
Hole forall a b. (a -> b) -> a -> b
$ a -> m b
f a
a
              run (Term f (Cxt h f a)
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f a -> m (Cxt h f b)
run f (Cxt h f a)
t

    sequence :: forall (m :: * -> *) a. Monad m => Cxt h f (m a) -> m (Cxt h f a)
sequence (Hole m a
a) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a (f :: * -> *). a -> Cxt Hole f a
Hole m a
a
    sequence (Term f (Cxt h f (m a))
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence f (Cxt h f (m a))
t



{-| This function unravels the given term at the topmost layer.  -}

unTerm :: Cxt NoHole f a -> f (Cxt NoHole f a)
{-# INLINE unTerm #-}
unTerm :: forall (f :: * -> *) a. Cxt NoHole f a -> f (Cxt NoHole f a)
unTerm (Term f (Cxt NoHole f a)
t) = f (Cxt NoHole f a)
t