0

我正在 Idris 中实现红黑树。在这个实现中，节点除了携带有关其值和颜色的信息外，还携带有关其黑色高度的信息（即从该节点到任何叶子的黑色节点的数量，不包括自身）。

data Colour = Red | Black

data RBTree : Nat -> Type -> Type where
      Empty : Ord elem => RBTree Z elem
      Node : Ord elem => (left: RBTree p elem) -> (val: elem) -> (col: Colour) ->
                          (h: Nat) -> (right: RBTree q elem) -> RBTree h elem

为了实现插入功能，我必须实现一个平衡功能，它修复了红色节点有一个红色子节点的任何情况（这违反了红黑规则）。这是它修复的一种情况。

           (n)  Bz                                       (S n) Ry
               /  \                                           /  \
              /    \                                         /    \
        (n)  Ry     d          ---->                    (n) Bx     Bz (n)
            /  \                                           / \     / \
           /    \                                         /   \   /   \
      (n) Rx     c                                       a     b c     d
         /  \
        /    \
       a      b

Bx 表示节点 x 为黑色，Rx 表示节点 x 为红色。括号中的 n 是该节点的黑色高度。

这是平衡的代码。

balance : Ord elem => RBTree p elem -> elem -> Colour -> Nat -> RBTree q elem -> RBTree h elem
balance (Node (Node a x Red n b) y Red n c) z Black n d = Node (Node a x Black n b) y Red (S n) (Node c z Black n d)
balance (Node a x Red n (Node b y Red n c)) z Black n d = Node (Node a x Black n b) y Red (S n) (Node c z Black n d)
balance a x Black n (Node (Node b y Red n c) z Red n d) = Node (Node a x Black n b) y Red (S n) (Node c z Black n d)
balance a x Black n (Node b y Red n (Node c z Red n d)) = Node (Node a x Black n b) y Red (S n) (Node c z Black n d)
balance left val col ht right = (Node left val col ht right)

第一行（不是类型定义）是图中的内容。

当我运行它时，我得到了这个：

   |
27 | balance (Node (Node a x Red n b) y Red n c) z Black n d = Node (Node a x Black n b) y Red (S n) (Node c z Black n d)
   | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking left hand side of balance:
Can't match on balance (Node (Node a x Red n b) y Red n c) z Black n d

我不确定错误是什么。它可能与类型定义中的 p 和 q 有关吗？

4

0 回答 0