-- | 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 
  { TDiag -> Int
_width  :: !Int      -- ^ the width is the number of leaves, minus 1, of both diagrams
  , TDiag -> T
_domain :: !T        -- ^ the top diagram correspond to the /domain/
  , TDiag -> T
_range  :: !T        -- ^ the bottom diagram corresponds to the /range/
  }
  deriving (TDiag -> TDiag -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TDiag -> TDiag -> Bool
$c/= :: TDiag -> TDiag -> Bool
== :: TDiag -> TDiag -> Bool
$c== :: TDiag -> TDiag -> Bool
Eq,Eq TDiag
TDiag -> TDiag -> Bool
TDiag -> TDiag -> Ordering
TDiag -> TDiag -> TDiag
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TDiag -> TDiag -> TDiag
$cmin :: TDiag -> TDiag -> TDiag
max :: TDiag -> TDiag -> TDiag
$cmax :: TDiag -> TDiag -> TDiag
>= :: TDiag -> TDiag -> Bool
$c>= :: TDiag -> TDiag -> Bool
> :: TDiag -> TDiag -> Bool
$c> :: TDiag -> TDiag -> Bool
<= :: TDiag -> TDiag -> Bool
$c<= :: TDiag -> TDiag -> Bool
< :: TDiag -> TDiag -> Bool
$c< :: TDiag -> TDiag -> Bool
compare :: TDiag -> TDiag -> Ordering
$ccompare :: TDiag -> TDiag -> Ordering
Ord,Int -> TDiag -> ShowS
[TDiag] -> ShowS
TDiag -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TDiag] -> ShowS
$cshowList :: [TDiag] -> ShowS
show :: TDiag -> String
$cshow :: TDiag -> String
showsPrec :: Int -> TDiag -> ShowS
$cshowsPrec :: Int -> TDiag -> ShowS
Show)

instance DrawASCII TDiag where
  ascii :: TDiag -> ASCII
ascii = TDiag -> ASCII
asciiTDiag

instance HasWidth TDiag where
  width :: TDiag -> Int
width = TDiag -> Int
_width

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

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


isValidTDiag :: TDiag -> Bool
isValidTDiag :: TDiag -> Bool
isValidTDiag (TDiag Int
w T
top T
bot) = (forall a. Tree a -> Int
treeWidth T
top forall a. Eq a => a -> a -> Bool
== Int
w Bool -> Bool -> Bool
&& forall a. Tree a -> Int
treeWidth T
bot forall a. Eq a => a -> a -> Bool
== Int
w)

isPositive :: TDiag -> Bool
isPositive :: TDiag -> Bool
isPositive (TDiag Int
w T
top T
bot) = (T
bot forall a. Eq a => a -> a -> Bool
== Int -> T
rightVine Int
w)

isReduced :: TDiag -> Bool
isReduced :: TDiag -> Bool
isReduced TDiag
diag = (TDiag -> TDiag
reduce TDiag
diag forall a. Eq a => a -> a -> Bool
== TDiag
diag)

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

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

-- | The generators x0, x1, x2 ...
xk :: Int -> TDiag
xk :: Int -> TDiag
xk = Int -> TDiag
go where
  go :: Int -> TDiag
go Int
k | Int
kforall a. Ord a => a -> a -> Bool
< Int
0      = forall a. HasCallStack => String -> a
error String
"xk: negative indexed generator"
       | Int
kforall a. Eq a => a -> a -> Bool
==Int
0      = TDiag
x0
       | Bool
otherwise = let TDiag Int
_ T
t T
b = Int -> TDiag
go (Int
kforall a. Num a => a -> a -> a
-Int
1) 
                     in  Int -> T -> T -> TDiag
TDiag (Int
kforall a. Num a => a -> a -> a
+Int
2) (T -> T -> T
branch T
leaf T
t) (T -> T -> T
branch T
leaf T
b)

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

-- | A /positive diagram/ is a diagram whose bottom tree (the range) is a right vine.
positive :: T -> TDiag
positive :: T -> TDiag
positive T
t = Int -> T -> T -> TDiag
TDiag Int
w T
t (Int -> T
rightVine Int
w) where w :: Int
w = forall a. Tree a -> Int
treeWidth T
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 -> TDiag
inverse (TDiag Int
w T
top T
bot) = Int -> T -> T -> TDiag
TDiag Int
w T
bot T
top

-- | Decides whether two (possibly unreduced) tree diagrams represents the same group element in F.
equivalent :: TDiag -> TDiag -> Bool
equivalent :: TDiag -> TDiag -> Bool
equivalent TDiag
diag1 TDiag
diag2 = (TDiag
identity forall a. Eq a => a -> a -> Bool
== TDiag -> TDiag
reduce (TDiag -> TDiag -> TDiag
compose TDiag
diag1 (TDiag -> TDiag
inverse TDiag
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 :: TDiag -> TDiag
reduce = TDiag -> TDiag
worker where

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

  step :: TDiag -> Maybe TDiag
  step :: TDiag -> Maybe TDiag
step (TDiag Int
w T
top T
bot) = 
    if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
idxs 
      then forall a. Maybe a
Nothing
      else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int -> T -> T -> TDiag
TDiag Int
w' T
top' T
bot'
    where
      cs1 :: [Int]
cs1  = T -> [Int]
treeCaretList T
top
      cs2 :: [Int]
cs2  = T -> [Int]
treeCaretList T
bot
      idxs :: [Int]
idxs = [Int] -> [Int] -> [Int]
sortedIntersect [Int]
cs1 [Int]
cs2
      w' :: Int
w'   = Int
w forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
idxs
      top' :: T
top' = [Int] -> T -> T
removeCarets [Int]
idxs T
top
      bot' :: T
bot' = [Int] -> T -> T
removeCarets [Int]
idxs T
bot

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

-- | List of carets at the bottom of the tree, indexed by their left edge position
treeCaretList :: T -> [Int]
treeCaretList :: T -> [Int]
treeCaretList = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. Num a => a -> T -> (a, [a])
go Int
0 where
  go :: a -> T -> (a, [a])
go !a
x T
t = case T
t of 
    T
Lf        ->  (a
xforall a. Num a => a -> a -> a
+a
1 , []  )
    T
Ct        ->  (a
xforall a. Num a => a -> a -> a
+a
2 , [a
x] )
    Br T
t1 T
t2  ->  (a
x2  , [a]
cs1forall a. [a] -> [a] -> [a]
++[a]
cs2) where
      (a
x1 , [a]
cs1) = a -> T -> (a, [a])
go a
x  T
t1
      (a
x2 , [a]
cs2) = a -> T -> (a, [a])
go a
x1 T
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 :: [Int] -> T -> T
removeCarets [Int]
idxs T
tree = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
rem then T
final else forall a. HasCallStack => String -> a
error (String
"removeCarets: some stuff remained: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Int]
rem) where

  (Int
_,[Int]
rem,T
final) =  Int -> [Int] -> T -> (Int, [Int], T)
go Int
0 [Int]
idxs T
tree where

  go :: Int -> [Int] -> T -> (Int,[Int],T)
  go :: Int -> [Int] -> T -> (Int, [Int], T)
go !Int
x []         T
t  = (Int
x forall a. Num a => a -> a -> a
+ forall a. Tree a -> Int
treeWidth T
t , [] , T
t)
  go !Int
x iis :: [Int]
iis@(Int
i:[Int]
is) T
t  = case T
t of
    T
Lf        ->  (Int
xforall a. Num a => a -> a -> a
+Int
1 , [Int]
iis , T
t)
    T
Ct        ->  if Int
xforall a. Eq a => a -> a -> Bool
==Int
i then (Int
xforall a. Num a => a -> a -> a
+Int
2 , [Int]
is , T
Lf) else (Int
xforall a. Num a => a -> a -> a
+Int
2 , [Int]
iis , T
Ct)
    Br T
t1 T
t2  ->  (Int
x2  , [Int]
iis2 , forall {a}. Tree a -> Tree a -> Tree a
Br T
t1' T
t2') where
      (Int
x1 , [Int]
iis1 , T
t1') = Int -> [Int] -> T -> (Int, [Int], T)
go Int
x  [Int]
iis  T
t1
      (Int
x2 , [Int]
iis2 , T
t2') = Int -> [Int] -> T -> (Int, [Int], T)
go Int
x1 [Int]
iis1 T
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 :: TDiag -> TDiag -> TDiag
compose TDiag
d1 TDiag
d2 = TDiag -> TDiag
reduce (TDiag -> TDiag -> TDiag
composeDontReduce TDiag
d1 TDiag
d2)

-- | Compose two tree diagrams without reducing the result
composeDontReduce :: TDiag -> TDiag -> TDiag
composeDontReduce :: TDiag -> TDiag -> TDiag
composeDontReduce (TDiag Int
w1 T
top1 T
bot1) (TDiag Int
w2 T
top2 T
bot2) = TDiag
new where
  new :: TDiag
new = T -> T -> TDiag
mkTDiagDontReduce T
top' T
bot' 
  ([T]
list1,[T]
list2) = T -> T -> ([T], [T])
extensionToCommonTree T
bot1 T
top2
  top' :: T
top' = forall a b. [Tree a] -> Tree b -> Tree a
listGraft [T]
list1 T
top1
  bot' :: T
bot' = forall a b. [Tree a] -> Tree b -> Tree a
listGraft [T]
list2 T
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 :: T -> T -> ([T], [T])
extensionToCommonTree T
t1 T
t2 = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ (Int, Int) -> (T, T) -> ((Int, Int), ([T], [T]))
go (Int
0,Int
0) (T
t1,T
t2) where
  go :: (Int, Int) -> (T, T) -> ((Int, Int), ([T], [T]))
go (!Int
x1,!Int
x2) (!T
t1,!T
t2) = 
    case (T
t1,T
t2) of
      ( T
Lf       , T
Lf       ) -> ( (Int
x1forall a. Num a => a -> a -> a
+Int
n1 , Int
x2forall a. Num a => a -> a -> a
+Int
n2 ) , (             [T
Lf] ,             [T
Lf] ) )
      ( T
Lf       , Br T
_  T
_  ) -> ( (Int
x1forall a. Num a => a -> a -> a
+Int
n1 , Int
x2forall a. Num a => a -> a -> a
+Int
n2 ) , (             [T
t2] , forall a. Int -> a -> [a]
replicate Int
n2 T
Lf  ) )
      ( Br T
_  T
_  , T
Lf       ) -> ( (Int
x1forall a. Num a => a -> a -> a
+Int
n1 , Int
x2forall a. Num a => a -> a -> a
+Int
n2 ) , ( forall a. Int -> a -> [a]
replicate Int
n1 T
Lf  ,             [T
t1] ) )
      ( Br T
l1 T
r1 , Br T
l2 T
r2 ) 
        -> let ( (Int
x1' ,Int
x2' ) , ([T]
ps1,[T]
ps2) ) = (Int, Int) -> (T, T) -> ((Int, Int), ([T], [T]))
go (Int
x1 ,Int
x2 ) (T
l1,T
l2)
               ( (Int
x1'',Int
x2'') , ([T]
qs1,[T]
qs2) ) = (Int, Int) -> (T, T) -> ((Int, Int), ([T], [T]))
go (Int
x1',Int
x2') (T
r1,T
r2)
           in  ( (Int
x1'',Int
x2'') , ([T]
ps1forall a. [a] -> [a] -> [a]
++[T]
qs1, [T]
ps2forall a. [a] -> [a] -> [a]
++[T]
qs2) )
    where
      n1 :: Int
n1 = forall t. HasNumberOfLeaves t => t -> Int
numberOfLeaves T
t1
      n2 :: Int
n2 = forall t. HasNumberOfLeaves t => t -> Int
numberOfLeaves T
t2

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

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

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


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

-- | A (strict) binary tree with labelled leaves (but unlabelled nodes)
data Tree a
  = Branch !(Tree a) !(Tree a)
  | Leaf   !a
  deriving (Tree a -> Tree a -> Bool
forall a. Eq a => Tree a -> Tree a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Tree a -> Tree a -> Bool
$c/= :: forall a. Eq a => Tree a -> Tree a -> Bool
== :: Tree a -> Tree a -> Bool
$c== :: forall a. Eq a => Tree a -> Tree a -> Bool
Eq,Tree a -> Tree a -> Bool
Tree a -> Tree a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (Tree a)
forall a. Ord a => Tree a -> Tree a -> Bool
forall a. Ord a => Tree a -> Tree a -> Ordering
forall a. Ord a => Tree a -> Tree a -> Tree a
min :: Tree a -> Tree a -> Tree a
$cmin :: forall a. Ord a => Tree a -> Tree a -> Tree a
max :: Tree a -> Tree a -> Tree a
$cmax :: forall a. Ord a => Tree a -> Tree a -> Tree a
>= :: Tree a -> Tree a -> Bool
$c>= :: forall a. Ord a => Tree a -> Tree a -> Bool
> :: Tree a -> Tree a -> Bool
$c> :: forall a. Ord a => Tree a -> Tree a -> Bool
<= :: Tree a -> Tree a -> Bool
$c<= :: forall a. Ord a => Tree a -> Tree a -> Bool
< :: Tree a -> Tree a -> Bool
$c< :: forall a. Ord a => Tree a -> Tree a -> Bool
compare :: Tree a -> Tree a -> Ordering
$ccompare :: forall a. Ord a => Tree a -> Tree a -> Ordering
Ord,Int -> Tree a -> ShowS
forall a. Show a => Int -> Tree a -> ShowS
forall a. Show a => [Tree a] -> ShowS
forall a. Show a => Tree a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Tree a] -> ShowS
$cshowList :: forall a. Show a => [Tree a] -> ShowS
show :: Tree a -> String
$cshow :: forall a. Show a => Tree a -> String
showsPrec :: Int -> Tree a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Tree a -> ShowS
Show,forall a b. a -> Tree b -> Tree a
forall a b. (a -> b) -> Tree a -> Tree b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Tree b -> Tree a
$c<$ :: forall a b. a -> Tree b -> Tree a
fmap :: forall a b. (a -> b) -> Tree a -> Tree b
$cfmap :: forall a b. (a -> b) -> Tree a -> Tree b
Functor)

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

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

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

instance DrawASCII T where
  ascii :: T -> ASCII
ascii = T -> ASCII
asciiT 

instance HasNumberOfLeaves (Tree a) where
  numberOfLeaves :: Tree a -> Int
numberOfLeaves = forall a. Tree a -> Int
treeNumberOfLeaves

instance HasWidth (Tree a) where
  width :: Tree a -> Int
width = forall a. Tree a -> Int
treeWidth

leaf :: T
leaf :: T
leaf = forall a. a -> Tree a
Leaf ()

branch :: T -> T -> T
branch :: T -> T -> T
branch = forall {a}. Tree a -> Tree a -> Tree a
Branch

caret :: T
caret :: T
caret = T -> T -> T
branch T
leaf T
leaf

treeNumberOfLeaves :: Tree a -> Int
treeNumberOfLeaves :: forall a. Tree a -> Int
treeNumberOfLeaves = forall {a} {a}. Num a => Tree a -> a
go where
  go :: Tree a -> a
go (Branch Tree a
l Tree a
r) = Tree a -> a
go Tree a
l forall a. Num a => a -> a -> a
+ Tree a -> a
go Tree a
r
  go (Leaf   a
_  ) = a
1  

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

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

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

-- | \"Right vine\" of the given width 
rightVine :: Int -> T
rightVine :: Int -> T
rightVine Int
k 
  | Int
kforall a. Ord a => a -> a -> Bool
< Int
0      = forall a. HasCallStack => String -> a
error String
"rightVine: negative width"
  | Int
kforall a. Eq a => a -> a -> Bool
==Int
0      = T
leaf
  | Bool
otherwise = T -> T -> T
branch T
leaf (Int -> T
rightVine (Int
kforall a. Num a => a -> a -> a
-Int
1))

-- | \"Left vine\" of the given width 
leftVine :: Int -> T
leftVine :: Int -> T
leftVine Int
k 
  | Int
kforall a. Ord a => a -> a -> Bool
< Int
0      = forall a. HasCallStack => String -> a
error String
"leftVine: negative width"
  | Int
kforall a. Eq a => a -> a -> Bool
==Int
0      = T
leaf
  | Bool
otherwise = T -> T -> T
branch (Int -> T
leftVine (Int
kforall a. Num a => a -> a -> a
-Int
1)) T
leaf 

-- | Flips each node of a binary tree
flipTree :: Tree a -> Tree a
flipTree :: forall a. Tree a -> Tree a
flipTree = forall a. Tree a -> Tree a
go where
  go :: Tree a -> Tree a
go Tree a
t = case Tree a
t of
    Leaf   a
_   -> Tree a
t
    Branch Tree a
l Tree a
r -> forall {a}. Tree a -> Tree a -> Tree a
Branch (Tree a -> Tree a
go Tree a
r) (Tree a -> Tree a
go Tree a
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 :: forall a. Tree a -> BinTree a
toBinTree = forall a. Tree a -> BinTree a
go where
  go :: Tree a -> BinTree a
go (Branch Tree a
l Tree a
r) = forall a. BinTree a -> BinTree a -> BinTree a
B.Branch (Tree a -> BinTree a
go Tree a
l) (Tree a -> BinTree a
go Tree a
r)
  go (Leaf   a
y  ) = forall a. a -> BinTree a
B.Leaf   a
y

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

pattern $bLf :: T
$mLf :: forall {r}. T -> ((# #) -> r) -> ((# #) -> r) -> r
Lf     = Leaf ()
pattern $bBr :: forall {a}. Tree a -> Tree a -> Tree a
$mBr :: forall {r} {a}.
Tree a -> (Tree a -> Tree a -> r) -> ((# #) -> r) -> r
Br l r = Branch l r
pattern $bCt :: T
$mCt :: forall {r}. T -> ((# #) -> r) -> ((# #) -> r) -> r
Ct     = Br Lf Lf
pattern $bX0 :: TDiag
$mX0 :: forall {r}. TDiag -> ((# #) -> r) -> ((# #) -> r) -> r
X0     = TDiag 2        (Br Ct Lf)         (Br Lf Ct)
pattern $bX1 :: TDiag
$mX1 :: forall {r}. TDiag -> ((# #) -> r) -> ((# #) -> r) -> r
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 :: T -> ASCII
asciiT = Bool -> T -> ASCII
asciiT' Bool
False

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

  go :: Tree a -> ASCII
go Tree a
t = case Tree a
t of
    Leaf a
_                   -> ASCII
emptyRect 
    Branch Tree a
l Tree a
r -> 
      if Int
yl forall a. Ord a => a -> a -> Bool
>= Int
yr
        then (Int, Int) -> ASCII -> ASCII -> ASCII
pasteOnto (Int
ylforall a. Num a => a -> a -> a
+Int
yrforall a. Num a => a -> a -> a
+Int
1,if Bool
inv then Int
yr else Int
0) (Int -> ASCII
rs forall a b. (a -> b) -> a -> b
$ Int
ylforall a. Num a => a -> a -> a
+Int
1) forall a b. (a -> b) -> a -> b
$ 
               HAlign -> ASCII -> ASCII -> ASCII
vcat HAlign
HCenter 
                 (Int -> ASCII
bc forall a b. (a -> b) -> a -> b
$ Int
yrforall a. Num a => a -> a -> a
+Int
1) 
                 (VAlign -> ASCII -> ASCII -> ASCII
hcat VAlign
bot ASCII
al ASCII
ar)
        else (Int, Int) -> ASCII -> ASCII -> ASCII
pasteOnto (Int
yl, if Bool
inv then Int
yl else Int
0) (Int -> ASCII
ls forall a b. (a -> b) -> a -> b
$ Int
yrforall a. Num a => a -> a -> a
+Int
1) forall a b. (a -> b) -> a -> b
$
               HAlign -> ASCII -> ASCII -> ASCII
vcat HAlign
HCenter 
                 (Int -> ASCII
bc forall a b. (a -> b) -> a -> b
$ Int
ylforall a. Num a => a -> a -> a
+Int
1) 
                 (VAlign -> ASCII -> ASCII -> ASCII
hcat VAlign
bot ASCII
al ASCII
ar)
      where
        al :: ASCII
al = Tree a -> ASCII
go Tree a
l
        ar :: ASCII
ar = Tree a -> ASCII
go Tree a
r
        yl :: Int
yl = ASCII -> Int
asciiYSize ASCII
al 
        yr :: Int
yr = ASCII -> Int
asciiYSize ASCII
ar 

  bot :: VAlign
bot = if Bool
inv then VAlign
VTop else VAlign
VBottom
  hcat :: VAlign -> ASCII -> ASCII -> ASCII
hcat VAlign
align ASCII
p ASCII
q = VAlign -> HSep -> [ASCII] -> ASCII
hCatWith VAlign
align (String -> HSep
HSepString String
"  ") [ASCII
p,ASCII
q]
  vcat :: HAlign -> ASCII -> ASCII -> ASCII
vcat HAlign
align ASCII
p ASCII
q = HAlign -> VSep -> [ASCII] -> ASCII
vCatWith HAlign
align VSep
VSepEmpty forall a b. (a -> b) -> a -> b
$ if Bool
inv then [ASCII
q,ASCII
p] else [ASCII
p,ASCII
q]
  bc :: Int -> ASCII
bc = if Bool
inv then Int -> ASCII
asciiBigInvCaret   else Int -> ASCII
asciiBigCaret
  ls :: Int -> ASCII
ls = if Bool
inv then Int -> ASCII
asciiBigRightSlope else Int -> ASCII
asciiBigLeftSlope
  rs :: Int -> ASCII
rs = if Bool
inv then Int -> ASCII
asciiBigLeftSlope  else Int -> ASCII
asciiBigRightSlope

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

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

  asciiBigLeftSlope :: Int -> ASCII  
  asciiBigLeftSlope :: Int -> ASCII
asciiBigLeftSlope Int
k = if Int
kforall a. Ord a => a -> a -> Bool
>Int
0 
    then [String] -> ASCII
asciiFromLines [ forall a. Int -> a -> [a]
replicate Int
l Char
' ' forall a. [a] -> [a] -> [a]
++ String
"/" | Int
l<-[Int
kforall a. Num a => a -> a -> a
-Int
1,Int
kforall a. Num a => a -> a -> a
-Int
2..Int
0] ]
    else ASCII
emptyRect

  asciiBigRightSlope :: Int -> ASCII  
  asciiBigRightSlope :: Int -> ASCII
asciiBigRightSlope Int
k = if Int
kforall a. Ord a => a -> a -> Bool
>Int
0 
    then [String] -> ASCII
asciiFromLines [ forall a. Int -> a -> [a]
replicate Int
l Char
' ' forall a. [a] -> [a] -> [a]
++ String
"\\" | Int
l<-[Int
0..Int
kforall a. Num a => a -> a -> a
-Int
1] ]
    else ASCII
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 :: T -> ASCII
asciiTLabels = Bool -> T -> ASCII
asciiTLabels' Bool
False

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

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