module Agda.TypeChecking.Rules.LHS.ProblemRest where
import Control.Arrow (first, second)
import Data.Functor ((<$))
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Abstract.Pattern
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 :: [NamedArg A.Pattern] -> Telescope -> Telescope
useNamesFromPattern ps = telFromList . zipWith ren (map namedArg ps ++ repeat dummy) . telToList
where
dummy = A.WildP __IMPOSSIBLE__
ren (A.VarP x) (Dom info (_, a)) | visible info && not (isNoName x) =
Dom info (nameToArgName x, a)
ren A.PatternSynP{} _ = __IMPOSSIBLE__
ren _ (Dom info (x, a)) | visible info && isNoName x =
Dom info (stringToArgName "x", a)
ren _ a = a
useOriginFrom :: (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
useOriginFrom = zipWith $ \x y -> setOrigin (getOrigin y) x
noProblemRest :: Problem -> Bool
noProblemRest (Problem _ _ _ (ProblemRest ps _)) = null ps
problemFromPats :: [NamedArg A.Pattern]
-> Type
-> TCM Problem
problemFromPats ps0 a = do
let ps = (`mapNamedArgPattern` ps0) $ \case
p | A.WildP{} <- namedArg p -> setOrigin Inserted p
p -> p
ps <- insertImplicitPatternsT ExpandLast ps a
reportSDoc "tc.lhs.imp" 20 $
text "insertImplicitPatternsT returned" <+> fsep (map prettyA ps)
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 = teleNamedArgs gamma `useOriginFrom` ps
problem = Problem 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 =" <+> addContext gamma (prettyTCM b)
]
]
return problem
updateProblemRest_ :: Problem -> TCM (Nat, Problem)
updateProblemRest_ p@(Problem ps0 qs0 tel0 (ProblemRest ps a)) = do
ps <- insertImplicitPatternsT ExpandLast ps $ unArg a
reportSDoc "tc.lhs.imp" 20 $
text "insertImplicitPatternsT returned" <+> fsep (map prettyA ps)
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 = teleNamedArgs gamma `useOriginFrom` ps
n = size as
reportSDoc "tc.lhs.problem" 10 $ addContext 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 =" <+> addContext gamma (prettyTCM b)
]
]
return $ (n,) $ Problem (ps0 ++ ps1) (applySubst (raiseS 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'
, lhsDPI = applyPatSubst tau (lhsDPI st)
, lhsShouldBeEmptyTypes = map (second $ applyPatSubst tau) (lhsShouldBeEmptyTypes st)
}