{-# OPTIONS_GHC -Wall #-}
module Agda.TypeChecking.Coverage.SplitTree where
import Control.DeepSeq
import Data.Tree
import GHC.Generics (Generic)
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Common.Pretty
import Agda.Utils.Null
import Agda.Utils.Impossible
type SplitTree = SplitTree' SplitTag
type SplitTrees = SplitTrees' SplitTag
data SplitTree' a
=
SplittingDone
{ forall a. SplitTree' a -> Int
splitBindings :: Int
}
|
SplitAt
{ forall a. SplitTree' a -> Arg Int
splitArg :: Arg Int
, forall a. SplitTree' a -> LazySplit
splitLazy :: LazySplit
, forall a. SplitTree' a -> SplitTrees' a
splitTrees :: SplitTrees' a
}
deriving (Int -> SplitTree' a -> ShowS
[SplitTree' a] -> ShowS
SplitTree' a -> String
(Int -> SplitTree' a -> ShowS)
-> (SplitTree' a -> String)
-> ([SplitTree' a] -> ShowS)
-> Show (SplitTree' a)
forall a. Show a => Int -> SplitTree' a -> ShowS
forall a. Show a => [SplitTree' a] -> ShowS
forall a. Show a => SplitTree' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> SplitTree' a -> ShowS
showsPrec :: Int -> SplitTree' a -> ShowS
$cshow :: forall a. Show a => SplitTree' a -> String
show :: SplitTree' a -> String
$cshowList :: forall a. Show a => [SplitTree' a] -> ShowS
showList :: [SplitTree' a] -> ShowS
Show, (forall x. SplitTree' a -> Rep (SplitTree' a) x)
-> (forall x. Rep (SplitTree' a) x -> SplitTree' a)
-> Generic (SplitTree' a)
forall x. Rep (SplitTree' a) x -> SplitTree' a
forall x. SplitTree' a -> Rep (SplitTree' a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SplitTree' a) x -> SplitTree' a
forall a x. SplitTree' a -> Rep (SplitTree' a) x
$cfrom :: forall a x. SplitTree' a -> Rep (SplitTree' a) x
from :: forall x. SplitTree' a -> Rep (SplitTree' a) x
$cto :: forall a x. Rep (SplitTree' a) x -> SplitTree' a
to :: forall x. Rep (SplitTree' a) x -> SplitTree' a
Generic)
data LazySplit = LazySplit | StrictSplit
deriving (Int -> LazySplit -> ShowS
[LazySplit] -> ShowS
LazySplit -> String
(Int -> LazySplit -> ShowS)
-> (LazySplit -> String)
-> ([LazySplit] -> ShowS)
-> Show LazySplit
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LazySplit -> ShowS
showsPrec :: Int -> LazySplit -> ShowS
$cshow :: LazySplit -> String
show :: LazySplit -> String
$cshowList :: [LazySplit] -> ShowS
showList :: [LazySplit] -> ShowS
Show, LazySplit -> LazySplit -> Bool
(LazySplit -> LazySplit -> Bool)
-> (LazySplit -> LazySplit -> Bool) -> Eq LazySplit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LazySplit -> LazySplit -> Bool
== :: LazySplit -> LazySplit -> Bool
$c/= :: LazySplit -> LazySplit -> Bool
/= :: LazySplit -> LazySplit -> Bool
Eq, Eq LazySplit
Eq LazySplit =>
(LazySplit -> LazySplit -> Ordering)
-> (LazySplit -> LazySplit -> Bool)
-> (LazySplit -> LazySplit -> Bool)
-> (LazySplit -> LazySplit -> Bool)
-> (LazySplit -> LazySplit -> Bool)
-> (LazySplit -> LazySplit -> LazySplit)
-> (LazySplit -> LazySplit -> LazySplit)
-> Ord LazySplit
LazySplit -> LazySplit -> Bool
LazySplit -> LazySplit -> Ordering
LazySplit -> LazySplit -> LazySplit
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LazySplit -> LazySplit -> Ordering
compare :: LazySplit -> LazySplit -> Ordering
$c< :: LazySplit -> LazySplit -> Bool
< :: LazySplit -> LazySplit -> Bool
$c<= :: LazySplit -> LazySplit -> Bool
<= :: LazySplit -> LazySplit -> Bool
$c> :: LazySplit -> LazySplit -> Bool
> :: LazySplit -> LazySplit -> Bool
$c>= :: LazySplit -> LazySplit -> Bool
>= :: LazySplit -> LazySplit -> Bool
$cmax :: LazySplit -> LazySplit -> LazySplit
max :: LazySplit -> LazySplit -> LazySplit
$cmin :: LazySplit -> LazySplit -> LazySplit
min :: LazySplit -> LazySplit -> LazySplit
Ord, (forall x. LazySplit -> Rep LazySplit x)
-> (forall x. Rep LazySplit x -> LazySplit) -> Generic LazySplit
forall x. Rep LazySplit x -> LazySplit
forall x. LazySplit -> Rep LazySplit x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LazySplit -> Rep LazySplit x
from :: forall x. LazySplit -> Rep LazySplit x
$cto :: forall x. Rep LazySplit x -> LazySplit
to :: forall x. Rep LazySplit x -> LazySplit
Generic)
type SplitTrees' a = [(a, SplitTree' a)]
data SplitTag
= SplitCon QName
| SplitLit Literal
| SplitCatchall
deriving (Int -> SplitTag -> ShowS
[SplitTag] -> ShowS
SplitTag -> String
(Int -> SplitTag -> ShowS)
-> (SplitTag -> String) -> ([SplitTag] -> ShowS) -> Show SplitTag
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SplitTag -> ShowS
showsPrec :: Int -> SplitTag -> ShowS
$cshow :: SplitTag -> String
show :: SplitTag -> String
$cshowList :: [SplitTag] -> ShowS
showList :: [SplitTag] -> ShowS
Show, SplitTag -> SplitTag -> Bool
(SplitTag -> SplitTag -> Bool)
-> (SplitTag -> SplitTag -> Bool) -> Eq SplitTag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SplitTag -> SplitTag -> Bool
== :: SplitTag -> SplitTag -> Bool
$c/= :: SplitTag -> SplitTag -> Bool
/= :: SplitTag -> SplitTag -> Bool
Eq, Eq SplitTag
Eq SplitTag =>
(SplitTag -> SplitTag -> Ordering)
-> (SplitTag -> SplitTag -> Bool)
-> (SplitTag -> SplitTag -> Bool)
-> (SplitTag -> SplitTag -> Bool)
-> (SplitTag -> SplitTag -> Bool)
-> (SplitTag -> SplitTag -> SplitTag)
-> (SplitTag -> SplitTag -> SplitTag)
-> Ord SplitTag
SplitTag -> SplitTag -> Bool
SplitTag -> SplitTag -> Ordering
SplitTag -> SplitTag -> SplitTag
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SplitTag -> SplitTag -> Ordering
compare :: SplitTag -> SplitTag -> Ordering
$c< :: SplitTag -> SplitTag -> Bool
< :: SplitTag -> SplitTag -> Bool
$c<= :: SplitTag -> SplitTag -> Bool
<= :: SplitTag -> SplitTag -> Bool
$c> :: SplitTag -> SplitTag -> Bool
> :: SplitTag -> SplitTag -> Bool
$c>= :: SplitTag -> SplitTag -> Bool
>= :: SplitTag -> SplitTag -> Bool
$cmax :: SplitTag -> SplitTag -> SplitTag
max :: SplitTag -> SplitTag -> SplitTag
$cmin :: SplitTag -> SplitTag -> SplitTag
min :: SplitTag -> SplitTag -> SplitTag
Ord, (forall x. SplitTag -> Rep SplitTag x)
-> (forall x. Rep SplitTag x -> SplitTag) -> Generic SplitTag
forall x. Rep SplitTag x -> SplitTag
forall x. SplitTag -> Rep SplitTag x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SplitTag -> Rep SplitTag x
from :: forall x. SplitTag -> Rep SplitTag x
$cto :: forall x. Rep SplitTag x -> SplitTag
to :: forall x. Rep SplitTag x -> SplitTag
Generic)
instance Pretty SplitTag where
pretty :: SplitTag -> Doc
pretty (SplitCon QName
c) = QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
c
pretty (SplitLit Literal
l) = Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
pretty SplitTag
SplitCatchall = Doc
forall a. Underscore a => a
underscore
data SplitTreeLabel a = SplitTreeLabel
{ forall a. SplitTreeLabel a -> Maybe a
lblConstructorName :: Maybe a
, forall a. SplitTreeLabel a -> Maybe (Arg Int)
lblSplitArg :: Maybe (Arg Int)
, forall a. SplitTreeLabel a -> LazySplit
lblLazy :: LazySplit
, forall a. SplitTreeLabel a -> Maybe Int
lblBindings :: Maybe Int
}
instance Pretty a => Pretty (SplitTreeLabel a) where
pretty :: SplitTreeLabel a -> Doc
pretty = \case
SplitTreeLabel Maybe a
Nothing Maybe (Arg Int)
Nothing LazySplit
_ (Just Int
n) -> String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"done, " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Pretty a => a -> String
prettyShow Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bindings"
SplitTreeLabel Maybe a
Nothing (Just Arg Int
n) LazySplit
lz Maybe Int
Nothing -> LazySplit -> Doc
forall {a}. (IsString a, Null a) => LazySplit -> a
lzp LazySplit
lz Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc
forall a. String -> Doc a
text (String
"split at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Arg Int -> String
forall a. Pretty a => a -> String
prettyShow Arg Int
n)
SplitTreeLabel (Just a
q) Maybe (Arg Int)
Nothing LazySplit
_ (Just Int
n) -> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
q Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc
forall a. String -> Doc a
text (String
"-> done, " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Pretty a => a -> String
prettyShow Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bindings")
SplitTreeLabel (Just a
q) (Just Arg Int
n) LazySplit
lz Maybe Int
Nothing -> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
q Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc
forall a. String -> Doc a
text String
"->" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> LazySplit -> Doc
forall {a}. (IsString a, Null a) => LazySplit -> a
lzp LazySplit
lz Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc
forall a. String -> Doc a
text (String
"split at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Arg Int -> String
forall a. Pretty a => a -> String
prettyShow Arg Int
n)
SplitTreeLabel a
_ -> Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
where lzp :: LazySplit -> a
lzp LazySplit
lz | LazySplit
lz LazySplit -> LazySplit -> Bool
forall a. Eq a => a -> a -> Bool
== LazySplit
LazySplit = a
"lazy"
| Bool
otherwise = a
forall a. Null a => a
empty
toTree :: SplitTree' a -> Tree (SplitTreeLabel a)
toTree :: forall a. SplitTree' a -> Tree (SplitTreeLabel a)
toTree = \case
SplittingDone Int
n -> SplitTreeLabel a
-> [Tree (SplitTreeLabel a)] -> Tree (SplitTreeLabel a)
forall a. a -> [Tree a] -> Tree a
Node (Maybe a
-> Maybe (Arg Int) -> LazySplit -> Maybe Int -> SplitTreeLabel a
forall a.
Maybe a
-> Maybe (Arg Int) -> LazySplit -> Maybe Int -> SplitTreeLabel a
SplitTreeLabel Maybe a
forall a. Maybe a
Nothing Maybe (Arg Int)
forall a. Maybe a
Nothing LazySplit
StrictSplit (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n)) []
SplitAt Arg Int
n LazySplit
lz SplitTrees' a
ts -> SplitTreeLabel a
-> [Tree (SplitTreeLabel a)] -> Tree (SplitTreeLabel a)
forall a. a -> [Tree a] -> Tree a
Node (Maybe a
-> Maybe (Arg Int) -> LazySplit -> Maybe Int -> SplitTreeLabel a
forall a.
Maybe a
-> Maybe (Arg Int) -> LazySplit -> Maybe Int -> SplitTreeLabel a
SplitTreeLabel Maybe a
forall a. Maybe a
Nothing (Arg Int -> Maybe (Arg Int)
forall a. a -> Maybe a
Just Arg Int
n) LazySplit
lz Maybe Int
forall a. Maybe a
Nothing) ([Tree (SplitTreeLabel a)] -> Tree (SplitTreeLabel a))
-> [Tree (SplitTreeLabel a)] -> Tree (SplitTreeLabel a)
forall a b. (a -> b) -> a -> b
$ SplitTrees' a -> [Tree (SplitTreeLabel a)]
forall a. SplitTrees' a -> Forest (SplitTreeLabel a)
toTrees SplitTrees' a
ts
toTrees :: SplitTrees' a -> Forest (SplitTreeLabel a)
toTrees :: forall a. SplitTrees' a -> Forest (SplitTreeLabel a)
toTrees = ((a, SplitTree' a) -> Tree (SplitTreeLabel a))
-> [(a, SplitTree' a)] -> [Tree (SplitTreeLabel a)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a
c,SplitTree' a
t) -> a -> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
forall a. a -> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
setCons a
c (Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a))
-> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
forall a b. (a -> b) -> a -> b
$ SplitTree' a -> Tree (SplitTreeLabel a)
forall a. SplitTree' a -> Tree (SplitTreeLabel a)
toTree SplitTree' a
t)
where
setCons :: a -> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
setCons :: forall a. a -> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
setCons a
c (Node SplitTreeLabel a
l [Tree (SplitTreeLabel a)]
ts) = SplitTreeLabel a
-> [Tree (SplitTreeLabel a)] -> Tree (SplitTreeLabel a)
forall a. a -> [Tree a] -> Tree a
Node (SplitTreeLabel a
l { lblConstructorName = Just c }) [Tree (SplitTreeLabel a)]
ts
instance Pretty a => Pretty (SplitTree' a) where
pretty :: SplitTree' a -> Doc
pretty = String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> (SplitTree' a -> String) -> SplitTree' a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tree String -> String
drawTree (Tree String -> String)
-> (SplitTree' a -> Tree String) -> SplitTree' a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitTreeLabel a -> String)
-> Tree (SplitTreeLabel a) -> Tree String
forall a b. (a -> b) -> Tree a -> Tree b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SplitTreeLabel a -> String
forall a. Pretty a => a -> String
prettyShow (Tree (SplitTreeLabel a) -> Tree String)
-> (SplitTree' a -> Tree (SplitTreeLabel a))
-> SplitTree' a
-> Tree String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitTree' a -> Tree (SplitTreeLabel a)
forall a. SplitTree' a -> Tree (SplitTreeLabel a)
toTree
instance KillRange SplitTag where
killRange :: SplitTag -> SplitTag
killRange = \case
SplitCon QName
c -> (QName -> SplitTag) -> QName -> SplitTag
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> SplitTag
SplitCon QName
c
SplitLit Literal
l -> (Literal -> SplitTag) -> Literal -> SplitTag
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Literal -> SplitTag
SplitLit Literal
l
SplitTag
SplitCatchall -> SplitTag
SplitCatchall
instance KillRange a => KillRange (SplitTree' a) where
killRange :: KillRangeT (SplitTree' a)
killRange = \case
SplittingDone Int
n -> Int -> SplitTree' a
forall a. Int -> SplitTree' a
SplittingDone Int
n
SplitAt Arg Int
i LazySplit
lz SplitTrees' a
ts -> (SplitTrees' a -> SplitTree' a) -> SplitTrees' a -> SplitTree' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
i LazySplit
lz) SplitTrees' a
ts
instance NFData a => NFData (SplitTree' a)
instance NFData LazySplit
instance NFData SplitTag