diff options
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs')
-rw-r--r-- | src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs | 34 |
1 files changed, 20 insertions, 14 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs b/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs index 5bccfff..3eb54b1 100644 --- a/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs +++ b/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs @@ -1,8 +1,9 @@ {-# LANGUAGE CPP #-} -{-# LANGUAGE TupleSections #-} module Agda.TypeChecking.Rules.LHS.ProblemRest where +import Data.Functor ((<$)) + import Agda.Syntax.Common import Agda.Syntax.Internal import qualified Agda.Syntax.Abstract as A @@ -11,7 +12,6 @@ import Agda.TypeChecking.Monad import Agda.TypeChecking.Pretty import Agda.TypeChecking.Telescope import Agda.TypeChecking.Substitute -import Agda.TypeChecking.Substitute.Pattern import Agda.TypeChecking.Rules.LHS.Problem import Agda.TypeChecking.Rules.LHS.Implicit @@ -26,18 +26,24 @@ import Agda.Utils.Impossible -- MOVED from LHS: -- | Rename the variables in a telescope using the names from a given pattern useNamesFromPattern :: [NamedArg A.Pattern] -> Telescope -> Telescope -useNamesFromPattern ps = telFromList . zipWith ren (toPats ps ++ repeat dummy) . telToList +useNamesFromPattern ps = telFromList . zipWith ren (map namedArg 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.VarP x) (Dom info (_, a)) | notHidden info && not (isNoName x) = + Dom info (nameToArgName x, a) ren A.AbsurdP{} (Dom info (_, a)) | notHidden info = Dom info ("()", a) -- Andreas, 2013-03-13: inserted the following line in the hope to fix issue 819 -- but it does not do the job, instead, it puts a lot of "_"s -- instead of more sensible names into error messages. -- ren A.WildP{} (Dom info (_, a)) | notHidden info = Dom info ("_", a) ren A.PatternSynP{} _ = __IMPOSSIBLE__ -- ensure there are no syns left + -- Andreas, 2016-05-10, issue 1848: if context variable has no name, call it "x" + ren _ (Dom info (x, a)) | notHidden info && isNoName x = + Dom info (stringToArgName "x", a) ren _ a = a - toPats = map namedArg + +useOriginFrom :: (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a] +useOriginFrom = zipWith $ \x y -> setOrigin (getOrigin y) x -- | Are there any untyped user patterns left? noProblemRest :: Problem -> Bool @@ -74,7 +80,9 @@ problemFromPats ps a = do -- For the initial problem, do not insert trailing implicits. -- This has the effect of not including trailing hidden domains in the problem telescope. -- In all later call to insertImplicitPatterns, we can then use ExpandLast. - ps <- insertImplicitPatternsT DontExpandLast ps a + -- Ulf, 2016-04-25: Actually we do need to ExpandLast because where blocks + -- need the implicits. + ps <- insertImplicitPatternsT ExpandLast ps a -- unless (size tel0' >= size ps) $ typeError $ TooManyArgumentsInLHS a -- Redo the telView, in order to *not* normalize the clause type further than necessary. @@ -87,7 +95,7 @@ problemFromPats ps a = do pr = ProblemRest ps2 $ defaultArg b -- internal patterns start as all variables - let ips = teleNamedArgs gamma + let ips = teleNamedArgs gamma `useOriginFrom` ps -- the initial problem for starting the splitting problem = Problem ps1 ips gamma pr :: Problem @@ -101,7 +109,7 @@ problemFromPats ps a = do -- , text "ips =" <+> prettyTCM ips -- no prettyTCM instance , text "gamma =" <+> prettyTCM gamma , text "ps2 =" <+> fsep (map prettyA ps2) - , text "b =" <+> addCtxTel gamma (prettyTCM b) + , text "b =" <+> addContext gamma (prettyTCM b) ] ] return problem @@ -110,7 +118,7 @@ problemFromPats ps a = do -- Possible if type of problem rest has been updated to a function type. updateProblemRest_ :: Problem -> TCM (Nat, Problem) updateProblemRest_ p@(Problem ps0 qs0 tel0 (ProblemRest ps a)) = do - ps <- insertImplicitPatternsT DontExpandLast ps $ unArg a + ps <- insertImplicitPatternsT ExpandLast ps $ unArg a -- (Issue 734: Do only the necessary telView to preserve clause types as much as possible.) TelV tel b <- telViewUpTo (length ps) $ unArg a let gamma = useNamesFromPattern ps tel @@ -118,9 +126,9 @@ updateProblemRest_ p@(Problem ps0 qs0 tel0 (ProblemRest ps a)) = do (ps1,ps2) = splitAt (size as) ps tel1 = telFromList $ telToList tel0 ++ as pr = ProblemRest ps2 (a $> b) - qs1 = teleNamedArgs gamma + qs1 = teleNamedArgs gamma `useOriginFrom` ps n = size as - reportSDoc "tc.lhs.problem" 10 $ addCtxTel tel0 $ vcat + reportSDoc "tc.lhs.problem" 10 $ addContext tel0 $ vcat [ text "checking lhs -- updated split problem:" , nest 2 $ vcat [ text "ps =" <+> fsep (map prettyA ps) @@ -129,7 +137,7 @@ updateProblemRest_ p@(Problem ps0 qs0 tel0 (ProblemRest ps a)) = do , text "ps1 =" <+> fsep (map prettyA ps1) , text "gamma =" <+> prettyTCM gamma , text "ps2 =" <+> fsep (map prettyA ps2) - , text "b =" <+> addCtxTel gamma (prettyTCM b) + , text "b =" <+> addContext gamma (prettyTCM b) ] ] return $ (n,) $ Problem (ps0 ++ ps1) (applySubst (raiseS n) qs0 ++ qs1) tel1 pr @@ -141,7 +149,5 @@ updateProblemRest st@LHSState { lhsProblem = p } = do let tau = raiseS n return $ LHSState { lhsProblem = p' - , lhsSubst = applySubst tau (lhsSubst st) , lhsDPI = applyPatSubst tau (lhsDPI st) - , lhsAsB = applyPatSubst tau (lhsAsB st) } |