{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.Positivity where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ( (<>), null )
#else
import Prelude hiding ( null )
#endif
import Control.Applicative hiding (empty)
import Control.DeepSeq
import Control.Monad.Reader
import Control.Monad.State (get)
import Data.Either
import qualified Data.Foldable as Fold
import Data.Function
import Data.Graph (SCC(..), flattenSCC)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid (mconcat)
import qualified Data.Sequence as DS
import Data.Set (Set)
import qualified Data.Set as Set
import Debug.Trace
import Agda.Syntax.Common
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Position (fuseRange, Range, HasRange(..), noRange)
import Agda.TypeChecking.Datatypes ( isDataOrRecordType )
import Agda.TypeChecking.Functions
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (primInf, CoinductionKit(..), coinductionKit)
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
import Agda.Utils.Function (applyUnless)
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.Permutation as Perm
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Pretty (Pretty, prettyShow)
import Agda.Utils.SemiRing
import Agda.Utils.Singleton
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
type Graph n e = Graph.Graph n e
checkStrictlyPositive :: Info.MutualInfo -> Set QName -> TCM ()
checkStrictlyPositive mi qset = disableDestructiveUpdate $ do
let qs = Set.toList qset
reportSDoc "tc.pos.tick" 100 $ text "positivity of" <+> prettyTCM qs
g <- buildOccurrenceGraph qset
let (gstar, sccs) =
Graph.gaussJordanFloydWarshallMcNaughtonYamada $ fmap occ g
reportSDoc "tc.pos.tick" 100 $ text "constructed graph"
reportSLn "tc.pos.graph" 5 $ "Positivity graph: N=" ++ show (size $ Graph.nodes g) ++
" E=" ++ show (length $ Graph.edges g)
reportSDoc "tc.pos.graph" 10 $ vcat
[ text "positivity graph for" <+> (fsep $ map prettyTCM qs)
, nest 2 $ prettyTCM g
]
reportSLn "tc.pos.graph" 5 $
"Positivity graph (completed): E=" ++ show (length $ Graph.edges gstar)
reportSDoc "tc.pos.graph" 50 $ vcat
[ text "transitive closure of positivity graph for" <+>
prettyTCM qs
, nest 2 $ prettyTCM gstar
]
setArgOccs qset qs gstar
reportSDoc "tc.pos.tick" 100 $ text "set args"
reportSDoc "tc.pos.graph.sccs" 10 $ do
let (triv, others) = partitionEithers $ for sccs $ \case
AcyclicSCC v -> Left v
CyclicSCC vs -> Right vs
sep [ text $ show (length triv) ++ " trivial sccs"
, text $ show (length others) ++ " non-trivial sccs with lengths " ++
show (map length others)
]
reportSLn "tc.pos.graph.sccs" 15 $
" sccs = " ++ prettyShow [ scc | CyclicSCC scc <- sccs ]
forM_ sccs $ \case
AcyclicSCC (DefNode q) -> whenM (isNothing <$> getMutual q) $ do
reportSLn "tc.pos.mutual" 10 $ "setting " ++ prettyShow q ++ " to non-recursive"
unless (Set.member q qset) __IMPOSSIBLE__
setMutual q []
AcyclicSCC (ArgNode{}) -> return ()
CyclicSCC scc -> setMut [ q | DefNode q <- scc ]
mapM_ (checkPos g gstar) qs
reportSDoc "tc.pos.tick" 100 $ text "checked positivity"
where
checkPos :: Graph Node Edge ->
Graph Node Occurrence ->
QName -> TCM ()
checkPos g gstar q = inConcreteOrAbstractMode q $ \ _def -> do
whenJustM (isDatatype q) $ \ dr -> do
reportSDoc "tc.pos.check" 10 $ text "Checking positivity of" <+> prettyTCM q
let loop :: Maybe Occurrence
loop = Graph.lookup (DefNode q) (DefNode q) gstar
reason bound =
case productOfEdgesInBoundedWalk
occ g (DefNode q) (DefNode q) bound of
Just (Edge _ how) -> how
Nothing -> __IMPOSSIBLE__
how :: String -> Occurrence -> TCM Doc
how msg bound = fsep $
[prettyTCM q] ++ pwords "is" ++
pwords (msg ++ ", because it occurs") ++
[prettyTCM (reason bound)]
when (Info.mutualPositivityCheck mi) $
whenM positivityCheckEnabled $
case loop of
Just o | o <= JustPos ->
warning $ NotStrictlyPositive q (reason JustPos)
_ -> return ()
when (dr == IsRecord) $
case loop of
Just o | o <= StrictPos -> do
reportSDoc "tc.pos.record" 5 $ how "not guarded" StrictPos
unguardedRecord q
checkInduction q
Just o | o <= GuardPos -> do
reportSDoc "tc.pos.record" 5 $ how "recursive" GuardPos
recursiveRecord q
checkInduction q
Nothing -> do
reportSDoc "tc.pos.record" 10 $
text "record type " <+> prettyTCM q <+>
text "is not recursive"
nonRecursiveRecord q
_ -> return ()
checkInduction :: QName -> TCM ()
checkInduction q =
when (Info.mutualPositivityCheck mi) $
whenM positivityCheckEnabled $ do
unlessM (isJust . recInduction . theDef <$> getConstInfo q) $
setCurrentRange (nameBindingSite $ qnameName q) $
typeError . GenericDocError =<<
text "Recursive record" <+> prettyTCM q <+>
text "needs to be declared as either inductive or coinductive"
occ (Edge o _) = o
isDatatype :: QName -> TCM (Maybe DataOrRecord)
isDatatype q = do
def <- theDef <$> getConstInfo q
return $ case def of
Datatype{dataClause = Nothing} -> Just IsData
Record {recClause = Nothing} -> Just IsRecord
_ -> Nothing
setMut :: [QName] -> TCM ()
setMut [] = return ()
setMut qs = forM_ qs $ \ q -> do
reportSLn "tc.pos.mutual" 10 $ "setting " ++ prettyShow q ++ " to (mutually) recursive"
setMutual q qs
setArgOccs :: Set QName -> [QName] -> Graph Node Occurrence -> TCM ()
setArgOccs qset qs g = do
forM_ qs $ \ q -> inConcreteOrAbstractMode q $ \ def -> do
reportSDoc "tc.pos.args" 10 $ text "checking args of" <+> prettyTCM q
n <- getDefArity def
let findOcc i = fromMaybe Unused $ Graph.lookup (ArgNode q i) (DefNode q) g
args =
map findOcc [0 .. n-1]
reportSDoc "tc.pos.args" 10 $ sep
[ text "args of" <+> prettyTCM q <+> text "="
, nest 2 $ prettyList $ map prettyTCM args
]
setArgOccurrences q $!! args
getDefArity :: Definition -> TCM Int
getDefArity def = do
let dropped = case theDef def of
defn@Function{} -> projectionArgs defn
_ -> 0
subtract dropped . arity <$> instantiateFull (defType def)
(>*<) :: OccursWhere -> OccursWhere -> OccursWhere
Unknown >*< _ = Unknown
Known _ _ >*< Unknown = Unknown
Known r1 os1 >*< Known r2 os2 = Known (fuseRange r1 r2) (os1 DS.>< os2)
instance PrettyTCM OccursWhere where
prettyTCM o = prettyOs $ map maxOneLeftOfArrow $ uniq $ splitOnDef o
where
nth 0 = pwords "first"
nth 1 = pwords "second"
nth 2 = pwords "third"
nth n = pwords $ show (n + 1) ++ "th"
uniq = map head . List.group
prettyOs [] = __IMPOSSIBLE__
prettyOs [o] = prettyO o <> text "."
prettyOs (o:os) = prettyO o <> text ", which occurs" $$ prettyOs os
prettyO Unknown = empty
prettyO (Known _ ws) =
Fold.foldrM (\w d -> return d $$ fsep (prettyW w)) empty ws
prettyW w = case w of
LeftOfArrow -> pwords "to the left of an arrow"
DefArg q i -> pwords "in the" ++ nth i ++ pwords "argument to" ++
[prettyTCM q]
UnderInf -> pwords "under" ++
[do
Def inf _ <- primInf
prettyTCM inf]
VarArg -> pwords "in an argument to a bound variable"
MetaArg -> pwords "in an argument to a metavariable"
ConArgType c -> pwords "in the type of the constructor" ++ [prettyTCM c]
IndArgType c -> pwords "in an index of the target type of the constructor" ++ [prettyTCM c]
InClause i -> pwords "in the" ++ nth i ++ pwords "clause"
Matched -> pwords "as matched against"
InDefOf d -> pwords "in the definition of" ++ [prettyTCM d]
maxOneLeftOfArrow Unknown = Unknown
maxOneLeftOfArrow (Known r ws) = Known r $
noArrows
DS.><
case DS.viewl startsWithArrow of
DS.EmptyL -> DS.empty
w DS.:< ws -> w DS.<| DS.filter (not . isArrow) ws
where
(noArrows, startsWithArrow) = DS.breakl isArrow ws
isArrow LeftOfArrow{} = True
isArrow _ = False
splitOnDef Unknown = [Unknown]
splitOnDef (Known r ws) = split ws DS.empty
where
split ws acc = case DS.viewl ws of
w@InDefOf{} DS.:< ws -> let rest = split ws (DS.singleton w) in
if DS.null acc
then rest
else Known r acc : rest
w DS.:< ws -> split ws (acc DS.|> w)
DS.EmptyL -> [Known r acc]
instance Sized OccursWhere where
size Unknown = 1
size (Known _ ws) = 1 + size ws
data Item = AnArg Nat
| ADef QName
deriving (Eq, Ord, Show)
instance HasRange Item where
getRange (AnArg _) = noRange
getRange (ADef qn) = getRange qn
type Occurrences = Map Item [OccursWhere]
data OccurrencesBuilder
= Concat [OccurrencesBuilder]
| OccursAs Where OccurrencesBuilder
| OccursHere Item
| OnlyVarsUpTo Nat OccurrencesBuilder
data OccurrencesBuilder'
= Concat' [OccurrencesBuilder']
| OccursAs' Where OccurrencesBuilder'
| OccursHere' Item OccursWhere
emptyOB :: OccurrencesBuilder
emptyOB = Concat []
(>+<) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
occs1 >+< occs2 = Concat [occs1, occs2]
preprocess :: OccurrencesBuilder -> OccurrencesBuilder'
preprocess ob = case pp Nothing DS.empty ob of
Nothing -> Concat' []
Just ob -> ob
where
pp :: Maybe Nat
-> DS.Seq Where
-> OccurrencesBuilder
-> Maybe OccurrencesBuilder'
pp !m ws (Concat obs) = case catMaybes $ map (pp m ws) obs of
[] -> Nothing
obs -> return (Concat' obs)
pp m ws (OccursAs w ob) = OccursAs' w <$> pp m (ws DS.|> w) ob
pp m ws (OnlyVarsUpTo n ob) = pp (Just $! maybe n (min n) m) ws ob
pp m ws (OccursHere i) = do guard keep
return (OccursHere' i (Known (getRange i) ws))
where
keep = case (m, i) of
(Nothing, _) -> True
(_, ADef _) -> True
(Just m, AnArg i) -> i < m
data OccursWheres
= OccursWheres :++ OccursWheres
| Occurs OccursWhere
flatten :: OccurrencesBuilder -> Occurrences
flatten =
fmap (flip flatten'' []) .
Map.fromListWith (:++) .
flip flatten' [] .
preprocess
where
flatten' :: OccurrencesBuilder'
-> [(Item, OccursWheres)] -> [(Item, OccursWheres)]
flatten' (Concat' obs) = foldr (\occs f -> flatten' occs . f) id obs
flatten' (OccursAs' _ ob) = flatten' ob
flatten' (OccursHere' i o) = ((i, Occurs o) :)
flatten'' (os1 :++ os2) = flatten'' os1 . flatten'' os2
flatten'' (Occurs o) = (o :)
data OccEnv = OccEnv
{ vars :: [Maybe Item]
, inf :: Maybe QName
}
type OccM = Reader OccEnv
withExtendedOccEnv :: Maybe Item -> OccM a -> OccM a
withExtendedOccEnv i = withExtendedOccEnv' [i]
withExtendedOccEnv' :: [Maybe Item] -> OccM a -> OccM a
withExtendedOccEnv' is = local $ \ e -> e { vars = is ++ vars e }
getOccurrences
:: (Show a, PrettyTCM a, ComputeOccurrences a)
=> [Maybe Item] -> a -> TCM OccurrencesBuilder
getOccurrences vars a = do
reportSDoc "tc.pos.occ" 70 $ text "computing occurrences in " <+> text (show a)
reportSDoc "tc.pos.occ" 20 $ text "computing occurrences in " <+> prettyTCM a
kit <- coinductionKit
return $ runReader (occurrences a) $ OccEnv vars $ fmap nameOfInf kit
class ComputeOccurrences a where
occurrences :: a -> OccM OccurrencesBuilder
instance ComputeOccurrences Clause where
occurrences cl = do
let ps = namedClausePats cl
items = IntMap.elems $ patItems ps
(Concat (mapMaybe matching (zip [0..] ps)) >+<) <$>
withExtendedOccEnv' items (occurrences $ clauseBody cl)
where
matching (i, p)
| properlyMatching (namedThing $ unArg p) =
Just $ OccursAs Matched $ OccursHere $ AnArg i
| otherwise = Nothing
patItems ps = mconcat $ zipWith patItem [0..] ps
patItem :: Int -> NamedArg DeBruijnPattern -> IntMap (Maybe Item)
patItem i p = Fold.foldMap makeEntry ixs
where
ixs = map dbPatVarIndex $ lefts $ map unArg $ patternVars $ namedThing <$> p
makeEntry x = singleton (x, Just $ AnArg i)
instance ComputeOccurrences Term where
occurrences v = case unSpine v of
Var i args -> do
vars <- asks vars
occs <- occurrences args
let mi | i < length vars = vars !! i
| otherwise = flip trace __IMPOSSIBLE__ $
"impossible: occurrence of de Bruijn index " ++ show i ++
" in vars " ++ show vars ++ " is unbound"
return $ maybe emptyOB OccursHere mi >+< OccursAs VarArg occs
Def d args -> do
inf <- asks inf
let occsAs = if Just d /= inf then OccursAs . DefArg d else \ n ->
if n == 1 then OccursAs UnderInf else OccursAs (DefArg d n)
occs <- mapM occurrences args
return $ OccursHere (ADef d) >+< Concat (zipWith occsAs [0..] occs)
Con _ _ args -> occurrences args
MetaV _ args -> OccursAs MetaArg <$> occurrences args
Pi a b -> do
oa <- occurrences a
ob <- occurrences b
return $ OccursAs LeftOfArrow oa >+< ob
Lam _ b -> occurrences b
Level l -> occurrences l
Lit{} -> return emptyOB
Sort{} -> return emptyOB
DontCare _ -> return emptyOB
instance ComputeOccurrences Level where
occurrences (Max as) = occurrences as
instance ComputeOccurrences PlusLevel where
occurrences ClosedLevel{} = return emptyOB
occurrences (Plus _ l) = occurrences l
instance ComputeOccurrences LevelAtom where
occurrences l = case l of
MetaLevel x es -> occurrences $ MetaV x es
BlockedLevel _ v -> occurrences v
NeutralLevel _ v -> occurrences v
UnreducedLevel v -> occurrences v
instance ComputeOccurrences Type where
occurrences (El _ v) = occurrences v
instance ComputeOccurrences a => ComputeOccurrences (Tele a) where
occurrences EmptyTel = return emptyOB
occurrences (ExtendTel a b) = occurrences (a, b)
instance ComputeOccurrences a => ComputeOccurrences (Abs a) where
occurrences (Abs _ b) = withExtendedOccEnv Nothing $ occurrences b
occurrences (NoAbs _ b) = occurrences b
instance ComputeOccurrences a => ComputeOccurrences (Elim' a) where
occurrences Proj{} = __IMPOSSIBLE__
occurrences (Apply a) = occurrences a
instance ComputeOccurrences a => ComputeOccurrences (Arg a) where
occurrences = occurrences . unArg
instance ComputeOccurrences a => ComputeOccurrences (Dom a) where
occurrences = occurrences . unDom
instance ComputeOccurrences a => ComputeOccurrences [a] where
occurrences vs = Concat <$> mapM occurrences vs
instance ComputeOccurrences a => ComputeOccurrences (Maybe a) where
occurrences (Just v) = occurrences v
occurrences Nothing = return emptyOB
instance (ComputeOccurrences a, ComputeOccurrences b) => ComputeOccurrences (a, b) where
occurrences (x, y) = do
ox <- occurrences x
oy <- occurrences y
return $ ox >+< oy
computeOccurrences :: QName -> TCM Occurrences
computeOccurrences q = flatten <$> computeOccurrences' q
computeOccurrences' :: QName -> TCM OccurrencesBuilder
computeOccurrences' q = inConcreteOrAbstractMode q $ \ def -> do
reportSDoc "tc.pos" 25 $ do
let a = defAbstract def
m <- asks envAbstractMode
cur <- asks envCurrentModule
text "computeOccurrences" <+> prettyTCM q <+> text (show a) <+> text (show m)
<+> prettyTCM cur
OccursAs (InDefOf q) <$> case theDef def of
Function{funClauses = cs} -> do
cs <- mapM etaExpandClause =<< instantiateFull cs
Concat . zipWith (OccursAs . InClause) [0..] <$>
mapM (getOccurrences []) cs
Datatype{dataClause = Just c} -> getOccurrences [] =<< instantiateFull c
Datatype{dataPars = np0, dataCons = cs} -> do
TelV tel t <- telView $ defType def
sizeIndex <- caseMaybe (headMaybe $ drop np0 $ telToList tel) (return 0) $ \ dom -> do
caseMaybeM (isSizeType dom) (return 0) $ \ _ -> return 1
let np = np0 + sizeIndex
let xs = [np .. size tel - 1]
ioccs = Concat $ map (OccursHere . AnArg) [np0 .. np - 1]
++ map (OccursAs Matched . OccursHere . AnArg) xs
let conOcc c = do
a <- defType <$> getConstInfo c
TelV tel t <- telView' <$> normalise a
let indices = case unEl t of
Def _ vs -> drop np vs
_ -> __IMPOSSIBLE__
let tel' = telFromList $ drop np $ telToList tel
vars np = map (Just . AnArg) $ downFrom np
(>+<) <$> (OccursAs (ConArgType c) <$> getOccurrences (vars np) tel')
<*> (OccursAs (IndArgType c) . OnlyVarsUpTo np <$> getOccurrences (vars $ size tel) indices)
(>+<) ioccs <$> (Concat <$> mapM conOcc cs)
Record{recClause = Just c} -> getOccurrences [] =<< instantiateFull c
Record{recPars = np, recTel = tel} -> do
let tel' = telFromList $ drop np $ telToList tel
vars = map (Just . AnArg) $ downFrom np
getOccurrences vars =<< normalise tel'
Constructor{} -> return emptyOB
Axiom{} -> return emptyOB
Primitive{} -> return emptyOB
AbstractDefn{}-> __IMPOSSIBLE__
data Node = DefNode !QName
| ArgNode !QName !Nat
deriving (Eq, Ord)
instance Pretty Node where
pretty = \case
DefNode q -> P.pretty q
ArgNode q i -> P.pretty q P.<> P.text ("." ++ show i)
instance PrettyTCM Node where
prettyTCM = return . P.pretty
instance PrettyTCM n => PrettyTCM (WithNode n Edge) where
prettyTCM (WithNode n (Edge o w)) = vcat
[ prettyTCM o <+> prettyTCM n
, nest 2 $ return $ P.pretty w
]
data Edge = Edge !Occurrence OccursWhere
deriving (Eq, Ord, Show)
instance Null Edge where
null (Edge o _) = null o
empty = Edge empty Unknown
instance SemiRing Edge where
ozero = Edge ozero Unknown
oone = Edge oone Unknown
oplus _ e@(Edge Mixed _) = e
oplus e@(Edge Mixed _) _ = e
oplus (Edge Unused _) e = e
oplus e (Edge Unused _) = e
oplus (Edge JustNeg _) e@(Edge JustNeg _) = e
oplus _ e@(Edge JustNeg w) = Edge Mixed w
oplus e@(Edge JustNeg w) _ = Edge Mixed w
oplus _ e@(Edge JustPos _) = e
oplus e@(Edge JustPos _) _ = e
oplus _ e@(Edge StrictPos _) = e
oplus e@(Edge StrictPos _) _ = e
oplus (Edge GuardPos _) e@(Edge GuardPos _) = e
otimes (Edge o1 w1) (Edge o2 w2) = Edge (otimes o1 o2) (w1 >*< w2)
instance StarSemiRing Edge where
ostar (Edge o w) = Edge (ostar o) w
buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge)
buildOccurrenceGraph qs =
Graph.fromEdgesWith oplus . concat <$>
mapM defGraph (Set.toList qs)
where
defGraph :: QName -> TCM [Graph.Edge Node Edge]
defGraph q = inConcreteOrAbstractMode q $ \ _def -> do
occs <- computeOccurrences' q
reportSDoc "tc.pos.occs" 40 $
(text "Occurrences in" <+> prettyTCM q <> text ":")
$+$
(nest 2 $ vcat $
map (\(i, (n, s)) ->
text (show i) <> text ":" <+> text (show n) <+>
text "occurrences, of total size" <+>
text (show s)) $
List.sortBy (compare `on` fst . snd) $
map (\(i, os) -> (i, (length os, sum $ map size os))) $
Map.toList (flatten occs))
reportSDoc "tc.pos.occs" 50 $
(nest 2 $ vcat $
map (\(i, os) ->
(text (show i) <> text ":")
$+$
(nest 2 $ vcat $ map (return . P.pretty) os))
(Map.toList (flatten occs)))
es <- computeEdges qs q occs
reportSDoc "tc.pos.occs.edges" 60 $
text "Edges:"
$+$
(nest 2 $ vcat $
map (\e ->
let Edge o w = Graph.label e in
prettyTCM (Graph.source e) <+>
text "-[" <+> return (P.pretty o) <> text "," <+>
return (P.pretty w) <+> text "]->" <+>
prettyTCM (Graph.target e))
es)
return es
computeEdges
:: Set QName
-> QName
-> OccurrencesBuilder
-> TCM [Graph.Edge Node Edge]
computeEdges muts q ob =
($ []) <$> mkEdge __IMPOSSIBLE__ StrictPos (preprocess ob)
where
mkEdge to !pol ob = case ob of
Concat' obs -> foldr (liftM2 (.)) (return id)
[ mkEdge to pol ob | ob <- obs ]
OccursAs' w ob -> do (to, pol) <- mkEdge' to pol w
mkEdge to pol ob
OccursHere' (AnArg i) o ->
return $ applyUnless (null pol) (Graph.Edge
{ Graph.source = ArgNode q i
, Graph.target = to
, Graph.label = Edge pol o
} :)
OccursHere' (ADef q') o ->
return $ applyUnless (null pol || Set.notMember q' muts) (Graph.Edge
{ Graph.source = DefNode q'
, Graph.target = to
, Graph.label = Edge pol o
} :)
mkEdge' to !pol w = case w of
VarArg -> mixed
MetaArg -> mixed
LeftOfArrow -> negative
DefArg d i -> do
pol' <- isGuarding d
if Set.member d muts
then return (ArgNode d i, pol')
else addPol =<< otimes pol' <$> getArgOccurrence d i
UnderInf -> addPol GuardPos
ConArgType _ -> keepGoing
IndArgType _ -> mixed
InClause _ -> keepGoing
Matched -> mixed
InDefOf d -> do
pol' <- isGuarding d
return (DefNode d, pol')
where
keepGoing = return (to, pol)
mixed = return (to, Mixed)
negative = return (to, otimes pol JustNeg)
addPol pol' = return (to, otimes pol pol')
isGuarding d = do
isDR <- isDataOrRecordType d
return $ case isDR of
Just IsData -> GuardPos
_ -> StrictPos