{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE TypeSynonymInstances #-} 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 {-# 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.List 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. 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 -- | A pattern is flexible if it is dotted or implicit, or a record pattern -- with only flexible subpatterns. 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 {-else-} (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 -- expanded from ImplicitP | Just _ <- conPRecord i -> maybeFlexiblePattern ps | otherwise -> mzero I.VarP{} -> mzero I.LitP{} -> mzero I.ProjP{} -> mzero -- | Lists of flexible patterns are 'RecordFlex'. 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 -- | 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.WildP _ -> 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 let s = case sub' !!! i of Nothing -> __IMPOSSIBLE__ Just s -> s return $ fromMaybe p $ DotP <$> s -- | 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 -- need further splitting: isSolved A.ConP{} = False isSolved A.DotP{} = False isSolved A.LitP{} = False isSolved A.DefP{} = False -- projection pattern -- solved: isSolved A.VarP{} = True isSolved A.WildP{} = True isSolved A.AbsurdP{} = True -- impossible: isSolved A.AsP{} = __IMPOSSIBLE__ -- removed by asView isSolved A.PatternSynP{} = __IMPOSSIBLE__ -- expanded before -- | 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 :: 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.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 and check that 'Hiding' of -- the patterns matches the hiding info in the type. -- -- Precondition: the patterns should -- all be 'A.VarP', 'A.WildP', or 'A.AbsurdP' 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 = 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) -- @bindDummy underscore@ does not fix issue 819, but -- introduces unwanted underscores in error messages -- (Andreas, 2015-05-28) 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 :: 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" foldListT trySplit nothingToSplit $ splitProblem f problem where nothingToSplit = do reportSLn "tc.lhs.split" 50 $ "checkLHS: nothing to split in problem " ++ show problem nothingToSplitError problem -- Split problem rest (projection pattern, does not fail as there is no call to unifier) 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 (does not fail as there is no call to unifier) 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 = singletonS (size delta2) (Lit lit) -- Andreas, 2015-06-13 Literals are closed, so need to raise them! -- rho = liftS (size delta2) $ singletonS 0 (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 (unifier might fail) 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 , 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) ] -- 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 $> porigin) (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 =" <+> 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) ] -- 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' =" <+> 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) ] -- 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' = " <+> prettyList (map (prettyTCM . namedArg) 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"