module Agda.TypeChecking.Rules.LHS.ProblemRest where
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import qualified Agda.Syntax.Abstract as A
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.Utils.Functor (($>))
import Agda.Utils.Size
import Agda.Utils.Permutation
#include "../../../undefined.h"
import Agda.Utils.Impossible
useNamesFromPattern :: [A.NamedArg A.Pattern] -> Telescope -> Telescope
useNamesFromPattern ps = telFromList . zipWith ren (toPats ps ++ repeat dummy) . telToList
where
dummy = A.WildP __IMPOSSIBLE__
ren (A.VarP x) (Dom info (_, a)) | notHidden info = Dom info (nameToArgName x, a)
ren A.PatternSynP{} _ = __IMPOSSIBLE__
ren _ a = a
toPats = map namedArg
noProblemRest :: Problem -> Bool
noProblemRest (Problem _ _ _ (ProblemRest ps _)) = null ps
problemFromPats :: [A.NamedArg A.Pattern]
-> Type
-> TCM Problem
problemFromPats ps a = do
ps <- insertImplicitPatternsT DontExpandLast ps a
TelV tel0 b <- telViewUpTo (length ps) a
let gamma = useNamesFromPattern ps tel0
as = telToList gamma
(ps1,ps2) = splitAt (size as) ps
pr = ProblemRest ps2 $ defaultArg b
let ips = map (argFromDom . fmap (namedVarP . fst)) as
let problem = Problem ps1 (idP $ size ps1, ips) gamma pr :: Problem
reportSDoc "tc.lhs.problem" 10 $
vcat [ text "checking lhs -- generated an initial split problem:"
, nest 2 $ vcat
[ text "ps =" <+> fsep (map prettyA ps)
, text "a =" <+> prettyTCM a
, text "xs =" <+> text (show $ map (fst . unDom) as)
, text "ps1 =" <+> fsep (map prettyA ps1)
, text "gamma =" <+> prettyTCM gamma
, text "ps2 =" <+> fsep (map prettyA ps2)
, text "b =" <+> addCtxTel gamma (prettyTCM b)
]
]
return problem
updateProblemRest_ :: Problem -> TCM (Nat, Problem)
updateProblemRest_ p@(Problem _ _ _ (ProblemRest [] _)) = return (0, p)
updateProblemRest_ p@(Problem ps0 (perm0@(Perm n0 is0), qs0) tel0 (ProblemRest ps a)) = do
TelV tel' b0 <- telView $ unArg a
case tel' of
EmptyTel -> return (0, p)
ExtendTel{} -> do
ps <- insertImplicitPatterns DontExpandLast ps tel'
TelV tel b <- telViewUpTo (length ps) $ unArg a
let gamma = useNamesFromPattern ps tel
as = telToList gamma
(ps1,ps2) = splitAt (size as) ps
tel1 = telFromList $ telToList tel0 ++ as
pr = ProblemRest ps2 (a $> b)
qs1 = map (argFromDom . fmap (namedVarP . fst)) as
n = size as
perm1 = liftP n perm0
reportSDoc "tc.lhs.problem" 10 $ addCtxTel tel0 $ vcat
[ text "checking lhs -- updated split problem:"
, nest 2 $ vcat
[ text "ps =" <+> fsep (map prettyA ps)
, text "a =" <+> prettyTCM a
, text "xs =" <+> text (show $ map (fst . unDom) as)
, text "ps1 =" <+> fsep (map prettyA ps1)
, text "gamma =" <+> prettyTCM gamma
, text "ps2 =" <+> fsep (map prettyA ps2)
, text "b =" <+> addCtxTel gamma (prettyTCM b)
]
]
return $ (n,) $ Problem (ps0 ++ ps1) (perm1, raise n qs0 ++ qs1) tel1 pr
updateProblemRest :: LHSState -> TCM LHSState
updateProblemRest st@LHSState { lhsProblem = p } = do
(n, p') <- updateProblemRest_ p
if (n == 0) then return st else do
let tau = raiseS n
return $ LHSState
{ lhsProblem = p'
, lhsSubst = applySubst tau (lhsSubst st)
, lhsDPI = applySubst tau (lhsDPI st)
, lhsAsB = applySubst tau (lhsAsB st)
}