module Agda.TypeChecking.MetaVars.Occurs where
import Control.Applicative
import Control.Monad
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.MetaVars
import Agda.Utils.Either
import Agda.Utils.Except
( ExceptT
, MonadError(catchError, throwError)
, runExceptT
)
import Agda.Utils.Lens
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 = stOccursCheckDefs %= f
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 <$> use 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
ExtLam{} -> __IMPOSSIBLE__
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
ExtLam{} -> __IMPOSSIBLE__
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 (runExceptT $ 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 -> ExceptT () 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__
ExtLam{} -> __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, strengthen __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)
tel = map ("v" <$) (reverse kills)
u = MetaV m' $ map Apply vars
dbg m' u
assignTerm m tel 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
]
]