module Hylos where

import Language.Pointwise.Syntax as Pointwise
import Language.Pointfree.Syntax as Pointfree hiding (Term)
import Data.List
import Control.Monad.State


-- Hylomorphism derivation a la Hu, Iwasaki, and Takeichi

derivable :: Term -> Bool
derivable (Pointwise.Fix (Lam f (Lam x l))) = branch l
    where branch (Case m (Lam _ n) (Lam _ o)) = 
	      (f `notElem` free m) && branch n && branch o
	  branch n = leaf n
	  leaf Unit          = True
	  leaf (Pointwise.Const _) = True
	  leaf (Var y)       = (y /= f)
	  leaf (Var g :@: n) | (g == f) = leaf n && (f `notElem` free n)
			     | otherwise = leaf n
	  leaf (n :@: m)     = leaf n && leaf m
	  leaf (n :&: m)     = leaf n && leaf m
	  leaf (Fst n)       = leaf n
	  leaf (Snd n)       = leaf n
	  leaf (Inl n)       = leaf n
	  leaf (Inr n)       = leaf n
	  leaf (In n)        = leaf n
	  leaf (Out n)       = leaf n
	  leaf _             = False
derivable _ = False

getVar :: String -> State Int String
getVar x = do seed <- get
	      modify (+1)
	      return (x ++ show seed)

fun :: Term -> String -> Funct
fun l r = evalState (aux l) 0
    where aux (Case _ (Lam x m) (Lam y n)) =
	      do f <- aux m
		 g <- aux n
		 return (f :++: g)
	  aux Unit        = return (Pointfree.Const One)
	  aux (Pointwise.Const _) = return (Pointfree.Const One)
	  aux (Var x) = liftM (Pointfree.Const . Base) (getVar "a")
	  aux (Var x :@: n) | x == r = return Id
	  aux (m :@: n) | null (free n) = aux m
			| null (free m) = aux n
			| otherwise = do f <- aux m
					 g <- aux n
					 return (f :**: g)
	  aux (m :&: n) | null (free n) = aux m
			| null (free m) = aux n
			| otherwise = do f <- aux m
					 g <- aux n
					 return (f :**: g)
	  aux (Fst n)   = aux n
	  aux (Snd n)   = aux n
	  aux (Inl n)   = aux n
	  aux (Inr n)   = aux n
	  aux (In n)    = aux n
	  aux (Out n)   = aux n

coa :: Term -> String -> Term
coa t r = aux t
    where aux (Case l (Lam x m) (Lam y n)) =
	      let f = aux m
		  g = aux n
		  in Case l (Lam x (Inl f)) (Lam y (Inr g))
	  aux Unit        = Unit
	  aux (Pointwise.Const _) = Unit
	  aux (Var x)     = Var x
	  aux (Var x :@: n) | x == r = n
	  aux (m :@: n) | null (free n) = aux m
			| null (free m) = aux n
			| otherwise = let f = aux m
					  g = aux n
					  in f :&: g
	  aux (m :&: n) | null (free n) = aux m
			| null (free m) = aux n
			| otherwise = let f = aux m
					  g = aux n
					  in f :&: g
	  aux (Fst n)   = aux n
	  aux (Snd n)   = aux n
	  aux (Inl n)   = aux n
	  aux (Inr n)   = aux n
	  aux (In n)    = aux n
	  aux (Out n)   = aux n

alg :: Term -> String -> Term -> Term
alg t r p = aux t p
    where aux (Case l (Lam x m) (Lam y n)) (Var p) =
	      let vl = p++"l"
		  vr = p++"r"
		  f = aux m (Var vl)
		  g = aux n (Var vr)
		  in Case (Var p) (Lam vl f) (Lam vr g)
	  aux Unit _        = Unit
	  aux (Pointwise.Const f) _ = Pointwise.Const f
	  aux (Var x) p     = p
	  aux (Var x :@: n) p | x == r = p
	  aux (m :@: n) p | null (free n) = let f = aux m p
					        g = aux n p
					        in f :@: g
			  | null (free m) = let f = aux m p
					        g = aux n p
					        in f :@: g
			  | otherwise = let f = aux m (Fst p)
					    g = aux n (Snd p)
					    in f :@: g
	  aux (m :&: n) p | null (free n) = let f = aux m p
					        g = aux n p
					        in f :&: g
			  | null (free m) = let f = aux m p
					        g = aux n p
					        in f :&: g
			  | otherwise = let f = aux m (Fst p)
					    g = aux n (Snd p)
					    in f :&: g
	  aux (Fst n) p = Fst (aux n p)
	  aux (Snd n) p = Snd (aux n p)
	  aux (Inl n) p = Inl (aux n p)
	  aux (Inr n) p = Inr (aux n p)
	  aux (In n)  p = In (aux n p)
	  aux (Out n) p = Out (aux n p)