{-# LANGUAGE DeriveDataTypeable #-}
module Agda.TypeChecking.Coverage.SplitTree where
import Data.Tree
import Data.Data (Data)
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Utils.Pretty
import Agda.Utils.Null
import Agda.Utils.Impossible
type SplitTree = SplitTree' SplitTag
type SplitTrees = SplitTrees' SplitTag
data SplitTree' a
=
SplittingDone
{ splitBindings :: Int
}
|
SplitAt
{ splitArg :: Arg Int
, splitLazy :: LazySplit
, splitTrees :: SplitTrees' a
}
deriving (Data, Show)
data LazySplit = LazySplit | StrictSplit
deriving (Data, Show, Eq, Ord)
type SplitTrees' a = [(a, SplitTree' a)]
data SplitTag
= SplitCon QName
| SplitLit Literal
| SplitCatchall
deriving (Show, Eq, Ord, Data)
instance Pretty SplitTag where
pretty (SplitCon c) = pretty c
pretty (SplitLit l) = pretty l
pretty SplitCatchall = underscore
data SplitTreeLabel a = SplitTreeLabel
{ lblConstructorName :: Maybe a
, lblSplitArg :: Maybe (Arg Int)
, lblLazy :: LazySplit
, lblBindings :: Maybe Int
}
instance Pretty a => Pretty (SplitTreeLabel a) where
pretty = \case
SplitTreeLabel Nothing Nothing _ (Just n) -> text $ "done, " ++ prettyShow n ++ " bindings"
SplitTreeLabel Nothing (Just n) lz Nothing -> lzp lz <+> text ("split at " ++ prettyShow n)
SplitTreeLabel (Just q) Nothing _ (Just n) -> pretty q <+> text ("-> done, " ++ prettyShow n ++ " bindings")
SplitTreeLabel (Just q) (Just n) lz Nothing -> pretty q <+> text "->" <+> lzp lz <+> text ("split at " ++ prettyShow n)
_ -> __IMPOSSIBLE__
where lzp lz | lz == LazySplit = "lazy"
| otherwise = empty
toTree :: SplitTree' a -> Tree (SplitTreeLabel a)
toTree t = case t of
SplittingDone n -> Node (SplitTreeLabel Nothing Nothing StrictSplit (Just n)) []
SplitAt n lz ts -> Node (SplitTreeLabel Nothing (Just n) lz 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
instance KillRange SplitTag where
killRange = \case
SplitCon c -> killRange1 SplitCon c
SplitLit l -> killRange1 SplitLit l
SplitCatchall -> SplitCatchall
instance KillRange a => KillRange (SplitTree' a) where
killRange = \case
SplittingDone n -> SplittingDone n
SplitAt i lz ts -> killRange1 (SplitAt i lz) ts