module Agda.TypeChecking.Positivity.Occurrence
( Occurrence(..)
, OccursWhere(..)
, Where(..)
, boundToEverySome
, productOfEdgesInBoundedWalk
) where
import Control.Applicative
import Control.DeepSeq
import Control.Monad
import Data.Either
import Data.Maybe
import Data.Typeable (Typeable)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Data.Sequence as DS
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.List
import Agda.Utils.Null
import Agda.Utils.SemiRing
#include "undefined.h"
import Agda.Utils.Impossible
data OccursWhere
= Unknown
| Known Range (DS.Seq Where)
deriving (Show, Eq, Ord)
data Where
= LeftOfArrow
| DefArg QName Nat
| UnderInf
| VarArg
| MetaArg
| ConArgType QName
| IndArgType QName
| InClause Nat
| Matched
| InDefOf QName
deriving (Show, Eq, Ord)
data Occurrence
= Mixed
| JustNeg
| JustPos
| StrictPos
| GuardPos
| Unused
deriving (Typeable, Show, Eq, Ord, Enum, Bounded)
instance NFData Occurrence where rnf x = seq x ()
instance KillRange Occurrence where
killRange = id
instance SemiRing Occurrence where
ozero = Unused
oone = StrictPos
oplus Mixed _ = Mixed
oplus _ Mixed = Mixed
oplus Unused o = o
oplus o Unused = o
oplus JustNeg JustNeg = JustNeg
oplus JustNeg o = Mixed
oplus o JustNeg = Mixed
oplus GuardPos o = o
oplus o GuardPos = o
oplus StrictPos o = o
oplus o StrictPos = o
oplus JustPos JustPos = JustPos
otimes Unused _ = Unused
otimes _ Unused = Unused
otimes Mixed _ = Mixed
otimes _ Mixed = Mixed
otimes JustNeg JustNeg = JustPos
otimes JustNeg _ = JustNeg
otimes _ JustNeg = JustNeg
otimes JustPos _ = JustPos
otimes _ JustPos = JustPos
otimes GuardPos _ = GuardPos
otimes _ GuardPos = GuardPos
otimes StrictPos StrictPos = StrictPos
instance StarSemiRing Occurrence where
ostar Mixed = Mixed
ostar JustNeg = Mixed
ostar JustPos = JustPos
ostar StrictPos = StrictPos
ostar GuardPos = StrictPos
ostar Unused = StrictPos
instance Null Occurrence where
empty = Unused
boundToEverySome ::
Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
boundToEverySome = Map.fromList
[ ( JustPos
, [((/= Unused), (`elem` [Mixed, JustNeg, JustPos]))]
)
, ( StrictPos
, [ ((/= Unused), (`elem` [Mixed, JustNeg, JustPos]))
, ((not . (`elem` [Unused, GuardPos])), const True)
]
)
, ( GuardPos
, [((/= Unused), const True)]
)
]
productOfEdgesInBoundedWalk ::
(SemiRing e, Ord n) =>
(e -> Occurrence) -> Graph n n e -> n -> n -> Occurrence -> Maybe e
productOfEdgesInBoundedWalk occ g u v bound =
case Map.lookup bound boundToEverySome of
Nothing -> __IMPOSSIBLE__
Just ess ->
case msum [ Graph.walkSatisfying (every . occ) (some . occ) g u v
| (every, some) <- ess
] of
Just es@(_ : _) -> Just (foldr1 otimes (map Graph.label es))
Just [] -> __IMPOSSIBLE__
Nothing -> Nothing