summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax')
-rw-r--r--src/full/Agda/Syntax/Abstract.hs79
-rw-r--r--src/full/Agda/Syntax/Abstract/Copatterns.hs31
-rw-r--r--src/full/Agda/Syntax/Abstract/Name.hs44
-rw-r--r--src/full/Agda/Syntax/Abstract/Name.hs-boot10
-rw-r--r--src/full/Agda/Syntax/Abstract/Views.hs10
-rw-r--r--src/full/Agda/Syntax/Common.hs128
-rw-r--r--src/full/Agda/Syntax/Concrete.hs134
-rw-r--r--src/full/Agda/Syntax/Concrete/Definitions.hs232
-rw-r--r--src/full/Agda/Syntax/Concrete/Generic.hs9
-rw-r--r--src/full/Agda/Syntax/Concrete/Name.hs35
-rw-r--r--src/full/Agda/Syntax/Concrete/Operators.hs219
-rw-r--r--src/full/Agda/Syntax/Concrete/Operators/Parser.hs24
-rw-r--r--src/full/Agda/Syntax/Concrete/Pretty.hs117
-rw-r--r--src/full/Agda/Syntax/Fixity.hs110
-rw-r--r--src/full/Agda/Syntax/Fixity.hs-boot3
-rw-r--r--src/full/Agda/Syntax/Info.hs6
-rw-r--r--src/full/Agda/Syntax/Internal.hs484
-rw-r--r--src/full/Agda/Syntax/Internal/Defs.hs8
-rw-r--r--src/full/Agda/Syntax/Internal/Generic.hs11
-rw-r--r--src/full/Agda/Syntax/Internal/Pattern.hs30
-rw-r--r--src/full/Agda/Syntax/Notation.hs18
-rw-r--r--src/full/Agda/Syntax/Parser/LookAhead.hs2
-rw-r--r--src/full/Agda/Syntax/Parser/Monad.hs85
-rw-r--r--src/full/Agda/Syntax/Parser/Parser.y144
-rw-r--r--src/full/Agda/Syntax/Position.hs142
-rw-r--r--src/full/Agda/Syntax/Scope/Base.hs13
-rw-r--r--src/full/Agda/Syntax/Scope/Monad.hs84
-rw-r--r--src/full/Agda/Syntax/Translation/AbstractToConcrete.hs279
-rw-r--r--src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs297
-rw-r--r--src/full/Agda/Syntax/Translation/InternalToAbstract.hs539
30 files changed, 1970 insertions, 1357 deletions
diff --git a/src/full/Agda/Syntax/Abstract.hs b/src/full/Agda/Syntax/Abstract.hs
index 406e8f9..ea02ed4 100644
--- a/src/full/Agda/Syntax/Abstract.hs
+++ b/src/full/Agda/Syntax/Abstract.hs
@@ -1,12 +1,12 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+-- GHC 7.4.2 requires this layout for the pragmas. See Issue 1460.
+{-# LANGUAGE CPP,
+ DeriveDataTypeable,
+ DeriveFoldable,
+ DeriveFunctor,
+ DeriveTraversable,
+ FlexibleInstances,
+ MultiParamTypeClasses,
+ TemplateHaskell #-}
{-| The abstract syntax. This is what you get after desugaring and scope
analysis of the concrete syntax. The type checker works on abstract syntax,
@@ -117,7 +117,7 @@ data Axiom
deriving (Typeable, Eq, Ord, Show)
-- | Renaming (generic).
-type Ren a = Map a a
+type Ren a = [(a, a)]
data Declaration
= Axiom Axiom DefInfo ArgInfo QName Expr -- ^ type signature (can be irrelevant and colored, but not hidden)
@@ -170,6 +170,9 @@ data ModuleApplication
data Pragma
= OptionsPragma [String]
| BuiltinPragma String Expr
+ | BuiltinNoDefPragma String QName
+ -- ^ Builtins that do not come with a definition,
+ -- but declare a name for an Agda concept.
| RewritePragma QName
| CompiledPragma QName String
| CompiledExportPragma QName String
@@ -209,20 +212,25 @@ data TypedBindings = TypedBindings Range (Arg TypedBinding)
-- ^ . @(xs : e)@ or @{xs : e}@
deriving (Typeable, Show)
--- | A typed binding. Appears in dependent function spaces, typed lambdas, and
--- telescopes. I might be tempting to simplify this to only bind a single
--- name at a time. This would mean that we would have to typecheck the type
--- several times (@(x y : A)@ vs. @(x : A)(y : A)@).
--- In most cases this wouldn't really be a problem, but it's good
--- principle to not do extra work unless you have to.
+-- | A typed binding. Appears in dependent function spaces, typed lambdas, and
+-- telescopes. It might be tempting to simplify this to only bind a single
+-- name at a time, and translate, say, @(x y : A)@ to @(x : A)(y : A)@
+-- before type-checking. However, this would be slightly problematic:
--
--- (Andreas, 2013-12-10: The more serious problem would that the translation
--- from @(x y : ?)@ to @(x : ?) (y : ?)@ duplicates the hole @?@.
+-- 1. We would have to typecheck the type @A@ several times.
+--
+-- 2. If @A@ contains a meta variable or hole, it would be duplicated
+-- by such a translation.
+--
+-- While 1. is only slightly inefficient, 2. would be an outright bug.
+-- Duplicating @A@ could not be done naively, we would have to make sure
+-- that the metas of the copy are aliases of the metas of the original.
+
data TypedBinding
- = TBind Range [Name] Expr
+ = TBind Range [WithHiding Name] Expr
-- ^ As in telescope @(x y z : A)@ or type @(x y z : A) -> B@.
| TLet Range [LetBinding]
- -- ^
+ -- ^ E.g. @(let x = e)@ or @(let open M)@.
deriving (Typeable, Show)
type Telescope = [TypedBindings]
@@ -244,7 +252,7 @@ data RHS
| AbsurdRHS
| WithRHS QName [Expr] [Clause]
-- ^ The 'QName' is the name of the with function.
- | RewriteRHS [QName] [Expr] RHS [Declaration]
+ | RewriteRHS [(QName, Expr)] RHS [Declaration]
-- ^ The 'QName's are the names of the generated with functions.
-- One for each 'Expr'.
-- The RHS shouldn't be another @RewriteRHS@.
@@ -399,6 +407,16 @@ instance IsProjP a => IsProjP (Named n a) where
Instances
--------------------------------------------------------------------------}
+instance LensHiding TypedBindings where
+ getHiding (TypedBindings _ a) = getHiding a
+ mapHiding f (TypedBindings r a) = TypedBindings r $ mapHiding f a
+
+instance LensHiding LamBinding where
+ getHiding (DomainFree ai _) = getHiding ai
+ getHiding (DomainFull tb) = getHiding tb
+ mapHiding f (DomainFree ai x) = mapHiding f ai `DomainFree` x
+ mapHiding f (DomainFull tb) = DomainFull $ mapHiding f tb
+
instance HasRange LamBinding where
getRange (DomainFree _ x) = getRange x
getRange (DomainFull b) = getRange b
@@ -488,7 +506,7 @@ instance HasRange RHS where
getRange AbsurdRHS = noRange
getRange (RHS e) = getRange e
getRange (WithRHS _ e cs) = fuseRange e cs
- getRange (RewriteRHS _ es rhs wh) = getRange (es, rhs, wh)
+ getRange (RewriteRHS xes rhs wh) = getRange (map snd xes, rhs, wh)
instance HasRange LetBinding where
getRange (LetBind i _ _ _ _ ) = getRange i
@@ -531,17 +549,15 @@ instance KillRange Expr where
killRange (App i e1 e2) = killRange3 App i e1 e2
killRange (WithApp i e es) = killRange3 WithApp i e es
killRange (Lam i b e) = killRange3 Lam i b e
- killRange (AbsurdLam i h) = killRange1 AbsurdLam i h
+ killRange (AbsurdLam i h) = killRange2 AbsurdLam i h
killRange (ExtendedLam i n d ps) = killRange4 ExtendedLam i n d ps
killRange (Pi i a b) = killRange3 Pi i a b
killRange (Fun i a b) = killRange3 Fun i a b
- killRange (Set i n) = Set (killRange i) n
+ killRange (Set i n) = killRange2 Set i n
killRange (Prop i) = killRange1 Prop i
killRange (Let i ds e) = killRange3 Let i ds e
- killRange (Rec i fs) = Rec (killRange i) (map (id -*- killRange) fs)
- killRange (RecUpdate i e fs) = RecUpdate (killRange i)
- (killRange e)
- (map (id -*- killRange) fs)
+ killRange (Rec i fs) = killRange2 Rec i fs
+ killRange (RecUpdate i e fs) = killRange3 RecUpdate i e fs
killRange (ETel tel) = killRange1 ETel tel
killRange (ScopedExpr s e) = killRange1 (ScopedExpr s) e
killRange (QuoteGoal i x e) = killRange3 QuoteGoal i x e
@@ -549,7 +565,7 @@ instance KillRange Expr where
killRange (Quote i) = killRange1 Quote i
killRange (QuoteTerm i) = killRange1 QuoteTerm i
killRange (Unquote i) = killRange1 Unquote i
- killRange (DontCare e) = DontCare e
+ killRange (DontCare e) = killRange1 DontCare e
killRange (PatternSyn x) = killRange1 PatternSyn x
instance KillRange Declaration where
@@ -608,7 +624,7 @@ instance KillRange RHS where
killRange AbsurdRHS = AbsurdRHS
killRange (RHS e) = killRange1 RHS e
killRange (WithRHS q e cs) = killRange3 WithRHS q e cs
- killRange (RewriteRHS x es rhs wh) = killRange4 RewriteRHS x es rhs wh
+ killRange (RewriteRHS xes rhs wh) = killRange3 RewriteRHS xes rhs wh
instance KillRange LetBinding where
killRange (LetBind i info a b c) = killRange5 LetBind i info a b c
@@ -685,7 +701,7 @@ instance AllNames RHS where
allNames (RHS e) = allNames e
allNames AbsurdRHS{} = Seq.empty
allNames (WithRHS q _ cls) = q <| allNames cls
- allNames (RewriteRHS qs _ rhs cls) = Seq.fromList qs >< allNames rhs >< allNames cls
+ allNames (RewriteRHS qes rhs cls) = Seq.fromList (map fst qes) >< allNames rhs >< allNames cls
instance AllNames Expr where
allNames Var{} = Seq.empty
@@ -892,4 +908,3 @@ insertImplicitPatSynArgs wild r ns as = matchArgs r ns as
matchArgs r (n:ns) as = do
(p, as) <- matchNextArg r n as
first ((unArg n, p) :) <$> matchArgs (getRange p) ns as
-
diff --git a/src/full/Agda/Syntax/Abstract/Copatterns.hs b/src/full/Agda/Syntax/Abstract/Copatterns.hs
index 5220c0c..56fe44c 100644
--- a/src/full/Agda/Syntax/Abstract/Copatterns.hs
+++ b/src/full/Agda/Syntax/Abstract/Copatterns.hs
@@ -1,12 +1,11 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
module Agda.Syntax.Abstract.Copatterns (translateCopatternClauses) where
@@ -263,6 +262,10 @@ class Rename e where
rename' :: NameMap -> e -> e
rename' rho = rename (flip lookup rho)
+-- | 'QName's are not renamed.
+instance Rename QName where
+ rename _ q = q
+
instance Rename Expr where
rename rho e =
case e of
@@ -325,19 +328,13 @@ instance Rename RHS where
RHS e -> RHS (rename rho e)
AbsurdRHS -> e
WithRHS n es cs -> WithRHS n (rename rho es) (rename rho cs)
- RewriteRHS ns es r ds -> RewriteRHS ns (rename rho es) (rename rho r) (rename rho ds)
+ RewriteRHS nes r ds -> RewriteRHS (rename rho nes) (rename rho r) (rename rho ds)
instance Rename LHS where
rename rho (LHS i core ps) = LHS i (rename rho core) (rename rho ps)
instance Rename LHSCore where
rename rho = fmap (rename rho) -- only rename in dot patterns
-{-
- rename rho = ren where
- ren e = case e of
- LHSHead f ps -> LHSHead f (ren ps)
- LHSProj d ps1 core ps2 -> LHSProj d (ren ps1) (ren core) (ren ps2)
--}
instance Rename Pattern where
rename rho = fmap (rename rho) -- only rename in dot patterns
@@ -354,6 +351,8 @@ instance Rename a => Rename (Named n a) where
instance Rename a => Rename [a] where
rename rho = map (rename rho)
+instance (Rename a, Rename b) => Rename (a, b) where
+ rename rho (a,b) = (rename rho a, rename rho b)
diff --git a/src/full/Agda/Syntax/Abstract/Name.hs b/src/full/Agda/Syntax/Abstract/Name.hs
index 1e29f4e..f62811b 100644
--- a/src/full/Agda/Syntax/Abstract/Name.hs
+++ b/src/full/Agda/Syntax/Abstract/Name.hs
@@ -1,12 +1,11 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE TypeSynonymInstances #-}
{-| Abstract names carry unique identifiers and stuff.
-}
@@ -288,6 +287,9 @@ instance Pretty ModuleName where
instance Pretty QName where
pretty = hcat . punctuate (text ".") . map pretty . qnameToList
+instance Pretty AmbiguousQName where
+ pretty (AmbQ qs) = hcat $ punctuate (text " | ") $ map pretty qs
+
------------------------------------------------------------------------
-- * Range instances
------------------------------------------------------------------------
@@ -326,23 +328,25 @@ instance SetRange ModuleName where
-- ** KillRange
instance KillRange Name where
- killRange x = x { nameConcrete = killRange $ nameConcrete x
- -- Andreas, 2014-03-30
- -- An experiment: what happens if we preserve
- -- the range of the binding site, but kill all
- -- other ranges before serialization?
- -- Andreas, Makoto, 2014-10-18 AIM XX
- -- Kill all ranges in signature, including nameBindingSite.
- , nameBindingSite = noRange
- }
+ killRange (Name a b c d) = killRange4 Name a b c d
+ -- killRange x = x { nameConcrete = killRange $ nameConcrete x
+ -- -- Andreas, 2014-03-30
+ -- -- An experiment: what happens if we preserve
+ -- -- the range of the binding site, but kill all
+ -- -- other ranges before serialization?
+ -- -- Andreas, Makoto, 2014-10-18 AIM XX
+ -- -- Kill all ranges in signature, including nameBindingSite.
+ -- , nameBindingSite = noRange
+ -- }
instance KillRange ModuleName where
killRange (MName xs) = MName $ killRange xs
instance KillRange QName where
- killRange q = q { qnameModule = killRange $ qnameModule q
- , qnameName = killRange $ qnameName q
- }
+ killRange (QName a b) = killRange2 QName a b
+ -- killRange q = q { qnameModule = killRange $ qnameModule q
+ -- , qnameName = killRange $ qnameName q
+ -- }
instance KillRange AmbiguousQName where
killRange (AmbQ xs) = AmbQ $ killRange xs
diff --git a/src/full/Agda/Syntax/Abstract/Name.hs-boot b/src/full/Agda/Syntax/Abstract/Name.hs-boot
new file mode 100644
index 0000000..187181b
--- /dev/null
+++ b/src/full/Agda/Syntax/Abstract/Name.hs-boot
@@ -0,0 +1,10 @@
+module Agda.Syntax.Abstract.Name where
+
+import {-# SOURCE #-} Agda.Syntax.Fixity (Fixity')
+
+data Name
+
+instance Show Name
+instance Ord Name
+
+nameFixity :: Name -> Fixity'
diff --git a/src/full/Agda/Syntax/Abstract/Views.hs b/src/full/Agda/Syntax/Abstract/Views.hs
index f5a8b55..2262217 100644
--- a/src/full/Agda/Syntax/Abstract/Views.hs
+++ b/src/full/Agda/Syntax/Abstract/Views.hs
@@ -1,6 +1,6 @@
{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE TupleSections #-}
module Agda.Syntax.Abstract.Views where
@@ -59,7 +59,7 @@ deepUnScope = mapExpr unScope
-- * Traversal
-- | Apply an expression rewriting to every subexpression, inside-out.
--- See 'Agda.Syntax.Internal.Generic'
+-- See "Agda.Syntax.Internal.Generic".
class ExprLike a where
foldExpr :: Monoid m => (Expr -> m) -> a -> m
traverseExpr :: (Monad m, Applicative m) => (Expr -> m Expr) -> a -> m a
@@ -214,7 +214,7 @@ instance ExprLike RHS where
RHS e -> fold e
AbsurdRHS{} -> mempty
WithRHS _ es cs -> fold es `mappend` fold cs
- RewriteRHS _ es rhs ds -> fold es `mappend` fold rhs `mappend` fold ds
+ RewriteRHS xes rhs ds -> fold xes `mappend` fold rhs `mappend` fold ds
where fold e = foldExpr f e
traverseExpr f rhs =
@@ -222,7 +222,7 @@ instance ExprLike RHS where
RHS e -> RHS <$> trav e
AbsurdRHS{} -> pure rhs
WithRHS x es cs -> WithRHS x <$> trav es <*> trav cs
- RewriteRHS xs es rhs ds -> RewriteRHS xs <$> trav es <*> trav rhs <*> trav ds
+ RewriteRHS xes rhs ds -> RewriteRHS <$> trav xes <*> trav rhs <*> trav ds
where trav e = traverseExpr f e
instance ExprLike Declaration where
diff --git a/src/full/Agda/Syntax/Common.hs b/src/full/Agda/Syntax/Common.hs
index 381b300..32c4420 100644
--- a/src/full/Agda/Syntax/Common.hs
+++ b/src/full/Agda/Syntax/Common.hs
@@ -1,11 +1,10 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE TypeSynonymInstances #-}
{-| Some common syntactic entities are defined in this module.
-}
@@ -17,16 +16,16 @@ import Data.ByteString.Char8 (ByteString)
import qualified Data.ByteString.Char8 as ByteString
import Data.Foldable
import Data.Hashable
+import Data.Monoid
import Data.Traversable
import Data.Typeable (Typeable)
-import Test.QuickCheck
+import Test.QuickCheck hiding (Small)
import Agda.Syntax.Position
import Agda.Utils.Functor
import Agda.Utils.Pretty
-import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
@@ -73,9 +72,39 @@ instance CoArbitrary Induction where
data Hiding = Hidden | Instance | NotHidden
deriving (Typeable, Show, Eq, Ord)
+-- | 'Hiding' is an idempotent partial monoid, with unit 'NotHidden'.
+-- 'Instance' and 'NotHidden' are incompatible.
+instance Monoid Hiding where
+ mempty = NotHidden
+ mappend NotHidden h = h
+ mappend h NotHidden = h
+ mappend Hidden Hidden = Hidden
+ mappend Instance Instance = Instance
+ mappend _ _ = __IMPOSSIBLE__
+
instance KillRange Hiding where
killRange = id
+-- | Decorating something with 'Hiding' information.
+data WithHiding a = WithHiding Hiding a
+ deriving (Typeable, Eq, Ord, Show, Functor, Foldable, Traversable)
+
+instance Decoration WithHiding where
+ traverseF f (WithHiding h a) = WithHiding h <$> f a
+
+instance Applicative WithHiding where
+ pure = WithHiding mempty
+ WithHiding h f <*> WithHiding h' a = WithHiding (mappend h h') (f a)
+
+instance HasRange a => HasRange (WithHiding a) where
+ getRange = getRange . dget
+
+instance SetRange a => SetRange (WithHiding a) where
+ setRange = fmap . setRange
+
+instance KillRange a => KillRange (WithHiding a) where
+ killRange = fmap killRange
+
-- | A lens to access the 'Hiding' attribute in data structures.
-- Minimal implementation: @getHiding@ and one of @setHiding@ or @mapHiding@.
class LensHiding a where
@@ -93,6 +122,15 @@ instance LensHiding Hiding where
setHiding = const
mapHiding = id
+instance LensHiding (WithHiding a) where
+ getHiding (WithHiding h _) = h
+ setHiding h (WithHiding _ a) = WithHiding h a
+ mapHiding f (WithHiding h a) = WithHiding (f h) a
+
+-- | Monoidal composition of 'Hiding' information in some data.
+mergeHiding :: LensHiding a => WithHiding a -> a
+mergeHiding (WithHiding h a) = mapHiding (mappend h) a
+
-- | @isHidden@ does not apply to 'Instance', only to 'Hidden'.
isHidden :: LensHiding a => a -> Bool
isHidden a = getHiding a == Hidden
@@ -119,27 +157,55 @@ makeInstance = setHiding Instance
-- * Relevance
---------------------------------------------------------------------------
+-- | An constructor argument is big if the sort of its type is bigger than
+-- the sort of the data type. Only parameters (and maybe forced arguments)
+-- are allowed to be big.
+-- @
+-- List : Set -> Set
+-- nil : (A : Set) -> List A
+-- @
+-- @A@ is big in constructor @nil@ as the sort @Set1@ of its type @Set@
+-- is bigger than the sort @Set@ of the data type @List@.
+data Big = Big | Small
+ deriving (Typeable, Show, Eq, Enum, Bounded)
+
+instance Ord Big where
+ Big <= Small = False
+ _ <= _ = True
+
-- | A function argument can be relevant or irrelevant.
--- See 'Agda.TypeChecking.Irrelevance'.
+-- See "Agda.TypeChecking.Irrelevance".
data Relevance
= Relevant -- ^ The argument is (possibly) relevant at compile-time.
| NonStrict -- ^ The argument may never flow into evaluation position.
-- Therefore, it is irrelevant at run-time.
-- It is treated relevantly during equality checking.
| Irrelevant -- ^ The argument is irrelevant at compile- and runtime.
- | Forced -- ^ The argument can be skipped during equality checking
+ | Forced Big -- ^ The argument can be skipped during equality checking
-- because its value is already determined by the type.
+ -- If a constructor argument is big, it has to be regarded
+ -- absent, otherwise we get into paradoxes.
| UnusedArg -- ^ The polarity checker has determined that this argument
-- is unused in the definition. It can be skipped during
-- equality checking but should be mined for solutions
-- of meta-variables with relevance 'UnusedArg'
- deriving (Typeable, Show, Eq, Enum, Bounded)
+ deriving (Typeable, Show, Eq)
+
+allRelevances :: [Relevance]
+allRelevances =
+ [ Relevant
+ , NonStrict
+ , Irrelevant
+ , Forced Small
+ , Forced Big
+ , UnusedArg
+ ]
instance KillRange Relevance where
killRange rel = rel -- no range to kill
instance Arbitrary Relevance where
- arbitrary = elements [minBound..maxBound]
+ arbitrary = elements allRelevances
instance Ord Relevance where
(<=) = moreRelevant
@@ -186,8 +252,8 @@ moreRelevant r r' =
(UnusedArg, _) -> True
(_, UnusedArg) -> False
-- third bottom
- (Forced, _) -> True
- (_, Forced) -> False
+ (Forced{}, _) -> True
+ (_, Forced{}) -> False
-- remaining case
(NonStrict,NonStrict) -> True
@@ -206,7 +272,7 @@ data ArgInfo c = ArgInfo
instance KillRange c => KillRange (ArgInfo c) where
killRange (ArgInfo h r cs) = killRange3 ArgInfo h r cs
-{- FAILED to define a less for ArgInfo, since it is parametrized by c
+{- FAILED to define a lens for ArgInfo, since it is parametrized by c
can't instantiate the following to f c = Arg c e
since Haskell does not have lambda abstraction
@@ -270,12 +336,12 @@ instance Decoration (Arg c) where
instance HasRange a => HasRange (Arg c a) where
getRange = getRange . unArg
+instance SetRange a => SetRange (Arg c a) where
+ setRange r = fmap $ setRange r
+
instance (KillRange c, KillRange a) => KillRange (Arg c a) where
killRange (Arg info a) = killRange2 Arg info a
-instance Sized a => Sized (Arg c a) where
- size = size . unArg
-
instance (Eq a, Eq c) => Eq (Arg c a) where
Arg (ArgInfo h1 _ cs1) x1 == Arg (ArgInfo h2 _ cs2) x2 = (h1, cs1, x1) == (h2, cs2, x2)
@@ -285,11 +351,13 @@ instance (Show a, Show c) => Show (Arg c a) where
showH Hidden s = "{" ++ s ++ "}"
showH NotHidden s = "(" ++ s ++ ")"
showH Instance s = "{{" ++ s ++ "}}"
- showR Irrelevant s = "." ++ s
- showR NonStrict s = "?" ++ s
- showR Forced s = "!" ++ s
- showR UnusedArg s = "k" ++ s -- constant
- showR Relevant s = "r" ++ s -- Andreas: I want to see it explicitly
+ showR r s = case r of
+ Irrelevant -> "." ++ s
+ NonStrict -> "?" ++ s
+ Forced Big -> "!b" ++ s
+ Forced Small -> "!" ++ s
+ UnusedArg -> "k" ++ s -- constant
+ Relevant -> "r" ++ s -- Andreas: I want to see it explicitly
showC cs s = show cs ++ s
instance LensHiding (Arg c e) where
@@ -392,9 +460,6 @@ instance HasRange a => HasRange (Dom c a) where
instance (KillRange c, KillRange a) => KillRange (Dom c a) where
killRange (Dom info a) = killRange2 Dom info a
-instance Sized a => Sized (Dom c a) where
- size = size . unDom
-
instance (Show a, Show c) => Show (Dom c a) where
show = show . argFromDom
@@ -447,12 +512,12 @@ instance Decoration (Named name) where
instance HasRange a => HasRange (Named name a) where
getRange = getRange . namedThing
+instance SetRange a => SetRange (Named name a) where
+ setRange r = fmap $ setRange r
+
instance (KillRange name, KillRange a) => KillRange (Named name a) where
killRange (Named n a) = Named (killRange n) (killRange a)
-instance Sized a => Sized (Named name a) where
- size = size . namedThing
-
instance Show a => Show (Named_ a) where
show (Named Nothing x) = show x
show (Named (Just n) x) = rawNameToString (rangedThing n) ++ " = " ++ show x
@@ -555,6 +620,9 @@ type Arity = Nat
data NameId = NameId Integer Integer
deriving (Eq, Ord, Typeable)
+instance KillRange NameId where
+ killRange = id
+
instance Show NameId where
show (NameId x i) = show x ++ "@" ++ show i
diff --git a/src/full/Agda/Syntax/Concrete.hs b/src/full/Agda/Syntax/Concrete.hs
index 1ba4fa2..bc124d4 100644
--- a/src/full/Agda/Syntax/Concrete.hs
+++ b/src/full/Agda/Syntax/Concrete.hs
@@ -1,10 +1,10 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+-- GHC 7.4.2 requires this layout for the pragmas. See Issue 1460.
+{-# LANGUAGE CPP,
+ DeriveDataTypeable,
+ DeriveFoldable,
+ DeriveFunctor,
+ DeriveTraversable,
+ FlexibleInstances #-}
{-| The concrete syntax is a raw representation of the program text
without any desugaring at all. This is what the parser produces.
@@ -62,6 +62,8 @@ import Data.Typeable (Typeable)
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import Data.List
+import Data.Set (Set)
+
import Agda.Syntax.Position
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import qualified Agda.Syntax.Common as Common
@@ -70,6 +72,7 @@ import Agda.Syntax.Notation
import Agda.Syntax.Literal
import Agda.Syntax.Concrete.Name
+import qualified Agda.Syntax.Abstract.Name as A
import Agda.Utils.Lens
@@ -101,7 +104,14 @@ data Expr
| Underscore !Range (Maybe String) -- ^ ex: @_@ or @_A_5@
| RawApp !Range [Expr] -- ^ before parsing operators
| App !Range Expr (NamedArg Expr) -- ^ ex: @e e@, @e {e}@, or @e {x = e}@
- | OpApp !Range QName [NamedArg (OpApp Expr)] -- ^ ex: @e + e@
+ | OpApp !Range QName (Set A.Name)
+ [NamedArg (OpApp Expr)] -- ^ ex: @e + e@
+ -- The 'QName' is
+ -- possibly ambiguous,
+ -- but it must
+ -- correspond to one of
+ -- the names in the
+ -- set.
| WithApp !Range Expr [Expr] -- ^ ex: @e | e1 | .. | en@
| HiddenArg !Range (Named_ Expr) -- ^ ex: @{e}@ or @{x=e}@
| InstanceArg !Range (Named_ Expr) -- ^ ex: @{{e}}@ or @{{x=e}}@
@@ -131,7 +141,7 @@ data Expr
| Equal !Range Expr Expr -- ^ ex: @a = b@, used internally in the parser
deriving (Typeable)
-instance NFData Expr
+instance NFData Expr where rnf x = seq x ()
-- | Concrete patterns. No literals in patterns at the moment.
data Pattern
@@ -139,7 +149,12 @@ data Pattern
| QuoteP !Range -- ^ @quote@
| AppP Pattern (NamedArg Pattern) -- ^ @p p'@ or @p {x = p'}@
| RawAppP !Range [Pattern] -- ^ @p1..pn@ before parsing operators
- | OpAppP !Range QName [NamedArg Pattern] -- ^ eg: @p => p'@ for operator @_=>_@
+ | OpAppP !Range QName (Set A.Name)
+ [NamedArg Pattern] -- ^ eg: @p => p'@ for operator @_=>_@
+ -- The 'QName' is possibly
+ -- ambiguous, but it must
+ -- correspond to one of
+ -- the names in the set.
| HiddenP !Range (Named_ Pattern) -- ^ @{p}@ or @{x = p}@
| InstanceP !Range (Named_ Pattern) -- ^ @{{p}}@ or @{{x = p}}@
| ParenP !Range Pattern -- ^ @(p)@
@@ -150,7 +165,7 @@ data Pattern
| LitP Literal -- ^ @0@, @1@, etc.
deriving (Typeable)
-instance NFData Pattern
+instance NFData Pattern where rnf x = seq x ()
-- | A lambda binding is either domain free or typed.
type LamBinding = LamBinding' TypedBindings
@@ -162,11 +177,14 @@ data LamBinding' a
-- | A sequence of typed bindings with hiding information. Appears in dependent
-- function spaces, typed lambdas, and telescopes.
+--
+-- If the individual binding contains hiding information as well, the
+-- 'Hiding' in @TypedBindings@ must be the unit 'NotHidden'.
type TypedBindings = TypedBindings' TypedBinding
data TypedBindings' a = TypedBindings !Range (Arg a)
- -- ^ . @(xs : e)@ or @{xs : e}@
+ -- ^ . @(xs : e)@ or @{xs : e}@ or something like @(x {y} _ : e)@.
deriving (Typeable, Functor, Foldable, Traversable)
data BoundName = BName
@@ -187,7 +205,7 @@ mkBoundName x f = BName x x f
type TypedBinding = TypedBinding' Expr
data TypedBinding' e
- = TBind !Range [BoundName] e -- ^ Binding @(x1 ... xn : A)@.
+ = TBind !Range [WithHiding BoundName] e -- ^ Binding @(x1 ... xn : A)@.
| TLet !Range [Declaration] -- ^ Let binding @(let Ds)@ or @(open M args)@.
deriving (Typeable, Functor, Foldable, Traversable)
@@ -239,15 +257,7 @@ data LHSCore
}
deriving (Typeable)
-instance NFData LHSCore
-
-{- TRASH
-lhsCoreToPattern :: LHSCore -> Pattern
-lhsCoreToPattern (LHSHead f args) = OpAppP (fuseRange f args) (unqualify f) args
-lhsCoreToPattern (LHSProj d ps1 lhscore ps2) = OpAppP (fuseRange d ps) (unqualify) ps
- where p = lhsCoreToPattern lhscore
- ps = ps1 ++ p : ps2
--}
+instance NFData LHSCore where rnf x = seq x ()
type RHS = RHS' Expr
data RHS' e
@@ -440,7 +450,7 @@ patternHead p =
AppP p p' -> patternHead p
RawAppP _ [] -> __IMPOSSIBLE__
RawAppP _ (p:_) -> patternHead p
- OpAppP _ name ps -> return $ unqualify name
+ OpAppP _ name _ ps -> return $ unqualify name
HiddenP _ (namedPat) -> patternHead (namedThing namedPat)
ParenP _ p -> patternHead p
WildP _ -> Nothing
@@ -460,7 +470,7 @@ patternNames p =
IdentP x -> [unqualify x]
AppP p p' -> concatMap patternNames [p, namedArg p']
RawAppP _ ps -> concatMap patternNames ps
- OpAppP _ name ps -> unqualify name : concatMap (patternNames . namedArg) ps
+ OpAppP _ name _ ps -> unqualify name : concatMap (patternNames . namedArg) ps
HiddenP _ (namedPat) -> patternNames (namedThing namedPat)
ParenP _ p -> patternNames p
WildP _ -> []
@@ -475,6 +485,26 @@ patternNames p =
Instances
--------------------------------------------------------------------------}
+-- Lenses
+------------------------------------------------------------------------
+
+instance LensRelevance TypedBindings where
+ getRelevance (TypedBindings _ b) = getRelevance b
+ mapRelevance f (TypedBindings r b) = TypedBindings r $ mapRelevance f b
+
+instance LensHiding TypedBindings where
+ getHiding (TypedBindings _ b) = getHiding b
+ mapHiding f (TypedBindings r b) = TypedBindings r $ mapHiding f b
+
+instance LensHiding LamBinding where
+ getHiding (DomainFree ai _) = getHiding ai
+ getHiding (DomainFull a) = getHiding a
+ mapHiding f (DomainFree ai x) = DomainFree (mapHiding f ai) x
+ mapHiding f (DomainFull a) = DomainFull $ mapHiding f a
+
+-- HasRange instances
+------------------------------------------------------------------------
+
instance HasRange e => HasRange (OpApp e) where
getRange e = case e of
Ordinary e -> getRange e
@@ -489,7 +519,7 @@ instance HasRange Expr where
Underscore r _ -> r
App r _ _ -> r
RawApp r _ -> r
- OpApp r _ _ -> r
+ OpApp r _ _ _ -> r
WithApp r _ _ -> r
Lam r _ _ -> r
AbsurdLam r _ -> r
@@ -617,7 +647,7 @@ instance HasRange AsName where
instance HasRange Pattern where
getRange (IdentP x) = getRange x
getRange (AppP p q) = fuseRange p q
- getRange (OpAppP r _ _) = r
+ getRange (OpAppP r _ _ _) = r
getRange (RawAppP r _) = r
getRange (ParenP r _) = r
getRange (WildP r) = r
@@ -629,6 +659,30 @@ instance HasRange Pattern where
getRange (InstanceP r _) = r
getRange (DotP r _) = r
+-- SetRange instances
+------------------------------------------------------------------------
+
+instance SetRange TypedBindings where
+ setRange r (TypedBindings _ b) = TypedBindings r b
+
+instance SetRange Pattern where
+ setRange r (IdentP x) = IdentP (setRange r x)
+ setRange r (AppP p q) = AppP (setRange r p) (setRange r q)
+ setRange r (OpAppP _ x ns ps) = OpAppP r x ns ps
+ setRange r (RawAppP _ ps) = RawAppP r ps
+ setRange r (ParenP _ p) = ParenP r p
+ setRange r (WildP _) = WildP r
+ setRange r (AsP _ x p) = AsP r (setRange r x) p
+ setRange r (AbsurdP _) = AbsurdP r
+ setRange r (LitP l) = LitP (setRange r l)
+ setRange r (QuoteP _) = QuoteP r
+ setRange r (HiddenP _ p) = HiddenP r p
+ setRange r (InstanceP _ p) = InstanceP r p
+ setRange r (DotP _ e) = DotP r e
+
+-- KillRange instances
+------------------------------------------------------------------------
+
instance KillRange AsName where
killRange (AsName n _) = killRange1 (flip AsName noRange) n
@@ -666,7 +720,7 @@ instance KillRange Expr where
killRange (Underscore _ n) = Underscore noRange n
killRange (RawApp _ e) = killRange1 (RawApp noRange) e
killRange (App _ e a) = killRange2 (App noRange) e a
- killRange (OpApp _ n o) = killRange2 (OpApp noRange) n o
+ killRange (OpApp _ n ns o) = killRange3 (OpApp noRange) n ns o
killRange (WithApp _ e es) = killRange2 (WithApp noRange) e es
killRange (HiddenArg _ n) = killRange1 (HiddenArg noRange) n
killRange (InstanceArg _ n) = killRange1 (InstanceArg noRange) n
@@ -720,19 +774,19 @@ instance KillRange e => KillRange (OpApp e) where
killRange (Ordinary e) = killRange1 Ordinary e
instance KillRange Pattern where
- killRange (IdentP q) = killRange1 IdentP q
- killRange (AppP p n) = killRange2 AppP p n
- killRange (RawAppP _ p) = killRange1 (RawAppP noRange) p
- killRange (OpAppP _ n p) = killRange2 (OpAppP noRange) n p
- killRange (HiddenP _ n) = killRange1 (HiddenP noRange) n
- killRange (InstanceP _ n) = killRange1 (InstanceP noRange) n
- killRange (ParenP _ p) = killRange1 (ParenP noRange) p
- killRange (WildP _) = WildP noRange
- killRange (AbsurdP _) = AbsurdP noRange
- killRange (AsP _ n p) = killRange2 (AsP noRange) n p
- killRange (DotP _ e) = killRange1 (DotP noRange) e
- killRange (LitP l) = killRange1 LitP l
- killRange (QuoteP _) = QuoteP noRange
+ killRange (IdentP q) = killRange1 IdentP q
+ killRange (AppP p n) = killRange2 AppP p n
+ killRange (RawAppP _ p) = killRange1 (RawAppP noRange) p
+ killRange (OpAppP _ n ns p) = killRange3 (OpAppP noRange) n ns p
+ killRange (HiddenP _ n) = killRange1 (HiddenP noRange) n
+ killRange (InstanceP _ n) = killRange1 (InstanceP noRange) n
+ killRange (ParenP _ p) = killRange1 (ParenP noRange) p
+ killRange (WildP _) = WildP noRange
+ killRange (AbsurdP _) = AbsurdP noRange
+ killRange (AsP _ n p) = killRange2 (AsP noRange) n p
+ killRange (DotP _ e) = killRange1 (DotP noRange) e
+ killRange (LitP l) = killRange1 LitP l
+ killRange (QuoteP _) = QuoteP noRange
instance KillRange Pragma where
killRange (OptionsPragma _ s) = OptionsPragma noRange s
diff --git a/src/full/Agda/Syntax/Concrete/Definitions.hs b/src/full/Agda/Syntax/Concrete/Definitions.hs
index acc46d1..af11faf 100644
--- a/src/full/Agda/Syntax/Concrete/Definitions.hs
+++ b/src/full/Agda/Syntax/Concrete/Definitions.hs
@@ -1,9 +1,13 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+-- GHC 7.4.2 requires this layout for the pragmas. See Issue 1460.
+{-# LANGUAGE CPP,
+ DeriveDataTypeable,
+ FlexibleInstances,
+ PatternGuards,
+ TupleSections #-}
+
+#if __GLASGOW_HASKELL__ >= 710
+{-# LANGUAGE FlexibleContexts #-}
+#endif
-- | Preprocess 'Agda.Syntax.Concrete.Declaration's, producing 'NiceDeclaration's.
--
@@ -39,15 +43,28 @@ module Agda.Syntax.Concrete.Definitions
, Measure
) where
+import Prelude hiding (null)
+
import Control.Arrow ((***))
-import Control.Applicative
+import Control.Applicative hiding (empty)
import Control.Monad.State
-import Data.Foldable hiding (concatMap, mapM_, notElem, elem, all)
+import Data.Foldable hiding
+ ( all
+ , concatMap
+ , elem
+ , mapM_
+ , notElem
+#if MIN_VERSION_base(4,8,0)
+ , null
+#endif
+ )
+
import qualified Data.Map as Map
import Data.Map (Map)
+import Data.Maybe
import Data.Monoid ( Monoid(mappend, mempty) )
-import Data.List as List
+import Data.List as List hiding (null)
import Data.Traversable (traverse)
import Data.Typeable (Typeable)
@@ -63,6 +80,7 @@ import Agda.Utils.Except ( Error(noMsg, strMsg), MonadError(throwError) )
import Agda.Utils.Lens
import Agda.Utils.List (headMaybe, isSublistOf)
import Agda.Utils.Monad
+import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.Update
@@ -79,28 +97,32 @@ import Agda.Utils.Impossible
modifiers have been distributed to the individual declarations.
-}
data NiceDeclaration
- = Axiom Range Fixity' Access IsInstance ArgInfo Name Expr
- -- ^ Axioms and functions can be declared irrelevant. (Hiding should be NotHidden)
- | NiceField Range Fixity' Access IsAbstract Name (Arg Expr)
- | PrimitiveFunction Range Fixity' Access IsAbstract Name Expr
- | NiceMutual Range TerminationCheck [NiceDeclaration]
- | NiceModule Range Access IsAbstract QName Telescope [Declaration]
- | NiceModuleMacro Range Access Name ModuleApplication OpenShortHand ImportDirective
- | NiceOpen Range QName ImportDirective
- | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
- | NicePragma Range Pragma
- | NiceRecSig Range Fixity' Access Name [LamBinding] Expr
- | NiceDataSig Range Fixity' Access Name [LamBinding] Expr
- | NiceFunClause Range Access IsAbstract TerminationCheck Declaration
- -- ^ a uncategorized function clause, could be a function clause
- -- without type signature or a pattern lhs (e.g. for irrefutable let)x
- | FunSig Range Fixity' Access IsInstance ArgInfo TerminationCheck Name Expr
- | FunDef Range [Declaration] Fixity' IsAbstract TerminationCheck Name [Clause] -- ^ block of function clauses (we have seen the type signature before)
- | DataDef Range Fixity' IsAbstract Name [LamBinding] [NiceConstructor]
- | RecDef Range Fixity' IsAbstract Name (Maybe (Ranged Induction)) (Maybe (ThingWithFixity Name)) [LamBinding] [NiceDeclaration]
- | NicePatternSyn Range Fixity' Name [Arg Name] Pattern
- | NiceUnquoteDecl Range Fixity' Access IsAbstract TerminationCheck Name Expr
- deriving (Typeable, Show)
+ = Axiom Range Fixity' Access IsInstance ArgInfo Name Expr
+ -- ^ Axioms and functions can be declared irrelevant. (Hiding should be NotHidden)
+ | NiceField Range Fixity' Access IsAbstract Name (Arg Expr)
+ | PrimitiveFunction Range Fixity' Access IsAbstract Name Expr
+ | NiceMutual Range TerminationCheck [NiceDeclaration]
+ | NiceModule Range Access IsAbstract QName Telescope [Declaration]
+ | NiceModuleMacro Range Access Name ModuleApplication OpenShortHand ImportDirective
+ | NiceOpen Range QName ImportDirective
+ | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
+ | NicePragma Range Pragma
+ | NiceRecSig Range Fixity' Access Name [LamBinding] Expr
+ | NiceDataSig Range Fixity' Access Name [LamBinding] Expr
+ | NiceFunClause Range Access IsAbstract TerminationCheck Declaration
+ -- ^ An uncategorized function clause, could be a function clause
+ -- without type signature or a pattern lhs (e.g. for irrefutable let).
+ -- The 'Declaration' is the actual 'FunClause'.
+ | FunSig Range Fixity' Access IsInstance ArgInfo TerminationCheck Name Expr
+ | FunDef Range [Declaration] Fixity' IsAbstract TerminationCheck Name [Clause]
+ -- ^ Block of function clauses (we have seen the type signature before).
+ -- The 'Declaration's are the original declarations that were processed
+ -- into this 'FunDef' and are only used in 'notSoNiceDeclaration'.
+ | DataDef Range Fixity' IsAbstract Name [LamBinding] [NiceConstructor]
+ | RecDef Range Fixity' IsAbstract Name (Maybe (Ranged Induction)) (Maybe (ThingWithFixity Name)) [LamBinding] [NiceDeclaration]
+ | NicePatternSyn Range Fixity' Name [Arg Name] Pattern
+ | NiceUnquoteDecl Range Fixity' Access IsInstance IsAbstract TerminationCheck Name Expr
+ deriving (Typeable, Show)
type TerminationCheck = Common.TerminationCheck Measure
@@ -121,6 +143,8 @@ data Clause = Clause Name LHS RHS WhereClause [Clause]
-- | The exception type.
data DeclarationException
= MultipleFixityDecls [(Name, [Fixity'])]
+ | InvalidName Name
+ | DuplicateDefinition Name
| MissingDefinition Name
| MissingWithClauses Name
| MissingTypeSignature LHS -- Andreas 2012-06-02: currently unused, remove after a while -- Fredrik 2012-09-20: now used, can we keep it?
@@ -147,6 +171,8 @@ data DeclarationException
instance HasRange DeclarationException where
getRange (MultipleFixityDecls xs) = getRange (fst $ head xs)
+ getRange (InvalidName x) = getRange x
+ getRange (DuplicateDefinition x) = getRange x
getRange (MissingDefinition x) = getRange x
getRange (MissingWithClauses x) = getRange x
getRange (MissingTypeSignature x) = getRange x
@@ -184,7 +210,7 @@ instance HasRange NiceDeclaration where
getRange (NiceDataSig r _ _ _ _ _) = r
getRange (NicePatternSyn r _ _ _ _) = r
getRange (NiceFunClause r _ _ _ _) = r
- getRange (NiceUnquoteDecl r _ _ _ _ _ _) = r
+ getRange (NiceUnquoteDecl r _ _ _ _ _ _ _) = r
instance Error DeclarationException where
noMsg = strMsg ""
@@ -192,46 +218,53 @@ instance Error DeclarationException where
-- These error messages can (should) be terminated by a dot ".",
-- there is no error context printed after them.
-instance Show DeclarationException where
- show (MultipleFixityDecls xs) = show $
+instance Pretty DeclarationException where
+ pretty (MultipleFixityDecls xs) =
sep [ fsep $ pwords "Multiple fixity or syntax declarations for"
, vcat $ map f xs
]
where
f (x, fs) = pretty x <> text ": " <+> fsep (map pretty fs)
- show (MissingDefinition x) = show $ fsep $
+ pretty (InvalidName x) = fsep $
+ pwords "Invalid name:" ++ [pretty x]
+ pretty (DuplicateDefinition x) = fsep $
+ pwords "Duplicate definition of" ++ [pretty x]
+ pretty (MissingDefinition x) = fsep $
pwords "Missing definition for" ++ [pretty x]
- show (MissingWithClauses x) = show $ fsep $
+ pretty (MissingWithClauses x) = fsep $
pwords "Missing with-clauses for function" ++ [pretty x]
- show (MissingTypeSignature x) = show $ fsep $
+ pretty (MissingTypeSignature x) = fsep $
pwords "Missing type signature for left hand side" ++ [pretty x]
- show (MissingDataSignature x) = show $ fsep $
+ pretty (MissingDataSignature x) = fsep $
pwords "Missing type signature for " ++ [pretty x]
- show (WrongDefinition x k k') = show $ fsep $ pretty x :
+ pretty (WrongDefinition x k k') = fsep $ pretty x :
pwords ("has been declared as a " ++ show k ++
", but is being defined as a " ++ show k')
- show (WrongParameters x) = show $ fsep $
+ pretty (WrongParameters x) = fsep $
pwords "List of parameters does not match previous signature for" ++ [pretty x]
- show (AmbiguousFunClauses lhs xs) = show $ fsep $
- pwords "More than one matching type signature for left hand side" ++ [pretty lhs] ++
- pwords "it could belong to any of:" ++ map pretty xs
- show (UnknownNamesInFixityDecl xs) = show $ fsep $
+ pretty (AmbiguousFunClauses lhs xs) = sep
+ [ fsep $
+ pwords "More than one matching type signature for left hand side " ++ [pretty lhs] ++
+ pwords "it could belong to any of:"
+ , vcat $ map (pretty . PrintRange) xs
+ ]
+ pretty (UnknownNamesInFixityDecl xs) = fsep $
pwords "The following names are not declared in the same scope as their syntax or fixity declaration (i.e., either not in scope at all, imported from another module, or declared in a super module):" ++ map pretty xs
- show (UselessPrivate _) = show $ fsep $
+ pretty (UselessPrivate _) = fsep $
pwords "Using private here has no effect. Private applies only to declarations that introduce new identifiers into the module, like type signatures and data, record, and module declarations."
- show (UselessAbstract _) = show $ fsep $
+ pretty (UselessAbstract _) = fsep $
pwords "Using abstract here has no effect. Abstract applies only definitions like data definitions, record type definitions and function clauses."
- show (UselessInstance _) = show $ fsep $
+ pretty (UselessInstance _) = fsep $
pwords "Using instance here has no effect. Instance applies only to declarations that introduce new identifiers into the module, like type signatures and axioms."
- show (WrongContentPostulateBlock _) = show $ fsep $
+ pretty (WrongContentPostulateBlock _) = fsep $
pwords "A postulate block can only contain type signatures or instance blocks"
- show (PragmaNoTerminationCheck _) = show $ fsep $
+ pretty (PragmaNoTerminationCheck _) = fsep $
pwords "Pragma {-# NO_TERMINATION_CHECK #-} has been removed. To skip the termination check, label your definitions either as {-# TERMINATING #-} or {-# NON_TERMINATING #-}."
- show (InvalidTerminationCheckPragma _) = show $ fsep $
+ pretty (InvalidTerminationCheckPragma _) = fsep $
pwords "Termination checking pragmas can only precede a mutual block or a function definition."
- show (InvalidMeasureMutual _) = show $ fsep $
+ pretty (InvalidMeasureMutual _) = fsep $
pwords "In a mutual block, either all functions must have the same (or no) termination checking pragma."
- show (NotAllowedInMutual nd) = show $ fsep $
+ pretty (NotAllowedInMutual nd) = fsep $
[text $ decl nd] ++ pwords "are not allowed in mutual blocks"
where
decl Axiom{} = "Postulates"
@@ -252,10 +285,10 @@ instance Show DeclarationException where
decl FunDef{} = __IMPOSSIBLE__
decl RecDef{} = __IMPOSSIBLE__
decl DataDef{} = __IMPOSSIBLE__
- show (Codata _) =
+ pretty (Codata _) = text $
"The codata construction has been removed. " ++
"Use the INFINITY builtin instead."
- show (DeclarationPanic s) = s
+ pretty (DeclarationPanic s) = text s
{--------------------------------------------------------------------------
The niceifier
@@ -336,15 +369,15 @@ data NiceEnv = NiceEnv
, fixs :: Fixities
}
-type LoneSigs = [(DataRecOrFun, Name)]
+type LoneSigs = Map Name DataRecOrFun
type Fixities = Map Name Fixity'
-- | Initial nicifier state.
initNiceEnv :: NiceEnv
initNiceEnv = NiceEnv
- { _loneSigs = []
- , fixs = Map.empty
+ { _loneSigs = empty
+ , fixs = empty
}
-- * Handling the lone signatures, stored to infer mutual blocks.
@@ -356,18 +389,22 @@ loneSigs f e = f (_loneSigs e) <&> \ s -> e { _loneSigs = s }
-- | Adding a lone signature to the state.
-addLoneSig :: DataRecOrFun -> Name -> Nice ()
-addLoneSig k x = loneSigs %= ((k, x) :)
+addLoneSig :: Name -> DataRecOrFun -> Nice ()
+addLoneSig x k = loneSigs %== \ s -> do
+ let (mr, s') = Map.insertLookupWithKey (\ k new old -> new) x k s
+ case mr of
+ Nothing -> return s'
+ Just{} -> throwError $ DuplicateDefinition x
-- | Remove a lone signature from the state.
removeLoneSig :: Name -> Nice ()
-removeLoneSig x = loneSigs %= filter (\ (k', x') -> x /= x')
+removeLoneSig x = loneSigs %= Map.delete x
-- | Search for forward type signature.
getSig :: Name -> Nice (Maybe DataRecOrFun)
-getSig n = fmap fst . List.find (\ (k, x) -> x == n) <$> use loneSigs
+getSig x = Map.lookup x <$> use loneSigs
-- | Check that no lone signatures are left in the state.
@@ -376,15 +413,17 @@ noLoneSigs = null <$> use loneSigs
-- | Ensure that all forward declarations have been given a definition.
-checkLoneSigs :: LoneSigs -> Nice ()
+checkLoneSigs :: [(Name, a)] -> Nice ()
checkLoneSigs xs =
case xs of
[] -> return ()
- (_, x):_ -> throwError $ MissingDefinition x
-
+ (x, _):_ -> throwError $ MissingDefinition x
+-- | Check whether name is not "_" and return its fixity.
getFixity :: Name -> Nice Fixity'
-getFixity x = gets $ Map.findWithDefault defaultFixity' x . fixs
+getFixity x = do
+ when (isUnderscore x) $ throwError $ InvalidName x
+ gets $ Map.findWithDefault defaultFixity' x . fixs
runNice :: Nice a -> Either DeclarationException a
runNice nice = nice `evalStateT` initNiceEnv
@@ -425,7 +464,7 @@ niceDeclarations ds = do
put $ initNiceEnv { fixs = fixs }
ds <- nice ds
-- Check that every signature got its definition.
- checkLoneSigs =<< use loneSigs
+ checkLoneSigs . Map.toList =<< use loneSigs
-- Note that loneSigs is ensured to be empty.
-- (Important, since inferMutualBlocks also uses loneSigs state).
inferMutualBlocks ds
@@ -467,7 +506,7 @@ niceDeclarations ds = do
OtherDecl -> (d :) <$> inferMutualBlocks ds
LoneDef _ x -> __IMPOSSIBLE__
LoneSig k x -> do
- addLoneSig k x
+ addLoneSig x k
(tcs, (ds0, ds1)) <- untilAllDefined [terminationCheck k] ds
tc <- combineTermChecks (getRange d) tcs
@@ -486,9 +525,9 @@ niceDeclarations ds = do
done <- noLoneSigs
if done then return (tc, ([], ds)) else
case ds of
- [] -> __IMPOSSIBLE__ <$ (checkLoneSigs =<< use loneSigs)
+ [] -> __IMPOSSIBLE__ <$ (checkLoneSigs . Map.toList =<< use loneSigs)
d : ds -> case declKind d of
- LoneSig k x -> addLoneSig k x >> cons d (untilAllDefined (terminationCheck k : tc) ds)
+ LoneSig k x -> addLoneSig x k >> cons d (untilAllDefined (terminationCheck k : tc) ds)
LoneDef k x -> removeLoneSig x >> cons d (untilAllDefined (terminationCheck k : tc) ds)
OtherDecl -> cons d (untilAllDefined tc ds)
where
@@ -512,8 +551,8 @@ niceDeclarations ds = do
nice (Pragma (TerminationCheckPragma r tc) : d@FunClause{} : ds) | notMeasure tc =
niceFunClause tc d ds
nice (Pragma (TerminationCheckPragma r tc) : ds@(UnquoteDecl{} : _)) | notMeasure tc = do
- NiceUnquoteDecl r f p a _ x e : ds <- nice ds
- return $ NiceUnquoteDecl r f p a tc x e : ds
+ NiceUnquoteDecl r f p a i _ x e : ds <- nice ds
+ return $ NiceUnquoteDecl r f p a i tc x e : ds
nice (d@TypeSig{} : Pragma (TerminationCheckPragma r (TerminationMeasure _ x)) : ds) =
niceTypeSig (TerminationMeasure r x) d ds
@@ -528,7 +567,7 @@ niceDeclarations ds = do
DataSig r CoInductive x tel t -> throwError (Codata r)
Data r CoInductive x tel t cs -> throwError (Codata r)
DataSig r Inductive x tel t -> do
- addLoneSig (DataName $ parameters tel) x
+ addLoneSig x (DataName $ parameters tel)
(++) <$> dataOrRec DataDef NiceDataSig niceAxioms r x tel (Just t) Nothing
<*> nice ds
Data r Inductive x tel t cs -> do
@@ -536,7 +575,7 @@ niceDeclarations ds = do
(++) <$> dataOrRec DataDef NiceDataSig niceAxioms r x tel t (Just cs)
<*> nice ds
RecordSig r x tel t -> do
- addLoneSig (RecName $ parameters tel) x
+ addLoneSig x (RecName $ parameters tel)
fx <- getFixity x
(NiceRecSig r fx PublicAccess x tel t :) <$> nice ds
Record r x i c tel t cs -> do
@@ -580,7 +619,7 @@ niceDeclarations ds = do
UnquoteDecl r x e -> do
fx <- getFixity x
- (NiceUnquoteDecl r fx PublicAccess ConcreteDef TerminationCheck x e :) <$> nice ds
+ (NiceUnquoteDecl r fx PublicAccess NotInstanceDef ConcreteDef TerminationCheck x e :) <$> nice ds
-- Andreas, AIM XX: do not forbid NO_TERMINATION_CHECK in maintenance version.
-- Pragma (TerminationCheckPragma r NoTerminationCheck) ->
-- throwError $ PragmaNoTerminationCheck r
@@ -590,7 +629,7 @@ niceDeclarations ds = do
niceFunClause :: TerminationCheck -> Declaration -> [Declaration] -> Nice [NiceDeclaration]
niceFunClause termCheck d@(FunClause lhs _ _) ds = do
- xs <- map snd . filter (isFunName . fst) <$> use loneSigs
+ xs <- map fst . filter (isFunName . snd) . Map.toList <$> use loneSigs
-- for each type signature 'x' waiting for clauses, we try
-- if we have some clauses for 'x'
fixs <- gets fixs
@@ -626,14 +665,14 @@ niceDeclarations ds = do
return $ d : ds1
-- case: clauses match more than one sigs (ambiguity)
- l -> throwError $ AmbiguousFunClauses lhs (map fst l) -- "ambiguous function clause; cannot assign it uniquely to one type signature"
+ l -> throwError $ AmbiguousFunClauses lhs $ reverse $ map fst l -- "ambiguous function clause; cannot assign it uniquely to one type signature"
niceFunClause _ _ _ = __IMPOSSIBLE__
niceTypeSig :: TerminationCheck -> Declaration -> [Declaration] -> Nice [NiceDeclaration]
niceTypeSig termCheck d@(TypeSig info x t) ds = do
fx <- getFixity x
-- register x as lone type signature, to recognize clauses later
- addLoneSig (FunName termCheck) x
+ addLoneSig x (FunName termCheck)
ds <- nice ds
return $ FunSig (getRange d) fx PublicAccess NotInstanceDef info termCheck x t : ds
niceTypeSig _ _ _ = __IMPOSSIBLE__
@@ -653,13 +692,15 @@ niceDeclarations ds = do
dataOrRec mkDef mkSig niceD r x tel mt mcs = do
mds <- traverse niceD mcs
f <- getFixity x
- return $
- [mkSig (fuseRange x t) f PublicAccess x tel t | Just t <- [mt] ] ++
- [mkDef (getRange x) f ConcreteDef x (concatMap dropType tel) ds | Just ds <- [mds] ]
+ return $ catMaybes $
+ [ mt <&> \ t -> mkSig (fuseRange x t) f PublicAccess x tel t
+ , mkDef r f ConcreteDef x (concatMap dropType tel) <$> mds
+ ]
where
- dropType (DomainFull (TypedBindings r (Common.Arg i (TBind _ xs _)))) =
- map (DomainFree i) xs
- dropType (DomainFull (TypedBindings _ (Common.Arg _ TLet{}))) = []
+ dropType :: LamBinding -> [LamBinding]
+ dropType (DomainFull (TypedBindings _r (Common.Arg ai (TBind _ xs _)))) =
+ map (mergeHiding . fmap (DomainFree ai)) xs
+ dropType (DomainFull (TypedBindings _r (Common.Arg _ TLet{}))) = []
dropType b@DomainFree{} = [b]
-- Translate axioms
@@ -702,10 +743,10 @@ niceDeclarations ds = do
d : expand p ps ds
where
expand _ _ [] = []
- expand p ps (FunClause (Ellipsis _ ps' eqs []) rhs wh : ds) =
- FunClause (LHS p (ps ++ ps') eqs []) rhs wh : expand p ps ds
- expand p ps (FunClause (Ellipsis _ ps' eqs es) rhs wh : ds) =
- FunClause (LHS p (ps ++ ps') eqs es) rhs wh : expand p (ps ++ ps') ds
+ expand p ps (FunClause (Ellipsis r ps' eqs []) rhs wh : ds) =
+ FunClause (LHS (setRange r p) ((setRange r ps) ++ ps') eqs []) rhs wh : expand p ps ds
+ expand p ps (FunClause (Ellipsis r ps' eqs es) rhs wh : ds) =
+ FunClause (LHS (setRange r p) ((setRange r ps) ++ ps') eqs es) rhs wh : expand p (ps ++ ps') ds
expand p ps (d@(FunClause (LHS _ _ _ []) _ _) : ds) =
d : expand p ps ds
expand _ _ (d@(FunClause (LHS p ps _ (_ : _)) _ _) : ds) =
@@ -807,10 +848,10 @@ niceDeclarations ds = do
isTypeSig d | LoneSig{} <- declKind d = True
isTypeSig _ = False
- sigNames = [ (k, x) | LoneSig k x <- map declKind ds ]
- defNames = [ (k, x) | LoneDef k x <- map declKind ds ]
+ sigNames = [ (x, k) | LoneSig k x <- map declKind ds ]
+ defNames = [ (x, k) | LoneDef k x <- map declKind ds ]
-- compute the set difference with equality just on names
- loneNames = [ (k, x) | (k, x) <- sigNames, List.all ((x /=) . snd) defNames ]
+ loneNames = [ (x, k) | (x, k) <- sigNames, List.all ((x /=) . fst) defNames ]
-- Andreas, 2013-02-28 (issue 804):
-- do not termination check a mutual block if any of its
@@ -818,7 +859,7 @@ niceDeclarations ds = do
termCheck (FunSig _ _ _ _ _ tc _ _) = tc
termCheck (FunDef _ _ _ _ tc _ _) = tc
termCheck (NiceMutual _ tc _) = tc
- termCheck (NiceUnquoteDecl _ _ _ _ tc _ _) = tc
+ termCheck (NiceUnquoteDecl _ _ _ _ _ tc _ _) = tc
termCheck _ = TerminationCheck
-- A mutual block cannot have a measure,
@@ -844,7 +885,7 @@ niceDeclarations ds = do
-- no effect on fields or primitives, the InAbstract field there is unused
NiceField r f p _ x e -> return $ NiceField r f p AbstractDef x e
PrimitiveFunction r f p _ x e -> return $ PrimitiveFunction r f p AbstractDef x e
- NiceUnquoteDecl r f p _ t x e -> return $ NiceUnquoteDecl r f p AbstractDef t x e
+ NiceUnquoteDecl r f p i _ t x e -> return $ NiceUnquoteDecl r f p i AbstractDef t x e
NiceModule{} -> return $ d
NiceModuleMacro{} -> return $ d
Axiom{} -> return $ d
@@ -895,7 +936,7 @@ niceDeclarations ds = do
NiceRecSig r f p x ls t -> (\ p -> NiceRecSig r f p x ls t) <$> setPrivate p
NiceDataSig r f p x ls t -> (\ p -> NiceDataSig r f p x ls t) <$> setPrivate p
NiceFunClause r p a termCheck d -> (\ p -> NiceFunClause r p a termCheck d) <$> setPrivate p
- NiceUnquoteDecl r f p a t x e -> (\ p -> NiceUnquoteDecl r f p a t x e) <$> setPrivate p
+ NiceUnquoteDecl r f p i a t x e -> (\ p -> NiceUnquoteDecl r f p i a t x e) <$> setPrivate p
NicePragma _ _ -> return $ d
NiceOpen _ _ _ -> return $ d
NiceImport _ _ _ _ _ -> return $ d
@@ -933,12 +974,12 @@ niceDeclarations ds = do
case d of
Axiom r f p i rel x e -> (\ i -> Axiom r f p i rel x e) <$> setInstance i
FunSig r f p i rel tc x e -> (\ i -> FunSig r f p i rel tc x e) <$> setInstance i
+ NiceUnquoteDecl r f p i a tc x e -> (\ i -> NiceUnquoteDecl r f p i a tc x e) <$> setInstance i
NiceMutual{} -> return $ d
NiceFunClause{} -> return $ d
FunDef{} -> return $ d
NiceField{} -> return $ d
PrimitiveFunction{} -> return $ d
- NiceUnquoteDecl{} -> return $ d
NiceRecSig{} -> return $ d
NiceDataSig{} -> return $ d
NiceModuleMacro{} -> return $ d
@@ -1055,5 +1096,4 @@ notSoNiceDeclaration d =
RecDef r _ _ x i c bs ds -> Record r x i (unThing <$> c) bs Nothing $ map notSoNiceDeclaration ds
where unThing (ThingWithFixity c _) = c
NicePatternSyn r _ n as p -> PatternSyn r n as p
- NiceUnquoteDecl r _ _ _ _ x e -> UnquoteDecl r x e
-
+ NiceUnquoteDecl r _ _ _ _ _ x e -> UnquoteDecl r x e
diff --git a/src/full/Agda/Syntax/Concrete/Generic.hs b/src/full/Agda/Syntax/Concrete/Generic.hs
index f499b2b..5e0fe80 100644
--- a/src/full/Agda/Syntax/Concrete/Generic.hs
+++ b/src/full/Agda/Syntax/Concrete/Generic.hs
@@ -1,9 +1,8 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
-- | Generic traversal and reduce for concrete syntax,
--- in the style of 'Agda.Syntax.Internal.Generic'.
+-- in the style of "Agda.Syntax.Internal.Generic".
--
-- However, here we use the terminology of 'Data.Traversable'.
@@ -100,7 +99,7 @@ instance ExprLike Expr where
Underscore{} -> f $ e0
RawApp r es -> f $ RawApp r $ mapE es
App r e es -> f $ App r (mapE e) $ mapE es
- OpApp r q es -> f $ OpApp r q $ mapE es
+ OpApp r q ns es -> f $ OpApp r q ns $ mapE es
WithApp r e es -> f $ WithApp r (mapE e) $ mapE es
HiddenArg r e -> f $ HiddenArg r $ mapE e
InstanceArg r e -> f $ InstanceArg r $ mapE e
diff --git a/src/full/Agda/Syntax/Concrete/Name.hs b/src/full/Agda/Syntax/Concrete/Name.hs
index 437b592..9ca524d 100644
--- a/src/full/Agda/Syntax/Concrete/Name.hs
+++ b/src/full/Agda/Syntax/Concrete/Name.hs
@@ -1,8 +1,7 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternGuards #-}
{-| Names in the concrete syntax are just strings (or lists of strings for
qualified names).
@@ -42,7 +41,7 @@ data Name
| NoName !Range NameId -- ^ @_@.
deriving (Typeable)
-instance NFData Name
+instance NFData Name where rnf x = seq x ()
instance Underscore Name where
underscore = NoName noRange __IMPOSSIBLE__
@@ -249,32 +248,32 @@ instance IsNoName QName where
-- instead. Later, simply derive Show for these types:
instance Show Name where
- show (Name _ xs) = concatMap show xs
- show (NoName _ _) = "_"
+ show (Name _ xs) = concatMap show xs
+ show (NoName _ _) = "_"
instance Show NamePart where
- show Hole = "_"
- show (Id s) = rawNameToString s
+ show Hole = "_"
+ show (Id s) = rawNameToString s
instance Show QName where
- show (Qual m x) = show m ++ "." ++ show x
- show (QName x) = show x
+ show (Qual m x) = show m ++ "." ++ show x
+ show (QName x) = show x
------------------------------------------------------------------------
-- * Printing names
------------------------------------------------------------------------
instance Pretty Name where
- pretty (Name _ xs) = hcat $ map pretty xs
- pretty (NoName _ _) = text $ "_"
+ pretty (Name _ xs) = hcat $ map pretty xs
+ pretty (NoName _ _) = text $ "_"
instance Pretty NamePart where
- pretty Hole = text $ "_"
- pretty (Id s) = text $ rawNameToString s
+ pretty Hole = text $ "_"
+ pretty (Id s) = text $ rawNameToString s
instance Pretty QName where
- pretty (Qual m x) = pretty m <> pretty "." <> pretty x
- pretty (QName x) = pretty x
+ pretty (Qual m x) = pretty m <> pretty "." <> pretty x
+ pretty (QName x) = pretty x
instance Pretty TopLevelModuleName where
pretty (TopLevelModuleName ms) = text $ intercalate "." ms
diff --git a/src/full/Agda/Syntax/Concrete/Operators.hs b/src/full/Agda/Syntax/Concrete/Operators.hs
index 2fa1546..d37ad98 100644
--- a/src/full/Agda/Syntax/Concrete/Operators.hs
+++ b/src/full/Agda/Syntax/Concrete/Operators.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-| The parser doesn't know about operators and parses everything as normal
@@ -45,57 +45,54 @@ import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.TypeChecking.Monad.Base (typeError, TypeError(..), LHSOrPatSyn(..))
-import Agda.TypeChecking.Monad.Benchmark (billSub)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Monad.State (getScope)
import Agda.TypeChecking.Monad.Options
import Agda.Utils.Either
import Agda.Utils.ReadP
+#if MIN_VERSION_base(4,8,0)
+import Agda.Utils.List hiding ( uncons )
+#else
import Agda.Utils.List
+#endif
#include "undefined.h"
import Agda.Utils.Impossible
---------------------------------------------------------------------------
--- * Building the parser
+-- * Billing
---------------------------------------------------------------------------
-partsInScope :: FlatScope -> ScopeM (Set QName)
-partsInScope flat = do
- (names, ops) <- localNames flat
- let xs = concatMap parts names ++ concatMap notationNames ops
- return $ Set.fromList xs
- where
- qual xs x = foldr Qual (QName x) xs
- parts q = parts' (init $ qnameParts q) (unqualify q)
- parts' ms (NoName _ _) = []
- parts' ms x@(Name _ [_]) = [qual ms x]
- -- The first part should be qualified, but not the rest
- parts' ms x@(Name _ xs) = qual ms x : qual ms (Name noRange [first]) : [ QName $ Name noRange [i] | i <- iparts ]
- where
- first:iparts = [ i | i@(Id {}) <- xs ]
+-- | Bills the operator parser.
+
+billToParser :: ScopeM a -> ScopeM a
+billToParser = Bench.billTo [Bench.Parsing, Bench.Operators]
+
+---------------------------------------------------------------------------
+-- * Building the parser
+---------------------------------------------------------------------------
type FlatScope = Map QName [AbstractName]
--- | Compute all unqualified defined names in scope and their fixities.
--- Note that overloaded names (constructors) can have several fixities.
--- Then we 'chooseFixity'. (See issue 1194.)
-getDefinedNames :: [KindOfName] -> FlatScope -> [(QName, Fixity')]
+-- | Compute all defined names in scope and their fixities/notations.
+-- Note that overloaded names (constructors) can have several
+-- fixities/notations. Then we 'mergeNotations'. (See issue 1194.)
+getDefinedNames :: [KindOfName] -> FlatScope -> [[NewNotation]]
getDefinedNames kinds names =
- [ (x, chooseFixity fixs)
+ [ mergeNotations $
+ map (\d -> namesToNotation x (A.qnameName $ anameName d)) ds
| (x, ds) <- Map.toList names
, any ((`elem` kinds) . anameKind) ds
- , let fixs = map (A.nameFixity . A.qnameName . anameName) ds
- , not (null fixs)
+ , not (null ds)
-- Andreas, 2013-03-21 see Issue 822
-- Names can have different kinds, i.e., 'defined' and 'constructor'.
-- We need to consider all names that have *any* matching kind,
-- not only those whose first appearing kind is matching.
- ]
+ ]
--- | Compute all names (first component) and operators (second component) in
--- scope.
+-- | Compute all names (first component) and operators/notations
+-- (second component) in scope.
localNames :: FlatScope -> ScopeM ([QName], [NewNotation])
localNames flat = do
let defs = getDefinedNames allKindsOfNames flat
@@ -106,17 +103,16 @@ localNames flat = do
, "defs = " ++ show defs
, "locals= " ++ show locals
]
- return $ split $ uniqOn fst $ map localOp locals ++ defs
+ let localNots = map localOp locals
+ localNames = Set.fromList $ map notaName localNots
+ otherNots = filter (\n -> not (Set.member (notaName n) localNames))
+ (concat defs)
+ return $ split $ localNots ++ otherNots
where
- localOp (x, y) = (QName x, A.nameFixity y)
- split ops = partitionEithers $ concatMap opOrNot ops
-
- opOrNot (q, Fixity' fx syn) = Left q : map Right (notaFromName ++ nota)
- where
- notaFromName = case unqualify q of
- Name _ [_] -> []
- x -> [NewNotation q fx $ syntaxOf x]
- nota = if null syn then [] else [NewNotation q fx syn]
+ localOp (x, y) = namesToNotation (QName x) y
+ split ops = partitionEithers $ concatMap opOrNot ops
+ opOrNot n = Left (notaName n) :
+ if null (notation n) then [] else [Right n]
-- | Data structure filled in by @buildParsers@.
-- The top-level parser @pTop@ is of primary interest,
@@ -167,10 +163,10 @@ buildParsers r flat use = do
[ "names = " ++ show names
, "ops = " ++ show ops
, "cons = " ++ show cons ]
- let conparts = Set.fromList $ concatMap notationNames $ map oldToNewNotation cons
- opsparts = Set.fromList $ concatMap notationNames $ ops
+ let conparts = Set.fromList $ concatMap notationNames $ concat cons
+ opsparts = Set.fromList $ concatMap notationNames ops
allParts = Set.union conparts opsparts
- connames = Set.fromList $ map fst cons
+ connames = Set.fromList $ map (notaName . head) cons
(non, fix) = partition nonfix ops
set = Set.fromList names
isAtom x = case use of
@@ -192,23 +188,16 @@ buildParsers r flat use = do
level :: NewNotation -> Integer
level = fixityLevel . notaFixity
- isinfixl, isinfixr, isinfix, nonfix, isprefix, ispostfix :: NewNotation -> Bool
-
- isinfixl (NewNotation _ (LeftAssoc _ _) syn) = isInfix syn
- isinfixl _ = False
-
- isinfixr (NewNotation _ (RightAssoc _ _) syn) = isInfix syn
- isinfixr _ = False
+ nonfix, isprefix, ispostfix :: NewNotation -> Bool
+ nonfix = (== NonfixNotation) . notationKind . notation
+ isprefix = (== PrefixNotation) . notationKind . notation
+ ispostfix = (== PostfixNotation) . notationKind . notation
- isinfix (NewNotation _ (NonAssoc _ _) syn) = isInfix syn
- isinfix _ = False
-
- nonfix (NewNotation _ _ syn) = notationKind syn == NonfixNotation
- isprefix (NewNotation _ _ syn) = notationKind syn == PrefixNotation
- ispostfix (NewNotation _ _ syn) = notationKind syn == PostfixNotation
-
- isInfix :: Notation -> Bool
- isInfix syn = notationKind syn == InfixNotation
+ isinfix :: Associativity -> NewNotation -> Bool
+ isinfix ass syn =
+ notationKind (notation syn) == InfixNotation
+ &&
+ fixityAssoc (notaFixity syn) == ass
-- | Group operators by precedence level
order :: [NewNotation] -> [[NewNotation]]
@@ -221,9 +210,9 @@ buildParsers r flat use = do
[] -> [id]
fs -> fs
where
- inlfx = fixP infixlP isinfixl
- inrfx = fixP infixrP isinfixr
- infx = fixP infixP isinfix
+ inlfx = fixP infixlP (isinfix LeftAssoc)
+ inrfx = fixP infixrP (isinfix RightAssoc)
+ infx = fixP infixP (isinfix NonAssoc)
prefx = fixP prefixP isprefix
postfx = fixP postfixP ispostfix
@@ -242,7 +231,7 @@ instance IsExpr Expr where
exprView e = case e of
Ident x -> LocalV x
App _ e1 e2 -> AppV e1 e2
- OpApp r d es -> OpAppV d es
+ OpApp r d ns es -> OpAppV d ns es
HiddenArg _ e -> HiddenArgV e
InstanceArg _ e -> InstanceArgV e
Paren _ e -> ParenV e
@@ -250,33 +239,33 @@ instance IsExpr Expr where
Underscore{} -> WildV e
_ -> OtherV e
unExprView e = case e of
- LocalV x -> Ident x
- AppV e1 e2 -> App (fuseRange e1 e2) e1 e2
- OpAppV d es -> OpApp (fuseRange d es) d es
- HiddenArgV e -> HiddenArg (getRange e) e
+ LocalV x -> Ident x
+ AppV e1 e2 -> App (fuseRange e1 e2) e1 e2
+ OpAppV d ns es -> OpApp (fuseRange d es) d ns es
+ HiddenArgV e -> HiddenArg (getRange e) e
InstanceArgV e -> InstanceArg (getRange e) e
- ParenV e -> Paren (getRange e) e
- LamV bs e -> Lam (fuseRange bs e) bs e
- WildV e -> e
- OtherV e -> e
+ ParenV e -> Paren (getRange e) e
+ LamV bs e -> Lam (fuseRange bs e) bs e
+ WildV e -> e
+ OtherV e -> e
instance IsExpr Pattern where
exprView e = case e of
- IdentP x -> LocalV x
- AppP e1 e2 -> AppV e1 e2
- OpAppP r d es -> OpAppV d ((map . fmap . fmap) Ordinary es)
- HiddenP _ e -> HiddenArgV e
- InstanceP _ e -> InstanceArgV e
- ParenP _ e -> ParenV e
- WildP{} -> WildV e
- _ -> OtherV e
+ IdentP x -> LocalV x
+ AppP e1 e2 -> AppV e1 e2
+ OpAppP r d ns es -> OpAppV d ns ((map . fmap . fmap) Ordinary es)
+ HiddenP _ e -> HiddenArgV e
+ InstanceP _ e -> InstanceArgV e
+ ParenP _ e -> ParenV e
+ WildP{} -> WildV e
+ _ -> OtherV e
unExprView e = case e of
LocalV x -> IdentP x
AppV e1 e2 -> AppP e1 e2
- OpAppV d es -> let ess :: [NamedArg Pattern]
+ OpAppV d ns es -> let ess :: [NamedArg Pattern]
ess = (map . fmap . fmap) (fromOrdinary __IMPOSSIBLE__) es
- in OpAppP (fuseRange d es) d ess
+ in OpAppP (fuseRange d es) d ns ess
HiddenArgV e -> HiddenP (getRange e) e
InstanceArgV e -> InstanceP (getRange e) e
ParenV e -> ParenP (getRange e) e
@@ -284,46 +273,21 @@ instance IsExpr Pattern where
WildV e -> e
OtherV e -> e
-{- TRASH
-instance IsExpr LHSCore where
- exprView e = case e of
- LHSHead f ps -> foldl AppV (LocalV f) $ map exprView ps
- LHSProj d ps1 e ps2 -> foldl AppV (LocalV d) $
- map exprView ps1 ++ exprView e : map exprView ps2
- unExprView e = LHSHead f ps
- where p :: Pattern
- p = unExprView
- (f, ps) = lhsArgs p
--}
-
---------------------------------------------------------------------------
-- * Helpers for pattern and lhs parsing
---------------------------------------------------------------------------
--- Andreas, 2011-11-24 moved here from ConcreteToAbstract
-lhsArgs :: Pattern -> (Name, [NamedArg Pattern])
-lhsArgs p = case lhsArgs' p of
- Just (x, args) -> (x, args)
- Nothing -> __IMPOSSIBLE__
-
--- | @lhsArgs' p@ splits a lhs @f ps@, given as a pattern @p@,
--- into @(f, ps)@.
-lhsArgs' :: Pattern -> Maybe (Name, [NamedArg Pattern])
-lhsArgs' p = case patternAppView p of
- Common.Arg _ (Named _ (IdentP (QName x))) : ps -> Just (x, ps)
- _ -> Nothing
-
-- | View a pattern @p@ as a list @p0 .. pn@ where @p0@ is the identifier
-- (in most cases a constructor).
--
-- Pattern needs to be parsed already (operators resolved).
patternAppView :: Pattern -> [NamedArg Pattern]
patternAppView p = case p of
- AppP p arg -> patternAppView p ++ [arg]
- OpAppP _ x ps -> defaultNamedArg (IdentP x) : ps
- ParenP _ p -> patternAppView p
- RawAppP _ _ -> __IMPOSSIBLE__
- _ -> [ defaultNamedArg p ]
+ AppP p arg -> patternAppView p ++ [arg]
+ OpAppP _ x _ ps -> defaultNamedArg (IdentP x) : ps
+ ParenP _ p -> patternAppView p
+ RawAppP _ _ -> __IMPOSSIBLE__
+ _ -> [ defaultNamedArg p ]
---------------------------------------------------------------------------
@@ -336,7 +300,7 @@ parsePat prs p = case p of
AppP p (Common.Arg info q) ->
fullParen' <$> (AppP <$> parsePat prs p <*> (Common.Arg info <$> traverse (parsePat prs) q))
RawAppP _ ps -> fullParen' <$> (parsePat prs =<< parse prs ps)
- OpAppP r d ps -> fullParen' . OpAppP r d <$> (mapM . traverse . traverse) (parsePat prs) ps
+ OpAppP r d ns ps -> fullParen' . OpAppP r d ns <$> (mapM . traverse . traverse) (parsePat prs) ps
HiddenP _ _ -> fail "bad hidden argument"
InstanceP _ _ -> fail "bad instance argument"
AsP r x p -> AsP r x <$> parsePat prs p
@@ -402,7 +366,8 @@ parseLHS' lhsOrPatSyn top p = do
rs -> typeError $ AmbiguousParseForLHS lhsOrPatSyn p $
map (fullParen . fst) rs
where
- getNames kinds flat = map fst $ getDefinedNames kinds flat
+ getNames kinds flat =
+ map (notaName . head) $ getDefinedNames kinds flat
-- validPattern returns an empty or singleton list (morally a Maybe)
validPattern :: PatternCheckConfig -> Pattern -> [(Pattern, ParseLHS)]
@@ -461,7 +426,7 @@ classifyPattern conf p =
-- intended _* applied to true, or as true applied to a variable *. If we
-- check arities this problem won't appear.
parseLHS :: Name -> Pattern -> ScopeM LHSCore
-parseLHS top p = do
+parseLHS top p = billToParser $ do
res <- parseLHS' IsLHS (Just top) p
case res of
Right (f, lhs) -> return lhs
@@ -480,7 +445,7 @@ parsePatternSyn :: Pattern -> ScopeM Pattern
parsePatternSyn = parsePatternOrSyn IsPatSyn
parsePatternOrSyn :: LHSOrPatSyn -> Pattern -> ScopeM Pattern
-parsePatternOrSyn lhsOrPatSyn p = do
+parsePatternOrSyn lhsOrPatSyn p = billToParser $ do
res <- parseLHS' lhsOrPatSyn Nothing p
case res of
Left p -> return p
@@ -502,7 +467,7 @@ validConPattern cons p = case appView p of
appView :: Pattern -> [Pattern]
appView p = case p of
AppP p a -> appView p ++ [namedArg a]
- OpAppP _ op ps -> IdentP op : map namedArg ps
+ OpAppP _ op _ ps -> IdentP op : map namedArg ps
ParenP _ p -> appView p
RawAppP _ _ -> __IMPOSSIBLE__
HiddenP _ _ -> __IMPOSSIBLE__
@@ -517,7 +482,7 @@ patternQNames p = case p of
ParenP _ p -> patternQNames p
HiddenP _ p -> patternQNames (namedThing p)
InstanceP _ p -> patternQNames (namedThing p)
- OpAppP r d ps -> __IMPOSSIBLE__
+ OpAppP r d _ ps -> __IMPOSSIBLE__
AppP{} -> __IMPOSSIBLE__
AsP r x p -> patternQNames p
AbsurdP{} -> []
@@ -536,25 +501,16 @@ qualifierModules qs =
-- | Parse a list of expressions into an application.
parseApplication :: [Expr] -> ScopeM Expr
parseApplication [e] = return e
-parseApplication es = do
+parseApplication es = billToParser $ do
-- Build the parser
let ms = qualifierModules [ q | Ident q <- es ]
flat <- flattenScope ms <$> getScope
- -- Andreas, 2014-04-27 Time for building the parser is negligible
- p <- -- billSub [Bench.Parsing, Bench.Operators, Bench.BuildParser] $
- buildParsers (getRange es) flat UseBoundNames
+ p <- buildParsers (getRange es) flat UseBoundNames
-- Parse
case force $ parse (pTop p) es of
[e] -> return e
- [] -> do
- -- When the parser fails and a name is not in scope, it is more
- -- useful to say that to the user rather than just "failed".
- inScope <- partsInScope flat
- case [ x | Ident x <- es, not (Set.member x inScope) ] of
- [] -> typeError $ NoParseForApplication es
- xs -> typeError $ NotInScope xs
-
+ [] -> typeError $ NoParseForApplication es
es' -> typeError $ AmbiguousParseForApplication es $ map fullParen es'
parseModuleIdentifier :: Expr -> ScopeM QName
@@ -562,7 +518,7 @@ parseModuleIdentifier (Ident m) = return m
parseModuleIdentifier e = typeError $ NotAModuleExpr e
parseRawModuleApplication :: [Expr] -> ScopeM (QName, [NamedArg Expr])
-parseRawModuleApplication es = do
+parseRawModuleApplication es = billToParser $ do
let e : es_args = es
m <- parseModuleIdentifier e
@@ -574,12 +530,7 @@ parseRawModuleApplication es = do
-- Parse
case {-force $-} parse (pArgs p) es_args of -- TODO: not sure about forcing
[as] -> return (m, as)
- [] -> do
- inScope <- partsInScope flat
- case [ x | Ident x <- es_args, not (Set.member x inScope) ] of
- [] -> typeError $ NoParseForApplication es
- xs -> typeError $ NotInScope xs
-
+ [] -> typeError $ NoParseForApplication es
ass -> do
let f = fullParen . foldl (App noRange) (Ident m)
typeError $ AmbiguousParseForApplication es
@@ -619,7 +570,7 @@ fullParen' e = case exprView e of
Hidden -> e2
Instance -> e2
NotHidden -> fullParen' <$> e2
- OpAppV x es -> par $ unExprView $ OpAppV x $ (map . fmap . fmap . fmap) fullParen' es
+ OpAppV x ns es -> par $ unExprView $ OpAppV x ns $ (map . fmap . fmap . fmap) fullParen' es
LamV bs e -> par $ unExprView $ LamV bs (fullParen e)
where
par = unExprView . ParenV
diff --git a/src/full/Agda/Syntax/Concrete/Operators/Parser.hs b/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
index b8e5a55..28ce619 100644
--- a/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
+++ b/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Agda.Syntax.Concrete.Operators.Parser where
@@ -6,15 +6,20 @@ module Agda.Syntax.Concrete.Operators.Parser where
import Control.Exception (throw)
import Data.Maybe
+import Data.Set (Set)
import Agda.Syntax.Position
+import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg)
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Concrete
+
import Agda.TypeChecking.Monad.Base (TCErr(Exception))
-import Agda.Utils.ReadP
+
import Agda.Utils.Monad
+import Agda.Utils.Pretty
+import Agda.Utils.ReadP
#include "undefined.h"
import Agda.Utils.Impossible
@@ -24,7 +29,9 @@ data ExprView e
| WildV e
| OtherV e
| AppV e (NamedArg e)
- | OpAppV QName [NamedArg (OpApp e)]
+ | OpAppV QName (Set A.Name) [NamedArg (OpApp e)]
+ -- ^ The 'QName' is possibly ambiguous, but it must correspond
+ -- to one of the names in the set.
| HiddenArgV (Named_ e)
| InstanceArgV (Named_ e)
| LamV [LamBinding] e
@@ -79,8 +86,9 @@ postop middleP = do
-- Note: it would be better to take the decision of "postprocessing" at the same
-- place as where the holes are discarded, however that would require a dependently
-- typed function (or duplicated code)
-opP :: IsExpr e => ReadP e e -> NewNotation -> ReadP e (NewNotation,Range,[e])
-opP p nsyn@(NewNotation q _ syn) = do
+opP :: IsExpr e =>
+ ReadP e e -> NewNotation -> ReadP e (NewNotation,Range,[e])
+opP p nsyn@(NewNotation q _ _ syn) = do
(range,es) <- worker (init $ qnameParts q) $ removeExternalHoles syn
return (nsyn,range,es)
where worker ms [IdPart x] = do r <- partP ms x; return (r,[])
@@ -97,7 +105,8 @@ opP p nsyn@(NewNotation q _ syn) = do
-- | Given a name with a syntax spec, and a list of parsed expressions
-- fitting it, rebuild the expression.
rebuild :: forall e. IsExpr e => NewNotation -> Range -> [e] -> e
-rebuild (NewNotation name _ syn) r es = unExprView $ OpAppV (setRange r name) exprs
+rebuild (NewNotation name names _ syn) r es =
+ unExprView $ OpAppV (setRange r name) names exprs
where
exprs = map findExprFor [0..lastHole]
filledHoles = zip es (filter isAHole syn)
@@ -118,7 +127,8 @@ rebuildBinding :: IsExpr e => ExprView e -> LamBinding
rebuildBinding (LocalV (QName name)) = DomainFree defaultArgInfo $ mkBoundName_ name
rebuildBinding (WildV e) =
DomainFree defaultArgInfo $ mkBoundName_ $ Name noRange [Hole]
-rebuildBinding e = throw $ Exception (getRange e) "Expected variable name in binding position"
+rebuildBinding e = throw $ Exception (getRange e) $
+ text "Expected variable name in binding position"
-- | Parse using the appropriate fixity, given a parser parsing the
-- operator part, the name of the operator, and a parser of
diff --git a/src/full/Agda/Syntax/Concrete/Pretty.hs b/src/full/Agda/Syntax/Concrete/Pretty.hs
index c2fe806..aa86a7b 100644
--- a/src/full/Agda/Syntax/Concrete/Pretty.hs
+++ b/src/full/Agda/Syntax/Concrete/Pretty.hs
@@ -1,13 +1,14 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-
{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+
{-| Pretty printer for the concrete syntax.
-}
module Agda.Syntax.Concrete.Pretty where
+import Prelude hiding (null)
+
import Data.Char
import Data.Functor
import Data.Maybe
@@ -20,6 +21,8 @@ import Agda.Syntax.Literal
import Agda.Syntax.Notation
import Agda.Syntax.Position
+import Agda.Utils.Functor
+import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.String
@@ -64,28 +67,19 @@ arrow, lambda :: Doc
arrow = text "\x2192"
lambda = text "\x03bb"
-pHidden :: Pretty a => ArgInfo -> a -> Doc
-pHidden i = bracks h . pretty
- where bracks Hidden = braces'
- bracks Instance = dbraces
- bracks NotHidden= id
- h = argInfoHiding i
-
-pRelevance :: Pretty a => ArgInfo -> a -> Doc
-pRelevance i a =
- let d = pretty a
- in if render d == "_" then d else pretty (argInfoRelevance i) <> d
-{-
-pRelevance Forced a = pretty a
-pRelevance UnusedArg a = pretty a
-pRelevance Relevant a = pretty a
-pRelevance Irrelevant a =
- let d = pretty a
- in if render d == "_" then d else text "." <> d
-pRelevance NonStrict a =
- let d = pretty a
- in if render d == "_" then d else text ".." <> d
--}
+-- | @prettyHiding info visible doc@ puts the correct braces
+-- around @doc@ according to info @info@ and returns
+-- @visible doc@ if the we deal with a visible thing.
+prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
+prettyHiding a parens =
+ case getHiding a of
+ Hidden -> braces'
+ Instance -> dbraces
+ NotHidden -> parens
+
+prettyRelevance :: LensRelevance a => a -> Doc -> Doc
+prettyRelevance a d =
+ if render d == "_" then d else pretty (getRelevance a) <> d
instance (Pretty a, Pretty b) => Pretty (a, b) where
pretty (a, b) = parens $ pretty a <> comma <+> pretty b
@@ -93,8 +87,11 @@ instance (Pretty a, Pretty b) => Pretty (a, b) where
instance Pretty (ThingWithFixity Name) where
pretty (ThingWithFixity n _) = pretty n
+instance Pretty a => Pretty (WithHiding a) where
+ pretty w = prettyHiding w id $ pretty $ dget w
+
instance Pretty Relevance where
- pretty Forced = empty
+ pretty Forced{} = empty
pretty UnusedArg = empty
pretty Relevant = empty
pretty Irrelevant = text "."
@@ -123,8 +120,8 @@ instance Pretty Expr where
-- sep [ pretty e1
-- , nest 2 $ fsep $ map pretty args
-- ]
- RawApp _ es -> fsep $ map pretty es
- OpApp _ q es -> fsep $ prettyOpApp q es
+ RawApp _ es -> fsep $ map pretty es
+ OpApp _ q _ es -> fsep $ prettyOpApp q es
WithApp _ e es -> fsep $
pretty e : map ((text "|" <+>) . pretty) es
@@ -193,21 +190,18 @@ instance Pretty BoundName where
instance Pretty LamBinding where
-- TODO guilhem: colors are unused (colored syntax disallowed)
- pretty (DomainFree i x) = pRelevance i $ pHidden i $ pretty x
+ pretty (DomainFree i x) = prettyRelevance i $ prettyHiding i id $ pretty x
pretty (DomainFull b) = pretty b
instance Pretty TypedBindings where
- pretty (TypedBindings _ a) =
- pRelevance (argInfo a) $ bracks $ pretty $ WithColors (argColors a) $ unArg a
+ pretty (TypedBindings _ a) = prettyRelevance a $ prettyHiding a p $
+ pretty $ WithColors (argColors a) $ unArg a
where
- bracks = case getHiding a of
- Hidden -> braces'
- Instance -> dbraces
- NotHidden | isMeta (unArg a) -> id
- | otherwise -> parens
+ p | isUnderscore (unArg a) = id
+ | otherwise = parens
- isMeta (TBind _ _ (Underscore _ Nothing)) = True
- isMeta _ = False
+ isUnderscore (TBind _ _ (Underscore _ Nothing)) = True
+ isUnderscore _ = False
newtype Tel = Tel Telescope
@@ -247,7 +241,7 @@ instance Pretty TypedBinding where
smashTel :: Telescope -> Telescope
smashTel (TypedBindings r (Common.Arg i (TBind r' xs e)) :
TypedBindings _ (Common.Arg i' (TBind _ ys e')) : tel)
- | show i == show i' && show e == show e' && all isUnnamed (xs ++ ys) =
+ | show i == show i' && show e == show e' && all (isUnnamed . dget) (xs ++ ys) =
smashTel (TypedBindings r (Common.Arg i (TBind r' (xs ++ ys) e)) : tel)
where
isUnnamed x = boundLabel x == boundName x
@@ -305,13 +299,13 @@ instance Pretty Declaration where
pretty d =
case d of
TypeSig i x e ->
- sep [ pRelevance i $ pretty x <+> pColors ":" (argInfoColors i)
+ sep [ prettyRelevance i $ pretty x <+> pColors ":" (argInfoColors i)
, nest 2 $ pretty e
]
Field x (Common.Arg i e) ->
sep [ text "field"
- , nest 2 $ pRelevance i $ pHidden i $
- TypeSig (i {argInfoRelevance = Relevant}) x e
+ , nest 2 $ prettyRelevance i $ prettyHiding i id $
+ pretty $ TypeSig (i {argInfoRelevance = Relevant}) x e
]
FunClause lhs rhs wh ->
sep [ pretty lhs
@@ -456,9 +450,12 @@ instance Pretty Pragma where
TerminationMeasure _ x -> hsep $ [text "MEASURE", pretty x]
instance Pretty Fixity where
- pretty (LeftAssoc _ n) = text "infixl" <+> text (show n)
- pretty (RightAssoc _ n) = text "infixr" <+> text (show n)
- pretty (NonAssoc _ n) = text "infix" <+> text (show n)
+ pretty (Fixity _ n ass) = text s <+> text (show n)
+ where
+ s = case ass of
+ LeftAssoc -> "infixl"
+ RightAssoc -> "infixr"
+ NonAssoc -> "infix"
instance Pretty GenPart where
pretty (IdPart x) = text x
@@ -478,7 +475,7 @@ instance Pretty e => Pretty (Arg e) where
-- Andreas 2010-09-24: and in record fields
pretty a = -- pRelevance r $
-- TODO guilhem: print colors
- pHidden (argInfo a) $ unArg a
+ prettyHiding (argInfo a) id $ pretty $ unArg a
instance Pretty e => Pretty (Named_ e) where
pretty (Named Nothing e) = pretty e
@@ -490,19 +487,19 @@ instance Pretty [Pattern] where
instance Pretty Pattern where
pretty p =
case p of
- 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 ps
- HiddenP _ p -> braces' $ pretty p
- InstanceP _ p -> dbraces $ pretty p
- ParenP _ p -> parens $ pretty p
- WildP _ -> underscore
- AsP _ x p -> pretty x <> text "@" <> pretty p
- DotP _ p -> text "." <> pretty p
- AbsurdP _ -> text "()"
- LitP l -> pretty l
- QuoteP _ -> text "quote"
+ 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 ps
+ HiddenP _ p -> braces' $ pretty p
+ InstanceP _ p -> dbraces $ pretty p
+ ParenP _ p -> parens $ pretty p
+ WildP _ -> underscore
+ AsP _ x p -> pretty x <> text "@" <> pretty p
+ DotP _ p -> text "." <> pretty p
+ AbsurdP _ -> text "()"
+ LitP l -> pretty l
+ QuoteP _ -> text "quote"
prettyOpApp :: Pretty a => QName -> [a] -> [Doc]
prettyOpApp q es = prOp ms xs es
diff --git a/src/full/Agda/Syntax/Fixity.hs b/src/full/Agda/Syntax/Fixity.hs
index ddf7947..55d2c82 100644
--- a/src/full/Agda/Syntax/Fixity.hs
+++ b/src/full/Agda/Syntax/Fixity.hs
@@ -1,24 +1,32 @@
+{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
{-| Definitions for fixity, precedence levels, and declared syntax.
-}
module Agda.Syntax.Fixity where
import Data.Foldable
+import Data.Function
import Data.List as List
+import Data.Set (Set)
+import qualified Data.Set as Set
import Data.Traversable
import Data.Typeable (Typeable)
import Agda.Syntax.Position
import Agda.Syntax.Common
+import {-# SOURCE #-} qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Notation
import Agda.Utils.List
+#include "undefined.h"
+import Agda.Utils.Impossible
+
-- * Notation coupled with 'Fixity'
-- | The notation is handled as the fixity in the renamer.
@@ -36,27 +44,34 @@ data ThingWithFixity x = ThingWithFixity x Fixity'
-- | All the notation information related to a name.
data NewNotation = NewNotation
{ notaName :: QName
- -- ^ The concrete name the syntax or fixity belongs to.
+ , notaNames :: Set A.Name
+ -- ^ The names the syntax and/or fixity belong to.
+ --
+ -- Invariant: The set is non-empty. Every name in the list matches
+ -- 'notaName'.
, notaFixity :: Fixity
- -- ^ Associativity and precedence (fixity) of the name.
+ -- ^ Associativity and precedence (fixity) of the names.
, notation :: Notation
- -- ^ Syntax associated with the name.
+ -- ^ Syntax associated with the names.
} deriving (Typeable, Show)
--- | If an operator has no specific notation, recover it from its name.
-oldToNewNotation :: (QName, Fixity') -> NewNotation
-oldToNewNotation (name, Fixity' f syn) = NewNotation
- { notaName = name
+-- | If an operator has no specific notation, then it is computed from
+-- its name.
+namesToNotation :: QName -> A.Name -> NewNotation
+namesToNotation q n = NewNotation
+ { notaName = q
+ , notaNames = Set.singleton n
, notaFixity = f
- , notation = if null syn then syntaxOf $ unqualify name else syn
+ , notation = if null syn then syntaxOf $ unqualify q else syn
}
+ where Fixity' f syn = A.nameFixity n
-- | Return the 'IdPart's of a notation, the first part qualified,
-- the other parts unqualified.
-- This allows for qualified use of operators, e.g.,
-- @M.for x ∈ xs return e@, or @x ℕ.+ y@.
notationNames :: NewNotation -> [QName]
-notationNames (NewNotation q _ parts) =
+notationNames (NewNotation q _ _ parts) =
zipWith ($) (reQualify : repeat QName) [Name noRange [Id x] | IdPart x <- parts ]
where
-- The qualification of @q@.
@@ -84,44 +99,59 @@ syntaxOf (Name _ xs) = mkSyn 0 xs
defaultFixity' :: Fixity'
defaultFixity' = Fixity' defaultFixity defaultNotation
--- | Removes copies of @defaultFixity'@ from a list of fixities.
--- Never returns an empty list, though, rather a singleton list
--- consisting of @defaultFixity'@.
-interestingFixities :: [Fixity'] -> [Fixity']
-interestingFixities fixs = if null fixs' then [defaultFixity'] else fixs'
- where fixs' = filter (not . (== defaultFixity')) fixs
+-- | Merges all 'NewNotation's that have the same notation.
+--
+-- If all 'NewNotation's with a given notation have the same fixity,
+-- then this fixity is preserved, and otherwise it is replaced by
+-- 'defaultFixity'.
+--
+-- Precondition: No 'A.Name' may occur in more than one list element.
+-- Every 'NewNotation' must have the same 'notaName'.
+--
+-- Postcondition: No 'A.Name' occurs in more than one list element.
+mergeNotations :: [NewNotation] -> [NewNotation]
+mergeNotations = map (merge . fixFixities) . groupOn notation
+ where
+ fixFixities ns
+ | allEqual (map notaFixity ns) = ns
+ | otherwise =
+ map (\n -> n { notaFixity = defaultFixity }) ns
--- | If different interesting fixities are available for the same symbol,
--- we take none of them.
-chooseFixity :: [Fixity'] -> Fixity'
-chooseFixity fixs = if allEqual fixs' then head fixs' else defaultFixity'
- where fixs' = interestingFixities fixs
+ merge :: [NewNotation] -> NewNotation
+ merge [] = __IMPOSSIBLE__
+ merge ns@(n : _) = n { notaNames = Set.unions $ map notaNames ns }
-- * Fixity
+-- | Associativity.
+
+data Associativity = NonAssoc | LeftAssoc | RightAssoc
+ deriving (Eq, Ord, Show, Typeable)
+
-- | Fixity of operators.
-data Fixity
- = LeftAssoc { fixityRange :: Range, fixityLevel :: Integer }
- | RightAssoc { fixityRange :: Range, fixityLevel :: Integer }
- | NonAssoc { fixityRange :: Range, fixityLevel :: Integer }
+data Fixity =
+ Fixity { fixityRange :: Range
+ , fixityLevel :: Integer
+ , fixityAssoc :: Associativity
+ }
deriving (Typeable, Show)
instance Eq Fixity where
- LeftAssoc _ n == LeftAssoc _ m = n == m
- RightAssoc _ n == RightAssoc _ m = n == m
- NonAssoc _ n == NonAssoc _ m = n == m
- _ == _ = False
+ f1 == f2 = compare f1 f2 == EQ
+
+instance Ord Fixity where
+ compare = compare `on` (\f -> (fixityLevel f, fixityAssoc f))
-- For @instance Pretty Fixity@, see Agda.Syntax.Concrete.Pretty
-- | The default fixity. Currently defined to be @'NonAssoc' 20@.
defaultFixity :: Fixity
-defaultFixity = NonAssoc noRange 20
+defaultFixity = Fixity noRange 20 NonAssoc
-- | Hack used for @syntax@ facility.
noFixity :: Fixity
-noFixity = NonAssoc noRange (negate 666)
+noFixity = Fixity noRange (negate 666) NonAssoc
-- Ts,ts,ts, why the number of the beast? Revelation 13, 18
--
-- It's not the number of the beast, it's the negation of the
@@ -150,10 +180,10 @@ hiddenArgumentCtx Instance = TopCtx
-- | Do we need to bracket an operator application of the given fixity
-- in a context with the given precedence.
opBrackets :: Fixity -> Precedence -> Bool
-opBrackets (LeftAssoc _ n1)
- (LeftOperandCtx (LeftAssoc _ n2)) | n1 >= n2 = False
-opBrackets (RightAssoc _ n1)
- (RightOperandCtx (RightAssoc _ n2)) | n1 >= n2 = False
+opBrackets (Fixity _ n1 LeftAssoc)
+ (LeftOperandCtx (Fixity _ n2 LeftAssoc)) | n1 >= n2 = False
+opBrackets (Fixity _ n1 RightAssoc)
+ (RightOperandCtx (Fixity _ n2 RightAssoc)) | n1 >= n2 = False
opBrackets f1
(LeftOperandCtx f2) | fixityLevel f1 > fixityLevel f2 = False
opBrackets f1
@@ -204,9 +234,7 @@ instance HasRange Fixity where
getRange = fixityRange
instance KillRange Fixity where
- killRange (LeftAssoc _ n) = LeftAssoc noRange n
- killRange (RightAssoc _ n) = RightAssoc noRange n
- killRange (NonAssoc _ n) = NonAssoc noRange n
+ killRange f = f { fixityRange = noRange }
instance KillRange Fixity' where
- killRange (Fixity' f n) = killRange1 (flip Fixity' n) f
+ killRange (Fixity' f n) = killRange2 Fixity' f n
diff --git a/src/full/Agda/Syntax/Fixity.hs-boot b/src/full/Agda/Syntax/Fixity.hs-boot
new file mode 100644
index 0000000..ae7c31c
--- /dev/null
+++ b/src/full/Agda/Syntax/Fixity.hs-boot
@@ -0,0 +1,3 @@
+module Agda.Syntax.Fixity where
+
+data Fixity'
diff --git a/src/full/Agda/Syntax/Info.hs b/src/full/Agda/Syntax/Info.hs
index 5c91955..98d1109 100644
--- a/src/full/Agda/Syntax/Info.hs
+++ b/src/full/Agda/Syntax/Info.hs
@@ -1,6 +1,6 @@
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-| An info object contains additional information about a piece of abstract
diff --git a/src/full/Agda/Syntax/Internal.hs b/src/full/Agda/Syntax/Internal.hs
index 5fda241..e586727 100644
--- a/src/full/Agda/Syntax/Internal.hs
+++ b/src/full/Agda/Syntax/Internal.hs
@@ -1,13 +1,14 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+-- GHC 7.4.2 requires this layout for the pragmas. See Issue 1460.
+{-# LANGUAGE CPP,
+ DeriveDataTypeable,
+ DeriveFoldable,
+ DeriveFunctor,
+ DeriveTraversable,
+ FlexibleInstances,
+ GeneralizedNewtypeDeriving,
+ MultiParamTypeClasses,
+ StandaloneDeriving,
+ TemplateHaskell #-}
module Agda.Syntax.Internal
( module Agda.Syntax.Internal
@@ -18,15 +19,22 @@ module Agda.Syntax.Internal
import Prelude hiding (foldr, mapM, null)
import Control.Arrow ((***))
-import Control.Applicative
+import Control.Applicative hiding (empty)
import Control.Monad.Identity hiding (mapM)
import Control.Monad.State hiding (mapM)
import Control.Parallel
-import Data.Foldable
+import Data.Foldable ( Foldable, foldMap )
import Data.Function
import qualified Data.List as List
import Data.Maybe
+import Data.Monoid
+
+-- base-4.7 defines the Num instance for Sum
+#if !(MIN_VERSION_base(4,7,0))
+import Data.Orphans ()
+#endif
+
import Data.Traversable
import Data.Typeable (Typeable)
@@ -39,6 +47,7 @@ import Agda.Syntax.Abstract.Name
import Agda.Utils.Empty
import Agda.Utils.Functor
import Agda.Utils.Geniplate
+import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Null
import Agda.Utils.Permutation
@@ -157,9 +166,13 @@ data Abs a = Abs { absName :: ArgName, unAbs :: a }
| NoAbs { absName :: ArgName, unAbs :: a }
deriving (Typeable, Functor, Foldable, Traversable)
+instance Decoration Abs where
+ traverseF f (Abs x a) = Abs x <$> f a
+ traverseF f (NoAbs x a) = NoAbs x <$> f a
+
-- | Types are terms with a sort annotation.
--
-data Type' a = El { getSort :: Sort, unEl :: a }
+data Type' a = El { _getSort :: Sort, unEl :: a }
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Type = Type' Term
@@ -167,6 +180,22 @@ type Type = Type' Term
instance Decoration Type' where
traverseF f (El s a) = El s <$> f a
+class LensSort a where
+ lensSort :: Lens' Sort a
+ getSort :: a -> Sort
+ getSort a = a ^. lensSort
+
+instance LensSort (Type' a) where
+ lensSort f (El s a) = f s <&> \ s' -> El s' a
+
+-- General instance leads to overlapping instances.
+-- instance (Decoration f, LensSort a) => LensSort (f a) where
+instance LensSort a => LensSort (Common.Dom c a) where
+ lensSort = traverseF . lensSort
+
+instance LensSort a => LensSort (Abs a) where
+ lensSort = traverseF . lensSort
+
-- | Sequence of types. An argument of the first type is bound in later types
-- and so on.
data Tele a = EmptyTel
@@ -175,14 +204,10 @@ data Tele a = EmptyTel
type Telescope = Tele (Dom Type)
-instance Null (Tele a) where
- null EmptyTel = True
- null ExtendTel{} = False
- empty = EmptyTel
-
+-- | A traversal for the names in a telescope.
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM f EmptyTel = pure EmptyTel
-mapAbsNamesM f (ExtendTel a (Abs x b)) = ExtendTel a <$> (Abs <$> f x <*> mapAbsNamesM f b)
+mapAbsNamesM f (ExtendTel a ( Abs x b)) = ExtendTel a <$> ( Abs <$> f x <*> mapAbsNamesM f b)
mapAbsNamesM f (ExtendTel a (NoAbs x b)) = ExtendTel a <$> (NoAbs <$> f x <*> mapAbsNamesM f b)
-- Ulf, 2013-11-06: Last case is really impossible but I'd rather find out we
-- violated that invariant somewhere other than here.
@@ -203,13 +228,16 @@ replaceEmptyName x = mapAbsNames $ \ y -> if null y then x else y
-- | Sorts.
--
-data Sort = Type Level
- | Prop -- ignore me
- | Inf
- | DLub Sort (Abs Sort)
- -- ^ if the free variable occurs in the second sort
- -- the whole thing should reduce to Inf, otherwise
- -- it's the normal Lub
+data Sort
+ = Type Level -- ^ @Set ℓ@.
+ | Prop -- ^ Dummy sort.
+ | Inf -- ^ @Setω@.
+ | SizeUniv -- ^ @SizeUniv@, a sort inhabited by type @Size@.
+ | DLub Sort (Abs Sort)
+ -- ^ Dependent least upper bound.
+ -- If the free variable occurs in the second sort,
+ -- the whole thing should reduce to Inf,
+ -- otherwise it's the normal lub.
deriving (Typeable, Show)
-- | A level is a maximum expression of 0..n 'PlusLevel' expressions
@@ -219,14 +247,19 @@ data Sort = Type Level
newtype Level = Max [PlusLevel]
deriving (Show, Typeable)
-data PlusLevel = ClosedLevel Integer
- | Plus Integer LevelAtom
+data PlusLevel
+ = ClosedLevel Integer -- ^ @n@, to represent @Setₙ@.
+ | Plus Integer LevelAtom -- ^ @n + ℓ@.
deriving (Show, Typeable)
+-- | An atomic term of type @Level@.
data LevelAtom
= MetaLevel MetaId Elims
+ -- ^ A meta variable targeting @Level@ under some eliminations.
| BlockedLevel MetaId Term
- | NeutralLevel Term
+ -- ^ A term of type @Level@ whose reduction is blocked by a meta.
+ | NeutralLevel NotBlocked Term
+ -- ^ A neutral term of type @Level@.
| UnreducedLevel Term
-- ^ Introduced by 'instantiate', removed by 'reduce'.
deriving (Show, Typeable)
@@ -236,16 +269,112 @@ data LevelAtom
newtype MetaId = MetaId { metaId :: Nat }
deriving (Eq, Ord, Num, Real, Enum, Integral, Typeable)
+-- | Even if we are not stuck on a meta during reduction
+-- we can fail to reduce a definition by pattern matching
+-- for another reason.
+data NotBlocked
+ = StuckOn Elim
+ -- ^ The 'Elim' is neutral and block a pattern match.
+ | Underapplied
+ -- ^ Not enough arguments were supplied to complete the matching.
+ | AbsurdMatch
+ -- ^ We matched an absurd clause, results in a neutral 'Def'.
+ | MissingClauses
+ -- ^ We ran out of clauses, all considered clauses
+ -- produced an actual mismatch.
+ -- This can happen when try to reduce a function application
+ -- but we are still missing some function clauses.
+ -- See "Agda.TypeChecking.Patterns.Match".
+ | ReallyNotBlocked
+ -- ^ Reduction was not blocked, we reached a whnf
+ -- which can be anything but a stuck @'Def'@.
+ deriving (Show, Typeable)
+
+-- | 'ReallyNotBlocked' is the unit.
+-- 'MissingClauses' is dominant.
+-- @'StuckOn'{}@ should be propagated, if tied, we take the left.
+instance Monoid NotBlocked where
+ -- ReallyNotBlocked is neutral
+ mempty = ReallyNotBlocked
+ ReallyNotBlocked `mappend` b = b
+ -- MissingClauses is dominant (absorptive)
+ b@MissingClauses `mappend` _ = b
+ _ `mappend` b@MissingClauses = b
+ -- StuckOn is second strongest
+ b@StuckOn{} `mappend` _ = b
+ _ `mappend` b@StuckOn{} = b
+ b `mappend` _ = b
+
-- | Something where a meta variable may block reduction.
-data Blocked t = Blocked MetaId t
- | NotBlocked t
- deriving (Typeable, Eq, Ord, Functor, Foldable, Traversable)
+data Blocked t
+ = Blocked { theBlockingMeta :: MetaId , ignoreBlocking :: t }
+ | NotBlocked { blockingStatus :: NotBlocked, ignoreBlocking :: t }
+ deriving (Typeable, Show, Functor, Foldable, Traversable)
+ -- deriving (Typeable, Eq, Ord, Functor, Foldable, Traversable)
+-- | Blocking by a meta is dominant.
instance Applicative Blocked where
pure = notBlocked
- Blocked x f <*> e = Blocked x $ f (ignoreBlocking e)
- NotBlocked f <*> e = f <$> e
-
+ f <*> e = ((f $> ()) `mappend` (e $> ())) $> ignoreBlocking f (ignoreBlocking e)
+
+-- -- | Blocking by a meta is dominant.
+-- instance Applicative Blocked where
+-- pure = notBlocked
+-- Blocked x f <*> e = Blocked x $ f (ignoreBlocking e)
+-- NotBlocked nb f <*> Blocked x e = Blocked x $ f e
+-- NotBlocked nb f <*> NotBlocked nb' e = NotBlocked (nb `mappend` nb') $ f e
+
+-- | @'Blocked' t@ without the @t@.
+type Blocked_ = Blocked ()
+
+instance Monoid Blocked_ where
+ mempty = notBlocked ()
+ -- ReallyNotBlocked is neutral
+ NotBlocked ReallyNotBlocked _ `mappend` b = b
+ b `mappend` NotBlocked ReallyNotBlocked _ = b
+ -- StuckOn is strongest
+ b@(NotBlocked StuckOn{} _) `mappend` _ = b
+ _ `mappend` b@(NotBlocked StuckOn{} _) = b
+ -- Blocked is weakest
+ b@Blocked{} `mappend` Blocked{} = b
+ Blocked{} `mappend` b = b
+ b `mappend` Blocked{} = b
+ -- For the other cases, we take the left
+ b `mappend` _ = b
+
+-- | When trying to reduce @f es@, on match failed on one
+-- elimination @e ∈ es@ that came with info @r :: NotBlocked@.
+-- @stuckOn e r@ produces the new @NotBlocked@ info.
+--
+-- 'MissingClauses' must be propagated, as this is blockage
+-- that can be lifted in the future (as more clauses are added).
+--
+-- @'StuckOn' e0@ is also propagated, since it provides more
+-- precise information as @StuckOn e@ (as @e0@ is the original
+-- reason why reduction got stuck and usually a subterm of @e@).
+-- An information like @StuckOn (Apply (Arg info (Var i [])))@
+-- (stuck on a variable) could be used by the lhs/coverage checker
+-- to trigger a split on that (pattern) variable.
+--
+-- In the remaining cases for @r@, we are terminally stuck
+-- due to @StuckOn e@. Propagating @'AbsurdMatch'@ does not
+-- seem useful.
+--
+-- 'Underapplied' must not be propagated, as this would mean
+-- that @f es@ is underapplied, which is not the case (it is stuck).
+-- Note that 'Underapplied' can only arise when projection patterns were
+-- missing to complete the original match (in @e@).
+-- (Missing ordinary pattern would mean the @e@ is of function type,
+-- but we cannot match against something of function type.)
+stuckOn :: Elim -> NotBlocked -> NotBlocked
+stuckOn e r =
+ case r of
+ MissingClauses -> r
+ StuckOn{} -> r
+ Underapplied -> r'
+ AbsurdMatch -> r'
+ ReallyNotBlocked -> r'
+ where r' = StuckOn e
---------------------------------------------------------------------------
-- * Definitions
@@ -258,7 +387,7 @@ instance Applicative Blocked where
-- the patterns to the order they occur in the telescope. The body
-- binds the variables in the order they appear in the patterns.
--
--- @clauseTel ~ permute clausePerm (patternVars clausPats)@
+-- @clauseTel ~ permute clausePerm (patternVars namedClausePats)@
--
-- Terms in dot patterns are valid in the clause telescope.
--
@@ -266,12 +395,16 @@ instance Applicative Blocked where
-- as variables. TODO: Change this!
data Clause = Clause
{ clauseRange :: Range
- , clauseTel :: Telescope -- ^ The types of the pattern variables.
+ , clauseTel :: Telescope
+ -- ^ @Δ@: The types of the pattern variables.
, clausePerm :: Permutation
+ -- ^ @π@ with @Γ ⊢ renamingR π : Δ@, which means @Δ ⊢ renaming π : Γ@.
, namedClausePats :: [NamedArg Pattern]
+ -- ^ @let Γ = patternVars namedClausePats@
, clauseBody :: ClauseBody
+ -- ^ @λΓ.v@
, clauseType :: Maybe (Arg Type)
- -- ^ The type of the rhs under @clauseTel@.
+ -- ^ @Δ ⊢ t@. The type of the rhs under @clauseTel@.
-- Used, e.g., by @TermCheck@.
-- Can be 'Irrelevant' if we encountered an irrelevant projection
-- pattern on the lhs.
@@ -342,6 +475,8 @@ data Pattern' x
type Pattern = Pattern' PatVarName
-- ^ The @PatVarName@ is a name suggestion.
+-- | Type used when numbering pattern variables.
+type DeBruijnPattern = Pattern' (Int, PatVarName)
namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern
namedVarP x = Named named $ VarP x
@@ -354,7 +489,23 @@ namedVarP x = Named named $ VarP x
-- The @Type@ is the type of the whole record pattern.
-- The scope used for the type is given by any outer scope
-- plus the clause's telescope ('clauseTel').
-type ConPatternInfo = Maybe (Bool, Arg Type)
+data ConPatternInfo = ConPatternInfo
+ { conPRecord :: Maybe Bool
+ -- ^ @Nothing@ if data constructor.
+ -- @Just@ if record constructor, then @True@ if pattern
+ -- was expanded from an implicit pattern.
+ , conPType :: Maybe (Arg Type)
+ -- ^ The type of the whole constructor pattern.
+ -- Should be present (@Just@) if constructor pattern is
+ -- is generated ordinarily by type-checking.
+ -- Could be absent (@Nothing@) if pattern comes from some
+ -- plugin (like Agsy).
+ -- Needed e.g. for with-clause stripping.
+ }
+ deriving (Typeable, Show)
+
+noConPatternInfo :: ConPatternInfo
+noConPatternInfo = ConPatternInfo Nothing Nothing
-- | Extract pattern variables in left-to-right order.
-- A 'DotP' is also treated as variable (see docu for 'Clause').
@@ -370,7 +521,7 @@ properlyMatching :: Pattern -> Bool
properlyMatching VarP{} = False
properlyMatching DotP{} = False
properlyMatching LitP{} = True
-properlyMatching (ConP _ mt ps) = isNothing mt || -- not a record cons
+properlyMatching (ConP _ ci ps) = isNothing (conPRecord ci) || -- not a record cons
List.any (properlyMatching . namedArg) ps -- or one of subpatterns is a proper m
properlyMatching ProjP{} = True
@@ -380,30 +531,56 @@ properlyMatching ProjP{} = True
-- | Substitutions.
-infixr 4 :#
data Substitution
- = IdS -- Γ ⊢ IdS : Γ
-
- | EmptyS -- Γ ⊢ EmptyS : ()
-
- -- Γ ⊢ ρ : Δ
- | Wk !Int Substitution -- -------------------
- -- Γ, Ψ ⊢ Wk |Ψ| ρ : Δ
-
- -- Γ ⊢ u : Aρ Γ ⊢ ρ : Δ
- | Term :# Substitution -- ---------------------
- -- Γ ⊢ u :# ρ : Δ, A
-
- -- First argument is __IMPOSSIBLE__ -- Γ ⊢ ρ : Δ
- | Strengthen Empty Substitution -- ---------------------------
- -- Γ ⊢ Strengthen ρ : Δ, A
-
- -- Γ ⊢ ρ : Δ
- | Lift !Int Substitution -- -------------------------
- -- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ
+ = IdS
+ -- ^ Identity substitution.
+ -- @Γ ⊢ IdS : Γ@
+
+ | EmptyS
+ -- ^ Empty substitution, lifts from the empty context.
+ -- Apply this to closed terms you want to use in a non-empty context.
+ -- @Γ ⊢ EmptyS : ()@
+
+ | Term :# Substitution
+ -- ^ Substitution extension, ``cons''.
+ -- @
+ -- Γ ⊢ u : Aρ Γ ⊢ ρ : Δ
+ -- ----------------------
+ -- Γ ⊢ u :# ρ : Δ, A
+ -- @
+
+ | Strengthen Empty Substitution
+ -- ^ Strengthening substitution. First argument is @__IMPOSSIBLE__@.
+ -- Apply this to a term which does not contain variable 0
+ -- to lower all de Bruijn indices by one.
+ -- @
+ -- Γ ⊢ ρ : Δ
+ -- ---------------------------
+ -- Γ ⊢ Strengthen ρ : Δ, A
+ -- @
+
+ | Wk !Int Substitution
+ -- ^ Weakning substitution, lifts to an extended context.
+ -- @
+ -- Γ ⊢ ρ : Δ
+ -- -------------------
+ -- Γ, Ψ ⊢ Wk |Ψ| ρ : Δ
+ -- @
+
+
+ | Lift !Int Substitution
+ -- ^ Lifting substitution. Use this to go under a binder.
+ -- @Lift 1 ρ == var 0 :# Wk 1 ρ@.
+ -- @
+ -- Γ ⊢ ρ : Δ
+ -- -------------------------
+ -- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ
+ -- @
deriving (Show)
+infixr 4 :#
+
---------------------------------------------------------------------------
-- * Absurd Lambda
---------------------------------------------------------------------------
@@ -518,12 +695,13 @@ sort :: Sort -> Type
sort s = El (sSuc s) $ Sort s
varSort :: Int -> Sort
-varSort n = Type $ Max [Plus 0 $ NeutralLevel $ Var n []]
+varSort n = Type $ Max [Plus 0 $ NeutralLevel mempty $ Var n []]
-- | Get the next higher sort.
sSuc :: Sort -> Sort
sSuc Prop = mkType 1
sSuc Inf = Inf
+sSuc SizeUniv = SizeUniv
sSuc (DLub a b) = DLub (sSuc a) (fmap sSuc b)
sSuc (Type l) = Type $ levelSuc l
@@ -542,6 +720,7 @@ impossibleTerm file line = Lit $ LitString noRange $ unlines
, "Location of the error: " ++ file ++ ":" ++ show line
]
+-- | Constructing a singleton telescope.
class SgTel a where
sgTel :: a -> Telescope
@@ -564,17 +743,13 @@ isHackReifyToMeta _ = False
blockingMeta :: Blocked t -> Maybe MetaId
blockingMeta (Blocked m _) = Just m
-blockingMeta (NotBlocked _) = Nothing
+blockingMeta NotBlocked{} = Nothing
blocked :: MetaId -> a -> Blocked a
blocked x = Blocked x
notBlocked :: a -> Blocked a
-notBlocked = NotBlocked
-
-ignoreBlocking :: Blocked a -> a
-ignoreBlocking (Blocked _ x) = x
-ignoreBlocking (NotBlocked x) = x
+notBlocked = NotBlocked ReallyNotBlocked
---------------------------------------------------------------------------
-- * Simple operations on terms and types.
@@ -610,6 +785,12 @@ instance Suggest String String where
instance Suggest (Abs a) (Abs b) where
suggest b1 b2 = suggest (absName b1) (absName b2)
+instance Suggest String (Abs b) where
+ suggest x b = suggest x (absName b)
+
+instance Suggest Name (Abs b) where
+ suggest n b = suggest (nameToArgName n) (absName b)
+
---------------------------------------------------------------------------
-- * Eliminations.
---------------------------------------------------------------------------
@@ -703,6 +884,30 @@ swapElimArg (Proj d) = defaultArg (Proj d)
-}
---------------------------------------------------------------------------
+-- * Null instances.
+---------------------------------------------------------------------------
+
+instance Null (Tele a) where
+ empty = EmptyTel
+ null EmptyTel = True
+ null ExtendTel{} = False
+
+instance Null ClauseBody where
+ empty = NoBody
+ null NoBody = True
+ null _ = False
+
+-- | A 'null' clause is one with no patterns and no rhs.
+-- Should not exist in practice.
+instance Null Clause where
+ empty = Clause empty empty empty empty empty empty
+ null (Clause r tel perm pats body t)
+ = null tel
+ && null pats
+ && null body
+
+
+---------------------------------------------------------------------------
-- * Show instances.
---------------------------------------------------------------------------
@@ -712,49 +917,21 @@ instance Show a => Show (Abs a) where
showsPrec p (NoAbs x a) = showParen (p > 0) $
showString "NoAbs " . shows x . showString " " . showsPrec 10 a
+-- | Show non-record version of this newtype.
instance Show MetaId where
- show (MetaId n) = "_" ++ show n
+ showsPrec p (MetaId n) = showParen (p > 0) $
+ showString "MetaId " . shows n
-instance Show t => Show (Blocked t) where
- showsPrec p (Blocked m x) = showParen (p > 0) $
- showString "Blocked " . shows m . showString " " . showsPrec 10 x
- showsPrec p (NotBlocked x) = showsPrec p x
+-- instance Show t => Show (Blocked t) where
+-- showsPrec p (Blocked m x) = showParen (p > 0) $
+-- showString "Blocked " . shows m . showString " " . showsPrec 10 x
+-- showsPrec p (NotBlocked x) = showsPrec p x
---------------------------------------------------------------------------
--- * Sized instances.
+-- * Sized instances and TermSize.
---------------------------------------------------------------------------
-instance Sized Term where
- size v = case v of
- Var _ vs -> 1 + Prelude.sum (map size vs)
- Def _ vs -> 1 + Prelude.sum (map size vs)
- Con _ vs -> 1 + Prelude.sum (map size vs)
- MetaV _ vs -> 1 + Prelude.sum (map size vs)
- Level l -> size l
- Lam _ f -> 1 + size f
- Lit _ -> 1
- Pi a b -> 1 + size a + size b
- Sort s -> 1
- DontCare mv -> size mv
- Shared p -> size (derefPtr p)
- ExtLam{} -> __IMPOSSIBLE__
-
-instance Sized Type where
- size = size . unEl
-
-instance Sized Level where
- size (Max as) = 1 + Prelude.sum (map size as)
-
-instance Sized PlusLevel where
- size (ClosedLevel _) = 1
- size (Plus _ a) = size a
-
-instance Sized LevelAtom where
- size (MetaLevel _ vs) = 1 + Prelude.sum (map size vs)
- size (BlockedLevel _ v) = size v
- size (NeutralLevel v) = size v
- size (UnreducedLevel v) = size v
-
+-- | The size of a telescope is its length (as a list).
instance Sized (Tele a) where
size EmptyTel = 0
size (ExtendTel _ tel) = 1 + size tel
@@ -762,9 +939,68 @@ instance Sized (Tele a) where
instance Sized a => Sized (Abs a) where
size = size . unAbs
-instance Sized a => Sized (Elim' a) where
- size (Apply v) = size v
- size Proj{} = 1
+-- | The size of a term is roughly the number of nodes in its
+-- syntax tree. This number need not be precise for logical
+-- correctness of Agda, it is only used for reporting
+-- (and maybe decisions regarding performance).
+--
+-- Not counting towards the term size are:
+--
+-- * sort and color annotations,
+-- * projections.
+--
+class TermSize a where
+ termSize :: a -> Int
+ termSize = getSum . tsize
+
+ tsize :: a -> Sum Int
+
+instance (Foldable t, TermSize a) => TermSize (t a) where
+ tsize = foldMap tsize
+
+instance TermSize Term where
+ tsize v = case v of
+ Var _ vs -> 1 + tsize vs
+ Def _ vs -> 1 + tsize vs
+ Con _ vs -> 1 + tsize vs
+ MetaV _ vs -> 1 + tsize vs
+ Level l -> tsize l
+ Lam _ f -> 1 + tsize f
+ Lit _ -> 1
+ Pi a b -> 1 + tsize a + tsize b
+ Sort s -> tsize s
+ DontCare mv -> tsize mv
+ Shared p -> tsize (derefPtr p)
+ ExtLam{} -> __IMPOSSIBLE__
+
+instance TermSize Sort where
+ tsize s = case s of
+ Type l -> 1 + tsize l
+ Prop -> 1
+ Inf -> 1
+ SizeUniv -> 1
+ DLub s s' -> 1 + tsize s + tsize s'
+
+instance TermSize Level where
+ tsize (Max as) = 1 + tsize as
+
+instance TermSize PlusLevel where
+ tsize (ClosedLevel _) = 1
+ tsize (Plus _ a) = tsize a
+
+instance TermSize LevelAtom where
+ tsize (MetaLevel _ vs) = 1 + tsize vs
+ tsize (BlockedLevel _ v) = tsize v
+ tsize (NeutralLevel _ v) = tsize v
+ tsize (UnreducedLevel v) = tsize v
+
+instance TermSize Substitution where
+ tsize IdS = 1
+ tsize EmptyS = 1
+ tsize (Wk _ rho) = 1 + tsize rho
+ tsize (t :# rho) = 1 + tsize t + tsize rho
+ tsize (Strengthen _ rho) = 1 + tsize rho
+ tsize (Lift _ rho) = 1 + tsize rho
---------------------------------------------------------------------------
-- * KillRange instances.
@@ -798,7 +1034,7 @@ instance KillRange PlusLevel where
instance KillRange LevelAtom where
killRange (MetaLevel n as) = killRange1 (MetaLevel n) as
killRange (BlockedLevel m v) = killRange1 (BlockedLevel m) v
- killRange (NeutralLevel v) = killRange1 NeutralLevel v
+ killRange (NeutralLevel r v) = killRange1 (NeutralLevel r) v
killRange (UnreducedLevel v) = killRange1 UnreducedLevel v
instance KillRange Type where
@@ -808,9 +1044,21 @@ instance KillRange Sort where
killRange s = case s of
Prop -> Prop
Inf -> Inf
+ SizeUniv -> SizeUniv
Type a -> killRange1 Type a
DLub s1 s2 -> killRange2 DLub s1 s2
+instance KillRange Substitution where
+ killRange IdS = IdS
+ killRange EmptyS = EmptyS
+ killRange (Wk n rho) = killRange1 (Wk n) rho
+ killRange (t :# rho) = killRange2 (:#) t rho
+ killRange (Strengthen err rho) = killRange1 (Strengthen err) rho
+ killRange (Lift n rho) = killRange1 (Lift n) rho
+
+instance KillRange ConPatternInfo where
+ killRange (ConPatternInfo mr mt) = killRange1 (ConPatternInfo mr) mt
+
instance KillRange Pattern where
killRange p =
case p of
@@ -857,8 +1105,19 @@ instanceUniverseBiT' [] [t| ([Term], Term) |]
-- * Simple pretty printing
-----------------------------------------------------------------------------
-showTerm :: Term -> String
-showTerm = show . pretty
+instance Pretty MetaId where
+ pretty (MetaId n) = text $ "_" ++ show n
+
+instance Pretty Substitution where
+ prettyPrec p rho = brackets $ pr rho
+ where
+ pr rho = case rho of
+ IdS -> text "idS"
+ EmptyS -> text "ε"
+ t :# rho -> prettyPrec 1 t <+> text ":#" <+> pr rho
+ Strengthen _ rho -> text "↓" <+> pr rho
+ Wk n rho -> text ("↑" ++ show n) <+> pr rho
+ Lift n rho -> text ("⇑" ++ show n) <+> pr rho
instance Pretty Term where
prettyPrec p v =
@@ -879,7 +1138,7 @@ instance Pretty Term where
, nest 2 $ pretty (unAbs b) ]
Sort s -> pretty s
Level l -> pretty l
- MetaV x els -> text (show x) `pApp` els
+ MetaV x els -> pretty x `pApp` els
DontCare v -> pretty v
Shared{} -> __IMPOSSIBLE__
ExtLam{} -> __IMPOSSIBLE__
@@ -914,7 +1173,7 @@ instance Pretty LevelAtom where
case a of
MetaLevel x els -> prettyPrec p (MetaV x els)
BlockedLevel _ v -> prettyPrec p v
- NeutralLevel v -> prettyPrec p v
+ NeutralLevel _ v -> prettyPrec p v
UnreducedLevel v -> prettyPrec p v
instance Pretty Sort where
@@ -925,6 +1184,7 @@ instance Pretty Sort where
Type l -> mparens (p > 9) $ text "Set" <+> prettyPrec 10 l
Prop -> text "Prop"
Inf -> text "Setω"
+ SizeUniv -> text "SizeUniv"
DLub s b -> mparens (p > 9) $
text "dlub" <+> prettyPrec 10 s
<+> parens (sep [ text ("λ " ++ show (absName b) ++ " ->")
diff --git a/src/full/Agda/Syntax/Internal/Defs.hs b/src/full/Agda/Syntax/Internal/Defs.hs
index dd4fc38..a79b7be 100644
--- a/src/full/Agda/Syntax/Internal/Defs.hs
+++ b/src/full/Agda/Syntax/Internal/Defs.hs
@@ -1,6 +1,5 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
-- | Extract used definitions from terms.
module Agda.Syntax.Internal.Defs where
@@ -82,6 +81,7 @@ instance GetDefs Sort where
Type l -> getDefs l
Prop -> return ()
Inf -> return ()
+ SizeUniv -> return ()
DLub s s' -> getDefs s >> getDefs s'
instance GetDefs Level where
@@ -95,7 +95,7 @@ instance GetDefs LevelAtom where
getDefs a = case a of
MetaLevel x vs -> getDefs x >> getDefs vs
BlockedLevel _ v -> getDefs v
- NeutralLevel v -> getDefs v
+ NeutralLevel _ v -> getDefs v
UnreducedLevel v -> getDefs v
-- collection instances
diff --git a/src/full/Agda/Syntax/Internal/Generic.hs b/src/full/Agda/Syntax/Internal/Generic.hs
index 9da57c2..d0e9552 100644
--- a/src/full/Agda/Syntax/Internal/Generic.hs
+++ b/src/full/Agda/Syntax/Internal/Generic.hs
@@ -1,6 +1,5 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
module Agda.Syntax.Internal.Generic where
@@ -160,17 +159,17 @@ instance TermLike PlusLevel where
instance TermLike LevelAtom where
traverseTerm f l = case l of
MetaLevel m vs -> MetaLevel m $ traverseTerm f vs
- NeutralLevel v -> NeutralLevel $ traverseTerm f v
+ NeutralLevel r v -> NeutralLevel r $ traverseTerm f v
BlockedLevel m v -> BlockedLevel m $ traverseTerm f v
UnreducedLevel v -> UnreducedLevel $ traverseTerm f v
traverseTermM f l = case l of
MetaLevel m vs -> MetaLevel m <$> traverseTermM f vs
- NeutralLevel v -> NeutralLevel <$> traverseTermM f v
+ NeutralLevel r v -> NeutralLevel r <$> traverseTermM f v
BlockedLevel m v -> BlockedLevel m <$> traverseTermM f v
UnreducedLevel v -> UnreducedLevel <$> traverseTermM f v
foldTerm f l = case l of
MetaLevel m vs -> foldTerm f vs
- NeutralLevel v -> foldTerm f v
+ NeutralLevel _ v -> foldTerm f v
BlockedLevel _ v -> foldTerm f v
UnreducedLevel v -> foldTerm f v
diff --git a/src/full/Agda/Syntax/Internal/Pattern.hs b/src/full/Agda/Syntax/Internal/Pattern.hs
index 7f9ca74..78da0c4 100644
--- a/src/full/Agda/Syntax/Internal/Pattern.hs
+++ b/src/full/Agda/Syntax/Internal/Pattern.hs
@@ -1,12 +1,14 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverlappingInstances #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE UndecidableInstances #-} -- because of func. deps.
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE UndecidableInstances #-} -- because of func. deps.
+
+#if __GLASGOW_HASKELL__ <= 708
+{-# LANGUAGE OverlappingInstances #-}
+#endif
module Agda.Syntax.Internal.Pattern where
@@ -49,7 +51,12 @@ class FunArity a where
funArity :: a -> Int
-- | Get the number of initial 'Apply' patterns.
+
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPABLE #-} IsProjP p => FunArity [p] where
+#else
instance IsProjP p => FunArity [p] where
+#endif
funArity = length . takeWhile (isNothing . isProjP)
-- | Get the number of initial 'Apply' patterns in a clause.
@@ -57,7 +64,11 @@ instance FunArity Clause where
funArity = funArity . clausePats
-- | Get the number of common initial 'Apply' patterns in a list of clauses.
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPING #-} FunArity [Clause] where
+#else
instance FunArity [Clause] where
+#endif
funArity [] = 0
funArity cls = minimum $ map funArity cls
@@ -90,7 +101,8 @@ instance LabelPatVars (Pattern' x) (Pattern' (i,x)) i where
where next = do (x:xs) <- get; put xs; return x
-- | Augment pattern variables with their de Bruijn index.
-{-# SPECIALIZE numberPatVars :: Permutation -> [NamedArg (Pattern' x)] -> [(NamedArg (Pattern' (Int, x)))] #-}
+{-# SPECIALIZE numberPatVars :: Permutation -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' (Int, x))] #-}
+{-# SPECIALIZE numberPatVars :: Permutation -> [NamedArg Pattern] -> [NamedArg DeBruijnPattern] #-}
numberPatVars :: LabelPatVars a b Int => Permutation -> a -> b
numberPatVars perm ps = evalState (labelPatVars ps) $
permute (invertP __IMPOSSIBLE__ perm) $ downFrom $ size perm
diff --git a/src/full/Agda/Syntax/Notation.hs b/src/full/Agda/Syntax/Notation.hs
index 71bc525..eee7ec5 100644
--- a/src/full/Agda/Syntax/Notation.hs
+++ b/src/full/Agda/Syntax/Notation.hs
@@ -1,6 +1,7 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+-- GHC 7.4.2 requires this layout for the pragmas. See Issue 1460.
+{-# LANGUAGE CPP,
+ DeriveDataTypeable,
+ ScopedTypeVariables #-}
{-| As a concrete name, a notation is a non-empty list of alternating 'IdPart's and holes.
In contrast to concrete names, holes can be binders.
@@ -23,6 +24,7 @@ import Data.Maybe
import Data.Typeable (Typeable)
import Agda.Syntax.Common
+import Agda.Syntax.Position
import Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.List
@@ -54,7 +56,13 @@ data GenPart
| NormalHole (NamedArg () Int)
-- ^ Argument is where the expression should go.
| IdPart RawName
- deriving (Typeable, Show, Eq)
+ deriving (Typeable, Show, Eq, Ord)
+
+instance KillRange GenPart where
+ killRange p = case p of
+ IdPart x -> IdPart x
+ BindHole i -> BindHole i
+ NormalHole x -> NormalHole $ killRange x
-- | Get a flat list of identifier parts of a notation.
stringParts :: Notation -> [RawName]
@@ -83,7 +91,7 @@ data NotationKind
| PostfixNotation -- ^ Ex: @bla_blub_@.
| NonfixNotation -- ^ Ex: @bla_blub@.
| NoNotation
- deriving (Eq)
+ deriving (Eq, Show)
-- | Classify a notation by presence of leading and/or trailing hole.
notationKind :: Notation -> NotationKind
diff --git a/src/full/Agda/Syntax/Parser/LookAhead.hs b/src/full/Agda/Syntax/Parser/LookAhead.hs
index c683627..da15019 100644
--- a/src/full/Agda/Syntax/Parser/LookAhead.hs
+++ b/src/full/Agda/Syntax/Parser/LookAhead.hs
@@ -1,5 +1,5 @@
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE Rank2Types #-}
{-| When lexing by hands (for instance string literals) we need to do some
looking ahead. The 'LookAhead' monad keeps track of the position we are
diff --git a/src/full/Agda/Syntax/Parser/Monad.hs b/src/full/Agda/Syntax/Parser/Monad.hs
index c5cb2d6..3b1015e 100644
--- a/src/full/Agda/Syntax/Parser/Monad.hs
+++ b/src/full/Agda/Syntax/Parser/Monad.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Agda.Syntax.Parser.Monad
@@ -32,7 +32,7 @@ module Agda.Syntax.Parser.Monad
import Control.Exception
import Data.Int
-import Data.Typeable
+import Data.Typeable ( Typeable )
import Control.Monad.State
import Control.Applicative
@@ -44,6 +44,8 @@ import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
import qualified Agda.Utils.IO.UTF8 as UTF8
+import Agda.Utils.Pretty
+
{--------------------------------------------------------------------------
The parse monad
--------------------------------------------------------------------------}
@@ -90,12 +92,11 @@ data ParseFlags = ParseFlags
-- | What you get if parsing fails.
data ParseError = ParseError
- { errPos :: Position -- ^ where the error occured
- , errInput :: String -- ^ the remaining input
- , errPrevToken :: String -- ^ the previous token
- , errMsg :: String -- ^ hopefully an explanation
- -- of what happened
- }
+ { errPos :: Position -- ^ where the error occured
+ , errInput :: String -- ^ the remaining input
+ , errPrevToken :: String -- ^ the previous token
+ , errMsg :: String -- ^ hopefully an explanation of what happened
+ }
deriving (Typeable)
instance Exception ParseError
@@ -109,55 +110,49 @@ data ParseResult a = ParseOk ParseState a
--------------------------------------------------------------------------}
instance Monad Parser where
- return x = P $ \s -> ParseOk s x
- P m >>= f = P $ \s -> case m s of
- ParseFailed e -> ParseFailed e
- ParseOk s' x -> unP (f x) s'
- fail msg = P $ \s -> ParseFailed $
- ParseError { errPos = parseLastPos s
- , errInput = parseInp s
- , errPrevToken = parsePrevToken s
- , errMsg = msg
- }
+ return x = P $ \s -> ParseOk s x
+
+ P m >>= f = P $ \s -> case m s of
+ ParseFailed e -> ParseFailed e
+ ParseOk s' x -> unP (f x) s'
+
+ fail msg = P $ \s -> ParseFailed $
+ ParseError { errPos = parseLastPos s
+ , errInput = parseInp s
+ , errPrevToken = parsePrevToken s
+ , errMsg = msg
+ }
instance Functor Parser where
- fmap = liftM
+ fmap = liftM
instance Applicative Parser where
- pure = return
- (<*>) = ap
+ pure = return
+ (<*>) = ap
instance MonadError ParseError Parser where
- throwError e = P $ \_ -> ParseFailed e
- P m `catchError` h = P $ \s -> case m s of
- ParseFailed err -> unP (h err) s
- m' -> m'
+ throwError e = P $ \_ -> ParseFailed e
+
+ P m `catchError` h = P $ \s -> case m s of
+ ParseFailed err -> unP (h err) s
+ m' -> m'
instance MonadState ParseState Parser where
- get = P $ \s -> ParseOk s s
- put s = P $ \_ -> ParseOk s ()
+ get = P $ \s -> ParseOk s s
+ put s = P $ \_ -> ParseOk s ()
instance Show ParseError where
- show err =
- unlines
- [ pos ++ ": " ++ errMsg err
- --, replicate (length pos + 2) ' ' ++ "on '" ++ errPrevToken err ++ "'"
- , errPrevToken err ++ "<ERROR>\n" ++ take 30 (errInput err) ++ "..."
- ]
- where
- pos = show (errPos err)
-
--- showInp "" = "at end of file"
--- showInp t = "on input " ++ elide 5 t
---
--- elide 3 s
--- | length (take 4 s) < 4 = s
--- | otherwise = "..."
--- elide n (c:s) = c : elide (n - 1) s
--- elide _ "" = ""
+ show = prettyShow
+
+instance Pretty ParseError where
+ pretty err = vcat
+ [ pretty (errPos err) <> colon <+> text (errMsg err)
+ , text $ errPrevToken err ++ "<ERROR>"
+ , text $ take 30 (errInput err) ++ "..."
+ ]
instance HasRange ParseError where
- getRange err = posToRange (errPos err) (errPos err)
+ getRange err = posToRange (errPos err) (errPos err)
{--------------------------------------------------------------------------
Running the parser
diff --git a/src/full/Agda/Syntax/Parser/Parser.y b/src/full/Agda/Syntax/Parser/Parser.y
index 0181719..cf924e6 100644
--- a/src/full/Agda/Syntax/Parser/Parser.y
+++ b/src/full/Agda/Syntax/Parser/Parser.y
@@ -1,4 +1,6 @@
{
+{-# LANGUAGE TupleSections #-}
+
{-| The parser is generated by Happy (<http://www.haskell.org/happy>).
-
- Ideally, ranges should be as precise as possible, to get messages that
@@ -43,6 +45,7 @@ import Agda.Utils.Hash
import Agda.Utils.List (spanJust)
import Agda.Utils.Monad
import Agda.Utils.QuickCheck
+import Agda.Utils.Singleton
import Agda.Utils.TestHelpers
import Agda.Utils.Tuple
@@ -456,33 +459,56 @@ CommaBIds : CommaBIdAndAbsurds {
Left ns -> ns
Right _ -> fail $ "expected sequence of bound identifiers, not absurd pattern"
}
-{-
- let getName (Ident (QName x)) = Just x
+
+CommaBIdAndAbsurds :: { Either [Name] [Expr] }
+CommaBIdAndAbsurds : Application {%
+ let getName :: Expr -> Maybe Name
+ getName (Ident (QName x)) = Just x
getName (Underscore r _) = Just (Name r [Hole])
getName _ = Nothing
+
+ isAbsurd :: Expr -> Bool
+ isAbsurd (Absurd _) = True
+ isAbsurd (HiddenArg _ (Named _ e)) = isAbsurd e
+ isAbsurd (InstanceArg _ (Named _ e)) = isAbsurd e
+ isAbsurd (Paren _ expr) = isAbsurd expr
+ isAbsurd (RawApp _ exprs) = any isAbsurd exprs
+ isAbsurd _ = False
in
- case partition isJust $ map getName $1 of
- (good, []) -> return $ map fromJust good
- _ -> fail $ "expected sequence of bound identifiers"
--}
+ if any isAbsurd $1 then return $ Right $1 else
+ case mapM getName $1 of
+ Just good -> return $ Left good
+ Nothing -> fail $ "expected sequence of bound identifiers"
+ }
-CommaBIdAndAbsurds :: { Either [Name] [Expr] }
-CommaBIdAndAbsurds : Application {%
- let getName (Ident (QName x)) = Just x
+-- Parse a sequence of identifiers, including hiding info.
+-- Does not include instance arguments.
+-- E.g. x {y z} _ {v}
+-- To be used in typed bindings, like (x {y z} _ {v} : Nat).
+BIdsWithHiding :: { [WithHiding Name] }
+BIdsWithHiding : Application {%
+ let -- interpret an expression as name
+ getName :: Expr -> Maybe Name
+ getName (Ident (QName x)) = Just x
getName (Underscore r _) = Just (Name r [Hole])
getName _ = Nothing
- containsAbsurd (Absurd _) = True
- containsAbsurd (HiddenArg _ (Named _ e)) = containsAbsurd e
- containsAbsurd (InstanceArg _ (Named _ e)) = containsAbsurd e
- containsAbsurd (Paren _ expr) = containsAbsurd expr
- containsAbsurd (RawApp _ exprs) = any containsAbsurd exprs
- containsAbsurd _ = False
+ getNames :: Expr -> Maybe [Name]
+ getNames (RawApp _ es) = mapM getName es
+ getNames e = singleton `fmap` getName e
+
+ -- interpret an expression as name or list of hidden names
+ getName1 :: Expr -> Maybe [WithHiding Name]
+ getName1 (Ident (QName x)) = Just [WithHiding NotHidden x]
+ getName1 (Underscore r _) = Just [WithHiding NotHidden $ Name r [Hole]]
+ getName1 (HiddenArg _ (Named Nothing e))
+ = map (WithHiding Hidden) `fmap` getNames e
+ getName1 _ = Nothing
+
in
- if isJust $ find containsAbsurd $1 then return $ Right $1 else
- case partition isJust $ map getName $1 of
- (good, []) -> return $ Left $ map fromJust good
- _ -> fail $ "expected sequence of bound identifiers"
+ case mapM getName1 $1 of
+ Just good -> return $ concat good
+ Nothing -> fail $ "expected sequence of possibly hidden bound identifiers"
}
@@ -646,32 +672,41 @@ TypedBindingss
-- Andreas, 2011-04-27: or ..(x1 .. xn : A) or ..{y1 .. ym : B}
TypedBindings :: { TypedBindings }
TypedBindings
- : '.' '(' TBind ')' { TypedBindings (getRange ($2,$3,$4))
- (setRelevance Irrelevant $ defaultColoredArg $3) }
- | '.' '{' TBind '}' { TypedBindings (getRange ($2,$3,$4))
- (hide $ setRelevance Irrelevant $ defaultColoredArg $3) }
- | '.' '{{' TBind DoubleCloseBrace { TypedBindings (getRange ($2,$3,$4))
- (makeInstance $ setRelevance Irrelevant $ defaultColoredArg $3) }
- | '..' '(' TBind ')' { TypedBindings (getRange ($2,$3,$4))
- (setRelevance NonStrict $ defaultColoredArg $3) }
- | '..' '{' TBind '}' { TypedBindings (getRange ($2,$3,$4))
- (hide $ setRelevance NonStrict $ defaultColoredArg $3) }
- | '..' '{{' TBind DoubleCloseBrace { TypedBindings (getRange ($2,$3,$4))
- (makeInstance $ setRelevance NonStrict $ defaultColoredArg $3) }
- | '(' TBind ')' { TypedBindings (getRange ($1,$2,$3))
- (defaultColoredArg $2) }
- | '{{' TBind DoubleCloseBrace { TypedBindings (getRange ($1,$2,$3))
- (makeInstance $ defaultColoredArg $2) }
- | '{' TBind '}' { TypedBindings (getRange ($1,$2,$3))
- (hide $ defaultColoredArg $2) }
+ : '.' '(' TBindWithHiding ')' { setRange (getRange ($2,$3,$4)) $
+ setRelevance Irrelevant $3 }
+ | '.' '{' TBind '}' { setRange (getRange ($2,$3,$4)) $
+ setHiding Hidden $
+ setRelevance Irrelevant $3 }
+ | '.' '{{' TBind DoubleCloseBrace
+ { setRange (getRange ($2,$3,$4)) $
+ setHiding Instance $
+ setRelevance Irrelevant $3 }
+ | '..' '(' TBindWithHiding ')' { setRange (getRange ($2,$3,$4)) $
+ setRelevance NonStrict $3 }
+ | '..' '{' TBind '}' { setRange (getRange ($2,$3,$4)) $
+ setHiding Hidden $
+ setRelevance NonStrict $3 }
+ | '..' '{{' TBind DoubleCloseBrace
+ { setRange (getRange ($2,$3,$4)) $
+ setHiding Instance $
+ setRelevance NonStrict $3 }
+ | '(' TBindWithHiding ')' { setRange (getRange ($1,$2,$3)) $2 }
+ | '{{' TBind DoubleCloseBrace
+ { setRange (getRange ($1,$2,$3)) $
+ setHiding Instance $2 }
+ | '{' TBind '}' { setRange (getRange ($1,$2,$3)) $
+ setHiding Hidden $2 }
| '(' Open ')' { tLet (getRange ($1,$3)) $2 }
| '(' 'let' Declarations ')' { tLet (getRange ($1,$4)) $3 }
-- x1 .. xn : A
-- x1 .. xn :{i1 i2 ..} A
-TBind :: { ( [Color], TypedBinding ) }
-TBind : CommaBIds ':' Expr { ( [], TBind (getRange ($1,$2,$3)) (map mkBoundName_ $1) $3 ) }
+TBind :: { TypedBindings }
+TBind : CommaBIds ':' Expr {
+ let r = getRange ($1,$2,$3) -- the range is approximate only for TypedBindings
+ in TypedBindings r $ defaultArg $ TBind r (map (pure . mkBoundName_) $1) $3
+ }
-- | Colors are not yet allowed in the syntax.
-- | CommaBIds ':{' Colors '}' Expr { ( $3, TBind (getRange ($1,$2,$3,$4,$5)) (map mkBoundName_ $1) $5 ) }
{-
@@ -679,6 +714,14 @@ Colors :: { [Color] }
Colors : QId Colors { Ident $1 : $2 }
| QId { [Ident $1] }
-}
+
+-- x {y z} _ {v} : A
+TBindWithHiding :: { TypedBindings }
+TBindWithHiding : BIdsWithHiding ':' Expr {
+ let r = getRange ($1,$2,$3) -- the range is approximate only for TypedBindings
+ in TypedBindings r $ defaultArg $ TBind r (map (fmap mkBoundName_) $1) $3
+ }
+
-- A non-empty sequence of lambda bindings.
LamBindings :: { [LamBinding] }
LamBindings
@@ -696,7 +739,7 @@ AbsurdLamBindings
Left lb -> case reverse lb of
Right _ : _ -> parseError "Missing body for lambda"
Left h : _ -> return $ Left ([ b | Right b <- init lb], h)
- _ -> parsePanic "Empty LamBindsAbsurd"
+ _ -> parseError "Unsupported variant of lambda"
Right es -> return $ Right es
}
@@ -814,13 +857,6 @@ DomainFreeBindingAbsurd
Modules and imports
--------------------------------------------------------------------------}
--- You can rename imports
--- ImportImportDirective :: { (Maybe AsName, ImportDirective) }
--- ImportImportDirective
--- : ImportDirective { (Nothing, $1) }
--- | id Id ImportDirective {% isName "as" $1 >>
--- return (Just (AsName $2 (getRange (fst $1))), $3) }
-
-- Import directives
ImportDirective :: { ImportDirective }
ImportDirective : ImportDirectives {% mergeImportDirectives $1 }
@@ -841,7 +877,6 @@ UsingOrHiding
-- using can have an empty list
| 'hiding' '(' CommaImportNames ')' { (Hiding $3 , getRange ($1,$2,$3,$4)) }
-- if you want to hide nothing that's fine, isn't it?
--- | 'hiding' '(' CommaImportNames1 ')' { (Hiding $3 , getRange ($1,$2,$3,$4)) }
RenamingDir :: { ([Renaming] , Range) }
RenamingDir
@@ -956,13 +991,13 @@ Declaration
-- Type signatures of the form "n1 n2 n3 ... : Type", with at least
-- one bound name.
TypeSigs :: { [Declaration] }
-TypeSigs : SpaceIds ':' Expr { map (flip (TypeSig defaultArgInfo) $3) $1 }
+TypeSigs : SpaceIds ':' Expr { map (\ x -> TypeSig defaultArgInfo x $3) $1 }
-- A variant of TypeSigs where any sub-sequence of names can be marked
-- as hidden or irrelevant using braces and dots:
-- {n1 .n2} n3 .n4 {n5} .{n6 n7} ... : Type.
ArgTypeSigs :: { [Arg Declaration] }
-ArgTypeSigs : ArgIds ':' Expr { map (fmap (flip (TypeSig defaultArgInfo) $3)) $1 }
+ArgTypeSigs : ArgIds ':' Expr { map (fmap (\ x -> TypeSig defaultArgInfo x $3)) $1 }
-- Function declarations. The left hand side is parsed as an expression to allow
-- declarations like 'x::xs ++ ys = e', when '::' has higher precedence than '++'.
@@ -1017,9 +1052,9 @@ RecordConstructorName : 'constructor' Id { $2 }
-- Fixity declarations.
Infix :: { Declaration }
-Infix : 'infix' Int SpaceBIds { Infix (NonAssoc (getRange ($1,$3)) $2) $3 }
- | 'infixl' Int SpaceBIds { Infix (LeftAssoc (getRange ($1,$3)) $2) $3 }
- | 'infixr' Int SpaceBIds { Infix (RightAssoc (getRange ($1,$3)) $2) $3 }
+Infix : 'infix' Int SpaceBIds { Infix (Fixity (getRange ($1,$3)) $2 NonAssoc) $3 }
+ | 'infixl' Int SpaceBIds { Infix (Fixity (getRange ($1,$3)) $2 LeftAssoc) $3 }
+ | 'infixr' Int SpaceBIds { Infix (Fixity (getRange ($1,$3)) $2 RightAssoc) $3 }
-- Field declarations.
Fields :: { [Declaration] }
@@ -1256,6 +1291,7 @@ BuiltinPragma :: { Pragma }
BuiltinPragma
: '{-#' 'BUILTIN' string PragmaQName '#-}'
{ BuiltinPragma (getRange ($1,$2,fst $3,$4,$5)) (snd $3) (Ident $4) }
+ -- Extra rule to accept keword REWRITE also as built-in:
| '{-#' 'BUILTIN' 'REWRITE' PragmaQName '#-}'
{ BuiltinPragma (getRange ($1,$2,$3,$4,$5)) "REWRITE" (Ident $4) }
@@ -1507,7 +1543,7 @@ tLet r = TypedBindings r . Common.Arg defaultArgInfo . TLet r
-- | Converts lambda bindings to typed bindings.
addType :: LamBinding -> TypedBindings
addType (DomainFull b) = b
-addType (DomainFree info x) = TypedBindings r $ Common.Arg info $ TBind r [x] $ Underscore r Nothing
+addType (DomainFree info x) = TypedBindings r $ Common.Arg info $ TBind r [pure x] $ Underscore r Nothing
where r = getRange x
mergeImportDirectives :: [ImportDirective] -> Parser ImportDirective
diff --git a/src/full/Agda/Syntax/Position.hs b/src/full/Agda/Syntax/Position.hs
index 33ac69b..47bf553 100644
--- a/src/full/Agda/Syntax/Position.hs
+++ b/src/full/Agda/Syntax/Position.hs
@@ -1,19 +1,14 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-
-#if __GLASGOW_HASKELL__ <= 700
-{-# LANGUAGE OverlappingInstances #-}
-#endif
-
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+-- GHC 7.4.2 requires this layout for the pragmas. See Issue 1460.
+{-# LANGUAGE CPP,
+ DeriveDataTypeable,
+ DeriveFoldable,
+ DeriveFunctor,
+ DeriveTraversable,
+ FlexibleInstances,
+ GeneralizedNewtypeDeriving,
+ NoMonomorphismRestriction,
+ ScopedTypeVariables,
+ TemplateHaskell #-}
{-| Position information for syntax. Crucial for giving good error messages.
-}
@@ -47,6 +42,7 @@ module Agda.Syntax.Position
, rangeToInterval
, continuous
, continuousPerLine
+ , PrintRange(..)
, HasRange(..)
, SetRange(..)
, KillRange(..)
@@ -66,13 +62,15 @@ module Agda.Syntax.Position
import Prelude hiding (null)
-import Control.Applicative
+import Control.Applicative hiding (empty)
import Control.Monad
import Data.Foldable (Foldable)
import Data.Function
import Data.Int
import Data.List hiding (null)
+import Data.Map (Map)
+import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (Traversable)
@@ -83,7 +81,7 @@ import Test.QuickCheck.All
import Agda.Utils.FileName hiding (tests)
import Agda.Utils.Maybe
import Agda.Utils.Null
-import Agda.Utils.Pretty ( (<>), Pretty(pretty) )
+import Agda.Utils.Pretty
import Agda.Utils.TestHelpers
import Agda.Utils.QuickCheck
@@ -171,6 +169,10 @@ rightMargin r@(Range is) =
if null is then r else
let i = last is in Range [ i { iStart = iEnd i } ]
+-- | Wrapper to indicate that range should be printed.
+newtype PrintRange a = PrintRange a
+ deriving (Eq, Ord, HasRange, SetRange, KillRange)
+
-- | Things that have a range are instances of this class.
class HasRange t where
getRange :: t -> Range
@@ -215,6 +217,9 @@ class HasRange t => SetRange t where
instance SetRange Range where
setRange = const
+instance SetRange a => SetRange [a] where
+ setRange r = fmap $ setRange r
+
-- | Killing the range of an object sets all range information to 'noRange'.
class KillRange a where
killRange :: KillRangeT a
@@ -356,9 +361,30 @@ instance KillRange Bool where
instance KillRange Int where
killRange = id
+instance KillRange Integer where
+ killRange = id
+
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPABLE #-} KillRange a => KillRange [a] where
+#else
instance KillRange a => KillRange [a] where
+#endif
killRange = map killRange
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPABLE #-} KillRange a => KillRange (Map k a) where
+#else
+instance KillRange a => KillRange (Map k a) where
+#endif
+ killRange = fmap killRange
+
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPABLE #-} (Ord a, KillRange a) => KillRange (Set a) where
+#else
+instance (Ord a, KillRange a) => KillRange (Set a) where
+#endif
+ killRange = Set.map killRange
+
instance (KillRange a, KillRange b) => KillRange (a, b) where
killRange (x, y) = (killRange x, killRange y)
@@ -366,6 +392,10 @@ instance (KillRange a, KillRange b, KillRange c) =>
KillRange (a, b, c) where
killRange (x, y, z) = killRange3 (,,) x y z
+instance (KillRange a, KillRange b, KillRange c, KillRange d) =>
+ KillRange (a, b, c, d) where
+ killRange (x, y, z, u) = killRange4 (,,,) x y z u
+
instance KillRange a => KillRange (Maybe a) where
killRange = fmap killRange
@@ -379,27 +409,34 @@ instance (KillRange a, KillRange b) => KillRange (Either a b) where
-- TODO: 'Show' should output Haskell-parseable representations.
-- The following instances are deprecated, and Pretty should be used
--- instead. Later, simply derive Show for these types:
+-- instead. Later, simply derive Show for these types.
+-- ASR (02 December 2014). This instance is not used anymore (module
+-- the test suite) when reporting errors. See Issue 1293.
instance Show a => Show (Position' (Maybe a)) where
- show (Pn Nothing _ l c) = show l ++ "," ++ show c
- show (Pn (Just f) _ l c) = show f ++ ":" ++ show l ++ "," ++ show c
+ show (Pn Nothing _ l c) = show l ++ "," ++ show c
+ show (Pn (Just f) _ l c) = show f ++ ":" ++ show l ++ "," ++ show c
instance Show a => Show (Interval' (Maybe a)) where
- show (Interval s e) = file ++ start ++ "-" ++ end
- where
- f = srcFile s
- sl = posLine s
- el = posLine e
- sc = posCol s
- ec = posCol e
- file = case f of
- Nothing -> ""
- Just f -> show f ++ ":"
- start = show sl ++ "," ++ show sc
- end
- | sl == el = show ec
- | otherwise = show el ++ "," ++ show ec
+ show (Interval s e) = file ++ start ++ "-" ++ end
+ where
+ f = srcFile s
+ sl = posLine s
+ el = posLine e
+ sc = posCol s
+ ec = posCol e
+
+ file :: String
+ file = case f of
+ Nothing -> ""
+ Just f -> show f ++ ":"
+
+ start :: String
+ start = show sl ++ "," ++ show sc
+
+ end :: String
+ end | sl == el = show ec
+ | otherwise = show el ++ "," ++ show ec
instance Show a => Show (Range' (Maybe a)) where
show r = case rangeToInterval r of
@@ -411,9 +448,38 @@ instance Show a => Show (Range' (Maybe a)) where
------------------------------------------------------------------------
instance Pretty a => Pretty (Position' (Maybe a)) where
- pretty (Pn Nothing _ l c) = pretty l <> pretty "," <> pretty c
- pretty (Pn (Just f) _ l c) =
- pretty f <> pretty ":" <> pretty l <> pretty "," <> pretty c
+ pretty (Pn Nothing _ l c) = pretty l <> pretty "," <> pretty c
+ pretty (Pn (Just f) _ l c) =
+ pretty f <> pretty ":" <> pretty l <> pretty "," <> pretty c
+
+instance Pretty a => Pretty (Interval' (Maybe a)) where
+ pretty (Interval s e) = file <> start <> pretty "-" <> end
+ where
+ f = srcFile s
+ sl = posLine s
+ el = posLine e
+ sc = posCol s
+ ec = posCol e
+
+ file :: Doc
+ file = case f of
+ Nothing -> empty
+ Just f -> pretty f <> colon
+
+ start :: Doc
+ start = pretty sl <> comma <> pretty sc
+
+ end :: Doc
+ | sl == el = pretty ec
+ | otherwise = pretty el <> comma <> pretty ec
+
+instance Pretty a => Pretty (Range' (Maybe a)) where
+ pretty r = case rangeToInterval r of
+ Nothing -> empty
+ Just i -> pretty i
+
+instance (Pretty a, HasRange a) => Pretty (PrintRange a) where
+ pretty (PrintRange a) = pretty a <+> parens (text "at" <+> pretty (getRange a))
{--------------------------------------------------------------------------
Functions on postitions and ranges
diff --git a/src/full/Agda/Syntax/Scope/Base.hs b/src/full/Agda/Syntax/Scope/Base.hs
index 34d9e45..184045b 100644
--- a/src/full/Agda/Syntax/Scope/Base.hs
+++ b/src/full/Agda/Syntax/Scope/Base.hs
@@ -1,10 +1,9 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE GADTs #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TupleSections #-}
-
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TupleSections #-}
{-| This module defines the notion of a scope and operations on scopes.
-}
@@ -113,7 +112,7 @@ data LocalVar
-- (List not empty).
deriving (Typeable)
-instance NFData LocalVar
+instance NFData LocalVar where rnf x = seq x ()
instance Eq LocalVar where
(==) = (==) `on` localVar
diff --git a/src/full/Agda/Syntax/Scope/Monad.hs b/src/full/Agda/Syntax/Scope/Monad.hs
index 0b7f399..c4fb90f 100644
--- a/src/full/Agda/Syntax/Scope/Monad.hs
+++ b/src/full/Agda/Syntax/Scope/Monad.hs
@@ -1,5 +1,9 @@
{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ >= 710
+{-# LANGUAGE FlexibleContexts #-}
+#endif
+
{-| The scope monad with operations.
-}
@@ -16,6 +20,8 @@ import Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
+import Data.Set (Set)
+import qualified Data.Set as Set
import Data.Traversable
import Agda.Syntax.Common
@@ -197,29 +203,43 @@ data ResolvedName = VarName A.Name
| ConstructorName [AbstractName]
| PatternSynResName AbstractName
| UnknownName
- deriving (Show)
+ deriving (Show, Eq)
-- | Look up the abstract name referred to by a given concrete name.
resolveName :: C.QName -> ScopeM ResolvedName
-resolveName = resolveName' allKindsOfNames
+resolveName = resolveName' allKindsOfNames Nothing
-- | Look up the abstract name corresponding to a concrete name of
--- a certain kind.
+-- a certain kind and/or from a given set of names.
-- Sometimes we know already that we are dealing with a constructor
-- or pattern synonym (e.g. when we have parsed a pattern).
-- Then, we can ignore conflicting definitions of that name
-- of a different kind. (See issue 822.)
-resolveName' :: [KindOfName] -> C.QName -> ScopeM ResolvedName
-resolveName' kinds x = do
+resolveName' ::
+ [KindOfName] -> Maybe (Set A.Name) -> C.QName -> ScopeM ResolvedName
+resolveName' kinds names x = do
scope <- getScope
- let vars = AssocList.mapKeysMonotonic C.QName $ scopeLocals scope
+ let vars = AssocList.mapKeysMonotonic C.QName $ scopeLocals scope
+ retVar y = return $ VarName $ y { nameConcrete = unqualify x }
+ aName = A.qnameName . anameName
case lookup x vars of
-- Case: we have a local variable x.
- Just (LocalVar y) -> return $ VarName $ y { nameConcrete = unqualify x }
- -- Case: ... but is shadowed by some imports.
- Just (ShadowedVar y ys) -> typeError $ AmbiguousName x $ A.qualify_ y : map anameName ys
+ Just (LocalVar y) -> retVar y
+ -- Case: ... but is (perhaps) shadowed by some imports.
+ Just (ShadowedVar y ys) -> case names of
+ Nothing -> shadowed ys
+ Just ns -> case filter (\y -> aName y `Set.member` ns) ys of
+ [] -> retVar y
+ ys -> shadowed ys
+ where
+ shadowed ys =
+ typeError $ AmbiguousName x $ A.qualify_ y : map anameName ys
-- Case: we do not have a local variable x.
- Nothing -> case filter ((`elem` kinds) . anameKind . fst) $ scopeLookup' x scope of
+ Nothing -> case filter (\y -> anameKind (fst y) `elem` kinds
+ &&
+ maybe True (Set.member (aName (fst y)))
+ names)
+ (scopeLookup' x scope) of
[] -> return UnknownName
ds | all ((==ConName) . anameKind . fst) ds ->
return $ ConstructorName
@@ -243,19 +263,25 @@ resolveModule x = do
[] -> typeError $ NoSuchModule x
ms -> typeError $ AmbiguousModule x (map amodName ms)
--- | Get the fixity of a name. The name is assumed to be in scope.
-getFixity :: C.QName -> ScopeM Fixity'
-getFixity x = do
- r <- resolveName x
+-- | Get the notation of a name. The name is assumed to be in scope.
+getNotation
+ :: C.QName
+ -> Set A.Name
+ -- ^ The name must correspond to one of the names in this set.
+ -> ScopeM NewNotation
+getNotation x ns = do
+ r <- resolveName' allKindsOfNames (Just ns) x
case r of
- VarName y -> return $ nameFixity y
- DefinedName _ d -> return $ aFixity d
- FieldName d -> return $ aFixity d
- ConstructorName ds -> return $ chooseFixity $ map aFixity ds
- PatternSynResName n -> return $ aFixity n
+ VarName y -> return $ namesToNotation x y
+ DefinedName _ d -> return $ notation d
+ FieldName d -> return $ notation d
+ ConstructorName ds -> case mergeNotations $ map notation ds of
+ [n] -> return n
+ _ -> __IMPOSSIBLE__
+ PatternSynResName n -> return $ notation n
UnknownName -> __IMPOSSIBLE__
where
- aFixity = nameFixity . qnameName . anameName
+ notation = namesToNotation x . qnameName . anameName
-- * Binding names
@@ -319,7 +345,7 @@ type WSM = StateT Out ScopeM
-- alternative to qualification by their module).
-- (See Issue 836).
copyScope :: C.QName -> A.ModuleName -> Scope -> ScopeM (Scope, (A.Ren A.ModuleName, A.Ren A.QName))
-copyScope oldc new s = first (inScopeBecause $ Applied oldc) <$> runStateT (copy new s) (Map.empty, Map.empty)
+copyScope oldc new s = first (inScopeBecause $ Applied oldc) <$> runStateT (copy new s) ([], [])
where
-- | A memoizing algorithm, the renamings serving as memo structure.
copy :: A.ModuleName -> Scope -> StateT (A.Ren A.ModuleName, A.Ren A.QName) ScopeM Scope
@@ -351,35 +377,29 @@ copyScope oldc new s = first (inScopeBecause $ Applied oldc) <$> runStateT (copy
_ -> lensAnameName f d
-- Adding to memo structure.
- addName x y = modify $ second $ Map.insert x y
- addMod x y = modify $ first $ Map.insert x y
+ addName x y = modify $ second $ ((x, y):)
+ addMod x y = modify $ first $ ((x, y):)
-- Querying the memo structure.
- findName x = Map.lookup x <$> gets snd
- findMod x = Map.lookup x <$> gets fst
+ findName x = lookup x <$> gets snd
+ findMod x = lookup x <$> gets fst
-- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
renName :: A.QName -> WSM A.QName
renName x = do
- lift $ reportSLn "scope.copy" 50 $ " Copying " ++ show x
- -- If we've seen it already, just return its copy.
- (`fromMaybeM` findName x) $ do
- -- We have not processed this name @x@, so copy it to some @y@.
-- Check whether we have already seen a module of the same name.
-- If yes, use its copy as @y@.
y <- ifJustM (findMod $ qnameToMName x) (return . mnameToQName) $ {- else -} do
-- First time, generate a fresh name for it.
i <- lift fresh
return $ A.qualify new' $ (qnameName x) { nameId = i }
+ lift $ reportSLn "scope.copy" 50 $ " Copying " ++ show x ++ " to " ++ show y
addName x y
return y
-- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
renMod :: A.ModuleName -> WSM A.ModuleName
renMod x = do
- -- If we've seen it already, just return its copy.
- (`fromMaybeM` findMod x) $ do
- -- We have not processed this name @x@, so copy it to some @y@.
-- Check whether we have seen it already, yet as name.
-- If yes, use its copy as @y@.
y <- ifJustM (findName $ mnameToQName x) (return . qnameToMName) $ {- else -} do
diff --git a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
index 31e6675..6653721 100644
--- a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
+++ b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
@@ -1,11 +1,10 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE UndecidableInstances #-}
-- {-# OPTIONS -fwarn-unused-binds #-}
@@ -35,10 +34,11 @@ import Control.Applicative hiding (empty)
import Control.Monad.Reader
import Data.List as List hiding (null)
-import Data.Maybe
import qualified Data.Map as Map
-import qualified Data.Set as Set
+import Data.Maybe
+import Data.Monoid
import Data.Set (Set)
+import qualified Data.Set as Set
import Data.Traversable (traverse)
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg)
@@ -58,9 +58,11 @@ import Agda.TypeChecking.Monad.Base (TCM, NamedMeta(..))
import Agda.TypeChecking.Monad.Options
import qualified Agda.Utils.AssocList as AssocList
+import Agda.Utils.Functor
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Tuple
+import Agda.Utils.Pretty (prettyShow)
#include "undefined.h"
import Agda.Utils.Impossible
@@ -77,14 +79,12 @@ defaultEnv = Env { takenNames = Set.empty
}
makeEnv :: ScopeInfo -> Env
-makeEnv scope = Env { takenNames = taken
+makeEnv scope = Env { takenNames = Set.union vars defs
, currentScope = scope
}
where
- ns = everythingInScope scope
- taken = Set.union vars defs
vars = Set.fromList $ map fst $ scopeLocals scope
- defs = Set.fromList [ x | (x, _) <- Map.toList $ nsNames ns ]
+ defs = Map.keysSet $ nsNames $ everythingInScope scope
currentPrecedence :: AbsToCon Precedence
currentPrecedence = asks $ scopePrecedence . currentScope
@@ -121,37 +121,6 @@ abstractToConcreteCtx ctx x = do
abstractToConcrete_ :: ToConcrete a c => a -> TCM c
abstractToConcrete_ = runAbsToCon . toConcrete
-{-
--- | We make the translation monadic for modularity purposes.
-type AbsToCon = Reader Env
-
-runAbsToCon :: AbsToCon a -> TCM a
-runAbsToCon m = do
- scope <- getScope
- return $ runReader m (makeEnv scope)
-
-abstractToConcreteEnv :: ToConcrete a c => Env -> a -> TCM c
-abstractToConcreteEnv flags a = return $ runReader (toConcrete a) flags
-
-{- Andreas, 2013-02-26 discontinue non-monadic version in favor of debug msg.
-abstractToConcrete :: ToConcrete a c => Env -> a -> c
-abstractToConcrete flags a = runReader (toConcrete a) flags
--}
-
-abstractToConcreteCtx :: ToConcrete a c => Precedence -> a -> TCM c
-abstractToConcreteCtx ctx x = do
- scope <- getScope
- let scope' = scope { scopePrecedence = ctx }
- return $ abstractToConcrete (makeEnv scope') x
- where
- scope = (currentScope defaultEnv) { scopePrecedence = ctx }
-
-abstractToConcrete_ :: ToConcrete a c => a -> TCM c
-abstractToConcrete_ x = do
- scope <- getScope
- return $ abstractToConcrete (makeEnv scope) x
--}
-
-- Dealing with names -----------------------------------------------------
-- | Names in abstract syntax are fully qualified, but the concrete syntax
@@ -287,6 +256,30 @@ toConcreteCtx p x = withPrecedence p $ toConcrete x
bindToConcreteCtx :: ToConcrete a c => Precedence -> a -> (c -> AbsToCon b) -> AbsToCon b
bindToConcreteCtx p x ret = withPrecedence p $ bindToConcrete x ret
+-- | Translate something in the top context.
+toConcreteTop :: ToConcrete a c => a -> AbsToCon c
+toConcreteTop = toConcreteCtx TopCtx
+
+-- | Translate something in the top context.
+bindToConcreteTop :: ToConcrete a c => a -> (c -> AbsToCon b) -> AbsToCon b
+bindToConcreteTop = bindToConcreteCtx TopCtx
+
+-- | Translate something in a context indicated by 'Hiding' info.
+toConcreteHiding :: (LensHiding h, ToConcrete a c) => h -> a -> AbsToCon c
+toConcreteHiding h =
+ case getHiding h of
+ NotHidden -> toConcrete
+ Hidden -> toConcreteTop
+ Instance -> toConcreteTop
+
+-- | Translate something in a context indicated by 'Hiding' info.
+bindToConcreteHiding :: (LensHiding h, ToConcrete a c) => h -> a -> (c -> AbsToCon b) -> AbsToCon b
+bindToConcreteHiding h =
+ case getHiding h of
+ NotHidden -> bindToConcrete
+ Hidden -> bindToConcreteTop
+ Instance -> bindToConcreteTop
+
-- General instances ------------------------------------------------------
instance ToConcrete a c => ToConcrete [a] [c] where
@@ -315,15 +308,19 @@ instance ToConcrete (Common.ArgInfo ac) C.ArgInfo where
return $ info { argInfoColors = [] } -- TODO: zapping ignoring colours
instance ToConcrete a c => ToConcrete (Common.Arg ac a) (C.Arg c) where
- toConcrete (Common.Arg info x) = liftM2 Common.Arg (toConcrete info) (f x)
- where f = case getHiding info of
- Hidden -> toConcreteCtx TopCtx
- Instance -> toConcreteCtx TopCtx
- NotHidden -> toConcrete
+ toConcrete (Common.Arg info x) = Common.Arg
+ <$> toConcrete info
+ <*> toConcreteHiding info x
+
+ bindToConcrete (Common.Arg info x) ret = do
+ info <- toConcrete info
+ bindToConcreteCtx (hiddenArgumentCtx $ getHiding info) x $
+ ret . Common.Arg info
- bindToConcrete (Common.Arg info x) ret = do info <- toConcrete info
- bindToConcreteCtx (hiddenArgumentCtx $ getHiding info) x $
- ret . Common.Arg info
+instance ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) where
+ toConcrete (WithHiding h a) = WithHiding h <$> toConcreteHiding h a
+ bindToConcrete (WithHiding h a) ret = bindToConcreteHiding h a $ \ a ->
+ ret $ WithHiding h a
instance ToConcrete a c => ToConcrete (Named name a) (Named name c) where
toConcrete (Named n x) = Named n <$> toConcrete x
@@ -371,7 +368,7 @@ instance ToConcrete A.Expr C.Expr where
toConcrete (A.Underscore i) = return $
C.Underscore (getRange i) $
- show . NamedMeta (metaNameSuggestion i) . MetaId <$> metaNumber i
+ prettyShow . NamedMeta (metaNameSuggestion i) . MetaId <$> metaNumber i
toConcrete e@(A.App i e1 e2) =
tryToRecoverOpApp e
@@ -394,7 +391,7 @@ instance ToConcrete A.Expr C.Expr where
$ case lamView e of
(bs, e) ->
bindToConcrete (map makeDomainFree bs) $ \bs -> do
- e <- toConcreteCtx TopCtx e
+ e <- toConcreteTop e
return $ C.Lam (getRange i) (concat bs) e
where
lamView (A.Lam _ b@(A.DomainFree _ _) e) =
@@ -438,7 +435,7 @@ instance ToConcrete A.Expr C.Expr where
(tel, e) ->
bracket piBrackets
$ bindToConcrete tel $ \b' -> do
- e' <- toConcreteCtx TopCtx e
+ e' <- toConcreteTop e
return $ C.Pi (concat b') e'
where
piTel (A.Pi _ tel e) = (tel ++) -*- id $ piTel e
@@ -447,7 +444,7 @@ instance ToConcrete A.Expr C.Expr where
toConcrete (A.Fun i a b) =
bracket piBrackets
$ do a' <- toConcreteCtx (if irr then DotPatternCtx else FunctionSpaceDomainCtx) a
- b' <- toConcreteCtx TopCtx b
+ b' <- toConcreteTop b
return $ C.Fun (getRange i) (addRel a' $ mkArg a') b'
where
irr = getRelevance a `elem` [Irrelevant, NonStrict]
@@ -468,20 +465,20 @@ instance ToConcrete A.Expr C.Expr where
toConcrete (A.Let i ds e) =
bracket lamBrackets
$ bindToConcrete ds $ \ds' -> do
- e' <- toConcreteCtx TopCtx e
+ e' <- toConcreteTop e
return $ C.Let (getRange i) (concat ds') e'
toConcrete (A.Rec i fs) =
bracket appBrackets $ do
let (xs, es) = unzip fs
- es <- toConcreteCtx TopCtx es
+ es <- toConcreteTop es
return $ C.Rec (getRange i) $ zip xs es
toConcrete (A.RecUpdate i e fs) =
bracket appBrackets $ do
let (xs, es) = unzip fs
e <- toConcrete e
- es <- toConcreteCtx TopCtx es
+ es <- toConcreteTop es
return $ C.RecUpdate (getRange i) e $ zip xs es
toConcrete (A.ETel tel) = do
@@ -508,7 +505,7 @@ instance ToConcrete A.Expr C.Expr where
-- Andreas, 2010-10-05 print irrelevant things as ordinary things
toConcrete (A.DontCare e) = C.Dot r . C.Paren r <$> toConcrete e
where r = getRange e
--- toConcrete (A.DontCare e) = C.DontCare <$> toConcreteCtx TopCtx e
+-- toConcrete (A.DontCare e) = C.DontCare <$> toConcreteTop e
{-
-- Andreas, 2010-09-21 abuse C.Underscore to print irrelevant things
toConcrete (A.DontCare) = return $ C.Underscore noRange Nothing
@@ -516,9 +513,9 @@ instance ToConcrete A.Expr C.Expr where
toConcrete (A.PatternSyn n) = C.Ident <$> toConcrete n
makeDomainFree :: A.LamBinding -> A.LamBinding
-makeDomainFree b@(A.DomainFull (A.TypedBindings r (Common.Arg info (A.TBind _ [x] t)))) =
+makeDomainFree b@(A.DomainFull (A.TypedBindings r (Common.Arg info (A.TBind _ [WithHiding h x] t)))) =
case unScope t of
- A.Underscore MetaInfo{metaNumber = Nothing} -> A.DomainFree info x
+ A.Underscore MetaInfo{metaNumber = Nothing} -> A.DomainFree (mapHiding (mappend h) info) x
_ -> b
makeDomainFree b = b
@@ -547,20 +544,20 @@ instance ToConcrete A.TypedBindings [C.TypedBindings] where
tbinds r e xs = [ C.TBind r xs e ]
tbind r e xs =
- case span (\x -> boundLabel x == boundName x) xs of
+ case span ((\ x -> boundLabel x == boundName x) . dget) xs of
(xs, x:ys) -> tbinds r e xs ++ [ C.TBind r [x] e ] ++ tbind r e ys
(xs, []) -> tbinds r e xs
- label x y = y { boundLabel = nameConcrete x }
+ label x = fmap $ \ y -> y { boundLabel = nameConcrete $ dget x }
instance ToConcrete A.TypedBinding C.TypedBinding where
bindToConcrete (A.TBind r xs e) ret =
- bindToConcrete xs $ \xs -> do
- e <- toConcreteCtx TopCtx e
- ret (C.TBind r (map mkBoundName_ xs) e)
+ bindToConcrete xs $ \ xs -> do
+ e <- toConcreteTop e
+ ret $ C.TBind r (map (fmap mkBoundName_) xs) e
bindToConcrete (A.TLet r lbs) ret =
- bindToConcrete lbs $ \ds -> do
- ret (C.TLet r (concat ds))
+ bindToConcrete lbs $ \ ds -> do
+ ret $ C.TLet r $ concat ds
instance ToConcrete LetBinding [C.Declaration] where
bindToConcrete (LetBind i info x t e) ret =
@@ -637,12 +634,12 @@ instance ToConcrete A.RHS (C.RHS, [C.Expr], [C.Expr], [C.Declaration]) where
es <- toConcrete es
cs <- concat <$> toConcrete cs
return (C.AbsurdRHS, [], es, cs)
- toConcrete (A.RewriteRHS _ eqs rhs wh) = do
+ toConcrete (A.RewriteRHS xeqs rhs wh) = do
wh <- declsToConcrete wh
(rhs, eqs', es, whs) <- toConcrete rhs
unless (null eqs')
__IMPOSSIBLE__
- eqs <- toConcrete eqs
+ eqs <- toConcrete $ map snd xeqs
return (rhs, eqs, es, wh ++ whs)
instance ToConcrete (Maybe A.QName) (Maybe C.Name) where
@@ -669,7 +666,7 @@ instance ToConcrete (Constr A.Constructor) C.Declaration where
withScope scope $ toConcrete (Constr d)
toConcrete (Constr (A.Axiom _ i info x t)) = do
x' <- unsafeQNameToName <$> toConcrete x
- t' <- toConcreteCtx TopCtx t
+ t' <- toConcreteTop t
info <- toConcrete info
return $ C.TypeSig info x' t'
toConcrete (Constr d) = head <$> toConcrete d
@@ -680,7 +677,7 @@ instance ToConcrete a C.LHS => ToConcrete (A.Clause' a) [C.Declaration] where
case lhs of
C.LHS p wps _ _ -> do
bindToConcrete (AsWhereDecls wh) $ \wh' -> do
- (rhs', eqs, with, wcs) <- toConcreteCtx TopCtx rhs
+ (rhs', eqs, with, wcs) <- toConcreteTop rhs
return $ FunClause (C.LHS p wps eqs with) rhs' wh' : wcs
C.Ellipsis {} -> __IMPOSSIBLE__
-- TODO: Is the case above impossible? Previously there was
@@ -691,9 +688,10 @@ instance ToConcrete A.ModuleApplication C.ModuleApplication where
toConcrete (A.SectionApp tel y es) = do
y <- toConcreteCtx FunctionCtx y
bindToConcrete tel $ \tel -> do
- es <- toConcreteCtx ArgumentCtx es
- let r = fuseRange y es
- return $ C.SectionApp r (concat tel) (foldl (C.App r) (C.Ident y) es)
+ es <- toConcreteCtx ArgumentCtx es
+ let r = fuseRange y es
+ return $ C.SectionApp r (concat tel) (foldl (C.App r) (C.Ident y) es)
+
toConcrete (A.RecordModuleIFS recm) = do
recm <- toConcrete recm
return $ C.RecordModuleIFS (getRange recm) recm
@@ -706,7 +704,7 @@ instance ToConcrete A.Declaration [C.Declaration] where
x' <- unsafeQNameToName <$> toConcrete x
withAbstractPrivate i $
withInfixDecl i x' $ do
- t' <- toConcreteCtx TopCtx t
+ t' <- toConcreteTop t
info <- toConcrete info
return [C.Postulate (getRange i) [C.TypeSig info x' t']]
@@ -714,14 +712,14 @@ instance ToConcrete A.Declaration [C.Declaration] where
x' <- unsafeQNameToName <$> toConcrete x
withAbstractPrivate i $
withInfixDecl i x' $ do
- t' <- toConcreteCtx TopCtx t
+ t' <- toConcreteTop t
return [C.Field x' t']
toConcrete (A.Primitive i x t) = do
x' <- unsafeQNameToName <$> toConcrete x
withAbstractPrivate i $
withInfixDecl i x' $ do
- t' <- toConcreteCtx TopCtx t
+ t' <- toConcreteTop t
return [C.Primitive (getRange i) [C.TypeSig defaultArgInfo x' t']]
-- Primitives are always relevant.
@@ -732,7 +730,7 @@ instance ToConcrete A.Declaration [C.Declaration] where
withAbstractPrivate i $
bindToConcrete bs $ \tel' -> do
x' <- unsafeQNameToName <$> toConcrete x
- t' <- toConcreteCtx TopCtx t
+ t' <- toConcreteTop t
return [ C.DataSig (getRange i) Inductive x' (map C.DomainFull $ concat tel') t' ]
toConcrete (A.DataDef i x bs cs) =
@@ -745,7 +743,7 @@ instance ToConcrete A.Declaration [C.Declaration] where
withAbstractPrivate i $
bindToConcrete bs $ \tel' -> do
x' <- unsafeQNameToName <$> toConcrete x
- t' <- toConcreteCtx TopCtx t
+ t' <- toConcreteTop t
return [ C.RecordSig (getRange i) x' (map C.DomainFull $ concat tel') t' ]
toConcrete (A.RecDef i x ind c bs t cs) =
@@ -759,8 +757,8 @@ instance ToConcrete A.Declaration [C.Declaration] where
toConcrete (A.Section i x tel ds) = do
x <- toConcrete x
bindToConcrete tel $ \tel -> do
- ds <- declsToConcrete ds
- return [ C.Module (getRange i) x (concat tel) ds ]
+ ds <- declsToConcrete ds
+ return [ C.Module (getRange i) x (concat tel) ds ]
toConcrete (A.Apply i x modapp _ _) = do
x <- unsafeQNameToName <$> toConcrete x
@@ -796,36 +794,32 @@ instance ToConcrete A.Declaration [C.Declaration] where
data RangeAndPragma = RangeAndPragma Range A.Pragma
instance ToConcrete RangeAndPragma C.Pragma where
- toConcrete (RangeAndPragma r p) = case p of
- A.OptionsPragma xs -> return $ C.OptionsPragma r xs
- A.BuiltinPragma b x -> do
- x <- toConcrete x
- return $ C.BuiltinPragma r b x
- A.RewritePragma x -> do
- x <- toConcrete x
- return $ C.RewritePragma r x
- A.CompiledTypePragma x hs -> do
- x <- toConcrete x
- return $ C.CompiledTypePragma r x hs
- A.CompiledDataPragma x hs hcs -> do
- x <- toConcrete x
- return $ C.CompiledDataPragma r x hs hcs
- A.CompiledPragma x hs -> do
- x <- toConcrete x
- return $ C.CompiledPragma r x hs
- A.CompiledExportPragma x hs -> do
- x <- toConcrete x
- return $ C.CompiledExportPragma r x hs
- A.CompiledEpicPragma x e -> do
- x <- toConcrete x
- return $ C.CompiledEpicPragma r x e
- A.CompiledJSPragma x e -> do
- x <- toConcrete x
- return $ C.CompiledJSPragma r x e
- A.StaticPragma x -> do
- x <- toConcrete x
- return $ C.StaticPragma r x
- A.EtaPragma x -> C.EtaPragma r <$> toConcrete x
+ toConcrete (RangeAndPragma r p) = case p of
+ A.OptionsPragma xs -> return $ C.OptionsPragma r xs
+ A.BuiltinPragma b e -> C.BuiltinPragma r b <$> toConcrete e
+ A.BuiltinNoDefPragma b x -> C.BuiltinPragma r b . C.Ident <$>
+ toConcrete x
+ A.RewritePragma x -> C.RewritePragma r <$> toConcrete x
+ A.CompiledTypePragma x hs -> do
+ x <- toConcrete x
+ return $ C.CompiledTypePragma r x hs
+ A.CompiledDataPragma x hs hcs -> do
+ x <- toConcrete x
+ return $ C.CompiledDataPragma r x hs hcs
+ A.CompiledPragma x hs -> do
+ x <- toConcrete x
+ return $ C.CompiledPragma r x hs
+ A.CompiledExportPragma x hs -> do
+ x <- toConcrete x
+ return $ C.CompiledExportPragma r x hs
+ A.CompiledEpicPragma x e -> do
+ x <- toConcrete x
+ return $ C.CompiledEpicPragma r x e
+ A.CompiledJSPragma x e -> do
+ x <- toConcrete x
+ return $ C.CompiledJSPragma r x e
+ A.StaticPragma x -> C.StaticPragma r <$> toConcrete x
+ A.EtaPragma x -> C.EtaPragma r <$> toConcrete x
-- Left hand sides --------------------------------------------------------
@@ -847,28 +841,9 @@ instance ToConcrete A.LHS C.LHS where
bindToConcreteCtx TopCtx lhscore $ \lhs ->
bindToConcreteCtx TopCtx (noImplicitPats wps) $ \wps ->
ret $ C.LHS lhs wps [] []
-{-
- bindToConcrete (A.LHS i (A.LHSHead x args) wps) ret = do
- bindToConcreteCtx TopCtx (A.DefP info x args) $ \lhs ->
- bindToConcreteCtx TopCtx (noImplicitPats wps) $ \wps ->
- ret $ C.LHS lhs wps [] []
- where info = PatRange (getRange i)
--}
instance ToConcrete A.LHSCore C.Pattern where
bindToConcrete = bindToConcrete . lhsCoreToPattern
-{-
- bindToConcrete (A.LHSHead x args) ret = do
- bindToConcreteCtx TopCtx (A.DefP info x args) $ \ lhs ->
- ret $ lhs
- where info = PatRange noRange -- seems to be unused anyway
- bindToConcrete (A.LHSProj d ps1 lhscore ps2) ret = do
- d <- toConcrete d
- bindToConcrete ps1 $ \ ps1 ->
- bindToConcrete lhscore $ \ p ->
- bindToConcrete ps2 $ \ ps2 ->
- ret $ makePattern d ps1 p ps2
- -}
appBrackets' :: [arg] -> Precedence -> Bool
appBrackets' [] _ = False
@@ -912,8 +887,9 @@ instance ToConcrete A.Pattern C.Pattern where
data Hd = HdVar A.Name | HdCon A.QName | HdDef A.QName
-cOpApp :: Range -> C.QName -> [C.Expr] -> C.Expr
-cOpApp r n es = C.OpApp r n (map (defaultNamedArg . Ordinary) es)
+cOpApp :: Range -> C.QName -> A.Name -> [C.Expr] -> C.Expr
+cOpApp r x n es =
+ C.OpApp r x (Set.singleton n) (map (defaultNamedArg . Ordinary) es)
tryToRecoverOpApp :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr
tryToRecoverOpApp e def = recoverOpApp bracket cOpApp view e def
@@ -930,7 +906,9 @@ tryToRecoverOpApp e def = recoverOpApp bracket cOpApp view e def
tryToRecoverOpAppP :: A.Pattern -> AbsToCon C.Pattern -> AbsToCon C.Pattern
tryToRecoverOpAppP p def = recoverOpApp bracketP_ opApp view p def
where
- opApp r x ps = C.OpAppP r x (map defaultNamedArg ps)
+ opApp r x n ps =
+ C.OpAppP r x (Set.singleton n) (map defaultNamedArg ps)
+
view p = case p of
ConP _ (AmbQ (c:_)) ps -> Just (HdCon c, ps)
DefP _ f ps -> Just (HdDef f, ps)
@@ -938,7 +916,7 @@ tryToRecoverOpAppP p def = recoverOpApp bracketP_ opApp view p def
recoverOpApp :: (ToConcrete a c, HasRange c)
=> ((Precedence -> Bool) -> AbsToCon c -> AbsToCon c)
- -> (Range -> C.QName -> [c] -> c)
+ -> (Range -> C.QName -> A.Name -> [c] -> c)
-> (a -> Maybe (Hd, [A.NamedArg a]))
-> a
-> AbsToCon c
@@ -959,19 +937,20 @@ recoverOpApp bracket opApp view e mDefault = case view e of
doQNameHelper fixityHelper conHelper n as = do
x <- toConcrete n
- doQName (theFixity $ nameFixity $ fixityHelper n) (conHelper x) as
+ doQName (theFixity $ nameFixity n') (conHelper x) n' as
+ where n' = fixityHelper n
-- fall-back (wrong number of arguments or no holes)
- doQName _ n es
+ doQName _ x _ es
| length xs == 1 = mDefault
| length es /= numHoles = mDefault
| null es = mDefault
where
- xs = C.nameParts $ C.unqualify n
+ xs = C.nameParts $ C.unqualify x
numHoles = length (filter (== Hole) xs)
-- binary case
- doQName fixity n as
+ doQName fixity x n as
| Hole <- head xs
, Hole <- last xs = do
let a1 = head as
@@ -983,12 +962,12 @@ recoverOpApp bracket opApp view e mDefault = case view e of
es <- mapM (toConcreteCtx InsideOperandCtx) as'
en <- toConcreteCtx (RightOperandCtx fixity) an
bracket (opBrackets fixity)
- $ return $ opApp (getRange (e1, en)) n ([e1] ++ es ++ [en])
+ $ return $ opApp (getRange (e1, en)) x n ([e1] ++ es ++ [en])
where
- xs = C.nameParts $ C.unqualify n
+ xs = C.nameParts $ C.unqualify x
-- prefix
- doQName fixity n as
+ doQName fixity x n as
| Hole <- last xs = do
let an = last as
as' = case as of
@@ -997,24 +976,24 @@ recoverOpApp bracket opApp view e mDefault = case view e of
es <- mapM (toConcreteCtx InsideOperandCtx) as'
en <- toConcreteCtx (RightOperandCtx fixity) an
bracket (opBrackets fixity)
- $ return $ opApp (getRange (n, en)) n (es ++ [en])
+ $ return $ opApp (getRange (n, en)) x n (es ++ [en])
where
- xs = C.nameParts $ C.unqualify n
+ xs = C.nameParts $ C.unqualify x
-- postfix
- doQName fixity n as
+ doQName fixity x n as
| Hole <- head xs = do
let a1 = head as
as' = tail as
e1 <- toConcreteCtx (LeftOperandCtx fixity) a1
es <- mapM (toConcreteCtx InsideOperandCtx) as'
bracket (opBrackets fixity)
- $ return $ opApp (getRange (e1, n)) n ([e1] ++ es)
+ $ return $ opApp (getRange (e1, n)) x n ([e1] ++ es)
where
- xs = C.nameParts $ C.unqualify n
+ xs = C.nameParts $ C.unqualify x
-- roundfix
- doQName _ n as = do
+ doQName _ x n as = do
es <- mapM (toConcreteCtx InsideOperandCtx) as
bracket roundFixBrackets
- $ return $ opApp (getRange n) n es
+ $ return $ opApp (getRange x) x n es
diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
index 2c0fd75..16b3f05 100644
--- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -1,12 +1,16 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DoAndIfThenElse #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverlappingInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if __GLASGOW_HASKELL__ <= 708
+{-# LANGUAGE OverlappingInstances #-}
+#endif
{-| Translation from "Agda.Syntax.Concrete" to "Agda.Syntax.Abstract". Involves scope analysis,
figuring out infix operator precedences and tidying up definitions.
@@ -34,6 +38,8 @@ import Control.Monad.Reader hiding (mapM)
import Data.Foldable (Foldable, traverse_)
import Data.Traversable (mapM, traverse)
import Data.List ((\\), nub, foldl')
+import Data.Set (Set)
+import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe
@@ -41,6 +47,7 @@ import Agda.Syntax.Concrete as C hiding (topLevelModuleName)
import Agda.Syntax.Concrete.Generic
import Agda.Syntax.Concrete.Operators
import Agda.Syntax.Abstract as A
+import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
@@ -52,11 +59,12 @@ import Agda.Syntax.Notation
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
-import Agda.TypeChecking.Monad.Base (TypeError(..), Call(..), typeError,
- TCErr(..), extendedLambdaName, fresh,
- freshName, freshName_, freshNoName)
-import Agda.TypeChecking.Monad.Benchmark (billTo, billTop, reimburseTop)
+import Agda.TypeChecking.Monad.Base
+ ( TypeError(..) , Call(..) , typeError , genericError , TCErr(..)
+ , fresh , freshName , freshName_ , freshNoName , extendedLambdaName
+ )
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
+import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Trace (traceCall, setCurrentRange)
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.MetaVars (registerInteractionPoint)
@@ -124,11 +132,6 @@ annotateExpr m = do
s <- getScope
return $ ScopedExpr s e
-expandEllipsis :: C.Pattern -> [C.Pattern] -> C.Clause -> C.Clause
-expandEllipsis _ _ c@(C.Clause _ C.LHS{} _ _ _) = c
-expandEllipsis p ps (C.Clause x (C.Ellipsis _ ps' eqs es) rhs wh wcs) =
- C.Clause x (C.LHS p (ps ++ ps') eqs es) rhs wh wcs
-
-- | Make sure that each variable occurs only once.
checkPatternLinearity :: [A.Pattern' e] -> ScopeM ()
checkPatternLinearity ps = unlessNull (duplicates xs) $ \ ys -> do
@@ -170,7 +173,7 @@ recordConstructorType fields = build fs
build (NiceModuleMacro r p x modapp open dir{ publicOpen = False } : fs)
build (NiceField r f _ _ x (Common.Arg info e) : fs) =
- C.Pi [C.TypedBindings r $ Common.Arg info (C.TBind r [mkBoundName x f] e)] $ build fs
+ C.Pi [C.TypedBindings r $ Common.Arg info (C.TBind r [pure $ mkBoundName x f] e)] $ build fs
where r = getRange x
build (d : fs) = C.Let (getRange d) [notSoNiceDeclaration d] $
build fs
@@ -302,6 +305,12 @@ toAbstractCtx :: ToAbstract concrete abstract =>
Precedence -> concrete -> ScopeM abstract
toAbstractCtx ctx c = withContextPrecedence ctx $ toAbstract c
+toAbstractTopCtx :: ToAbstract c a => c -> ScopeM a
+toAbstractTopCtx = toAbstractCtx TopCtx
+
+toAbstractHiding :: (LensHiding h, ToAbstract c a) => h -> c -> ScopeM a
+toAbstractHiding h = toAbstractCtx $ hiddenArgumentCtx $ getHiding h
+
setContextCPS :: Precedence -> (a -> ScopeM b) ->
((a -> ScopeM b) -> ScopeM b) -> ScopeM b
setContextCPS p ret f = do
@@ -325,8 +334,7 @@ localToAbstract' x ret = do
withScope scope $ ret =<< toAbstract x
instance (ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (c1,c2) (a1,a2) where
- toAbstract (x,y) =
- (,) <$> toAbstract x <*> toAbstract y
+ toAbstract (x,y) = (,) <$> toAbstract x <*> toAbstract y
instance (ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) =>
ToAbstract (c1,c2,c3) (a1,a2,a3) where
@@ -334,19 +342,26 @@ instance (ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) =>
where
flatten (x,(y,z)) = (x,y,z)
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPABLE #-} ToAbstract c a => ToAbstract [c] [a] where
+#else
instance ToAbstract c a => ToAbstract [c] [a] where
- toAbstract = mapM toAbstract
+#endif
+ toAbstract = mapM toAbstract
instance ToAbstract c a => ToAbstract (Maybe c) (Maybe a) where
- toAbstract Nothing = return Nothing
- toAbstract (Just x) = Just <$> toAbstract x
+ toAbstract = traverse toAbstract
-- Names ------------------------------------------------------------------
newtype NewName a = NewName a
-newtype OldQName = OldQName C.QName
+data OldQName = OldQName C.QName (Maybe (Set A.Name))
+ -- ^ If a set is given, then the first name must correspond to one
+ -- of the names in the set.
newtype OldName = OldName C.Name
-newtype PatName = PatName C.QName
+data PatName = PatName C.QName (Maybe (Set A.Name))
+ -- ^ If a set is given, then the first name must correspond to one
+ -- of the names in the set.
instance ToAbstract (NewName C.Name) A.Name where
toAbstract (NewName x) = do
@@ -371,8 +386,8 @@ nameExpr d = mk (anameKind d) $ anameName d
where i = ExprRange (getRange x)
instance ToAbstract OldQName A.Expr where
- toAbstract (OldQName x) = do
- qx <- resolveName x
+ toAbstract (OldQName x ns) = do
+ qx <- resolveName' allKindsOfNames ns x
reportSLn "scope.name" 10 $ "resolved " ++ show x ++ ": " ++ show qx
case qx of
VarName x' -> return $ A.Var x'
@@ -387,9 +402,11 @@ data APatName = VarPatName A.Name
| PatternSynPatName AbstractName
instance ToAbstract PatName APatName where
- toAbstract (PatName x) = do
+ toAbstract (PatName x ns) = do
reportSLn "scope.pat" 10 $ "checking pattern name: " ++ show x
- rx <- resolveName' [ConName, PatternSynName] x -- Andreas, 2013-03-21 ignore conflicting names which cannot be meant since we are in a pattern
+ rx <- resolveName' [ConName, PatternSynName] ns x
+ -- Andreas, 2013-03-21 ignore conflicting names which cannot
+ -- be meant since we are in a pattern
z <- case (rx, x) of
-- TODO: warn about shadowing
(VarName y, C.QName x) -> return $ Left x -- typeError $ RepeatedVariableInPattern y x
@@ -398,9 +415,7 @@ instance ToAbstract PatName APatName where
(UnknownName, C.QName x) -> return $ Left x
(ConstructorName ds, _) -> return $ Right (Left ds)
(PatternSynResName d, _) -> return $ Right (Right d)
- _ ->
- typeError $ GenericError $
- "Cannot pattern match on " ++ show x ++ ", because it is not a constructor"
+ _ -> genericError $ "Cannot pattern match on non-constructor " ++ prettyShow x
case z of
Left x -> do
reportSLn "scope.pat" 10 $ "it was a var: " ++ show x
@@ -436,7 +451,7 @@ checkForModuleClash x = do
ms <- scopeLookup (C.QName x) <$> getScope
unless (null ms) $ do
reportSLn "scope.clash" 20 $ "clashing modules ms = " ++ show ms
- setCurrentRange (getRange x) $
+ setCurrentRange x $
typeError $ ShadowedModule x $
map ((`withRangeOf` x) . amodName) ms
@@ -460,7 +475,8 @@ instance ToAbstract NewModuleQName A.ModuleName where
toAbs m' q
instance ToAbstract OldModuleName A.ModuleName where
- toAbstract (OldModuleName q) = amodName <$> resolveModule q
+ toAbstract (OldModuleName q) = setCurrentRange q $ do
+ amodName <$> resolveModule q
-- Expressions ------------------------------------------------------------
@@ -518,7 +534,7 @@ toAbstractLam r bs e ctx = do
e <- toAbstractCtx ctx e
-- We have at least one binder. Get first @b@ and rest @bs@.
caseList bs __IMPOSSIBLE__ $ \ b bs -> do
- return $ A.Lam (ExprRange r) b $ foldr mkLam e bs
+ return $ A.Lam (ExprRange r) b $ foldr mkLam e bs
where
mkLam b e = A.Lam (ExprRange $ fuseRange b e) b e
@@ -526,7 +542,7 @@ toAbstractLam r bs e ctx = do
scopeCheckExtendedLam :: Range -> [(C.LHS, C.RHS, WhereClause)] -> ScopeM A.Expr
scopeCheckExtendedLam r cs = do
whenM isInsideDotPattern $
- typeError $ GenericError "Extended lambdas are not allowed in dot patterns"
+ genericError "Extended lambdas are not allowed in dot patterns"
-- Find an unused name for the extended lambda definition.
cname <- nextlamname r 0 extendedLambdaName
@@ -570,7 +586,7 @@ instance ToAbstract C.Expr A.Expr where
traceCall (ScopeCheckExpr e) $ annotateExpr $ case e of
-- Names
- Ident x -> toAbstract (OldQName x)
+ Ident x -> toAbstract (OldQName x Nothing)
-- Literals
C.Lit l -> return $ A.Lit l
@@ -598,8 +614,7 @@ instance ToAbstract C.Expr A.Expr where
-- Raw application
C.RawApp r es -> do
- e <- reimburseTop Bench.Scoping $ billTo [Bench.Parsing, Bench.Operators] $
- parseApplication es
+ e <- parseApplication es
toAbstract e
-- Application
@@ -609,7 +624,7 @@ instance ToAbstract C.Expr A.Expr where
return $ A.App (ExprRange r) e1 e2
-- Operator application
- C.OpApp r op es -> toAbstractOpApp op es
+ C.OpApp r op ns es -> toAbstractOpApp op ns es
-- With application
C.WithApp r e es -> do
@@ -652,7 +667,7 @@ instance ToAbstract C.Expr A.Expr where
-- Let
e0@(C.Let _ ds e) ->
- ifM isInsideDotPattern (typeError $ GenericError $ "Let-expressions are not allowed in dot patterns") $
+ ifM isInsideDotPattern (genericError $ "Let-expressions are not allowed in dot patterns") $
localToAbstract (LetDefs ds) $ \ds' -> do
e <- toAbstractCtx TopCtx e
let info = ExprRange (getRange e0)
@@ -681,7 +696,7 @@ instance ToAbstract C.Expr A.Expr where
-- Impossible things
C.ETel _ -> __IMPOSSIBLE__
- C.Equal{} -> typeError $ GenericError "Parse error: unexpected '='"
+ C.Equal{} -> genericError "Parse error: unexpected '='"
-- Quoting
C.QuoteGoal _ x e -> do
@@ -713,7 +728,7 @@ instance ToAbstract C.LamBinding A.LamBinding where
makeDomainFull :: C.LamBinding -> C.TypedBindings
makeDomainFull (C.DomainFull b) = b
makeDomainFull (C.DomainFree info x) =
- C.TypedBindings r $ Common.Arg info $ C.TBind r [x] $ C.Underscore r Nothing
+ C.TypedBindings r $ Common.Arg info $ C.TBind r [pure x] $ C.Underscore r Nothing
where r = getRange x
instance ToAbstract C.TypedBindings A.TypedBindings where
@@ -722,11 +737,9 @@ instance ToAbstract C.TypedBindings A.TypedBindings where
instance ToAbstract C.TypedBinding A.TypedBinding where
toAbstract (C.TBind r xs t) = do
t' <- toAbstractCtx TopCtx t
- xs' <- toAbstract (map NewName xs)
+ xs' <- toAbstract $ map (fmap NewName) xs
return $ A.TBind r xs' t'
- toAbstract (C.TLet r ds) = do
- ds' <- toAbstract (LetDefs ds)
- return $ A.TLet r ds'
+ toAbstract (C.TLet r ds) = A.TLet r <$> toAbstract (LetDefs ds)
-- | Scope check a module (top level function).
--
@@ -915,10 +928,14 @@ instance ToAbstract (TopLevel [C.Declaration]) TopLevelInfo where
-- | runs Syntax.Concrete.Definitions.niceDeclarations on main module
niceDecls :: [C.Declaration] -> ScopeM [NiceDeclaration]
niceDecls ds = case runNice $ niceDeclarations ds of
- Left e -> throwError $ Exception (getRange e) (show e)
+ Left e -> throwError $ Exception (getRange e) $ pretty e
Right ds -> return ds
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPING #-} ToAbstract [C.Declaration] [A.Declaration] where
+#else
instance ToAbstract [C.Declaration] [A.Declaration] where
+#endif
toAbstract ds = do
-- don't allow to switch off termination checker in --safe mode
ds <- ifM (optSafe <$> commandLineOptions) (mapM noNoTermCheck ds) (return ds)
@@ -944,9 +961,9 @@ instance ToAbstract LetDef [A.LetBinding] where
case d of
NiceMutual _ _ d@[C.FunSig _ fx _ instanc info _ x t, C.FunDef _ _ _ abstract _ _ [cl]] ->
do when (abstract == AbstractDef) $ do
- typeError $ GenericError $ "abstract not allowed in let expressions"
+ genericError $ "abstract not allowed in let expressions"
when (instanc == InstanceDef) $ do
- typeError $ GenericError $ "Using instance is useless here, let expressions are always eligible for instance search."
+ genericError $ "Using instance is useless here, let expressions are always eligible for instance search."
e <- letToAbstract cl
t <- toAbstract t
x <- toAbstract (NewName $ mkBoundName x fx)
@@ -955,7 +972,10 @@ instance ToAbstract LetDef [A.LetBinding] where
-- irrefutable let binding, like (x , y) = rhs
NiceFunClause r PublicAccess ConcreteDef termCheck d@(C.FunClause lhs@(C.LHS p [] [] []) (C.RHS rhs) NoWhere) -> do
- mp <- setCurrentRange (getRange p) $ (Right <$> parsePattern p) `catchError` (return . Left)
+ mp <- setCurrentRange p $
+ (Right <$> parsePattern p)
+ `catchError`
+ (return . Left)
case mp of
Right p -> do
rhs <- toAbstract rhs
@@ -1015,10 +1035,10 @@ instance ToAbstract LetDef [A.LetBinding] where
localToAbstract (snd $ lhsArgs p) $ \args ->
-}
(x, args) <- do
- res <- setCurrentRange (getRange p) $ parseLHS top p
+ res <- setCurrentRange p $ parseLHS top p
case res of
C.LHSHead x args -> return (x, args)
- C.LHSProj{} -> typeError $ GenericError $ "copatterns not allowed in let bindings"
+ C.LHSProj{} -> genericError $ "copatterns not allowed in let bindings"
localToAbstract args $ \args ->
do rhs <- toAbstract rhs
@@ -1060,7 +1080,7 @@ instance ToAbstract NiceDeclaration A.Declaration where
-- Fields
C.NiceField r f p a x t -> do
- unless (p == PublicAccess) $ typeError $ GenericError "Record fields can not be private"
+ unless (p == PublicAccess) $ genericError "Record fields can not be private"
-- Interaction points for record fields have already been introduced
-- when checking the type of the record constructor.
-- To avoid introducing interaction points (IP) twice, we turn
@@ -1121,7 +1141,7 @@ instance ToAbstract NiceDeclaration A.Declaration where
-- Uncategorized function clauses
C.NiceFunClause r acc abs termCheck (C.FunClause lhs rhs wcls) ->
- typeError $ GenericError $
+ genericError $
"Missing type signature for left hand side " ++ show lhs
C.NiceFunClause{} -> __IMPOSSIBLE__
@@ -1134,7 +1154,7 @@ instance ToAbstract NiceDeclaration A.Declaration where
dups = nub $ cs \\ nub cs
bad = filter (`elem` dups) cs
unless (distinct cs) $
- setCurrentRange (getRange bad) $
+ setCurrentRange bad $
typeError $ DuplicateConstructors dups
pars <- toAbstract pars
@@ -1186,7 +1206,7 @@ instance ToAbstract NiceDeclaration A.Declaration where
scopeCheckNiceModule r p name tel $ toAbstract ds
NiceModule _ _ _ m@C.Qual{} _ _ ->
- typeError $ GenericError $ "Local modules cannot have qualified names"
+ genericError $ "Local modules cannot have qualified names"
NiceModuleMacro r p x modapp open dir ->
checkModuleMacro Apply r p x modapp open dir
@@ -1209,7 +1229,7 @@ instance ToAbstract NiceDeclaration A.Declaration where
ps <- toAbstract p
return $ map (A.Pragma r) ps
- NiceImport r x as open dir -> traceCall (SetRange r) $ do
+ NiceImport r x as open dir -> setCurrentRange r $ do
notPublicWithoutOpen open dir
-- First scope check the imported module and return its name and
@@ -1254,13 +1274,13 @@ instance ToAbstract NiceDeclaration A.Declaration where
}
return [ A.Import minfo m ]
- NiceUnquoteDecl r fx p a tc x e -> do
+ NiceUnquoteDecl r fx p i a tc x e -> do
y <- freshAbstractQName fx x
bindName p QuotableName x y
e <- toAbstract e
rebindName p DefName x y
let mi = MutualInfo tc r
- return [A.UnquoteDecl mi (mkDefInfo x fx p a r) y e]
+ return [A.UnquoteDecl mi (mkDefInfoInstance x fx p a i r) y e]
NicePatternSyn r fx n as p -> do
reportSLn "scope.pat" 10 $ "found nice pattern syn: " ++ show r
@@ -1328,81 +1348,100 @@ instance ToAbstract C.Pragma [A.Pragma] where
toAbstract (C.ImpossiblePragma _) = impossibleTest
toAbstract (C.OptionsPragma _ opts) = return [ A.OptionsPragma opts ]
toAbstract (C.RewritePragma _ x) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
case e of
A.Def x -> return [ A.RewritePragma x ]
A.Proj x -> return [ A.RewritePragma x ]
A.Con (AmbQ [x]) -> return [ A.RewritePragma x ]
- A.Con x -> fail $ "REWRITE used on ambiguous name " ++ show x
+ A.Con x -> genericError $ "REWRITE used on ambiguous name " ++ show x
+ A.Var x -> genericError $ "REWRITE used on parameter " ++ show x ++ " instead of on a defined symbol"
_ -> __IMPOSSIBLE__
toAbstract (C.CompiledTypePragma _ x hs) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
case e of
A.Def x -> return [ A.CompiledTypePragma x hs ]
- _ -> fail $ "Bad compiled type: " ++ show x -- TODO: error message
+ _ -> genericError $ "Bad compiled type: " ++ prettyShow x -- TODO: error message
toAbstract (C.CompiledDataPragma _ x hs hcs) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
case e of
A.Def x -> return [ A.CompiledDataPragma x hs hcs ]
- _ -> fail $ "Not a datatype: " ++ show x -- TODO: error message
+ _ -> genericError $ "Not a datatype: " ++ prettyShow x -- TODO: error message
toAbstract (C.CompiledPragma _ x hs) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
A.Proj x -> return x -- TODO: do we need to do s.th. special for projections? (Andreas, 2014-10-12)
- A.Con _ -> fail "Use COMPILED_DATA for constructors" -- TODO
+ A.Con _ -> genericError "Use COMPILED_DATA for constructors" -- TODO
_ -> __IMPOSSIBLE__
return [ A.CompiledPragma y hs ]
toAbstract (C.CompiledExportPragma _ x hs) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
_ -> __IMPOSSIBLE__
return [ A.CompiledExportPragma y hs ]
toAbstract (C.CompiledEpicPragma _ x ep) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
_ -> __IMPOSSIBLE__
return [ A.CompiledEpicPragma y ep ]
toAbstract (C.CompiledJSPragma _ x ep) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
A.Proj x -> return x
A.Con (AmbQ [x]) -> return x
- A.Con x -> fail ("COMPILED_JS used on ambiguous name " ++ show x)
+ A.Con x -> genericError $
+ "COMPILED_JS used on ambiguous name " ++ prettyShow x
_ -> __IMPOSSIBLE__
return [ A.CompiledJSPragma y ep ]
toAbstract (C.StaticPragma _ x) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
_ -> __IMPOSSIBLE__
return [ A.StaticPragma y ]
toAbstract (C.BuiltinPragma _ b e) = do
+ -- Andreas, 2015-02-14
+ -- Some builtins cannot be given a valid Agda type,
+ -- thus, they do not come with accompanying postulate or definition.
+ if b `elem` builtinsNoDef then do
+ case e of
+ C.Ident q@(C.QName x) -> do
+ unlessM ((UnknownName ==) <$> resolveName q) $ genericError $
+ "BUILTIN " ++ b ++ " declares an identifier " ++
+ "(no longer expects an already defined identifier)"
+ y <- freshAbstractQName defaultFixity' x
+ bindName PublicAccess DefName x y
+ return [ A.BuiltinNoDefPragma b y ]
+ _ -> genericError $
+ "Pragma BUILTIN " ++ b ++ ": expected unqualified identifier, " ++
+ "but found expression " ++ prettyShow e
+ else do
e <- toAbstract e
return [ A.BuiltinPragma b e ]
toAbstract (C.ImportPragma _ i) = do
addHaskellImport i
return []
toAbstract (C.EtaPragma _ x) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
case e of
A.Def x -> return [ A.EtaPragma x ]
- _ -> fail "Bad ETA pragma"
+ _ -> do
+ e <- showA e
+ genericError $ "Pragma ETA: expected identifier, " ++
+ "but found expression " ++ e
-- Termination checking pragmes are handled by the nicifier
toAbstract C.TerminationCheckPragma{} = __IMPOSSIBLE__
instance ToAbstract C.Clause A.Clause where
- toAbstract (C.Clause top C.Ellipsis{} _ _ _) = fail "bad '...'" -- TODO: errors message
+ toAbstract (C.Clause top C.Ellipsis{} _ _ _) = genericError "bad '...'" -- TODO: error message
toAbstract (C.Clause top lhs@(C.LHS p wps eqs with) rhs wh wcs) = withLocalVars $ do
-- Andreas, 2012-02-14: need to reset local vars before checking subclauses
vars <- getLocalVars
- let wcs' = for wcs $ \ c -> do
- setLocalVars vars
- return $ expandEllipsis p wps c
- lhs' <- toAbstract (LeftHandSide top p wps)
+ let wcs' = for wcs $ \ c -> setLocalVars vars $> c
+ lhs' <- toAbstract $ LeftHandSide top p wps
printLocals 10 "after lhs:"
let (whname, whds) = case wh of
NoWhere -> (Nothing, [])
@@ -1420,16 +1459,12 @@ instance ToAbstract C.Clause A.Clause where
return $ A.Clause lhs' rhs ds
whereToAbstract :: Range -> Maybe C.Name -> [C.Declaration] -> ScopeM a -> ScopeM (a, [A.Declaration])
-whereToAbstract _ _ [] inner = do
- x <- inner
- return (x, [])
+whereToAbstract _ _ [] inner = (,[]) <$> inner
whereToAbstract r whname whds inner = do
- m <- maybe (nameConcrete <$> freshNoName noRange) return whname
- m <- if (maybe False isNoName whname)
- then do
- (i :: NameId) <- fresh
- return (C.NoName (getRange m) i)
- else return m
+ -- Create a fresh concrete name if there isn't (a proper) one.
+ m <- case whname of
+ Just m | not (isNoName m) -> return m
+ _ -> C.NoName (getRange whname) <$> fresh
let acc = maybe PrivateAccess (const PublicAccess) whname -- unnamed where's are private
let tel = []
old <- getCurrentModule
@@ -1440,23 +1475,25 @@ whereToAbstract r whname whds inner = do
setCurrentModule old
bindModule acc m am
-- Issue 848: if the module was anonymous (module _ where) open it public
- when (maybe False isNoName whname) $
+ let anonymous = maybe False isNoName whname
+ when anonymous $
openModule_ (C.QName m) $
defaultImportDir { publicOpen = True }
return (x, ds)
data RightHandSide = RightHandSide
- { rhsRewriteEqn :: [C.RewriteEqn] -- ^ @rewrite e@ (many)
- , rhsWithExpr :: [C.WithExpr] -- ^ @with e@ (many)
+ { rhsRewriteEqn :: [C.RewriteEqn] -- ^ @rewrite e@ (many)
+ , rhsWithExpr :: [C.WithExpr] -- ^ @with e@ (many)
, rhsSubclauses :: [ScopeM C.Clause] -- ^ the subclauses spawned by a with (monadic because we need to reset the local vars before checking these clauses)
, rhs :: C.RHS
, rhsWhereDecls :: [C.Declaration]
}
-data AbstractRHS = AbsurdRHS'
- | WithRHS' [A.Expr] [ScopeM C.Clause] -- ^ The with clauses haven't been translated yet
- | RHS' A.Expr
- | RewriteRHS' [A.Expr] AbstractRHS [A.Declaration]
+data AbstractRHS
+ = AbsurdRHS'
+ | WithRHS' [A.Expr] [ScopeM C.Clause] -- ^ The with clauses haven't been translated yet
+ | RHS' A.Expr
+ | RewriteRHS' [A.Expr] AbstractRHS [A.Declaration]
qualifyName_ :: A.Name -> ScopeM A.QName
qualifyName_ x = do
@@ -1474,7 +1511,7 @@ instance ToAbstract AbstractRHS A.RHS where
toAbstract (RewriteRHS' eqs rhs wh) = do
auxs <- replicateM (length eqs) $ withFunctionName "rewrite-"
rhs <- toAbstract rhs
- return $ RewriteRHS auxs eqs rhs wh
+ return $ RewriteRHS (zip auxs eqs) rhs wh
toAbstract (WithRHS' es cs) = do
aux <- withFunctionName "with-"
A.WithRHS aux es <$> do toAbstract =<< sequence cs
@@ -1539,7 +1576,7 @@ instance ToAbstract C.LHSCore (A.LHSCore' C.Expr) where
d <- case qx of
FieldName d -> return $ anameName d
UnknownName -> notInScope d
- _ -> typeError $ GenericError $
+ _ -> genericError $
"head of copattern needs to be a field identifier, but "
++ show d ++ " isn't one"
args1 <- toAbstract ps1
@@ -1547,9 +1584,12 @@ instance ToAbstract C.LHSCore (A.LHSCore' C.Expr) where
args2 <- toAbstract ps2
return $ A.LHSProj d args1 l args2
+instance ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) where
+ toAbstract (WithHiding h a) = WithHiding h <$> toAbstractHiding h a
+
instance ToAbstract c a => ToAbstract (C.Arg c) (A.Arg a) where
toAbstract (Common.Arg info e) =
- Common.Arg <$> toAbstract info <*> toAbstractCtx (hiddenArgumentCtx $ getHiding info) e
+ Common.Arg <$> toAbstract info <*> toAbstractHiding info e
instance ToAbstract c a => ToAbstract (Named name c) (Named name a) where
toAbstract (Named n e) = Named n <$> toAbstract e
@@ -1587,32 +1627,37 @@ instance ToAbstract (A.Pattern' C.Expr) (A.Pattern' A.Expr) where
toAbstract (A.ImplicitP i) = return $ A.ImplicitP i
toAbstract (A.PatternSynP i x as) = A.PatternSynP i x <$> mapM toAbstract as
+resolvePatternIdentifier ::
+ Range -> C.QName -> Maybe (Set A.Name) -> ScopeM (A.Pattern' C.Expr)
+resolvePatternIdentifier r x ns = do
+ px <- toAbstract (PatName x ns)
+ case px of
+ VarPatName y -> return $ VarP y
+ ConPatName ds -> return $ ConP (ConPatInfo False $ PatRange r)
+ (AmbQ $ map anameName ds)
+ []
+ PatternSynPatName d -> return $ PatternSynP (PatRange r)
+ (anameName d) []
+
instance ToAbstract C.Pattern (A.Pattern' C.Expr) where
- toAbstract p@(C.IdentP x) = do
- px <- toAbstract (PatName x)
- case px of
- VarPatName y -> return $ VarP y
- ConPatName ds -> return $ ConP (ConPatInfo False $ PatRange (getRange p))
- (AmbQ $ map anameName ds)
- []
- PatternSynPatName d -> return $ PatternSynP (PatRange (getRange p))
- (anameName d) []
+ toAbstract (C.IdentP x) =
+ resolvePatternIdentifier (getRange x) x Nothing
toAbstract (AppP (QuoteP _) p)
| IdentP x <- namedArg p,
getHiding p == NotHidden = do
- e <- toAbstract (OldQName x)
+ e <- toAbstract (OldQName x Nothing)
let quoted (A.Def x) = return x
quoted (A.Proj x) = return x
quoted (A.Con (AmbQ [x])) = return x
- quoted (A.Con (AmbQ xs)) = typeError $ GenericError $ "quote: Ambigous name: " ++ show xs
+ quoted (A.Con (AmbQ xs)) = genericError $ "quote: Ambigous name: " ++ show xs
quoted (A.ScopedExpr _ e) = quoted e
- quoted _ = typeError $ GenericError $ "quote: not a defined name"
+ quoted _ = genericError $ "quote: not a defined name"
A.LitP . LitQName (getRange x) <$> quoted e
toAbstract (QuoteP r) =
- typeError $ GenericError "quote must be applied to an identifier"
+ genericError "quote must be applied to an identifier"
toAbstract p0@(AppP p q) = do
(p', q') <- toAbstract (p,q)
@@ -1625,20 +1670,16 @@ instance ToAbstract C.Pattern (A.Pattern' C.Expr) where
r = getRange p0
info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0
- toAbstract p0@(OpAppP r op ps) = do
- p <- toAbstract (IdentP op)
+ toAbstract p0@(OpAppP r op ns ps) = do
+ p <- resolvePatternIdentifier (getRange op) op (Just ns)
ps <- toAbstract ps
case p of
- ConP i x as -> return $ ConP (i {patInfo = info}) x
- (as ++ ps)
- DefP _ x as -> return $ DefP info x
- (as ++ ps)
- PatternSynP _ x as -> return $ PatternSynP info x
- (as ++ ps)
+ ConP i x as -> return $ ConP (i {patInfo = info}) x (as ++ ps)
+ DefP _ x as -> return $ DefP info x (as ++ ps)
+ PatternSynP _ x as -> return $ PatternSynP info x (as ++ ps)
_ -> __IMPOSSIBLE__
where
- r = getRange p0
- info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0
+ info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0
-- Removed when parsing
toAbstract (HiddenP _ _) = __IMPOSSIBLE__
@@ -1664,11 +1705,11 @@ instance ToAbstract C.Pattern (A.Pattern' C.Expr) where
-- | Turn an operator application into abstract syntax. Make sure to record the
-- right precedences for the various arguments.
-toAbstractOpApp :: C.QName -> [C.NamedArg (OpApp C.Expr)] -> ScopeM A.Expr
-toAbstractOpApp op es = do
+toAbstractOpApp :: C.QName -> Set A.Name -> [C.NamedArg (OpApp C.Expr)] -> ScopeM A.Expr
+toAbstractOpApp op ns es = do
-- Get the notation for the operator.
- f <- getFixity op
- let parts = notation . oldToNewNotation $ (op, f)
+ nota <- getNotation op ns
+ let parts = notation nota
-- We can throw away the @BindingHoles@, since binders
-- have been preprocessed into @OpApp C.Expr@.
let nonBindingParts = filter (not . isBindingHole) parts
@@ -1676,8 +1717,8 @@ toAbstractOpApp op es = do
-- If not, crash.
unless (length (filter isAHole nonBindingParts) == length es) __IMPOSSIBLE__
-- Translate operator and its arguments (each in the right context).
- op <- toAbstract (OldQName op)
- foldl' app op <$> left (theFixity f) nonBindingParts es
+ op <- toAbstract (OldQName op (Just ns))
+ foldl' app op <$> left (notaFixity nota) nonBindingParts es
where
-- Build an application in the abstract syntax, with correct Range.
app e arg = A.App (ExprRange (fuseRange e arg)) e (setArgColors [] arg)
diff --git a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
index da47b35..1333506 100644
--- a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
@@ -1,12 +1,11 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE UndecidableInstances #-}
{-|
Translating from internal syntax to abstract syntax. Enables nice
@@ -51,6 +50,7 @@ import Agda.Syntax.Internal as I
import qualified Agda.Utils.VarSet as VSet
import Agda.TypeChecking.Monad as M hiding (MetaInfo)
+import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import {-# SOURCE #-} Agda.TypeChecking.Records
import Agda.TypeChecking.CompiledClause (CompiledClauses(Fail))
@@ -99,6 +99,22 @@ reifyIArg' e = flip Common.Arg (unArg e) <$> reify (argInfo e)
reifyIArgs' :: [I.Arg e] -> TCM [A.Arg e]
reifyIArgs' = mapM reifyIArg'
+-- Composition of reified eliminations ------------------------------------
+
+elims :: Expr -> [I.Elim' Expr] -> TCM Expr
+elims e [] = return e
+elims e (I.Apply arg : es) = do
+ arg <- reifyIArg' arg
+ elims (A.App exprInfo e $ fmap unnamed arg) es
+elims e (I.Proj d : es) = elims (A.App exprInfo (A.Proj d) $ defaultNamedArg e) es
+
+reifyIElim :: Reify i a => I.Elim' i -> TCM (I.Elim' a)
+reifyIElim (I.Apply i) = I.Apply <$> traverse reify i
+reifyIElim (I.Proj d) = return $ I.Proj d
+
+reifyIElims :: Reify i a => [I.Elim' i] -> TCM [I.Elim' a]
+reifyIElims = mapM reifyIElim
+
-- Omitting information ---------------------------------------------------
exprInfo :: ExprInfo
@@ -146,13 +162,18 @@ instance Reify MetaId Expr where
caseMaybeM (isInteractionMeta x) underscore $ \ ii@InteractionId{} ->
return $ A.QuestionMark (mi' {metaNumber = Just n}) ii
+-- Does not print with-applications correctly:
+-- instance Reify DisplayTerm Expr where
+-- reifyWhen = reifyWhenE
+-- reify d = reifyTerm False $ dtermToTerm d
+
instance Reify DisplayTerm Expr where
reifyWhen = reifyWhenE
reify d = case d of
DTerm v -> reifyTerm False v
DDot v -> reify v
DCon c vs -> apps (A.Con (AmbQ [conName c])) =<< reifyIArgs vs
- DDef f vs -> apps (A.Def f) =<< reifyIArgs vs
+ DDef f es -> elims (A.Def f) =<< reifyIElims es
DWithApp u us vs -> do
(e, es) <- reify (u, us)
reifyApp (if null es then e else A.WithApp exprInfo e es) vs
@@ -164,7 +185,7 @@ instance Reify DisplayTerm Expr where
reifyDisplayForm :: QName -> I.Args -> TCM A.Expr -> TCM A.Expr
reifyDisplayForm f vs fallback = do
ifNotM displayFormsEnabled fallback $ {- else -} do
- caseMaybeM (liftTCM $ displayForm f vs) fallback reify
+ caseMaybeM (liftTCM $ displayForm f vs) fallback reify
-- | @reifyDisplayFormP@ tries to recursively
-- rewrite a lhs with a display form.
@@ -197,10 +218,12 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
reifyDisplayFormP =<< displayLHS (map namedArg ps) wps d
_ -> return lhs
where
+ -- Andreas, 2015-05-03: Ulf, please comment on what
+ -- is the idea behind okDisplayForm.
okDisplayForm (DWithApp d ds []) =
okDisplayForm d && all okDisplayTerm ds
okDisplayForm (DTerm (I.Def f vs)) = all okElim vs
- okDisplayForm (DDef f vs) = all okDArg vs
+ okDisplayForm (DDef f es) = all okDElim es
okDisplayForm DDot{} = False
okDisplayForm DCon{} = False
okDisplayForm DTerm{} = True -- False?
@@ -212,7 +235,8 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
okDisplayTerm DDef{} = False
okDisplayTerm _ = False
- okDArg = okDisplayTerm . unArg
+ okDElim (I.Apply v) = okDisplayTerm $ unArg v
+ okDElim I.Proj{} = True -- True, man, or False? No clue what I am implementing here --Andreas, 2015-05-03
okArg = okTerm . unArg
okElim (I.Apply a) = okArg a
@@ -223,27 +247,27 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
okTerm (I.Def x []) = isNoName $ qnameToConcrete x -- Handling wildcards in display forms
okTerm _ = True -- False
- -- Flatten a dt into (parentName, parentArgs, withArgs).
- flattenWith :: DisplayTerm -> (QName, [I.Arg DisplayTerm], [DisplayTerm])
+ -- Flatten a dt into (parentName, parentElims, withArgs).
+ flattenWith :: DisplayTerm -> (QName, [I.Elim' DisplayTerm], [DisplayTerm])
flattenWith (DWithApp d ds1 ds2) = case flattenWith d of
- (f, vs, ds0) -> (f, vs, ds0 ++ ds1 ++ map (DTerm . unArg) ds2)
- flattenWith (DDef f vs) = (f, vs, []) -- .^ hacky, but we should only hit this when printing debug info
- flattenWith (DTerm (I.Def f es)) =
- let vs = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es
- in (f, map (fmap DTerm) vs, [])
+ (f, es, ds0) -> (f, es, ds0 ++ ds1 ++ map (DTerm . unArg) ds2)
+ flattenWith (DDef f es) = (f, es, []) -- .^ hacky, but we should only hit this when printing debug info
+ flattenWith (DTerm (I.Def f es)) = (f, map (fmap DTerm) es, [])
flattenWith _ = __IMPOSSIBLE__
displayLHS :: [A.Pattern] -> [A.Pattern] -> DisplayTerm -> TCM A.SpineLHS
displayLHS ps wps d = case flattenWith d of
(f, vs, ds) -> do
ds <- mapM termToPat ds
- vs <- mapM argToPat vs
+ vs <- mapM elimToPat vs
vs <- reifyIArgs' vs
return $ SpineLHS i f vs (ds ++ wps)
--- return $ LHS i (LHSHead f vs) (ds ++ wps)
where
ci = ConPatInfo False patNoRange
+
argToPat arg = fmap unnamed <$> traverse termToPat arg
+ elimToPat (I.Apply arg) = argToPat arg
+ elimToPat (I.Proj d) = return $ defaultNamedArg $ A.DefP patNoRange d []
termToPat :: DisplayTerm -> TCM A.Pattern
@@ -302,42 +326,41 @@ instance Reify Term Expr where
reifyTerm :: Bool -> Term -> TCM Expr
reifyTerm expandAnonDefs0 v = do
- hasDisplayForms <- displayFormsEnabled
- -- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled
- -- (i.e. when we don't care about nice printing)
- let expandAnonDefs = expandAnonDefs0 && hasDisplayForms
- v <- unSpine <$> instantiate v
- case v of
- _ | isHackReifyToMeta v -> return $ A.Underscore emptyMetaInfo
- I.Var n es -> do
- let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
- x <- liftTCM $ nameOfBV n `catchError` \_ -> freshName_ ("@" ++ show n)
- reifyApp (A.Var x) vs
- I.Def x es -> do
+ -- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled
+ -- (i.e. when we don't care about nice printing)
+ expandAnonDefs <- return expandAnonDefs0 `and2M` displayFormsEnabled
+ v <- unSpine <$> instantiate v
+ case v of
+ _ | isHackReifyToMeta v -> return $ A.Underscore emptyMetaInfo
+ I.Var n es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
- reifyDisplayForm x vs $ reifyDef expandAnonDefs x vs
- I.Con c vs -> do
- let x = conName c
- isR <- isGeneratedRecordConstructor x
- case isR of
- True -> do
- showImp <- showImplicitArguments
- let keep (a, v) = showImp || notHidden a
- r <- getConstructorData x
- xs <- getRecordFieldNames r
- vs <- map unArg <$> reifyIArgs vs
- return $ A.Rec exprInfo $ map (unArg *** id) $ filter keep $ zip xs vs
- False -> reifyDisplayForm x vs $ do
- ci <- getConstInfo x
- let Constructor{conPars = np} = theDef ci
- -- if we are the the module that defines constructor x
- -- then we have to drop at least the n module parameters
- n <- getDefFreeVars x
- -- the number of parameters is greater (if the data decl has
- -- extra parameters) or equal (if not) to n
- when (n > np) __IMPOSSIBLE__
- let h = A.Con (AmbQ [x])
- if null vs then return h else do
+ x <- liftTCM $ nameOfBV n `catchError` \_ -> freshName_ ("@" ++ show n)
+ reifyApp (A.Var x) vs
+ I.Def x es -> do
+ let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
+ reifyDisplayForm x vs $ reifyDef expandAnonDefs x vs
+ I.Con c vs -> do
+ let x = conName c
+ isR <- isGeneratedRecordConstructor x
+ case isR of
+ True -> do
+ showImp <- showImplicitArguments
+ let keep (a, v) = showImp || notHidden a
+ r <- getConstructorData x
+ xs <- getRecordFieldNames r
+ vs <- map unArg <$> reifyIArgs vs
+ return $ A.Rec exprInfo $ map (unArg *** id) $ filter keep $ zip xs vs
+ False -> reifyDisplayForm x vs $ do
+ ci <- getConstInfo x
+ let Constructor{conPars = np} = theDef ci
+ -- if we are the the module that defines constructor x
+ -- then we have to drop at least the n module parameters
+ n <- getDefFreeVars x
+ -- the number of parameters is greater (if the data decl has
+ -- extra parameters) or equal (if not) to n
+ when (n > np) __IMPOSSIBLE__
+ let h = A.Con (AmbQ [x])
+ if null vs then return h else do
es <- reifyIArgs vs
-- Andreas, 2012-04-20: do not reify parameter arguments of constructor
-- if the first regular constructor argument is hidden
@@ -379,86 +402,86 @@ reifyTerm expandAnonDefs0 v = do
]
napps h $ genericDrop (n - np) $ nameFirstIfHidden doms es
-}
--- I.Lam info b | isAbsurdBody b -> return $ A.AbsurdLam exprInfo $ getHiding info
- I.Lam info b -> do
- (x,e) <- reify b
- info <- reify info
- return $ A.Lam exprInfo (DomainFree info x) e
- -- Andreas, 2011-04-07 we do not need relevance information at internal Lambda
- I.Lit l -> reify l
- I.Level l -> reify l
- I.Pi a b -> case b of
- NoAbs _ b'
- | notHidden a -> uncurry (A.Fun $ exprInfo) <$> reify (a, b')
- -- Andreas, 2013-11-11 Hidden/Instance I.Pi must be A.Pi
- -- since (a) the syntax {A} -> B or {{A}} -> B is not legal
- -- and (b) the name of the binder might matter.
- -- See issue 951 (a) and 952 (b).
- | otherwise -> mkPi b =<< reify a
- b -> mkPi b =<< do
- ifM (domainFree a (absBody b))
- {- then -} (Common.Arg <$> reify (domInfo a) <*> pure underscore)
- {- else -} (reify a)
- where
- mkPi b (Common.Arg info a) = do
- (x, b) <- reify b
- return $ A.Pi exprInfo [TypedBindings noRange $ Common.Arg info (TBind noRange [x] a)] b
- -- We can omit the domain type if it doesn't have any free variables
- -- and it's mentioned in the target type.
- domainFree a b = do
- df <- asks envPrintDomainFreePi
- return $ and [df, freeIn 0 b, VSet.null $ allVars $ freeVars a]
-
- I.Sort s -> reify s
- I.MetaV x es -> do
- let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
- x' <- reify x
- apps x' =<< reifyIArgs vs
- I.DontCare v -> A.DontCare <$> reifyTerm expandAnonDefs v
- I.Shared p -> reifyTerm expandAnonDefs $ derefPtr p
- I.ExtLam cls args -> do
- x <- freshName_ "extlam"
- reifyExtLam (qnameFromList [x]) 0 cls (map (fmap unnamed) args)
- where
- -- Andreas, 2012-10-20 expand a copy in an anonymous module
- -- to improve error messages.
- -- Don't do this if we have just expanded into a display form,
- -- otherwise we loop!
- reifyDef :: Bool -> QName -> I.Args -> TCM Expr
- reifyDef True x@(QName m name) vs | A.isAnonymousModuleName m = do
- r <- reduceDefCopy x vs
- case r of
- YesReduction _ v -> do
- reportSLn "reify.anon" 60 $ unlines
- [ "reduction on defined ident. in anonymous module"
- , "x = " ++ show x
- , "v = " ++ show v
- ]
- reify v
- NoReduction () -> do
- reportSLn "reify.anon" 60 $ unlines
- [ "no reduction on defined ident. in anonymous module"
- , "x = " ++ show x
- , "vs = " ++ show vs
- ]
- reifyDef' x vs
- reifyDef _ x vs = reifyDef' x vs
-
- reifyDef' :: QName -> I.Args -> TCM Expr
- reifyDef' x@(QName _ name) vs = do
- -- We should drop this many arguments from the local context.
- n <- getDefFreeVars x
- mdefn <- liftTCM $ (Just <$> getConstInfo x) `catchError` \_ -> return Nothing
- -- check if we have an absurd lambda
- let reifyAbsurdLambda cont =
- case theDef <$> mdefn of
- Just Function{ funCompiled = Just Fail, funClauses = [cl] }
- | isAbsurdLambdaName x -> do
- -- get hiding info from last pattern, which should be ()
- let h = getHiding $ last (clausePats cl)
- apps (A.AbsurdLam exprInfo h) =<< reifyIArgs vs
- _ -> cont
- reifyAbsurdLambda $ do
+-- I.Lam info b | isAbsurdBody b -> return $ A.AbsurdLam exprInfo $ getHiding info
+ I.Lam info b -> do
+ (x,e) <- reify b
+ info <- reify info
+ return $ A.Lam exprInfo (DomainFree info x) e
+ -- Andreas, 2011-04-07 we do not need relevance information at internal Lambda
+ I.Lit l -> reify l
+ I.Level l -> reify l
+ I.Pi a b -> case b of
+ NoAbs _ b'
+ | notHidden a -> uncurry (A.Fun $ exprInfo) <$> reify (a, b')
+ -- Andreas, 2013-11-11 Hidden/Instance I.Pi must be A.Pi
+ -- since (a) the syntax {A} -> B or {{A}} -> B is not legal
+ -- and (b) the name of the binder might matter.
+ -- See issue 951 (a) and 952 (b).
+ | otherwise -> mkPi b =<< reify a
+ b -> mkPi b =<< do
+ ifM (domainFree a (absBody b))
+ {- then -} (Common.Arg <$> reify (domInfo a) <*> pure underscore)
+ {- else -} (reify a)
+ where
+ mkPi b (Common.Arg info a) = do
+ (x, b) <- reify b
+ return $ A.Pi exprInfo [TypedBindings noRange $ Common.Arg info (TBind noRange [pure x] a)] b
+ -- We can omit the domain type if it doesn't have any free variables
+ -- and it's mentioned in the target type.
+ domainFree a b = do
+ df <- asks envPrintDomainFreePi
+ return $ and [df, freeIn 0 b, VSet.null $ allVars $ freeVars a]
+
+ I.Sort s -> reify s
+ I.MetaV x es -> do
+ let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
+ x' <- reify x
+ apps x' =<< reifyIArgs vs
+ I.DontCare v -> A.DontCare <$> reifyTerm expandAnonDefs v
+ I.Shared p -> reifyTerm expandAnonDefs $ derefPtr p
+ I.ExtLam cls args -> do
+ x <- freshName_ "extlam"
+ reifyExtLam (qnameFromList [x]) 0 cls (map (fmap unnamed) args)
+ where
+ -- Andreas, 2012-10-20 expand a copy in an anonymous module
+ -- to improve error messages.
+ -- Don't do this if we have just expanded into a display form,
+ -- otherwise we loop!
+ reifyDef :: Bool -> QName -> I.Args -> TCM Expr
+ reifyDef True x@(QName m name) vs | A.isAnonymousModuleName m = do
+ r <- reduceDefCopy x vs
+ case r of
+ YesReduction _ v -> do
+ reportSLn "reify.anon" 60 $ unlines
+ [ "reduction on defined ident. in anonymous module"
+ , "x = " ++ show x
+ , "v = " ++ show v
+ ]
+ reify v
+ NoReduction () -> do
+ reportSLn "reify.anon" 60 $ unlines
+ [ "no reduction on defined ident. in anonymous module"
+ , "x = " ++ show x
+ , "vs = " ++ show vs
+ ]
+ reifyDef' x vs
+ reifyDef _ x vs = reifyDef' x vs
+
+ reifyDef' :: QName -> I.Args -> TCM Expr
+ reifyDef' x@(QName _ name) vs = do
+ -- We should drop this many arguments from the local context.
+ n <- getDefFreeVars x
+ mdefn <- liftTCM $ (Just <$> getConstInfo x) `catchError` \_ -> return Nothing
+ -- check if we have an absurd lambda
+ let reifyAbsurdLambda cont =
+ case theDef <$> mdefn of
+ Just Function{ funCompiled = Just Fail, funClauses = [cl] }
+ | isAbsurdLambdaName x -> do
+ -- get hiding info from last pattern, which should be ()
+ let h = getHiding $ last (clausePats cl)
+ apps (A.AbsurdLam exprInfo h) =<< reifyIArgs vs
+ _ -> cont
+ reifyAbsurdLambda $ do
(pad, vs :: [I.NamedArg Term]) <- do
case mdefn of
Nothing -> return ([], map (fmap unnamed) $ genericDrop n vs)
@@ -475,7 +498,7 @@ reifyTerm expandAnonDefs0 v = do
-- These are the dropped projection arguments
(np, pad, dom) <-
case def of
- Function{ funProjection = Just Projection{ projIndex = np } } -> do
+ Function{ funProjection = Just Projection{ projIndex = np } } | np > 0 -> do
TelV tel _ <- telView (defType defn)
scope <- getScope
let (as, dom:_) = splitAt (np - 1) $ telToList tel
@@ -507,14 +530,14 @@ reifyTerm expandAnonDefs0 v = do
let apps = foldl' (\e a -> A.App exprInfo e (fmap unnamed a))
napps (A.Def x `apps` pad) =<< reifyIArgs vs
- reifyExtLam :: QName -> Int -> [I.Clause] -> [I.NamedArg Term] -> TCM Expr
- reifyExtLam x n cls vs = do
- reportSLn "reify.def" 10 $ "reifying extended lambda with definition: x = " ++ show x
- -- drop lambda lifted arguments
- cls <- mapM (reify . QNamed x . dropArgs n) $ cls
- let cx = nameConcrete $ qnameName x
- dInfo = mkDefInfo cx defaultFixity' PublicAccess ConcreteDef (getRange x)
- napps (A.ExtendedLam exprInfo dInfo x cls) =<< reifyIArgs vs
+ reifyExtLam :: QName -> Int -> [I.Clause] -> [I.NamedArg Term] -> TCM Expr
+ reifyExtLam x n cls vs = do
+ reportSLn "reify.def" 10 $ "reifying extended lambda with definition: x = " ++ show x
+ -- drop lambda lifted arguments
+ cls <- mapM (reify . QNamed x . dropArgs n) $ cls
+ let cx = nameConcrete $ qnameName x
+ dInfo = mkDefInfo cx defaultFixity' PublicAccess ConcreteDef (getRange x)
+ napps (A.ExtendedLam exprInfo dInfo x cls) =<< reifyIArgs vs
-- | @nameFirstIfHidden n (a1->...an->{x:a}->b) ({e} es) = {x = e} es@
nameFirstIfHidden :: [I.Dom (ArgName, t)] -> [I.Arg a] -> [I.NamedArg a]
@@ -647,95 +670,95 @@ stripImplicits :: ([A.NamedArg A.Pattern], [A.Pattern]) ->
TCM ([A.NamedArg A.Pattern], [A.Pattern])
stripImplicits (ps, wps) = do -- v if show-implicit we don't need the names
ifM showImplicitArguments (return (map (unnamed . namedThing <$>) ps, wps)) $ do
- let vars = dotVars (ps, wps)
- reportSLn "reify.implicit" 30 $ unlines
- [ "stripping implicits"
- , " ps = " ++ show ps
- , " wps = " ++ show wps
- , " vars = " ++ show vars
- ]
- let allps = ps ++ map defaultNamedArg wps
- sps = blankDots $ foldl (.) (strip Set.empty) (map rearrangeBinding $ Set.toList vars) $ allps
- (ps', wps') = splitAt (length sps - length wps) sps
- reportSLn "reify.implicit" 30 $ unlines
- [ " ps' = " ++ show ps'
- , " wps' = " ++ show (map namedArg wps')
- ]
- return (ps', map namedArg wps')
- where
- argsVars = Set.unions . map argVars
- argVars = patVars . namedArg
- patVars p = case p of
- A.VarP x -> Set.singleton x
- A.ConP _ _ ps -> argsVars ps
- A.DefP _ _ ps -> Set.empty
- A.DotP _ e -> Set.empty
- A.WildP _ -> Set.empty
- A.AbsurdP _ -> Set.empty
- A.LitP _ -> Set.empty
- A.ImplicitP _ -> Set.empty
- A.AsP _ _ p -> patVars p
- A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- Set.empty
-
- -- Replace dot variables by ._ if they use implicitly bound variables. This
- -- is slightly nicer than making the implicts explicit.
- blankDots ps = (map . fmap . fmap . fmap) blank ps
- where
- bound = argsVars ps
- blank e | Set.null (Set.difference (dotVars e) bound) = e
- | otherwise = A.Underscore emptyMetaInfo
-
- -- Pick the "best" place to bind the variable. Best in this case
- -- is the left-most explicit binding site. But, of course we can't
- -- do this since binding site might be forced by a parent clause.
- -- Why? Because the binding site we pick might not exist in the
- -- generated with function if it corresponds to a dot pattern.
- rearrangeBinding x ps = ps
-
- strip dvs ps = stripArgs True ps
- where
- stripArgs _ [] = []
- stripArgs fixedPos (a : as) =
- case getHiding a of
- Hidden | canStrip a as -> stripArgs False as
- Instance | canStrip a as -> stripArgs False as
- _ -> stripName fixedPos (stripArg a) :
- stripArgs True as
-
- stripName True = fmap (unnamed . namedThing)
- stripName False = id
-
- canStrip a as = and
- [ varOrDot p
- , noInterestingBindings p
- , all (flip canStrip []) $ takeWhile isUnnamedHidden as
- ]
- where p = namedArg a
-
- isUnnamedHidden x = notVisible x && nameOf (unArg x) == Nothing
-
- stripArg a = fmap (fmap stripPat) a
-
- stripPat p = case p of
- A.VarP _ -> p
- A.ConP i c ps -> A.ConP i c $ stripArgs True ps
- A.DefP _ _ _ -> p
- A.DotP _ e -> p
- A.WildP _ -> p
- A.AbsurdP _ -> p
- A.LitP _ -> p
- A.ImplicitP _ -> p
- A.AsP i x p -> A.AsP i x $ stripPat p
- A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- p
-
- noInterestingBindings p =
- Set.null $ dvs `Set.intersection` patVars p
-
- varOrDot A.VarP{} = True
- varOrDot A.WildP{} = True
- varOrDot A.DotP{} = True
- varOrDot A.ImplicitP{} = True
- varOrDot _ = False
+ let vars = dotVars (ps, wps)
+ reportSLn "reify.implicit" 30 $ unlines
+ [ "stripping implicits"
+ , " ps = " ++ show ps
+ , " wps = " ++ show wps
+ , " vars = " ++ show vars
+ ]
+ let allps = ps ++ map defaultNamedArg wps
+ sps = blankDots $ foldl (.) (strip Set.empty) (map rearrangeBinding $ Set.toList vars) $ allps
+ (ps', wps') = splitAt (length sps - length wps) sps
+ reportSLn "reify.implicit" 30 $ unlines
+ [ " ps' = " ++ show ps'
+ , " wps' = " ++ show (map namedArg wps')
+ ]
+ return (ps', map namedArg wps')
+ where
+ argsVars = Set.unions . map argVars
+ argVars = patVars . namedArg
+ patVars p = case p of
+ A.VarP x -> Set.singleton x
+ A.ConP _ _ ps -> argsVars ps
+ A.DefP _ _ ps -> Set.empty
+ A.DotP _ e -> Set.empty
+ A.WildP _ -> Set.empty
+ A.AbsurdP _ -> Set.empty
+ A.LitP _ -> Set.empty
+ A.ImplicitP _ -> Set.empty
+ A.AsP _ _ p -> patVars p
+ A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- Set.empty
+
+ -- Replace dot variables by ._ if they use implicitly bound variables. This
+ -- is slightly nicer than making the implicts explicit.
+ blankDots ps = (map . fmap . fmap . fmap) blank ps
+ where
+ bound = argsVars ps
+ blank e | Set.null (Set.difference (dotVars e) bound) = e
+ | otherwise = A.Underscore emptyMetaInfo
+
+ -- Pick the "best" place to bind the variable. Best in this case
+ -- is the left-most explicit binding site. But, of course we can't
+ -- do this since binding site might be forced by a parent clause.
+ -- Why? Because the binding site we pick might not exist in the
+ -- generated with function if it corresponds to a dot pattern.
+ rearrangeBinding x ps = ps
+
+ strip dvs ps = stripArgs True ps
+ where
+ stripArgs _ [] = []
+ stripArgs fixedPos (a : as) =
+ case getHiding a of
+ Hidden | canStrip a as -> stripArgs False as
+ Instance | canStrip a as -> stripArgs False as
+ _ -> stripName fixedPos (stripArg a) :
+ stripArgs True as
+
+ stripName True = fmap (unnamed . namedThing)
+ stripName False = id
+
+ canStrip a as = and
+ [ varOrDot p
+ , noInterestingBindings p
+ , all (flip canStrip []) $ takeWhile isUnnamedHidden as
+ ]
+ where p = namedArg a
+
+ isUnnamedHidden x = notVisible x && nameOf (unArg x) == Nothing
+
+ stripArg a = fmap (fmap stripPat) a
+
+ stripPat p = case p of
+ A.VarP _ -> p
+ A.ConP i c ps -> A.ConP i c $ stripArgs True ps
+ A.DefP _ _ _ -> p
+ A.DotP _ e -> p
+ A.WildP _ -> p
+ A.AbsurdP _ -> p
+ A.LitP _ -> p
+ A.ImplicitP _ -> p
+ A.AsP i x p -> A.AsP i x $ stripPat p
+ A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- p
+
+ noInterestingBindings p =
+ Set.null $ dvs `Set.intersection` patVars p
+
+ varOrDot A.VarP{} = True
+ varOrDot A.WildP{} = True
+ varOrDot A.DotP{} = True
+ varOrDot A.ImplicitP{} = True
+ varOrDot _ = False
-- | @dotVars ps@ gives all the variables inside of dot patterns of @ps@
-- It is only invoked for patternish things. (Ulf O-tone!)
@@ -820,7 +843,7 @@ instance DotVars RHS where
dotVars (RHS e) = dotVars e
dotVars AbsurdRHS = Set.empty
dotVars (WithRHS _ es clauses) = __IMPOSSIBLE__ -- NZ
- dotVars (RewriteRHS _ es rhs _) = __IMPOSSIBLE__ -- NZ
+ dotVars (RewriteRHS xes rhs _) = __IMPOSSIBLE__ -- NZ
instance DotVars TypedBindings where
dotVars (TypedBindings _ bs) = dotVars bs
@@ -858,14 +881,14 @@ reifyPatterns tel perm ps = evalStateT (reifyArgs ps) 0
lift $ A.VarP <$> nameOfBV (size tel - 1 - j)
I.DotP v -> do
t <- lift $ reify v
- tick
+ _ <- tick
let vars = Set.map show (dotVars t)
t' = if Set.member "()" vars then underscore else t
return $ A.DotP patNoRange t'
I.LitP l -> return $ A.LitP l
I.ProjP d -> return $ A.DefP patNoRange d []
- I.ConP c mt ps -> A.ConP ci (AmbQ [conName c]) <$> reifyArgs ps
- where ci = flip ConPatInfo patNoRange $ maybe False fst mt
+ I.ConP c cpi ps -> A.ConP ci (AmbQ [conName c]) <$> reifyArgs ps
+ where ci = flip ConPatInfo patNoRange $ fromMaybe False $ I.conPRecord cpi
instance Reify NamedClause A.Clause where
reify (QNamed f (I.Clause _ tel perm ps body _)) = addCtxTel tel $ do
@@ -893,21 +916,24 @@ instance Reify Type Expr where
instance Reify Sort Expr where
reifyWhen = reifyWhenE
- reify s =
- do s <- instantiateFull s
- case s of
- I.Type (I.Max []) -> return $ A.Set exprInfo 0
- I.Type (I.Max [I.ClosedLevel n]) -> return $ A.Set exprInfo n
- I.Type a -> do
- a <- reify a
- return $ A.App exprInfo (A.Set exprInfo 0) (defaultNamedArg a)
- I.Prop -> return $ A.Prop exprInfo
- I.Inf -> A.Var <$> freshName_ ("Setω" :: String)
- I.DLub s1 s2 -> do
- lub <- freshName_ ("dLub" :: String) -- TODO: hack
- (e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)
- let app x y = A.App exprInfo x (defaultNamedArg y)
- return $ A.Var lub `app` e1 `app` e2
+ reify s = do
+ s <- instantiateFull s
+ case s of
+ I.Type (I.Max []) -> return $ A.Set exprInfo 0
+ I.Type (I.Max [I.ClosedLevel n]) -> return $ A.Set exprInfo n
+ I.Type a -> do
+ a <- reify a
+ return $ A.App exprInfo (A.Set exprInfo 0) (defaultNamedArg a)
+ I.Prop -> return $ A.Prop exprInfo
+ I.Inf -> A.Var <$> freshName_ ("Setω" :: String)
+ I.SizeUniv -> do
+ I.Def sizeU [] <- primSizeUniv
+ return $ A.Def sizeU
+ I.DLub s1 s2 -> do
+ lub <- freshName_ ("dLub" :: String) -- TODO: hack
+ (e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)
+ let app x y = A.App exprInfo x (defaultNamedArg y)
+ return $ A.Var lub `app` e1 `app` e2
instance Reify Level Expr where
reifyWhen = reifyWhenE
@@ -932,7 +958,7 @@ instance Reify I.Telescope A.Telescope where
Common.Arg info e <- reify arg
(x,bs) <- reify tel
let r = getRange e
- return $ TypedBindings r (Common.Arg info (TBind r [x] e)) : bs
+ return $ TypedBindings r (Common.Arg info (TBind r [pure x] e)) : bs
instance Reify I.ArgInfo A.ArgInfo where
reify i = flip (mapArgInfoColors.const) i <$> reify (argInfoColors i)
@@ -951,8 +977,3 @@ instance (Reify i1 a1, Reify i2 a2, Reify i3 a3) => Reify (i1,i2,i3) (a1,a2,a3)
instance (Reify i1 a1, Reify i2 a2, Reify i3 a3, Reify i4 a4) => Reify (i1,i2,i3,i4) (a1,a2,a3,a4) where
reify (x,y,z,w) = (,,,) <$> reify x <*> reify y <*> reify z <*> reify w
-
-instance (Reify t t', Reify a a')
- => Reify (Judgement t a) (Judgement t' a') where
- reify (HasType i t) = HasType <$> reify i <*> reify t
- reify (IsSort i t) = IsSort <$> reify i <*> reify t