module Agda.TypeChecking.Rules.LHS where
import Data.Maybe
import qualified Data.List as List
import Control.Applicative
import Control.Monad
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute hiding (Substitution)
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Primitive (constructorForm)
import Agda.TypeChecking.Empty (isReallyEmptyType)
import Agda.TypeChecking.Telescope (renamingR, teleArgs)
import Agda.TypeChecking.Rules.Term (checkExpr)
import Agda.TypeChecking.Rules.LHS.Problem
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.Permutation
import Agda.Utils.Size
import Agda.Utils.Monad
#include "../../undefined.h"
import Agda.Utils.Impossible
data DotPatternInst = DPI A.Expr Term Type
data AsBinding = AsB Name Term Type
instance Subst DotPatternInst where
substs us (DPI e v a) = uncurry (DPI e) $ substs us (v,a)
substUnder n u (DPI e v a) = uncurry (DPI e) $ substUnder n u (v,a)
instance PrettyTCM DotPatternInst where
prettyTCM (DPI e v a) = sep [ prettyA e <+> text "="
, nest 2 $ prettyTCM v <+> text ":"
, nest 2 $ prettyTCM a
]
instance Subst AsBinding where
substs us (AsB x v a) = uncurry (AsB x) $ substs us (v, a)
substUnder n u (AsB x v a) = uncurry (AsB x) $ substUnder n u (v, a)
instance Raise AsBinding where
raiseFrom m k (AsB x v a) = uncurry (AsB x) $ raiseFrom m k (v, a)
renameFrom m k (AsB x v a) = uncurry (AsB x) $ renameFrom m k (v, a)
instance PrettyTCM AsBinding where
prettyTCM (AsB x v a) =
sep [ prettyTCM x <> text "@" <> parens (prettyTCM v)
, nest 2 $ text ":" <+> prettyTCM a
]
flexiblePatterns :: [NamedArg A.Pattern] -> FlexibleVars
flexiblePatterns nps = [ i | (i, p) <- zip [0..] $ reverse ps, flexible p ]
where
ps = map (namedThing . unArg) nps
flexible (A.DotP _ _) = True
flexible (A.ImplicitP _) = True
flexible _ = False
dotPatternInsts :: [NamedArg A.Pattern] -> Substitution -> [Type] -> [DotPatternInst]
dotPatternInsts ps s as = dpi (map (namedThing . unArg) ps) (reverse s) as
where
dpi (_ : _) [] _ = __IMPOSSIBLE__
dpi (_ : _) (Just _ : _) [] = __IMPOSSIBLE__
dpi [] _ _ = []
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
_ -> __IMPOSSIBLE__
instantiatePattern :: Substitution -> Permutation -> [Arg Pattern] -> [Arg 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 = a1 { unArg = mergeP (unArg a1) (unArg a2) }
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 mt1 ps) (ConP c2 mt2 qs)
| c1 == c2 = ConP (c1 `withRangeOf` c2) (mplus mt1 mt2) $ 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__
isSolvedProblem :: Problem -> Bool
isSolvedProblem = all (isVar . snd . asView . namedThing . unArg) . problemInPat
where
isVar (A.VarP _) = True
isVar (A.WildP _) = True
isVar (A.ImplicitP _) = True
isVar (A.AbsurdP _) = True
isVar _ = False
noShadowingOfConstructors
:: A.Clause
-> Problem -> TCM ()
noShadowingOfConstructors c problem =
traceCall (CheckPatternShadowing c) $ do
let pat = map (snd . asView . namedThing . unArg) $
problemInPat problem
tel = map (unEl . snd . unArg) $ telToList $ problemTel problem
zipWithM' noShadowing pat tel
return ()
where
noShadowing (A.WildP {}) t = return ()
noShadowing (A.AbsurdP {}) t = return ()
noShadowing (A.ImplicitP {}) t = return ()
noShadowing (A.ConP {}) t = __IMPOSSIBLE__
noShadowing (A.DefP {}) t = __IMPOSSIBLE__
noShadowing (A.AsP {}) t = __IMPOSSIBLE__
noShadowing (A.DotP {}) t = __IMPOSSIBLE__
noShadowing (A.LitP {}) t = __IMPOSSIBLE__
noShadowing (A.VarP x) t = do
t <- normalise t
case t of
Def t _ -> do
d <- theDef <$> getConstInfo t
case d of
Datatype { dataCons = cs } -> do
let ns = map (\c -> (c, A.nameConcrete $ A.qnameName c)) cs
match x = catMaybes $
map (\(c, n) -> if A.nameConcrete x == n
then Just c else Nothing) ns
case match x of
[] -> return ()
(c : _) -> setCurrentRange (getRange x) $
typeError $ PatternShadowsConstructor x c
Axiom {} -> return ()
Function {} -> return ()
Record {} -> return ()
Constructor {} -> __IMPOSSIBLE__
Primitive {} -> __IMPOSSIBLE__
Var {} -> return ()
Pi {} -> return ()
Sort {} -> return ()
MetaV {} -> return ()
Lam {} -> __IMPOSSIBLE__
Lit {} -> __IMPOSSIBLE__
Level {} -> __IMPOSSIBLE__
Con {} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
checkDotPattern :: DotPatternInst -> TCM ()
checkDotPattern (DPI e v 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
]
u <- checkExpr e a
noConstraints $ equalTerm a u v
bindLHSVars :: [NamedArg A.Pattern] -> Telescope -> TCM a -> TCM a
bindLHSVars [] (ExtendTel _ _) _ = __IMPOSSIBLE__
bindLHSVars (_ : _) EmptyTel _ = __IMPOSSIBLE__
bindLHSVars [] EmptyTel ret = ret
bindLHSVars (p : ps) (ExtendTel a tel) ret =
case namedThing $ unArg p of
A.VarP x -> addCtx x a $ bindLHSVars ps (absBody tel) ret
A.WildP _ -> bindDummy (absName tel)
A.ImplicitP _ -> bindDummy (absName tel)
A.AbsurdP _ -> do
isReallyEmptyType $ unArg a
bindDummy (absName tel)
_ -> __IMPOSSIBLE__
where
name "_" = freshNoName_
name s = freshName_ ("." ++ s)
bindDummy s = do
x <- name s
addCtx 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 Relevant x v a $ bindAsPatterns asb ret
useNamesFromPattern :: [NamedArg A.Pattern] -> Telescope -> Telescope
useNamesFromPattern ps = telFromList . zipWith ren (toPats ps ++ repeat dummy) . telToList
where
dummy = A.WildP __IMPOSSIBLE__
ren (A.VarP x) (Arg NotHidden r (_, a)) = Arg NotHidden r (show x, a)
ren _ a = a
toPats = map (namedThing . unArg)
checkLeftHandSide
:: A.Clause
-> [NamedArg A.Pattern]
-> Type
-> (Telescope -> Telescope -> [Term] -> [String] -> [Arg Pattern]
-> Type -> Permutation -> TCM a)
-> TCM a
checkLeftHandSide c ps a ret = do
TelV tel0' b0 <- telView a
ps <- insertImplicitPatterns ps tel0'
unless (size tel0' >= size ps) $ typeError $ TooManyArgumentsInLHS (size ps) a
let tel0 = useNamesFromPattern ps tel0'
(as, bs) = splitAt (size ps) $ telToList tel0
gamma = telFromList as
b = telePi (telFromList bs) b0
ips = map (fmap (VarP . fst)) as
problem = Problem ps (idP $ size ps, ips) gamma
reportSDoc "tc.lhs.top" 10 $
vcat [ text "checking lhs:"
, nest 2 $ vcat
[ text "ps =" <+> fsep (map prettyA ps)
, text "a =" <+> (prettyTCM =<< normalise a)
, text "a' =" <+> prettyTCM (telePi tel0 b0)
, text "a'' =" <+> prettyTCM (telePi tel0' b0)
, text "xs =" <+> text (show $ map (fst . unArg) as)
, text "tel0 =" <+> prettyTCM tel0
, text "b0 =" <+> prettyTCM b0
, text "gamma =" <+> prettyTCM gamma
, text "b =" <+> addCtxTel gamma (prettyTCM b)
]
]
let idsub = [ Var i [] | i <- [0..] ]
(Problem ps (perm, qs) delta, sigma, dpi, asb) <- checkLHS problem idsub [] []
let b' = substs sigma b
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)
]
]
bindLHSVars ps delta $ bindAsPatterns asb $ do
reportSDoc "tc.lhs.top" 10 $ nest 2 $ text "type = " <+> prettyTCM b'
mapM_ checkDotPattern dpi
let rho = renamingR perm
Perm n _ = perm
xs = [ "h" ++ show n | n <- [0..n 1] ]
ret gamma delta rho xs qs b' perm
where
checkLHS :: Problem -> [Term] -> [DotPatternInst] -> [AsBinding] ->
TCM (Problem, [Term], [DotPatternInst], [AsBinding])
checkLHS problem sigma dpi asb
| isSolvedProblem problem = do
problem <- insertImplicitProblem problem
noShadowingOfConstructors c problem
return (problem, sigma, dpi, asb)
| otherwise = do
sp <- splitProblem =<< insertImplicitProblem problem
reportSDoc "tc.lhs.top" 20 $ text "splitting completed"
case sp of
Left NothingToSplit -> nothingToSplitError problem
Left (SplitPanic err) -> __IMPOSSIBLE__
Right (Split p0 xs (Arg _ _ (LitFocus lit iph hix a)) p1) -> do
let ip = plugHole (LitP lit) iph
iperm = expandP (fromIntegral hix) 0 $ fst (problemOutPat problem)
let delta1 = problemTel p0
delta2 = absApp (fmap problemTel p1) (Lit lit)
rho = [ var i | i <- [0..size delta2 1] ]
++ [ raise (size delta2) $ Lit lit ]
++ [ var i | i <- [size delta2 ..] ]
where
var i = Var i []
sigma' = substs rho sigma
dpi' = substs rho dpi
asb0 = substs rho asb
ip' = substs rho ip
let ps' = problemInPat p0 ++ problemInPat (absBody p1)
delta' = abstract delta1 delta2
problem' = Problem ps' (iperm, ip') delta'
asb' = raise (size delta2) (map (\x -> AsB x (Lit lit) a) xs) ++ asb0
checkLHS problem' sigma' dpi' asb'
Right (Split p0 xs (Arg h rel
( Focus { focusCon = c
, focusConArgs = qs
, focusRange = r
, focusOutPat = iph
, focusHoleIx = hix
, focusDatatype = d
, focusParams = vs
, focusIndices = ws
, focusType = a
}
)) p1
) -> traceCall (CheckPattern (A.ConP (PatRange r) (A.AmbQ [c]) qs)
(problemTel p0)
(El Prop $ Def d $ vs ++ ws)) $ do
let delta1 = problemTel p0
let typeOfSplitVar = Arg h rel a
reportSDoc "tc.lhs.top" 10 $ sep
[ text "checking lhs"
, nest 2 $ text "tel =" <+> prettyTCM (problemTel problem)
, nest 2 $ text "rel =" <+> (text $ show rel)
]
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)
]
]
Con c' [] <- constructorForm =<< normalise (Con c [])
c <- return $ c' `withRangeOf` c
ca <- defType <$> getConstInfo c
reportSDoc "tc.lhs.top" 20 $ nest 2 $ vcat
[ text "ca =" <+> prettyTCM ca
, text "vs =" <+> prettyList (map prettyTCM vs)
]
let a = ca `piApply` vs
TelV gamma' ca@(El _ (Def d' us)) <- telView a
unless (d == d') $ typeError $ ShouldBeApplicationOf ca d'
gamma' <- return $ fmap (applyRelevance rel) gamma'
qs' <- insertImplicitPatterns qs gamma'
unless (size qs' == size gamma') $
typeError $ WrongNumberOfConstructorArguments c (size gamma') (size qs')
let gamma = useNamesFromPattern qs' gamma'
da <- (`piApply` vs) . defType <$> getConstInfo d
let flex = flexiblePatterns (problemInPat p0 ++ qs')
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 "ws =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ws)
]
]
sub0 <- addCtxTel (delta1 `abstract` gamma) $
unifyIndices_ flex (raise (size gamma) da) (drop (size vs) us) (raise (size gamma) ws)
let ys = teleArgs gamma
delta2 = absApp (raise (size gamma) $ fmap problemTel p1) (Con c ys)
rho0 = [ var i | i <- [0..size delta2 1] ]
++ [ raise (size delta2) $ Con c ys ]
++ [ var i | i <- [size delta2 + size gamma ..] ]
where
var i = Var i []
sigma0 = substs rho0 sigma
dpi0 = substs rho0 dpi
asb0 = substs rho0 asb
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)
]
storedPatternType <- ifM (isRecord d)
(return $ Just $ raise (1 + size delta2) $ typeOfSplitVar)
(return $ Nothing)
let ysp = map (fmap (VarP . fst)) $ telToList gamma
ip = plugHole (ConP c storedPatternType ysp) iph
ip0 = substs 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 =" <+> text (show ip)
, text "ip0 =" <+> text (show ip0)
]
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ text "rho0 =" <+> text (show $ take (size delta1 + size gamma + size delta2) 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)
newDpi = dotPatternInsts ps0' (substs rho sub) instTypes
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ text "subst rho sub =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) (substs rho sub))
, text "ps0' =" <+> brackets (fsep $ punctuate comma $ map prettyA ps0')
]
let dpi' = substs rho dpi0 ++ newDpi
asb' = substs 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' = substs rho sigma0
reportSDoc "tc.lhs.inst" 15 $
nest 2 $ text "ps0 = " <+> brackets (fsep $ punctuate comma $ map prettyA ps0')
let ps' = permute perm ps0'
let perm' = expandP (fromIntegral hix) (size gamma) $ fst (problemOutPat problem)
iperm' = perm `composeP` perm'
let ip' = instantiatePattern sub perm' ip0
newip = substs rho ip'
let problem' = Problem ps' (iperm', newip) delta'
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)
]
checkLHS problem' sigma' dpi' asb'
noPatternMatchingOnCodata :: [Arg Pattern] -> TCM ()
noPatternMatchingOnCodata = mapM_ (check . unArg)
where
check (VarP {}) = return ()
check (DotP {}) = return ()
check (LitP {}) = return ()
check (ConP q _ ps) = do
TelV _ t <- telView' . defType <$> getConstInfo q
c <- isCoinductive t
case c of
Nothing -> __IMPOSSIBLE__
Just False -> mapM_ (check . unArg) ps
Just True -> typeError $
GenericError "Pattern matching on codata is not allowed"