如何解决Idris函数在红黑树实现上获取模式匹配错误
我正在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有关吗?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。