summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndresSicardRamirez <>2016-06-21 14:53:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2016-06-21 14:53:00 (GMT)
commit8ade7eec7e2e736938610db608d87cd6b8b5122e (patch)
treef767fb9a92966d5e1a60159d89ab759ed5a73217
parent29066e411fb1fd4f75e85b14fe834e28385219a1 (diff)
version 2.5.1.12.5.1.1
-rw-r--r--Agda.cabal23
-rw-r--r--CHANGELOG56
-rw-r--r--dist/build/Agda/Syntax/Parser/Lexer.hs21
-rw-r--r--dist/build/Agda/Syntax/Parser/Parser.hs21
-rw-r--r--src/data/emacs-mode/agda2-mode.el2
-rw-r--r--src/full/Agda/Interaction/BasicOps.hs2
-rw-r--r--src/full/Agda/Interaction/Imports.hs8
-rw-r--r--src/full/Agda/Syntax/Common.hs42
-rw-r--r--src/full/Agda/Syntax/Concrete/Operators.hs12
-rw-r--r--src/full/Agda/Syntax/Concrete/Operators/Parser.hs107
-rw-r--r--src/full/Agda/Syntax/Concrete/Pretty.hs9
-rw-r--r--src/full/Agda/Syntax/Translation/AbstractToConcrete.hs2
-rw-r--r--src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs6
-rw-r--r--src/full/Agda/Syntax/Translation/InternalToAbstract.hs31
-rw-r--r--src/full/Agda/TypeChecking/Constraints.hs10
-rw-r--r--src/full/Agda/TypeChecking/Constraints.hs-boot1
-rw-r--r--src/full/Agda/TypeChecking/Coverage.hs13
-rw-r--r--src/full/Agda/TypeChecking/Errors.hs8
-rw-r--r--src/full/Agda/TypeChecking/Implicit.hs6
-rw-r--r--src/full/Agda/TypeChecking/InstanceArguments.hs87
-rw-r--r--src/full/Agda/TypeChecking/InstanceArguments.hs-boot7
-rw-r--r--src/full/Agda/TypeChecking/MetaVars.hs19
-rw-r--r--src/full/Agda/TypeChecking/MetaVars.hs-boot2
-rw-r--r--src/full/Agda/TypeChecking/Monad/Base.hs4
-rw-r--r--src/full/Agda/TypeChecking/Monad/Constraints.hs59
-rw-r--r--src/full/Agda/TypeChecking/Pretty.hs2
-rw-r--r--src/full/Agda/TypeChecking/Rules/LHS/Unify.hs4
-rw-r--r--src/full/Agda/TypeChecking/Serialise/Instances/Common.hs30
28 files changed, 397 insertions, 197 deletions
diff --git a/Agda.cabal b/Agda.cabal
index cb3ed7a..30b0e5d 100644
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -1,5 +1,5 @@
name: Agda
-version: 2.5.1
+version: 2.5.1.1
cabal-version: >= 1.8
build-type: Custom
license: OtherLicense
@@ -35,6 +35,7 @@ description:
tested-with: GHC == 7.6.3
GHC == 7.8.4
GHC == 7.10.3
+ GHC == 8.0.1
extra-source-files: src/full/undefined.h
README.md
CHANGELOG
@@ -76,8 +77,8 @@ source-repository head
source-repository this
type: git
- location: https://github.com/agda/agda/tree/2.5.1
- tag: 2.5.1
+ location: https://github.com/agda/agda/tree/v2.5.1.1
+ tag: v2.5.1.1
flag cpphs
default: True
@@ -99,12 +100,13 @@ library
ghc-options: -pgmP cpphs -optP --cpp
if flag(uhc)
- build-depends: shuffle >= 0.1.3.3
- , uhc-light >= 1.1.9.2 && < 1.2
- , uhc-util >= 0.1.6.3 && < 0.1.6.6
- , uulib >= 0.9.20
- -- we use the CPP processor to conditionally import the UHC Light modules. If UHC Light is not
- -- present, we instead create dummy definitions, see module Agda.Compiler.UHC.Bridge.
+ build-depends: shuffle >= 0.1.3.3
+ , uhc-light >= 1.1.9.2 && < 1.2
+ , uhc-util >= 0.1.6.3 && < 0.1.6.7
+ , uulib >= 0.9.20
+ -- we use the CPP processor to conditionally import the UHC Light
+ -- modules. If UHC Light is not present, we instead create dummy
+ -- definitions, see module Agda.Compiler.UHC.Bridge.
cpp-options: -DUHC_BACKEND
if os(windows)
@@ -534,7 +536,7 @@ executable agda
hs-source-dirs: src/main
main-is: Main.hs
build-depends:
- Agda == 2.5.1
+ Agda == 2.5.1.1
-- Nothing is used from the following package, except for the
-- prelude.
, base >= 4.6.0.1 && < 6
@@ -572,3 +574,4 @@ executable agda-ghc-names
, mtl >= 2.1.1 && <= 2.1.3.1 || >= 2.2.1 && < 2.3
, filepath >= 1.3.0.1 && < 1.5
ghc-options: -rtsopts
+
diff --git a/CHANGELOG b/CHANGELOG
index 86e575f..62f2315 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,4 +1,60 @@
------------------------------------------------------------------------
+-- Release notes for Agda version 2.5.1.1
+------------------------------------------------------------------------
+
+Important changes since 2.5.1:
+
+Installation and infrastructure
+===============================
+
+* Added support for GHC 8.0.1.
+
+Bug fixes
+=========
+
+* Fixed a serious performance problem with instance search
+
+ Issues #1952 and #1998. Also related: #1955 and #2025
+
+* Interactively splitting variable with C-c C-c no longer introduces
+ new trailing patterns. This fixes issue #1950.
+
+ data Ty : Set where
+ _⇒_ : Ty → Ty → Ty
+
+ ⟦_⟧ : Ty → Set
+ ⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧
+
+ data Term : Ty → Set where
+ K : (A B : Ty) → Term (A ⇒ (B ⇒ A))
+
+ test : (A : Ty) (a : Term A) → ⟦ A ⟧
+ test A a = {!a!}
+
+ Before change, case splitting on `a` would give
+
+ test .(A ⇒ (B ⇒ A)) (K A B) x x₁ = ?
+
+ Now, it yields
+
+ test .(A ⇒ (B ⇒ A)) (K A B) = ?
+
+* Other issues fixed ( see https://github.com/agda/agda/issues ):
+ - #1322 (Missing error for attempted higher order instance)
+ - #1951 (mixfix binders not working in 'syntax')
+ - #1967 (too eager insteance search error)
+ - #1974 (lost constraint dependencies)
+ - #1982 (internal error in unifier)
+ - #2034 (function type instance goals)
+
+Compiler backends
+=================
+
+* UHC compiler backend
+
+ Added support for UHC 1.1.9.4.
+
+------------------------------------------------------------------------
-- Release notes for Agda version 2.5.1
------------------------------------------------------------------------
diff --git a/dist/build/Agda/Syntax/Parser/Lexer.hs b/dist/build/Agda/Syntax/Parser/Lexer.hs
index c6e25c7..135bf75 100644
--- a/dist/build/Agda/Syntax/Parser/Lexer.hs
+++ b/dist/build/Agda/Syntax/Parser/Lexer.hs
@@ -267,27 +267,6 @@ alex_action_117 = identifier
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "<built-in>" #-}
{-# LINE 1 "<command-line>" #-}
-{-# LINE 9 "<command-line>" #-}
-{-# LINE 1 "/usr/local/stow/ghc-8.0-upstream/lib/ghc-8.0.0.20160316/include/ghcversion.h" #-}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-{-# LINE 9 "<command-line>" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
-- -----------------------------------------------------------------------------
-- ALEX TEMPLATE
diff --git a/dist/build/Agda/Syntax/Parser/Parser.hs b/dist/build/Agda/Syntax/Parser/Parser.hs
index 2eac864..49642f6 100644
--- a/dist/build/Agda/Syntax/Parser/Parser.hs
+++ b/dist/build/Agda/Syntax/Parser/Parser.hs
@@ -6324,27 +6324,6 @@ tests = runTests "Agda.Syntax.Parser.Parser"
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "<built-in>" #-}
{-# LINE 1 "<command-line>" #-}
-{-# LINE 11 "<command-line>" #-}
-{-# LINE 1 "/usr/local/stow/ghc-8.0-upstream/lib/ghc-8.0.0.20160316/include/ghcversion.h" #-}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-{-# LINE 11 "<command-line>" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
-- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp
diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el
index b9295c8..d58eaf9 100644
--- a/src/data/emacs-mode/agda2-mode.el
+++ b/src/data/emacs-mode/agda2-mode.el
@@ -10,7 +10,7 @@
;;; Code:
-(defvar agda2-version "2.5.1"
+(defvar agda2-version "2.5.1.1"
"The version of the Agda mode.
Note that the same version of the Agda executable must be used.")
diff --git a/src/full/Agda/Interaction/BasicOps.hs b/src/full/Agda/Interaction/BasicOps.hs
index f211873..640c910 100644
--- a/src/full/Agda/Interaction/BasicOps.hs
+++ b/src/full/Agda/Interaction/BasicOps.hs
@@ -295,7 +295,7 @@ outputFormId (OutputForm _ _ o) = out o
FindInScopeOF _ _ _ -> __IMPOSSIBLE__
instance Reify ProblemConstraint (Closure (OutputForm Expr Expr)) where
- reify (PConstr pid cl) = enterClosure cl $ \c -> buildClosure =<< (OutputForm (getRange c) pid <$> reify c)
+ reify (PConstr pids cl) = enterClosure cl $ \c -> buildClosure =<< (OutputForm (getRange c) (last pids) <$> reify c)
instance Reify Constraint (OutputConstraint Expr Expr) where
reify (ValueCmp cmp t u v) = CmpInType cmp <$> reify t <*> reify u <*> reify v
diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs
index 22c8c2d..9dbc00a 100644
--- a/src/full/Agda/Interaction/Imports.hs
+++ b/src/full/Agda/Interaction/Imports.hs
@@ -726,6 +726,11 @@ buildInterface file topLevel syntaxInfo previousHsImports previousHsImportsUHC p
-- Andreas, Makoto, 2014-10-18 AIM XX: repeating the experiment
-- with discarding also the nameBindingSite in QName:
-- Saves 10% on serialization time (and file size)!
+ --
+ -- NOTE: We no longer discard all nameBindingSites (but the commit
+ -- that introduced this change seems to have made Agda a bit
+ -- faster and interface file sizes a bit smaller, at least for the
+ -- standard library).
builtin <- use stLocalBuiltins
ms <- getImports
mhs <- mapM (\ m -> (m,) <$> moduleHash m) $ Set.toList ms
@@ -736,7 +741,8 @@ buildInterface file topLevel syntaxInfo previousHsImports previousHsImportsUHC p
-- Non-closed display forms are not applicable outside the module anyway,
-- and should be dead-code eliminated (#1928).
display <- HMap.filter (not . null) . HMap.map (filter isClosed) <$> use stImportsDisplayForms
- (display, sig) <- second killRange <$> (eliminateDeadCode display =<< getSignature)
+ -- TODO: Kill some ranges?
+ (display, sig) <- eliminateDeadCode display =<< getSignature
-- Andreas, 2015-02-09 kill ranges in pattern synonyms before
-- serialization to avoid error locations pointing to external files
-- when expanding a pattern synoym.
diff --git a/src/full/Agda/Syntax/Common.hs b/src/full/Agda/Syntax/Common.hs
index 60e2ff5..f1ac5d7 100644
--- a/src/full/Agda/Syntax/Common.hs
+++ b/src/full/Agda/Syntax/Common.hs
@@ -18,6 +18,7 @@ import Data.ByteString.Char8 (ByteString)
import qualified Data.ByteString.Char8 as ByteString
import Data.Foldable
import Data.Hashable
+import qualified Data.Strict.Maybe as Strict
import Data.Monoid
import Data.Traversable
import Data.Typeable (Typeable)
@@ -768,32 +769,49 @@ instance NFData MetaId where
newtype Constr a = Constr a
-data Placeholder
+------------------------------------------------------------------------
+-- * Placeholders (used to parse sections)
+------------------------------------------------------------------------
+
+-- | The position of a name part or underscore in a name.
+
+data PositionInName
= Beginning
- -- ^ @_foo@.
+ -- ^ The following underscore is at the beginning of the name:
+ -- @_foo@.
| Middle
- -- ^ @foo_bar@.
+ -- ^ The following underscore is in the middle of the name:
+ -- @foo_bar@.
| End
- -- ^ @foo_@.
+ -- ^ The following underscore is at the end of the name: @foo_@.
deriving (Show, Eq, Ord)
-- | Placeholders are used to represent the underscores in a section.
+
data MaybePlaceholder e
- = Placeholder !Placeholder
- | NoPlaceholder e
+ = Placeholder !PositionInName
+ | NoPlaceholder !(Strict.Maybe PositionInName) e
+ -- ^ The second argument is used only (but not always) for name
+ -- parts other than underscores.
deriving (Typeable, Eq, Ord, Functor, Foldable, Traversable, Show)
+-- | An abbreviation: @noPlaceholder = 'NoPlaceholder'
+-- 'Strict.Nothing'@.
+
+noPlaceholder :: e -> MaybePlaceholder e
+noPlaceholder = NoPlaceholder Strict.Nothing
+
instance HasRange a => HasRange (MaybePlaceholder a) where
- getRange Placeholder{} = noRange
- getRange (NoPlaceholder e) = getRange e
+ getRange Placeholder{} = noRange
+ getRange (NoPlaceholder _ e) = getRange e
instance KillRange a => KillRange (MaybePlaceholder a) where
- killRange p@Placeholder{} = p
- killRange (NoPlaceholder e) = killRange1 NoPlaceholder e
+ killRange p@Placeholder{} = p
+ killRange (NoPlaceholder p e) = killRange1 (NoPlaceholder p) e
instance NFData a => NFData (MaybePlaceholder a) where
- rnf (Placeholder _) = ()
- rnf (NoPlaceholder a) = rnf a
+ rnf (Placeholder _) = ()
+ rnf (NoPlaceholder _ a) = rnf a
---------------------------------------------------------------------------
-- * Interaction meta variables
diff --git a/src/full/Agda/Syntax/Concrete/Operators.hs b/src/full/Agda/Syntax/Concrete/Operators.hs
index 97fcfc4..246ce8f 100644
--- a/src/full/Agda/Syntax/Concrete/Operators.hs
+++ b/src/full/Agda/Syntax/Concrete/Operators.hs
@@ -452,9 +452,9 @@ buildParsers r flat kind exprNames = do
nonAssoc = case filter (isInfix NonAssoc) ops of
[] -> Nothing
ops -> Just $ do
- x <- NoPlaceholder <$> higher
+ x <- noPlaceholder <$> higher
f <- choice In ops
- y <- NoPlaceholder <$> higher
+ y <- noPlaceholder <$> higher
return (f x y)
or p1 [] p2 [] = Nothing
@@ -466,7 +466,7 @@ buildParsers r flat kind exprNames = do
preRight =
or (choice Pre)
(filter isPrefix ops)
- (\ops -> flip ($) <$> (NoPlaceholder <$> higher)
+ (\ops -> flip ($) <$> (noPlaceholder <$> higher)
<*> choice In ops)
(filter (isInfix RightAssoc) ops)
@@ -474,14 +474,14 @@ buildParsers r flat kind exprNames = do
preRights = do
preRight <- preRight
return $ Data.Function.fix $ \preRights ->
- preRight <*> (NoPlaceholder <$> (preRights <|> higher))
+ preRight <*> (noPlaceholder <$> (preRights <|> higher))
postLeft :: Maybe (Parser e (MaybePlaceholder e -> e))
postLeft =
or (choice Post)
(filter isPostfix ops)
(\ops -> flip <$> choice In ops
- <*> (NoPlaceholder <$> higher))
+ <*> (noPlaceholder <$> higher))
(filter (isInfix LeftAssoc) ops)
postLefts :: Maybe (Parser e e)
@@ -489,7 +489,7 @@ buildParsers r flat kind exprNames = do
postLeft <- postLeft
return $ Data.Function.fix $ \postLefts ->
memoise (PostLeftsK key) $
- flip ($) <$> (NoPlaceholder <$> (postLefts <|> higher))
+ flip ($) <$> (noPlaceholder <$> (postLefts <|> higher))
<*> postLeft
---------------------------------------------------------------------------
diff --git a/src/full/Agda/Syntax/Concrete/Operators/Parser.hs b/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
index e46b068..79596b7 100644
--- a/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
+++ b/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
@@ -12,6 +12,7 @@ import Control.Applicative
import Data.Either
import Data.Hashable
import Data.Maybe
+import qualified Data.Strict.Maybe as Strict
import Data.Set (Set)
import GHC.Generics (Generic)
@@ -42,26 +43,26 @@ instance Hashable MemoKey
type Parser tok a =
MemoisedCPS.Parser MemoKey tok (MaybePlaceholder tok) a
-placeholder :: Placeholder -> Parser e (MaybePlaceholder e)
+placeholder :: PositionInName -> Parser e (MaybePlaceholder e)
placeholder p = sat $ \t ->
case t of
Placeholder p' | p' == p -> True
_ -> False
maybePlaceholder ::
- Maybe Placeholder -> Parser e e -> Parser e (MaybePlaceholder e)
+ Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e)
maybePlaceholder mp p = case mp of
Nothing -> p'
Just h -> placeholder h <|> p'
where
- p' = NoPlaceholder <$> p
+ p' = noPlaceholder <$> p
notPlaceholder :: Parser e e
notPlaceholder = do
tok <- token
case tok of
- Placeholder _ -> empty
- NoPlaceholder e -> return e
+ Placeholder _ -> empty
+ NoPlaceholder _ e -> return e
sat' :: (e -> Bool) -> Parser e e
sat' p = do
@@ -116,7 +117,7 @@ instance IsExpr Pattern where
IdentP x -> LocalV x
AppP e1 e2 -> AppV e1 e2
OpAppP r d ns es -> OpAppV d ns ((map . fmap . fmap)
- (NoPlaceholder . Ordinary) es)
+ (noPlaceholder . Ordinary) es)
HiddenP _ e -> HiddenArgV e
InstanceP _ e -> InstanceArgV e
ParenP _ e -> ParenV e
@@ -128,8 +129,8 @@ instance IsExpr Pattern where
OpAppV d ns es -> let ess :: [NamedArg Pattern]
ess = (map . fmap . fmap)
(\x -> case x of
- Placeholder{} -> __IMPOSSIBLE__
- NoPlaceholder x -> fromOrdinary __IMPOSSIBLE__ x)
+ Placeholder{} -> __IMPOSSIBLE__
+ NoPlaceholder _ x -> fromOrdinary __IMPOSSIBLE__ x)
es
in OpAppP (fuseRange d ess) d ns ess
HiddenArgV e -> HiddenP (getRange e) e
@@ -143,8 +144,13 @@ instance IsExpr Pattern where
data ParseSections = ParseSections | DoNotParseSections
deriving (Eq, Show)
+-- | Runs a parser. If sections should be parsed, then identifiers
+-- with at least two name parts are split up into multiple tokens,
+-- using 'PositionInName' to record the tokens' original positions
+-- within their respective identifiers.
+
parse :: IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
-parse (DoNotParseSections, p) es = Parser.parse p (map NoPlaceholder es)
+parse (DoNotParseSections, p) es = Parser.parse p (map noPlaceholder es)
parse (ParseSections, p) es = Parser.parse p
(concat $ map splitExpr es)
where
@@ -153,11 +159,11 @@ parse (ParseSections, p) es = Parser.parse p
LocalV n -> splitName n
_ -> noSplit
where
- noSplit = [NoPlaceholder e]
+ noSplit = [noPlaceholder e]
splitName n = case last ns of
- NoName{} -> noSplit
- Name r ps -> splitParts r (init ns) Beginning ps
+ Name r ps@(_ : _ : _) -> splitParts r (init ns) Beginning ps
+ _ -> noSplit
where
ns = qnameParts n
@@ -168,13 +174,16 @@ parse (ParseSections, p) es = Parser.parse p
-- Note also that the module qualifier, if any, is only applied
-- to the first name part.
- splitParts _ _ _ [] = []
+ splitParts _ _ _ [] = __IMPOSSIBLE__
splitParts _ _ _ (Hole : []) = [Placeholder End]
+ splitParts r m _ (Id s : []) = [part r m End s]
splitParts r m w (Hole : ps) = Placeholder w : splitParts r m Middle ps
- splitParts r m _ (Id s : ps) = part : splitParts r [] Middle ps
- where
- part = NoPlaceholder $ unExprView $ LocalV $
- foldr Qual (QName (Name r [Id s])) m
+ splitParts r m w (Id s : ps) = part r m w s : splitParts r [] Middle ps
+
+ part r m w s =
+ NoPlaceholder (Strict.Just w)
+ (unExprView $ LocalV $
+ foldr Qual (QName (Name r [Id s])) m)
---------------------------------------------------------------------------
-- * Parser combinators
@@ -196,6 +205,51 @@ partP ms s = do
LocalV y | str == show y -> Just (getRange y)
_ -> Nothing
+-- | Parses a split-up, unqualified name consisting of at least two
+-- name parts.
+--
+-- The parser does not check that underscores and other name parts
+-- alternate. The range of the resulting name is the range of the
+-- first name part that is not an underscore.
+
+atLeastTwoParts :: IsExpr e => Parser e Name
+atLeastTwoParts = do
+ (r, ps) <- parts Beginning
+ case r of
+ Nothing -> __IMPOSSIBLE__
+ Just r -> return (Name r ps)
+ where
+ parts pos = do
+ tok <- token
+ (pos', r, p) <- case tok of
+ Placeholder pos' -> return (pos', Nothing, Hole)
+ NoPlaceholder (Strict.Just pos') e -> case exprView e of
+ LocalV (QName (Name r [Id s])) -> return (pos', Just r, Id s)
+ _ -> empty
+ _ -> empty
+ if pos == Middle && pos' == End then
+ return (r, [p])
+ else if pos' == pos then do
+ (r', ps) <- parts Middle
+ return (maybe r' Just r, p : ps)
+ else
+ empty
+
+-- | Either a wildcard (@_@), or an unqualified name (possibly
+-- containing multiple name parts).
+
+wildOrUnqualifiedName :: IsExpr e => Parser e (Maybe Name)
+wildOrUnqualifiedName =
+ (Nothing <$ partP [] "_")
+ <|>
+ (do e <- notPlaceholder
+ case exprView e of
+ LocalV (QName n) -> return (Just n)
+ WildV _ -> return Nothing
+ _ -> empty)
+ <|>
+ Just <$> atLeastTwoParts
+
-- | Used to define the return type of 'opP'.
type family OperatorType (k :: NotationKind) (e :: *) :: *
@@ -288,13 +342,10 @@ opP parseSections p (NewNotation q names _ syn isOp) kind = do
(r, es) <- worker ms xs
return (r, Right (mkBinding h $ Name noRange [Hole]) : es)
worker ms (BindHole h : xs) = do
- e <- notPlaceholder
- case exprView e of
- LocalV (QName name) -> ret name
- WildV e -> ret (Name noRange [Hole])
- _ -> empty
- -- Old error message: "Expected variable name in binding
- -- position".
+ e <- wildOrUnqualifiedName
+ case e of
+ Just name -> ret name
+ Nothing -> ret (Name noRange [Hole])
where
ret x = do
(r, es) <- worker ms xs
@@ -311,10 +362,10 @@ opP parseSections p (NewNotation q names _ syn isOp) kind = do
NamedArg (MaybePlaceholder (OpApp e))
findExprFor normalHoles binders n =
case [ h | h@(_, m) <- normalHoles, namedArg m == n ] of
- [(Placeholder p, arg)] -> set (Placeholder p) arg
- [(NoPlaceholder e, arg)] -> case [b | (b, m) <- binders, m == n] of
- [] -> set (NoPlaceholder (Ordinary e)) arg -- no variable to bind
- bs -> set (NoPlaceholder (SyntaxBindingLambda (fuseRange bs e) bs e)) arg
+ [(Placeholder p, arg)] -> set (Placeholder p) arg
+ [(NoPlaceholder _ e, arg)] -> case [b | (b, m) <- binders, m == n] of
+ [] -> set (noPlaceholder (Ordinary e)) arg -- no variable to bind
+ bs -> set (noPlaceholder (SyntaxBindingLambda (fuseRange bs e) bs e)) arg
_ -> __IMPOSSIBLE__
noPlaceholders :: [NamedArg (MaybePlaceholder (OpApp e))] -> Int
diff --git a/src/full/Agda/Syntax/Concrete/Pretty.hs b/src/full/Agda/Syntax/Concrete/Pretty.hs
index ed224bc..6683057 100644
--- a/src/full/Agda/Syntax/Concrete/Pretty.hs
+++ b/src/full/Agda/Syntax/Concrete/Pretty.hs
@@ -12,6 +12,7 @@ import Prelude hiding (null)
import Data.Functor
import Data.Maybe
+import qualified Data.Strict.Maybe as Strict
import Agda.Syntax.Common
import Agda.Syntax.Concrete
@@ -105,8 +106,8 @@ instance Pretty (OpApp Expr) where
pretty (SyntaxBindingLambda r bs e) = pretty (Lam r bs e)
instance Pretty a => Pretty (MaybePlaceholder a) where
- pretty Placeholder{} = text "_"
- pretty (NoPlaceholder e) = pretty e
+ pretty Placeholder{} = text "_"
+ pretty (NoPlaceholder _ e) = pretty e
instance Pretty Expr where
pretty e =
@@ -511,7 +512,7 @@ instance Pretty Pattern where
IdentP x -> pretty x
AppP p1 p2 -> sep [ pretty p1, nest 2 $ pretty p2 ]
RawAppP _ ps -> fsep $ map pretty ps
- OpAppP _ q _ ps -> fsep $ prettyOpApp q (fmap (fmap (fmap NoPlaceholder)) ps)
+ OpAppP _ q _ ps -> fsep $ prettyOpApp q (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) ps)
HiddenP _ p -> braces' $ pretty p
InstanceP _ p -> dbraces $ pretty p
ParenP _ p -> parens $ pretty p
@@ -545,7 +546,7 @@ prettyOpApp q es = merge [] $ prOp ms xs es
-- Section underscores should be printed without surrounding
-- whitespace. This function takes care of that.
- merge :: [Doc] -> [(Doc, Maybe Placeholder)] -> [Doc]
+ merge :: [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
merge before [] = reverse before
merge before ((d, Nothing) : after) = merge (d : before) after
merge before ((d, Just Beginning) : after) = mergeRight before d after
diff --git a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
index c246e60..0b856ed 100644
--- a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
+++ b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
@@ -914,7 +914,7 @@ data Hd = HdVar A.Name | HdCon A.QName | HdDef A.QName
cOpApp :: Range -> C.QName -> A.Name -> [C.Expr] -> C.Expr
cOpApp r x n es =
C.OpApp r x (Set.singleton n)
- (map (defaultNamedArg . NoPlaceholder . Ordinary) es)
+ (map (defaultNamedArg . noPlaceholder . Ordinary) es)
tryToRecoverOpApp :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr
tryToRecoverOpApp e def = caseMaybeM (recoverOpApp bracket cOpApp view e) def return
diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
index 4ade91c..ecbb14b 100644
--- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -2049,9 +2049,9 @@ toAbstractOpApp op ns es = do
ScopeM ([A.LamBinding], [NamedArg (Either A.Expr (OpApp e))])
replacePlaceholders [] = return ([], [])
replacePlaceholders (a : as) = case namedArg a of
- NoPlaceholder x -> mapSnd (set (Right x) a :) <$>
- replacePlaceholders as
- Placeholder p -> do
+ NoPlaceholder _ x -> mapSnd (set (Right x) a :) <$>
+ replacePlaceholders as
+ Placeholder _ -> do
x <- freshName noRange "section"
let i = argInfo a
(ls, ns) <- replacePlaceholders as
diff --git a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
index 301333d..2091338 100644
--- a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
@@ -46,6 +46,7 @@ import Agda.Syntax.Fixity
import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA)
import Agda.Syntax.Info as Info
import Agda.Syntax.Abstract as A
+import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import Agda.Syntax.Scope.Base (isNameInScope, inverseScopeLookupName)
@@ -69,6 +70,7 @@ import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
+import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Tuple
@@ -198,16 +200,25 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
-- Ulf, can you add an explanation?
md <- liftTCM $ -- addContext (replicate (length ps) "x") $
displayForm f vs
- reportSLn "reify.display" 20 $
+ reportSLn "reify.display" 60 $
"display form of " ++ show f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n " ++ show md
case md of
- Just d | okDisplayForm d ->
+ Just d | okDisplayForm d -> do
-- In the display term @d@, @var i@ should be a placeholder
-- for the @i@th pattern of @ps@.
-- Andreas, 2014-06-11:
-- Are we sure that @d@ did not use @var i@ otherwise?
- reifyDisplayFormP =<< displayLHS (map namedArg ps) wps d
- _ -> return lhs
+ lhs' <- displayLHS (map namedArg ps) wps d
+ reportSDoc "reify.display" 70 $ do
+ doc <- prettyA lhs'
+ return $ vcat
+ [ text "rewritten lhs to"
+ , text " lhs' = " <+> doc
+ ]
+ reifyDisplayFormP lhs'
+ _ -> do
+ reportSLn "reify.display" 70 $ "display form absent or not valid as lhs"
+ return lhs
where
-- Andreas, 2015-05-03: Ulf, please comment on what
-- is the idea behind okDisplayForm.
@@ -215,13 +226,15 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
-- can serve as a valid left-hand side. That means checking that it is a
-- defined name applied to valid lhs eliminators (projections or
-- applications to constructor patterns).
- okDisplayForm (DWithApp d ds []) = okDisplayForm d && all okDisplayTerm ds
+ okDisplayForm (DWithApp d ds args) =
+ okDisplayForm d && all okDisplayTerm ds && all okToDrop args
+ -- Andreas, 2016-05-03, issue #1950.
+ -- We might drop trailing hidden trivial (=variable) patterns.
okDisplayForm (DTerm (I.Def f vs)) = all okElim vs
okDisplayForm (DDef f es) = all okDElim es
okDisplayForm DDot{} = False
okDisplayForm DCon{} = False
okDisplayForm DTerm{} = False
- okDisplayForm DWithApp{} = False
okDisplayTerm (DTerm v) = okTerm v
okDisplayTerm DDot{} = True
@@ -232,6 +245,12 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
okDElim (I.Apply v) = okDisplayTerm $ unArg v
okDElim I.Proj{} = True
+ okToDrop arg = notVisible arg && case ignoreSharing $ unArg arg of
+ I.Var _ [] -> True
+ I.DontCare{} -> True -- no matching on irrelevant things. __IMPOSSIBLE__ anyway?
+ I.Level{} -> True -- no matching on levels. __IMPOSSIBLE__ anyway?
+ _ -> False
+
okArg = okTerm . unArg
okElim (I.Apply a) = okArg a
diff --git a/src/full/Agda/TypeChecking/Constraints.hs b/src/full/Agda/TypeChecking/Constraints.hs
index 76f3bf3..2271202 100644
--- a/src/full/Agda/TypeChecking/Constraints.hs
+++ b/src/full/Agda/TypeChecking/Constraints.hs
@@ -25,6 +25,7 @@ import Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow)
+import Agda.Utils.Lens
#include "undefined.h"
import Agda.Utils.Impossible
@@ -206,3 +207,12 @@ checkTypeCheckingProblem p = case p of
CheckLambda args body target -> checkPostponedLambda args body target
UnquoteTactic tac hole t -> unquoteTactic tac hole t $ return hole
+debugConstraints :: TCM ()
+debugConstraints = verboseS "tc.constr" 50 $ do
+ awake <- use stAwakeConstraints
+ sleeping <- use stSleepingConstraints
+ reportSDoc "" 0 $ vcat
+ [ text "Current constraints"
+ , nest 2 $ vcat [ text "awake " <+> vcat (map prettyTCM awake)
+ , text "asleep" <+> vcat (map prettyTCM sleeping) ] ]
+
diff --git a/src/full/Agda/TypeChecking/Constraints.hs-boot b/src/full/Agda/TypeChecking/Constraints.hs-boot
index a1d3ba7..0dfd0b6 100644
--- a/src/full/Agda/TypeChecking/Constraints.hs-boot
+++ b/src/full/Agda/TypeChecking/Constraints.hs-boot
@@ -9,3 +9,4 @@ solveAwakeConstraints' :: Bool -> TCM ()
noConstraints :: TCM a -> TCM a
ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
guardConstraint :: Constraint -> TCM () -> TCM ()
+debugConstraints :: TCM ()
diff --git a/src/full/Agda/TypeChecking/Coverage.hs b/src/full/Agda/TypeChecking/Coverage.hs
index 0cb71a1..62707f3 100644
--- a/src/full/Agda/TypeChecking/Coverage.hs
+++ b/src/full/Agda/TypeChecking/Coverage.hs
@@ -551,7 +551,10 @@ computeNeighbourhood delta1 n delta2 d pars ixs hix ps c = do
-- | Entry point from @Interaction.MakeCase@.
splitClauseWithAbsurd :: SplitClause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
-splitClauseWithAbsurd c x = split' Inductive c (BlockingVar x Nothing)
+splitClauseWithAbsurd c x = split' Inductive False c (BlockingVar x Nothing)
+ -- Andreas, 2016-05-03, issue 1950:
+ -- Do not introduce trailing pattern vars after split,
+ -- because this does not work for with-clauses.
-- | Entry point from @TypeChecking.Empty@ and @Interaction.BasicOps@.
-- @splitLast CoInductive@ is used in the @refine@ tactics.
@@ -578,7 +581,7 @@ split :: Induction
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError Covering)
-split ind sc x = fmap blendInAbsurdClause <$> split' ind sc x
+split ind sc x = fmap blendInAbsurdClause <$> split' ind True sc x
where
n = lookupPatternVar sc $ blockingVarNo x
blendInAbsurdClause :: Either SplitClause Covering -> Covering
@@ -613,10 +616,13 @@ lookupPatternVar SClause{ scTel = tel, scPats = pats } x = arg $>
split' :: Induction
-- ^ Coinductive constructors are allowed if this argument is
-- 'CoInductive'.
+ -> Bool
+ -- ^ If 'True', introduce new trailing variable patterns via
+ -- 'fixTarget'.
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))
-split' ind sc@(SClause tel ps _ target) (BlockingVar x mcons) = liftTCM $ runExceptionT $ do
+split' ind fixtarget sc@(SClause tel ps _ target) (BlockingVar x mcons) = liftTCM $ runExceptionT $ do
debugInit tel x ps
@@ -636,6 +642,7 @@ split' ind sc@(SClause tel ps _ target) (BlockingVar x mcons) = liftTCM $ runExc
forM cons $ \ con ->
fmap (con,) <$> do
msc <- computeNeighbourhood delta1 n delta2 d pars ixs x ps con
+ if not fixtarget then return msc else do
Trav.forM msc $ \ sc -> lift $ snd <$> fixTarget sc{ scTarget = target }
case ns of
diff --git a/src/full/Agda/TypeChecking/Errors.hs b/src/full/Agda/TypeChecking/Errors.hs
index 9ac9e6f..5288d6c 100644
--- a/src/full/Agda/TypeChecking/Errors.hs
+++ b/src/full/Agda/TypeChecking/Errors.hs
@@ -839,12 +839,12 @@ instance PrettyTCM TypeError where
unambiguous e = pretty e
isOrdinary :: MaybePlaceholder (C.OpApp e) -> Bool
- isOrdinary (NoPlaceholder (C.Ordinary _)) = True
- isOrdinary _ = False
+ isOrdinary (NoPlaceholder _ (C.Ordinary _)) = True
+ isOrdinary _ = False
fromOrdinary :: MaybePlaceholder (C.OpApp e) -> e
- fromOrdinary (NoPlaceholder (C.Ordinary e)) = e
- fromOrdinary _ = __IMPOSSIBLE__
+ fromOrdinary (NoPlaceholder _ (C.Ordinary e)) = e
+ fromOrdinary _ = __IMPOSSIBLE__
isPlaceholder :: MaybePlaceholder a -> Bool
isPlaceholder Placeholder{} = True
diff --git a/src/full/Agda/TypeChecking/Implicit.hs b/src/full/Agda/TypeChecking/Implicit.hs
index b02fb7c..35282bb 100644
--- a/src/full/Agda/TypeChecking/Implicit.hs
+++ b/src/full/Agda/TypeChecking/Implicit.hs
@@ -16,7 +16,6 @@ import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
-import {-# SOURCE #-} Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.Pretty
import Agda.Utils.Tuple
@@ -53,9 +52,10 @@ implicitNamedArgs n expand t0 = do
mapFst (narg :) <$> implicitNamedArgs (n-1) expand (absApp b v)
_ -> return ([], t0')
where
+ newMeta :: Hiding -> String -> Type -> TCM Term
newMeta Hidden = newNamedValueMeta RunMetaOccursCheck
- newMeta Instance = initializeIFSMeta
- newMeta NotHidden = initializeIFSMeta
+ newMeta Instance = newIFSMeta
+ newMeta NotHidden = newIFSMeta
---------------------------------------------------------------------------
diff --git a/src/full/Agda/TypeChecking/InstanceArguments.hs b/src/full/Agda/TypeChecking/InstanceArguments.hs
index 28c2ee6..bf49093 100644
--- a/src/full/Agda/TypeChecking/InstanceArguments.hs
+++ b/src/full/Agda/TypeChecking/InstanceArguments.hs
@@ -111,14 +111,6 @@ initialIFSCandidates t = do
handle (TypeError _ (Closure {clValue = InternalError _})) = return Nothing
handle err = throwError err
--- | @initializeIFSMeta s t@ generates an instance meta of type @t@
--- with suggested name @s@, possibly with leading lambdas.
-initializeIFSMeta :: String -> Type -> TCM Term
-initializeIFSMeta s t = do
- t <- reduce t -- see Issue 1321
- cands <- initialIFSCandidates t
- newIFSMeta s t cands
-
-- | @findInScope m (v,a)s@ tries to instantiate on of the types @a@s
-- of the candidate terms @v@s to the type @t@ of the metavariable @m@.
-- If successful, meta @m@ is solved with the instantiation of @v@.
@@ -169,6 +161,7 @@ findInScope' m cands = ifM (isFrozen m) (return (Just (cands, Nothing))) $ do
reportSDoc "tc.instance" 70 $ nest 2 $ vcat
[ sep [ prettyTCM v <+> text ":", nest 2 $ prettyTCM t ] | Candidate v t _ <- cands ]
t <- normalise =<< getMetaTypeInContext m
+ insidePi t $ \ t -> do
reportSDoc "tc.instance" 15 $ text "findInScope 3: t =" <+> prettyTCM t
reportSLn "tc.instance" 70 $ "findInScope 3: t: " ++ show t
@@ -177,6 +170,7 @@ findInScope' m cands = ifM (isFrozen m) (return (Just (cands, Nothing))) $ do
ifJustM (areThereNonRigidMetaArguments (unEl t)) (\ m -> return (Just (cands, Just m))) $ do
mcands <- checkCandidates m t cands
+ debugConstraints
case mcands of
Just [] -> do
@@ -192,6 +186,10 @@ findInScope' m cands = ifM (isFrozen m) (return (Just (cands, Nothing))) $ do
, text "for type" <+> prettyTCM t
]
+ -- If we actually solved the constraints we should wake up any held
+ -- instance constraints, to make sure we don't forget about them.
+ wakeConstraints (return . const True)
+ solveAwakeConstraints' False
return Nothing -- We’re done
_ -> do
@@ -201,6 +199,22 @@ findInScope' m cands = ifM (isFrozen m) (return (Just (cands, Nothing))) $ do
prettyTCM (List.map candidateTerm cs)
return (Just (cs, Nothing))
+-- | Precondition: type is spine reduced and ends in a Def or a Var.
+insidePi :: Type -> (Type -> TCM a) -> TCM a
+insidePi t ret =
+ case ignoreSharing $ unEl t of
+ Pi a b -> addContext (absName b, a) $ insidePi (unAbs b) ret
+ Def{} -> ret t
+ Var{} -> ret t
+ Sort{} -> __IMPOSSIBLE__
+ Con{} -> __IMPOSSIBLE__
+ Lam{} -> __IMPOSSIBLE__
+ Lit{} -> __IMPOSSIBLE__
+ Level{} -> __IMPOSSIBLE__
+ MetaV{} -> __IMPOSSIBLE__
+ Shared{} -> __IMPOSSIBLE__
+ DontCare{} -> __IMPOSSIBLE__
+
-- | A meta _M is rigidly constrained if there is a constraint _M us == D vs,
-- for inert D. Such metas can safely be instantiated by recursive instance
-- search, since the constraint limits the solution space.
@@ -309,18 +323,21 @@ areThereNonRigidMetaArguments t = case ignoreSharing t of
-- If the resulting list contains exactly one element, then the state is the
-- same as the one obtained after running the corresponding computation. In
-- all the other cases, the state is reseted.
-filterResetingState :: MetaId -> [Candidate] -> (Candidate -> TCM Bool) -> TCM [Candidate]
+filterResetingState :: MetaId -> [Candidate] -> (Candidate -> TCM YesNoMaybe) -> TCM [Candidate]
filterResetingState m cands f = disableDestructiveUpdate $ do
ctxArgs <- getContextArgs
let ctxElims = map Apply ctxArgs
tryC c = do
ok <- f c
v <- instantiateFull (MetaV m ctxElims)
- a <- instantiateFull =<< (`piApply` ctxArgs) <$> getMetaType m
+ a <- instantiateFull =<< (`piApplyM` ctxArgs) =<< getMetaType m
return (ok, v, a)
result <- mapM (\c -> do bs <- localTCStateSaving (tryC c); return (c, bs)) cands
- let result' = [ (c, v, a, s) | (c, ((True, v, a), s)) <- result ]
- result <- dropSameCandidates m result'
+ let result' = [ (c, v, a, s) | (c, ((r, v, a), s)) <- result, r /= No ]
+ noMaybes = null [ Maybe | (_, ((Maybe, _, _), _)) <- result ]
+ -- It's not safe to compare maybes for equality because they might
+ -- not have instantiated at all.
+ result <- if noMaybes then dropSameCandidates m result' else return result'
case result of
[(c, _, _, s)] -> [c] <$ put s
_ -> return [ c | (c, _, _, _) <- result ]
@@ -355,12 +372,16 @@ dropSameCandidates m cands = do
{- else -} (\ _ -> return False)
`catchError` (\ _ -> return False)
+data YesNoMaybe = Yes | No | Maybe
+ deriving (Show, Eq)
+
-- | Given a meta @m@ of type @t@ and a list of candidates @cands@,
-- @checkCandidates m t cands@ returns a refined list of valid candidates.
checkCandidates :: MetaId -> Type -> [Candidate] -> TCM (Maybe [Candidate])
checkCandidates m t cands = disableDestructiveUpdate $
verboseBracket "tc.instance.candidates" 20 ("checkCandidates " ++ prettyShow m) $
- ifM (anyMetaTypes cands) (return Nothing) $ Just <$> do
+ ifM (anyMetaTypes cands) (return Nothing) $
+ holdConstraints (\ _ -> isIFSConstraint . clValue . theConstraint) $ Just <$> do
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ text "target:" <+> prettyTCM t
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
[ text "candidates"
@@ -379,14 +400,15 @@ checkCandidates m t cands = disableDestructiveUpdate $
MetaV{} -> return True
_ -> anyMetaTypes cands
- checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM Bool
+ checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNoMaybe
checkCandidateForMeta m t (Candidate term t' eti) = do
-- Andreas, 2015-02-07: New metas should be created with range of the
-- current instance meta, thus, we set the range.
mv <- lookupMeta m
setCurrentRange mv $ do
- verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $ do
- liftTCM $ flip catchError handle $ do
+ debugConstraints
+ verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $
+ liftTCM $ runCandidateCheck $ do
reportSLn "tc.instance" 70 $ " t: " ++ show t ++ "\n t':" ++ show t' ++ "\n term: " ++ show term ++ "."
reportSDoc "tc.instance" 20 $ vcat
[ text "checkCandidateForMeta"
@@ -415,24 +437,37 @@ checkCandidates m t cands = disableDestructiveUpdate $
-- unsolvable by the assignment, but don't do this for FindInScope's
-- to prevent loops. We currently also ignore UnBlock constraints
-- to be on the safe side.
+ debugConstraints
solveAwakeConstraints' True
+
verboseS "tc.instance" 15 $ do
sol <- instantiateFull (MetaV m ctxElims)
- reportSDoc "tc.instance" 15 $
- sep [ text "instance search: found solution for" <+> prettyTCM m <> text ":"
- , nest 2 $ prettyTCM sol ]
- return True
+ case sol of
+ MetaV m' _ | m == m' ->
+ reportSDoc "tc.instance" 15 $
+ sep [ text "instance search: maybe solution for" <+> prettyTCM m <> text ":"
+ , nest 2 $ prettyTCM v ]
+ _ ->
+ reportSDoc "tc.instance" 15 $
+ sep [ text "instance search: found solution for" <+> prettyTCM m <> text ":"
+ , nest 2 $ prettyTCM sol ]
where
- handle :: TCErr -> TCM Bool
+ runCandidateCheck check =
+ flip catchError handle $
+ ifNoConstraints_ check
+ (return Yes)
+ (\ _ -> Maybe <$ reportSLn "tc.instance" 50 "assignment inconclusive")
+
+ handle :: TCErr -> TCM YesNoMaybe
handle err = do
reportSDoc "tc.instance" 50 $
text "assignment failed:" <+> prettyTCM err
- return False
+ return No
- isIFSConstraint :: Constraint -> Bool
- isIFSConstraint FindInScope{} = True
- isIFSConstraint UnBlock{} = True -- otherwise test/fail/Issue723 loops
- isIFSConstraint _ = False
+isIFSConstraint :: Constraint -> Bool
+isIFSConstraint FindInScope{} = True
+isIFSConstraint UnBlock{} = True -- otherwise test/fail/Issue723 loops
+isIFSConstraint _ = False
-- | To preserve the invariant that a constructor is not applied to its
-- parameter arguments, we explicitly check whether function term
diff --git a/src/full/Agda/TypeChecking/InstanceArguments.hs-boot b/src/full/Agda/TypeChecking/InstanceArguments.hs-boot
deleted file mode 100644
index 37f2f34..0000000
--- a/src/full/Agda/TypeChecking/InstanceArguments.hs-boot
+++ /dev/null
@@ -1,7 +0,0 @@
-
-module Agda.TypeChecking.InstanceArguments where
-
-import Agda.TypeChecking.Monad.Base (TCM)
-import Agda.Syntax.Internal (Type, Term)
-
-initializeIFSMeta :: String -> Type -> TCM Term
diff --git a/src/full/Agda/TypeChecking/MetaVars.hs b/src/full/Agda/TypeChecking/MetaVars.hs
index 5f5000c..781f249 100644
--- a/src/full/Agda/TypeChecking/MetaVars.hs
+++ b/src/full/Agda/TypeChecking/MetaVars.hs
@@ -177,20 +177,19 @@ newTypeMeta_ = newTypeMeta =<< (workOnTypes $ newSortMeta)
-- newTypeMeta_ = newTypeMeta Inf
-- | @newIFSMeta s t cands@ creates a new "implicit from scope" metavariable
--- of type the output type of @t@ with name suggestion @s@ and initial
--- solution candidates @cands@. If @t@ is a function type, then insert enough
+-- of type the output type of @t@ with name suggestion @s@.
+-- If @t@ is a function type, then insert enough
-- lambdas in front of it.
-newIFSMeta :: MetaNameSuggestion -> Type -> Maybe [Candidate] -> TCM Term
-newIFSMeta s t cands = do
+newIFSMeta :: MetaNameSuggestion -> Type -> TCM Term
+newIFSMeta s t = do
TelV tel t' <- telView t
addCtxTel tel $ do
vs <- getContextArgs
ctx <- getContextTelescope
- teleLam tel <$> newIFSMetaCtx s (telePi_ ctx t') vs (raise (size tel) cands)
+ teleLam tel <$> newIFSMetaCtx s (telePi_ ctx t') vs
--- | Create a new value meta with specific dependencies.
-newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> Maybe [Candidate] -> TCM Term
-newIFSMetaCtx s t vs cands = do
+newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> TCM Term
+newIFSMetaCtx s t vs = do
reportSDoc "tc.meta.new" 50 $ fsep
[ text "new ifs meta:"
, nest 2 $ prettyTCM vs <+> text "|-"
@@ -203,11 +202,11 @@ newIFSMetaCtx s t vs cands = do
reportSDoc "tc.meta.new" 50 $ fsep
[ nest 2 $ pretty x <+> text ":" <+> prettyTCM t
]
- addConstraint $ FindInScope x Nothing cands
+ addConstraint $ FindInScope x Nothing Nothing
etaExpandMetaSafe x
return $ MetaV x $ map Apply vs
-
+-- | Create a new value meta with specific dependencies.
newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM Term
newNamedValueMeta b s t = do
v <- newValueMeta b t
diff --git a/src/full/Agda/TypeChecking/MetaVars.hs-boot b/src/full/Agda/TypeChecking/MetaVars.hs-boot
index 3fcc9ee..fb309ad 100644
--- a/src/full/Agda/TypeChecking/MetaVars.hs-boot
+++ b/src/full/Agda/TypeChecking/MetaVars.hs-boot
@@ -12,7 +12,7 @@ assignTerm :: MetaId -> [Arg String] -> Term -> TCM ()
etaExpandMetaSafe :: MetaId -> TCM ()
assignV :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
assign :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
-newIFSMeta :: String -> Type -> Maybe [Candidate] -> TCM Term
+newIFSMeta :: String -> Type -> TCM Term
newValueMeta :: RunMetaOccursCheck -> Type -> TCM Term
newNamedValueMeta :: RunMetaOccursCheck -> String -> Type -> TCM Term
newTelMeta :: Telescope -> TCM Args
diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs
index 3259ec4..b225c01 100644
--- a/src/full/Agda/TypeChecking/Monad/Base.hs
+++ b/src/full/Agda/TypeChecking/Monad/Base.hs
@@ -713,8 +713,8 @@ buildClosure x = do
type Constraints = [ProblemConstraint]
data ProblemConstraint = PConstr
- { constraintProblem :: ProblemId
- , theConstraint :: Closure Constraint
+ { constraintProblems :: [ProblemId]
+ , theConstraint :: Closure Constraint
}
deriving (Typeable, Show)
diff --git a/src/full/Agda/TypeChecking/Monad/Constraints.hs b/src/full/Agda/TypeChecking/Monad/Constraints.hs
index d5ed5be..4eb0457 100644
--- a/src/full/Agda/TypeChecking/Monad/Constraints.hs
+++ b/src/full/Agda/TypeChecking/Monad/Constraints.hs
@@ -16,6 +16,7 @@ import Agda.TypeChecking.Monad.Options
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Monad
+import Agda.Utils.Except
#include "undefined.h"
import Agda.Utils.Impossible
@@ -30,21 +31,26 @@ stealConstraints pid = do
current <- currentProblem
reportSLn "tc.constr.steal" 50 $ "problem " ++ show current ++ " is stealing problem " ++ show pid ++ "'s constraints!"
-- Rename @pid@ to @current@ in all constraints.
- let rename pc@(PConstr pid' c) | pid' == pid = PConstr current c
- | otherwise = pc
+ let rename pc@(PConstr pids c) | elem pid pids = PConstr (current : pids) c
+ | otherwise = pc
-- We should never steal from an active problem.
whenM (elem pid <$> asks envActiveProblems) __IMPOSSIBLE__
modifyAwakeConstraints $ List.map rename
modifySleepingConstraints $ List.map rename
solvingProblem :: ProblemId -> TCM a -> TCM a
-solvingProblem pid m = verboseBracket "tc.constr.solve" 50 ("working on problem " ++ show pid) $ do
- x <- local (\e -> e { envActiveProblems = pid : envActiveProblems e }) m
- ifNotM (isProblemSolved pid)
- (reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was not solved.")
- $ {- else -} do
- reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was solved!"
- wakeConstraints (return . blockedOn pid . clValue . theConstraint)
+solvingProblem pid = solvingProblems [pid]
+
+solvingProblems :: [ProblemId] -> TCM a -> TCM a
+solvingProblems pids m = verboseBracket "tc.constr.solve" 50 ("working on problems " ++ show pids) $ do
+ x <- local (\e -> e { envActiveProblems = pids ++ envActiveProblems e }) m
+ sequence_
+ [ ifNotM (isProblemSolved pid)
+ (reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was not solved.")
+ $ {- else -} do
+ reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was solved!"
+ wakeConstraints (return . blockedOn pid . clValue . theConstraint)
+ | pid <- pids ]
return x
where
blockedOn pid (Guarded _ pid') = pid == pid'
@@ -53,10 +59,10 @@ solvingProblem pid m = verboseBracket "tc.constr.solve" 50 ("working on problem
isProblemSolved :: ProblemId -> TCM Bool
isProblemSolved pid =
and2M (notElem pid <$> asks envActiveProblems)
- (all ((/= pid) . constraintProblem) <$> getAllConstraints)
+ (all (notElem pid . constraintProblems) <$> getAllConstraints)
getConstraintsForProblem :: ProblemId -> TCM Constraints
-getConstraintsForProblem pid = List.filter ((== pid) . constraintProblem) <$> getAllConstraints
+getConstraintsForProblem pid = List.filter (elem pid . constraintProblems) <$> getAllConstraints
-- | Get the awake constraints
getAwakeConstraints :: TCM Constraints
@@ -67,8 +73,8 @@ wakeConstraints wake = do
c <- use stSleepingConstraints
(wakeup, sleepin) <- partitionM wake c
reportSLn "tc.constr.wake" 50 $
- "waking up " ++ show (List.map constraintProblem wakeup) ++ "\n" ++
- " still sleeping: " ++ show (List.map constraintProblem sleepin)
+ "waking up " ++ show (List.map constraintProblems wakeup) ++ "\n" ++
+ " still sleeping: " ++ show (List.map constraintProblems sleepin)
modifySleepingConstraints $ const sleepin
modifyAwakeConstraints (++ wakeup)
@@ -92,6 +98,23 @@ putAllConstraintsToSleep = do
modifySleepingConstraints $ (++ awakeOnes)
modifyAwakeConstraints $ const []
+data ConstraintStatus = AwakeConstraint | SleepingConstraint
+ deriving (Eq, Show)
+
+-- | Suspend constraints matching the predicate during the execution of the
+-- second argument. Caution: held sleeping constraints will not be woken up
+-- by events that would normally trigger a wakeup call.
+holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
+holdConstraints p m = do
+ (holdAwake, stillAwake) <- partition (p AwakeConstraint) <$> use stAwakeConstraints
+ (holdAsleep, stillAsleep) <- partition (p SleepingConstraint) <$> use stSleepingConstraints
+ stAwakeConstraints .= stillAwake
+ stSleepingConstraints .= stillAsleep
+ let restore = do
+ stAwakeConstraints %= (holdAwake ++)
+ stSleepingConstraints %= (holdAsleep ++)
+ catchError (m <* restore) (\ err -> restore *> throwError err)
+
takeAwakeConstraint :: TCM (Maybe ProblemConstraint)
takeAwakeConstraint = do
cs <- getAwakeConstraints
@@ -105,15 +128,15 @@ getAllConstraints :: TCM Constraints
getAllConstraints = gets $ \s -> s^.stAwakeConstraints ++ s^.stSleepingConstraints
withConstraint :: (Constraint -> TCM a) -> ProblemConstraint -> TCM a
-withConstraint f (PConstr pid c) = do
+withConstraint f (PConstr pids c) = do
-- We should preserve the problem stack and the isSolvingConstraint flag
- (pids, isSolving) <- asks $ envActiveProblems &&& envSolvingConstraints
+ (pids', isSolving) <- asks $ envActiveProblems &&& envSolvingConstraints
enterClosure c $ \c ->
- local (\e -> e { envActiveProblems = pids, envSolvingConstraints = isSolving }) $
- solvingProblem pid (f c)
+ local (\e -> e { envActiveProblems = pids', envSolvingConstraints = isSolving }) $
+ solvingProblems pids (f c)
buildProblemConstraint :: ProblemId -> Constraint -> TCM ProblemConstraint
-buildProblemConstraint pid c = PConstr pid <$> buildClosure c
+buildProblemConstraint pid c = PConstr [pid] <$> buildClosure c
buildConstraint :: Constraint -> TCM ProblemConstraint
buildConstraint c = flip buildProblemConstraint c =<< currentProblem
diff --git a/src/full/Agda/TypeChecking/Pretty.hs b/src/full/Agda/TypeChecking/Pretty.hs
index 75c32ec..d3136c0 100644
--- a/src/full/Agda/TypeChecking/Pretty.hs
+++ b/src/full/Agda/TypeChecking/Pretty.hs
@@ -221,7 +221,7 @@ instance PrettyTCM Relevance where
prettyTCM UnusedArg = empty
instance PrettyTCM ProblemConstraint where
- prettyTCM (PConstr pid c) = brackets (prettyTCM pid) <+> prettyTCM c
+ prettyTCM (PConstr pid c) = prettyList (map prettyTCM pid) <+> prettyTCM c
instance PrettyTCM Constraint where
prettyTCM c = case c of
diff --git a/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs b/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs
index 7380827..0654c61 100644
--- a/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs
+++ b/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs
@@ -602,10 +602,10 @@ dataStrategy k s = do
reportSDoc "tc.lhs.unify" 80 $ text "Type of constructor: " <+> prettyTCM ctype
withMetaInfo' mv $ do
let perm = mvPermutation mv
- tel <- permuteTel perm <$> getContextTelescope
+ tel <- permuteTel perm <$> (instantiateFull =<< getContextTelescope)
reportSDoc "tc.lhs.unify" 100 $ text "Context tel (for new metas): " <+> prettyTCM tel
-- important: create the meta in the same environment as the original meta
- newArgsMetaCtx ctype tel (mvPermutation mv) us
+ newArgsMetaCtx ctype tel perm us
reportSDoc "tc.lhs.unify" 80 $ text "Generated meta args: " <+> prettyTCM margs
noConstraints $ assignV DirEq m us (Con c margs)
return $ Just margs
diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
index 0260c1a..0922ce2 100644
--- a/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
+++ b/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
@@ -1,6 +1,8 @@
{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
#if __GLASGOW_HASKELL__ >= 710
@@ -13,7 +15,7 @@
{-# OPTIONS_GHC -fno-warn-orphans #-}
-module Agda.TypeChecking.Serialise.Instances.Common where
+module Agda.TypeChecking.Serialise.Instances.Common () where
import Control.Applicative
import Control.Monad.Reader
@@ -33,6 +35,7 @@ import Data.Set (Set)
import qualified Data.Set as Set
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
+import Data.Typeable (Typeable)
import Data.Void
import Agda.Syntax.Common
@@ -224,9 +227,24 @@ instance EmbPrj a => EmbPrj (P.Interval' a) where
valu [p, q] = valu2 P.Interval p q
valu _ = malformed
+-- | Ranges are always deserialised as 'noRange'.
+
instance EmbPrj Range where
- icod_ r = icode (P.rangeFile r, P.rangeIntervals r)
- value r = uncurry P.intervalsToRange `fmap` value r
+ icod_ _ = icode0'
+ value _ = return noRange
+
+-- | Ranges that should be serialised properly.
+
+newtype SerialisedRange = SerialisedRange { underlyingRange :: Range }
+ deriving (Typeable)
+
+instance EmbPrj SerialisedRange where
+ icod_ (SerialisedRange r) =
+ icode2' (P.rangeFile r) (P.rangeIntervals r)
+
+ value = vcase valu where
+ valu [a, b] = SerialisedRange <$> valu2 P.intervalsToRange a b
+ valu _ = malformed
instance EmbPrj C.Name where
icod_ (C.NoName a b) = icode2 0 a b
@@ -322,10 +340,12 @@ instance EmbPrj A.ModuleName where
value n = A.MName `fmap` value n
instance EmbPrj A.Name where
- icod_ (A.Name a b c d) = icodeMemo nameD nameC a $ icode4' a b c d
+ icod_ (A.Name a b c d) = icodeMemo nameD nameC a $
+ icode4' a b (SerialisedRange c) d
value = vcase valu where
- valu [a, b, c, d] = valu4 A.Name a b c d
+ valu [a, b, c, d] = valu4 (\a b c -> A.Name a b (underlyingRange c))
+ a b c d
valu _ = malformed
instance EmbPrj a => EmbPrj (C.FieldAssignment' a) where