{-# LANGUAGE CPP #-}
{-# 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.Either
import Data.Foldable (toList)
import Data.Maybe
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq)
import qualified Data.Sequence as 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.List
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.SemiRing
#include "undefined.h"
import Agda.Utils.Impossible
data OccursWhere
= Unknown
| Known Range (Seq Where)
deriving (Show, Eq, Ord, Data)
data Where
= LeftOfArrow
| DefArg QName Nat
| UnderInf
| VarArg
| MetaArg
| ConArgType QName
| IndArgType QName
| InClause Nat
| Matched
| InDefOf QName
deriving (Show, Eq, Ord, Data)
data Occurrence
= Mixed
| JustNeg
| JustPos
| StrictPos
| GuardPos
| Unused
deriving (Data, Show, Eq, Ord, Enum, Bounded)
instance Pretty Occurrence where
pretty = text . \case
Unused -> "_"
Mixed -> "*"
JustNeg -> "-"
JustPos -> "+"
StrictPos -> "++"
GuardPos -> "g+"
instance Pretty Where where
pretty = \case
LeftOfArrow -> text "LeftOfArrow"
DefArg q i -> text "DefArg" <+> pretty q <+> pretty i
UnderInf -> text "UnderInf"
VarArg -> text "VarArg"
MetaArg -> text "MetaArg"
ConArgType q -> text "ConArgType" <+> pretty q
IndArgType q -> text "IndArgType" <+> pretty q
InClause i -> text "InClause" <+> pretty i
Matched -> text "Matched"
InDefOf q -> text "InDefOf" <+> pretty q
instance Pretty OccursWhere where
pretty = \case
Unknown -> text "Unknown"
Known _r ws -> text "Known _" <+> pretty (toList ws)
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 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 . Graph.label)
(some . occ . Graph.label)
g u v
| (every, some) <- ess
] of
Just es@(_ : _) -> Just (foldr1 otimes (map Graph.label es))
Just [] -> __IMPOSSIBLE__
Nothing -> Nothing