{-# LANGUAGE CPP #-} 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 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 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 {-# SOURCE #-} 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 {-# SOURCE #-} 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.ListT import Agda.Utils.Monad import Agda.Utils.Permutation import Agda.Utils.Size #include "undefined.h" import Agda.Utils.Impossible -- | Compute the set of flexible patterns in a list of patterns. The result is -- the deBruijn indices of the flexible patterns. A pattern is flexible if it -- is dotted or implicit. flexiblePatterns :: [A.NamedArg A.Pattern] -> TCM FlexibleVars flexiblePatterns nps = map setFlex <$> filterM (flexible . namedArg . snd) (zip [0..] $ reverse nps) where setFlex (i, Arg ai p) = FlexibleVar (getHiding ai) (classify $ namedThing p) i classify A.DotP{} = DotFlex classify A.ImplicitP{} = ImplicitFlex classify A.ConP{} = RecordFlex classify _ = __IMPOSSIBLE__ flexible (A.DotP _ _) = return True flexible (A.ImplicitP _) = return True flexible (A.ConP _ (A.AmbQ [c]) qs) = ifM (isJust <$> isRecordConstructor c) (andM $ map (flexible . namedArg) qs) (return False) flexible _ = return False -- | Compute the dot pattern instantiations. 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__ -- the substitution also contains entries for module parameters, so it can -- be longer than the pattern 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.ImplicitP _ -> dpi ps s as -- record pattern 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) -- Andreas, 2012-09-19 propagate relevance info to dot patterns bs = map (mapRelevance (composeRelevance (getRelevance a))) bs0 dpi (map namedArg qs ++ ps) (map (Just . unArg) us ++ s) (bs ++ as) _ -> __IMPOSSIBLE__ -- | In an internal pattern, replace some pattern variables -- by dot patterns, according to the given substitution. instantiatePattern :: Substitution -- ^ Partial substitution for the pattern variables, -- given in order of the clause telescope, -- (not in the order of occurrence in the patterns). -> Permutation -- ^ Map from the pattern variables to the telescope variables. -> [I.NamedArg Pattern] -- ^ Input patterns. -> [I.NamedArg Pattern] -- ^ Output patterns, with some @VarP@ replaced by @DotP@ -- according to the @Substitution@. 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 -- For each pattern variable get a copy of the patterns -- focusing on this variable. -- Order them in the dependency (telescope) order. hps = permute perm $ allHoles ps -- If we do not want to substitute a variable, we -- throw away the corresponding one-hole pattern. inst Nothing hps = Nothing -- If we want to substitute, we replace the variable -- by the dot pattern. inst (Just t) hps = Just $ plugHole (DotP t) hps -- If we did not instantiate a variable, we can keep the original -- patterns in this iteration. merge Nothing ps = ps -- Otherwise, we merge the changes in @qs@ into @ps@. -- This means we walk simultaneously through @qs@ and @ps@ -- and expect them to be the same everywhere except that -- a @q@ can be a @DotP@ and the corresponding @p@ a @VarP@. -- In this case, we take the @DotP@. -- Apparently, the other way round can also happen (why?). 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__ -- interesting cases: mergeP (DotP t) (VarP _) = DotP t mergeP (VarP _) (DotP t) = DotP t -- the rest is homomorphical 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) -- | In an internal pattern, replace some pattern variables -- by dot patterns, according to the given substitution. instantiatePattern' :: Substitution -- ^ Partial substitution for the pattern variables, -- given in order of the clause telescope, -- (not in the order of occurrence in the patterns). -> Permutation -- ^ Map from the pattern variables to the telescope variables. -> [I.NamedArg Pattern] -- ^ Input patterns. -> [I.NamedArg Pattern] -- ^ Output patterns, with some @VarP@ replaced by @DotP@ -- according to the @Substitution@. instantiatePattern' sub perm ps = evalState (mapM goArg ps) 0 where -- get a partial substitution from pattern variables to terms sub' = inversePermute perm sub -- get next pattern variable 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 return $ fromMaybe p $ DotP <$> sub' !! i -- | Check if a problem is solved. That is, if the patterns are all variables. isSolvedProblem :: Problem -> Bool isSolvedProblem problem = null (restPats $ problemRest problem) && all (isSolved . snd . asView . namedArg) (problemInPat problem) where isSolved (A.DefP _ _ []) = False -- projection pattern isSolved (A.VarP _) = True isSolved (A.WildP _) = True isSolved (A.ImplicitP _) = True isSolved (A.AbsurdP _) = True isSolved _ = False -- | For each user-defined pattern variable in the 'Problem', check -- that the corresponding data type (if any) does not contain a -- constructor of the same name (which is not in scope); this -- \"shadowing\" could indicate an error, and is not allowed. -- -- Precondition: The problem has to be solved. noShadowingOfConstructors :: (Maybe r -> Call) -- ^ Trace, e.g., @CheckPatternShadowing clause@ -> 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 -- TODO: does not work for flexible arity and projection patterns return () where noShadowing (A.WildP {}) t = return () noShadowing (A.AbsurdP {}) t = return () noShadowing (A.ImplicitP {}) t = return () noShadowing (A.ConP {}) t = return () -- only happens for eta expanded record patterns noShadowing (A.DefP {}) t = return () -- projection pattern 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 () -- TODO: If the type is a meta-variable, should the test be -- postponed? If there is a problem, then it will be caught when -- the completed module is type checked, so it is safe to skip -- the test here. However, users may be annoyed if they get an -- error in code which has already passed the type checker. Lam {} -> __IMPOSSIBLE__ Lit {} -> __IMPOSSIBLE__ Level {} -> __IMPOSSIBLE__ Con {} -> __IMPOSSIBLE__ DontCare{} -> __IMPOSSIBLE__ ExtLam{} -> __IMPOSSIBLE__ -- | Check that a dot pattern matches it's instantiation. 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 -- Should be ok to do noConstraints here noConstraints $ equalTerm a u v -- | Bind the variables in a left hand side. Precondition: the patterns should -- all be 'A.VarP', 'A.WildP', 'A.AbsurdP', or 'A.ImplicitP' and the -- telescope should have the same size as the pattern list. -- There could also be 'A.ConP's resulting from eta expanded implicit record -- patterns. 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 = case namedArg p of A.VarP x -> addContext (x, a) $ bindLHSVars ps (absBody tel) ret A.WildP _ -> bindDummy (absName tel) A.ImplicitP _ -> bindDummy (absName tel) A.AbsurdP pi -> do -- Andreas, 2012-03-15: allow postponement of emptyness check isEmptyType (getRange pi) $ unDom a -- OLD CODE: isReallyEmptyType $ unArg a bindDummy (absName tel) A.ConP _ (A.AmbQ [c]) qs -> do -- eta expanded record pattern 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] ] -- ^ TODO guilhem 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 -- | Bind as patterns 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 -- | Result of checking the LHS of a clause. data LHSResult = LHSResult { lhsVarTele :: Telescope -- ^ Δ : The types of the pattern variables, in internal dependency order. -- Corresponds to 'clauseTel'. , lhsPatterns :: [I.NamedArg Pattern] -- ^ The patterns in internal syntax. , lhsBodyType :: I.Arg Type -- ^ The type of the body. Is @bσ@ if @Γ@ is defined. -- 'Irrelevant' to indicate the rhs must be checked in irrelevant mode. , lhsPermutation :: Permutation -- ^ The permutation from pattern vars to @Δ@. -- Corresponds to 'clausePerm'. } instance InstantiateFull LHSResult where instantiateFull' (LHSResult tel ps t perm) = LHSResult <$> instantiateFull' tel <*> instantiateFull' ps <*> instantiateFull' t <*> return perm -- | Check a LHS. Main function. -- -- @checkLeftHandSide a ps a ret@ checks that user patterns @ps@ eliminate -- the type @a@ of the defined function, and calls continuation @ret@ -- if successful. checkLeftHandSide :: (Maybe r -> Call) -- ^ Trace, e.g. @CheckPatternShadowing clause@ -> Maybe QName -- ^ The name of the definition we are checking. -> [A.NamedArg A.Pattern] -- ^ The patterns. -> Type -- ^ The expected type @a = Γ → b@. -> (LHSResult -> TCM a) -- ^ Continuation. -> TCM a checkLeftHandSide c f ps a ret = do problem0 <- problemFromPats ps a -- Andreas, 2013-03-15 deactivating the following test allows -- flexible arity -- unless (noProblemRest problem) $ typeError $ TooManyArgumentsInLHS a -- doing the splits: 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' -- Check dot patterns mapM_ checkDotPattern dpi lhsResult <- return $ LHSResult delta qs b' perm applyRelevanceToContext (getRelevance b') $ ret lhsResult -- | The loop (tail-recursive): split at a variable in the problem until problem is solved checkLHS :: Maybe QName -- ^ The name of the definition we are checking. -> LHSState -- ^ The current state. -> TCM LHSState -- ^ The final state after all splitting is completed checkLHS f st@(LHSState problem sigma dpi asb) = do problem <- insertImplicitProblem problem -- Note: inserting implicits no longer preserve solvedness, -- since we might insert eta expanded record patterns. if isSolvedProblem problem then return $ st { lhsProblem = problem } else do unlessM (optPatternMatching <$> gets getPragmaOptions) $ typeError $ GenericError $ "Pattern matching is disabled" sp <- runListT $ splitProblem f problem reportSDoc "tc.lhs.split" 20 $ text "splitting completed" foldListT trySplit nothingToSplit $ ListT $ return sp where nothingToSplit = do reportSLn "tc.lhs.split" 50 $ "checkLHS: nothing to split in problem " ++ show problem nothingToSplitError problem -- Split problem rest (projection pattern) trySplit (SplitRest projPat projType) _ = do -- Compute the new problem let Problem ps1 (iperm, ip) delta (ProblemRest (p:ps2) b) = problem -- ps' = ps1 ++ [p] ps' = ps1 -- drop the projection pattern (already splitted) rest = ProblemRest ps2 (projPat $> projType) ip' = ip ++ [fmap (Named Nothing . ProjP) projPat] problem' = Problem ps' (iperm, ip') delta rest -- Jump the trampolin st' <- updateProblemRest (LHSState problem' sigma dpi asb) -- If the field is irrelevant, we need to continue in irr. cxt. -- (see Issue 939). applyRelevanceToContext (getRelevance projPat) $ do checkLHS f st' -- Split on literal pattern trySplit (Split p0 xs (Arg _ (LitFocus lit iph hix a)) p1) _ = do -- plug the hole with a lit pattern let ip = plugHole (LitP lit) iph iperm = expandP hix 0 $ fst (problemOutPat problem) -- substitute the literal in p1 and sigma and dpi and asb let delta1 = problemTel p0 delta2 = absApp (fmap problemTel p1) (Lit lit) rho = liftS (size delta2) $ singletonS (Lit lit) -- rho = [ var i | i <- [0..size delta2 - 1] ] -- ++ [ raise (size delta2) $ Lit lit ] -- ++ [ var i | i <- [size delta2 ..] ] sigma' = applySubst rho sigma dpi' = applySubst rho dpi asb0 = applySubst rho asb ip' = applySubst rho ip rest' = applySubst rho (problemRest problem) -- Compute the new 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' -- Split on constructor pattern trySplit (Split p0 xs focus@(Arg info Focus{}) p1) tryNextSplit = do res <- trySplitConstructor p0 xs focus p1 case res of -- Success. Continue checking LHS. Unifies st' -> checkLHS f st' -- Mismatch. Report and abort. NoUnify tcerr -> throwError tcerr -- Unclear situation. Try next split. -- If no split works, give error from first split. -- This is conservative, but might not be the best behavior. -- It might be better to collect all the errors and print all of them. 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 , focusImplicit = impl , focusConArgs = qs , focusRange = r , focusOutPat = iph , focusHoleIx = hix , focusDatatype = d , focusParams = vs , focusIndices = ws , focusType = a } )) p1 = do traceCall (CheckPattern (A.ConP (ConPatInfo impl $ 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) ] -- Lookup the type of the constructor at the given parameters let a = ca `piApply` vs -- It will end in an application of the datatype (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) -- This should be the same datatype as we split on unless (d == d') $ typeError $ ShouldBeApplicationOf ca d' -- reportSDoc "tc.lhs.top" 20 $ nest 2 $ vcat -- [ text "gamma' =" <+> text (show gamma') -- ] -- Andreas 2010-09-07 propagate relevance info to new vars let updRel = composeRelevance (getRelevance info) gamma' <- return $ mapRelevance updRel <$> gamma' -- Insert implicit patterns qs' <- insertImplicitPatterns ExpandLast qs gamma' unless (size qs' == size gamma') $ typeError $ WrongNumberOfConstructorArguments (conName c) (size gamma') (size qs') let gamma = useNamesFromPattern qs' gamma' -- Get the type of the datatype. da <- (`piApply` vs) . defType <$> getConstInfo d -- Compute the flexible variables flex <- flexiblePatterns (problemInPat p0 ++ qs') -- Compute the constructor indices by dropping the parameters 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) ] ] -- Unify constructor target and given type (in Δ₁Γ) res <- addCtxTel (delta1 `abstract` gamma) $ unifyIndices flex (raise (size gamma) da) us' (raise (size gamma) ws) whenUnifies res $ \ sub0 -> do -- Andreas 2014-11-25 clear 'Forced' and 'Unused' -- Andreas 2015-01-19 ... only after unification gamma <- return $ mapRelevance ignoreForced <$> gamma -- We should substitute c ys for x in Δ₂ and sigma 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) -- rho0 = [ var i | i <- [0..size delta2 - 1] ] -- ++ [ raise (size delta2) $ Con c ys ] -- ++ [ var i | i <- [size delta2 + 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) ] -- Andreas, 2010-09-09, save the type. -- It is relative to delta1, but it should be relative to -- all variables which will be bound by patterns. -- Thus, it has to be raised by 1 (the "hole" variable) -- plus the length of delta2 (the variables coming after the hole). let storedPatternType = raise (1 + size delta2) typeOfSplitVar -- Also remember if we are a record pattern and from an implicit pattern. isRec <- isRecord d let cpi = ConPatternInfo (isRec $> impl) (Just storedPatternType) -- Plug the hole in the out pattern with c ys let ysp = map (argFromDom . fmap (namedVarP . fst)) $ telToList gamma ip = plugHole (ConP c cpi ysp) iph ip0 = applySubst rho0 ip -- Δ₁Γ ⊢ sub0, we need something in Δ₁ΓΔ₂ -- Also needs to be padded with Nothing's to have the right length. 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 =" <+> text (show ip) , text "ip0 =" <+> text (show ip0) ] reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat [ text "rho0 =" <+> text (show rho0) ] -- Instantiate the new telescope with the given substitution (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) ] {- -- Andreas, 2010-09-09 -- temporary error message to find non-id perms let sorted (Perm _ xs) = xs == List.sort xs unless (sorted (perm)) $ typeError $ GenericError $ "detected proper permutation " ++ show perm -} -- Compute the new dot pattern instantiations 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 -- The final dpis and asbs are the new ones plus the old ones substituted by ρ 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') ] -- Apply the substitution to the type 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') -- Permute the in patterns let ps' = permute perm ps0' -- Compute the new permutation of the out patterns. This is the composition of -- the new permutation with the expansion of the old permutation to -- reflect the split. let perm' = expandP hix (size gamma) $ fst (problemOutPat problem) iperm' = perm `composeP` perm' -- Instantiate the out patterns let ip' = instantiatePattern sub perm' ip0 newip = applySubst rho ip' -- Construct the new problem 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' =" <+> text (show ip') , text "newip =" <+> text (show newip) ] -- if rest type reduces, -- extend the split problem by previously not considered patterns 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' =" <+> text (show ip') , text "iperm' =" <+> text (show iperm') ] ] return $ Unifies st' -- | Ensures that we are not performing pattern matching on codata. noPatternMatchingOnCodata :: [I.NamedArg Pattern] -> TCM () noPatternMatchingOnCodata = mapM_ (check . namedArg) where check (VarP {}) = return () check (DotP {}) = return () check (ProjP{}) = return () check (LitP {}) = return () -- Literals are assumed not to be coinductive. 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"