module Agda.TypeChecking.Coverage.SplitTree where
import Data.Tree
import Test.QuickCheck
import Agda.Syntax.Common
import Agda.Syntax.Abstract.Name
import Agda.Utils.Monad
import Agda.Utils.Impossible
#include "../../undefined.h"
type SplitTree = SplitTree' QName
type SplitTrees = SplitTrees' QName
data SplitTree' a
=
SplittingDone
{ splitBindings :: Int
}
|
SplitAt
{ splitArg :: Int
, splitTrees :: SplitTrees' a
}
deriving (Eq)
type SplitTrees' a = [(a, SplitTree' a)]
data SplitTreeLabel a = SplitTreeLabel
{ lblConstructorName :: Maybe a
, lblSplitArg :: Maybe Int
, lblBindings :: Maybe Int
}
instance Show a => Show (SplitTreeLabel a) where
show (SplitTreeLabel Nothing Nothing (Just n)) = "done, " ++ show n ++ " bindings"
show (SplitTreeLabel Nothing (Just n) Nothing) = "split at " ++ show n
show (SplitTreeLabel (Just q) Nothing (Just n)) = show q ++ " -> done, " ++ show n ++ " bindings"
show (SplitTreeLabel (Just q) (Just n) Nothing) = show q ++ " -> split at " ++ show n
show _ = __IMPOSSIBLE__
toTree :: SplitTree' a -> Tree (SplitTreeLabel a)
toTree t = case t of
SplittingDone n -> Node (SplitTreeLabel Nothing Nothing (Just n)) []
SplitAt n ts -> Node (SplitTreeLabel Nothing (Just n) Nothing) $ toTrees ts
toTrees :: SplitTrees' a -> Forest (SplitTreeLabel a)
toTrees = map (\ (c,t) -> setCons c $ toTree t)
where
setCons :: a -> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
setCons c (Node l ts) = Node (l { lblConstructorName = Just c }) ts
instance Show a => Show (SplitTree' a) where
show = drawTree . fmap show . toTree
instance Arbitrary a => Arbitrary (SplitTree' a) where
arbitrary = frequency
[ (5, return $ SplittingDone 0)
, (3, SplitAt <$> choose (1,5) <*> (take 3 <$> listOf1 arbitrary))
]
newtype CName = CName String
instance Show CName where
show (CName s) = s
instance Arbitrary CName where
arbitrary = CName <$> elements
[ "zero", "suc", "nil", "cons", "left", "right", "just", "nothing" ]
testSplitTreePrinting = sample (arbitrary :: Gen (SplitTree' CName))