{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
module Data.Comp.Decompose (
Decomp (..),
DecompTerm,
Decompose,
decomp,
structure,
arguments,
decompose
) where
import Data.Comp.Term
import Data.Comp.Variables
import Data.Foldable
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 ())
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
data Decomp f v a = Var v
| Fun (Const f) [a]
type DecompTerm f v = Decomp f v (Term f)
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
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