{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE GADTs #-}
module Agda.TypeChecking.MetaVars where
import Prelude hiding (null)
import Control.Monad.Reader
import Data.Function
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Foldable as Fold
import qualified Data.Traversable as Trav
import Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.Syntax.Position (killRange)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Free
import Agda.TypeChecking.Level
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.SizedTypes (boundedSizeMetaHook, isSizeProblem)
import {-# SOURCE #-} Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.MetaVars.Occurs
import Agda.Utils.Except
( ExceptT
, MonadError(throwError)
, runExceptT
)
import Agda.Utils.Function
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Permutation
import Agda.Utils.Pretty ( prettyShow, render )
import qualified Agda.Utils.VarSet as Set
#include "undefined.h"
import Agda.Utils.Impossible
findIdx :: Eq a => [a] -> a -> Maybe Int
findIdx vs v = List.findIndex (==v) (reverse vs)
isBlockedTerm :: MetaId -> TCM Bool
isBlockedTerm x = do
reportSLn "tc.meta.blocked" 12 $ "is " ++ prettyShow x ++ " a blocked term? "
i <- mvInstantiation <$> lookupMeta x
let r = case i of
BlockedConst{} -> True
PostponedTypeCheckingProblem{} -> True
InstV{} -> False
Open{} -> False
OpenIFS{} -> False
reportSLn "tc.meta.blocked" 12 $
if r then " yes, because " ++ show i else " no"
return r
isEtaExpandable :: [MetaKind] -> MetaId -> TCM Bool
isEtaExpandable kinds x = do
i <- mvInstantiation <$> lookupMeta x
return $ case i of
Open{} -> True
OpenIFS{} -> notElem Records kinds
InstV{} -> False
BlockedConst{} -> False
PostponedTypeCheckingProblem{} -> False
assignTerm :: MetaId -> [Arg ArgName] -> Term -> TCM ()
assignTerm x tel v = do
whenM (isFrozen x) __IMPOSSIBLE__
assignTerm' x tel v
assignTerm' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
assignTerm' x tel v = do
reportSLn "tc.meta.assign" 70 $ prettyShow x ++ " := " ++ show v ++ "\n in " ++ show tel
whenM (not <$> asks envAssignMetas) __IMPOSSIBLE__
verboseS "profile.metas" 10 $ liftTCM $ tickMax "max-open-metas" . (fromIntegral . size) =<< getOpenMetas
modifyMetaStore $ ins x $ InstV tel $ killRange v
etaExpandListeners x
wakeupConstraints x
reportSLn "tc.meta.assign" 20 $ "completed assignment of " ++ prettyShow x
where
ins x i = Map.adjust (\ mv -> mv { mvInstantiation = i }) x
newSortMetaBelowInf :: TCM Sort
newSortMetaBelowInf = do
x <- newSortMeta
hasBiggerSort x
return x
newSortMeta :: TCM Sort
newSortMeta = newSortMeta' $ IsSort ()
newSortMeta' :: (Type -> Judgement ()) -> TCM Sort
newSortMeta' judge =
ifM typeInType (return $ mkType 0) $
ifM hasUniversePolymorphism (newSortMetaCtx' judge =<< getContextArgs)
$ do i <- createMetaInfo
x <- newMeta i normalMetaPriority (idP 0) $ judge typeDontCare
return $ MetaS x []
newSortMetaCtx :: Args -> TCM Sort
newSortMetaCtx = newSortMetaCtx' $ IsSort ()
newSortMetaCtx' :: (Type -> Judgement ()) -> Args -> TCM Sort
newSortMetaCtx' judge vs = do
ifM typeInType (return $ mkType 0) $ do
i <- createMetaInfo
tel <- getContextTelescope
let t = telePi_ tel typeDontCare
x <- newMeta i normalMetaPriority (idP 0) $ judge t
reportSDoc "tc.meta.new" 50 $
text "new sort meta" <+> prettyTCM x <+> text ":" <+> prettyTCM t
return $ MetaS x $ map Apply vs
newTypeMeta :: Sort -> TCM Type
newTypeMeta s = El s . snd <$> newValueMeta RunMetaOccursCheck (sort s)
newTypeMeta_ :: TCM Type
newTypeMeta_ = newTypeMeta =<< (workOnTypes $ newSortMeta)
newIFSMeta :: MetaNameSuggestion -> Type -> TCM (MetaId, Term)
newIFSMeta s t = do
vs <- getContextArgs
ctx <- getContextTelescope
newIFSMetaCtx s (telePi_ ctx t) vs
newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> TCM (MetaId, Term)
newIFSMetaCtx s t vs = do
reportSDoc "tc.meta.new" 50 $ fsep
[ text "new ifs meta:"
, nest 2 $ prettyTCM vs <+> text "|-"
]
i0 <- createMetaInfo' DontRunMetaOccursCheck
let i = i0 { miNameSuggestion = s }
TelV tel _ <- telView t
let perm = idP (size tel)
x <- newMeta' OpenIFS i normalMetaPriority perm (HasType () t)
reportSDoc "tc.meta.new" 50 $ fsep
[ nest 2 $ pretty x <+> text ":" <+> prettyTCM t
]
let c = FindInScope x Nothing Nothing
ifM isSolvingConstraints (addConstraint c) (addAwakeConstraint' c)
etaExpandMetaSafe x
return (x, MetaV x $ map Apply vs)
newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM (MetaId, Term)
newNamedValueMeta b s t = do
(x, v) <- newValueMeta b t
setMetaNameSuggestion x s
return (x, v)
newNamedValueMeta' :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM (MetaId, Term)
newNamedValueMeta' b s t = do
(x, v) <- newValueMeta' b t
setMetaNameSuggestion x s
return (x, v)
newValueMeta :: RunMetaOccursCheck -> Type -> TCM (MetaId, Term)
newValueMeta b t = do
vs <- getContextArgs
tel <- getContextTelescope
newValueMetaCtx b t tel (idP $ size tel) vs
newValueMetaCtx :: RunMetaOccursCheck -> Type -> Telescope -> Permutation -> Args -> TCM (MetaId, Term)
newValueMetaCtx b t tel perm ctx =
mapSndM instantiateFull =<< newValueMetaCtx' b t tel perm ctx
newValueMeta' :: RunMetaOccursCheck -> Type -> TCM (MetaId, Term)
newValueMeta' b t = do
vs <- getContextArgs
tel <- getContextTelescope
newValueMetaCtx' b t tel (idP $ size tel) vs
newValueMetaCtx' :: RunMetaOccursCheck -> Type -> Telescope -> Permutation -> Args -> TCM (MetaId, Term)
newValueMetaCtx' b a tel perm vs = do
i <- createMetaInfo' b
let t = telePi_ tel a
x <- newMeta i normalMetaPriority perm (HasType () t)
reportSDoc "tc.meta.new" 50 $ fsep
[ text "new meta:"
, nest 2 $ prettyTCM vs <+> text "|-"
, nest 2 $ pretty x <+> text ":" <+> prettyTCM t
]
etaExpandMetaSafe x
let u = MetaV x $ map Apply vs
boundedSizeMetaHook u tel a
return (x, u)
newTelMeta :: Telescope -> TCM Args
newTelMeta tel = newArgsMeta (abstract tel $ typeDontCare)
type Condition = Dom Type -> Abs Type -> Bool
trueCondition :: Condition
trueCondition _ _ = True
newArgsMeta :: Type -> TCM Args
newArgsMeta = newArgsMeta' trueCondition
newArgsMeta' :: Condition -> Type -> TCM Args
newArgsMeta' condition t = do
args <- getContextArgs
tel <- getContextTelescope
newArgsMetaCtx' condition t tel (idP $ size tel) args
newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args
newArgsMetaCtx = newArgsMetaCtx' trueCondition
newArgsMetaCtx' :: Condition -> Type -> Telescope -> Permutation -> Args -> TCM Args
newArgsMetaCtx' condition (El s tm) tel perm ctx = do
tm <- reduce tm
case tm of
Pi dom@(Dom info a) codom | condition dom codom -> do
let r = getRelevance info
tel' = telFromList . map (inverseApplyRelevance r) . telToList $ tel
ctx' = (map . mapRelevance) (r `inverseComposeRelevance`) ctx
(_, u) <- applyRelevanceToContext (getRelevance info) $
newValueMetaCtx RunMetaOccursCheck a tel' perm ctx'
args <- newArgsMetaCtx' condition (codom `absApp` u) tel perm ctx
return $ Arg info u : args
_ -> return []
newRecordMeta :: QName -> Args -> TCM Term
newRecordMeta r pars = do
args <- getContextArgs
tel <- getContextTelescope
newRecordMetaCtx r pars tel (idP $ size tel) args
newRecordMetaCtx :: QName -> Args -> Telescope -> Permutation -> Args -> TCM Term
newRecordMetaCtx r pars tel perm ctx = do
ftel <- flip apply pars <$> getRecordFieldTypes r
fields <- newArgsMetaCtx (telePi_ ftel $ sort Prop) tel perm ctx
con <- getRecordConstructor r
return $ Con con ConOSystem (map Apply fields)
newQuestionMark :: InteractionId -> Type -> TCM (MetaId, Term)
newQuestionMark = newQuestionMark' $ newValueMeta' RunMetaOccursCheck
newQuestionMark' :: (Type -> TCM (MetaId, Term)) -> InteractionId -> Type -> TCM (MetaId, Term)
newQuestionMark' new ii t = do
let existing x = (x,) . MetaV x . map Apply <$> getContextArgs
flip (caseMaybeM $ lookupInteractionMeta ii) existing $ do
(x, m) <- new t
connectInteractionPoint ii x
return (x, m)
blockTerm :: Type -> TCM Term -> TCM Term
blockTerm t blocker = do
(pid, v) <- newProblem blocker
blockTermOnProblem t v pid
blockTermOnProblem :: Type -> Term -> ProblemId -> TCM Term
blockTermOnProblem t v pid =
ifM (isProblemSolved pid `or2M` isSizeProblem pid) (return v) $ do
i <- createMetaInfo
es <- map Apply <$> getContextArgs
tel <- getContextTelescope
x <- newMeta' (BlockedConst $ abstract tel v)
i lowMetaPriority (idP $ size tel)
(HasType () $ telePi_ tel t)
inTopContext $ addConstraint (Guarded (UnBlock x) pid)
reportSDoc "tc.meta.blocked" 20 $ vcat
[ text "blocked" <+> prettyTCM x <+> text ":=" <+> inTopContext (prettyTCM $ abstract tel v)
, text " by" <+> (prettyTCM =<< getConstraintsForProblem pid) ]
inst <- isInstantiatedMeta x
case inst of
True -> instantiate (MetaV x es)
False -> do
(_, v) <- newValueMeta DontRunMetaOccursCheck t
i <- liftTCM fresh
cmp <- buildProblemConstraint_ (ValueCmp CmpEq t v (MetaV x es))
listenToMeta (CheckConstraint i cmp) x
return v
blockTypeOnProblem :: Type -> ProblemId -> TCM Type
blockTypeOnProblem (El s a) pid = El s <$> blockTermOnProblem (El Inf $ Sort s) a pid
unblockedTester :: Type -> TCM Bool
unblockedTester t = ifBlockedType t (\ m t -> return False) (\ _ t -> return True)
postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ p = do
postponeTypeCheckingProblem p (unblock p)
where
unblock (CheckExpr _ t) = unblockedTester t
unblock (CheckArgs _ _ _ t _ _) = unblockedTester t
unblock (CheckLambda _ _ t) = unblockedTester t
unblock (UnquoteTactic _ _ _) = __IMPOSSIBLE__
postponeTypeCheckingProblem :: TypeCheckingProblem -> TCM Bool -> TCM Term
postponeTypeCheckingProblem p unblock = do
i <- createMetaInfo' DontRunMetaOccursCheck
tel <- getContextTelescope
cl <- buildClosure p
t <- problemType p
m <- newMeta' (PostponedTypeCheckingProblem cl unblock)
i normalMetaPriority (idP (size tel))
$ HasType () $ telePi_ tel t
es <- map Apply <$> getContextArgs
(_, v) <- newValueMeta DontRunMetaOccursCheck t
cmp <- buildProblemConstraint_ (ValueCmp CmpEq t v (MetaV m es))
i <- liftTCM fresh
listenToMeta (CheckConstraint i cmp) m
addConstraint (UnBlock m)
return v
problemType :: TypeCheckingProblem -> TCM Type
problemType (CheckExpr _ t ) = return t
problemType (CheckArgs _ _ _ _ t _ ) = return t
problemType (CheckLambda _ _ t ) = return t
problemType (UnquoteTactic tac hole t) = return t
etaExpandListeners :: MetaId -> TCM ()
etaExpandListeners m = do
ls <- getMetaListeners m
clearMetaListeners m
mapM_ wakeupListener ls
wakeupListener :: Listener -> TCM ()
wakeupListener (EtaExpand x) = etaExpandMetaSafe x
wakeupListener (CheckConstraint _ c) = do
reportSDoc "tc.meta.blocked" 20 $ text "waking boxed constraint" <+> prettyTCM c
addAwakeConstraints [c]
solveAwakeConstraints
etaExpandMetaSafe :: MetaId -> TCM ()
etaExpandMetaSafe = etaExpandMeta [SingletonRecords,Levels]
data MetaKind =
Records
| SingletonRecords
| Levels
deriving (Eq, Enum, Bounded, Show)
allMetaKinds :: [MetaKind]
allMetaKinds = [minBound .. maxBound]
etaExpandMeta :: [MetaKind] -> MetaId -> TCM ()
etaExpandMeta kinds m = whenM (asks envAssignMetas `and2M` isEtaExpandable kinds m) $ do
verboseBracket "tc.meta.eta" 20 ("etaExpandMeta " ++ prettyShow m) $ do
let waitFor x = do
reportSDoc "tc.meta.eta" 20 $ do
text "postponing eta-expansion of meta variable" <+>
prettyTCM m <+>
text "which is blocked by" <+> prettyTCM x
listenToMeta (EtaExpand m) x
dontExpand = do
reportSDoc "tc.meta.eta" 20 $ do
text "we do not expand meta variable" <+> prettyTCM m <+>
text ("(requested was expansion of " ++ show kinds ++ ")")
meta <- lookupMeta m
case mvJudgement meta of
IsSort{} -> dontExpand
HasType _ a -> do
TelV tel b <- telView a
ifBlocked (unEl b) (\ x _ -> waitFor x) $ \ _ t -> case t of
lvl@(Def r es) ->
ifM (isEtaRecord r) (do
let ps = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
let expand = do
u <- withMetaInfo' meta $ newRecordMetaCtx r ps tel (idP $ size tel) $ teleArgs tel
inTopContext $ do
verboseS "tc.meta.eta" 15 $ do
du <- prettyTCM u
reportSDoc "tc.meta.eta" 15 $ sep
[ text "eta expanding: " <+> pretty m <+> text " --> "
, nest 2 $ prettyTCM u
]
noConstraints $ assignTerm' m (telToArgs tel) u
if Records `elem` kinds then
expand
else if (SingletonRecords `elem` kinds) then do
singleton <- isSingletonRecord r ps
case singleton of
Left x -> waitFor x
Right False -> dontExpand
Right True -> expand
else dontExpand
) $ ifM (andM [ return $ Levels `elem` kinds
, typeInType
, (Just lvl ==) <$> getBuiltin' builtinLevel
]) (do
reportSLn "tc.meta.eta" 20 $ "Expanding level meta to 0 (type-in-type)"
noConstraints $ assignTerm m (telToArgs tel) (Level $ Max [])
) $ dontExpand
_ -> dontExpand
etaExpandBlocked :: Reduce t => Blocked t -> TCM (Blocked t)
etaExpandBlocked t@NotBlocked{} = return t
etaExpandBlocked (Blocked m t) = do
etaExpandMeta [Records] m
t <- reduceB t
case t of
Blocked m' _ | m /= m' -> etaExpandBlocked t
_ -> return t
assignV :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
assignV dir x args v = assignWrapper dir x (map Apply args) v $ assign dir x args v
assignWrapper :: CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM ()
assignWrapper dir x es v doAssign = do
ifNotM (asks envAssignMetas) patternViolation $ do
reportSDoc "tc.meta.assign" 10 $ do
text "term" <+> prettyTCM (MetaV x es) <+> text (":" ++ show dir) <+> prettyTCM v
liftTCM $ nowSolvingConstraints doAssign `finally` solveAwakeConstraints
assign :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
assign dir x args v = do
mvar <- lookupMeta x
let t = jMetaType $ mvJudgement mvar
v <- instantiate v
reportSDoc "tc.meta.assign" 45 $
text "MetaVars.assign: assigning to " <+> prettyTCM v
reportSLn "tc.meta.assign" 75 $
"MetaVars.assign: assigning meta " ++ show x ++ " with args " ++ show args ++ " to " ++ show v
case (v, mvJudgement mvar) of
(Sort Inf, HasType{}) -> typeError SetOmegaNotValidType
_ -> return ()
when (mvFrozen mvar == Frozen) $ do
reportSLn "tc.meta.assign" 25 $ "aborting: meta is frozen!"
patternViolation
whenM (isBlockedTerm x) patternViolation
reportSLn "tc.meta.assign" 50 $ "MetaVars.assign: I want to see whether rhs is blocked"
reportSDoc "tc.meta.assign" 25 $ do
v0 <- reduceB v
case v0 of
Blocked m0 _ -> text "r.h.s. blocked on:" <+> prettyTCM m0
NotBlocked{} -> text "r.h.s. not blocked"
subtypingForSizeLt dir x mvar t args v $ \ v -> do
reportSDoc "tc.meta.assign.proj" 45 $ do
cxt <- getContextTelescope
vcat
[ text "context before projection expansion"
, nest 2 $ inTopContext $ prettyTCM cxt
]
expandProjectedVars args v $ \ args v -> do
reportSDoc "tc.meta.assign.proj" 45 $ do
cxt <- getContextTelescope
vcat
[ text "context after projection expansion"
, nest 2 $ inTopContext $ prettyTCM cxt
]
(relVL, nonstrictVL, irrVL) <- do
if False
then do
reportSDoc "tc.meta.assign" 25 $ text "meta is irrelevant or unused"
return (Set.toList $ allFreeVars args, empty, empty)
else do
let vars = allFreeVarsWithOcc args
relVL = IntMap.keys $ IntMap.filter isRelevant vars
nonstrictVL = IntMap.keys $ IntMap.filter isNonStrict vars
let fromIrrVar (Var i []) = return [i]
fromIrrVar (Con c _ vs) =
ifM (isNothing <$> isRecordConstructor (conName c)) (return []) $
concat <$> mapM (fromIrrVar . unArg) (fromMaybe __IMPOSSIBLE__ (allApplyElims vs))
fromIrrVar _ = return []
irrVL <- concat <$> mapM fromIrrVar
[ v | Arg info v <- args, isIrrelevant info ]
return (relVL, nonstrictVL, irrVL)
reportSDoc "tc.meta.assign" 20 $
let pr (Var n []) = text (show n)
pr (Def c []) = prettyTCM c
pr _ = text ".."
in vcat
[ text "mvar args:" <+> sep (map (pr . unArg) args)
, text "fvars lhs (rel):" <+> sep (map (text . show) relVL)
, text "fvars lhs (nonstrict):" <+> sep (map (text . show) nonstrictVL)
, text "fvars lhs (irr):" <+> sep (map (text . show) irrVL)
]
v <- liftTCM $ occursCheck x (relVL, nonstrictVL, irrVL) v
reportSLn "tc.meta.assign" 15 "passed occursCheck"
verboseS "tc.meta.assign" 30 $ do
let n = termSize v
when (n > 200) $ reportSDoc "tc.meta.assign" 30 $
sep [ text "size" <+> text (show n)
, nest 2 $ text "term" <+> prettyTCM v
]
let fvs = allFreeVars v
reportSDoc "tc.meta.assign" 20 $
text "fvars rhs:" <+> sep (map (text . show) $ Set.toList fvs)
mids <- do
res <- runExceptT $ inverseSubst args
case res of
Right ids -> do
reportSDoc "tc.meta.assign" 50 $
text "inverseSubst returns:" <+> sep (map prettyTCM ids)
return $ Just ids
Left CantInvert -> return Nothing
Left NeutralArg -> Just <$> attemptPruning x args fvs
Left ProjectedVar{} -> Just <$> attemptPruning x args fvs
case mids of
Nothing -> patternViolation
Just ids -> do
ids <- do
res <- runExceptT $ checkLinearity ids
case res of
Right ids -> return ids
Left () -> attemptPruning x args fvs
m <- getContextSize
assignMeta' m x t (length args) ids v
where
attemptPruning
:: MetaId
-> Args
-> FVs
-> TCM a
attemptPruning x args fvs = do
killResult <- prune x args $ Set.toList fvs
reportSDoc "tc.meta.assign" 10 $
text "pruning" <+> prettyTCM x <+> do
text $
if killResult `elem` [PrunedSomething,PrunedEverything] then "succeeded"
else "failed"
patternViolation
assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
assignMeta m x t ids v = do
let n = length ids
cand = List.sort $ zip ids $ map var $ downFrom n
assignMeta' m x t n cand v
assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
assignMeta' m x t n ids v = do
reportSDoc "tc.meta.assign" 25 $
text "preparing to instantiate: " <+> prettyTCM v
v' <- do
let assocToList i l = case l of
_ | i >= m -> []
((j,u) : l) | i == j -> Just u : assocToList (i+1) l
_ -> Nothing : assocToList (i+1) l
ivs = assocToList 0 ids
rho = prependS __IMPOSSIBLE__ ivs $ raiseS n
return $ applySubst rho v
inTopContext $ do
reportSDoc "tc.meta.assign" 15 $ text "type of meta =" <+> prettyTCM t
reportSDoc "tc.meta.assign" 70 $ text "type of meta =" <+> text (show t)
TelV tel' _ <- telViewUpTo n t
reportSDoc "tc.meta.assign" 30 $ text "tel' =" <+> prettyTCM tel'
reportSDoc "tc.meta.assign" 30 $ text "#args =" <+> text (show n)
when (size tel' < n)
patternViolation
let vsol = abstract tel' v'
reportSDoc "tc.meta.assign" 10 $
text "solving" <+> prettyTCM x <+> text ":=" <+> prettyTCM vsol
assignTerm x (telToArgs tel') v'
subtypingForSizeLt
:: CompareDirection
-> MetaId
-> MetaVariable
-> Type
-> Args
-> Term
-> (Term -> TCM ())
-> TCM ()
subtypingForSizeLt DirEq x mvar t args v cont = cont v
subtypingForSizeLt dir x mvar t args v cont = do
let fallback = cont v
(mSize, mSizeLt) <- getBuiltinSize
caseMaybe mSize fallback $ \ qSize -> do
caseMaybe mSizeLt fallback $ \ qSizeLt -> do
v <- reduce v
case v of
Def q [Apply (Arg ai u)] | q == qSizeLt -> do
TelV tel _ <- telView t
let size = sizeType_ qSize
t' = telePi tel size
y <- newMeta (mvInfo mvar) (mvPriority mvar) (mvPermutation mvar)
(HasType __IMPOSSIBLE__ t')
let yArgs = MetaV y $ map Apply args
addConstraint $ dirToCmp (`ValueCmp` size) dir yArgs u
let xArgs = MetaV x $ map Apply args
v' = Def qSizeLt [Apply $ Arg ai yArgs]
c = dirToCmp (`ValueCmp` sizeUniv) dir xArgs v'
catchConstraint c $ cont v'
_ -> fallback
expandProjectedVars
:: ( Show a, PrettyTCM a, NoProjectedVar a
, ReduceAndEtaContract a
, PrettyTCM b, Subst Term b
)
=> a
-> b
-> (a -> b -> TCM c)
-> TCM c
expandProjectedVars args v ret = loop (args, v) where
loop (args, v) = do
reportSDoc "tc.meta.assign.proj" 45 $ text "meta args: " <+> prettyTCM args
args <- callByName $ reduceAndEtaContract args
reportSDoc "tc.meta.assign.proj" 45 $ text "norm args: " <+> prettyTCM args
reportSDoc "tc.meta.assign.proj" 85 $ text "norm args: " <+> text (show args)
let done = ret args v
case noProjectedVar args of
Right () -> do
reportSDoc "tc.meta.assign.proj" 40 $
text "no projected var found in args: " <+> prettyTCM args
done
Left (ProjVarExc i _) -> etaExpandProjectedVar i (args, v) done loop
etaExpandProjectedVar :: (PrettyTCM a, Subst Term a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar i v fail succeed = do
reportSDoc "tc.meta.assign.proj" 40 $
text "trying to expand projected variable" <+> prettyTCM (var i)
caseMaybeM (etaExpandBoundVar i) fail $ \ (delta, sigma, tau) -> do
reportSDoc "tc.meta.assign.proj" 25 $
text "eta-expanding var " <+> prettyTCM (var i) <+>
text " in terms " <+> prettyTCM v
inTopContext $ addContext delta $
succeed $ applySubst tau v
class NoProjectedVar a where
noProjectedVar :: a -> Either ProjVarExc ()
data ProjVarExc = ProjVarExc Int [(ProjOrigin, QName)]
instance NoProjectedVar Term where
noProjectedVar t =
case t of
Var i es
| qs@(_:_) <- takeWhileJust id $ map isProjElim es -> Left $ ProjVarExc i qs
Con (ConHead _ Inductive (_:_)) _ es | Just vs <- allApplyElims es -> noProjectedVar vs
_ -> return ()
instance NoProjectedVar a => NoProjectedVar (Arg a) where
noProjectedVar = Fold.mapM_ noProjectedVar
instance NoProjectedVar a => NoProjectedVar [a] where
noProjectedVar = Fold.mapM_ noProjectedVar
class (TermLike a, Subst Term a, Reduce a) => ReduceAndEtaContract a where
reduceAndEtaContract :: a -> TCM a
default reduceAndEtaContract
:: (Traversable f, TermLike b, Subst Term b, Reduce b, ReduceAndEtaContract b, f b ~ a)
=> a -> TCM a
reduceAndEtaContract = Trav.mapM reduceAndEtaContract
instance ReduceAndEtaContract a => ReduceAndEtaContract [a] where
instance ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) where
instance ReduceAndEtaContract Term where
reduceAndEtaContract u = do
reduce u >>= \case
Lam ai (Abs x b) -> etaLam ai x =<< reduceAndEtaContract b
Con c ci es | Just args <- allApplyElims es -> etaCon c ci args $ \ r c ci args -> do
args <- reduceAndEtaContract args
etaContractRecord r c ci args
v -> return v
type FVs = Set.VarSet
type SubstCand = [(Int,Term)]
checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
checkLinearity ids0 = do
let ids = List.sortBy (compare `on` fst) ids0
let grps = groupOn fst ids
concat <$> mapM makeLinear grps
where
makeLinear :: SubstCand -> ExceptT () TCM SubstCand
makeLinear [] = __IMPOSSIBLE__
makeLinear grp@[_] = return grp
makeLinear (p@(i,t) : _) =
ifM ((Right True ==) <$> do isSingletonTypeModuloRelevance =<< typeOfBV i)
(return [p])
(throwError ())
type Res = [(Arg Nat, Term)]
data InvertExcept
= CantInvert
| NeutralArg
| ProjectedVar Int [(ProjOrigin, QName)]
inverseSubst :: Args -> ExceptT InvertExcept TCM SubstCand
inverseSubst args = map (mapFst unArg) <$> loop (zip args terms)
where
loop = foldM isVarOrIrrelevant []
terms = map var (downFrom (size args))
failure = do
lift $ reportSDoc "tc.meta.assign" 15 $ vcat
[ text "not all arguments are variables: " <+> prettyTCM args
, text " aborting assignment" ]
throwError CantInvert
neutralArg = throwError NeutralArg
isVarOrIrrelevant :: Res -> (Arg Term, Term) -> ExceptT InvertExcept TCM Res
isVarOrIrrelevant vars (arg, t) =
case arg of
Arg info (Var i []) -> return $ (Arg info i, t) `cons` vars
Arg _ (Var i es) | Just qs <- mapM isProjElim es ->
throwError $ ProjectedVar i qs
Arg info (Con c ci es) -> do
let fallback
| isIrrelevant info = return vars
| otherwise = failure
isRC <- lift $ isRecordConstructor $ conName c
case isRC of
Just (_, Record{ recFields = fs })
| length fs == length es -> do
let aux (Arg _ v) (Arg info' f) = (Arg ai v,) $ t `applyE` [Proj ProjSystem f] where
ai = ArgInfo
{ argInfoHiding = min (getHiding info) (getHiding info')
, argInfoModality = Modality
{ modRelevance = max (getRelevance info) (getRelevance info')
, modQuantity = max (getQuantity info) (getQuantity info')
}
, argInfoOrigin = min (getOrigin info) (getOrigin info')
, argInfoFreeVariables = unknownFreeVariables
}
vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
res <- loop $ zipWith aux vs fs
return $ res `append` vars
| otherwise -> fallback
Just _ -> __IMPOSSIBLE__
Nothing -> fallback
Arg info _ | isIrrelevant info -> return vars
Arg _ DontCare{} -> return vars
Arg _ Var{} -> neutralArg
Arg _ Def{} -> neutralArg
Arg _ Lam{} -> failure
Arg _ Lit{} -> failure
Arg _ MetaV{} -> failure
Arg _ Pi{} -> neutralArg
Arg _ Sort{} -> neutralArg
Arg _ Level{} -> neutralArg
append :: Res -> Res -> Res
append res vars = foldr cons vars res
cons :: (Arg Nat, Term) -> Res -> Res
cons a@(Arg ai i, t) vars
| isIrrelevant ai = applyUnless (any ((i==) . unArg . fst) vars) (a :) vars
| otherwise = a :
filter (not . (\ a@(Arg info j, t) -> isIrrelevant info && i == j)) vars
openMetasToPostulates :: TCM ()
openMetasToPostulates = do
m <- asks envCurrentModule
ms <- Map.assocs <$> use stMetaStore
forM_ ms $ \ (x, mv) -> do
when (isOpenMeta $ mvInstantiation mv) $ do
let t = jMetaType $ mvJudgement mv
let r = clValue $ miClosRange $ mvInfo mv
let s = "unsolved#meta." ++ show (metaId x)
n <- freshName r s
let q = A.QName m n
reportSDoc "meta.postulate" 20 $ vcat
[ text ("Turning " ++ if isSortMeta_ mv then "sort" else "value" ++ " meta ")
<+> prettyTCM x <+> text " into postulate."
, nest 2 $ vcat
[ text "Name: " <+> prettyTCM q
, text "Type: " <+> prettyTCM t
]
]
addConstant q $ defaultDefn defaultArgInfo q t Axiom
let inst = InstV [] $ Def q []
stMetaStore %= Map.adjust (\ mv0 -> mv0 { mvInstantiation = inst }) x
return ()