summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Positivity.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Positivity.hs')
-rw-r--r--src/full/Agda/TypeChecking/Positivity.hs232
1 files changed, 91 insertions, 141 deletions
diff --git a/src/full/Agda/TypeChecking/Positivity.hs b/src/full/Agda/TypeChecking/Positivity.hs
index d7add67..f94cf4b 100644
--- a/src/full/Agda/TypeChecking/Positivity.hs
+++ b/src/full/Agda/TypeChecking/Positivity.hs
@@ -1,8 +1,5 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TupleSections #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Check that a datatype is strictly positive.
@@ -13,28 +10,31 @@ import Prelude hiding (null)
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 Data.List as List hiding (null)
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 Test.QuickCheck
-
import Agda.Syntax.Common
import qualified Agda.Syntax.Info as Info
+import Agda.Syntax.Position (fuseRange, Range, HasRange(..), noRange)
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.Datatypes (isDataOrRecordType, DataOrRecord(..))
-import Agda.TypeChecking.Records (unguardedRecord, recursiveRecord)
+import Agda.TypeChecking.Records
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (primInf, CoinductionKit(..), coinductionKit)
import Agda.TypeChecking.Reduce
@@ -51,6 +51,7 @@ import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.Permutation as Perm
import Agda.Utils.SemiRing
+import Agda.Utils.Singleton
import Agda.Utils.Size
#include "undefined.h"
@@ -109,7 +110,7 @@ checkStrictlyPositive mi qset = disableDestructiveUpdate $ do
checkPos :: Graph Node Edge ->
Graph Node Occurrence ->
QName -> TCM ()
- checkPos g gstar q = inConcreteOrAbstractMode q $ do
+ checkPos g gstar q = inConcreteOrAbstractMode q $ \ _def -> do
-- we check positivity only for data or record definitions
whenJustM (isDatatype q) $ \ dr -> do
reportSDoc "tc.pos.check" 10 $ text "Checking positivity of" <+> prettyTCM q
@@ -122,15 +123,17 @@ checkStrictlyPositive mi qset = disableDestructiveUpdate $ do
-- which relates productOfEdgesInBoundedWalk to
-- gaussJordanFloydWarshallMcNaughtonYamada.
- how :: String -> Occurrence -> TCM Doc
- how msg bound =
+ reason bound =
case productOfEdgesInBoundedWalk
occ g (DefNode q) (DefNode q) bound of
- Just (Edge _ how) -> fsep $
+ 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 how]
- Nothing -> __IMPOSSIBLE__
+ [prettyTCM (reason bound)]
-- if we have a negative loop, raise error
@@ -140,9 +143,8 @@ checkStrictlyPositive mi qset = disableDestructiveUpdate $ do
when (Info.mutualPositivityCheck mi) $
whenM positivityCheckEnabled $
case loop of
- Just o | o <= JustPos -> do
- err <- how "not strictly positive" JustPos
- setCurrentRange q $ typeError $ GenericDocError err
+ Just o | o <= JustPos ->
+ warning $ NotStrictlyPositive q (reason JustPos)
_ -> return ()
-- if we find an unguarded record, mark it as such
@@ -157,6 +159,13 @@ checkStrictlyPositive mi qset = disableDestructiveUpdate $ do
reportSDoc "tc.pos.record" 5 $ how "recursive" GuardPos
recursiveRecord q
checkInduction q
+ -- If the record is not recursive, switch on eta
+ -- unless it is coinductive or a no-eta-equality record.
+ Nothing -> do
+ reportSDoc "tc.pos.record" 10 $
+ text "record type " <+> prettyTCM q <+>
+ text "is not recursive"
+ nonRecursiveRecord q
_ -> return ()
checkInduction :: QName -> TCM ()
@@ -202,9 +211,9 @@ checkStrictlyPositive mi qset = disableDestructiveUpdate $ do
-- Compute a map from each name in q to the maximal argument index
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
+ forM_ qs $ \ q -> inConcreteOrAbstractMode q $ \ def -> do
reportSDoc "tc.pos.args" 10 $ text "checking args of" <+> prettyTCM q
- n <- getDefArity =<< getConstInfo q
+ n <- getDefArity def
-- If there is no outgoing edge @ArgNode q i@, all @n@ arguments are @Unused@.
-- Otherwise, we obtain the occurrences from the Graph.
let findOcc i = fromMaybe Unused $ Graph.lookup (ArgNode q i) (DefNode q) g
@@ -231,37 +240,14 @@ getDefArity def = case theDef def of
Record{ recPars = n } -> return n
_ -> return 0
--- Specification of occurrences -------------------------------------------
+-- Operations on occurrences -------------------------------------------
-- See also Agda.TypeChecking.Positivity.Occurrence.
--- | Description of an occurrence.
-data OccursWhere
- = Unknown
- -- ^ an unknown position (treated as negative)
- | Known (DS.Seq Where)
- -- ^ The elements of the sequence, from left to right, explain how
- -- to get to the occurrence.
- deriving (Show, Eq, Ord)
-
--- | One part of the description of an occurrence.
-data Where
- = LeftOfArrow
- | DefArg QName Nat -- ^ in the nth argument of a define constant
- | UnderInf -- ^ in the principal argument of built-in ∞
- | VarArg -- ^ as an argument to a bound variable
- | MetaArg -- ^ as an argument of a metavariable
- | ConArgType QName -- ^ in the type of a constructor
- | IndArgType QName -- ^ in a datatype index of a constructor
- | InClause Nat -- ^ in the nth clause of a defined function
- | Matched -- ^ matched against in a clause of a defined function
- | InDefOf QName -- ^ in the definition of a constant
- deriving (Show, Eq, Ord)
-
(>*<) :: OccursWhere -> OccursWhere -> OccursWhere
-Unknown >*< _ = Unknown
-Known _ >*< Unknown = Unknown
-Known os1 >*< Known os2 = Known (os1 DS.>< os2)
+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
@@ -278,8 +264,8 @@ instance PrettyTCM OccursWhere where
prettyOs [o] = prettyO o <> text "."
prettyOs (o:os) = prettyO o <> text ", which occurs" $$ prettyOs os
- prettyO Unknown = empty
- prettyO (Known ws) =
+ prettyO Unknown = empty
+ prettyO (Known _ ws) =
Fold.foldrM (\w d -> return d $$ fsep (prettyW w)) empty ws
prettyW w = case w of
@@ -298,8 +284,8 @@ instance PrettyTCM OccursWhere where
Matched -> pwords "as matched against"
InDefOf d -> pwords "in the definition of" ++ [prettyTCM d]
- maxOneLeftOfArrow Unknown = Unknown
- maxOneLeftOfArrow (Known ws) = Known $
+ maxOneLeftOfArrow Unknown = Unknown
+ maxOneLeftOfArrow (Known r ws) = Known r $
noArrows
DS.><
case DS.viewl startsWithArrow of
@@ -311,20 +297,20 @@ instance PrettyTCM OccursWhere where
isArrow LeftOfArrow{} = True
isArrow _ = False
- splitOnDef Unknown = [Unknown]
- splitOnDef (Known ws) = split ws DS.empty
+ 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 acc : rest
+ else Known r acc : rest
w DS.:< ws -> split ws (acc DS.|> w)
- DS.EmptyL -> [Known acc]
+ DS.EmptyL -> [Known r acc]
instance Sized OccursWhere where
- size Unknown = 1
- size (Known ws) = 1 + size ws
+ size Unknown = 1
+ size (Known _ ws) = 1 + size ws
-- Computing occurrences --------------------------------------------------
@@ -332,6 +318,10 @@ 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]
-- | Used to build 'Occurrences' and occurrence graphs.
@@ -377,7 +367,7 @@ preprocess ob = case pp Nothing DS.empty ob of
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 ws))
+ return (OccursHere' i (Known (getRange i) ws))
where
keep = case (m, i) of
(Nothing, _) -> True
@@ -427,7 +417,10 @@ data OccEnv = OccEnv
type OccM = Reader OccEnv
withExtendedOccEnv :: Maybe Item -> OccM a -> OccM a
-withExtendedOccEnv i = local $ \ e -> e { vars = i : vars e }
+withExtendedOccEnv i = withExtendedOccEnv' [i]
+
+withExtendedOccEnv' :: [Maybe Item] -> OccM a -> OccM a
+withExtendedOccEnv' is = local $ \ e -> e { vars = is ++ vars e }
-- | Running the monad
getOccurrences
@@ -444,30 +437,27 @@ class ComputeOccurrences a where
instance ComputeOccurrences Clause where
occurrences cl = do
- let ps = unnumberPatVars $ clausePats cl
+ let ps = namedClausePats cl
+ items = IntMap.elems $ patItems ps -- sorted from low to high DBI
(Concat (mapMaybe matching (zip [0..] ps)) >+<) <$>
- walk (patItems ps) (clauseBody cl)
+ withExtendedOccEnv' items (occurrences $ clauseBody cl)
where
matching (i, p)
- | properlyMatching (unArg p) = Just $ OccursAs Matched $
- OccursHere $ AnArg i
+ | properlyMatching (namedThing $ unArg p) =
+ Just $ OccursAs Matched $ OccursHere $ AnArg i
| otherwise = Nothing
- walk _ NoBody = return emptyOB
- walk [] (Body v) = occurrences v
- walk (i : pis) (Bind b) = withExtendedOccEnv i $ walk pis $ absBody b
- walk [] Bind{} = __IMPOSSIBLE__
- walk (_ : _) Body{} = __IMPOSSIBLE__
-
-- @patItems ps@ creates a map from the pattern variables of @ps@
-- to the index of the argument they are bound in.
- -- This map is given as a list.
- patItems ps = concat $ zipWith patItem [0..] ps
+ patItems ps = mconcat $ zipWith patItem [0..] ps
- -- @patItem i p@ replicates index @i@ as often as there are
- -- pattern variables in @p@ (dot patterns count as variable)
- patItem :: Int -> Arg Pattern -> [Maybe Item]
- patItem i p = map (const $ Just $ AnArg i) $ patternVars p
+ -- @patItem i p@ assigns index @i@ to each pattern variable in @p@
+ 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
@@ -490,7 +480,7 @@ instance ComputeOccurrences Term where
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 c args -> occurrences args
+ Con _ _ args -> occurrences args
MetaV _ args -> OccursAs MetaArg <$> occurrences args
Pi a b -> do
oa <- occurrences a
@@ -512,7 +502,11 @@ instance ComputeOccurrences PlusLevel where
instance ComputeOccurrences LevelAtom where
occurrences l = case l of
- MetaLevel _ vs -> OccursAs MetaArg <$> occurrences vs
+ MetaLevel x es -> occurrences $ MetaV x es
+ -- Andreas, 2016-07-25, issue 2108
+ -- NOT: OccursAs MetaArg <$> occurrences vs
+ -- since we need to unSpine!
+ -- (Otherwise, we run into __IMPOSSIBLE__ at Proj elims)
BlockedLevel _ v -> occurrences v
NeutralLevel _ v -> occurrences v
UnreducedLevel v -> occurrences v
@@ -541,6 +535,10 @@ instance ComputeOccurrences a => ComputeOccurrences (Dom a) where
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
@@ -557,12 +555,13 @@ computeOccurrences q = flatten <$> computeOccurrences' q
-- | Computes the occurrences in the given definition.
computeOccurrences' :: QName -> TCM OccurrencesBuilder
-computeOccurrences' q = inConcreteOrAbstractMode q $ do
+computeOccurrences' q = inConcreteOrAbstractMode q $ \ def -> do
reportSDoc "tc.pos" 25 $ do
- a <- defAbstract <$> getConstInfo q
+ let a = defAbstract def
m <- asks envAbstractMode
+ cur <- asks envCurrentModule
text "computeOccurrences" <+> prettyTCM q <+> text (show a) <+> text (show m)
- def <- getConstInfo q
+ <+> prettyTCM cur
OccursAs (InDefOf q) <$> case theDef def of
Function{funClauses = cs} -> do
n <- getDefArity def
@@ -597,33 +596,31 @@ computeOccurrences' q = inConcreteOrAbstractMode q $ do
Constructor{} -> return emptyOB
Axiom{} -> return emptyOB
Primitive{} -> return emptyOB
+ AbstractDefn -> __IMPOSSIBLE__
-- | Eta expand a clause to have the given number of variables.
-- Warning: doesn't put correct types in telescope!
-- This is used instead of special treatment of lambdas
-- (which was unsound: issue 121)
etaExpandClause :: Nat -> Clause -> Clause
-etaExpandClause n c@Clause{ clauseTel = tel, namedClausePats = ps, clauseBody = b }
+etaExpandClause n c
| m <= 0 = c
| otherwise = c
- { namedClausePats = raise m ps ++ map (defaultArg . unnamed . VarP . (,underscore)) (downFrom m)
- , clauseBody = liftBody m b
+ { namedClausePats = raise m (namedClausePats c) ++
+ map (\i -> defaultArg $ namedDBVarP i underscore) (downFrom m)
+ , clauseBody = liftBody m $ clauseBody c
, clauseTel = telFromList $
- telToList tel ++ (replicate m $ (underscore,) <$> dummyDom)
+ telToList (clauseTel c) ++ (replicate m $ (underscore,) <$> dummyDom)
-- dummyDom, not __IMPOSSIBLE__, because of debug printing.
}
where
- m = n - genericLength ps
-
- bind 0 = id
- bind n = Bind . Abs underscore . bind (n - 1)
+ m = n - genericLength (namedClausePats c)
vars = map (defaultArg . var) $ downFrom m
-- vars = reverse [ defaultArg $ var i | i <- [0..m - 1] ]
- 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
+ liftBody m (Just v) = Just $ raise m v `apply` vars
+ liftBody m Nothing = Nothing
-- Building the occurrence graph ------------------------------------------
@@ -690,9 +687,8 @@ buildOccurrenceGraph qs =
mapM defGraph (Set.toList qs)
where
defGraph :: QName -> TCM [Graph.Edge Node Node Edge]
- defGraph q = do
+ defGraph q = inConcreteOrAbstractMode q $ \ _def -> do
occs <- computeOccurrences' q
- es <- computeEdges qs q occs
reportSDoc "tc.pos.occs" 40 $
(text "Occurrences in" <+> prettyTCM q <> text ":")
@@ -712,6 +708,11 @@ buildOccurrenceGraph qs =
$+$
(nest 2 $ vcat $ map (text . show) os))
(Map.toList (flatten occs)))
+
+ -- Placing this line before the reportSDoc lines above creates a
+ -- space leak: occs is retained for too long.
+ es <- computeEdges qs q occs
+
reportSDoc "tc.pos.occs.edges" 60 $
text "Edges:"
$+$
@@ -800,54 +801,3 @@ computeEdges muts q ob =
return $ case isDR of
Just IsData -> GuardPos -- a datatype is guarding
_ -> StrictPos
-
-------------------------------------------------------------------------
--- * Generators and tests
-------------------------------------------------------------------------
-
-instance Arbitrary OccursWhere where
- arbitrary = oneof [return Unknown, Known <$> arbitrary]
-
- shrink Unknown = []
- shrink (Known ws) = Unknown : [ Known ws | ws <- shrink ws ]
-
-instance Arbitrary Where where
- arbitrary = oneof
- [ return LeftOfArrow
- , DefArg <$> arbitrary <*> arbitrary
- , return UnderInf
- , return VarArg
- , return MetaArg
- , ConArgType <$> arbitrary
- , IndArgType <$> arbitrary
- , InClause <$> arbitrary
- , return Matched
- , InDefOf <$> arbitrary
- ]
-
-instance CoArbitrary OccursWhere where
- coarbitrary (Known ws) = variant 0 . coarbitrary ws
- coarbitrary Unknown = variant 1
-
-instance CoArbitrary Where where
- coarbitrary LeftOfArrow = variant 0
- coarbitrary (DefArg a b) = variant 1 . coarbitrary (a, b)
- coarbitrary UnderInf = variant 2
- coarbitrary VarArg = variant 3
- coarbitrary MetaArg = variant 4
- coarbitrary (ConArgType a) = variant 5 . coarbitrary a
- coarbitrary (IndArgType a) = variant 6 . coarbitrary a
- coarbitrary (InClause a) = variant 7 . coarbitrary a
- coarbitrary Matched = variant 8
- coarbitrary (InDefOf a) = variant 9 . coarbitrary a
-
-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)
-
--- properties moved to Agda.TypeChecking.Positivity.Tests