module Agda.TypeChecking.Rules.LHS.AsPatterns
( recoverAsPatterns ) where
import Control.Applicative
import Control.Monad.Writer hiding ((<>))
import qualified Data.Foldable as Fold
import Agda.Syntax.Common
import Agda.Syntax.Concrete ()
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Abstract.Pattern ( containsAsPattern )
import qualified Agda.Syntax.Abstract as A
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Size
import Agda.Utils.Impossible
#include "undefined.h"
recoverAsPatterns :: Telescope -> Type -> Term -> [NamedArg A.Pattern] -> [NamedArg DeBruijnPattern] -> TCM [AsBinding]
recoverAsPatterns delta a self ps qs = do
let es = patternsToElims qs
as <- typeElims (raise (size delta) a) self es
ps <- insertImplicitPatternsT DontExpandLast ps a
reportSDoc "tc.lhs.as" 30 $ vcat
[ text "recovering as patterns"
, nest 2 $ vcat [ text "es =" <+> prettyList (map prettyTCM es)
, text "as =" <+> prettyList (map prettyTCM as)
, text "ps =" <+> prettyList (map prettyA ps) ]
]
execWriterT $ asPatterns as ps es
asPatterns :: [ElimType] -> [NamedArg A.Pattern] -> [Elim] -> WriterT [AsBinding] TCM ()
asPatterns _ [] _ = return ()
asPatterns (ProjT _ a : as) (p : ps) (Proj{} : vs) = do
unless (isJust $ A.maybePostfixProjP p) __IMPOSSIBLE__
ps <- lift $ insertImplicitPatternsT DontExpandLast ps a
asPatterns as ps vs
asPatterns (ArgT dom : as) (p : ps) (Apply v : vs)
| not $ containsAsPattern p = asPatterns as ps vs
| otherwise = do
let a = unDom dom
case namedArg p of
A.AsP _ x p' -> do
tell [AsB x (unArg v) a]
asPatterns (ArgT dom : as) (fmap (p' <$) p : ps) (Apply v : vs)
A.ConP _ _ ps' -> do
(_, _, tel, as', args) <- lift $ conPattern a (unArg v)
ps' <- lift $ insertImplicitPatterns ExpandLast ps' tel
asPatterns (map ArgT as' ++ as) (ps' ++ ps) (map Apply args ++ vs)
A.RecP i fps -> do
(r, c, _, as', args) <- lift $ conPattern a (unArg v)
let fs = zipWith (<$) (map (nameConcrete . qnameName) $ conFields c) args
ps' <- lift $ insertMissingFields r (const $ A.WildP i) fps fs
asPatterns (map ArgT as' ++ as) (ps' ++ ps) (map Apply args ++ vs)
A.DefP{} -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
asPatterns _ _ _ = __IMPOSSIBLE__
conPattern
:: Type
-> Term
-> TCM (QName, ConHead, Telescope, [Dom Type], Args)
conPattern a (Con c ci args) = do
((d, _, _), ca) <- fromMaybe __IMPOSSIBLE__ <.> getFullyAppliedConType c =<< reduce a
TelV tel _ <- telView ca
let as = fromMaybe __IMPOSSIBLE__ $ typeArgsWithTel tel $ map unArg args
return (d, c, tel, as, args)
conPattern _ _ = __IMPOSSIBLE__