Tree.idr

module Tree

mutual
  data Node : (Nat) -> a -> Type where
    Leaf : a -> Node 1 a
    Node2 : FingerTree n a -> FingerTree m a -> Node (n + m) a
    Node3 : FingerTree n a -> FingerTree m a -> FingerTree p a -> Node (n + m + p) a

  data FingerTree : Nat -> a -> Type where
    Empty : FingerTree 0 a
    Single : {n : Nat} -> Node n a -> FingerTree n a
    Deep : {n : Nat} -> {m : Nat} -> {p : Nat} -> Digit n a -> FingerTree m (Node m a) -> Digit p a -> FingerTree (m + n + p) a

  data Digit : Nat -> a -> Type where
    One : FingerTree n a -> Digit n a
    Two : FingerTree n a -> FingerTree m a -> Digit (n + m) a
    Three : FingerTree n a -> FingerTree m a -> FingerTree p a -> Digit (n + m + p) a
    Four : FingerTree n a -> FingerTree m a -> FingerTree p a -> FingerTree q a -> Digit (n + m + p + q) a

      
infixr 5 <|

(<|) : {n : Nat} -> {m : Nat} -> Node n a -> FingerTree m a -> FingerTree (n + m) a
(<|) {n} {m = Z} a Empty = rewrite plusCommutative n Z in Single a
(<|) a (Single b) = Deep (One (Single a)) Empty (One (Single b))
-- (<|) av (Deep (Four b c d e) m p) = Deep (Two (Single av) b) (Node3 c d e <| m) p
-- (<|) a (Deep (Three b c d) m p) = (Deep (Four (Single a) b c d) m p)
-- (<|) a (Deep (Two b c d) m p) = (Deep (Tree (Single a) b c d) m p)
(<|) a (Deep (One b) m p) = (Deep (Two (Single a) b) m p)

{-

Empty
Single a
Deep [b] Empty [a]
Deep (c, b) Empty [a]
Deep (d, c, b) Empty [a]
Deep (e, d, c, b) Empty [a]
Deep (f, e) (Node3 d c b <| Empty) [a]
Deep (f, e) (Single (Node3 d c b)) [a]

-}

----
{-
- + Errors (1)
 `-- Tree.idr line 30 col 5:
     When checking right hand side of <| with expected type
             FingerTree (n + (m + n + p)) a
     
     Type mismatch between
             FingerTree (m + (n1 + n) + p) a (Type of Deep (Two (Single a) b) m p)
     and
             FingerTree (plus n1 (plus (plus m n) p)) a (Expected type)
     
     Specifically:
             Type mismatch between
                     plus (plus m (n1 + n)) p
             and
                     plus n1 (plus (plus m n) p)
                     
                     -}