{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Rules.LHS.ProblemRest where
import Control.Arrow (first, second)
import Control.Monad
import Data.Functor ((<$))
import Data.Maybe
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
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.List
import Agda.Utils.Size
import Agda.Utils.Permutation
#include "undefined.h"
import Agda.Utils.Impossible
useNamesFromPattern :: [NamedArg A.Pattern] -> Telescope -> Telescope
useNamesFromPattern ps tel = telFromList (zipWith ren ps telList ++ telRemaining)
where
telList = telToList tel
telRemaining = drop (length ps) telList
ren (Arg ai (Named nm p)) dom@(Dom info (y, a)) =
case p of
A.VarP (A.BindName x) | not (isNoName x)
, visible info || (getOrigin ai == UserWritten && nm == Nothing) ->
Dom info (nameToArgName x, a)
A.PatternSynP{} -> __IMPOSSIBLE__
_ | visible info && isNoName y -> Dom info (stringToArgName "x", a)
| otherwise -> dom
useOriginFrom :: (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
useOriginFrom = zipWith $ \x y -> setOrigin (getOrigin y) x
noProblemRest :: Problem a -> Bool
noProblemRest (Problem _ rp _) = null rp
initLHSState
:: Telescope
-> [ProblemEq]
-> [NamedArg A.Pattern]
-> Type
-> (LHSState a -> TCM a)
-> TCM (LHSState a)
initLHSState delta eqs ps a ret = do
let problem = Problem eqs ps ret
qs0 = teleNamedArgs delta
updateProblemRest $ LHSState delta qs0 problem (defaultArg a)
updateProblemRest :: LHSState a -> TCM (LHSState a)
updateProblemRest st@(LHSState tel0 qs0 p@(Problem oldEqs ps ret) a) = do
ps <- addContext tel0 $ insertImplicitPatternsT ExpandLast ps $ unArg a
reportSDoc "tc.lhs.imp" 20 $
text "insertImplicitPatternsT returned" <+> fsep (map prettyA ps)
let m = length $ takeWhile (isNothing . A.maybePostfixProjP) ps
TelV gamma b <- telViewUpTo m $ unArg a
forM_ (zip ps (telToList gamma)) $ \(p, a) ->
unless (sameHiding p a) $ typeError WrongHidingInLHS
let tel1 = useNamesFromPattern ps gamma
n = size tel1
(ps1,ps2) = splitAt n ps
tel = telFromList $ telToList tel0 ++ telToList tel1
qs1 = teleNamedArgs tel1
newEqs = zipWith3 ProblemEq
(map namedArg ps1)
(map (patternToTerm . namedArg) qs1)
(flattenTel tel1 `useOriginFrom` ps1)
tau = raiseS n
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 "tel1 =" <+> prettyTCM tel1
, text "ps1 =" <+> fsep (map prettyA ps1)
, text "ps2 =" <+> fsep (map prettyA ps2)
, text "b =" <+> addContext tel1 (prettyTCM b)
]
]
reportSDoc "tc.lhs.problem" 60 $ addContext tel0 $ vcat
[ nest 2 $ vcat
[ text "qs1 =" <+> fsep (map pretty qs1)
]
]
return $ LHSState
{ _lhsTel = tel
, _lhsOutPat = applySubst tau qs0 ++ qs1
, _lhsProblem = Problem
{ _problemEqs = applyPatSubst tau oldEqs ++ newEqs
, _problemRestPats = ps2
, _problemCont = ret
}
, _lhsTarget = a $> b
}