{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Coverage.SplitTree where
import Data.Tree
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Literal
import Agda.TypeChecking.Pretty ( PrettyTCM(..) )
import Agda.Utils.Monad
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
type SplitTree = SplitTree' SplitTag
type SplitTrees = SplitTrees' SplitTag
data SplitTree' a
=
SplittingDone
{ splitBindings :: Int
}
|
SplitAt
{ splitArg :: Arg Int
, splitTrees :: SplitTrees' a
}
type SplitTrees' a = [(a, SplitTree' a)]
data SplitTag
= SplitCon QName
| SplitLit Literal
| SplitCatchall
deriving (Show, Eq, Ord)
instance Pretty SplitTag where
pretty (SplitCon c) = pretty c
pretty (SplitLit l) = pretty l
pretty SplitCatchall = underscore
instance PrettyTCM SplitTag where
prettyTCM (SplitCon c) = prettyTCM c
prettyTCM (SplitLit l) = prettyTCM l
prettyTCM SplitCatchall = return underscore
data SplitTreeLabel a = SplitTreeLabel
{ lblConstructorName :: Maybe a
, lblSplitArg :: Maybe (Arg Int)
, lblBindings :: Maybe Int
}
instance Pretty a => Pretty (SplitTreeLabel a) where
pretty = \case
SplitTreeLabel Nothing Nothing (Just n) -> text $ "done, " ++ show n ++ " bindings"
SplitTreeLabel Nothing (Just n) Nothing -> text $ "split at " ++ show n
SplitTreeLabel (Just q) Nothing (Just n) -> pretty q <+> text (" -> done, " ++ show n ++ " bindings")
SplitTreeLabel (Just q) (Just n) Nothing -> pretty q <+> text (" -> split at " ++ show n)
_ -> __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 Pretty a => Pretty (SplitTree' a) where
pretty = text . drawTree . fmap prettyShow . toTree