module Agda.TypeChecking.With where
import Control.Applicative hiding (empty)
import Control.Monad
import Data.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 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 (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 = addCtxTel 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
let countArgs OtherType{} = 1
countArgs EqualityType{} = 2
return (telePi_ delta1 wd2b, sum $ map countArgs as)
withArguments :: [Term] -> [EqualityView] -> [Term]
withArguments vs as = concat $ for (zip vs as) $ \case
(v, OtherType a) -> [v]
(prf, eqt@(EqualityType s _eq _l t v _v')) -> [unArg v, prf]
buildWithFunction
:: QName
-> QName
-> Type
-> [NamedArg Pattern]
-> Permutation
-> Nat
-> Nat
-> [A.SpineClause]
-> TCM [A.SpineClause]
buildWithFunction f aux t qs perm n1 n cs = mapM buildWithClause cs
where
buildWithClause (A.Clause (A.SpineLHS i _ ps wps) rhs wh catchall) = do
let (wps0, wps1) = genericSplitAt n wps
ps0 = map defaultNamedArg wps0
rhs <- buildRHS rhs
(ps1, ps2) <- genericSplitAt n1 <$> stripWithClausePatterns f aux t qs perm ps
let result = A.Clause (A.SpineLHS i aux (ps1 ++ ps0 ++ ps2) wps1) 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 <.> buildWithClause . A.lhsToSpine) cs
buildRHS (A.RewriteRHS qes rhs wh) = flip (A.RewriteRHS qes) wh <$> buildRHS rhs
stripWithClausePatterns
:: QName
-> QName
-> Type
-> [NamedArg Pattern]
-> Permutation
-> [NamedArg A.Pattern]
-> TCM [NamedArg A.Pattern]
stripWithClausePatterns parent f t qs perm ps = do
ps <- expandPatternSynonyms ps
psi <- insertImplicitPatternsT ExpandLast ps t
reportSDoc "tc.with.strip" 10 $ vcat
[ text "stripping patterns"
, nest 2 $ text "t = " <+> prettyTCM t
, nest 2 $ text "psi = " <+> fsep (punctuate comma $ map prettyA psi)
, nest 2 $ text "qs = " <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs)
]
ps' <- strip (Def parent []) t psi $ numberPatVars perm qs
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 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 e -> case unScope e of
A.Underscore{} -> return ()
e | getRange info /= noRange -> typeError $ GenericError $
"This inaccessible pattern is never checked, so only _ allowed here"
_ -> return ()
_ -> return ()
return psp
where
strip
:: Term
-> Type
-> [NamedArg A.Pattern]
-> [NamedArg DeBruijnPattern]
-> 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 <- 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 == ConPImplicit
implicit _ = False
unless (all (implicit . namedArg) ps) $
typeError $ GenericError $ "Too many arguments given in with-clause"
return []
strip self t ps0@(p0 : ps) qs0@(q : qs) = do
p <- 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 = do
d <- 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 d -> case A.isProjP p of
Just d' -> do
d' <- getOriginalProjection d'
if d /= d' then mismatch else do
t <- reduce t
(self1, t1) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped self t d
ps <- insertImplicitPatternsT ExpandLast ps t1
strip self1 t1 ps qs
Nothing -> mismatch
VarP (i, _x) -> do
ps <- intro1 t $ \ t -> strip (self `apply1` var i) t ps qs
return $ p : ps
DotP v -> case namedArg p of
A.DotP _ _ -> ok p
A.WildP _ -> ok p
A.ConP ci _ _ | patOrigin ci == ConPImplicit -> okFlex p
p'@A.ConP{} -> ifM (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 = do
t' <- piApply1 t v
(p :) <$> strip (self `apply1` v) t' ps qs
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 <- ignoreSharing <$> normalise (unEl $ unDom a)
let us = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
c <- (`withRangeOf` c) <$> do getConForm $ conName c
case namedArg p of
A.DotP{} -> ifNotM (isFlexiblePattern q') mismatch $ do
maybe __IMPOSSIBLE__ (\ p -> strip self t (p : ps) qs0) =<< do
expandImplicitPattern' (unDom a) $ makeImplicitP p
A.WildP{} | Just _ <- conPRecord ci -> do
maybe __IMPOSSIBLE__ (\ p -> strip self t (p : ps) qs0) =<<
expandImplicitPattern' (unDom a) p
A.ConP _ (A.AmbQ cs') ps' -> do
cs' <- mapM getConForm cs'
unless (elem c cs') mismatch
stripConP d us b c qs' ps'
A.RecP _ fs -> caseMaybeM (isRecord d) mismatch $ \ def -> do
ps' <- insertMissingFields d (const $ A.WildP empty) fs (recordFieldNames def)
stripConP d us b c 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' -> do
(a, b) <- mustBePi t
let v = Lit lit
strip (self `apply1` v) (b `absApp` v) ps qs
p@(A.PatternSynP pi' c' [ps']) -> do
reportSDoc "impossible" 10 $
text "stripWithClausePatterns: encountered pattern synonym " <+> prettyA p
__IMPOSSIBLE__
_ -> mismatch
where
mismatch = typeError $
WithClausePatternMismatch (namedArg p0) (snd <$> namedArg q)
makeImplicitP :: NamedArg A.Pattern -> NamedArg A.Pattern
makeImplicitP = updateNamedArg $ const $ A.WildP patNoRange
stripConP
:: QName
-> [Arg Term]
-> Abs Type
-> ConHead
-> [NamedArg DeBruijnPattern]
-> [NamedArg A.Pattern]
-> TCM [NamedArg A.Pattern]
stripConP d us b c qs' ps' = do
Defn {defType = ct, theDef = Constructor{conPars = np}} <- getConInfo c
let ct' = ct `piApply` genericTake np us
TelV tel' _ <- 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 $ genericTake np us)
]
let v = Con c [ 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' <- insertImplicitPatterns ExpandLast ps' tel'
unless (size psi' == size tel') $ typeError $
WrongNumberOfConstructorArguments (conName c) (size tel') (size psi')
strip self' t' (psi' ++ ps) (qs' ++ qs)
withDisplayForm
:: QName
-> QName
-> Telescope
-> Telescope
-> Nat
-> [NamedArg Pattern]
-> 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 lhsPerm 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 $ var 0) dt
let addFullCtx = addCtxTel delta1
. flip (foldr addContext) (for [1..n] $ \ i -> "w" ++ show i)
. addCtxTel delta2
reportSDoc "tc.with.display" 20 $ vcat
[ text "withDisplayForm"
, nest 2 $ vcat
[ text "f =" <+> text (show f)
, text "aux =" <+> text (show aux)
, text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> do addCtxTel delta1 $ prettyTCM delta2
, text "n =" <+> text (show n)
, text "perm =" <+> text (show perm)
, text "top =" <+> do addFullCtx $ prettyTCM topArgs
, text "qs =" <+> sep (map (prettyTCM . namedArg) 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 $ findIndex (Just i ==) ys
patsToElims :: Permutation -> [NamedArg Pattern] -> [I.Elim' DisplayTerm]
patsToElims perm ps = toElims $ numberPatVars perm ps
where
toElims :: [NamedArg DeBruijnPattern] -> [I.Elim' DisplayTerm]
toElims = map $ toElim . fmap namedThing
toElim :: Arg DeBruijnPattern -> I.Elim' DisplayTerm
toElim (Arg ai p) = case p of
ProjP d -> I.Proj 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 (i, x) -> DTerm $ var i
DotP t -> DDot $ t
ConP c _ ps -> DCon c $ toTerms ps
LitP l -> DTerm $ Lit l