{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
module Agda.TypeChecking.Coverage.SplitTree where
import Data.Tree
import Data.Data (Data, toConstr)
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Literal
import Agda.Syntax.Position
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
}
deriving (Data, Show)
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)
, 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) Nothing -> text $ "split at " ++ prettyShow n
SplitTreeLabel (Just q) Nothing (Just n) -> pretty q <+> text (" -> done, " ++ prettyShow n ++ " bindings")
SplitTreeLabel (Just q) (Just n) Nothing -> pretty q <+> text (" -> split at " ++ prettyShow 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
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 ts -> killRange1 (SplitAt i) ts