{-# 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 Data.Sequence (Seq)
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 = do
let qs = Set.toList qset
reportSDoc "tc.pos.tick" 100 $ "positivity of" <+> prettyTCM qs
g <- buildOccurrenceGraph qset
let (gstar, sccs) =
Graph.gaussJordanFloydWarshallMcNaughtonYamada $ fmap occ g
reportSDoc "tc.pos.tick" 100 $ "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
[ "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
[ "transitive closure of positivity graph for" <+>
prettyTCM qs
, nest 2 $ prettyTCM gstar
]
setArgOccs qset qs gstar
reportSDoc "tc.pos.tick" 100 $ "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 $ "checked positivity"
where
checkPos :: Graph Node (Edge OccursWhere) ->
Graph Node Occurrence ->
QName -> TCM ()
checkPos g gstar q = inConcreteOrAbstractMode q $ \ _def -> do
whenJustM (isDatatype q) $ \ dr -> do
reportSDoc "tc.pos.check" 10 $ "Checking positivity of" <+> prettyTCM q
let loop :: Maybe Occurrence
loop = Graph.lookup (DefNode q) (DefNode q) gstar
g' :: Graph Node (Edge (Seq OccursWhere))
g' = fmap (fmap DS.singleton) g
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 $
"record type " <+> prettyTCM q <+>
"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 =<<
"Recursive record" <+> prettyTCM q <+>
"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 -> when (hasDefinition $ theDef def) $ do
reportSDoc "tc.pos.args" 10 $ "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
[ "args of" <+> prettyTCM q <+> "="
, nest 2 $ prettyList $ map prettyTCM args
]
setArgOccurrences q $!! args
where
hasDefinition :: Defn -> Bool
hasDefinition = \case
Axiom{} -> False
DataOrRecSig{} -> False
GeneralizableVar{} -> False
AbstractDefn{} -> False
Primitive{} -> False
Constructor{} -> False
Function{} -> True
Datatype{} -> True
Record{} -> True
getDefArity :: Definition -> TCM Int
getDefArity def = do
let dropped = case theDef def of
defn@Function{} -> projectionArgs defn
_ -> 0
subtract dropped . arity <$> instantiateFull (defType def)
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
emptyOB :: OccurrencesBuilder
emptyOB = Concat []
(>+<) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
occs1 >+< occs2 = Concat [occs1, occs2]
preprocess :: OccurrencesBuilder -> OccurrencesBuilder'
preprocess ob = case pp Nothing ob of
Nothing -> Concat' []
Just ob -> ob
where
pp :: Maybe Nat
-> OccurrencesBuilder
-> Maybe OccurrencesBuilder'
pp !m = \case
Concat obs -> case mapMaybe (pp m) obs of
[] -> Nothing
obs -> return (Concat' obs)
OccursAs w ob -> OccursAs' w <$> pp m ob
OnlyVarsUpTo n ob -> pp (Just $! maybe n (min n) m) ob
OccursHere i -> do
guard keep
return (OccursHere' i)
where
keep = case (m, i) of
(Nothing, _) -> True
(_, ADef _) -> True
(Just m, AnArg i) -> i < m
flatten :: OccurrencesBuilder -> Map Item Integer
flatten =
Map.fromListWith (+) .
flip flatten' [] .
preprocess
where
flatten' :: OccurrencesBuilder'
-> [(Item, Integer)] -> [(Item, Integer)]
flatten' (Concat' obs) = foldr (\occs f -> flatten' occs . f) id obs
flatten' (OccursAs' _ ob) = flatten' ob
flatten' (OccursHere' i) = ((i, 1) :)
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 $ "computing occurrences in " <+> text (show a)
reportSDoc "tc.pos.occ" 20 $ "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 = indexWithDefault unbound vars i
unbound = 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
Dummy{} -> 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
occurrences (IApply x y a) = occurrences (x,(y,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 (Map Item Integer)
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 <- asksTC envAbstractMode
cur <- asksTC envCurrentModule
"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 IsIndex . OccursHere . AnArg) xs
let conOcc c = do
a <- defType <$> getConstInfo c
TelV tel t <- telView'Path =<< 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
DataOrRecSig{} -> return emptyOB
Primitive{} -> return emptyOB
GeneralizableVar{} -> return emptyOB
AbstractDefn{} -> __IMPOSSIBLE__
data Node = DefNode !QName
| ArgNode !QName !Nat
deriving (Eq, Ord)
data Edge a = Edge !Occurrence a
deriving (Eq, Ord, Show, Functor)
mergeEdges :: Edge a -> Edge a -> Edge a
mergeEdges _ e@(Edge Mixed _) = e
mergeEdges e@(Edge Mixed _) _ = e
mergeEdges (Edge Unused _) e = e
mergeEdges e (Edge Unused _) = e
mergeEdges (Edge JustNeg _) e@(Edge JustNeg _) = e
mergeEdges _ e@(Edge JustNeg w) = Edge Mixed w
mergeEdges e@(Edge JustNeg w) _ = Edge Mixed w
mergeEdges _ e@(Edge JustPos _) = e
mergeEdges e@(Edge JustPos _) _ = e
mergeEdges _ e@(Edge StrictPos _) = e
mergeEdges e@(Edge StrictPos _) _ = e
mergeEdges (Edge GuardPos _) e@(Edge GuardPos _) = e
instance SemiRing (Edge (Seq OccursWhere)) where
ozero = Edge ozero DS.empty
oone = Edge oone DS.empty
oplus = mergeEdges
otimes (Edge o1 w1) (Edge o2 w2) = Edge (otimes o1 o2) (w1 DS.>< w2)
buildOccurrenceGraph :: Set QName -> TCM (Graph Node (Edge OccursWhere))
buildOccurrenceGraph qs =
Graph.fromEdgesWith mergeEdges . concat <$>
mapM defGraph (Set.toList qs)
where
defGraph :: QName -> TCM [Graph.Edge Node (Edge OccursWhere)]
defGraph q = inConcreteOrAbstractMode q $ \ _def -> do
occs <- computeOccurrences' q
reportSDoc "tc.pos.occs" 40 $
("Occurrences in" <+> prettyTCM q <> ":")
$+$
(nest 2 $ vcat $
map (\(i, n) ->
text (show i) <> ":" <+> text (show n) <+>
"occurrences") $
List.sortBy (compare `on` snd) $
Map.toList (flatten occs))
es <- computeEdges qs q occs
reportSDoc "tc.pos.occs.edges" 60 $
"Edges:"
$+$
(nest 2 $ vcat $
map (\e ->
let Edge o w = Graph.label e in
prettyTCM (Graph.source e) <+>
"-[" <+> return (P.pretty o) <> "," <+>
return (P.pretty w) <+> "]->" <+>
prettyTCM (Graph.target e))
es)
return es
computeEdges
:: Set QName
-> QName
-> OccurrencesBuilder
-> TCM [Graph.Edge Node (Edge OccursWhere)]
computeEdges muts q ob =
($ []) <$> mkEdge StrictPos (preprocess ob)
__IMPOSSIBLE__ DS.empty DS.empty
where
mkEdge
:: Occurrence
-> OccurrencesBuilder'
-> Node
-> DS.Seq Where
-> DS.Seq Where
-> TCM ([Graph.Edge Node (Edge OccursWhere)] ->
[Graph.Edge Node (Edge OccursWhere)])
mkEdge !pol ob to cs os = case ob of
Concat' obs ->
foldr (liftM2 (.)) (return id)
[ mkEdge pol ob to cs os | ob <- obs ]
OccursAs' w ob -> do
(to', pol) <- mkEdge' to pol w
let mk = mkEdge pol ob
case to' of
Nothing -> mk to cs (os DS.|> w)
Just to -> mk to (cs DS.>< os) (DS.singleton w)
OccursHere' i ->
let o = OccursWhere (getRange i) cs os in
case i of
AnArg i ->
return $ applyUnless (null pol) (Graph.Edge
{ Graph.source = ArgNode q i
, Graph.target = to
, Graph.label = Edge pol o
} :)
ADef q' ->
return $ applyUnless (null pol || Set.notMember q' muts)
(Graph.Edge
{ Graph.source = DefNode q'
, Graph.target = to
, Graph.label = Edge pol o
} :)
mkEdge'
:: Node
-> Occurrence
-> Where
-> TCM (Maybe Node, Occurrence)
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 (Just (ArgNode d i), pol')
else addPol =<< otimes pol' <$> getArgOccurrence d i
UnderInf -> addPol GuardPos
ConArgType _ -> keepGoing
IndArgType _ -> mixed
InClause _ -> keepGoing
Matched -> mixed
IsIndex -> mixed
InDefOf d -> do
pol' <- isGuarding d
return (Just (DefNode d), pol')
where
keepGoing = return (Nothing, pol)
mixed = return (Nothing, Mixed)
negative = return (Nothing, otimes pol JustNeg)
addPol pol' = return (Nothing, otimes pol pol')
isGuarding d = do
isDR <- isDataOrRecordType d
return $ case isDR of
Just IsData -> GuardPos
_ -> StrictPos
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 OccursWhere)) where
prettyTCM (WithNode n (Edge o w)) = vcat
[ prettyTCM o <+> prettyTCM n
, nest 2 $ return $ P.pretty w
]
instance PrettyTCM (Seq OccursWhere) where
prettyTCM =
fmap snd . prettyOWs . map adjustLeftOfArrow . uniq . Fold.toList
where
nth 0 = pwords "first"
nth 1 = pwords "second"
nth 2 = pwords "third"
nth n = pwords $ show (n + 1) ++ "th"
uniq :: [OccursWhere] -> [OccursWhere]
uniq = map head . List.groupBy ((==) `on` snd')
where
snd' (OccursWhere _ _ ws) = ws
prettyOWs :: [OccursWhere] -> TCM (String, Doc)
prettyOWs [] = __IMPOSSIBLE__
prettyOWs [o] = do
(s, d) <- prettyOW o
return (s, d P.<> ".")
prettyOWs (o:os) = do
(s1, d1) <- prettyOW o
(s2, d2) <- prettyOWs os
return (s1, d1 P.<> "," P.<+> "which" P.<+> P.text s2 P.$$ d2)
prettyOW :: OccursWhere -> TCM (String, Doc)
prettyOW (OccursWhere _ cs ws)
| null cs = prettyWs ws
| otherwise = do
(s, d1) <- prettyWs ws
(_, d2) <- prettyWs cs
return (s, d1 P.$$ "(" P.<> d2 P.<> ")")
prettyWs :: Seq Where -> TCM (String, Doc)
prettyWs ws = case Fold.toList ws of
[InDefOf d, IsIndex] ->
(,) "is" <$> fsep (pwords "an index of" ++ [prettyTCM d])
_ ->
(,) "occurs" <$>
Fold.foldrM (\w d -> return d $$ fsep (prettyW w)) empty ws
prettyW :: Where -> [TCM Doc]
prettyW w = case w of
LeftOfArrow -> pwords "to the left of an arrow"
DefArg q i -> pwords "in the" ++ nth i ++ pwords "argument of" ++
[prettyTCM q]
UnderInf -> pwords "under" ++
[do
Def inf _ <- primInf
prettyTCM inf]
VarArg -> pwords "in an argument of a bound variable"
MetaArg -> pwords "in an argument of 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"
IsIndex -> pwords "as an index"
InDefOf d -> pwords "in the definition of" ++ [prettyTCM d]
adjustLeftOfArrow :: OccursWhere -> OccursWhere
adjustLeftOfArrow (OccursWhere r cs os) =
OccursWhere r (DS.filter (not . isArrow) cs) $
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 os
isArrow LeftOfArrow{} = True
isArrow _ = False