{-# LANGUAGE BangPatterns #-}
{-# 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{ unDom = (y, a) } =
case p of
A.VarP (A.BindName x)
| not (isNoName x)
, visible dom || (getOrigin ai == UserWritten && nm == Nothing) ->
dom{ unDom = (nameToArgName x, a) }
A.AbsurdP{} | visible dom -> dom{ unDom = (stringToArgName "()", a) }
A.PatternSynP{} -> __IMPOSSIBLE__
_ | visible dom && isNoName y -> dom{ unDom = (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 psplit) = do
ps <- addContext tel0 $ insertImplicitPatternsT ExpandLast ps $ unArg a
reportSDoc "tc.lhs.imp" 20 $
"insertImplicitPatternsT returned" <+> fsep (map prettyA ps)
let m = length $ takeWhile (isNothing . A.isProjP) ps
(TelV gamma b, boundary) <- telViewUpToPathBoundaryP 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 = telePatterns tel1 boundary
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
[ "checking lhs -- updated split problem:"
, nest 2 $ vcat
[ "ps =" <+> fsep (map prettyA ps)
, "a =" <+> prettyTCM a
, "tel1 =" <+> prettyTCM tel1
, "ps1 =" <+> fsep (map prettyA ps1)
, "ps2 =" <+> fsep (map prettyA ps2)
, "b =" <+> addContext tel1 (prettyTCM b)
]
]
reportSDoc "tc.lhs.problem" 60 $ addContext tel0 $ vcat
[ nest 2 $ vcat
[ "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
, _lhsPartialSplit = psplit
}