{-# LANGUAGE DeriveDataTypeable #-}
module Agda.TypeChecking.Positivity.Occurrence
( Occurrence(..)
, OccursWhere(..)
, Where(..)
, boundToEverySome
, productOfEdgesInBoundedWalk
) where
import Control.DeepSeq
import Control.Monad
import Data.Data (Data)
import Data.Foldable (toList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq)
import Agda.Syntax.Common
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Position
import Agda.Utils.Graph.AdjacencyMap.Unidirectional (Graph)
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.SemiRing
import Agda.Utils.Size
import Agda.Utils.Impossible
data OccursWhere
= OccursWhere Range (Seq Where) (Seq Where)
deriving (Int -> OccursWhere -> ShowS
[OccursWhere] -> ShowS
OccursWhere -> String
(Int -> OccursWhere -> ShowS)
-> (OccursWhere -> String)
-> ([OccursWhere] -> ShowS)
-> Show OccursWhere
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OccursWhere] -> ShowS
$cshowList :: [OccursWhere] -> ShowS
show :: OccursWhere -> String
$cshow :: OccursWhere -> String
showsPrec :: Int -> OccursWhere -> ShowS
$cshowsPrec :: Int -> OccursWhere -> ShowS
Show, OccursWhere -> OccursWhere -> Bool
(OccursWhere -> OccursWhere -> Bool)
-> (OccursWhere -> OccursWhere -> Bool) -> Eq OccursWhere
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OccursWhere -> OccursWhere -> Bool
$c/= :: OccursWhere -> OccursWhere -> Bool
== :: OccursWhere -> OccursWhere -> Bool
$c== :: OccursWhere -> OccursWhere -> Bool
Eq, Eq OccursWhere
Eq OccursWhere =>
(OccursWhere -> OccursWhere -> Ordering)
-> (OccursWhere -> OccursWhere -> Bool)
-> (OccursWhere -> OccursWhere -> Bool)
-> (OccursWhere -> OccursWhere -> Bool)
-> (OccursWhere -> OccursWhere -> Bool)
-> (OccursWhere -> OccursWhere -> OccursWhere)
-> (OccursWhere -> OccursWhere -> OccursWhere)
-> Ord OccursWhere
OccursWhere -> OccursWhere -> Bool
OccursWhere -> OccursWhere -> Ordering
OccursWhere -> OccursWhere -> OccursWhere
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
min :: OccursWhere -> OccursWhere -> OccursWhere
$cmin :: OccursWhere -> OccursWhere -> OccursWhere
max :: OccursWhere -> OccursWhere -> OccursWhere
$cmax :: OccursWhere -> OccursWhere -> OccursWhere
>= :: OccursWhere -> OccursWhere -> Bool
$c>= :: OccursWhere -> OccursWhere -> Bool
> :: OccursWhere -> OccursWhere -> Bool
$c> :: OccursWhere -> OccursWhere -> Bool
<= :: OccursWhere -> OccursWhere -> Bool
$c<= :: OccursWhere -> OccursWhere -> Bool
< :: OccursWhere -> OccursWhere -> Bool
$c< :: OccursWhere -> OccursWhere -> Bool
compare :: OccursWhere -> OccursWhere -> Ordering
$ccompare :: OccursWhere -> OccursWhere -> Ordering
$cp1Ord :: Eq OccursWhere
Ord, Typeable OccursWhere
DataType
Constr
Typeable OccursWhere =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OccursWhere -> c OccursWhere)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OccursWhere)
-> (OccursWhere -> Constr)
-> (OccursWhere -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OccursWhere))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c OccursWhere))
-> ((forall b. Data b => b -> b) -> OccursWhere -> OccursWhere)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r)
-> (forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> OccursWhere -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere)
-> Data OccursWhere
OccursWhere -> DataType
OccursWhere -> Constr
(forall b. Data b => b -> b) -> OccursWhere -> OccursWhere
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OccursWhere -> c OccursWhere
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OccursWhere
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> OccursWhere -> u
forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OccursWhere
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OccursWhere -> c OccursWhere
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OccursWhere)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c OccursWhere)
$cOccursWhere :: Constr
$tOccursWhere :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
gmapMp :: (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
gmapM :: (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
gmapQi :: Int -> (forall d. Data d => d -> u) -> OccursWhere -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> OccursWhere -> u
gmapQ :: (forall d. Data d => d -> u) -> OccursWhere -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
gmapT :: (forall b. Data b => b -> b) -> OccursWhere -> OccursWhere
$cgmapT :: (forall b. Data b => b -> b) -> OccursWhere -> OccursWhere
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c OccursWhere)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c OccursWhere)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c OccursWhere)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OccursWhere)
dataTypeOf :: OccursWhere -> DataType
$cdataTypeOf :: OccursWhere -> DataType
toConstr :: OccursWhere -> Constr
$ctoConstr :: OccursWhere -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OccursWhere
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OccursWhere
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OccursWhere -> c OccursWhere
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OccursWhere -> c OccursWhere
$cp1Data :: Typeable OccursWhere
Data)
data Where
= LeftOfArrow
| DefArg QName Nat
| UnderInf
| VarArg
| MetaArg
| ConArgType QName
| IndArgType QName
| InClause Nat
| Matched
| IsIndex
| InDefOf QName
deriving (Int -> Where -> ShowS
[Where] -> ShowS
Where -> String
(Int -> Where -> ShowS)
-> (Where -> String) -> ([Where] -> ShowS) -> Show Where
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Where] -> ShowS
$cshowList :: [Where] -> ShowS
show :: Where -> String
$cshow :: Where -> String
showsPrec :: Int -> Where -> ShowS
$cshowsPrec :: Int -> Where -> ShowS
Show, Where -> Where -> Bool
(Where -> Where -> Bool) -> (Where -> Where -> Bool) -> Eq Where
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Where -> Where -> Bool
$c/= :: Where -> Where -> Bool
== :: Where -> Where -> Bool
$c== :: Where -> Where -> Bool
Eq, Eq Where
Eq Where =>
(Where -> Where -> Ordering)
-> (Where -> Where -> Bool)
-> (Where -> Where -> Bool)
-> (Where -> Where -> Bool)
-> (Where -> Where -> Bool)
-> (Where -> Where -> Where)
-> (Where -> Where -> Where)
-> Ord Where
Where -> Where -> Bool
Where -> Where -> Ordering
Where -> Where -> Where
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
min :: Where -> Where -> Where
$cmin :: Where -> Where -> Where
max :: Where -> Where -> Where
$cmax :: Where -> Where -> Where
>= :: Where -> Where -> Bool
$c>= :: Where -> Where -> Bool
> :: Where -> Where -> Bool
$c> :: Where -> Where -> Bool
<= :: Where -> Where -> Bool
$c<= :: Where -> Where -> Bool
< :: Where -> Where -> Bool
$c< :: Where -> Where -> Bool
compare :: Where -> Where -> Ordering
$ccompare :: Where -> Where -> Ordering
$cp1Ord :: Eq Where
Ord, Typeable Where
DataType
Constr
Typeable Where =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Where -> c Where)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Where)
-> (Where -> Constr)
-> (Where -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Where))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where))
-> ((forall b. Data b => b -> b) -> Where -> Where)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r)
-> (forall u. (forall d. Data d => d -> u) -> Where -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Where -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Where -> m Where)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Where -> m Where)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Where -> m Where)
-> Data Where
Where -> DataType
Where -> Constr
(forall b. Data b => b -> b) -> Where -> Where
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Where -> c Where
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Where
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Where -> u
forall u. (forall d. Data d => d -> u) -> Where -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Where -> m Where
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Where -> m Where
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Where
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Where -> c Where
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Where)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where)
$cInDefOf :: Constr
$cIsIndex :: Constr
$cMatched :: Constr
$cInClause :: Constr
$cIndArgType :: Constr
$cConArgType :: Constr
$cMetaArg :: Constr
$cVarArg :: Constr
$cUnderInf :: Constr
$cDefArg :: Constr
$cLeftOfArrow :: Constr
$tWhere :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Where -> m Where
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Where -> m Where
gmapMp :: (forall d. Data d => d -> m d) -> Where -> m Where
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Where -> m Where
gmapM :: (forall d. Data d => d -> m d) -> Where -> m Where
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Where -> m Where
gmapQi :: Int -> (forall d. Data d => d -> u) -> Where -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Where -> u
gmapQ :: (forall d. Data d => d -> u) -> Where -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Where -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
gmapT :: (forall b. Data b => b -> b) -> Where -> Where
$cgmapT :: (forall b. Data b => b -> b) -> Where -> Where
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Where)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Where)
dataTypeOf :: Where -> DataType
$cdataTypeOf :: Where -> DataType
toConstr :: Where -> Constr
$ctoConstr :: Where -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Where
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Where
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Where -> c Where
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Where -> c Where
$cp1Data :: Typeable Where
Data)
data Occurrence
= Mixed
| JustNeg
| JustPos
| StrictPos
| GuardPos
| Unused
deriving (Typeable Occurrence
DataType
Constr
Typeable Occurrence =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Occurrence -> c Occurrence)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Occurrence)
-> (Occurrence -> Constr)
-> (Occurrence -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Occurrence))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Occurrence))
-> ((forall b. Data b => b -> b) -> Occurrence -> Occurrence)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r)
-> (forall u. (forall d. Data d => d -> u) -> Occurrence -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> Occurrence -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence)
-> Data Occurrence
Occurrence -> DataType
Occurrence -> Constr
(forall b. Data b => b -> b) -> Occurrence -> Occurrence
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Occurrence -> c Occurrence
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Occurrence
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Occurrence -> u
forall u. (forall d. Data d => d -> u) -> Occurrence -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Occurrence
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Occurrence -> c Occurrence
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Occurrence)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence)
$cUnused :: Constr
$cGuardPos :: Constr
$cStrictPos :: Constr
$cJustPos :: Constr
$cJustNeg :: Constr
$cMixed :: Constr
$tOccurrence :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
gmapMp :: (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
gmapM :: (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
gmapQi :: Int -> (forall d. Data d => d -> u) -> Occurrence -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Occurrence -> u
gmapQ :: (forall d. Data d => d -> u) -> Occurrence -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Occurrence -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
gmapT :: (forall b. Data b => b -> b) -> Occurrence -> Occurrence
$cgmapT :: (forall b. Data b => b -> b) -> Occurrence -> Occurrence
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Occurrence)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Occurrence)
dataTypeOf :: Occurrence -> DataType
$cdataTypeOf :: Occurrence -> DataType
toConstr :: Occurrence -> Constr
$ctoConstr :: Occurrence -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Occurrence
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Occurrence
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Occurrence -> c Occurrence
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Occurrence -> c Occurrence
$cp1Data :: Typeable Occurrence
Data, Int -> Occurrence -> ShowS
[Occurrence] -> ShowS
Occurrence -> String
(Int -> Occurrence -> ShowS)
-> (Occurrence -> String)
-> ([Occurrence] -> ShowS)
-> Show Occurrence
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Occurrence] -> ShowS
$cshowList :: [Occurrence] -> ShowS
show :: Occurrence -> String
$cshow :: Occurrence -> String
showsPrec :: Int -> Occurrence -> ShowS
$cshowsPrec :: Int -> Occurrence -> ShowS
Show, Occurrence -> Occurrence -> Bool
(Occurrence -> Occurrence -> Bool)
-> (Occurrence -> Occurrence -> Bool) -> Eq Occurrence
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Occurrence -> Occurrence -> Bool
$c/= :: Occurrence -> Occurrence -> Bool
== :: Occurrence -> Occurrence -> Bool
$c== :: Occurrence -> Occurrence -> Bool
Eq, Eq Occurrence
Eq Occurrence =>
(Occurrence -> Occurrence -> Ordering)
-> (Occurrence -> Occurrence -> Bool)
-> (Occurrence -> Occurrence -> Bool)
-> (Occurrence -> Occurrence -> Bool)
-> (Occurrence -> Occurrence -> Bool)
-> (Occurrence -> Occurrence -> Occurrence)
-> (Occurrence -> Occurrence -> Occurrence)
-> Ord Occurrence
Occurrence -> Occurrence -> Bool
Occurrence -> Occurrence -> Ordering
Occurrence -> Occurrence -> Occurrence
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
min :: Occurrence -> Occurrence -> Occurrence
$cmin :: Occurrence -> Occurrence -> Occurrence
max :: Occurrence -> Occurrence -> Occurrence
$cmax :: Occurrence -> Occurrence -> Occurrence
>= :: Occurrence -> Occurrence -> Bool
$c>= :: Occurrence -> Occurrence -> Bool
> :: Occurrence -> Occurrence -> Bool
$c> :: Occurrence -> Occurrence -> Bool
<= :: Occurrence -> Occurrence -> Bool
$c<= :: Occurrence -> Occurrence -> Bool
< :: Occurrence -> Occurrence -> Bool
$c< :: Occurrence -> Occurrence -> Bool
compare :: Occurrence -> Occurrence -> Ordering
$ccompare :: Occurrence -> Occurrence -> Ordering
$cp1Ord :: Eq Occurrence
Ord, Int -> Occurrence
Occurrence -> Int
Occurrence -> [Occurrence]
Occurrence -> Occurrence
Occurrence -> Occurrence -> [Occurrence]
Occurrence -> Occurrence -> Occurrence -> [Occurrence]
(Occurrence -> Occurrence)
-> (Occurrence -> Occurrence)
-> (Int -> Occurrence)
-> (Occurrence -> Int)
-> (Occurrence -> [Occurrence])
-> (Occurrence -> Occurrence -> [Occurrence])
-> (Occurrence -> Occurrence -> [Occurrence])
-> (Occurrence -> Occurrence -> Occurrence -> [Occurrence])
-> Enum Occurrence
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence]
$cenumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence]
enumFromTo :: Occurrence -> Occurrence -> [Occurrence]
$cenumFromTo :: Occurrence -> Occurrence -> [Occurrence]
enumFromThen :: Occurrence -> Occurrence -> [Occurrence]
$cenumFromThen :: Occurrence -> Occurrence -> [Occurrence]
enumFrom :: Occurrence -> [Occurrence]
$cenumFrom :: Occurrence -> [Occurrence]
fromEnum :: Occurrence -> Int
$cfromEnum :: Occurrence -> Int
toEnum :: Int -> Occurrence
$ctoEnum :: Int -> Occurrence
pred :: Occurrence -> Occurrence
$cpred :: Occurrence -> Occurrence
succ :: Occurrence -> Occurrence
$csucc :: Occurrence -> Occurrence
Enum, Occurrence
Occurrence -> Occurrence -> Bounded Occurrence
forall a. a -> a -> Bounded a
maxBound :: Occurrence
$cmaxBound :: Occurrence
minBound :: Occurrence
$cminBound :: Occurrence
Bounded)
instance Pretty Occurrence where
pretty :: Occurrence -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Occurrence -> String) -> Occurrence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
Unused -> "_"
Mixed -> "*"
JustNeg -> "-"
JustPos -> "+"
StrictPos -> "++"
GuardPos -> "g+"
instance Pretty Where where
pretty :: Where -> Doc
pretty = \case
LeftOfArrow -> "LeftOfArrow"
DefArg q :: QName
q i :: Int
i -> "DefArg" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
i
UnderInf -> "UnderInf"
VarArg -> "VarArg"
MetaArg -> "MetaArg"
ConArgType q :: QName
q -> "ConArgType" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q
IndArgType q :: QName
q -> "IndArgType" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q
InClause i :: Int
i -> "InClause" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
i
Matched -> "Matched"
IsIndex -> "IsIndex"
InDefOf q :: QName
q -> "InDefOf" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q
instance Pretty OccursWhere where
pretty :: OccursWhere -> Doc
pretty = \case
OccursWhere _r :: Range
_r ws1 :: Seq Where
ws1 ws2 :: Seq Where
ws2 ->
"OccursWhere _" Doc -> Doc -> Doc
<+> [Where] -> Doc
forall a. Pretty a => a -> Doc
pretty (Seq Where -> [Where]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Where
ws1) Doc -> Doc -> Doc
<+> [Where] -> Doc
forall a. Pretty a => a -> Doc
pretty (Seq Where -> [Where]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Where
ws2)
instance NFData Occurrence where rnf :: Occurrence -> ()
rnf x :: Occurrence
x = Occurrence -> () -> ()
forall a b. a -> b -> b
seq Occurrence
x ()
instance KillRange Occurrence where
killRange :: Occurrence -> Occurrence
killRange = Occurrence -> Occurrence
forall a. a -> a
id
instance SemiRing Occurrence where
ozero :: Occurrence
ozero = Occurrence
Unused
oone :: Occurrence
oone = Occurrence
StrictPos
oplus :: Occurrence -> Occurrence -> Occurrence
oplus Mixed _ = Occurrence
Mixed
oplus _ Mixed = Occurrence
Mixed
oplus Unused o :: Occurrence
o = Occurrence
o
oplus o :: Occurrence
o Unused = Occurrence
o
oplus JustNeg JustNeg = Occurrence
JustNeg
oplus JustNeg o :: Occurrence
o = Occurrence
Mixed
oplus o :: Occurrence
o JustNeg = Occurrence
Mixed
oplus GuardPos o :: Occurrence
o = Occurrence
o
oplus o :: Occurrence
o GuardPos = Occurrence
o
oplus StrictPos o :: Occurrence
o = Occurrence
o
oplus o :: Occurrence
o StrictPos = Occurrence
o
oplus JustPos JustPos = Occurrence
JustPos
otimes :: Occurrence -> Occurrence -> Occurrence
otimes Unused _ = Occurrence
Unused
otimes _ Unused = Occurrence
Unused
otimes Mixed _ = Occurrence
Mixed
otimes _ Mixed = Occurrence
Mixed
otimes JustNeg JustNeg = Occurrence
JustPos
otimes JustNeg _ = Occurrence
JustNeg
otimes _ JustNeg = Occurrence
JustNeg
otimes JustPos _ = Occurrence
JustPos
otimes _ JustPos = Occurrence
JustPos
otimes GuardPos _ = Occurrence
GuardPos
otimes _ GuardPos = Occurrence
GuardPos
otimes StrictPos StrictPos = Occurrence
StrictPos
instance StarSemiRing Occurrence where
ostar :: Occurrence -> Occurrence
ostar Mixed = Occurrence
Mixed
ostar JustNeg = Occurrence
Mixed
ostar JustPos = Occurrence
JustPos
ostar StrictPos = Occurrence
StrictPos
ostar GuardPos = Occurrence
StrictPos
ostar Unused = Occurrence
StrictPos
instance Null Occurrence where
empty :: Occurrence
empty = Occurrence
Unused
instance Sized OccursWhere where
size :: OccursWhere -> Int
size (OccursWhere _ cs :: Seq Where
cs os :: Seq Where
os) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Seq Where -> Int
forall a. Sized a => a -> Int
size Seq Where
cs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Seq Where -> Int
forall a. Sized a => a -> Int
size Seq Where
os
boundToEverySome ::
Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
boundToEverySome :: Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
boundToEverySome = [(Occurrence, [(Occurrence -> Bool, Occurrence -> Bool)])]
-> Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[ ( Occurrence
JustPos
, [((Occurrence -> Occurrence -> Bool
forall a. Eq a => a -> a -> Bool
/= Occurrence
Unused), (Occurrence -> [Occurrence] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Occurrence
Mixed, Occurrence
JustNeg, Occurrence
JustPos]))]
)
, ( Occurrence
StrictPos
, [ ((Occurrence -> Occurrence -> Bool
forall a. Eq a => a -> a -> Bool
/= Occurrence
Unused), (Occurrence -> [Occurrence] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Occurrence
Mixed, Occurrence
JustNeg, Occurrence
JustPos]))
, ((Bool -> Bool
not (Bool -> Bool) -> (Occurrence -> Bool) -> Occurrence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Occurrence -> [Occurrence] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Occurrence
Unused, Occurrence
GuardPos])), Bool -> Occurrence -> Bool
forall a b. a -> b -> a
const Bool
True)
]
)
, ( Occurrence
GuardPos
, [((Occurrence -> Occurrence -> Bool
forall a. Eq a => a -> a -> Bool
/= Occurrence
Unused), Bool -> Occurrence -> Bool
forall a b. a -> b -> a
const Bool
True)]
)
]
productOfEdgesInBoundedWalk ::
(SemiRing e, Ord n) =>
(e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e
productOfEdgesInBoundedWalk :: (e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e
productOfEdgesInBoundedWalk occ :: e -> Occurrence
occ g :: Graph n e
g u :: n
u v :: n
v bound :: Occurrence
bound =
case Occurrence
-> Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
-> Maybe [(Occurrence -> Bool, Occurrence -> Bool)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Occurrence
bound Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
boundToEverySome of
Nothing -> Maybe e
forall a. HasCallStack => a
__IMPOSSIBLE__
Just ess :: [(Occurrence -> Bool, Occurrence -> Bool)]
ess ->
case [Maybe [Edge n e]] -> Maybe [Edge n e]
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ (Edge n e -> Bool)
-> (Edge n e -> Bool) -> Graph n e -> n -> n -> Maybe [Edge n e]
forall n e.
Ord n =>
(Edge n e -> Bool)
-> (Edge n e -> Bool) -> Graph n e -> n -> n -> Maybe [Edge n e]
Graph.walkSatisfying
(Occurrence -> Bool
every (Occurrence -> Bool)
-> (Edge n e -> Occurrence) -> Edge n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Occurrence
occ (e -> Occurrence) -> (Edge n e -> e) -> Edge n e -> Occurrence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Edge n e -> e
forall n e. Edge n e -> e
Graph.label)
(Occurrence -> Bool
some (Occurrence -> Bool)
-> (Edge n e -> Occurrence) -> Edge n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Occurrence
occ (e -> Occurrence) -> (Edge n e -> e) -> Edge n e -> Occurrence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Edge n e -> e
forall n e. Edge n e -> e
Graph.label)
Graph n e
g n
u n
v
| (every :: Occurrence -> Bool
every, some :: Occurrence -> Bool
some) <- [(Occurrence -> Bool, Occurrence -> Bool)]
ess
] of
Just es :: [Edge n e]
es@(_ : _) -> e -> Maybe e
forall a. a -> Maybe a
Just ((e -> e -> e) -> [e] -> e
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 e -> e -> e
forall a. SemiRing a => a -> a -> a
otimes ((Edge n e -> e) -> [Edge n e] -> [e]
forall a b. (a -> b) -> [a] -> [b]
map Edge n e -> e
forall n e. Edge n e -> e
Graph.label [Edge n e]
es))
Just [] -> Maybe e
forall a. HasCallStack => a
__IMPOSSIBLE__
Nothing -> Maybe e
forall a. Maybe a
Nothing