{-# 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.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 :: Const f -> Term f
constTerm = f (Term f) -> Term f
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (Term f) -> Term f)
-> (Const f -> f (Term f)) -> Const f -> Term f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() -> Term f) -> Const f -> f (Term f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term f -> () -> Term f
forall a b. a -> b -> a
const Term f
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 :: * -> (* -> *) -> * -> * 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 :: f a -> Context f a
simpCxt = f (Context f a) -> Context f a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (Context f a) -> Context f a)
-> (f a -> f (Context f a)) -> f a -> Context f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Context f a) -> f a -> f (Context f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Context f a
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 :: Term f -> Cxt h f a
toCxt = Term f -> Cxt h f a
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 :: (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) = b -> Cxt Hole f b
forall a (f :: * -> *). a -> Cxt Hole f a
Hole (a -> b
f a
v)
              run (Term f (Cxt h f a)
t) = f (Cxt h f b) -> Cxt h f b
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term ((Cxt h f a -> Cxt h f b) -> f (Cxt h f a) -> f (Cxt h f b)
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 :: a -> Context f a
pure = a -> Context f a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole
    <*> :: Context f (a -> b) -> Context f a -> Context f 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
    return :: a -> Context f a
return = a -> Context f a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole
    Context f a
m >>= :: 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) = f (Context f b) -> Context f b
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term ((Context f a -> Context f b) -> f (Context f a) -> f (Context f b)
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 :: (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 = (Cxt h f a -> b -> b) -> b -> f (Cxt h f a) -> b
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 :: (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) = (b -> Cxt h f a -> b) -> b -> f (Cxt h f a) -> b
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 :: Cxt h f m -> m
fold (Hole m
a) = m
a
    fold (Term f (Cxt h f m)
t) = (Cxt h f m -> m) -> f (Cxt h f m) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Cxt h f m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold f (Cxt h f m)
t

    foldMap :: (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) = (Cxt h f a -> m) -> f (Cxt h f a) -> m
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 :: (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) = b -> Cxt Hole f b
forall a (f :: * -> *). a -> Cxt Hole f a
Hole (b -> Cxt Hole f b) -> f b -> f (Cxt Hole f b)
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) = f (Cxt h f b) -> Cxt h f b
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (Cxt h f b) -> Cxt h f b) -> f (f (Cxt h f b)) -> f (Cxt h f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Cxt h f a -> f (Cxt h f b)) -> f (Cxt h f a) -> f (f (Cxt h 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 :: Cxt h f (f a) -> f (Cxt h f a)
sequenceA (Hole f a
a) = a -> Cxt Hole f a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole (a -> Cxt Hole f a) -> f a -> f (Cxt Hole f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
a
    sequenceA (Term f (Cxt h f (f a))
t) = f (Cxt h f a) -> Cxt h f a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (Cxt h f a) -> Cxt h f a) -> f (f (Cxt h f a)) -> f (Cxt h f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Cxt h f (f a) -> f (Cxt h f a))
-> f (Cxt h f (f a)) -> f (f (Cxt h f a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Cxt h f (f a) -> f (Cxt h f a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA f (Cxt h f (f a))
t

    mapM :: (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) = (b -> Cxt Hole f b) -> m b -> m (Cxt Hole f b)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM b -> Cxt Hole f b
forall a (f :: * -> *). a -> Cxt Hole f a
Hole (m b -> m (Cxt Hole f b)) -> m b -> m (Cxt Hole f b)
forall a b. (a -> b) -> a -> b
$ a -> m b
f a
a
              run (Term f (Cxt h f a)
t) = (f (Cxt h f b) -> Cxt h f b) -> m (f (Cxt h f b)) -> m (Cxt h f b)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM f (Cxt h f b) -> Cxt h f b
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (m (f (Cxt h f b)) -> m (Cxt h f b))
-> m (f (Cxt h f b)) -> m (Cxt h f b)
forall a b. (a -> b) -> a -> b
$ (Cxt h f a -> m (Cxt h f b)) -> f (Cxt h f a) -> m (f (Cxt h f 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 :: Cxt h f (m a) -> m (Cxt h f a)
sequence (Hole m a
a) = (a -> Cxt Hole f a) -> m a -> m (Cxt Hole f a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM a -> Cxt Hole f a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole m a
a
    sequence (Term f (Cxt h f (m a))
t) = (f (Cxt h f a) -> Cxt h f a) -> m (f (Cxt h f a)) -> m (Cxt h f a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM f (Cxt h f a) -> Cxt h f a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (m (f (Cxt h f a)) -> m (Cxt h f a))
-> m (f (Cxt h f a)) -> m (Cxt h f a)
forall a b. (a -> b) -> a -> b
$ (Cxt h f (m a) -> m (Cxt h f a))
-> f (Cxt h f (m a)) -> m (f (Cxt h f a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f (m a) -> m (Cxt h f a)
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 :: Cxt NoHole f a -> f (Cxt NoHole f a)
unTerm (Term f (Cxt NoHole f a)
t) = f (Cxt NoHole f a)
t