Skip to content

Instantly share code, notes, and snippets.

@comfly comfly/ProveBST.hs
Created Jun 7, 2016

What would you like to do?
BST Prover
module Main where
data Tree a = Leaf | Node a (Tree a) (Tree a)
isBST :: Tree Double -> Bool
isBST = fst . isBST'
where isBST' Leaf = (True, Nothing)
isBST' (Node n left right) =
let (l, lminmax) = isBST' left
~(r, rminmax) = isBST' right
in if l && r then minimax n lminmax rminmax else (False, Nothing)
minimax n Nothing Nothing = (True, pure (n, n))
minimax n Nothing (Just (rmin, rmax)) = (n < rmin, pure (n, rmax))
minimax n (Just (lmin, lmax)) Nothing = (n >= lmax, pure (lmin, n))
minimax n (Just (lmin, lmax)) (Just (rmin, rmax)) = (n >= lmax && n < rmin, pure (lmin, rmax))
tree1 = Node 7
(Node 3
(Node 5
(Node 4 Leaf Leaf)
(Node 6 Leaf Leaf)))
(Node 9
(Node 2 Leaf Leaf)
(Node 10 Leaf Leaf))
tree2 = Node 7
(Node 3
(Node 2 Leaf Leaf)
(Node 5
(Node 4 Leaf Leaf)
(Node 6 Leaf Leaf))) -- (Node 8 Leaf Leaf)))
(Node 9 Leaf (Node 10 Leaf Leaf))
tree3 = Node 7 Leaf Leaf
tree4 = Leaf
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.