{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
module Fcf.Alg.Tree where
import qualified GHC.TypeLits as TL
import Fcf
import Fcf.Data.Nat
import Fcf.Alg.List
import Fcf.Alg.Morphism
import Fcf.Data.Tree
data TreeF a b = NodeF a [b]
type instance Eval (Map f ('NodeF a '[])) = 'NodeF a '[]
type instance Eval (Map f ('NodeF a (b ': bs))) = 'NodeF a (Eval (Map f (b ': bs)))
data TreeToFix :: Tree a -> Exp (Fix (TreeF a))
type instance Eval (TreeToFix ('Node a '[])) = 'Fix ('NodeF a '[])
type instance Eval (TreeToFix ('Node a (b ': bs))) =
'Fix ('NodeF a (Eval (Map TreeToFix (b ': bs))))
data SumNodesAlg :: Algebra (TreeF Nat) Nat
type instance Eval (SumNodesAlg ('NodeF x '[])) = x
type instance Eval (SumNodesAlg ('NodeF x (b ': bs))) = x TL.+ (Eval (Sum (b ': bs)))
data CountNodesAlg :: Algebra (TreeF a) Nat
type instance Eval (CountNodesAlg ('NodeF x '[])) = 1
type instance Eval (CountNodesAlg ('NodeF x (b ': bs))) = 1 TL.+ (Eval (Sum (b ': bs)))
data Size :: Tree a -> Exp Nat
type instance Eval (Size tr) = Eval (Cata CountNodesAlg =<< TreeToFix tr)
data BuildNodeCoA :: CoAlgebra (TreeF Nat) Nat
type instance Eval (BuildNodeCoA n) =
If (Eval (((2 TL.* n) TL.+ 1) >= 8))
('NodeF n '[])
('NodeF n '[ 2 TL.* n, (2 TL.* n) TL.+ 1 ])
data BuildFibTreeCoA :: CoAlgebra (TreeF Nat) Nat
type instance Eval (BuildFibTreeCoA n) =
If (Eval (n >= 2))
('NodeF 0 '[n TL.- 1, n TL.- 2])
('NodeF n '[])
data Fib :: Nat -> Exp Nat
type instance Eval (Fib n) = Eval (Hylo SumNodesAlg BuildFibTreeCoA n)
data BTreeF a b = BEmptyF | BNodeF a b b
type instance Eval (Map f 'BEmptyF) = 'BEmptyF
type instance Eval (Map f ('BNodeF a b1 b2)) = 'BNodeF a (Eval (f b1)) (Eval (f b2))
data PartHlp :: (a -> a -> Exp Bool) -> CoAlgebra (BTreeF a) [a]
type instance Eval (PartHlp _ '[]) = 'BEmptyF
type instance Eval (PartHlp smaller (h ': t)) =
'BNodeF h
(Eval (Filter (smaller h) t))
(Eval (Filter (Not <=< smaller h) t))
data SymbolCompareInc :: TL.Symbol -> TL.Symbol -> Exp Bool
type instance Eval (SymbolCompareInc n1 n2) = Eval (TyEq (TL.CmpSymbol n1 n2) 'LT)
data SymbolCompareDec :: TL.Symbol -> TL.Symbol -> Exp Bool
type instance Eval (SymbolCompareDec n1 n2) = Eval (TyEq (TL.CmpSymbol n1 n2) 'GT)
data Inord :: Algebra (BTreeF a) [a]
type instance Eval (Inord 'BEmptyF) = '[]
type instance Eval (Inord ('BNodeF v l r)) = Eval (l ++ (Eval ('[v] ++ r)))
data Qsort :: (a -> a -> Exp Bool) -> [a] -> Exp [a]
type instance Eval (Qsort cmp lst) = Eval (Hylo Inord (PartCmp cmp) lst)
data PartCmp :: (a -> a -> Exp Bool) -> CoAlgebra (BTreeF a) [a]
type instance Eval (PartCmp cmp coalg) = Eval (PartHlp (Flip cmp) coalg)