-- | Thompson's group F.
--
-- See eg. <https://en.wikipedia.org/wiki/Thompson_groups>
--
-- Based mainly on James Michael Belk's PhD thesis \"THOMPSON'S GROUP F\";
-- see <http://www.math.u-psud.fr/~breuilla/Belk.pdf>
--

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, BangPatterns, PatternSynonyms, DeriveFunctor #-}
module Math.Combinat.Groups.Thompson.F where

--------------------------------------------------------------------------------

import Data.List

import Math.Combinat.Classes
import Math.Combinat.ASCII

import Math.Combinat.Trees.Binary ( BinTree )
import qualified Math.Combinat.Trees.Binary as B

--------------------------------------------------------------------------------
-- * Tree diagrams

-- | A tree diagram, consisting of two binary trees with the same number of leaves, 
-- representing an element of the group F.
data TDiag = TDiag 
  { _width  :: !Int      -- ^ the width is the number of leaves, minus 1, of both diagrams
  , _domain :: !T        -- ^ the top diagram correspond to the /domain/
  , _range  :: !T        -- ^ the bottom diagram corresponds to the /range/
  }
  deriving (Eq,Ord,Show)

instance DrawASCII TDiag where
  ascii = asciiTDiag

instance HasWidth TDiag where
  width = _width

-- | Creates a tree diagram from two trees
mkTDiag :: T -> T -> TDiag 
mkTDiag d1 d2 = reduce $ mkTDiagDontReduce d1 d2

-- | Creates a tree diagram, but does not reduce it.
mkTDiagDontReduce :: T -> T -> TDiag 
mkTDiagDontReduce top bot = 
  if w1 == w2 
    then TDiag w1 top bot 
    else error "mkTDiag: widths do not match"
  where
    w1 = treeWidth top 
    w2 = treeWidth bot


isValidTDiag :: TDiag -> Bool
isValidTDiag (TDiag w top bot) = (treeWidth top == w && treeWidth bot == w)

isPositive :: TDiag -> Bool
isPositive (TDiag w top bot) = (bot == rightVine w)

isReduced :: TDiag -> Bool
isReduced diag = (reduce diag == diag)

-- | The generator x0
x0 :: TDiag
x0 = TDiag 2 top bot where
  top = branch caret leaf
  bot = branch leaf  caret

-- | The generator x1
x1 :: TDiag
x1 = xk 1

-- | The generators x0, x1, x2 ...
xk :: Int -> TDiag
xk = go where
  go k | k< 0      = error "xk: negative indexed generator"
       | k==0      = x0
       | otherwise = let TDiag _ t b = go (k-1) 
                     in  TDiag (k+2) (branch leaf t) (branch leaf b)

-- | The identity element in the group F                     
identity :: TDiag
identity = TDiag 0 Lf Lf

-- | A /positive diagram/ is a diagram whose bottom tree (the range) is a right vine.
positive :: T -> TDiag
positive t = TDiag w t (rightVine w) where w = treeWidth t

-- | Swaps the top and bottom of a tree diagram. This is the inverse in the group F.
-- (Note: we don't do reduction here, as this operation keeps the reducedness)
inverse :: TDiag -> TDiag
inverse (TDiag w top bot) = TDiag w bot top

-- | Decides whether two (possibly unreduced) tree diagrams represents the same group element in F.
equivalent :: TDiag -> TDiag -> Bool
equivalent diag1 diag2 = (identity == reduce (compose diag1 (inverse diag2)))

--------------------------------------------------------------------------------
-- * Reduction of tree diagrams

-- | Reduces a diagram. The result is a normal form of an element in the group F.
reduce :: TDiag -> TDiag
reduce = worker where

  worker :: TDiag -> TDiag
  worker diag = case step diag of
    Nothing    -> diag
    Just diag' -> worker diag'

  step :: TDiag -> Maybe TDiag
  step (TDiag w top bot) = 
    if null idxs 
      then Nothing
      else Just $ TDiag w' top' bot'
    where
      cs1  = treeCaretList top
      cs2  = treeCaretList bot
      idxs = sortedIntersect cs1 cs2
      w'   = w - length idxs
      top' = removeCarets idxs top
      bot' = removeCarets idxs bot

  -- | Intersects sorted lists      
  sortedIntersect :: [Int] -> [Int] -> [Int]
  sortedIntersect = go where
    go [] _  = []
    go _  [] = []
    go xxs@(x:xs) yys@(y:ys) = case compare x y of
      LT ->     go  xs yys
      EQ -> x : go  xs  ys
      GT ->     go xxs  ys

-- | List of carets at the bottom of the tree, indexed by their left edge position
treeCaretList :: T -> [Int]
treeCaretList = snd . go 0 where
  go !x t = case t of 
    Lf        ->  (x+1 , []  )
    Ct        ->  (x+2 , [x] )
    Br t1 t2  ->  (x2  , cs1++cs2) where
      (x1 , cs1) = go x  t1
      (x2 , cs2) = go x1 t2

-- | Remove the carets with the given indices 
-- (throws an error if there is no caret at the given index)
removeCarets :: [Int] -> T -> T
removeCarets idxs tree = if null rem then final else error ("removeCarets: some stuff remained: " ++ show rem) where

  (_,rem,final) =  go 0 idxs tree where

  go :: Int -> [Int] -> T -> (Int,[Int],T)
  go !x []         t  = (x + treeWidth t , [] , t)
  go !x iis@(i:is) t  = case t of
    Lf        ->  (x+1 , iis , t)
    Ct        ->  if x==i then (x+2 , is , Lf) else (x+2 , iis , Ct)
    Br t1 t2  ->  (x2  , iis2 , Br t1' t2') where
      (x1 , iis1 , t1') = go x  iis  t1
      (x2 , iis2 , t2') = go x1 iis1 t2
      
--------------------------------------------------------------------------------
-- * Composition of tree diagrams

-- | If @diag1@ corresponds to the PL function @f@, and @diag2@ to @g@, then @compose diag1 diag2@ 
-- will correspond to @(g.f)@ (note that the order is opposite than normal function composition!)
--
-- This is the multiplication in the group F.
--
compose :: TDiag -> TDiag -> TDiag
compose d1 d2 = reduce (composeDontReduce d1 d2)

-- | Compose two tree diagrams without reducing the result
composeDontReduce :: TDiag -> TDiag -> TDiag
composeDontReduce (TDiag w1 top1 bot1) (TDiag w2 top2 bot2) = new where
  new = mkTDiagDontReduce top' bot' 
  (list1,list2) = extensionToCommonTree bot1 top2
  top' = listGraft list1 top1
  bot' = listGraft list2 bot2

-- | Given two binary trees, we return a pair of list of subtrees which, grafted the to leaves of
-- the first (resp. the second) tree, results in the same extended tree.
extensionToCommonTree :: T -> T -> ([T],[T])
extensionToCommonTree t1 t2 = snd $ go (0,0) (t1,t2) where
  go (!x1,!x2) (!t1,!t2) = 
    case (t1,t2) of
      ( Lf       , Lf       ) -> ( (x1+n1 , x2+n2 ) , (             [Lf] ,             [Lf] ) )
      ( Lf       , Br _  _  ) -> ( (x1+n1 , x2+n2 ) , (             [t2] , replicate n2 Lf  ) )
      ( Br _  _  , Lf       ) -> ( (x1+n1 , x2+n2 ) , ( replicate n1 Lf  ,             [t1] ) )
      ( Br l1 r1 , Br l2 r2 ) 
        -> let ( (x1' ,x2' ) , (ps1,ps2) ) = go (x1 ,x2 ) (l1,l2)
               ( (x1'',x2'') , (qs1,qs2) ) = go (x1',x2') (r1,r2)
           in  ( (x1'',x2'') , (ps1++qs1, ps2++qs2) )
    where
      n1 = numberOfLeaves t1
      n2 = numberOfLeaves t2

--------------------------------------------------------------------------------
-- * Subdivions

-- | Returns the list of dyadic subdivision points
subdivision1 :: T -> [Rational]
subdivision1 = go 0 1 where
  go !a !b t = case t of
    Leaf   _   -> [a,b]
    Branch l r -> go a c l ++ tail (go c b r) where c = (a+b)/2

-- | Returns the list of dyadic intervals
subdivision2 :: T -> [(Rational,Rational)]
subdivision2 = go 0 1 where
  go !a !b t = case t of
    Leaf   _   -> [(a,b)]
    Branch l r -> go a c l ++ go c b r where c = (a+b)/2


--------------------------------------------------------------------------------
-- * Binary trees

-- | A (strict) binary tree with labelled leaves (but unlabelled nodes)
data Tree a
  = Branch !(Tree a) !(Tree a)
  | Leaf   !a
  deriving (Eq,Ord,Show,Functor)

-- | The monadic join operation of binary trees
graft :: Tree (Tree a) -> Tree a
graft = go where
  go (Branch l r) = Branch (go l) (go r)
  go (Leaf   t  ) = t 

-- | A list version of 'graft'
listGraft :: [Tree a] -> Tree b -> Tree a
listGraft subs big = snd $ go subs big where  
  go ggs@(g:gs) t = case t of
    Leaf   _   -> (gs,g)
    Branch l r -> (gs2, Branch l' r') where
                    (gs1,l') = go ggs l
                    (gs2,r') = go gs1 r

-- | A completely unlabelled binary tree
type T = Tree ()

instance DrawASCII T where
  ascii = asciiT 

instance HasNumberOfLeaves (Tree a) where
  numberOfLeaves = treeNumberOfLeaves

instance HasWidth (Tree a) where
  width = treeWidth

leaf :: T
leaf = Leaf ()

branch :: T -> T -> T
branch = Branch

caret :: T
caret = branch leaf leaf

treeNumberOfLeaves :: Tree a -> Int
treeNumberOfLeaves = go where
  go (Branch l r) = go l + go r
  go (Leaf   _  ) = 1  

-- | The width of the tree is the number of leaves minus 1.
treeWidth :: Tree a -> Int
treeWidth t = numberOfLeaves t - 1

-- | Enumerates the leaves a tree, starting from 0
enumerate_ :: Tree a -> Tree Int
enumerate_ = snd . enumerate

-- | Enumerates the leaves a tree, and also returns the number of leaves
enumerate :: Tree a -> (Int, Tree Int)
enumerate = go 0 where
  go !k t = case t of
    Leaf   _   -> (k+1 , Leaf k)
    Branch l r -> let (k' ,l') = go k  l
                      (k'',r') = go k' r
                  in (k'', Branch l' r') 

-- | \"Right vine\" of the given width 
rightVine :: Int -> T
rightVine k 
  | k< 0      = error "rightVine: negative width"
  | k==0      = leaf
  | otherwise = branch leaf (rightVine (k-1))

-- | \"Left vine\" of the given width 
leftVine :: Int -> T
leftVine k 
  | k< 0      = error "leftVine: negative width"
  | k==0      = leaf
  | otherwise = branch (leftVine (k-1)) leaf 

-- | Flips each node of a binary tree
flipTree :: Tree a -> Tree a
flipTree = go where
  go t = case t of
    Leaf   _   -> t
    Branch l r -> Branch (go r) (go l)

--------------------------------------------------------------------------------
-- * Conversion to\/from BinTree

-- | 'Tree' and 'BinTree' are the same type, except that 'Tree' is strict.
--
-- TODO: maybe unify these two types? Until that, you can convert between the two
-- with these functions if necessary.
--
toBinTree :: Tree a -> B.BinTree a
toBinTree = go where
  go (Branch l r) = B.Branch (go l) (go r)
  go (Leaf   y  ) = B.Leaf   y

fromBinTree :: B.BinTree a -> Tree a 
fromBinTree = go where
  go (B.Branch l r) = Branch (go l) (go r)
  go (B.Leaf   y  ) = Leaf   y
    
--------------------------------------------------------------------------------
-- * Pattern synonyms

pattern Lf     = Leaf ()
pattern Br l r = Branch l r
pattern Ct     = Br Lf Lf
pattern X0     = TDiag 2        (Br Ct Lf)         (Br Lf Ct)
pattern X1     = TDiag 3 (Br Lf (Br Ct Lf)) (Br Lf (Br Lf Ct))

--------------------------------------------------------------------------------
-- * ASCII

-- | Draws a binary tree, with all leaves at the same (bottom) row
asciiT :: T -> ASCII
asciiT = asciiT' False

-- | Draws a binary tree; when the boolean flag is @True@, we draw upside down
asciiT' :: Bool -> T -> ASCII
asciiT' inv = go where

  go t = case t of
    Leaf _                   -> emptyRect 
    Branch l r -> 
      if yl >= yr
        then pasteOnto (yl+yr+1,if inv then yr else 0) (rs $ yl+1) $ 
               vcat HCenter 
                 (bc $ yr+1) 
                 (hcat bot al ar)
        else pasteOnto (yl, if inv then yl else 0) (ls $ yr+1) $
               vcat HCenter 
                 (bc $ yl+1) 
                 (hcat bot al ar)
      where
        al = go l
        ar = go r
        yl = asciiYSize al 
        yr = asciiYSize ar 

  bot = if inv then VTop else VBottom
  hcat align p q = hCatWith align (HSepString "  ") [p,q]
  vcat align p q = vCatWith align VSepEmpty $ if inv then [q,p] else [p,q]
  bc = if inv then asciiBigInvCaret   else asciiBigCaret
  ls = if inv then asciiBigRightSlope else asciiBigLeftSlope
  rs = if inv then asciiBigLeftSlope  else asciiBigRightSlope

  asciiBigCaret :: Int -> ASCII
  asciiBigCaret k = hCatWith VTop HSepEmpty [ asciiBigLeftSlope k , asciiBigRightSlope k ]

  asciiBigInvCaret :: Int -> ASCII
  asciiBigInvCaret k = hCatWith VTop HSepEmpty [ asciiBigRightSlope k , asciiBigLeftSlope k ]

  asciiBigLeftSlope :: Int -> ASCII  
  asciiBigLeftSlope k = if k>0 
    then asciiFromLines [ replicate l ' ' ++ "/" | l<-[k-1,k-2..0] ]
    else emptyRect

  asciiBigRightSlope :: Int -> ASCII  
  asciiBigRightSlope k = if k>0 
    then asciiFromLines [ replicate l ' ' ++ "\\" | l<-[0..k-1] ]
    else emptyRect
  
-- | Draws a binary tree, with all leaves at the same (bottom) row, and labelling
-- the leaves starting with 0 (continuing with letters after 9)
asciiTLabels :: T -> ASCII
asciiTLabels = asciiTLabels' False

-- | When the flag is true, we draw upside down
asciiTLabels' :: Bool -> T -> ASCII
asciiTLabels' inv t = 
  if inv 
    then vCatWith HLeft VSepEmpty [ labels , asciiT' inv t ]
    else vCatWith HLeft VSepEmpty [ asciiT' inv t , labels ]
  where
    w = treeWidth t
    labels = asciiFromString $ intersperse ' ' $ take (w+1) allLabels
    allLabels = ['0'..'9'] ++ ['a'..'z']
    
-- | Draws a tree diagram
asciiTDiag :: TDiag -> ASCII
asciiTDiag (TDiag _ top bot) = vCatWith HLeft (VSepString " ") [asciiT' False top , asciiT' True bot]

--------------------------------------------------------------------------------