module Agda.TypeChecking.MetaVars.Occurs where
import Control.Applicative
import Control.Monad
import Control.Monad.Error
import Control.Monad.Reader
import Control.Monad.State
import Data.List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set
import Data.Traversable (traverse)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Free hiding (Occurrence(..))
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Eliminators
import Agda.TypeChecking.Records
import Agda.TypeChecking.Datatypes (isDataOrRecordType, DataOrRecord(..))
import Agda.TypeChecking.MetaVars
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
import qualified Agda.Utils.VarSet as Set
import Agda.Utils.Impossible
#include "../../undefined.h"
modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()
modifyOccursCheckDefs f = modify $ \ st ->
st { stOccursCheckDefs = f (stOccursCheckDefs st) }
initOccursCheck :: MetaVariable -> TCM ()
initOccursCheck mv = modifyOccursCheckDefs . const =<<
if (miMetaOccursCheck (mvInfo mv) == DontRunMetaOccursCheck)
then return Data.Set.empty
else maybe (return Data.Set.empty) lookupMutualBlock =<< asks envMutualBlock
defNeedsChecking :: QName -> TCM Bool
defNeedsChecking d = Data.Set.member d <$> gets stOccursCheckDefs
tallyDef :: QName -> TCM ()
tallyDef d = modifyOccursCheckDefs $ \ s -> Data.Set.delete d s
data OccursCtx
= Flex
| Rigid
| StronglyRigid
| Top
| Irrel
deriving (Eq, Show)
data UnfoldStrategy = YesUnfold | NoUnfold
deriving (Eq, Show)
defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx
defArgs NoUnfold _ = Flex
defArgs YesUnfold ctx = weakly ctx
unfold :: UnfoldStrategy -> Term -> TCM (Blocked Term)
unfold NoUnfold v = NotBlocked <$> instantiate v
unfold YesUnfold v = reduceB v
leaveTop :: OccursCtx -> OccursCtx
leaveTop Top = StronglyRigid
leaveTop ctx = ctx
weakly :: OccursCtx -> OccursCtx
weakly Top = Rigid
weakly StronglyRigid = Rigid
weakly ctx = ctx
strongly :: OccursCtx -> OccursCtx
strongly Rigid = StronglyRigid
strongly ctx = ctx
abort :: OccursCtx -> TypeError -> TCM a
abort Top err = typeError err
abort StronglyRigid err = typeError err
abort Flex _ = patternViolation
abort Rigid _ = patternViolation
abort Irrel _ = patternViolation
type Vars = ([Nat],[Nat])
goIrrelevant :: Vars -> Vars
goIrrelevant (relVs, irrVs) = (irrVs ++ relVs, [])
allowedVar :: Nat -> Vars -> Bool
allowedVar i (relVs, irrVs) = i `elem` relVs
takeRelevant :: Vars -> [Nat]
takeRelevant = fst
liftUnderAbs :: Vars -> Vars
liftUnderAbs (relVs, irrVs) = (0 : map (1+) relVs, map (1+) irrVs)
class Occurs t where
occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> t -> TCM t
metaOccurs :: MetaId -> t -> TCM ()
occursCheck :: MetaId -> Vars -> Term -> TCM Term
occursCheck m xs v = liftTCM $ do
mv <- lookupMeta m
initOccursCheck mv
let redo m = m
redo (occurs NoUnfold Top m xs v) `catchError` \_ -> do
initOccursCheck mv
redo (occurs YesUnfold Top m xs v) `catchError` \err -> case err of
TypeError _ cl -> case clValue cl of
MetaOccursInItself{} ->
typeError . GenericError . show =<<
fsep [ text ("Refuse to construct infinite term by instantiating " ++ show m ++ " to")
, prettyTCM =<< instantiateFull v
]
MetaCannotDependOn _ _ i ->
ifM ((&&) <$> isSortMeta m <*> (not <$> hasUniversePolymorphism))
( typeError . GenericError . show =<<
fsep [ text ("Cannot instantiate the metavariable " ++ show m ++ " to")
, prettyTCM v
, text "since universe polymorphism is disabled"
]
)
( typeError . GenericError . show =<<
fsep [ text ("Cannot instantiate the metavariable " ++ show m ++ " to solution")
, prettyTCM v
, text "since it contains the variable"
, enterClosure cl $ \_ -> prettyTCM (Var i [])
, text $ "which is not in scope of the metavariable or irrelevant in the metavariable but relevant in the solution"
]
)
_ -> throwError err
_ -> throwError err
instance Occurs Term where
occurs red ctx m xs v = do
v <- unfold red v
case v of
Blocked _ v -> occurs' Flex v
NotBlocked v -> occurs' ctx v
where
occurs' ctx v = case v of
Var i vs -> do
if (i `allowedVar` xs) then Var i <$> occ (weakly ctx) vs else do
isST <- isSingletonType =<< typeOfBV i
case isST of
Left mid -> patternViolation
Right Nothing ->
abort (strongly ctx) $ MetaCannotDependOn m (takeRelevant xs) i
Right (Just sv) -> return $ sv `apply` vs
Lam h f -> Lam h <$> occ (leaveTop ctx) f
Level l -> Level <$> occ ctx l
Lit l -> return v
DontCare v -> DontCare <$> occurs red Irrel m (goIrrelevant xs) v
Def d vs -> Def d <$> occDef d (leaveTop ctx) vs
Con c vs -> Con c <$> occ (leaveTop ctx) vs
Pi a b -> uncurry Pi <$> occ (leaveTop ctx) (a,b)
Sort s -> Sort <$> occ (leaveTop ctx) s
v@Shared{} -> updateSharedTerm (occ ctx) v
MetaV m' vs -> do
when (m == m') $ if ctx == Top then patternViolation else
abort ctx $ MetaOccursInItself m'
(MetaV m' <$> occurs red Flex m xs vs) `catchError` \err -> do
reportSDoc "tc.meta.kill" 25 $ vcat
[ text $ "error during flexible occurs check, we are " ++ show ctx
, text $ show err
]
case err of
PatternErr{} | ctx /= Flex -> do
reportSLn "tc.meta.kill" 20 $
"oops, pattern violation for " ++ show m'
killResult <- prune m' vs (takeRelevant xs)
if (killResult == PrunedEverything)
then occurs red ctx m xs =<< instantiate (MetaV m' vs)
else throwError err
_ -> throwError err
where
occ ctx v = occurs red ctx m xs v
occDef d ctx vs = do
def <- theDef <$> getConstInfo d
whenM (defNeedsChecking d) $ do
tallyDef d
metaOccurs m def
if (defIsDataOrRecord def) then (occ ctx vs) else (occ (defArgs red ctx) vs)
metaOccurs m v = do
v <- instantiate v
case v of
Var i vs -> metaOccurs m vs
Lam h f -> metaOccurs m f
Level l -> metaOccurs m l
Lit l -> return ()
DontCare v -> metaOccurs m v
Def d vs -> metaOccurs m d >> metaOccurs m vs
Con c vs -> metaOccurs m vs
Pi a b -> metaOccurs m (a,b)
Sort s -> metaOccurs m s
Shared p -> metaOccurs m $ derefPtr p
MetaV m' vs | m == m' -> patternViolation
| otherwise -> metaOccurs m vs
instance Occurs QName where
occurs red ctx m xs d = __IMPOSSIBLE__
metaOccurs m d = whenM (defNeedsChecking d) $ do
tallyDef d
metaOccurs m . theDef =<< getConstInfo d
instance Occurs Defn where
occurs red ctx m xs def = __IMPOSSIBLE__
metaOccurs m Axiom{} = return ()
metaOccurs m Function{ funClauses = cls } = metaOccurs m cls
metaOccurs m Datatype{ dataCons = cs } = mapM_ mocc cs
where mocc c = metaOccurs m . defType =<< getConstInfo c
metaOccurs m Record{ recConType = v } = metaOccurs m v
metaOccurs m Constructor{} = return ()
metaOccurs m Primitive{} = return ()
instance Occurs Clause where
occurs red ctx m xs cl = __IMPOSSIBLE__
metaOccurs m (Clause { clauseBody = body }) = walk body
where walk NoBody = return ()
walk (Body v) = metaOccurs m v
walk (Bind b) = underAbstraction_ b walk
instance Occurs Level where
occurs red ctx m xs (Max as) = Max <$> occurs red ctx m xs as
metaOccurs m (Max as) = metaOccurs m as
instance Occurs PlusLevel where
occurs red ctx m xs l@ClosedLevel{} = return l
occurs red ctx m xs (Plus n l) = Plus n <$> occurs red ctx' m xs l
where ctx' | n == 0 = ctx
| otherwise = leaveTop ctx
metaOccurs m ClosedLevel{} = return ()
metaOccurs m (Plus n l) = metaOccurs m l
instance Occurs LevelAtom where
occurs red ctx m xs l = do
l <- case red of
YesUnfold -> reduce l
NoUnfold -> instantiate l
case l of
MetaLevel m' args -> do
MetaV m' args <- ignoreSharing <$> occurs red ctx m xs (MetaV m' args)
return $ MetaLevel m' args
NeutralLevel v -> NeutralLevel <$> occurs red ctx m xs v
BlockedLevel m v -> BlockedLevel m <$> occurs red Flex m xs v
UnreducedLevel v -> UnreducedLevel <$> occurs red ctx m xs v
metaOccurs m l = do
l <- instantiate l
case l of
MetaLevel m' args -> metaOccurs m (MetaV m' args)
NeutralLevel v -> metaOccurs m v
BlockedLevel m v -> metaOccurs m v
UnreducedLevel v -> metaOccurs m v
instance Occurs Type where
occurs red ctx m xs (El s v) = uncurry El <$> occurs red ctx m xs (s,v)
metaOccurs m (El s v) = metaOccurs m (s,v)
instance Occurs Sort where
occurs red ctx m xs s = do
s' <- case red of
YesUnfold -> reduce s
NoUnfold -> instantiate s
case s' of
DLub s1 s2 -> uncurry DLub <$> occurs red (weakly ctx) m xs (s1,s2)
Type a -> Type <$> occurs red ctx m xs a
Prop -> return s'
Inf -> return s'
metaOccurs m s = do
s <- instantiate s
case s of
DLub s1 s2 -> metaOccurs m (s1,s2)
Type a -> metaOccurs m a
Prop -> return ()
Inf -> return ()
instance (Occurs a, Subst a) => Occurs (Abs a) where
occurs red ctx m xs b@(Abs s x) = Abs s <$> underAbstraction_ b (occurs red ctx m (liftUnderAbs xs))
occurs red ctx m xs b@(NoAbs s x) = NoAbs s <$> occurs red ctx m xs x
metaOccurs m (Abs s x) = metaOccurs m x
metaOccurs m (NoAbs s x) = metaOccurs m x
instance Occurs a => Occurs (Arg a) where
occurs red ctx m xs (Arg h r@Irrelevant{} x) = Arg h r <$>
occurs red Irrel m (goIrrelevant xs) x
occurs red ctx m xs (Arg h r x) = Arg h r <$>
occurs red ctx m xs x
metaOccurs m a = metaOccurs m (unArg a)
instance Occurs a => Occurs (Dom a) where
occurs red ctx m xs (Dom h r x) = Dom h r <$> occurs red ctx m xs x
metaOccurs m = metaOccurs m . unDom
instance (Occurs a, Occurs b) => Occurs (a,b) where
occurs red ctx m xs (x,y) = (,) <$> occurs red ctx m xs x <*> occurs red ctx m xs y
metaOccurs m (x,y) = metaOccurs m x >> metaOccurs m y
instance Occurs a => Occurs [a] where
occurs red ctx m xs ys = mapM (occurs red ctx m xs) ys
metaOccurs m ys = mapM_ (metaOccurs m) ys
prune :: MetaId -> Args -> [Nat] -> TCM PruneResult
prune m' vs xs = liftTCM $ do
kills <- mapM (hasBadRigid xs) $ map unArg vs
reportSDoc "tc.meta.kill" 10 $ vcat
[ text "attempting kills"
, nest 2 $ vcat
[ text "m' =" <+> text (show m')
, text "xs =" <+> text (show xs)
, text "vs =" <+> prettyList (map prettyTCM vs)
, text "kills =" <+> text (show kills)
]
]
killArgs kills m'
hasBadRigid :: [Nat] -> Term -> TCM Bool
hasBadRigid xs (Var x _) = return $ notElem x xs
hasBadRigid xs (Lam _ v) = hasBadRigid (0 : map (+1) xs) (absBody v)
hasBadRigid xs (DontCare v) = hasBadRigid xs v
hasBadRigid xs v@(Def f vs) =
ifM (isJust <$> isDataOrRecordType f) (return $ vs `rigidVarsNotContainedIn` xs) $ do
elV <- elimView v
case elV of
VarElim x els -> return $ notElem x xs
_ -> return $ False
hasBadRigid xs (Pi a b) = return $ (a,b) `rigidVarsNotContainedIn` xs
hasBadRigid xs (Level v) = return $ v `rigidVarsNotContainedIn` xs
hasBadRigid xs (Sort s) = return $ s `rigidVarsNotContainedIn` xs
hasBadRigid xs Con{} = return $ False
hasBadRigid xs Lit{} = return $ False
hasBadRigid xs MetaV{} = return $ False
hasBadRigid xs (Shared p) = hasBadRigid xs (derefPtr p)
rigidVarsNotContainedIn :: Free a => a -> [Nat] -> Bool
rigidVarsNotContainedIn v xs =
not $ Set.isSubsetOf
(rigidVars $ freeVars v)
(Set.fromList xs)
data PruneResult
= NothingToPrune
| PrunedNothing
| PrunedSomething
| PrunedEverything
deriving (Eq, Show)
killArgs :: [Bool] -> MetaId -> TCM PruneResult
killArgs kills _
| not (or kills) = return NothingToPrune
killArgs kills m = do
mv <- lookupMeta m
if mvFrozen mv == Frozen then return PrunedNothing else do
let a = jMetaType $ mvJudgement mv
TelV tel b <- telView' <$> instantiateFull a
let args = zip (telToList tel) (kills ++ repeat False)
(kills', a') = killedType args b
dbg kills' a a'
if not (any unArg kills') then return PrunedNothing else do
performKill (reverse kills') m a'
return $ if (and $ zipWith implies kills $ map unArg kills')
then PrunedEverything
else PrunedSomething
where
implies :: Bool -> Bool -> Bool
implies False _ = True
implies True x = x
dbg kills' a a' =
reportSDoc "tc.meta.kill" 10 $ vcat
[ text "after kill analysis"
, nest 2 $ vcat
[ text "metavar =" <+> prettyTCM m
, text "kills =" <+> text (show kills)
, text "kills' =" <+> text (show kills')
, text "oldType =" <+> prettyTCM a
, text "newType =" <+> prettyTCM a'
]
]
killedType :: [(Dom (String, Type), Bool)] -> Type -> ([Arg Bool], Type)
killedType [] b = ([], b)
killedType ((arg@(Dom h r _), kill) : kills) b
| dontKill = (Arg h r False : args, mkPi arg b')
| otherwise = (Arg h r True : args, subst __IMPOSSIBLE__ b')
where
(args, b') = killedType kills b
dontKill = not kill || 0 `freeIn` b'
performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()
performKill kills m a = do
mv <- lookupMeta m
when (mvFrozen mv == Frozen) __IMPOSSIBLE__
let perm = Perm (size kills)
[ i | (i, Arg _ _ False) <- zip [0..] (reverse kills) ]
m' <- newMeta (mvInfo mv) (mvPriority mv) perm
(HasType __IMPOSSIBLE__ a)
etaExpandMetaSafe m'
let vars = reverse [ Arg h r (var i) | (i, Arg h r False) <- zip [0..] kills ]
lam b a = Lam (argHiding a) (Abs "v" b)
u = foldl' lam (MetaV m' vars) kills
dbg m' u
assignTerm m u
where
dbg m' u = reportSDoc "tc.meta.kill" 10 $ vcat
[ text "actual killing"
, nest 2 $ vcat
[ text "new meta:" <+> text (show m')
, text "kills :" <+> text (show kills)
, text "inst :" <+> text (show m) <+> text ":=" <+> prettyTCM u
]
]