module Agda.TypeChecking.Positivity where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.DeepSeq
import Control.Monad.Reader
import Data.Either
import Data.Graph (SCC(..), flattenSCC)
import Data.List as List hiding (null)
import Data.Maybe (mapMaybe, fromMaybe)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Debug.Trace
import Test.QuickCheck
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Datatypes (isDataOrRecordType, DataOrRecord(..))
import Agda.TypeChecking.Records (unguardedRecord, recursiveRecord)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (primInf, CoinductionKit(..), coinductionKit)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
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 Agda.Utils.SemiRing
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
type Graph n e = Graph.Graph n n e
checkStrictlyPositive :: Set QName -> TCM ()
checkStrictlyPositive qset = disableDestructiveUpdate $ do
let qs = Set.toList qset
reportSDoc "tc.pos.tick" 100 $ text "positivity of" <+> prettyTCM qs
g <- Graph.clean <$> buildOccurrenceGraph qset
let gstar = 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"
let sccs' = Graph.sccs' gstar
sccs = map flattenSCC sccs'
reportSDoc "tc.pos.graph.sccs" 10 $ do
let (triv, others) = partitionEithers $ for sccs' $ \ scc -> case scc of
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)
]
reportSDoc "tc.pos.graph.sccs" 15 $ text $ " sccs = " ++ show sccs
forM_ sccs $ \ 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 $ do
whenJustM (isDatatype q) $ \ dr -> do
reportSDoc "tc.pos.check" 10 $ text "Checking positivity of" <+> prettyTCM q
let loop = Graph.lookup (DefNode q) (DefNode q) gstar
how msg p =
fsep $ [prettyTCM q] ++ pwords "is" ++
case filter (p . occ) $
Graph.allPaths (p . occ) (DefNode q) (DefNode q) g of
Edge _ how : _ -> pwords (msg ++ ", because it occurs") ++
[prettyTCM how]
_ -> pwords $ msg ++ "."
whenM positivityCheckEnabled $
case loop of
Just o | p o -> do
err <- how "not strictly positive" p
setCurrentRange q $ typeError $ GenericDocError err
where p = (<= JustPos)
_ -> return ()
when (dr == IsRecord) $
case loop of
Just o | p o -> do
reportSDoc "tc.pos.record" 5 $ how "not guarded" p
unguardedRecord q
checkInduction q
where p = (<= StrictPos)
_ ->
case loop of
Just o | p o -> do
reportSDoc "tc.pos.record" 5 $ how "recursive" p
recursiveRecord q
checkInduction q
where p = (== GuardPos)
_ -> return ()
checkInduction q = 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 q = do
def <- theDef <$> getConstInfo q
return $ case def of
Datatype{dataClause = Nothing} -> Just IsData
Record {recClause = Nothing} -> Just IsRecord
_ -> Nothing
setMut [] = return ()
setMut [q] = return ()
setMut qs = forM_ qs $ \ q -> setMutual q (delete q qs)
setArgOccs :: Set QName -> [QName] -> Graph Node Occurrence -> TCM ()
setArgOccs qset qs g = do
let maxs = Map.fromListWith max
[ (q, i) | ArgNode q i <- Set.toList $ Graph.sourceNodes g, q `Set.member` qset ]
forM_ qs $ \ q -> inConcreteOrAbstractMode q $ do
reportSDoc "tc.pos.args" 10 $ text "checking args of" <+> prettyTCM q
n <- getDefArity =<< getConstInfo q
let findOcc i = fromMaybe Unused $ Graph.lookup (ArgNode q i) (DefNode q) g
args = caseMaybe (Map.lookup q maxs) (replicate n Unused) $ \ m ->
map findOcc [0 .. max m (n 1)]
reportSDoc "tc.pos.args" 10 $ sep
[ text "args of" <+> prettyTCM q <+> text "="
, nest 2 $ prettyList $ map (text . show) args
]
setArgOccurrences q $!! args
getDefArity :: Definition -> TCM Int
getDefArity def = case theDef def of
defn@Function{} -> do
let dropped = projectionArgs defn
subtract dropped . arity <$> instantiateFull (defType def)
Datatype{ dataPars = n } -> return n
Record{ recPars = n } -> return n
_ -> return 0
data OccursWhere
= LeftOfArrow OccursWhere
| DefArg QName Nat OccursWhere
| UnderInf OccursWhere
| VarArg OccursWhere
| MetaArg OccursWhere
| ConArgType QName OccursWhere
| IndArgType QName OccursWhere
| InClause Nat OccursWhere
| Matched OccursWhere
| InDefOf QName OccursWhere
| Here
| Unknown
deriving (Show, Eq, Ord)
(>*<) :: OccursWhere -> OccursWhere -> OccursWhere
Here >*< o = o
Unknown >*< o = Unknown
LeftOfArrow o1 >*< o2 = LeftOfArrow (o1 >*< o2)
DefArg d i o1 >*< o2 = DefArg d i (o1 >*< o2)
UnderInf o1 >*< o2 = UnderInf (o1 >*< o2)
VarArg o1 >*< o2 = VarArg (o1 >*< o2)
MetaArg o1 >*< o2 = MetaArg (o1 >*< o2)
ConArgType c o1 >*< o2 = ConArgType c (o1 >*< o2)
IndArgType c o1 >*< o2 = IndArgType c (o1 >*< o2)
InClause i o1 >*< o2 = InClause i (o1 >*< o2)
Matched o1 >*< o2 = Matched (o1 >*< o2)
InDefOf d o1 >*< o2 = InDefOf d (o1 >*< o2)
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 . group
prettyOs [] = __IMPOSSIBLE__
prettyOs [o] = prettyO o <> text "."
prettyOs (o:os) = prettyO o <> text ", which occurs" $$ prettyOs os
prettyO o = case o of
Here -> empty
Unknown -> empty
LeftOfArrow o -> explain o $ pwords "to the left of an arrow"
DefArg q i o -> explain o $ pwords "in the" ++ nth i ++ pwords "argument to" ++
[prettyTCM q]
UnderInf o -> do
Def inf _ <- ignoreSharing <$> primInf
explain o $ pwords "under" ++ [prettyTCM inf]
VarArg o -> explain o $ pwords "in an argument to a bound variable"
MetaArg o -> explain o $ pwords "in an argument to a metavariable"
ConArgType c o -> explain o $ pwords "in the type of the constructor" ++ [prettyTCM c]
IndArgType c o -> explain o $ pwords "in an index of the target type of the constructor" ++ [prettyTCM c]
InClause i o -> explain o $ pwords "in the" ++ nth i ++ pwords "clause"
Matched o -> explain o $ pwords "as matched against"
InDefOf d o -> explain o $ pwords "in the definition of" ++ [prettyTCM d]
explain o ds = prettyO o $$ fsep ds
maxOneLeftOfArrow o = case o of
LeftOfArrow o -> LeftOfArrow $ purgeArrows o
Here -> Here
Unknown -> Unknown
DefArg q i o -> DefArg q i $ maxOneLeftOfArrow o
UnderInf o -> UnderInf $ maxOneLeftOfArrow o
InDefOf d o -> InDefOf d $ maxOneLeftOfArrow o
VarArg o -> VarArg $ maxOneLeftOfArrow o
MetaArg o -> MetaArg $ maxOneLeftOfArrow o
ConArgType c o -> ConArgType c $ maxOneLeftOfArrow o
IndArgType c o -> IndArgType c $ maxOneLeftOfArrow o
InClause i o -> InClause i $ maxOneLeftOfArrow o
Matched o -> Matched $ maxOneLeftOfArrow o
purgeArrows o = case o of
LeftOfArrow o -> purgeArrows o
Here -> Here
Unknown -> Unknown
DefArg q i o -> DefArg q i $ purgeArrows o
UnderInf o -> UnderInf $ purgeArrows o
InDefOf d o -> InDefOf d $ purgeArrows o
VarArg o -> VarArg $ purgeArrows o
MetaArg o -> MetaArg $ purgeArrows o
ConArgType c o -> ConArgType c $ purgeArrows o
IndArgType c o -> IndArgType c $ purgeArrows o
InClause i o -> InClause i $ purgeArrows o
Matched o -> Matched $ purgeArrows o
splitOnDef o = case o of
Here -> [Here]
Unknown -> [Unknown]
InDefOf d o -> sp (InDefOf d) o
LeftOfArrow o -> sp LeftOfArrow o
DefArg q i o -> sp (DefArg q i) o
UnderInf o -> sp UnderInf o
VarArg o -> sp VarArg o
MetaArg o -> sp MetaArg o
ConArgType c o -> sp (ConArgType c) o
IndArgType c o -> sp (IndArgType c) o
InClause i o -> sp (InClause i) o
Matched o -> sp Matched o
where
sp f o = case splitOnDef o of
os@(InDefOf _ _:_) -> f Here : os
o:os -> f o : os
[] -> __IMPOSSIBLE__
data Item = AnArg Nat
| ADef QName
deriving (Eq, Ord, Show)
type Occurrences = Map Item [OccursWhere]
(>+<) :: Occurrences -> Occurrences -> Occurrences
(>+<) = Map.unionWith (++)
concatOccurs :: [Occurrences] -> Occurrences
concatOccurs = Map.unionsWith (++)
occursAs :: (OccursWhere -> OccursWhere) -> Occurrences -> Occurrences
occursAs f = Map.map (map f)
here :: Item -> Occurrences
here i = Map.singleton i [Here]
onlyVarsUpTo :: Nat -> Occurrences -> Occurrences
onlyVarsUpTo n = Map.filterWithKey p
where p (AnArg i) v = i < n
p (ADef q) v = True
data OccEnv = OccEnv
{ vars :: [Maybe Item]
, inf :: Maybe QName
}
type OccM = Reader OccEnv
withExtendedOccEnv :: Maybe Item -> OccM a -> OccM a
withExtendedOccEnv i = local $ \ e -> e { vars = i : vars e }
getOccurrences
:: (Show a, PrettyTCM a, ComputeOccurrences a)
=> [Maybe Item] -> a -> TCM Occurrences
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 Occurrences
instance ComputeOccurrences Clause where
occurrences cl = do
let ps = clausePats cl
(concatOccurs (mapMaybe matching (zip [0..] ps)) >+<) <$>
walk (patItems ps) (clauseBody cl)
where
matching (i, p)
| properlyMatching (unArg p) = Just $ occursAs Matched $ here $ AnArg i
| otherwise = Nothing
walk _ NoBody = return empty
walk [] (Body v) = occurrences v
walk (i : pis) (Bind b) = withExtendedOccEnv i $ walk pis $ absBody b
walk [] Bind{} = __IMPOSSIBLE__
walk (_ : _) Body{} = __IMPOSSIBLE__
patItems ps = concat $ zipWith patItem [0..] ps
patItem :: Int -> I.Arg Pattern -> [Maybe Item]
patItem i p = map (const $ Just $ AnArg i) $ patternVars p
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 empty here 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 $ here (ADef d) >+< concatOccurs (zipWith occsAs [0..] occs)
Con c 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 empty
Sort{} -> return empty
DontCare _ -> return empty
Shared p -> occurrences $ derefPtr p
ExtLam{} -> __IMPOSSIBLE__
instance ComputeOccurrences Level where
occurrences (Max as) = occurrences as
instance ComputeOccurrences PlusLevel where
occurrences ClosedLevel{} = return empty
occurrences (Plus _ l) = occurrences l
instance ComputeOccurrences LevelAtom where
occurrences l = case l of
MetaLevel _ vs -> occursAs MetaArg <$> occurrences vs
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 empty
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 (I.Arg a) where
occurrences = occurrences . unArg
instance ComputeOccurrences a => ComputeOccurrences (I.Dom a) where
occurrences = occurrences . unDom
instance ComputeOccurrences a => ComputeOccurrences [a] where
occurrences vs = concatOccurs <$> mapM occurrences vs
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 = inConcreteOrAbstractMode q $ do
reportSDoc "tc.pos" 25 $ do
a <- defAbstract <$> getConstInfo q
m <- asks envAbstractMode
text "computeOccurrences" <+> prettyTCM q <+> text (show a) <+> text (show m)
def <- getConstInfo q
occursAs (InDefOf q) <$> case theDef def of
Function{funClauses = cs} -> do
n <- getDefArity def
cs <- map (etaExpandClause n) <$> instantiateFull cs
concatOccurs . zipWith (occursAs . InClause) [0..] <$>
mapM (getOccurrences []) cs
Datatype{dataClause = Just c} -> getOccurrences [] =<< instantiateFull c
Datatype{dataPars = np, dataCons = cs} -> do
TelV tel t <- telView $ defType def
let xs = [np .. size tel 1]
ioccs = concatOccurs $ map (occursAs Matched . here . AnArg) xs
let conOcc c = do
a <- defType <$> getConstInfo c
TelV tel t <- telView' <$> normalise a
let indices = case unEl t of
Def _ vs -> genericDrop np vs
_ -> __IMPOSSIBLE__
let tel' = telFromList $ genericDrop 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 <$> (concatOccurs <$> mapM conOcc cs)
Record{recClause = Just c} -> getOccurrences [] =<< instantiateFull c
Record{recPars = np, recTel = tel} -> do
let tel' = telFromList $ genericDrop np $ telToList tel
vars = map (Just . AnArg) $ downFrom np
getOccurrences vars =<< instantiateFull tel'
Constructor{} -> return empty
Axiom{} -> return empty
Primitive{} -> return empty
etaExpandClause :: Nat -> Clause -> Clause
etaExpandClause n c@Clause{ clauseTel = tel, clausePerm = perm, namedClausePats = ps, clauseBody = b }
| m <= 0 = c
| otherwise = c
{ namedClausePats = ps ++ genericReplicate m (defaultArg $ unnamed $ VarP underscore)
, clauseBody = liftBody m b
, clauseTel = telFromList $
telToList tel ++ (replicate m $ (underscore,) <$> dummyDom)
, clausePerm = Perm.liftP m perm
}
where
m = n genericLength ps
bind 0 = id
bind n = Bind . Abs underscore . bind (n 1)
vars = map (defaultArg . var) $ downFrom m
liftBody m (Bind b) = Bind $ fmap (liftBody m) b
liftBody m NoBody = bind m NoBody
liftBody m (Body v) = bind m $ Body $ raise m v `apply` vars
data Node = DefNode QName
| ArgNode QName Nat
deriving (Eq, Ord)
instance Show Node where
show (DefNode q) = show q
show (ArgNode q i) = show q ++ "." ++ show i
instance PrettyTCM Node where
prettyTCM (DefNode q) = prettyTCM q
prettyTCM (ArgNode q i) = prettyTCM q <> text ("." ++ show i)
instance PrettyTCM n => PrettyTCM (WithNode n Edge) where
prettyTCM (WithNode n (Edge o w)) =
prettyTCM o <+> prettyTCM n <+> fsep (pwords $ show 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.unionsWith oplus <$> mapM defGraph (Set.toList qs)
where
defGraph :: QName -> TCM (Graph Node Edge)
defGraph q = do
occs <- computeOccurrences q
Graph.unionsWith oplus <$> do
forM (Map.assocs occs) $ \ (item, occs) -> do
let src = itemToNode item
es <- mapM (computeEdge qs) occs
return $ Graph.unionsWith oplus $
for es $ \ (tgt, w) -> Graph.singleton src tgt w
where
itemToNode (AnArg i) = ArgNode q i
itemToNode (ADef q) = DefNode q
computeEdge :: Set QName -> OccursWhere -> TCM (Node, Edge)
computeEdge muts o = do
(to, occ) <- mkEdge __IMPOSSIBLE__ StrictPos o
return (to, Edge occ o)
where
mkEdge to pol o = case o of
Here -> return (to, pol)
Unknown -> return (to, Mixed)
VarArg o -> mixed o
MetaArg o -> mixed o
LeftOfArrow o -> negative o
DefArg d i o -> do
isDR <- isDataOrRecordType d
let pol' | isDR == Just IsData = GuardPos
| otherwise = StrictPos
if Set.member d muts then mkEdge (ArgNode d i) pol' o
else addPol o =<< otimes pol' <$> getArgOccurrence d i
UnderInf o -> addPol o GuardPos
ConArgType _ o -> keepGoing o
IndArgType _ o -> mixed o
InClause _ o -> keepGoing o
Matched o -> mixed o
InDefOf d o -> do
isDR <- isDataOrRecordType d
let pol' | isDR == Just IsData = GuardPos
| otherwise = StrictPos
mkEdge (DefNode d) pol' o
where
keepGoing = mkEdge to pol
mixed = mkEdge to Mixed
negative o = mkEdge to (otimes pol JustNeg) o
addPol o pol' = mkEdge to (otimes pol pol') o
inArg d i = mkEdge (ArgNode d i) StrictPos
instance Arbitrary OccursWhere where
arbitrary = sized arbitraryS
where
arbitraryS n = oneof $
[ return Here
, return Unknown
] ++
if n <= 0 then [] else
[ LeftOfArrow <$> arb
, DefArg <$> arbitrary <*> arbitrary <*> arb
, UnderInf <$> arb
, VarArg <$> arb
, MetaArg <$> arb
, ConArgType <$> arbitrary <*> arb
, IndArgType <$> arbitrary <*> arb
, InClause <$> arbitrary <*> arb
, Matched <$> arb
, InDefOf <$> arbitrary <*> arb
]
where arb = arbitraryS (n 1)
shrink x = replaceConstructor x ++ genericShrink x
where
replaceConstructor Here = []
replaceConstructor Unknown = []
replaceConstructor _ = [Here, Unknown]
genericShrink (LeftOfArrow a) = a : [ LeftOfArrow a | a <- shrink a ]
genericShrink (DefArg a b c) = c : [ DefArg a b c | c <- shrink c ]
genericShrink (UnderInf a) = a : [ UnderInf a | a <- shrink a ]
genericShrink (VarArg a) = a : [ VarArg a | a <- shrink a ]
genericShrink (MetaArg a) = a : [ MetaArg a | a <- shrink a ]
genericShrink (ConArgType a b) = b : [ ConArgType a b | b <- shrink b ]
genericShrink (IndArgType a b) = b : [ IndArgType a b | b <- shrink b ]
genericShrink (InClause a b) = b : [ InClause a b | b <- shrink b ]
genericShrink (Matched a) = a : [ Matched a | a <- shrink a ]
genericShrink (InDefOf a b) = b : [ InDefOf a b | b <- shrink b ]
genericShrink Here = []
genericShrink Unknown = []
instance CoArbitrary OccursWhere where
coarbitrary (LeftOfArrow a) = variant 0 . coarbitrary a
coarbitrary (DefArg a b c) = variant 1 . coarbitrary (a, b, c)
coarbitrary (UnderInf a) = variant 2 . coarbitrary a
coarbitrary (VarArg a) = variant 3 . coarbitrary a
coarbitrary (MetaArg a) = variant 4 . coarbitrary a
coarbitrary (ConArgType a b) = variant 5 . coarbitrary (a, b)
coarbitrary (IndArgType a b) = variant 6 . coarbitrary (a, b)
coarbitrary (InClause a b) = variant 7 . coarbitrary (a, b)
coarbitrary (Matched a) = variant 8 . coarbitrary a
coarbitrary (InDefOf a b) = variant 9 . coarbitrary (a, b)
coarbitrary Here = variant 10
coarbitrary Unknown = variant 11
instance Arbitrary Edge where
arbitrary = Edge <$> arbitrary <*> arbitrary
shrink (Edge o w) = [ Edge o w | o <- shrink o ] ++
[ Edge o w | w <- shrink w ]
instance CoArbitrary Edge where
coarbitrary (Edge o w) = coarbitrary (o, w)