module Agda.TypeChecking.Rules.LHS where
import Prelude hiding (mapM, sequence)
import Data.Maybe
import Control.Applicative
import Control.Arrow (first, second, (***))
import Control.Monad hiding (mapM, forM, sequence)
import Control.Monad.State hiding (mapM, forM, sequence)
import Control.Monad.Trans.Maybe
import Data.Function (on)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.List (delete, sortBy, stripPrefix)
import Data.Monoid
import Data.Traversable
import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Abstract (IsProjP(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (asView)
import Agda.Syntax.Common as Common
import Agda.Syntax.Info as A
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base (ScopeInfo, emptyScopeInfo)
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Empty
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Substitute.Pattern
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.Term (checkExpr)
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.TypeChecking.Rules.LHS.ProblemRest
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Rules.LHS.Split
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Rules.LHS.Instantiate
import Agda.TypeChecking.Rules.Data
import Agda.Utils.Except (MonadError(..))
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
flexiblePatterns :: [NamedArg A.Pattern] -> TCM FlexibleVars
flexiblePatterns nps = do
forMaybeM (zip (downFrom $ length nps) nps) $ \ (i, Arg ai p) -> do
runMaybeT $ (\ f -> FlexibleVar (getHiding ai) f i) <$> maybeFlexiblePattern p
class IsFlexiblePattern a where
maybeFlexiblePattern :: a -> MaybeT TCM FlexibleVarKind
isFlexiblePattern :: a -> TCM Bool
isFlexiblePattern p = isJust <$> runMaybeT (maybeFlexiblePattern p)
instance IsFlexiblePattern A.Pattern where
maybeFlexiblePattern p =
case p of
A.DotP{}
-> return DotFlex
A.WildP{}
-> return ImplicitFlex
A.ConP _ (A.AmbQ [c]) qs
-> ifM (isNothing <$> isRecordConstructor c) mzero
(maybeFlexiblePattern qs)
_ -> mzero
instance IsFlexiblePattern (I.Pattern' a) where
maybeFlexiblePattern p =
case p of
I.DotP{} -> return DotFlex
I.ConP _ i ps
| Just ConPImplicit <- conPRecord i -> return ImplicitFlex
| Just _ <- conPRecord i -> maybeFlexiblePattern ps
| otherwise -> mzero
I.VarP{} -> mzero
I.LitP{} -> mzero
I.ProjP{} -> mzero
instance IsFlexiblePattern a => IsFlexiblePattern [a] where
maybeFlexiblePattern ps = RecordFlex <$> mapM maybeFlexiblePattern ps
instance IsFlexiblePattern a => IsFlexiblePattern (Arg a) where
maybeFlexiblePattern = maybeFlexiblePattern . unArg
instance IsFlexiblePattern a => IsFlexiblePattern (Common.Named name a) where
maybeFlexiblePattern = maybeFlexiblePattern . namedThing
updateInPatterns
:: [Dom Type]
-> [NamedArg A.Pattern]
-> [Arg DeBruijnPattern]
-> TCM ([NamedArg A.Pattern]
,[DotPatternInst])
updateInPatterns as ps qs = do
reportSDoc "tc.lhs.top" 20 $ text "updateInPatterns" <+> nest 2 (vcat
[ text "as =" <+> prettyList (map prettyTCM as)
, text "ps =" <+> prettyList (map prettyA ps)
, text "qs =" <+> prettyList (map (text . show) qs)
])
first (map snd . IntMap.toDescList) <$> updates as ps qs
where
updates :: [Dom Type] -> [NamedArg A.Pattern] -> [Arg DeBruijnPattern]
-> TCM (IntMap (NamedArg A.Pattern), [DotPatternInst])
updates as ps qs = mconcat <$> sequence (zipWith3 update as ps qs)
update :: Dom Type -> NamedArg A.Pattern -> Arg DeBruijnPattern
-> TCM (IntMap (NamedArg A.Pattern), [DotPatternInst])
update a p q = case unArg q of
VarP (i,_) -> return (IntMap.singleton i p, [])
DotP u -> case namedThing (unArg p) of
A.DotP _ e -> return (IntMap.empty,[DPI (Just e) u a])
A.WildP _ -> return (IntMap.empty,[DPI Nothing u a])
A.ConP _ (A.AmbQ [c]) qs -> do
Def r es <- ignoreSharing <$> reduce (unEl $ unDom a)
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
(ftel, us) <- etaExpandRecord r vs u
qs <- insertImplicitPatterns ExpandLast qs ftel
let instTel EmptyTel _ = []
instTel (ExtendTel arg tel) (u : us) = arg : instTel (absApp tel u) us
instTel ExtendTel{} [] = __IMPOSSIBLE__
bs0 = instTel ftel (map unArg us)
bs = map (mapRelevance (composeRelevance (getRelevance a))) bs0
updates bs qs (map (DotP . unArg) us `withArgsFrom` teleArgNames ftel)
A.VarP _ -> __IMPOSSIBLE__
A.ConP _ _ _ -> __IMPOSSIBLE__
A.RecP _ _ -> __IMPOSSIBLE__
A.DefP _ _ _ -> __IMPOSSIBLE__
A.AsP _ _ _ -> __IMPOSSIBLE__
A.AbsurdP _ -> __IMPOSSIBLE__
A.LitP _ -> __IMPOSSIBLE__
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
ConP c cpi qs -> do
Def r es <- ignoreSharing <$> reduce (unEl $ unDom a)
def <- theDef <$> getConstInfo r
let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
fs = killRange $ recFields def
tel = recTel def `apply` pars
as = applyPatSubst (parallelS $ map (namedThing . unArg) qs) $ flattenTel tel
dpi :: [DotPatternInst]
dpi = maybe [] (\e -> [DPI (Just e) (patternToTerm $ unArg q) a]) (isDotP (namedThing $ unArg p))
second (dpi++) <$>
updates as (projectInPat p fs) (map (fmap namedThing) qs)
LitP _ -> __IMPOSSIBLE__
ProjP f -> __IMPOSSIBLE__
projectInPat :: NamedArg A.Pattern -> [Arg QName] -> [NamedArg A.Pattern]
projectInPat p fs = case namedThing (unArg p) of
A.VarP x -> map makeVarField fs
A.ConP cpi _ nps -> nps
A.WildP pi -> map (makeWildField pi) fs
A.DotP pi e -> map (makeDotField pi) fs
A.DefP _ _ _ -> __IMPOSSIBLE__
A.AsP _ _ _ -> __IMPOSSIBLE__
A.AbsurdP _ -> __IMPOSSIBLE__
A.LitP _ -> __IMPOSSIBLE__
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
A.RecP _ _ -> __IMPOSSIBLE__
where
makeVarField (Arg fi f) = Arg fi $ unnamed $ A.VarP $ qnameName f
makeWildField pi (Arg fi f) = Arg fi $ unnamed $ A.WildP pi
makeDotField pi (Arg fi f) = Arg fi $ unnamed $
A.DotP pi $ A.Underscore underscoreInfo
where
underscoreInfo = A.MetaInfo
{ A.metaRange = getRange pi
, A.metaScope = emptyScopeInfo
, A.metaNumber = Nothing
, A.metaNameSuggestion = show $ A.nameConcrete $ qnameName f
}
isDotP :: A.Pattern -> Maybe A.Expr
isDotP (A.DotP _ e) = Just e
isDotP _ = Nothing
isSolvedProblem :: Problem -> Bool
isSolvedProblem problem = null (restPats $ problemRest problem) &&
all (isSolved . snd . asView . namedArg) (problemInPat problem)
where
isSolved A.ConP{} = False
isSolved A.LitP{} = False
isSolved A.DefP{} = False
isSolved A.RecP{} = False
isSolved A.VarP{} = True
isSolved A.WildP{} = True
isSolved A.DotP{} = True
isSolved A.AbsurdP{} = True
isSolved A.AsP{} = __IMPOSSIBLE__
isSolved A.PatternSynP{} = __IMPOSSIBLE__
noShadowingOfConstructors
:: Call
-> Problem -> TCM ()
noShadowingOfConstructors mkCall problem =
traceCall mkCall $ do
let pat = map (snd . asView . namedArg) $
problemInPat problem
tel = map (unEl . snd . unDom) $ telToList $ problemTel problem
zipWithM_ noShadowing pat tel
return ()
where
noShadowing (A.WildP {}) t = return ()
noShadowing (A.AbsurdP {}) t = return ()
noShadowing (A.ConP {}) t = return ()
noShadowing (A.RecP {}) t = return ()
noShadowing (A.DefP {}) t = return ()
noShadowing (A.DotP {}) t = return ()
noShadowing (A.AsP {}) t = __IMPOSSIBLE__
noShadowing (A.LitP {}) t = __IMPOSSIBLE__
noShadowing (A.PatternSynP {}) t = __IMPOSSIBLE__
noShadowing (A.VarP x) t = do
reportSDoc "tc.lhs.shadow" 30 $ vcat
[ text $ "checking whether pattern variable " ++ show x ++ " shadows a constructor"
, nest 2 $ text "type of variable =" <+> prettyTCM t
]
reportSLn "tc.lhs.shadow" 70 $ " t = " ++ show t
t <- reduce t
case t of
Def t _ -> do
d <- theDef <$> getConstInfo t
case d of
Datatype { dataCons = cs } -> do
case filter ((A.nameConcrete x ==) . A.nameConcrete . A.qnameName) cs of
[] -> return ()
(c : _) -> setCurrentRange x $
typeError $ PatternShadowsConstructor x c
Axiom {} -> return ()
Function {} -> return ()
Record {} -> return ()
Constructor {} -> __IMPOSSIBLE__
Primitive {} -> __IMPOSSIBLE__
Var {} -> return ()
Pi {} -> return ()
Sort {} -> return ()
Shared p -> noShadowing (A.VarP x) $ derefPtr p
MetaV {} -> return ()
Lam {} -> __IMPOSSIBLE__
Lit {} -> __IMPOSSIBLE__
Level {} -> __IMPOSSIBLE__
Con {} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
checkDotPattern :: DotPatternInst -> TCM ()
checkDotPattern (DPI (Just e) v (Dom info a)) =
traceCall (CheckDotPattern e v) $ do
reportSDoc "tc.lhs.dot" 15 $
sep [ text "checking dot pattern"
, nest 2 $ prettyA e
, nest 2 $ text "=" <+> prettyTCM v
, nest 2 $ text ":" <+> prettyTCM a
]
applyRelevanceToContext (argInfoRelevance info) $ do
u <- checkExpr e a
reportSDoc "tc.lhs.dot" 30 $
sep [ text "equalTerm"
, nest 2 $ text $ show a
, nest 2 $ text $ show u
, nest 2 $ text $ show v
]
noConstraints $ equalTerm a u v
checkDotPattern (DPI Nothing _ _) = return ()
checkLeftoverDotPatterns
:: [NamedArg A.Pattern]
-> [Int]
-> [Dom Type]
-> [DotPatternInst]
-> TCM ()
checkLeftoverDotPatterns ps vs as dpi = do
reportSDoc "tc.lhs.dot" 15 $ text "checking leftover dot patterns..."
idv <- sortBy (compare `on` length . snd) . concat <$>
traverse gatherImplicitDotVars dpi
reportSDoc "tc.lhs.dot" 30 $ nest 2 $
text "implicit dotted variables:" <+>
prettyList (map (\(i,fs) -> prettyTCM $ Var i (map Proj fs)) idv)
checkUserDots ps vs as idv
reportSDoc "tc.lhs.dot" 15 $ text "all leftover dot patterns ok!"
where
checkUserDots :: [NamedArg A.Pattern] -> [Int] -> [Dom Type]
-> [(Int,[QName])]
-> TCM ()
checkUserDots [] [] [] idv = return ()
checkUserDots [] (_:_) _ idv = __IMPOSSIBLE__
checkUserDots [] _ (_:_) idv = __IMPOSSIBLE__
checkUserDots (_:_) [] _ idv = __IMPOSSIBLE__
checkUserDots (_:_) _ [] idv = __IMPOSSIBLE__
checkUserDots (p:ps) (v:vs) (a:as) idv = do
idv' <- checkUserDot p v a idv
checkUserDots ps vs as idv'
checkUserDot :: NamedArg A.Pattern -> Int -> Dom Type
-> [(Int,[QName])]
-> TCM [(Int,[QName])]
checkUserDot p v a idv = case namedArg p of
A.DotP i e -> do
reportSDoc "tc.lhs.dot" 30 $ nest 2 $
text "checking user dot pattern: " <+> prettyA e
caseMaybeM (undotImplicitVar (v,[],unDom a) idv)
(traceCall (CheckPattern (namedArg p) EmptyTel (unDom a)) $
typeError $ UninstantiatedDotPattern e)
(\idv' -> do
u <- checkExpr e (unDom a)
reportSDoc "tc.lhs.dot" 30 $ nest 2 $
text "checked expression: " <+> prettyTCM u
noConstraints $ equalTerm (unDom a) u (var v)
return idv')
A.VarP _ -> return idv
A.WildP _ -> return idv
A.AbsurdP _ -> return idv
A.ConP _ _ _ -> __IMPOSSIBLE__
A.LitP _ -> __IMPOSSIBLE__
A.DefP _ _ _ -> __IMPOSSIBLE__
A.RecP _ _ -> __IMPOSSIBLE__
A.AsP _ _ _ -> __IMPOSSIBLE__
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
gatherImplicitDotVars :: DotPatternInst -> TCM [(Int,[QName])]
gatherImplicitDotVars (DPI (Just _) _ _) = return []
gatherImplicitDotVars (DPI Nothing u _) = gatherVars u
where
gatherVars :: Term -> TCM [(Int,[QName])]
gatherVars u = case ignoreSharing u of
Var i es -> return $ (i,) <$> maybeToList (allProjElims es)
Con c us -> ifM (isEtaCon $ conName c)
(concat <$> traverse (gatherVars . unArg) us)
(return [])
_ -> return []
lookupImplicitDotVar :: (Int,[QName]) -> [(Int,[QName])] -> Maybe [QName]
lookupImplicitDotVar (i,fs) [] = Nothing
lookupImplicitDotVar (i,fs) ((j,gs):js)
| i == j , Just hs <- stripPrefix fs gs = Just hs
| otherwise = lookupImplicitDotVar (i,fs) js
undotImplicitVar :: (Int,[QName],Type) -> [(Int,[QName])]
-> TCM (Maybe [(Int,[QName])])
undotImplicitVar (i,fs,a) idv = case lookupImplicitDotVar (i,fs) idv of
Nothing -> return Nothing
Just [] -> return $ Just $ delete (i,fs) idv
Just rs -> caseMaybeM (isEtaRecordType a) (return Nothing) $ \(d,pars) -> do
gs <- recFields . theDef <$> getConstInfo d
let u = Var i (map Proj fs)
is <- forM gs $ \(Arg _ g) -> do
(_,b) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped u a g
return (i,fs++[g],b)
undotImplicitVars is idv
undotImplicitVars :: [(Int,[QName],Type)] -> [(Int,[QName])]
-> TCM (Maybe [(Int,[QName])])
undotImplicitVars [] idv = return $ Just idv
undotImplicitVars (i:is) idv =
caseMaybeM (undotImplicitVar i idv)
(return Nothing)
(\idv' -> undotImplicitVars is idv')
bindLHSVars :: [NamedArg A.Pattern] -> Telescope -> TCM a -> TCM a
bindLHSVars [] tel@ExtendTel{} _ = do
reportSDoc "impossible" 10 $
text "bindLHSVars: no patterns left, but tel =" <+> prettyTCM tel
__IMPOSSIBLE__
bindLHSVars (_ : _) EmptyTel _ = __IMPOSSIBLE__
bindLHSVars [] EmptyTel ret = ret
bindLHSVars (p : ps) (ExtendTel a tel) ret = do
unless (getHiding p == getHiding a) $ typeError WrongHidingInLHS
case namedArg p of
A.VarP x -> addContext (x, a) $ bindLHSVars ps (absBody tel) ret
A.WildP _ -> bindDummy (absName tel)
A.DotP _ _ -> bindDummy (absName tel)
A.AbsurdP pi -> do
isEmptyType (getRange pi) $ unDom a
bindDummy (absName tel)
A.ConP{} -> __IMPOSSIBLE__
A.RecP{} -> __IMPOSSIBLE__
A.DefP{} -> __IMPOSSIBLE__
A.AsP{} -> __IMPOSSIBLE__
A.LitP{} -> __IMPOSSIBLE__
A.PatternSynP{} -> __IMPOSSIBLE__
where
bindDummy s = do
x <- if isUnderscore s then freshNoName_ else freshName_ ("." ++ argNameToString s)
addContext (x, a) $ bindLHSVars ps (absBody tel) ret
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
bindAsPatterns [] ret = ret
bindAsPatterns (AsB x v a : asb) ret = do
reportSDoc "tc.lhs.as" 10 $ text "as pattern" <+> prettyTCM x <+>
sep [ text ":" <+> prettyTCM a
, text "=" <+> prettyTCM v
]
addLetBinding defaultArgInfo x v a $ bindAsPatterns asb ret
data LHSResult = LHSResult
{ lhsVarTele :: Telescope
, lhsPatterns :: [NamedArg Pattern]
, lhsBodyType :: Arg Type
, lhsPermutation :: Permutation
}
instance InstantiateFull LHSResult where
instantiateFull' (LHSResult tel ps t perm) = LHSResult
<$> instantiateFull' tel
<*> instantiateFull' ps
<*> instantiateFull' t
<*> return perm
checkLeftHandSide
:: Call
-> Maybe QName
-> [NamedArg A.Pattern]
-> Type
-> (LHSResult -> TCM a)
-> TCM a
checkLeftHandSide c f ps a ret = Bench.billTo [Bench.Typing, Bench.CheckLHS] $ do
problem0 <- problemFromPats ps a
LHSState problem@(Problem ps qs delta rest) sigma dpi asb
<- checkLHS f $ LHSState problem0 idS [] []
unless (null $ restPats rest) $ typeError $ TooManyArgumentsInLHS a
addCtxTel delta $ do
noShadowingOfConstructors c problem
noPatternMatchingOnCodata qs
reportSDoc "tc.lhs.top" 10 $
vcat [ text "checked lhs:"
, nest 2 $ vcat
[ text "ps = " <+> fsep (map prettyA ps)
, text "delta = " <+> prettyTCM delta
, text "dpi = " <+> addCtxTel delta (brackets $ fsep $ punctuate comma $ map prettyTCM dpi)
, text "asb = " <+> addCtxTel delta (brackets $ fsep $ punctuate comma $ map prettyTCM asb)
, text "qs = " <+> text (show qs)
]
]
let b' = restType rest
bindLHSVars (filter (isNothing . isProjP) ps) delta $ bindAsPatterns asb $ do
reportSDoc "tc.lhs.top" 10 $ text "bound pattern variables"
reportSDoc "tc.lhs.top" 60 $ nest 2 $ text "context = " <+> ((text . show) =<< getContext)
reportSDoc "tc.lhs.top" 10 $ nest 2 $ text "type = " <+> prettyTCM b'
reportSDoc "tc.lhs.top" 60 $ nest 2 $ text "type = " <+> text (show b')
mapM_ checkDotPattern dpi
checkLeftoverDotPatterns ps (downFrom $ size delta) (flattenTel delta) dpi
let qs' = unnumberPatVars qs
perm = dbPatPerm qs
lhsResult = LHSResult delta qs' b' perm
reportSDoc "tc.lhs.top" 20 $ nest 2 $ text "perm = " <+> text (show perm)
applyRelevanceToContext (getRelevance b') $ ret lhsResult
checkLHS
:: Maybe QName
-> LHSState
-> TCM LHSState
checkLHS f st@(LHSState problem sigma dpi asb) = do
problem <- insertImplicitProblem problem
if isSolvedProblem problem then return $ st { lhsProblem = problem } else do
unlessM (optPatternMatching <$> gets getPragmaOptions) $
typeError $ GenericError $ "Pattern matching is disabled"
foldListT trySplit nothingToSplit $ splitProblem f problem
where
nothingToSplit = do
reportSLn "tc.lhs.split" 50 $ "checkLHS: nothing to split in problem " ++ show problem
nothingToSplitError problem
trySplit (SplitRest projPat projType) _ = do
let Problem ps1 ip delta (ProblemRest (p:ps2) b) = problem
ps' = ps1
rest = ProblemRest ps2 (projPat $> projType)
ip' = ip ++ [fmap (Named Nothing . ProjP) projPat]
problem' = Problem ps' ip' delta rest
st' <- updateProblemRest (LHSState problem' sigma dpi asb)
applyRelevanceToContext (getRelevance projPat) $ do
checkLHS f st'
trySplit (Split p0 xs (Arg _ (LitFocus lit ip a)) p1) _ = do
let delta1 = problemTel p0
delta2 = absApp (fmap problemTel p1) (Lit lit)
rho = singletonS (size delta2) (LitP lit)
sigma' = applySubst rho sigma
dpi' = applyPatSubst rho dpi
asb0 = applyPatSubst rho asb
ip' = applySubst rho ip
rest' = applyPatSubst rho (problemRest problem)
let ps' = problemInPat p0 ++ problemInPat (absBody p1)
delta' = abstract delta1 delta2
problem' = Problem ps' ip' delta' rest'
asb' = raise (size delta2) (map (\x -> AsB x (Lit lit) a) xs) ++ asb0
st' <- updateProblemRest (LHSState problem' sigma' dpi' asb')
checkLHS f st'
trySplit (Split p0 xs focus@(Arg info Focus{}) p1) tryNextSplit = do
res <- trySplitConstructor p0 xs focus p1
case res of
Unifies st' -> checkLHS f st'
NoUnify tcerr -> throwError tcerr
DontKnow tcerr -> tryNextSplit `catchError` \ _ -> throwError tcerr
whenUnifies
:: UnificationResult' a
-> (a -> TCM (UnificationResult' b))
-> TCM (UnificationResult' b)
whenUnifies res cont = do
case res of
Unifies a -> cont a
NoUnify tcerr -> return $ NoUnify tcerr
DontKnow tcerr -> return $ DontKnow tcerr
trySplitConstructor p0 xs (Arg info LitFocus{}) p1 = __IMPOSSIBLE__
trySplitConstructor p0 xs (Arg info
(Focus { focusCon = c
, focusPatOrigin= porigin
, focusConArgs = qs
, focusRange = r
, focusOutPat = ip
, focusDatatype = d
, focusParams = vs
, focusIndices = ws
, focusType = a
}
)) p1 = do
traceCall (CheckPattern (A.ConP (ConPatInfo porigin $ PatRange r) (A.AmbQ [c]) qs)
(problemTel p0)
(El Prop $ Def d $ map Apply $ vs ++ ws)) $ do
let delta1 = problemTel p0
delta2 = problemTel $ absBody p1
let typeOfSplitVar = Arg info a
reportSDoc "tc.lhs.split" 10 $ sep
[ text "checking lhs"
, nest 2 $ text "tel =" <+> prettyTCM (problemTel problem)
, nest 2 $ text "rel =" <+> (text $ show $ argInfoRelevance info)
]
reportSDoc "tc.lhs.split" 15 $ sep
[ text "split problem"
, nest 2 $ vcat
[ text "delta1 = " <+> prettyTCM delta1
, text "typeOfSplitVar =" <+> addCtxTel delta1 (prettyTCM typeOfSplitVar)
, text "focusOutPat =" <+> (text . show) ip
, text "delta2 = " <+> addCtxTel delta1 (addContext ("x",domFromArg typeOfSplitVar) (prettyTCM delta2))
]
]
c <- (`withRangeOf` c) <$> getConForm c
ca <- defType <$> getConInfo c
reportSDoc "tc.lhs.split" 20 $ nest 2 $ vcat
[ text "ca =" <+> prettyTCM ca
, text "vs =" <+> prettyList (map prettyTCM vs)
]
let a = ca `piApply` vs
(gamma', ca, d', us) <- do
TelV gamma' ca@(El _ def) <- telView a
let Def d' es = ignoreSharing def
Just us = allApplyElims es
return (gamma', ca, d', us)
unless (d == d') $ typeError $ ShouldBeApplicationOf ca d'
let updRel = composeRelevance (getRelevance info)
gamma' <- return $ mapRelevance updRel <$> gamma'
qs' <- insertImplicitPatterns ExpandLast qs gamma'
unless ((size qs' :: Int) == size gamma') $
typeError $ WrongNumberOfConstructorArguments (conName c) (size gamma') (size qs')
let gamma = useNamesFromPattern qs' gamma'
da <- (`piApply` vs) . defType <$> getConstInfo d
flex <- flexiblePatterns (problemInPat p0 ++ qs')
let us' = drop (size vs) us
reportSDoc "tc.lhs.top" 15 $ addCtxTel delta1 $
sep [ text "preparing to unify"
, nest 2 $ vcat
[ text "c =" <+> prettyTCM c <+> text ":" <+> prettyTCM a
, text "d =" <+> prettyTCM (Def d (map Apply $ vs++ws)) <+> text ":" <+> prettyTCM da
, text "gamma =" <+> prettyTCM gamma
, text "gamma' =" <+> prettyTCM gamma'
, text "vs =" <+> brackets (fsep $ punctuate comma $ map prettyTCM vs)
, text "us' =" <+> addCtxTel gamma (brackets (fsep $ punctuate comma $ map prettyTCM us'))
, text "ws =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ws)
]
]
res <- unifyIndices
(delta1 `abstract` gamma)
flex
(raise (size gamma) da)
us'
(raise (size gamma) ws)
whenUnifies res $ \ (delta1',rho0) -> do
reportSDoc "tc.lhs.top" 15 $ text "unification successful"
reportSDoc "tc.lhs.top" 20 $ nest 2 $ vcat
[ text "delta1' =" <+> prettyTCM delta1'
, text "rho0 =" <+> addCtxTel delta1' (prettyTCM rho0)
]
delta1' <- return $ mapRelevance ignoreForced <$> delta1'
let newPats = applySubst rho0 $ teleArgs $ delta1 `abstract` gamma
oldTypes = applyPatSubst rho0 $ flattenTel $ delta1 `abstract` gamma
(p0',newDpi) <- addCtxTel delta1' $ updateInPatterns
oldTypes
(problemInPat p0 ++ qs')
newPats
reportSDoc "tc.lhs.top" 20 $ addCtxTel delta1' $ nest 2 $ vcat
[ text "p0' =" <+> text (show p0')
, text "newDpi =" <+> brackets (fsep $ punctuate comma $ map prettyTCM newDpi)
]
let (rho1,rho2) = splitS (size gamma) rho0
reportSDoc "tc.lhs.top" 20 $ addCtxTel delta1' $ nest 2 $ vcat
[ text "rho1 =" <+> prettyTCM rho1
, text "rho2 =" <+> prettyTCM rho2
]
let storedPatternType = applyPatSubst rho1 typeOfSplitVar
isRec <- isRecord d
let cpi = ConPatternInfo (isRec $> porigin) (Just storedPatternType)
let crho2 = ConP c cpi $ applySubst rho2 $ teleNamedArgs gamma
rho3 = consS crho2 rho1
delta2' = applyPatSubst rho3 delta2
delta' = delta1' `abstract` delta2'
rho = liftS (size delta2) rho3
reportSDoc "tc.lhs.top" 20 $ addCtxTel delta1' $ nest 2 $ vcat
[ text "crho2 =" <+> prettyTCM crho2
, text "rho3 =" <+> prettyTCM rho3
, text "delta2' =" <+> prettyTCM delta2'
]
reportSDoc "tc.lhs.top" 70 $ addCtxTel delta1' $ nest 2 $ vcat
[ text "crho2 =" <+> text (show crho2)
, text "rho3 =" <+> text (show rho3)
, text "delta2' =" <+> text (show delta2')
]
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ text "delta' =" <+> prettyTCM delta'
, text "rho =" <+> addCtxTel delta' (prettyTCM rho)
]
let ps' = p0' ++ problemInPat (absBody p1)
reportSDoc "tc.lhs.top" 15 $ addCtxTel delta' $
nest 2 $ vcat
[ text "ps' =" <+> brackets (fsep $ punctuate comma $ map prettyA ps')
]
let dpi' = applyPatSubst rho dpi ++ raise (size delta2') newDpi
asb' = applyPatSubst rho asb ++ raise (size delta2') (map (\x -> AsB x (patternToTerm crho2) ca) xs)
reportSDoc "tc.lhs.top" 15 $ addCtxTel delta' $
nest 2 $ vcat
[ text "dpi' =" <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi')
, text "asb' =" <+> brackets (fsep $ punctuate comma $ map prettyTCM asb')
]
let sigma' = applySubst rho sigma
ip' = applySubst rho ip
rest' = applyPatSubst rho (problemRest problem)
reportSDoc "tc.lhs.top" 15 $ addCtxTel delta' $
nest 2 $ vcat
[ text "sigma' =" <+> prettyTCM sigma'
, text "ip' =" <+> text (show ip)
]
let problem' = Problem ps' ip' delta' rest'
st'@(LHSState problem'@(Problem ps' ip' delta' rest')
sigma' dpi' asb')
<- updateProblemRest $ LHSState problem' sigma' dpi' asb'
reportSDoc "tc.lhs.top" 12 $ sep
[ text "new problem from rest"
, nest 2 $ vcat
[ text "ps' =" <+> fsep (map prettyA ps')
, text "delta' =" <+> prettyTCM delta'
, text "ip' =" <+> text (show ip')
]
]
return $ Unifies st'
noPatternMatchingOnCodata :: [NamedArg DeBruijnPattern] -> TCM ()
noPatternMatchingOnCodata = mapM_ (check . namedArg)
where
check (VarP {}) = return ()
check (DotP {}) = return ()
check (ProjP{}) = return ()
check (LitP {}) = return ()
check (ConP con _ ps) = do
TelV _ t <- telView' . defType <$> do getConstInfo $ conName con
c <- isCoinductive t
case c of
Nothing -> __IMPOSSIBLE__
Just False -> mapM_ (check . namedArg) ps
Just True -> typeError $
GenericError "Pattern matching on coinductive types is not allowed"