summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs')
-rw-r--r--src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs34
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)
}