{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ConstraintKinds  #-}

--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Decompose
-- Copyright   :  (c) 2010-2011 Patrick Bahr
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module implements the decomposition of terms into function
-- symbols and arguments resp. variables.
--
--------------------------------------------------------------------------------
module Data.Comp.Decompose (
  Decomp (..),
  DecompTerm,
  Decompose,
  decomp,
  structure,
  arguments,
  decompose
  ) where

import Data.Comp.Term
import Data.Comp.Variables
import Data.Foldable

{-| This function computes the structure of a functorial value. -}

structure :: (Functor f) => f a -> Const f
structure :: forall (f :: * -> *) a. Functor f => f a -> Const f
structure = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const ())

{-| This function computes the arguments of a functorial value.  -}

arguments :: (Foldable f) => f a -> [a]
arguments :: forall (f :: * -> *) a. Foldable f => f a -> [a]
arguments = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

{-| This type represents decompositions of functorial values. -}

data Decomp f v a = Var v
                  | Fun (Const f) [a]

{-| This type represents decompositions of terms.  -}

type DecompTerm f v = Decomp f v (Term f)

{-| This class specifies the decomposability of a functorial value. -}

type Decompose f v = (HasVars f v, Functor f, Foldable f)

decomp :: Decompose f v => f a -> Decomp f v a
decomp :: forall (f :: * -> *) v a. Decompose f v => f a -> Decomp f v a
decomp f a
t = case forall (f :: * -> *) v a. HasVars f v => f a -> Maybe v
isVar f a
t of
             Just v
v -> forall (f :: * -> *) v a. v -> Decomp f v a
Var v
v
             Maybe v
Nothing -> forall (f :: * -> *) v a. Const f -> [a] -> Decomp f v a
Fun f ()
sym [a]
args
               where sym :: f ()
sym = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const ()) f a
t
                     args :: [a]
args = forall (f :: * -> *) a. Foldable f => f a -> [a]
arguments f a
t


{-| This function decomposes a term. -}

decompose :: Decompose f v => Term f -> DecompTerm f v
decompose :: forall (f :: * -> *) v. Decompose f v => Term f -> DecompTerm f v
decompose (Term f (Cxt NoHole f ())
t) = forall (f :: * -> *) v a. Decompose f v => f a -> Decomp f v a
decomp f (Cxt NoHole f ())
t