module Agda.TypeChecking.Rules.LHS where
import Prelude hiding (mapM)
import Data.Maybe
import Control.Applicative
import Control.Monad hiding (mapM)
import Control.Monad.State hiding (mapM)
import Control.Monad.Trans.Maybe
import Data.Traversable
import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses
import Agda.Syntax.Internal as I hiding (Substitution)
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
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
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 hiding (Substitution)
import qualified Agda.TypeChecking.Substitute as S (Substitution)
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.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
flexiblePatterns :: [A.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 (Common.Arg c a) where
maybeFlexiblePattern = maybeFlexiblePattern . unArg
instance IsFlexiblePattern a => IsFlexiblePattern (Common.Named name a) where
maybeFlexiblePattern = maybeFlexiblePattern . namedThing
dotPatternInsts :: [A.NamedArg A.Pattern] -> Substitution -> [I.Dom Type] -> TCM [DotPatternInst]
dotPatternInsts ps s as = dpi (map namedArg ps) (reverse s) as
where
dpi (_ : _) [] _ = __IMPOSSIBLE__
dpi (_ : _) (Just _ : _) [] = __IMPOSSIBLE__
dpi [] _ _ = return []
dpi (_ : ps) (Nothing : s) as = dpi ps s as
dpi (p : ps) (Just u : s) (a : as) =
case p of
A.DotP _ e -> (DPI e u a :) <$> dpi ps s as
A.WildP _ -> dpi ps s as
A.ConP _ (A.AmbQ [c]) qs -> do
Def r es <- ignoreSharing <$> reduce (unEl $ unDom a)
let Just vs = 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
dpi (map namedArg qs ++ ps) (map (Just . unArg) us ++ s) (bs ++ as)
_ -> __IMPOSSIBLE__
instantiatePattern
:: Substitution
-> Permutation
-> [I.NamedArg Pattern]
-> [I.NamedArg Pattern]
instantiatePattern sub perm ps
| length sub /= length hps = error $ unlines
[ "instantiatePattern:"
, " sub = " ++ show sub
, " perm = " ++ show perm
, " ps = " ++ show ps
]
| otherwise = foldr merge ps $ zipWith inst (reverse sub) hps
where
hps = permute perm $ allHoles ps
inst Nothing hps = Nothing
inst (Just t) hps = Just $ plugHole (DotP t) hps
merge Nothing ps = ps
merge (Just qs) ps = zipWith mergeA qs ps
where
mergeA a1 a2 = fmap (mergeP (namedArg a1) (namedArg a2) <$) a1
mergeP (DotP s) (DotP t)
| s == t = DotP s
| otherwise = __IMPOSSIBLE__
mergeP (DotP t) (VarP _) = DotP t
mergeP (VarP _) (DotP t) = DotP t
mergeP (DotP _) _ = __IMPOSSIBLE__
mergeP _ (DotP _) = __IMPOSSIBLE__
mergeP (ConP c1 i1 ps) (ConP c2 i2 qs)
| c1 == c2 = ConP (c1 `withRangeOf` c2) (mergeCPI i1 i2) $
zipWith mergeA ps qs
| otherwise = __IMPOSSIBLE__
mergeP (LitP l1) (LitP l2)
| l1 == l2 = LitP (l1 `withRangeOf` l2)
| otherwise = __IMPOSSIBLE__
mergeP (VarP x) (VarP y)
| x == y = VarP x
| otherwise = __IMPOSSIBLE__
mergeP (ConP _ _ _) (VarP _) = __IMPOSSIBLE__
mergeP (ConP _ _ _) (LitP _) = __IMPOSSIBLE__
mergeP (VarP _) (ConP _ _ _) = __IMPOSSIBLE__
mergeP (VarP _) (LitP _) = __IMPOSSIBLE__
mergeP (LitP _) (ConP _ _ _) = __IMPOSSIBLE__
mergeP (LitP _) (VarP _) = __IMPOSSIBLE__
mergeP (ProjP x) (ProjP y)
| x == y = ProjP x
| otherwise = __IMPOSSIBLE__
mergeP ProjP{} _ = __IMPOSSIBLE__
mergeP _ ProjP{} = __IMPOSSIBLE__
mergeCPI (ConPatternInfo mr1 mt1) (ConPatternInfo mr2 mt2) =
ConPatternInfo (mplus mr1 mr2) (mplus mt1 mt2)
instantiatePattern'
:: Substitution
-> Permutation
-> [I.NamedArg Pattern]
-> [I.NamedArg Pattern]
instantiatePattern' sub perm ps = evalState (mapM goArg ps) 0
where
sub' = inversePermute perm sub
next = do n <- get; put (n+1); return n
goArg = traverse goNamed
goNamed = traverse goPat
goPat p = case p of
VarP x -> replace p
DotP t -> replace p
ConP c mt ps -> ConP c mt <$> mapM goArg ps
LitP{} -> return p
ProjP{} -> return p
replace p = do
i <- next
let s = case sub' !!! i of
Nothing -> __IMPOSSIBLE__
Just s -> s
return $ fromMaybe p $ DotP <$> s
isSolvedProblem :: Problem -> Bool
isSolvedProblem problem = null (restPats $ problemRest problem) &&
all (isSolved . snd . asView . namedArg) (problemInPat problem)
where
isSolved A.ConP{} = False
isSolved A.DotP{} = False
isSolved A.LitP{} = False
isSolved A.DefP{} = False
isSolved A.VarP{} = True
isSolved A.WildP{} = 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.DefP {}) t = return ()
noShadowing (A.AsP {}) t = __IMPOSSIBLE__
noShadowing (A.DotP {}) 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__
ExtLam{} -> __IMPOSSIBLE__
checkDotPattern :: DotPatternInst -> TCM ()
checkDotPattern (DPI 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
noConstraints $ equalTerm a u v
bindLHSVars :: [A.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.AbsurdP pi -> do
isEmptyType (getRange pi) $ unDom a
bindDummy (absName tel)
A.ConP _ (A.AmbQ [c]) qs -> do
Def r es <- reduce (unEl $ unDom a)
let Just vs = allApplyElims es
ftel <- (`apply` vs) <$> getRecordFieldTypes r
con <- getConHead c
let n = size ftel
eta = Con con [ var i <$ (namedThing <$> setArgColors [] q) | (q, i) <- zip qs [n 1, n 2..0] ]
bindLHSVars (qs ++ ps) (ftel `abstract` absApp (raise (size ftel) tel) eta) ret
A.ConP{} -> __IMPOSSIBLE__
A.DefP{} -> __IMPOSSIBLE__
A.AsP{} -> __IMPOSSIBLE__
A.DotP{} -> __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 :: [I.NamedArg Pattern]
, lhsBodyType :: I.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
-> [A.NamedArg A.Pattern]
-> Type
-> (LHSResult -> TCM a)
-> TCM a
checkLeftHandSide c f ps a ret = do
problem0 <- problemFromPats ps a
LHSState problem@(Problem ps (perm, qs) delta rest) sigma dpi asb
<- checkLHS f $ LHSState problem0 idS [] []
unless (null $ restPats rest) $ typeError $ TooManyArgumentsInLHS a
noShadowingOfConstructors c problem
noPatternMatchingOnCodata qs
reportSDoc "tc.lhs.top" 10 $
vcat [ text "checked lhs:"
, nest 2 $ vcat
[ text "ps = " <+> fsep (map prettyA ps)
, text "perm = " <+> text (show perm)
, text "delta = " <+> prettyTCM delta
, text "dpi = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi)
, text "asb = " <+> 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" 10 $ nest 2 $ text "type = " <+> prettyTCM b'
mapM_ checkDotPattern dpi
lhsResult <- return $ LHSResult delta qs b' 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 (iperm, ip) delta (ProblemRest (p:ps2) b) = problem
ps' = ps1
rest = ProblemRest ps2 (projPat $> projType)
ip' = ip ++ [fmap (Named Nothing . ProjP) projPat]
problem' = Problem ps' (iperm, ip') delta rest
st' <- updateProblemRest (LHSState problem' sigma dpi asb)
applyRelevanceToContext (getRelevance projPat) $ do
checkLHS f st'
trySplit (Split p0 xs (Arg _ (LitFocus lit iph hix a)) p1) _ = do
let ip = plugHole (LitP lit) iph
iperm = expandP hix 0 $ fst (problemOutPat problem)
let delta1 = problemTel p0
delta2 = absApp (fmap problemTel p1) (Lit lit)
rho = singletonS (size delta2) (Lit lit)
sigma' = applySubst rho sigma
dpi' = applySubst rho dpi
asb0 = applySubst rho asb
ip' = applySubst rho ip
rest' = applySubst rho (problemRest problem)
let ps' = problemInPat p0 ++ problemInPat (absBody p1)
delta' = abstract delta1 delta2
problem' = Problem ps' (iperm, 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 = iph
, focusHoleIx = hix
, 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
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 =" <+> prettyTCM typeOfSplitVar
, text "focusOutPat =" <+> (text . show) iph
, text "delta2 = " <+> prettyTCM (problemTel $ absBody p1)
]
]
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' == 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 d <+> text ":" <+> prettyTCM da
, text "gamma =" <+> prettyTCM gamma
, text "gamma' =" <+> prettyTCM gamma'
, text "vs =" <+> brackets (fsep $ punctuate comma $ map prettyTCM vs)
, text "us' =" <+> brackets (fsep $ punctuate comma $ map prettyTCM us')
, text "ws =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ws)
]
]
res <- addCtxTel (delta1 `abstract` gamma) $
unifyIndices flex (raise (size gamma) da) us' (raise (size gamma) ws)
whenUnifies res $ \ sub0 -> do
gamma <- return $ mapRelevance ignoreForced <$> gamma
let ys = teleArgs gamma
delta2 = absApp (raise (size gamma) $ fmap problemTel p1) (Con c ys)
rho0 = liftS (size delta2) $ consS (Con c ys) $ raiseS (size gamma)
sigma0 = applySubst rho0 sigma
dpi0 = applySubst rho0 dpi
asb0 = applySubst rho0 asb
rest0 = applySubst rho0 (problemRest problem)
reportSDoc "tc.lhs.top" 15 $ addCtxTel (delta1 `abstract` gamma) $ nest 2 $ vcat
[ text "delta2 =" <+> prettyTCM delta2
, text "sub0 =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub0)
]
reportSDoc "tc.lhs.top" 15 $ addCtxTel (delta1 `abstract` gamma `abstract` delta2) $
nest 2 $ vcat
[ text "dpi0 = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi0)
, text "asb0 = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb0)
]
let storedPatternType = raise (1 + size delta2) typeOfSplitVar
isRec <- isRecord d
let cpi = ConPatternInfo (isRec $> porigin) (Just storedPatternType)
let ysp = map (argFromDom . fmap (namedVarP . fst)) $ telToList gamma
ip = plugHole (ConP c cpi ysp) iph
ip0 = applySubst rho0 ip
let pad n xs x = xs ++ replicate (max 0 $ n size xs) x
newTel = problemTel p0 `abstract` (gamma `abstract` delta2)
sub = replicate (size delta2) Nothing ++
pad (size delta1 + size gamma) (raise (size delta2) sub0) Nothing
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ text "newTel =" <+> prettyTCM newTel
, addCtxTel newTel $ text "sub =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub)
, text "ip =" <+> do prettyList $ map (prettyTCM . namedArg) ip
, text "ip0 =" <+> do prettyList $ map (prettyTCM . namedArg) ip0
]
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ text "rho0 =" <+> text (show rho0)
]
(delta', perm, rho, instTypes) <- instantiateTel sub newTel
reportSDoc "tc.lhs.inst" 12 $
vcat [ sep [ text "instantiateTel"
, nest 4 $ brackets $ fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub
, nest 4 $ prettyTCM newTel
]
, nest 2 $ text "delta' =" <+> prettyTCM delta'
, nest 2 $ text "perm =" <+> text (show perm)
, nest 2 $ text "itypes =" <+> fsep (punctuate comma $ map prettyTCM instTypes)
]
let ps0' = problemInPat p0 ++ qs' ++ problemInPat (absBody p1)
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ text "subst rho sub =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) (applySubst rho sub))
, text "ps0' =" <+> brackets (fsep $ punctuate comma $ map prettyA ps0')
]
newDpi <- dotPatternInsts ps0' (applySubst rho sub) instTypes
let dpi' = applySubst rho dpi0 ++ newDpi
asb' = applySubst rho $ asb0 ++ raise (size delta2) (map (\x -> AsB x (Con c ys) ca) xs)
reportSDoc "tc.lhs.top" 15 $ 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 sigma0
rest' = applySubst rho rest0
reportSDoc "tc.lhs.inst" 15 $
nest 2 $ text "ps0 = " <+> brackets (fsep $ punctuate comma $ map prettyA ps0')
let ps' = permute perm ps0'
let perm' = expandP hix (size gamma) $ fst (problemOutPat problem)
iperm' = perm `composeP` perm'
let ip' = instantiatePattern sub perm' ip0
newip = applySubst rho ip'
let problem' = Problem ps' (iperm', newip) delta' rest'
reportSDoc "tc.lhs.top" 12 $ sep
[ text "new problem"
, nest 2 $ vcat
[ text "ps' = " <+> fsep (map prettyA ps')
, text "delta' = " <+> prettyTCM delta'
]
]
reportSDoc "tc.lhs.top" 14 $ nest 2 $ vcat
[ text "perm' =" <+> text (show perm')
, text "iperm' =" <+> text (show iperm')
]
reportSDoc "tc.lhs.top" 14 $ nest 2 $ vcat
[ text "ip' =" <+> prettyList (map (prettyTCM . namedArg) ip')
, text "newip =" <+> prettyList (map (prettyTCM . namedArg) newip)
]
reportSDoc "tc.lhs.top" 60 $ nest 2 $ vcat
[ text "ip' =" <+> text (show ip')
, text "newip =" <+> text (show newip)
]
st'@(LHSState problem'@(Problem ps' (iperm', 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' = " <+> prettyList (map (prettyTCM . namedArg) ip')
, text "iperm' = " <+> text (show iperm')
]
]
return $ Unifies st'
noPatternMatchingOnCodata :: [I.NamedArg Pattern] -> 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"