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 as Set
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
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.Records
import Agda.TypeChecking.Datatypes (isDataOrRecordType)
import Agda.TypeChecking.MetaVars
import Agda.Utils.Either
import Agda.Utils.List (takeWhileJust)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
import qualified Agda.Utils.VarSet as VarSet
#include "../../undefined.h"
import Agda.Utils.Impossible
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 Set.empty
else maybe (return Set.empty) lookupMutualBlock =<< asks envMutualBlock
defNeedsChecking :: QName -> TCM Bool
defNeedsChecking d = Set.member d <$> gets stOccursCheckDefs
tallyDef :: QName -> TCM ()
tallyDef d = modifyOccursCheckDefs $ \ s -> 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
patternViolation' :: Int -> String -> TCM a
patternViolation' n err = do
reportSLn "tc.meta.occurs" n err
patternViolation
abort :: OccursCtx -> TypeError -> TCM a
abort Top err = typeError err
abort StronglyRigid err = typeError err
abort Flex err = patternViolation' 70 (show err)
abort Rigid err = patternViolation' 70 (show err)
abort Irrel err = patternViolation' 70 (show err)
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 `and2M` (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
NotBlocked v -> occurs' ctx v
Blocked _ v -> occurs' Flex v
where
occurs' ctx v = do
reportSDoc "tc.meta.occurs" 45 $
text ("occursCheck " ++ show m ++ " (" ++ show ctx ++ ") of ") <+> prettyTCM v
reportSDoc "tc.meta.occurs" 70 $
nest 2 $ text $ show v
case v of
Var i es -> do
if (i `allowedVar` xs) then Var i <$> occ (weakly ctx) es else do
isST <- isSingletonType =<< typeOfBV i
case isST of
Left mid -> patternViolation' 70 $ "Disallowed var " ++ show i ++ " not obviously singleton"
Right Nothing ->
abort (strongly ctx) $ MetaCannotDependOn m (takeRelevant xs) i
Right (Just sv) -> return $ sv `applyE` es
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 es -> Def d <$> occDef d (leaveTop ctx) es
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' es -> do
when (m == m') $ patternViolation' 50 $ "occursCheck failed: Found " ++ show m
(MetaV m' <$> occurs red Flex m xs es) `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'
caseMaybe (allApplyElims es) (throwError err) $ \ vs -> do
killResult <- prune m' vs (takeRelevant xs)
if (killResult == PrunedEverything)
then occurs red ctx m xs =<< instantiate (MetaV m' es)
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
reportSLn "tc.meta.occurs" 30 $ "Checking for occurrences in " ++ show 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' 50 $ "Found occurrence of " ++ show m
| otherwise -> metaOccurs m vs
instance Occurs QName where
occurs red ctx m xs d = __IMPOSSIBLE__
metaOccurs m d = whenM (defNeedsChecking d) $ do
tallyDef d
reportSLn "tc.meta.occurs" 30 $ "Checking for occurrences in " ++ show 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 => Occurs (Elim' a) where
occurs red ctx m xs e@Proj{} = return e
occurs red ctx m xs (Apply a) = Apply <$> occurs red ctx m xs a
metaOccurs m (Proj{} ) = return ()
metaOccurs m (Apply a) = metaOccurs m a
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 (I.Arg a) where
occurs red ctx m xs (Arg info x) | isIrrelevant info = Arg info <$>
occurs red Irrel m (goIrrelevant xs) x
occurs red ctx m xs (Arg info x) = Arg info <$>
occurs red ctx m xs x
metaOccurs m a = metaOccurs m (unArg a)
instance Occurs a => Occurs (I.Dom a) where
occurs red ctx m xs (Dom info x) = Dom info <$> 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 = do
caseEitherM (runErrorT $ mapM (hasBadRigid xs) $ map unArg vs)
(const $ return PrunedNothing) $ \ kills -> do
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 -> ErrorT () TCM Bool
hasBadRigid xs t = do
let failure = throwError ()
t <- liftTCM $ reduce t
case ignoreSharing t of
(Var x _) -> return $ notElem x xs
(Lam _ v) -> failure
(DontCare v) -> hasBadRigid xs v
v@(Def f es) -> ifNotM (isNeutral f es) failure $ do
return $ es `rigidVarsNotContainedIn` xs
(Pi a b) -> return $ (a,b) `rigidVarsNotContainedIn` xs
(Level v) -> return $ v `rigidVarsNotContainedIn` xs
(Sort s) -> return $ s `rigidVarsNotContainedIn` xs
(Con c args) -> do
ifM (liftTCM $ isEtaCon (conName c))
(and <$> mapM (hasBadRigid xs . unArg) args)
failure
Lit{} -> failure
MetaV{} -> failure
(Shared p) -> __IMPOSSIBLE__
isNeutral :: MonadTCM tcm => QName -> Elims -> tcm Bool
isNeutral f es = liftTCM $ do
let yes = return True
def <- getConstInfo f
case theDef def of
Axiom{} -> yes
Datatype{} -> yes
Record{} -> yes
_ -> return False
rigidVarsNotContainedIn :: Free a => a -> [Nat] -> Bool
rigidVarsNotContainedIn v xs =
not $ rigidVars (freeVars v) `VarSet.isSubsetOf` VarSet.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
allowAssign <- asks envAssignMetas
if mvFrozen mv == Frozen || not allowAssign 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 :: [(I.Dom (ArgName, Type), Bool)] -> Type -> ([I.Arg Bool], Type)
killedType [] b = ([], b)
killedType ((arg@(Dom info _), kill) : kills) b
| dontKill = (Arg info False : args, mkPi arg b')
| otherwise = (Arg info True : args, subst __IMPOSSIBLE__ b')
where
(args, b') = killedType kills b
dontKill = not kill || 0 `freeIn` b'
performKill :: [I.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 info (var i) | (i, Arg info False) <- zip [0..] kills ]
lam b a = Lam (argInfo a) (Abs "v" b)
u = foldl' lam (MetaV m' $ map Apply 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
]
]