module Agda.TypeChecking.With where
import Control.Arrow ((&&&), (***), first, second)
import Control.Applicative hiding (empty)
import Control.Monad
import Control.Monad.Writer (WriterT, runWriterT, tell)
import Data.Either
import qualified Data.List as List
import Data.Maybe
import Data.Monoid
import Data.Traversable (traverse)
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Info
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Free
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.ReconstructParameters
import Agda.TypeChecking.Abstract
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Rules.LHS (isFlexiblePattern)
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null (empty)
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
splitTelForWith
:: Telescope
-> Type
-> [EqualityView]
-> [Term]
-> ( Telescope
, Telescope
, Permutation
, Type
, [EqualityView]
, [Term]
)
splitTelForWith delta t as vs = let
rewriteTerms = map snd $ filter (isEqualityType . fst) $ zip as vs
fv = allFreeVars (as, vs)
SplitTel delta1 delta2 perm = splitTelescope fv delta
pi = renaming __IMPOSSIBLE__ (reverseP perm)
rho = strengthenS __IMPOSSIBLE__ $ size delta2
rhopi = composeS rho pi
t' = applySubst pi t
as' = applySubst rhopi as
vs' = applySubst rhopi vs
in (delta1, delta2, perm, t', as', vs')
withFunctionType
:: Telescope
-> [Term]
-> [EqualityView]
-> Telescope
-> Type
-> TCM (Type, Nat)
withFunctionType delta1 vs as delta2 b = addContext delta1 $ do
reportSLn "tc.with.abstract" 20 $ "preparing for with-abstraction"
let dbg n s x = reportSDoc "tc.with.abstract" n $ nest 2 $ text (s ++ " =") <+> prettyTCM x
let d2b = telePi_ delta2 b
dbg 30 "Δ₂ → B" d2b
d2b <- normalise d2b
dbg 30 "normal Δ₂ → B" d2b
d2b <- etaContract d2b
dbg 30 "eta-contracted Δ₂ → B" d2b
vs <- etaContract =<< normalise vs
as <- etaContract =<< normalise as
let piAbstractVs [] b = return b
piAbstractVs (va : vas) b = piAbstract va =<< piAbstractVs vas b
wd2b <- piAbstractVs (zip vs as) d2b
dbg 30 "wΓ → Δ₂ → B" wd2b
return (telePi_ delta1 wd2b, countWithArgs as)
countWithArgs :: [EqualityView] -> Nat
countWithArgs = sum . map countArgs
where
countArgs OtherType{} = 1
countArgs EqualityType{} = 2
withArguments :: [Term] -> [EqualityView] -> [Term]
withArguments vs as = concat $ for (zip vs as) $ \case
(v, OtherType a) -> [v]
(prf, eqt@(EqualityType s _eq _pars _t v _v')) -> [unArg v, prf]
buildWithFunction
:: [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Nat
-> Substitution
-> Permutation
-> Nat
-> Nat
-> [A.SpineClause]
-> TCM [A.SpineClause]
buildWithFunction cxtNames f aux t delta qs npars withSub perm n1 n cs = mapM buildWithClause cs
where
buildWithClause (A.Clause (A.SpineLHS i _ ps wps) inheritedDots rhs wh catchall) = do
let (wps0, wps1) = splitAt n wps
ps0 = map defaultNamedArg wps0
reportSDoc "tc.with" 50 $ text "inheritedDots:" <+> vcat [ prettyTCM x <+> text "=" <+> prettyTCM v <+> text ":" <+> prettyTCM a
| A.NamedDot x v a <- inheritedDots ]
rhs <- buildRHS rhs
(namedDots, ps') <- stripWithClausePatterns cxtNames f aux t delta qs npars perm ps
let (ps1, ps2) = splitAt n1 ps'
let result = A.Clause (A.SpineLHS i aux (ps1 ++ ps0 ++ ps2) wps1) (inheritedDots ++ namedDots) rhs wh catchall
reportSDoc "tc.with" 20 $ vcat
[ text "buildWithClause returns" <+> prettyA result
]
return result
buildRHS rhs@A.RHS{} = return rhs
buildRHS rhs@A.AbsurdRHS = return rhs
buildRHS (A.WithRHS q es cs) = A.WithRHS q es <$>
mapM ((A.spineToLhs . permuteNamedDots) <.> buildWithClause . A.lhsToSpine) cs
buildRHS (A.RewriteRHS qes rhs wh) = flip (A.RewriteRHS qes) wh <$> buildRHS rhs
permuteNamedDots :: A.SpineClause -> A.SpineClause
permuteNamedDots (A.Clause lhs dots rhs wh catchall) =
A.Clause lhs (applySubst withSub dots) rhs wh catchall
stripWithClausePatterns
:: [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Nat
-> Permutation
-> [NamedArg A.Pattern]
-> TCM ([A.NamedDotPattern], [NamedArg A.Pattern])
stripWithClausePatterns cxtNames parent f t delta qs npars perm ps = do
ps <- expandPatternSynonyms ps
let paramPat i _ = A.VarP (cxtNames !! i)
ps' = zipWith (fmap . fmap . paramPat) [0..] (take npars qs) ++ ps
psi <- insertImplicitPatternsT ExpandLast ps' t
reportSDoc "tc.with.strip" 10 $ vcat
[ text "stripping patterns"
, nest 2 $ text "t = " <+> prettyTCM t
, nest 2 $ text "ps = " <+> fsep (punctuate comma $ map prettyA ps)
, nest 2 $ text "ps' = " <+> fsep (punctuate comma $ map prettyA ps')
, nest 2 $ text "psi = " <+> fsep (punctuate comma $ map prettyA psi)
, nest 2 $ text "qs = " <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs)
, nest 2 $ text "perm= " <+> text (show perm)
]
(ps', namedDots) <- runWriterT $ strip (Def parent []) t psi qs
reportSDoc "tc.with.strip" 50 $ nest 2 $
text "namedDots:" <+> vcat [ prettyTCM x <+> text "=" <+> prettyTCM v <+> text ":" <+> prettyTCM a | A.NamedDot x v a <- namedDots ]
let psp = permute perm ps'
reportSDoc "tc.with.strip" 10 $ vcat
[ nest 2 $ text "ps' = " <+> fsep (punctuate comma $ map prettyA ps')
, nest 2 $ text "psp = " <+> fsep (punctuate comma $ map prettyA $ psp)
]
if True then return (namedDots, psp) else do
forM_ (permute (droppedP perm) ps') $ \ p -> setCurrentRange p $ do
reportSDoc "tc.with.strip" 10 $ text "warning: dropped pattern " <+> prettyA p
reportSDoc "tc.with.strip" 60 $ text $ show p
case namedArg p of
A.DotP info o e -> case unScope e of
A.Underscore{} -> return ()
e | o == UserWritten -> typeError $ GenericError $
"This inaccessible pattern is never checked, so only _ allowed here"
_ -> return ()
_ -> return ()
return (namedDots, psp)
where
strip
:: Term
-> Type
-> [NamedArg A.Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [A.NamedDotPattern] TCM [NamedArg A.Pattern]
strip self t [] qs@(_ : _) = do
reportSDoc "tc.with.strip" 15 $ vcat
[ text "strip (out of A.Patterns)"
, nest 2 $ text "qs =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs)
, nest 2 $ text "self=" <+> prettyTCM self
, nest 2 $ text "t =" <+> prettyTCM t
]
ps <- liftTCM $ insertImplicitPatternsT ExpandLast [] t
if null ps then
typeError $ GenericError $ "Too few arguments given in with-clause"
else strip self t ps qs
strip _ _ ps [] = do
let implicit (A.WildP{}) = True
implicit (A.ConP ci _ _) = patOrigin ci == ConOSystem
implicit _ = False
unless (all (implicit . namedArg) ps) $
typeError $ GenericError $ "Too many arguments given in with-clause"
return []
strip self t (p0 : ps) qs@(q : _)
| A.AsP _ x p <- namedArg p0 = do
(a, _) <- mustBePi t
let v = patternToTerm (namedArg q)
tell [A.NamedDot x v (unDom a)]
strip self t (fmap (p <$) p0 : ps) qs
strip self t ps0@(p0 : ps) qs0@(q : qs) = do
p <- liftTCM $ expandLitPattern p0
reportSDoc "tc.with.strip" 15 $ vcat
[ text "strip"
, nest 2 $ text "ps0 =" <+> fsep (punctuate comma $ map prettyA ps0)
, nest 2 $ text "exp =" <+> prettyA p
, nest 2 $ text "qs0 =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs0)
, nest 2 $ text "self=" <+> prettyTCM self
, nest 2 $ text "t =" <+> prettyTCM t
]
let failDotPat :: Monoid w => WriterT w TCM a
failDotPat = do
d <- liftTCM $ prettyA p
typeError $ GenericError $
"Inaccessible (dotted) patterns from the parent clause must " ++
"also be inaccessible in the with clause, when checking the " ++
"pattern " ++ show d ++ ","
case namedArg q of
ProjP o d -> case A.maybePostfixProjP p of
Just (o', AmbQ ds) -> do
d <- liftTCM $ getOriginalProjection d
found <- anyM ds ((d ==) <.> (liftTCM . getOriginalProjection))
if o /= o' then liftTCM $ mismatchOrigin o o' else do
if not found then mismatch else do
(self1, t1, ps) <- liftTCM $ do
t <- reduce t
(_, self1, t1) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped self t o d
ps <- insertImplicitPatternsT ExpandLast ps t1
return (self1, t1, ps)
strip self1 t1 ps qs
Nothing -> mismatch
VarP x -> (p :) <$> recurse (var (dbPatVarIndex x))
AbsurdP p -> __IMPOSSIBLE__
DotP v -> case namedArg p of
A.DotP r o _ -> ok p
A.WildP _ -> ok p
A.VarP x -> do
(a, _) <- mustBePi t
tell [A.NamedDot x v (unDom a)]
ok p
A.ConP ci _ _ | patOrigin ci == ConOSystem -> okFlex p
p'@A.ConP{} -> ifM (liftTCM $ isFlexiblePattern p') (okFlex p) failDotPat
p@(A.PatternSynP pi' c' [ps']) -> do
reportSDoc "impossible" 10 $
text "stripWithClausePatterns: encountered pattern synonym " <+> prettyA p
__IMPOSSIBLE__
_ -> failDotPat
where
okFlex = ok . makeImplicitP
ok p = (p :) <$> recurse v
q'@(ConP c ci qs') -> do
reportSDoc "tc.with.strip" 60 $
text "parent pattern is constructor " <+> prettyTCM c
(a, b) <- mustBePi t
Def d es <- liftTCM $ ignoreSharing <$> normalise (unEl $ unDom a)
let us = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
c <- either __IMPOSSIBLE__ (`withRangeOf` c) <$> do liftTCM $ getConForm $ conName c
case namedArg p of
A.DotP{} -> ifNotM (liftTCM $ isFlexiblePattern q') mismatch $ do
maybe __IMPOSSIBLE__ (\ p -> strip self t (p : ps) qs0) =<< do
liftTCM $ expandImplicitPattern' (unDom a) $ makeImplicitP p
A.WildP{} -> do
let ps' = map (updateNamedArg $ const $ A.WildP empty) qs'
stripConP d us b c ConOCon qs' ps'
A.ConP _ (A.AmbQ cs') ps' -> do
cs' <- liftTCM $ do snd . partitionEithers <$> mapM getConForm cs'
unless (elem c cs') mismatch
stripConP d us b c ConOCon qs' ps'
A.RecP _ fs -> caseMaybeM (liftTCM $ isRecord d) mismatch $ \ def -> do
ps' <- liftTCM $ insertMissingFields d (const $ A.WildP empty) fs (recordFieldNames def)
stripConP d us b c ConORec qs' ps'
p@(A.PatternSynP pi' c' ps') -> do
reportSDoc "impossible" 10 $
text "stripWithClausePatterns: encountered pattern synonym " <+> prettyA p
__IMPOSSIBLE__
p -> do
reportSDoc "tc.with.strip" 60 $
text $ "with clause pattern is " ++ show p
mismatch
LitP lit -> case namedArg p of
A.LitP lit' | lit == lit' -> recurse $ Lit lit
A.WildP{} -> recurse $ Lit lit
p@(A.PatternSynP pi' c' [ps']) -> do
reportSDoc "impossible" 10 $
text "stripWithClausePatterns: encountered pattern synonym " <+> prettyA p
__IMPOSSIBLE__
_ -> mismatch
where
recurse v = do
t' <- piApply1 t v
strip (self `apply1` v) t' ps qs
mismatch = addContext delta $ typeError $
WithClausePatternMismatch (namedArg p0) q
mismatchOrigin o o' = addContext delta . typeError . GenericDocError =<< fsep
[ text "With clause pattern"
, prettyA p0
, text "is not an instance of its parent pattern"
, P.fsep <$> prettyTCMPatterns [q]
, text $ "since the parent pattern is " ++ prettyProjOrigin o ++
" and the with clause pattern is " ++ prettyProjOrigin o'
]
prettyProjOrigin ProjPrefix = "a prefix projection"
prettyProjOrigin ProjPostfix = "a postfix projection"
prettyProjOrigin ProjSystem = __IMPOSSIBLE__
makeImplicitP :: NamedArg A.Pattern -> NamedArg A.Pattern
makeImplicitP = updateNamedArg $ const $ A.WildP patNoRange
stripConP
:: QName
-> [Arg Term]
-> Abs Type
-> ConHead
-> ConInfo
-> [NamedArg DeBruijnPattern]
-> [NamedArg A.Pattern]
-> WriterT [A.NamedDotPattern] TCM [NamedArg A.Pattern]
stripConP d us b c ci qs' ps' = do
Defn {defType = ct, theDef = Constructor{conPars = np}} <- getConInfo c
let ct' = ct `piApply` take np us
TelV tel' _ <- liftTCM $ telView ct'
reportSDoc "tc.with.strip" 20 $
vcat [ text "ct = " <+> prettyTCM ct
, text "ct' = " <+> prettyTCM ct'
, text "np = " <+> text (show np)
, text "us = " <+> prettyList (map prettyTCM us)
, text "us' = " <+> prettyList (map prettyTCM $ take np us)
]
let v = Con c ci [ Arg info (var i) | (i, Arg info _) <- zip (downFrom $ size qs') qs' ]
t' = tel' `abstract` absApp (raise (size tel') b) v
self' = tel' `abstract` apply1 (raise (size tel') self) v
reportSDoc "tc.with.strip" 15 $ sep
[ text "inserting implicit"
, nest 2 $ prettyList $ map prettyA (ps' ++ ps)
, nest 2 $ text ":" <+> prettyTCM t'
]
psi' <- liftTCM $ insertImplicitPatterns ExpandLast ps' tel'
unless (size psi' == size tel') $ typeError $
WrongNumberOfConstructorArguments (conName c) (size tel') (size psi')
psi <- liftTCM $ insertImplicitPatternsT ExpandLast (psi' ++ ps) t'
strip self' t' psi (qs' ++ qs)
withDisplayForm
:: QName
-> QName
-> Telescope
-> Telescope
-> Nat
-> [NamedArg DeBruijnPattern]
-> Permutation
-> Permutation
-> TCM DisplayForm
withDisplayForm f aux delta1 delta2 n qs perm@(Perm m _) lhsPerm = do
let arity0 = n + size delta1 + size delta2
topArgs <- raise arity0 <$> getContextArgs
let top = length topArgs
arity = arity0 + top
wild <- freshNoName_ <&> \ x -> Def (qualify_ x) []
let
tqs0 = patsToElims qs
(ys0, ys1) = splitAt (size delta1) $ permute perm $ downFrom m
ys = reverse (map Just ys0 ++ replicate n Nothing ++ map Just ys1)
++ map (Just . (m +)) [0..top1]
rho = sub top ys wild
tqs = applySubst rho tqs0
es = map (Apply . fmap DTerm) topArgs ++ tqs
withArgs = map var $ take n $ downFrom $ size delta2 + n
dt = DWithApp (DDef f es) (map DTerm withArgs) []
let display = Display arity (replicate arity $ Apply $ defaultArg $ var 0) dt
let addFullCtx = addContext delta1
. flip (foldr addContext) (for [1..n] $ \ i -> "w" ++ show i)
. addContext delta2
reportSDoc "tc.with.display" 20 $ vcat
[ text "withDisplayForm"
, nest 2 $ vcat
[ text "f =" <+> text (prettyShow f)
, text "aux =" <+> text (prettyShow aux)
, text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> do addContext delta1 $ prettyTCM delta2
, text "n =" <+> text (show n)
, text "perm =" <+> text (show perm)
, text "top =" <+> do addFullCtx $ prettyTCM topArgs
, text "qs =" <+> prettyList (map pretty qs)
, text "qsToTm =" <+> prettyTCM tqs0
, text "ys =" <+> text (show ys)
, text "rho =" <+> text (prettyShow rho)
, text "qs[rho]=" <+> do addFullCtx $ prettyTCM tqs
, text "dt =" <+> do addFullCtx $ prettyTCM dt
]
]
reportSDoc "tc.with.display" 70 $ nest 2 $ vcat
[ text "raw =" <+> text (show display)
]
return display
where
sub top ys wild = parallelS $ map term [0 .. m + top 1]
where
term i = maybe wild var $ List.findIndex (Just i ==) ys
patsToElims :: [NamedArg DeBruijnPattern] -> [I.Elim' DisplayTerm]
patsToElims = map $ toElim . fmap namedThing
where
toElim :: Arg DeBruijnPattern -> I.Elim' DisplayTerm
toElim (Arg ai p) = case p of
ProjP o d -> I.Proj o d
p -> I.Apply $ Arg ai $ toTerm p
toTerms :: [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
toTerms = map $ fmap $ toTerm . namedThing
toTerm :: DeBruijnPattern -> DisplayTerm
toTerm p = case p of
ProjP _ d -> DDef d []
VarP x -> DTerm $ var $ dbPatVarIndex x
DotP t -> DDot $ t
AbsurdP p -> toTerm p
ConP c cpi ps -> DCon c (fromConPatternInfo cpi) $ toTerms ps
LitP l -> DTerm $ Lit l