summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Concrete
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Concrete')
-rw-r--r--src/full/Agda/Syntax/Concrete/Definitions.hs1034
-rw-r--r--src/full/Agda/Syntax/Concrete/Generic.hs4
-rw-r--r--src/full/Agda/Syntax/Concrete/Name.hs57
-rw-r--r--src/full/Agda/Syntax/Concrete/Operators.hs101
-rw-r--r--src/full/Agda/Syntax/Concrete/Operators/Parser.hs101
-rw-r--r--src/full/Agda/Syntax/Concrete/Operators/Parser/Monad.hs100
-rw-r--r--src/full/Agda/Syntax/Concrete/Pretty.hs53
7 files changed, 874 insertions, 576 deletions
diff --git a/src/full/Agda/Syntax/Concrete/Definitions.hs b/src/full/Agda/Syntax/Concrete/Definitions.hs
index 413cf48..020234e 100644
--- a/src/full/Agda/Syntax/Concrete/Definitions.hs
+++ b/src/full/Agda/Syntax/Concrete/Definitions.hs
@@ -1,13 +1,7 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TupleSections #-}
-
-#if __GLASGOW_HASKELL__ >= 710
-{-# LANGUAGE FlexibleContexts #-}
-#endif
-- | Preprocess 'Agda.Syntax.Concrete.Declaration's, producing 'NiceDeclaration's.
--
@@ -39,7 +33,7 @@ module Agda.Syntax.Concrete.Definitions
, DeclarationException(..)
, Nice, runNice
, niceDeclarations
- , notSoNiceDeclaration
+ , notSoNiceDeclarations
, niceHasAbstract
, Measure
) where
@@ -57,9 +51,10 @@ import Data.Foldable ( foldMap )
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Maybe
-import Data.Monoid ( Monoid(mappend, mempty) )
+import Data.Semigroup ( Semigroup, Monoid, (<>), mempty, mappend )
import Data.List as List hiding (null)
-import Data.Traversable (traverse)
+import qualified Data.Set as Set
+import Data.Traversable (Traversable, traverse)
import Data.Typeable (Typeable)
import Agda.Syntax.Concrete
@@ -70,12 +65,17 @@ import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Concrete.Pretty ()
+import Agda.TypeChecking.Positivity.Occurrence
+
import Agda.Utils.Except ( Error(strMsg), MonadError(throwError) )
+import Agda.Utils.Functor
import Agda.Utils.Lens
-import Agda.Utils.List (headMaybe, isSublistOf)
+import Agda.Utils.List (caseList, headMaybe, isSublistOf)
import Agda.Utils.Monad
import Agda.Utils.Null
-import Agda.Utils.Pretty
+import qualified Agda.Utils.Pretty as Pretty
+import Agda.Utils.Pretty hiding ((<>))
+import Agda.Utils.Singleton
import Agda.Utils.Tuple
import Agda.Utils.Update
@@ -90,11 +90,32 @@ import Agda.Utils.Impossible
contained in a single constructor instead of spread out between type
signatures and clauses. The @private@, @postulate@, @abstract@ and @instance@
modifiers have been distributed to the individual declarations.
+
+ Observe the order of components:
+
+ Range
+ Fixity'
+ Access
+ IsAbstract
+ IsInstance
+ TerminationCheck
+ PositivityCheck
+
+ further attributes
+
+ (Q)Name
+
+ content (Expr, Declaration ...)
-}
data NiceDeclaration
- = Axiom Range Fixity' Access IsInstance ArgInfo Name Expr
- -- ^ Axioms and functions can be declared irrelevant. (Hiding should be NotHidden)
- | NiceField Range IsInstance Fixity' Access IsAbstract Name (Arg Expr)
+ = Axiom Range Fixity' Access IsAbstract IsInstance ArgInfo (Maybe [Occurrence]) Name Expr
+ -- ^ 'IsAbstract' argument: We record whether a declaration was made in an @abstract@ block.
+ --
+ -- 'ArgInfo' argument: Axioms and functions can be declared irrelevant.
+ -- ('Hiding' should be 'NotHidden'.)
+ --
+ -- @Maybe [Occurrence]@ argument: Polarities can be assigned to identifiers.
+ | NiceField Range Fixity' Access IsAbstract IsInstance Name (Arg Expr)
| PrimitiveFunction Range Fixity' Access IsAbstract Name Expr
| NiceMutual Range TerminationCheck PositivityCheck [NiceDeclaration]
| NiceModule Range Access IsAbstract QName Telescope [Declaration]
@@ -102,21 +123,21 @@ data NiceDeclaration
| NiceOpen Range QName ImportDirective
| NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
| NicePragma Range Pragma
- | NiceRecSig Range Fixity' Access Name [LamBinding] Expr PositivityCheck
- | NiceDataSig Range Fixity' Access Name [LamBinding] Expr PositivityCheck
+ | NiceRecSig Range Fixity' Access IsAbstract PositivityCheck Name [LamBinding] Expr
+ | NiceDataSig Range Fixity' Access IsAbstract PositivityCheck Name [LamBinding] Expr
| NiceFunClause Range Access IsAbstract TerminationCheck Catchall 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 IsMacro ArgInfo TerminationCheck Name Expr
- | FunDef Range [Declaration] Fixity' IsAbstract TerminationCheck Name [Clause]
+ | FunSig Range Fixity' Access IsAbstract IsInstance IsMacro 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] PositivityCheck [NiceConstructor]
- | RecDef Range Fixity' IsAbstract Name (Maybe (Ranged Induction)) (Maybe Bool) (Maybe (ThingWithFixity Name, IsInstance)) [LamBinding] PositivityCheck [NiceDeclaration]
+ | DataDef Range Fixity' IsAbstract PositivityCheck Name [LamBinding] [NiceConstructor]
+ | RecDef Range Fixity' IsAbstract PositivityCheck Name (Maybe (Ranged Induction)) (Maybe Bool) (Maybe (ThingWithFixity Name, IsInstance)) [LamBinding] [NiceDeclaration]
| NicePatternSyn Range Fixity' Name [Arg Name] Pattern
- | NiceUnquoteDecl Range [Fixity'] Access IsInstance IsAbstract TerminationCheck [Name] Expr
+ | NiceUnquoteDecl Range [Fixity'] Access IsAbstract IsInstance TerminationCheck [Name] Expr
| NiceUnquoteDef Range [Fixity'] Access IsAbstract TerminationCheck [Name] Expr
deriving (Typeable, Show)
@@ -141,6 +162,7 @@ data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
-- | The exception type.
data DeclarationException
= MultipleFixityDecls [(Name, [Fixity'])]
+ | MultiplePolarityPragmas [Name]
| InvalidName Name
| DuplicateDefinition Name
| MissingDefinition Name
@@ -151,6 +173,8 @@ data DeclarationException
| WrongParameters Name
| NotAllowedInMutual NiceDeclaration
| UnknownNamesInFixityDecl [Name]
+ | UnknownNamesInPolarityPragmas [Name]
+ | PolarityPragmasButNotPostulates [Name]
| Codata Range
| DeclarationPanic String
| UselessPrivate Range
@@ -169,6 +193,7 @@ data DeclarationException
| UnquoteDefRequiresSignature [Name]
| BadMacroDef NiceDeclaration
| InvalidNoPositivityCheckPragma Range
+
deriving (Typeable)
-- | Several declarations expect only type signatures as sub-declarations. These are:
@@ -182,34 +207,37 @@ data KindOfBlock
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
- getRange (MissingDataSignature x) = getRange x
- getRange (WrongDefinition x k k') = getRange x
- getRange (WrongParameters x) = getRange x
- getRange (AmbiguousFunClauses lhs xs) = getRange lhs
- getRange (NotAllowedInMutual x) = getRange x
- getRange (UnknownNamesInFixityDecl xs) = getRange . head $ xs
- getRange (Codata r) = r
- getRange (DeclarationPanic _) = noRange
- getRange (UselessPrivate r) = r
- getRange (UselessAbstract r) = r
- getRange (UselessInstance r) = r
- getRange (WrongContentBlock _ r) = r
- getRange (InvalidTerminationCheckPragma r) = r
- getRange (InvalidMeasureMutual r) = r
- getRange (PragmaNoTerminationCheck r) = r
- getRange (InvalidCatchallPragma r) = r
- getRange (UnquoteDefRequiresSignature x) = getRange x
- getRange (BadMacroDef d) = getRange d
- getRange (InvalidNoPositivityCheckPragma r) = r
+ getRange (MultipleFixityDecls xs) = getRange (fst $ head xs)
+ getRange (MultiplePolarityPragmas xs) = getRange (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
+ getRange (MissingDataSignature x) = getRange x
+ getRange (WrongDefinition x k k') = getRange x
+ getRange (WrongParameters x) = getRange x
+ getRange (AmbiguousFunClauses lhs xs) = getRange lhs
+ getRange (NotAllowedInMutual x) = getRange x
+ getRange (UnknownNamesInFixityDecl xs) = getRange . head $ xs
+ getRange (UnknownNamesInPolarityPragmas xs) = getRange . head $ xs
+ getRange (PolarityPragmasButNotPostulates xs) = getRange . head $ xs
+ getRange (Codata r) = r
+ getRange (DeclarationPanic _) = noRange
+ getRange (UselessPrivate r) = r
+ getRange (UselessAbstract r) = r
+ getRange (UselessInstance r) = r
+ getRange (WrongContentBlock _ r) = r
+ getRange (InvalidTerminationCheckPragma r) = r
+ getRange (InvalidMeasureMutual r) = r
+ getRange (PragmaNoTerminationCheck r) = r
+ getRange (InvalidCatchallPragma r) = r
+ getRange (UnquoteDefRequiresSignature x) = getRange x
+ getRange (BadMacroDef d) = getRange d
+ getRange (InvalidNoPositivityCheckPragma r) = r
instance HasRange NiceDeclaration where
- getRange (Axiom r _ _ _ _ _ _) = r
+ getRange (Axiom r _ _ _ _ _ _ _ _) = r
getRange (NiceField r _ _ _ _ _ _) = r
getRange (NiceMutual r _ _ _) = r
getRange (NiceModule r _ _ _ _ _ ) = r
@@ -218,12 +246,12 @@ instance HasRange NiceDeclaration where
getRange (NiceImport r _ _ _ _) = r
getRange (NicePragma r _) = r
getRange (PrimitiveFunction r _ _ _ _ _) = r
- getRange (FunSig r _ _ _ _ _ _ _ _) = r
+ getRange (FunSig r _ _ _ _ _ _ _ _ _) = r
getRange (FunDef r _ _ _ _ _ _) = r
getRange (DataDef r _ _ _ _ _ _) = r
getRange (RecDef r _ _ _ _ _ _ _ _ _) = r
- getRange (NiceRecSig r _ _ _ _ _ _) = r
- getRange (NiceDataSig r _ _ _ _ _ _) = r
+ getRange (NiceRecSig r _ _ _ _ _ _ _) = r
+ getRange (NiceDataSig r _ _ _ _ _ _ _) = r
getRange (NicePatternSyn r _ _ _ _) = r
getRange (NiceFunClause r _ _ _ _ _) = r
getRange (NiceUnquoteDecl r _ _ _ _ _ _ _) = r
@@ -240,7 +268,9 @@ instance Pretty DeclarationException where
, vcat $ map f xs
]
where
- f (x, fs) = pretty x <> text ": " <+> fsep (map pretty fs)
+ f (x, fs) = pretty x Pretty.<> text ": " <+> fsep (map pretty fs)
+ pretty (MultiplePolarityPragmas xs) = fsep $
+ pwords "Multiple polarity pragmas for" ++ map pretty xs
pretty (InvalidName x) = fsep $
pwords "Invalid name:" ++ [pretty x]
pretty (DuplicateDefinition x) = fsep $
@@ -266,6 +296,10 @@ instance Pretty DeclarationException where
]
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
+ pretty (UnknownNamesInPolarityPragmas xs) = fsep $
+ pwords "The following names are not declared in the same scope as their polarity pragmas (they could for instance be out of scope, imported from another module, or declared in a super module):" ++ map pretty xs
+ pretty (PolarityPragmasButNotPostulates xs) = fsep $
+ pwords "Polarity pragmas have been given for the following identifiers which are not postulates:" ++ map pretty xs
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."
pretty (UselessAbstract _) = fsep $
@@ -407,18 +441,30 @@ type Nice = StateT NiceEnv (Either DeclarationException)
data NiceEnv = NiceEnv
{ _loneSigs :: LoneSigs
-- ^ Lone type signatures that wait for their definition.
+ , _termChk :: TerminationCheck
+ -- ^ Termination checking pragma waiting for a definition.
+ , _posChk :: PositivityCheck
+ -- ^ Positivity checking pragma waiting for a definition.
+ , _catchall :: Catchall
+ -- ^ Catchall pragma waiting for a function clause.
, fixs :: Fixities
+ , pols :: Polarities
}
-type LoneSigs = Map Name DataRecOrFun
-type Fixities = Map Name Fixity'
+type LoneSigs = Map Name DataRecOrFun
+type Fixities = Map Name Fixity'
+type Polarities = Map Name [Occurrence]
-- | Initial nicifier state.
initNiceEnv :: NiceEnv
initNiceEnv = NiceEnv
{ _loneSigs = empty
+ , _termChk = TerminationCheck
+ , _posChk = True
+ , _catchall = False
, fixs = empty
+ , pols = empty
}
-- * Handling the lone signatures, stored to infer mutual blocks.
@@ -460,11 +506,64 @@ checkLoneSigs xs =
[] -> return ()
(x, _):_ -> throwError $ MissingDefinition x
+-- | Lens for field '_termChk'.
+
+terminationCheckPragma :: Lens' TerminationCheck NiceEnv
+terminationCheckPragma f e = f (_termChk e) <&> \ s -> e { _termChk = s }
+
+withTerminationCheckPragma :: TerminationCheck -> Nice a -> Nice a
+withTerminationCheckPragma tc f = do
+ tc_old <- use terminationCheckPragma
+ terminationCheckPragma .= tc
+ result <- f
+ terminationCheckPragma .= tc_old
+ return result
+
+-- | Lens for field '_posChk'.
+
+positivityCheckPragma :: Lens' PositivityCheck NiceEnv
+positivityCheckPragma f e = f (_posChk e) <&> \ s -> e { _posChk = s }
+
+withPositivityCheckPragma :: PositivityCheck -> Nice a -> Nice a
+withPositivityCheckPragma pc f = do
+ pc_old <- use positivityCheckPragma
+ positivityCheckPragma .= pc
+ result <- f
+ positivityCheckPragma .= pc_old
+ return result
+
+-- | Lens for field '_catchall'.
+
+catchallPragma :: Lens' Catchall NiceEnv
+catchallPragma f e = f (_catchall e) <&> \ s -> e { _catchall = s }
+
+-- | Get current catchall pragma, and reset it for the next clause.
+
+popCatchallPragma :: Nice Catchall
+popCatchallPragma = do
+ ca <- use catchallPragma
+ catchallPragma .= False
+ return ca
+
+withCatchallPragma :: Catchall -> Nice a -> Nice a
+withCatchallPragma ca f = do
+ ca_old <- use catchallPragma
+ catchallPragma .= ca
+ result <- f
+ catchallPragma .= ca_old
+ return result
+
-- | Check whether name is not "_" and return its fixity.
getFixity :: Name -> Nice Fixity'
-getFixity x = do
- when (isUnderscore x) $ throwError $ InvalidName x
- Map.findWithDefault noFixity' x <$> gets fixs -- WAS: defaultFixity'
+getFixity x = Map.findWithDefault noFixity' x <$> gets fixs -- WAS: defaultFixity'
+
+-- | Fail if the name is @_@. Otherwise the name's polarity, if any,
+-- is removed from the state and returned.
+getPolarity :: Name -> Nice (Maybe [Occurrence])
+getPolarity x = do
+ p <- gets (Map.lookup x . pols)
+ modify (\s -> s { pols = Map.delete x (pols s) })
+ return p
runNice :: Nice a -> Either DeclarationException a
runNice nice = nice `evalStateT` initNiceEnv
@@ -476,12 +575,12 @@ data DeclKind
deriving (Eq, Show)
declKind :: NiceDeclaration -> DeclKind
-declKind (FunSig _ _ _ _ _ _ tc x _) = LoneSig (FunName tc) x
-declKind (NiceRecSig _ _ _ x pars _ pc) = LoneSig (RecName pc $ parameters pars) x
-declKind (NiceDataSig _ _ _ x pars _ pc) = LoneSig (DataName pc $ parameters pars) x
+declKind (FunSig _ _ _ _ _ _ _ tc x _) = LoneSig (FunName tc) x
+declKind (NiceRecSig _ _ _ _ pc x pars _) = LoneSig (RecName pc $ parameters pars) x
+declKind (NiceDataSig _ _ _ _ pc x pars _)= LoneSig (DataName pc $ parameters pars) x
declKind (FunDef _ _ _ _ tc x _) = LoneDefs (FunName tc) [x]
-declKind (DataDef _ _ _ x pars pc _) = LoneDefs (DataName pc $ parameters pars) [x]
-declKind (RecDef _ _ _ x _ _ _ pars pc _) = LoneDefs (RecName pc $ parameters pars) [x]
+declKind (DataDef _ _ _ pc x pars _) = LoneDefs (DataName pc $ parameters pars) [x]
+declKind (RecDef _ _ _ pc x _ _ _ pars _) = LoneDefs (RecName pc $ parameters pars) [x]
declKind (NiceUnquoteDef _ _ _ _ tc xs _) = LoneDefs (FunName tc) xs
declKind Axiom{} = OtherDecl
declKind NiceField{} = OtherDecl
@@ -507,15 +606,27 @@ parameters = List.concat . List.map numP where
niceDeclarations :: [Declaration] -> Nice [NiceDeclaration]
niceDeclarations ds = do
-- Get fixity and syntax declarations.
- fixs <- fixities ds
- case Map.keys fixs \\ concatMap declaredNames ds of
+ (fixs, polarities) <- fixitiesAndPolarities ds
+ let declared = Set.fromList (concatMap declaredNames ds)
+ unknownFixs = Map.keysSet fixs Set.\\ declared
+ unknownPols = Map.keysSet polarities Set.\\ declared
+ case (Set.null unknownFixs, Set.null unknownPols) of
-- If we have fixity/syntax decls for names not declared
-- in the current scope, fail.
- xs@(_:_) -> throwError $ UnknownNamesInFixityDecl xs
- [] -> localState $ do
- -- Run the nicifier in an initial environment of fixity decls.
- put $ initNiceEnv { fixs = fixs }
+ (False, _) -> throwError $ UnknownNamesInFixityDecl
+ (Set.toList unknownFixs)
+ -- Fail if there are polarity pragmas with undeclared names.
+ (_, False) -> throwError $ UnknownNamesInPolarityPragmas
+ (Set.toList unknownPols)
+ (True, True) -> localState $ do
+ -- Run the nicifier in an initial environment of fixity decls
+ -- and polarities.
+ put $ initNiceEnv { fixs = fixs, pols = polarities }
ds <- nice ds
+ -- Check that every polarity pragma was used.
+ unusedPolarities <- gets (Map.keys . pols)
+ unless (null unusedPolarities) $ do
+ throwError $ PolarityPragmasButNotPostulates unusedPolarities
-- Check that every signature got its definition.
checkLoneSigs . Map.toList =<< use loneSigs
-- Note that loneSigs is ensured to be empty.
@@ -541,7 +652,7 @@ niceDeclarations ds = do
PatternSyn _ x _ _ -> [x]
Mutual _ ds -> concatMap declaredNames ds
Abstract _ ds -> concatMap declaredNames ds
- Private _ ds -> concatMap declaredNames ds
+ Private _ _ ds -> concatMap declaredNames ds
InstanceB _ ds -> concatMap declaredNames ds
Macro _ ds -> concatMap declaredNames ds
Postulate _ ds -> concatMap declaredNames ds
@@ -573,7 +684,7 @@ niceDeclarations ds = do
-- block. See Issue 1760.
let prefix :: [NiceDeclaration] -> [NiceDeclaration]
prefix = case (d, ds0) of
- (NiceRecSig{}, [r@(RecDef _ _ _ _ _ _ _ _ True _)]) -> ([d, r] ++)
+ (NiceRecSig{}, [r@(RecDef _ _ _ True _ _ _ _ _ _)]) -> ([d, r] ++)
_ ->
(NiceMutual (getRange (d : ds0)) tc (and pcs) (d : ds0) :)
@@ -607,116 +718,137 @@ niceDeclarations ds = do
nice :: [Declaration] -> Nice [NiceDeclaration]
nice [] = return []
+ nice ds = do
+ (xs , ys) <- nice1 ds
+ (xs ++) <$> nice ys
+
+ nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
+ nice1 [] = __IMPOSSIBLE__
+ nice1 (d:ds) = case d of
+
+ (TypeSig info x t) -> do
+ termCheck <- use terminationCheckPragma
+ fx <- getFixity x
+ -- register x as lone type signature, to recognize clauses later
+ addLoneSig x (FunName termCheck)
+ return ([FunSig (getRange d) fx PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck x t] , ds)
+
+ (FunClause lhs _ _ _) -> do
+ termCheck <- use terminationCheckPragma
+ catchall <- popCatchallPragma
+ 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
+ case [ (x, (fits, rest))
+ | x <- xs
+ , let (fits, rest) =
+ -- Anonymous declarations only have 1 clause each!
+ if isNoName x then ([d], ds)
+ else span (couldBeFunClauseOf (Map.lookup x fixs) x) (d : ds)
+ , not (null fits)
+ ] of
- nice (Pragma (TerminationCheckPragma r NoTerminationCheck) : _) =
- throwError $ PragmaNoTerminationCheck r
-
- nice (Pragma (TerminationCheckPragma r tc) : ds@(Mutual{} : _)) | notMeasure tc = do
- ds <- nice ds
- case ds of
- NiceMutual r _ pc ds' : ds -> return $ NiceMutual r tc pc ds' : ds
- _ -> __IMPOSSIBLE__
-
- nice (Pragma (TerminationCheckPragma r tc) : d@TypeSig{} : ds) =
- niceTypeSig tc d ds
-
- nice (Pragma (TerminationCheckPragma r tc) : d@FunClause{} : ds) | notMeasure tc =
- niceFunClause tc False d ds
-
- nice (Pragma (TerminationCheckPragma r tc) : ds@(UnquoteDecl{} : _)) | notMeasure tc = do
- NiceUnquoteDecl r f p a i _ x e : ds <- nice ds
- return $ NiceUnquoteDecl r f p a i tc x e : ds
-
- nice (Pragma (TerminationCheckPragma r tc) : d@(Pragma (NoPositivityCheckPragma _)) : ds@(Mutual{} : _)) | notMeasure tc = do
- ds <- nice (d : ds)
- case ds of
- NiceMutual r _ pc ds' : ds -> return $ NiceMutual r tc pc ds' : ds
- _ -> __IMPOSSIBLE__
-
- nice (Pragma (CatchallPragma r) : d@FunClause{} : ds) =
- niceFunClause TerminationCheck True d ds
-
- nice (d@TypeSig{} : Pragma (TerminationCheckPragma r (TerminationMeasure _ x)) : ds) =
- niceTypeSig (TerminationMeasure r x) d ds
-
- -- nice (Pragma (MeasurePragma r x) : d@FunClause{} : ds) =
- -- niceFunClause (TerminationMeasure r x) d ds
-
- nice (Pragma (NoPositivityCheckPragma _) : ds@(Mutual{} : _)) = do
- ds <- nice ds
- case ds of
- NiceMutual r tc _ ds' : ds -> return $ NiceMutual r tc False ds' : ds
- _ -> __IMPOSSIBLE__
-
- nice (Pragma (NoPositivityCheckPragma _) : d@(Data _ Inductive _ _ _ _) : ds) =
- niceDataDef False d ds
-
- nice (Pragma (NoPositivityCheckPragma _) : d@(DataSig _ Inductive _ _ _) : ds) =
- niceDataSig False d ds
-
- nice (Pragma (NoPositivityCheckPragma _) : d@Record{} : ds) =
- niceRecord False d ds
+ -- case: clauses match none of the sigs
+ [] -> case lhs of
+ -- Subcase: The lhs is single identifier (potentially anonymous).
+ -- Treat it as a function clause without a type signature.
+ LHS p [] [] [] | Just x <- isSingleIdentifierP p -> do
+ d <- mkFunDef defaultArgInfo termCheck x Nothing [d] -- fun def without type signature is relevant
+ return (d , ds)
+ -- Subcase: The lhs is a proper pattern.
+ -- This could be a let-pattern binding. Pass it on.
+ -- A missing type signature error might be raise in ConcreteToAbstract
+ _ -> do
+ return ([NiceFunClause (getRange d) PublicAccess ConcreteDef termCheck catchall d] , ds)
- nice (Pragma (NoPositivityCheckPragma _) : d@RecordSig{} : ds) =
- niceRecordSig False d ds
+ -- case: clauses match exactly one of the sigs
+ [(x,(fits,rest))] -> do
+ removeLoneSig x
+ cs <- mkClauses x (expandEllipsis fits) False
+ fx <- getFixity x
+ return ([FunDef (getRange fits) fits fx ConcreteDef termCheck x cs] , rest)
- nice (Pragma (NoPositivityCheckPragma _) : d@(Pragma (TerminationCheckPragma _ _)) : ds@(Mutual{} : _)) = do
- ds <- nice (d : ds)
- case ds of
- NiceMutual r tc _ ds' : ds -> return $ NiceMutual r tc False ds' : ds
- _ -> __IMPOSSIBLE__
+ -- case: clauses match more than one sigs (ambiguity)
+ l -> throwError $ AmbiguousFunClauses lhs $ reverse $ map fst l -- "ambiguous function clause; cannot assign it uniquely to one type signature"
- nice (d:ds) = do
- case d of
- TypeSig{} -> niceTypeSig TerminationCheck d ds
- FunClause{} -> niceFunClause TerminationCheck False d ds
- Field{} -> (++) <$> niceAxioms FieldBlock [ d ] <*> nice ds
+ Field{} -> (,ds) <$> niceAxioms FieldBlock [ d ]
DataSig r CoInductive _ _ _ -> throwError (Codata r)
Data r CoInductive _ _ _ _ -> throwError (Codata r)
- d@(DataSig _ Inductive _ _ _) -> niceDataSig True d ds
- d@(Data _ Inductive _ _ _ _) -> niceDataDef True d ds
- d@RecordSig{} -> niceRecordSig True d ds
- d@Record{} -> niceRecord True d ds
+
+ (DataSig r Inductive x tel t) -> do
+ pc <- use positivityCheckPragma
+ addLoneSig x (DataName pc $ parameters tel)
+ (,) <$> dataOrRec pc DataDef NiceDataSig (niceAxioms DataBlock) r x tel (Just t) Nothing
+ <*> return ds
+
+ (Data r Inductive x tel t cs) -> do
+ pc <- use positivityCheckPragma
+ t <- defaultTypeSig (DataName pc $ parameters tel) x t
+ (,) <$> dataOrRec pc DataDef NiceDataSig (niceAxioms DataBlock) r x tel t (Just cs)
+ <*> return ds
+
+ (RecordSig r x tel t) -> do
+ pc <- use positivityCheckPragma
+ addLoneSig x (RecName pc $ parameters tel)
+ fx <- getFixity x
+ return ([NiceRecSig r fx PublicAccess ConcreteDef pc x tel t] , ds)
+
+ (Record r x i e c tel t cs) -> do
+ pc <- use positivityCheckPragma
+ t <- defaultTypeSig (RecName pc $ parameters tel) x t
+ c <- traverse (\(cname, cinst) -> do fix <- getFixity cname; return (ThingWithFixity cname fix, cinst)) c
+ (,) <$> dataOrRec pc (\ r f a pc x tel cs -> RecDef r f a pc x i e c tel cs) NiceRecSig
+ niceDeclarations r x tel t (Just cs)
+ <*> return ds
Mutual r ds' ->
- (:) <$> (mkOldMutual r =<< nice ds') <*> nice ds
+ (,ds) <$> (singleton <$> (mkOldMutual r =<< nice ds'))
Abstract r ds' ->
- (++) <$> (abstractBlock r =<< nice ds') <*> nice ds
+ (,ds) <$> (abstractBlock r =<< nice ds')
- Private r ds' ->
- (++) <$> (privateBlock r =<< nice ds') <*> nice ds
+ Private r o ds' ->
+ (,ds) <$> (privateBlock r o =<< nice ds')
InstanceB r ds' ->
- (++) <$> (instanceBlock r =<< nice ds') <*> nice ds
+ (,ds) <$> (instanceBlock r =<< nice ds')
Macro r ds' ->
- (++) <$> (macroBlock r =<< nice ds') <*> nice ds
+ (,ds) <$> (macroBlock r =<< nice ds')
- Postulate _ ds' -> (++) <$> niceAxioms PostulateBlock ds' <*> nice ds
+ Postulate _ ds' ->
+ (,ds) <$> (mapM setPolarity =<< niceAxioms PostulateBlock ds')
+ where
+ setPolarity (Axiom r f acc a i arg Nothing x e) = do
+ mp <- getPolarity x
+ return (Axiom r f acc a i arg mp x e)
+ setPolarity (Axiom _ _ _ _ _ _ (Just _) _ _) = __IMPOSSIBLE__
+ setPolarity d = return d
- Primitive _ ds' -> (++) <$> (map toPrim <$> niceAxioms PrimitiveBlock ds') <*> nice ds
+ Primitive _ ds' -> (,ds) <$> (map toPrim <$> niceAxioms PrimitiveBlock ds')
- Module r x tel ds' ->
- (NiceModule r PublicAccess ConcreteDef x tel ds' :) <$> nice ds
+ Module r x tel ds' -> return $
+ ([NiceModule r PublicAccess ConcreteDef x tel ds'] , ds)
- ModuleMacro r x modapp op is ->
- (NiceModuleMacro r PublicAccess x modapp op is :)
- <$> nice ds
+ ModuleMacro r x modapp op is -> return $
+ ([NiceModuleMacro r PublicAccess x modapp op is] , ds)
- -- Fixity and syntax declarations have been looked at already.
- Infix _ _ -> nice ds
- Syntax _ _ -> nice ds
+ -- Fixity and syntax declarations and polarity pragmas have
+ -- already been processed.
+ Infix _ _ -> return ([], ds)
+ Syntax _ _ -> return ([], ds)
PatternSyn r n as p -> do
fx <- getFixity n
- (NicePatternSyn r fx n as p :) <$> nice ds
- Open r x is -> (NiceOpen r x is :) <$> nice ds
- Import r x as op is -> (NiceImport r x as op is :) <$> nice ds
+ return ([NicePatternSyn r fx n as p] , ds)
+ Open r x is -> return ([NiceOpen r x is] , ds)
+ Import r x as op is -> return ([NiceImport r x as op is] , ds)
UnquoteDecl r xs e -> do
fxs <- mapM getFixity xs
- (NiceUnquoteDecl r fxs PublicAccess NotInstanceDef ConcreteDef TerminationCheck xs e :) <$> nice ds
+ tc <- use terminationCheckPragma
+ return ([NiceUnquoteDecl r fxs PublicAccess ConcreteDef NotInstanceDef tc xs e] , ds)
UnquoteDef r xs e -> do
fxs <- mapM getFixity xs
@@ -725,105 +857,85 @@ niceDeclarations ds = do
if null missing
then do
mapM_ removeLoneSig xs
- (NiceUnquoteDef r fxs PublicAccess ConcreteDef TerminationCheck xs e :) <$> nice ds
+ return ([NiceUnquoteDef r fxs PublicAccess ConcreteDef TerminationCheck xs e] , ds)
else throwError $ UnquoteDefRequiresSignature missing
- Pragma (TerminationCheckPragma r NoTerminationCheck) ->
- throwError $ PragmaNoTerminationCheck r
- Pragma (TerminationCheckPragma r _) ->
- throwError $ InvalidTerminationCheckPragma r
-
- Pragma (CatchallPragma r) ->
- throwError $ InvalidCatchallPragma r
-
- Pragma (NoPositivityCheckPragma r) ->
- throwError $ InvalidNoPositivityCheckPragma r
-
- Pragma p -> (NicePragma (getRange p) p :) <$> nice ds
-
- niceFunClause :: TerminationCheck -> Catchall -> Declaration -> [Declaration] -> Nice [NiceDeclaration]
- niceFunClause termCheck catchall d@(FunClause lhs _ _ _) ds = do
- 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
- case [ (x, (fits, rest))
- | x <- xs
- , let (fits, rest) =
- span (couldBeFunClauseOf (Map.lookup x fixs) x) (d : ds)
- , not (null fits)
- ] of
+ Pragma p -> nicePragma p ds
- -- case: clauses match none of the sigs
- [] -> case lhs of
- -- Subcase: The lhs is single identifier.
- -- Treat it as a function clause without a type signature.
- LHS p [] [] [] | IdentP (QName x) <- removeSingletonRawAppP p -> do
- ds <- nice ds
- d <- mkFunDef defaultArgInfo termCheck x Nothing [d] -- fun def without type signature is relevant
- return $ d ++ ds
- -- Subcase: The lhs is a proper pattern.
- -- This could be a let-pattern binding. Pass it on.
- -- A missing type signature error might be raise in ConcreteToAbstract
- _ -> do
- ds <- nice ds
- return $ NiceFunClause (getRange d) PublicAccess ConcreteDef termCheck catchall d : ds
+ nicePragma :: Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
- -- case: clauses match exactly one of the sigs
- [(x,(fits,rest))] -> do
- removeLoneSig x
- cs <- mkClauses x (expandEllipsis fits) False
- ds1 <- nice rest
- fx <- getFixity x
- d <- return $ FunDef (getRange fits) fits fx ConcreteDef termCheck x cs
- return $ d : ds1
+ nicePragma (TerminationCheckPragma r (TerminationMeasure _ x)) ds =
+ if canHaveTerminationMeasure ds then
+ withTerminationCheckPragma (TerminationMeasure r x) $ nice1 ds
+ else
+ throwError $ InvalidTerminationCheckPragma r
- -- case: clauses match more than one sigs (ambiguity)
- l -> throwError $ AmbiguousFunClauses lhs $ reverse $ map fst l -- "ambiguous function clause; cannot assign it uniquely to one type signature"
- niceFunClause _ _ _ _ = __IMPOSSIBLE__
+ nicePragma (TerminationCheckPragma r NoTerminationCheck) ds =
+ throwError $ PragmaNoTerminationCheck r
- 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 x (FunName termCheck)
- ds <- nice ds
- return $ FunSig (getRange d) fx PublicAccess NotInstanceDef NotMacroDef info termCheck x t : ds
- niceTypeSig _ _ _ = __IMPOSSIBLE__
-
- niceDataDef :: PositivityCheck -> Declaration -> [Declaration] ->
- Nice [NiceDeclaration]
- niceDataDef pc (Data r Inductive x tel t cs) ds = do
- t <- defaultTypeSig (DataName pc $ parameters tel) x t
- (++) <$> dataOrRec pc DataDef NiceDataSig (niceAxioms DataBlock) r x tel t (Just cs)
- <*> nice ds
- niceDataDef _ _ _ = __IMPOSSIBLE__
-
- niceDataSig :: PositivityCheck -> Declaration -> [Declaration] ->
- Nice [NiceDeclaration]
- niceDataSig pc (DataSig r Inductive x tel t) ds = do
- addLoneSig x (DataName pc $ parameters tel)
- (++) <$> dataOrRec pc DataDef NiceDataSig (niceAxioms DataBlock) r x tel (Just t) Nothing
- <*> nice ds
- niceDataSig _ _ _ = __IMPOSSIBLE__
-
- niceRecord :: PositivityCheck -> Declaration -> [Declaration] ->
- Nice [NiceDeclaration]
- niceRecord pc (Record r x i e c tel t cs) ds = do
- t <- defaultTypeSig (RecName pc $ parameters tel) x t
- c <- traverse (\(cname, cinst) -> do fix <- getFixity cname; return (ThingWithFixity cname fix, cinst)) c
- (++) <$> dataOrRec pc (\x1 x2 x3 x4 -> RecDef x1 x2 x3 x4 i e c) NiceRecSig
- niceDeclarations r x tel t (Just cs)
- <*> nice ds
- niceRecord _ _ _ = __IMPOSSIBLE__
-
- niceRecordSig :: PositivityCheck -> Declaration -> [Declaration] ->
- Nice [NiceDeclaration]
- niceRecordSig pc (RecordSig r x tel t) ds = do
- addLoneSig x (RecName pc $ parameters tel)
- fx <- getFixity x
- (NiceRecSig r fx PublicAccess x tel t pc :) <$> nice ds
- niceRecordSig _ _ _ = __IMPOSSIBLE__
+ nicePragma (TerminationCheckPragma r tc) ds =
+ if canHaveTerminationCheckPragma ds then
+ withTerminationCheckPragma tc $ nice1 ds
+ else
+ throwError $ InvalidTerminationCheckPragma r
+
+ nicePragma (CatchallPragma r) ds =
+ if canHaveCatchallPragma ds then
+ withCatchallPragma True $ nice1 ds
+ else
+ throwError $ InvalidCatchallPragma r
+
+ nicePragma (NoPositivityCheckPragma r) ds =
+ if canHaveNoPositivityCheckPragma ds then
+ withPositivityCheckPragma False $ nice1 ds
+ else
+ throwError $ InvalidNoPositivityCheckPragma r
+
+ nicePragma (PolarityPragma{}) ds = return ([], ds)
+
+ nicePragma p ds = return ([NicePragma (getRange p) p], ds)
+
+ canHaveTerminationMeasure :: [Declaration] -> Bool
+ canHaveTerminationMeasure [] = False
+ canHaveTerminationMeasure (d:ds) = case d of
+ TypeSig{} -> True
+ (Pragma p) | isAttachedPragma p -> canHaveTerminationMeasure ds
+ _ -> False
+
+ canHaveTerminationCheckPragma :: [Declaration] -> Bool
+ canHaveTerminationCheckPragma [] = False
+ canHaveTerminationCheckPragma (d:ds) = case d of
+ Mutual{} -> True
+ TypeSig{} -> True
+ FunClause{} -> True
+ UnquoteDecl{} -> True
+ (Pragma p) | isAttachedPragma p -> canHaveTerminationCheckPragma ds
+ _ -> False
+
+ canHaveCatchallPragma :: [Declaration] -> Bool
+ canHaveCatchallPragma [] = False
+ canHaveCatchallPragma (d:ds) = case d of
+ FunClause{} -> True
+ (Pragma p) | isAttachedPragma p -> canHaveCatchallPragma ds
+ _ -> False
+
+ canHaveNoPositivityCheckPragma :: [Declaration] -> Bool
+ canHaveNoPositivityCheckPragma [] = False
+ canHaveNoPositivityCheckPragma (d:ds) = case d of
+ Mutual{} -> True
+ (Data _ Inductive _ _ _ _) -> True
+ (DataSig _ Inductive _ _ _) -> True
+ Record{} -> True
+ RecordSig{} -> True
+ (Pragma p) | isAttachedPragma p -> canHaveNoPositivityCheckPragma ds
+ _ -> False
+
+ isAttachedPragma :: Pragma -> Bool
+ isAttachedPragma p = case p of
+ TerminationCheckPragma{} -> True
+ CatchallPragma{} -> True
+ NoPositivityCheckPragma{} -> True
+ _ -> False
-- We could add a default type signature here, but at the moment we can't
-- infer the type of a record or datatype, so better to just fail here.
@@ -839,10 +951,10 @@ niceDeclarations ds = do
dataOrRec :: forall a .
PositivityCheck ->
- (Range -> Fixity' -> IsAbstract -> Name -> [LamBinding] ->
- PositivityCheck -> [NiceConstructor] -> NiceDeclaration) ->
- (Range -> Fixity' -> Access -> Name -> [LamBinding] -> Expr ->
- PositivityCheck -> NiceDeclaration) ->
+ (Range -> Fixity' -> IsAbstract -> PositivityCheck -> Name -> [LamBinding] ->
+ [NiceConstructor] -> NiceDeclaration) ->
+ (Range -> Fixity' -> Access -> IsAbstract -> PositivityCheck -> Name -> [LamBinding] -> Expr ->
+ NiceDeclaration) ->
([a] -> Nice [NiceDeclaration]) ->
Range ->
Name ->
@@ -854,8 +966,8 @@ niceDeclarations ds = do
mds <- traverse niceD mcs
f <- getFixity x
return $ catMaybes $
- [ mt <&> \ t -> mkSig (fuseRange x t) f PublicAccess x tel t pc
- , mkDef r f ConcreteDef x (concatMap dropType tel) pc <$> mds
+ [ mt <&> \ t -> mkSig (fuseRange x t) f PublicAccess ConcreteDef pc x tel t
+ , mkDef r f ConcreteDef pc x (concatMap dropType tel) <$> mds
]
where
dropType :: LamBinding -> [LamBinding]
@@ -872,10 +984,10 @@ niceDeclarations ds = do
niceAxiom b d = case d of
TypeSig rel x t -> do
fx <- getFixity x
- return [ Axiom (getRange d) fx PublicAccess NotInstanceDef rel x t ]
+ return [ Axiom (getRange d) fx PublicAccess ConcreteDef NotInstanceDef rel Nothing x t ]
Field i x argt -> do
fx <- getFixity x
- return [ NiceField (getRange d) i fx PublicAccess ConcreteDef x argt ]
+ return [ NiceField (getRange d) fx PublicAccess ConcreteDef i x argt ]
InstanceB r decls -> do
instanceBlock r =<< niceAxioms InstanceBlock decls
Pragma p@(RewritePragma r _) -> do
@@ -883,14 +995,14 @@ niceDeclarations ds = do
_ -> throwError $ WrongContentBlock b $ getRange d
toPrim :: NiceDeclaration -> NiceDeclaration
- toPrim (Axiom r f a i rel x t) = PrimitiveFunction r f a ConcreteDef x t
- toPrim _ = __IMPOSSIBLE__
+ toPrim (Axiom r f p a i rel Nothing x t) = PrimitiveFunction r f p a x t
+ toPrim _ = __IMPOSSIBLE__
-- Create a function definition.
mkFunDef info termCheck x mt ds0 = do
cs <- mkClauses x (expandEllipsis ds0) False
f <- getFixity x
- return [ FunSig (fuseRange x t) f PublicAccess NotInstanceDef NotMacroDef info termCheck x t
+ return [ FunSig (fuseRange x t) f PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck x t
, FunDef (getRange ds0) ds0 f ConcreteDef termCheck x cs ]
where
t = case mt of
@@ -905,7 +1017,7 @@ niceDeclarations ds = do
expandEllipsis (d@(FunClause Ellipsis{} _ _ _) : ds) =
d : expandEllipsis ds
expandEllipsis (d@(FunClause lhs@(LHS p ps _ _) _ _ _) : ds) =
- d : expand p ps ds
+ d : expand (setInserted p) (map setInserted ps) ds
where
expand _ _ [] = []
expand p ps (d@(Pragma (CatchallPragma r)) : ds) = d : expand p ps ds
@@ -920,6 +1032,23 @@ niceDeclarations ds = do
expand _ _ (_ : ds) = __IMPOSSIBLE__
expandEllipsis (_ : ds) = __IMPOSSIBLE__
+ setInserted :: Pattern -> Pattern
+ setInserted p = case p of
+ IdentP{} -> p
+ QuoteP{} -> p
+ AppP p q -> AppP (setInserted p) (fmap (fmap setInserted) q)
+ RawAppP r ps -> RawAppP r (map setInserted ps)
+ OpAppP r c ns ps -> OpAppP r c ns (map (fmap $ fmap setInserted) ps)
+ HiddenP r p -> HiddenP r (fmap setInserted p)
+ InstanceP r p -> InstanceP r (fmap setInserted p)
+ ParenP r p -> ParenP r (setInserted p)
+ WildP{} -> p
+ AbsurdP{} -> p
+ AsP r n p -> AsP r n (setInserted p)
+ DotP r _ e -> DotP r Inserted e
+ LitP{} -> p
+ RecP r fs -> RecP r (map (fmap setInserted) fs)
+
-- Turn function clauses into nice function clauses.
mkClauses :: Name -> [Declaration] -> Catchall -> Nice [Clause]
mkClauses _ [] _ = return []
@@ -998,9 +1127,14 @@ niceDeclarations ds = do
-- -- it's part of the current definition
-- isFunClauseOf _ _ = False
+ isSingleIdentifierP :: Pattern -> Maybe Name
+ isSingleIdentifierP p = case removeSingletonRawAppP p of
+ IdentP (QName x) -> Just x
+ WildP r -> Just $ noName r
+ _ -> Nothing
+
removeSingletonRawAppP :: Pattern -> Pattern
- removeSingletonRawAppP p =
- case p of
+ removeSingletonRawAppP p = case p of
RawAppP _ [p'] -> removeSingletonRawAppP p'
ParenP _ p' -> removeSingletonRawAppP p'
_ -> p
@@ -1015,11 +1149,13 @@ niceDeclarations ds = do
[] -> return ()
(NiceFunClause _ _ _ _ s_ (FunClause lhs _ _ _)):_ -> throwError $ MissingTypeSignature lhs
d:_ -> throwError $ NotAllowedInMutual d
+ tc0 <- use terminationCheckPragma
let tcs = map termCheck ds
- tc <- combineTermChecks r tcs
+ tc <- combineTermChecks r (tc0:tcs)
+ pc0 <- use positivityCheckPragma
let pc :: PositivityCheck
- pc = all positivityCheckOldMutual ds
+ pc = pc0 && all positivityCheckOldMutual ds
return $ NiceMutual r tc pc $ sigs ++ other
where
@@ -1040,7 +1176,7 @@ niceDeclarations ds = do
-- Andreas, 2013-02-28 (issue 804):
-- do not termination check a mutual block if any of its
-- inner declarations comes with a {-# NO_TERMINATION_CHECK #-}
- termCheck (FunSig _ _ _ _ _ _ tc _ _) = tc
+ termCheck (FunSig _ _ _ _ _ _ _ tc _ _) = tc
termCheck (FunDef _ _ _ _ tc _ _) = tc
-- ASR (28 December 2015): Is this equation necessary?
termCheck (NiceMutual _ tc _ _) = __IMPOSSIBLE__
@@ -1065,11 +1201,11 @@ niceDeclarations ds = do
-- block if any of its inner declarations comes with a
-- NO_POSITIVITY_CHECK pragma. See Issue 1614.
positivityCheckOldMutual :: NiceDeclaration -> PositivityCheck
- positivityCheckOldMutual (DataDef _ _ _ _ _ pc _) = pc
- positivityCheckOldMutual (NiceDataSig _ _ _ _ _ _ pc) = pc
+ positivityCheckOldMutual (DataDef _ _ _ pc _ _ _) = pc
+ positivityCheckOldMutual (NiceDataSig _ _ _ _ pc _ _ _)= pc
positivityCheckOldMutual (NiceMutual _ _ pc _) = __IMPOSSIBLE__
- positivityCheckOldMutual (NiceRecSig _ _ _ _ _ _ pc) = pc
- positivityCheckOldMutual (RecDef _ _ _ _ _ _ _ _ pc _) = pc
+ positivityCheckOldMutual (NiceRecSig _ _ _ _ pc _ _ _) = pc
+ positivityCheckOldMutual (RecDef _ _ _ pc _ _ _ _ _ _) = pc
positivityCheckOldMutual _ = True
-- A mutual block cannot have a measure,
@@ -1077,101 +1213,16 @@ niceDeclarations ds = do
abstractBlock _ [] = return []
abstractBlock r ds = do
- let (ds', anyChange) = runChange $ mapM mkAbstract ds
+ let (ds', anyChange) = runChange $ mkAbstract ds
inherited = r == noRange
-- hack to avoid failing on inherited abstract blocks in where clauses
if anyChange || inherited then return ds' else throwError $ UselessAbstract r
- -- Make a declaration abstract
- mkAbstract :: Updater NiceDeclaration
- mkAbstract d =
- case d of
- NiceMutual r termCheck pc ds -> NiceMutual r termCheck pc <$> mapM mkAbstract ds
- FunDef r ds f a tc x cs -> (\ a -> FunDef r ds f a tc x) <$> setAbstract a <*> mapM mkAbstractClause cs
- DataDef r f a x ps pc cs -> (\ a -> DataDef r f a x ps pc) <$> setAbstract a <*> mapM mkAbstract cs
- RecDef r f a x i e c ps pc cs -> (\ a -> RecDef r f a x i e c ps pc) <$> setAbstract a <*> mapM mkAbstract cs
- NiceFunClause r p a termCheck catchall d -> (\ a -> NiceFunClause r p a termCheck catchall d) <$> setAbstract a
- -- no effect on fields or primitives, the InAbstract field there is unused
- NiceField r i f p _ x e -> return $ NiceField r i f p AbstractDef x e
- PrimitiveFunction r f p _ x e -> return $ PrimitiveFunction r f p AbstractDef x e
- NiceUnquoteDecl r f p i _ t x e -> return $ NiceUnquoteDecl r f p i AbstractDef t x e
- NiceUnquoteDef r f p _ t x e -> return $ NiceUnquoteDef r f p AbstractDef t x e
- NiceModule{} -> return d
- NiceModuleMacro{} -> return d
- Axiom{} -> return d
- NicePragma{} -> return d
- NiceOpen{} -> return d
- NiceImport{} -> return d
- FunSig{} -> return d
- NiceRecSig{} -> return d
- NiceDataSig{} -> return d
- NicePatternSyn{} -> return d
-
- setAbstract :: Updater IsAbstract
- setAbstract a = case a of
- AbstractDef -> return a
- ConcreteDef -> dirty $ AbstractDef
-
- mkAbstractClause :: Updater Clause
- mkAbstractClause (Clause x catchall lhs rhs wh with) = do
- wh <- mkAbstractWhere wh
- Clause x catchall lhs rhs wh <$> mapM mkAbstractClause with
-
- mkAbstractWhere :: Updater WhereClause
- mkAbstractWhere NoWhere = return $ NoWhere
- mkAbstractWhere (AnyWhere ds) = dirty $ AnyWhere [Abstract noRange ds]
- mkAbstractWhere (SomeWhere m ds) = dirty $SomeWhere m [Abstract noRange ds]
-
- privateBlock _ [] = return []
- privateBlock r ds = do
- let (ds', anyChange) = runChange $ mapM mkPrivate ds
- if anyChange then return ds' else throwError $ UselessPrivate r
-
- -- Make a declaration private.
- -- Andreas, 2012-11-17:
- -- Mark computation 'dirty' if there was a declaration that could be privatized.
- -- If no privatization is taking place, we want to complain about 'UselessPrivate'.
- -- Alternatively, we could only dirty if a non-private thing was privatized.
- -- Then, nested 'private's would sometimes also be complained about.
- mkPrivate :: Updater NiceDeclaration
- mkPrivate d =
- case d of
- Axiom r f p i rel x e -> (\ p -> Axiom r f p i rel x e) <$> setPrivate p
- NiceField r i f p a x e -> (\ p -> NiceField r i f p a x e) <$> setPrivate p
- PrimitiveFunction r f p a x e -> (\ p -> PrimitiveFunction r f p a x e) <$> setPrivate p
- NiceMutual r termCheck pc ds -> NiceMutual r termCheck pc <$> mapM mkPrivate ds
- NiceModule r p a x tel ds -> (\ p -> NiceModule r p a x tel ds) <$> setPrivate p
- NiceModuleMacro r p x ma op is -> (\ p -> NiceModuleMacro r p x ma op is) <$> setPrivate p
- FunSig r f p i m rel tc x e -> (\ p -> FunSig r f p i m rel tc x e) <$> setPrivate p
- NiceRecSig r f p x ls t pc -> (\ p -> NiceRecSig r f p x ls t pc) <$> setPrivate p
- NiceDataSig r f p x ls t pc -> (\ p -> NiceDataSig r f p x ls t pc) <$> setPrivate p
- NiceFunClause r p a termCheck catchall d -> (\ p -> NiceFunClause r p a termCheck catchall d) <$> setPrivate p
- NiceUnquoteDecl r f p i a t x e -> (\ p -> NiceUnquoteDecl r f p i a t x e) <$> setPrivate p
- NiceUnquoteDef r f p a t x e -> (\ p -> NiceUnquoteDef r f p a t x e) <$> setPrivate p
- NicePragma _ _ -> return $ d
- NiceOpen _ _ _ -> return $ d
- NiceImport _ _ _ _ _ -> return $ d
- FunDef{} -> return $ d
- DataDef{} -> return $ d
- RecDef{} -> return $ d
- NicePatternSyn _ _ _ _ _ -> return $ d
-
- setPrivate :: Updater Access
- setPrivate p = case p of
- PrivateAccess -> return p
- _ -> dirty $ PrivateAccess
-
- -- Andreas, 2012-11-22: Q: is this necessary?
- -- Are where clauses not always private?
- mkPrivateClause :: Updater Clause
- mkPrivateClause (Clause x catchall lhs rhs wh with) = do
- wh <- mkPrivateWhere wh
- Clause x catchall lhs rhs wh <$> mapM mkPrivateClause with
-
- mkPrivateWhere :: Updater WhereClause
- mkPrivateWhere NoWhere = return $ NoWhere
- mkPrivateWhere (AnyWhere ds) = dirty $ AnyWhere [Private (getRange ds) ds]
- mkPrivateWhere (SomeWhere m ds) = dirty $ SomeWhere m [Private (getRange ds) ds]
+ privateBlock _ _ [] = return []
+ privateBlock r o ds = do
+ let (ds', anyChange) = runChange $ mkPrivate o ds
+ if anyChange then return ds' else
+ if o == UserWritten then throwError $ UselessPrivate r else return ds -- no change!
instanceBlock _ [] = return []
instanceBlock r ds = do
@@ -1182,9 +1233,9 @@ niceDeclarations ds = do
mkInstance :: Updater NiceDeclaration
mkInstance d =
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 m rel tc x e -> (\ i -> FunSig r f p i m 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
+ Axiom r f p a i rel mp x e -> (\ i -> Axiom r f p a i rel mp x e) <$> setInstance i
+ FunSig r f p a i m rel tc x e -> (\ i -> FunSig r f p a i m rel tc x e) <$> setInstance i
+ NiceUnquoteDecl r f p a i tc x e -> (\ i -> NiceUnquoteDecl r f p a i tc x e) <$> setInstance i
NiceMutual{} -> return d
NiceFunClause{} -> return d
FunDef{} -> return d
@@ -1212,10 +1263,142 @@ niceDeclarations ds = do
mkMacro :: NiceDeclaration -> Nice NiceDeclaration
mkMacro d =
case d of
- FunSig r f p i _ rel tc x e -> return $ FunSig r f p i MacroDef rel tc x e
+ FunSig r f p a i _ rel tc x e -> return $ FunSig r f p a i MacroDef rel tc x e
FunDef{} -> return d
_ -> throwError (BadMacroDef d)
+-- | Make a declaration abstract.
+--
+-- Mark computation as 'dirty' if there was a declaration that could be made abstract.
+-- If no abstraction is taking place, we want to complain about 'UselessAbstract'.
+--
+-- Alternatively, we could only flag 'dirty' if a non-abstract thing was abstracted.
+-- Then, nested @abstract@s would sometimes also be complained about.
+
+class MakeAbstract a where
+ mkAbstract :: Updater a
+ default mkAbstract :: (Traversable f, MakeAbstract a', a ~ f a') => Updater a
+ mkAbstract = traverse mkAbstract
+
+instance MakeAbstract a => MakeAbstract [a] where
+ -- Default definition kicks in here!
+ -- But note that we still have to declare the instance!
+
+-- Leads to overlap with 'WhereClause':
+-- instance (Traversable f, MakeAbstract a) => MakeAbstract (f a) where
+-- mkAbstract = traverse mkAbstract
+
+instance MakeAbstract IsAbstract where
+ mkAbstract a = case a of
+ AbstractDef -> return a
+ ConcreteDef -> dirty $ AbstractDef
+
+instance MakeAbstract NiceDeclaration where
+ mkAbstract d =
+ case d of
+ NiceMutual r termCheck pc ds -> NiceMutual r termCheck pc <$> mkAbstract ds
+ FunDef r ds f a tc x cs -> (\ a -> FunDef r ds f a tc x) <$> mkAbstract a <*> mkAbstract cs
+ DataDef r f a pc x ps cs -> (\ a -> DataDef r f a pc x ps) <$> mkAbstract a <*> mkAbstract cs
+ RecDef r f a pc x i e c ps cs -> (\ a -> RecDef r f a pc x i e c ps) <$> mkAbstract a <*> mkAbstract cs
+ NiceFunClause r p a termCheck catchall d -> (\ a -> NiceFunClause r p a termCheck catchall d) <$> mkAbstract a
+ -- The following declarations have an @InAbstract@ field
+ -- but are not really definitions, so we do count them into
+ -- the declarations which can be made abstract
+ -- (thus, do not notify progress with @dirty@).
+ Axiom r f p a i rel mp x e -> return $ Axiom r f p AbstractDef i rel mp x e
+ FunSig r f p a i m rel tc x e -> return $ FunSig r f p AbstractDef i m rel tc x e
+ NiceRecSig r f p a pc x ls t -> return $ NiceRecSig r f p AbstractDef pc x ls t
+ NiceDataSig r f p a pc x ls t -> return $ NiceDataSig r f p AbstractDef pc x ls t
+ NiceField r f p _ i x e -> return $ NiceField r f p AbstractDef i x e
+ PrimitiveFunction r f p _ x e -> return $ PrimitiveFunction r f p AbstractDef x e
+ -- Andreas, 2016-07-17 it does have effect on unquoted defs.
+ -- Need to set updater state to dirty!
+ NiceUnquoteDecl r f p _ i t x e -> dirty $ NiceUnquoteDecl r f p AbstractDef i t x e
+ NiceUnquoteDef r f p _ t x e -> dirty $ NiceUnquoteDef r f p AbstractDef t x e
+ NiceModule{} -> return d
+ NiceModuleMacro{} -> return d
+ NicePragma{} -> return d
+ NiceOpen{} -> return d
+ NiceImport{} -> return d
+ NicePatternSyn{} -> return d
+
+instance MakeAbstract Clause where
+ mkAbstract (Clause x catchall lhs rhs wh with) = do
+ Clause x catchall lhs rhs <$> mkAbstract wh <*> mkAbstract with
+
+-- | Contents of a @where@ clause are abstract if the parent is.
+instance MakeAbstract WhereClause where
+ mkAbstract NoWhere = return $ NoWhere
+ mkAbstract (AnyWhere ds) = dirty $ AnyWhere [Abstract noRange ds]
+ mkAbstract (SomeWhere m a ds) = dirty $ SomeWhere m a [Abstract noRange ds]
+
+-- | Make a declaration private.
+--
+-- Andreas, 2012-11-17:
+-- Mark computation as 'dirty' if there was a declaration that could be privatized.
+-- If no privatization is taking place, we want to complain about 'UselessPrivate'.
+--
+-- Alternatively, we could only flag 'dirty' if a non-private thing was privatized.
+-- Then, nested @private@s would sometimes also be complained about.
+
+class MakePrivate a where
+ mkPrivate :: Origin -> Updater a
+ default mkPrivate :: (Traversable f, MakePrivate a', a ~ f a') => Origin -> Updater a
+ mkPrivate o = traverse $ mkPrivate o
+
+instance MakePrivate a => MakePrivate [a] where
+ -- Default definition kicks in here!
+ -- But note that we still have to declare the instance!
+
+-- Leads to overlap with 'WhereClause':
+-- instance (Traversable f, MakePrivate a) => MakePrivate (f a) where
+-- mkPrivate = traverse mkPrivate
+
+instance MakePrivate Access where
+ mkPrivate o p = case p of
+ PrivateAccess{} -> return p -- OR? return $ PrivateAccess o
+ _ -> dirty $ PrivateAccess o
+
+instance MakePrivate NiceDeclaration where
+ mkPrivate o d =
+ case d of
+ Axiom r f p a i rel mp x e -> (\ p -> Axiom r f p a i rel mp x e) <$> mkPrivate o p
+ NiceField r f p a i x e -> (\ p -> NiceField r f p a i x e) <$> mkPrivate o p
+ PrimitiveFunction r f p a x e -> (\ p -> PrimitiveFunction r f p a x e) <$> mkPrivate o p
+ NiceMutual r termCheck pc ds -> (\ p -> NiceMutual r termCheck pc p) <$> mkPrivate o ds
+ NiceModule r p a x tel ds -> (\ p -> NiceModule r p a x tel ds) <$> mkPrivate o p
+ NiceModuleMacro r p x ma op is -> (\ p -> NiceModuleMacro r p x ma op is) <$> mkPrivate o p
+ FunSig r f p a i m rel tc x e -> (\ p -> FunSig r f p a i m rel tc x e) <$> mkPrivate o p
+ NiceRecSig r f p a pc x ls t -> (\ p -> NiceRecSig r f p a pc x ls t) <$> mkPrivate o p
+ NiceDataSig r f p a pc x ls t -> (\ p -> NiceDataSig r f p a pc x ls t) <$> mkPrivate o p
+ NiceFunClause r p a termCheck catchall d -> (\ p -> NiceFunClause r p a termCheck catchall d) <$> mkPrivate o p
+ NiceUnquoteDecl r f p a i t x e -> (\ p -> NiceUnquoteDecl r f p a i t x e) <$> mkPrivate o p
+ NiceUnquoteDef r f p a t x e -> (\ p -> NiceUnquoteDef r f p a t x e) <$> mkPrivate o p
+ NicePragma _ _ -> return $ d
+ NiceOpen _ _ _ -> return $ d
+ NiceImport _ _ _ _ _ -> return $ d
+ -- Andreas, 2016-07-08, issue #2089
+ -- we need to propagate 'private' to the named where modules
+ FunDef r ds f a tc x cls -> FunDef r ds f a tc x <$> mkPrivate o cls
+ DataDef{} -> return $ d
+ RecDef{} -> return $ d
+ NicePatternSyn _ _ _ _ _ -> return $ d
+
+instance MakePrivate Clause where
+ mkPrivate o (Clause x catchall lhs rhs wh with) = do
+ Clause x catchall lhs rhs <$> mkPrivate o wh <*> mkPrivate o with
+
+instance MakePrivate WhereClause where
+ mkPrivate o NoWhere = return $ NoWhere
+ -- @where@-declarations are protected behind an anonymous module,
+ -- thus, they are effectively private by default.
+ mkPrivate o (AnyWhere ds) = return $ AnyWhere ds
+ -- Andreas, 2016-07-08
+ -- A @where@-module is private if the parent function is private.
+ -- The contents of this module are not private, unless declared so!
+ -- Thus, we do not recurse into the @ds@ (could not anyway).
+ mkPrivate o (SomeWhere m a ds) = mkPrivate o a <&> \ a' -> SomeWhere m a' ds
+
-- | Add more fixities. Throw an exception for multiple fixity declarations.
-- OR: Disjoint union of fixity maps. Throws exception if not disjoint.
@@ -1227,7 +1410,7 @@ plusFixities m1 m2
| otherwise = return $ Map.unionWithKey mergeFixites m1 m2
where
-- Merge two fixities, assuming there is no conflict
- mergeFixites name (Fixity' f1 s1) (Fixity' f2 s2) = Fixity' f s
+ mergeFixites name (Fixity' f1 s1 r1) (Fixity' f2 s2 r2) = Fixity' f s $ fuseRange r1 r2
where f | f1 == noFixity = f2
| f2 == noFixity = f1
| otherwise = __IMPOSSIBLE__
@@ -1240,32 +1423,54 @@ plusFixities m1 m2
| (x, False) <- Map.assocs $ Map.intersectionWith compatible m1 m2 ]
-- Check for no conflict.
- compatible (Fixity' f1 s1) (Fixity' f2 s2) = (f1 == noFixity || f2 == noFixity) &&
- (s1 == noNotation || s2 == noNotation)
+ compatible (Fixity' f1 s1 _) (Fixity' f2 s2 _) =
+ (f1 == noFixity || f2 == noFixity ) &&
+ (s1 == noNotation || s2 == noNotation)
+
+-- | While 'Fixities' and Polarities are not semigroups under disjoint
+-- union (which might fail), we get a semigroup instance for the
+-- monadic @Nice (Fixities, Polarities)@ which propagates the first
+-- error.
+instance Semigroup (Nice (Fixities, Polarities)) where
+ c1 <> c2 = do
+ (f1, p1) <- c1
+ (f2, p2) <- c2
+ f <- plusFixities f1 f2
+ p <- mergePolarities p1 p2
+ return (f, p)
+ where
+ mergePolarities p1 p2
+ | Set.null i = return (Map.union p1 p2)
+ | otherwise = throwError $ MultiplePolarityPragmas (Set.toList i)
+ where
+ i = Set.intersection (Map.keysSet p1) (Map.keysSet p2)
--- | While 'Fixities' is not a monoid under disjoint union (which might fail),
--- we get the monoid instance for the monadic @Nice Fixities@ which propagates
--- the first error.
-instance Monoid (Nice Fixities) where
- mempty = return $ Map.empty
- mappend c1 c2 = plusFixities ==<< (c1, c2)
+instance Monoid (Nice (Fixities, Polarities)) where
+ mempty = return (Map.empty, Map.empty)
+ mappend = (<>)
--- | Get the fixities from the current block.
+-- | Get the fixities and polarity pragmas from the current block.
-- Doesn't go inside modules and where blocks.
--- The reason for this is that fixity declarations have to appear at the same
--- level (or possibly outside an abstract or mutual block) as its target
+-- The reason for this is that these declarations have to appear at the same
+-- level (or possibly outside an abstract or mutual block) as their target
-- declaration.
-fixities :: [Declaration] -> Nice Fixities
-fixities = foldMap $ \ d -> case d of
+fixitiesAndPolarities :: [Declaration] -> Nice (Fixities, Polarities)
+fixitiesAndPolarities = foldMap $ \ d -> case d of
+ -- These declarations define polarities:
+ Pragma (PolarityPragma _ x occs) -> return (Map.empty, Map.singleton x occs)
-- These declarations define fixities:
- Syntax x syn -> return $ Map.singleton x $ Fixity' noFixity syn
- Infix f xs -> return $ Map.fromList $ map (,Fixity' f noNotation) xs
+ Syntax x syn -> return ( Map.singleton x (Fixity' noFixity syn $ getRange x)
+ , Map.empty
+ )
+ Infix f xs -> return ( Map.fromList $ for xs $ \ x -> (x, Fixity' f noNotation$ getRange x)
+ , Map.empty
+ )
-- We look into these blocks:
- Mutual _ ds' -> fixities ds'
- Abstract _ ds' -> fixities ds'
- Private _ ds' -> fixities ds'
- InstanceB _ ds' -> fixities ds'
- Macro _ ds' -> fixities ds'
+ Mutual _ ds' -> fixitiesAndPolarities ds'
+ Abstract _ ds' -> fixitiesAndPolarities ds'
+ Private _ _ ds' -> fixitiesAndPolarities ds'
+ InstanceB _ ds' -> fixitiesAndPolarities ds'
+ Macro _ ds' -> fixitiesAndPolarities ds'
-- All other declarations are ignored.
-- We expand these boring cases to trigger a revisit
-- in case the @Declaration@ type is extended in the future.
@@ -1288,42 +1493,47 @@ fixities = foldMap $ \ d -> case d of
Pragma {} -> mempty
--- Andreas, 2012-04-07
--- The following function is only used twice, for building a Let, and for
--- printing an error message.
+-- The following function is (at the time of writing) only used three
+-- times: for building Lets, and for printing error messages.
--- | (Approximately) convert a 'NiceDeclaration' back to a 'Declaration'.
-notSoNiceDeclaration :: NiceDeclaration -> Declaration
-notSoNiceDeclaration d =
+-- | (Approximately) convert a 'NiceDeclaration' back to a list of
+-- 'Declaration's.
+notSoNiceDeclarations :: NiceDeclaration -> [Declaration]
+notSoNiceDeclarations d =
case d of
- Axiom _ _ _ _ rel x e -> TypeSig rel x e
- NiceField _ i _ _ _ x argt -> Field i x argt
- PrimitiveFunction r _ _ _ x e -> Primitive r [TypeSig defaultArgInfo x e]
- NiceMutual r _ _ ds -> Mutual r $ map notSoNiceDeclaration ds
- NiceModule r _ _ x tel ds -> Module r x tel ds
- NiceModuleMacro r _ x ma o dir -> ModuleMacro r x ma o dir
- NiceOpen r x dir -> Open r x dir
- NiceImport r x as o dir -> Import r x as o dir
- NicePragma _ p -> Pragma p
- NiceRecSig r _ _ x bs e _ -> RecordSig r x bs e
- NiceDataSig r _ _ x bs e _ -> DataSig r Inductive x bs e
- NiceFunClause _ _ _ _ _ d -> d
- FunSig _ _ _ _ _ rel tc x e -> TypeSig rel x e
- FunDef r [d] _ _ _ _ _ -> d
- FunDef r ds _ _ _ _ _ -> Mutual r ds -- Andreas, 2012-04-07 Hack!
- DataDef r _ _ x bs _ cs -> Data r Inductive x bs Nothing $ map notSoNiceDeclaration cs
- RecDef r _ _ x i e c bs _ ds -> Record r x i e (unThing <$> c) bs Nothing $ map notSoNiceDeclaration ds
+ Axiom _ _ _ _ i rel mp x e -> (case mp of
+ Nothing -> []
+ Just occs -> [Pragma (PolarityPragma noRange x occs)]) ++
+ inst i [TypeSig rel x e]
+ NiceField _ _ _ _ i x argt -> [Field i x argt]
+ PrimitiveFunction r _ _ _ x e -> [Primitive r [TypeSig defaultArgInfo x e]]
+ NiceMutual r _ _ ds -> [Mutual r $ concatMap notSoNiceDeclarations ds]
+ NiceModule r _ _ x tel ds -> [Module r x tel ds]
+ NiceModuleMacro r _ x ma o dir -> [ModuleMacro r x ma o dir]
+ NiceOpen r x dir -> [Open r x dir]
+ NiceImport r x as o dir -> [Import r x as o dir]
+ NicePragma _ p -> [Pragma p]
+ NiceRecSig r _ _ _ _ x bs e -> [RecordSig r x bs e]
+ NiceDataSig r _ _ _ _ x bs e -> [DataSig r Inductive x bs e]
+ NiceFunClause _ _ _ _ _ d -> [d]
+ FunSig _ _ _ _ i _ rel tc x e -> inst i [TypeSig rel x e]
+ FunDef _r ds _ _ _ _ _ -> ds
+ DataDef r _ _ _ x bs cs -> [Data r Inductive x bs Nothing $ concatMap notSoNiceDeclarations cs]
+ RecDef r _ _ _ x i e c bs ds -> [Record r x i e (unThing <$> c) bs Nothing $ concatMap notSoNiceDeclarations ds]
where unThing (ThingWithFixity c _, inst) = (c, inst)
- NicePatternSyn r _ n as p -> PatternSyn r n as p
- NiceUnquoteDecl r _ _ _ _ _ x e -> UnquoteDecl r x e
- NiceUnquoteDef r _ _ _ _ x e -> UnquoteDef r x e
+ NicePatternSyn r _ n as p -> [PatternSyn r n as p]
+ NiceUnquoteDecl r _ _ _ i _ x e -> inst i [UnquoteDecl r x e]
+ NiceUnquoteDef r _ _ _ _ x e -> [UnquoteDef r x e]
+ where
+ inst InstanceDef ds = [InstanceB (getRange ds) ds]
+ inst NotInstanceDef ds = ds
-- | Has the 'NiceDeclaration' a field of type 'IsAbstract'?
niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract
niceHasAbstract d =
case d of
Axiom{} -> Nothing
- NiceField _ _ _ _ a _ _ -> Just a
+ NiceField _ _ _ a _ _ _ -> Just a
PrimitiveFunction _ _ _ a _ _ -> Just a
NiceMutual{} -> Nothing
NiceModule _ _ a _ _ _ -> Just a
@@ -1339,5 +1549,5 @@ niceHasAbstract d =
DataDef _ _ a _ _ _ _ -> Just a
RecDef _ _ a _ _ _ _ _ _ _ -> Just a
NicePatternSyn{} -> Nothing
- NiceUnquoteDecl _ _ _ _ a _ _ _ -> Just a
+ NiceUnquoteDecl _ _ _ a _ _ _ _ -> Just a
NiceUnquoteDef _ _ _ a _ _ _ -> Just a
diff --git a/src/full/Agda/Syntax/Concrete/Generic.hs b/src/full/Agda/Syntax/Concrete/Generic.hs
index f9066e3..66990ad 100644
--- a/src/full/Agda/Syntax/Concrete/Generic.hs
+++ b/src/full/Agda/Syntax/Concrete/Generic.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-- | Generic traversal and reduce for concrete syntax,
-- in the style of "Agda.Syntax.Internal.Generic".
@@ -143,6 +142,7 @@ instance ExprLike Expr where
RecUpdate r e es -> f $ RecUpdate r (mapE e) $ mapE es
Let r ds e -> f $ Let r (mapE ds) $ mapE e
Paren r e -> f $ Paren r $ mapE e
+ IdiomBrackets r e -> f $ IdiomBrackets r $ mapE e
Absurd{} -> f $ e0
As r x e -> f $ As r x $ mapE e
Dot r e -> f $ Dot r $ mapE e
@@ -210,7 +210,7 @@ instance ExprLike Declaration where
PatternSyn{} -> e0
Mutual r ds -> Mutual r $ mapE ds
Abstract r ds -> Abstract r $ mapE ds
- Private r ds -> Private r $ mapE ds
+ Private r o ds -> Private r o $ mapE ds
InstanceB r ds -> InstanceB r $ mapE ds
Macro r ds -> Macro r $ mapE ds
Postulate r ds -> Postulate r $ mapE ds
diff --git a/src/full/Agda/Syntax/Concrete/Name.hs b/src/full/Agda/Syntax/Concrete/Name.hs
index df2a945..0a22253 100644
--- a/src/full/Agda/Syntax/Concrete/Name.hs
+++ b/src/full/Agda/Syntax/Concrete/Name.hs
@@ -1,9 +1,7 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-| Names in the concrete syntax are just strings (or lists of strings for
qualified names).
@@ -21,12 +19,12 @@ import GHC.Generics (Generic)
import System.FilePath
-import Test.QuickCheck
-
import Agda.Syntax.Common
import Agda.Syntax.Position
+
import Agda.Utils.FileName
import Agda.Utils.Pretty
+import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
@@ -111,7 +109,7 @@ instance Underscore QName where
newtype TopLevelModuleName
= TopLevelModuleName { moduleNameParts :: [String] }
- deriving (Show, Eq, Ord, Typeable)
+ deriving (Show, Eq, Ord, Typeable, Sized)
------------------------------------------------------------------------
-- * Operations on 'Name' and 'NamePart'
@@ -202,6 +200,17 @@ qnameParts (QName x) = [x]
toTopLevelModuleName :: QName -> TopLevelModuleName
toTopLevelModuleName = TopLevelModuleName . map prettyShow . qnameParts
+-- | Turns a top level module into a qualified name with 'noRange'.
+
+fromTopLevelModuleName :: TopLevelModuleName -> QName
+fromTopLevelModuleName (TopLevelModuleName []) = __IMPOSSIBLE__
+fromTopLevelModuleName (TopLevelModuleName (x:xs)) = loop x xs
+ where
+ loop x [] = QName (mk x)
+ loop x (y : ys) = Qual (mk x) $ loop y ys
+ mk :: String -> Name
+ mk x = Name noRange [Id x]
+
-- | Turns a top-level module name into a file name with the given
-- suffix.
@@ -250,6 +259,7 @@ instance IsNoName Name where
isNoName (NoName _ _) = True
isNoName (Name _ [Hole]) = True -- TODO: Track down where these come from
isNoName (Name _ []) = True
+ isNoName (Name _ [Id x]) = isNoName x
isNoName _ = False
instance IsNoName QName where
@@ -292,44 +302,15 @@ instance Pretty NamePart where
pretty (Id s) = text $ rawNameToString s
instance Pretty QName where
- pretty (Qual m x) = pretty m <> pretty "." <> pretty x
+ pretty (Qual m x)
+ | isUnderscore m = pretty x -- don't print anonymous modules
+ | otherwise = pretty m <> pretty "." <> pretty x
pretty (QName x) = pretty x
instance Pretty TopLevelModuleName where
pretty (TopLevelModuleName ms) = text $ intercalate "." ms
------------------------------------------------------------------------
--- * QuickCheck instances
-------------------------------------------------------------------------
-
-instance Arbitrary TopLevelModuleName where
- arbitrary = TopLevelModuleName <$> listOf1 (listOf1 $ elements "AB")
-
-instance CoArbitrary TopLevelModuleName where
- coarbitrary (TopLevelModuleName m) = coarbitrary m
-
-instance Arbitrary Name where
- arbitrary = oneof
- [ Name <$> arbitrary <*> parts
- , NoName <$> arbitrary <*> arbitrary
- ]
- where
- parts = do
- parts <- listOf1 (elements ["x", "y", "z"])
- startWithHole <- arbitrary
- endWithHole <- arbitrary
- return $
- (if startWithHole then (Hole :) else id) $
- (if endWithHole then (++ [Hole]) else id) $
- intersperse Hole (map Id parts)
-
-instance CoArbitrary NamePart
-
-instance CoArbitrary Name where
- coarbitrary (Name _ ns) = variant 0 . coarbitrary ns
- coarbitrary (NoName _ i) = variant 1 . coarbitrary i
-
-------------------------------------------------------------------------
-- * Range instances
------------------------------------------------------------------------
diff --git a/src/full/Agda/Syntax/Concrete/Operators.hs b/src/full/Agda/Syntax/Concrete/Operators.hs
index 246ce8f..5b4210c 100644
--- a/src/full/Agda/Syntax/Concrete/Operators.hs
+++ b/src/full/Agda/Syntax/Concrete/Operators.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
@@ -40,6 +39,7 @@ import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Common
import Agda.Syntax.Concrete hiding (appView)
import Agda.Syntax.Concrete.Operators.Parser
+import Agda.Syntax.Concrete.Operators.Parser.Monad hiding (parse)
import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Position
import Agda.Syntax.Fixity
@@ -53,7 +53,6 @@ import Agda.TypeChecking.Monad.State (getScope)
import Agda.TypeChecking.Monad.Options
import Agda.Utils.Either
-import Agda.Utils.Parser.MemoisedCPS (memoise)
import Agda.Utils.Pretty
#if MIN_VERSION_base(4,8,0)
import Agda.Utils.List hiding ( uncons )
@@ -346,44 +345,49 @@ buildParsers r flat kind exprNames = do
, "relatedOperators = " ++ show relatedOperators
]
- return (parseSections, everything, Data.Function.fix $ \p -> Parsers
- { pTop = memoise TopK $
- Fold.asum $
- foldr ($) (pApp p)
- (map (\(l, ns) higher ->
- mkP (Right l) parseSections
- (pTop p) ns higher True)
- relatedOperators) :
- map (\(k, n) ->
- mkP (Left k) parseSections
- (pTop p) [n] (pApp p) False)
- (zip [0..] unrelatedOperators)
- , pApp = memoise AppK $ appP (pNonfix p) (pArgs p)
- , pArgs = argsP (pNonfix p)
- , pNonfix = memoise NonfixK $
- Fold.asum $
- pAtom p :
- flip map nonWithSections (\sect ->
- let n = sectNotation sect
-
- inner :: forall k. NK k ->
- Parser e (OperatorType k e)
- inner = opP parseSections (pTop p) n
- in
- case notationKind (notation n) of
- InfixNotation ->
- flip ($) <$> placeholder Beginning
- <*> inner In
- <*> placeholder End
- PrefixNotation ->
- inner Pre <*> placeholder End
- PostfixNotation ->
- flip ($) <$> placeholder Beginning
- <*> inner Post
- NonfixNotation -> inner Non
- NoNotation -> __IMPOSSIBLE__)
- , pAtom = atomP isAtom
- })
+ let g = Data.Function.fix $ \p -> Parsers
+ { pTop = memoise TopK $
+ Fold.asum $
+ foldr ($) (pApp p)
+ (map (\(l, ns) higher ->
+ mkP (Right l) parseSections
+ (pTop p) ns higher True)
+ relatedOperators) :
+ map (\(k, n) ->
+ mkP (Left k) parseSections
+ (pTop p) [n] (pApp p) False)
+ (zip [0..] unrelatedOperators)
+ , pApp = memoise AppK $ appP (pNonfix p) (pArgs p)
+ , pArgs = argsP (pNonfix p)
+ , pNonfix = memoise NonfixK $
+ Fold.asum $
+ pAtom p :
+ flip map nonWithSections (\sect ->
+ let n = sectNotation sect
+
+ inner :: forall k. NK k ->
+ Parser e (OperatorType k e)
+ inner = opP parseSections (pTop p) n
+ in
+ case notationKind (notation n) of
+ InfixNotation ->
+ flip ($) <$> placeholder Beginning
+ <*> inner In
+ <*> placeholder End
+ PrefixNotation ->
+ inner Pre <*> placeholder End
+ PostfixNotation ->
+ flip ($) <$> placeholder Beginning
+ <*> inner Post
+ NonfixNotation -> inner Non
+ NoNotation -> __IMPOSSIBLE__)
+ , pAtom = atomP isAtom
+ }
+
+ reportSDoc "scope.grammar" 10 $ return $
+ text "Operator grammar:" $$ nest 2 (grammar (pTop g))
+
+ return (parseSections, everything, g)
where
level :: NewNotation -> PrecedenceLevel
level = fixityLevel . notaFixity
@@ -451,11 +455,11 @@ buildParsers r flat kind exprNames = do
nonAssoc :: Maybe (Parser e e)
nonAssoc = case filter (isInfix NonAssoc) ops of
[] -> Nothing
- ops -> Just $ do
- x <- noPlaceholder <$> higher
- f <- choice In ops
- y <- noPlaceholder <$> higher
- return (f x y)
+ ops -> Just $
+ (\x f y -> f (noPlaceholder x) (noPlaceholder y))
+ <$> higher
+ <*> choice In ops
+ <*> higher
or p1 [] p2 [] = Nothing
or p1 [] p2 ops2 = Just (p2 ops2)
@@ -474,7 +478,8 @@ buildParsers r flat kind exprNames = do
preRights = do
preRight <- preRight
return $ Data.Function.fix $ \preRights ->
- preRight <*> (noPlaceholder <$> (preRights <|> higher))
+ memoiseIfPrinting (PreRightsK key) $
+ preRight <*> (noPlaceholder <$> (preRights <|> higher))
postLeft :: Maybe (Parser e (MaybePlaceholder e -> e))
postLeft =
@@ -524,7 +529,7 @@ parsePat prs p = case p of
HiddenP _ _ -> fail "bad hidden argument"
InstanceP _ _ -> fail "bad instance argument"
AsP r x p -> AsP r x <$> parsePat prs p
- DotP r e -> return $ DotP r e
+ DotP r o e -> return $ DotP r o e
ParenP r p -> fullParen' <$> parsePat prs p
WildP _ -> return p
AbsurdP _ -> return p
@@ -578,6 +583,8 @@ type ParseLHS = Either Pattern (QName, LHSCore)
parseLHS' ::
LHSOrPatSyn -> Maybe QName -> Pattern ->
ScopeM (ParseLHS, [NotationSection])
+parseLHS' IsLHS (Just qn) (RawAppP _ [WildP{}]) =
+ return (Right (qn, LHSHead qn []), [])
parseLHS' lhsOrPatSyn top p = do
let names = patternQNames p
ms = qualifierModules names
diff --git a/src/full/Agda/Syntax/Concrete/Operators/Parser.hs b/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
index 79596b7..b8a15fc 100644
--- a/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
+++ b/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
@@ -1,6 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
@@ -15,7 +13,7 @@ import Data.Maybe
import qualified Data.Strict.Maybe as Strict
import Data.Set (Set)
-import GHC.Generics (Generic)
+import Text.PrettyPrint.HughesPJ hiding (empty)
import Agda.Syntax.Position
import qualified Agda.Syntax.Abstract.Name as A
@@ -23,28 +21,16 @@ import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Concrete
-
-import qualified Agda.Utils.Parser.MemoisedCPS as MemoisedCPS
-import Agda.Utils.Parser.MemoisedCPS hiding (Parser, parse)
-import qualified Agda.Utils.Parser.MemoisedCPS as Parser
+import Agda.Syntax.Concrete.Operators.Parser.Monad hiding (parse)
+import qualified Agda.Syntax.Concrete.Operators.Parser.Monad as P
#include "undefined.h"
import Agda.Utils.Impossible
-data MemoKey = NodeK (Either Integer Integer)
- | PostLeftsK (Either Integer Integer)
- | TopK
- | AppK
- | NonfixK
- deriving (Eq, Generic)
-
-instance Hashable MemoKey
-
-type Parser tok a =
- MemoisedCPS.Parser MemoKey tok (MaybePlaceholder tok) a
-
placeholder :: PositionInName -> Parser e (MaybePlaceholder e)
-placeholder p = sat $ \t ->
+placeholder p =
+ annotate (const $ text ("_" ++ show p)) $
+ sat $ \t ->
case t of
Placeholder p' | p' == p -> True
_ -> False
@@ -150,9 +136,8 @@ data ParseSections = ParseSections | DoNotParseSections
-- within their respective identifiers.
parse :: IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
-parse (DoNotParseSections, p) es = Parser.parse p (map noPlaceholder es)
-parse (ParseSections, p) es = Parser.parse p
- (concat $ map splitExpr es)
+parse (DoNotParseSections, p) es = P.parse p (map noPlaceholder es)
+parse (ParseSections, p) es = P.parse p (concat $ map splitExpr es)
where
splitExpr :: IsExpr e => e -> [MaybePlaceholder e]
splitExpr e = case exprView e of
@@ -194,7 +179,7 @@ parse (ParseSections, p) es = Parser.parse p
-- | Parse a specific identifier as a NamePart
partP :: IsExpr e => [Name] -> RawName -> Parser e Range
-partP ms s = do
+partP ms s = annotate (const $ text (show str)) $ do
tok <- notPlaceholder
case isLocal tok of
Just p -> return p
@@ -277,9 +262,9 @@ data NK (k :: NotationKind) :: * where
opP :: forall e k. IsExpr e
=> ParseSections
-> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
-opP parseSections p (NewNotation q names _ syn isOp) kind = do
-
- (range, hs) <- worker (init $ qnameParts q) withoutExternalHoles
+opP parseSections p (NewNotation q names _ syn isOp) kind =
+ flip fmap (worker (init $ qnameParts q)
+ withoutExternalHoles) $ \(range, hs) ->
let (normal, binders) = partitionEithers hs
lastHole = maximum $ mapMaybe holeTarget syn
@@ -299,8 +284,9 @@ opP parseSections p (NewNotation q names _ syn isOp) kind = do
where
args = map (findExprFor (f normal) binders) [0..lastHole]
q' = setRange range q
+ in
- return $ case kind of
+ case kind of
In -> \x y -> app (\es -> (x, leadingHole) : es ++ [(y, trailingHole)])
Pre -> \ y -> app (\es -> es ++ [(y, trailingHole)])
Post -> \x -> app (\es -> (x, leadingHole) : es)
@@ -325,32 +311,31 @@ opP parseSections p (NewNotation q names _ syn isOp) kind = do
Parser e (Range, [Either (MaybePlaceholder e, NamedArg Int)
(LamBinding, Int)])
worker ms [] = return (noRange, [])
- worker ms (IdPart x : xs) = do
- r1 <- partP ms x
- (r2, es) <- worker [] xs
- -- Only the first
- -- part is qualified.
- return (fuseRanges r1 r2, es)
- worker ms (NormalHole h : xs) = do
- e <- maybePlaceholder
- (if isOp && parseSections == ParseSections
- then Just Middle else Nothing)
- p
- (r, es) <- worker ms xs
- return (r, Left (e, h) : es)
- worker ms (WildHole h : xs) = do
- (r, es) <- worker ms xs
- return (r, Right (mkBinding h $ Name noRange [Hole]) : es)
+ worker ms (IdPart x : xs) =
+ (\r1 (r2, es) -> (fuseRanges r1 r2, es))
+ <$> partP ms x
+ <*> worker [] xs
+ -- Only the first part is qualified.
+ worker ms (NormalHole h : xs) =
+ (\e (r, es) -> (r, Left (e, h) : es))
+ <$> maybePlaceholder
+ (if isOp && parseSections == ParseSections
+ then Just Middle else Nothing)
+ p
+ <*> worker ms xs
+ worker ms (WildHole h : xs) =
+ (\(r, es) -> (r, Right (mkBinding h $ Name noRange [Hole]) : es))
+ <$> worker ms xs
worker ms (BindHole h : xs) = do
- e <- wildOrUnqualifiedName
- case e of
- Just name -> ret name
- Nothing -> ret (Name noRange [Hole])
- where
- ret x = do
- (r, es) <- worker ms xs
- return (r, Right (mkBinding h x) : es)
- -- Andreas, 2011-04-07 put just 'Relevant' here, is this correct?
+ (\e (r, es) ->
+ let x = case e of
+ Just name -> name
+ Nothing -> Name noRange [Hole]
+ in (r, Right (mkBinding h x) : es))
+ -- Andreas, 2011-04-07 put just 'Relevant' here, is this
+ -- correct?
+ <$> wildOrUnqualifiedName
+ <*> worker ms xs
mkBinding h x = (DomainFree defaultArgInfo $ mkBoundName_ x, h)
@@ -375,7 +360,8 @@ opP parseSections p (NewNotation q names _ syn isOp) kind = do
isPlaceholder Placeholder{} = 1
argsP :: IsExpr e => Parser e e -> Parser e [NamedArg e]
-argsP p = many (nothidden <|> hidden <|> instanceH)
+argsP p = many (annotate (const $ text "<argument>") $
+ nothidden <|> hidden <|> instanceH)
where
isHidden (HiddenArgV _) = True
isHidden _ = False
@@ -399,15 +385,12 @@ argsP p = many (nothidden <|> hidden <|> instanceH)
return $ hide $ defaultArg e
appP :: IsExpr e => Parser e e -> Parser e [NamedArg e] -> Parser e e
-appP p pa = do
- h <- p
- es <- pa
- return $ foldl app h es
+appP p pa = foldl app <$> p <*> pa
where
app e = unExprView . AppV e
atomP :: IsExpr e => (QName -> Bool) -> Parser e e
-atomP p = do
+atomP p = annotate (const $ text "<atom>") $ do
e <- notPlaceholder
case exprView e of
LocalV x | not (p x) -> empty
diff --git a/src/full/Agda/Syntax/Concrete/Operators/Parser/Monad.hs b/src/full/Agda/Syntax/Concrete/Operators/Parser/Monad.hs
new file mode 100644
index 0000000..2c0dfc6
--- /dev/null
+++ b/src/full/Agda/Syntax/Concrete/Operators/Parser/Monad.hs
@@ -0,0 +1,100 @@
+------------------------------------------------------------------------
+-- | The parser monad used by the operator parser
+------------------------------------------------------------------------
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Agda.Syntax.Concrete.Operators.Parser.Monad
+ ( MemoKey(..)
+ , Parser
+ , parse
+ , token
+ , sat
+ , tok
+ , annotate
+ , memoise
+ , memoiseIfPrinting
+ , grammar
+ ) where
+
+import Data.Hashable
+import GHC.Generics (Generic)
+import Text.PrettyPrint.HughesPJ
+
+import Agda.Syntax.Common
+import qualified Agda.Utils.Parser.MemoisedCPS as Parser
+
+-- | Memoisation keys.
+
+data MemoKey = NodeK (Either Integer Integer)
+ | PostLeftsK (Either Integer Integer)
+ | PreRightsK (Either Integer Integer)
+ | TopK
+ | AppK
+ | NonfixK
+ deriving (Eq, Show, Generic)
+
+instance Hashable MemoKey
+
+-- | The parser monad.
+
+type Parser tok a =
+#ifdef DEBUG
+ Parser.ParserWithGrammar
+#else
+ Parser.Parser
+#endif
+ MemoKey tok (MaybePlaceholder tok) a
+
+-- | Runs the parser.
+
+parse :: forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a]
+parse = Parser.parse
+
+-- | Parses a single token.
+
+token :: Parser tok (MaybePlaceholder tok)
+token = Parser.token
+
+-- | Parses a token satisfying the given predicate.
+
+sat :: (MaybePlaceholder tok -> Bool) ->
+ Parser tok (MaybePlaceholder tok)
+sat = Parser.sat
+
+-- | Parses a given token.
+
+tok :: (Eq tok, Show tok) =>
+ MaybePlaceholder tok -> Parser tok (MaybePlaceholder tok)
+tok = Parser.tok
+
+-- | Uses the given function to modify the printed representation (if
+-- any) of the given parser.
+
+annotate :: (Doc -> Doc) -> Parser tok a -> Parser tok a
+annotate = Parser.annotate
+
+-- | Memoises the given parser.
+--
+-- Every memoised parser must be annotated with a /unique/ key.
+-- (Parametrised parsers must use distinct keys for distinct inputs.)
+
+memoise :: MemoKey -> Parser tok tok -> Parser tok tok
+memoise = Parser.memoise
+
+-- | Memoises the given parser, but only if printing, not if parsing.
+--
+-- Every memoised parser must be annotated with a /unique/ key.
+-- (Parametrised parsers must use distinct keys for distinct inputs.)
+
+memoiseIfPrinting :: MemoKey -> Parser tok tok -> Parser tok tok
+memoiseIfPrinting = Parser.memoiseIfPrinting
+
+-- | Tries to print the parser, or returns 'empty', depending on the
+-- implementation. This function might not terminate.
+
+grammar :: Parser tok a -> Doc
+grammar = Parser.grammar
diff --git a/src/full/Agda/Syntax/Concrete/Pretty.hs b/src/full/Agda/Syntax/Concrete/Pretty.hs
index 6683057..92922a4 100644
--- a/src/full/Agda/Syntax/Concrete/Pretty.hs
+++ b/src/full/Agda/Syntax/Concrete/Pretty.hs
@@ -1,8 +1,6 @@
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
{-| Pretty printer for the concrete syntax.
-}
@@ -20,6 +18,9 @@ import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Position
+import Agda.TypeChecking.Positivity.Occurrence
+
+import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Null
import Agda.Utils.Pretty
@@ -162,6 +163,7 @@ instance Pretty Expr where
, text "in" <+> pretty e
]
Paren _ e -> parens $ pretty e
+ IdiomBrackets _ e -> text "(|" <+> pretty e <+> text "|)"
As _ x e -> pretty x <> text "@" <> pretty e
Dot _ e -> text "." <> pretty e
Absurd _ -> text "()"
@@ -255,8 +257,9 @@ instance Pretty WhereClause where
pretty (AnyWhere [Module _ x [] ds]) | isNoName (unqualify x)
= vcat [ text "where", nest 2 (vcat $ map pretty ds) ]
pretty (AnyWhere ds) = vcat [ text "where", nest 2 (vcat $ map pretty ds) ]
- pretty (SomeWhere m ds) =
- vcat [ hsep [ text "module", pretty m, text "where" ]
+ pretty (SomeWhere m a ds) =
+ vcat [ hsep $ applyWhen (a == PrivateAccess UserWritten) (text "private" :)
+ [ text "module", pretty m, text "where" ]
, nest 2 (vcat $ map pretty ds)
]
@@ -300,13 +303,16 @@ instance Pretty Declaration where
]
Field inst x (Arg i e) ->
sep [ text "field"
- , nest 2 $ mkInst inst $
+ , nest 2 $ mkInst inst $ mkOverlap i $
prettyRelevance i $ prettyHiding i id $
pretty $ TypeSig (i {argInfoRelevance = Relevant}) x e
]
where
mkInst InstanceDef d = sep [ text "instance", nest 2 d ]
mkInst NotInstanceDef d = d
+
+ mkOverlap i d | argInfoOverlappable i = text "overlap" <+> d
+ | otherwise = d
FunClause lhs rhs wh _ ->
sep [ pretty lhs
, nest 2 $ pretty rhs
@@ -376,7 +382,7 @@ instance Pretty Declaration where
<+> text "=" <+> pretty p
Mutual _ ds -> namedBlock "mutual" ds
Abstract _ ds -> namedBlock "abstract" ds
- Private _ ds -> namedBlock "private" ds
+ Private _ _ ds -> namedBlock "private" ds
InstanceB _ ds -> namedBlock "instance" ds
Macro _ ds -> namedBlock "macro" ds
Postulate _ ds -> namedBlock "postulate" ds
@@ -424,8 +430,8 @@ instance Pretty OpenShortHand where
instance Pretty Pragma where
pretty (OptionsPragma _ opts) = fsep $ map text $ "OPTIONS" : opts
pretty (BuiltinPragma _ b x) = hsep [ text "BUILTIN", text b, pretty x ]
- pretty (RewritePragma _ x) =
- hsep [ text "REWRITE", pretty x ]
+ pretty (RewritePragma _ xs) =
+ hsep [ text "REWRITE", hsep $ map pretty xs ]
pretty (CompiledPragma _ x hs) =
hsep [ text "COMPILED", pretty x, text hs ]
pretty (CompiledExportPragma _ x hs) =
@@ -446,8 +452,6 @@ instance Pretty Pragma where
hsep $ [ text "COMPILED_DATA_UHC", pretty x] ++ map text (crd : crcs)
pretty (HaskellCodePragma _ s) =
vcat (text "HASKELL" : map text (lines s))
- pretty (NoSmashingPragma _ i) =
- hsep $ [text "NO_SMASHING", pretty i]
pretty (StaticPragma _ i) =
hsep $ [text "STATIC", pretty i]
pretty (InlinePragma _ i) =
@@ -468,6 +472,8 @@ instance Pretty Pragma where
pretty (CatchallPragma _) = text "CATCHALL"
pretty (DisplayPragma _ lhs rhs) = text "DISPLAY" <+> sep [ pretty lhs <+> text "=", nest 2 $ pretty rhs ]
pretty (NoPositivityCheckPragma _) = text "NO_POSITIVITY_CHECK"
+ pretty (PolarityPragma _ q occs) =
+ hsep (text "NO_POSITIVITY_CHECK" : pretty q : map pretty occs)
instance Pretty Fixity where
pretty (Fixity _ Unrelated _) = __IMPOSSIBLE__
@@ -478,6 +484,17 @@ instance Pretty Fixity where
RightAssoc -> "infixr"
NonAssoc -> "infix"
+instance Pretty Occurrence where
+ pretty Unused = text "_"
+ pretty Mixed = text "*"
+ pretty JustNeg = text "-"
+ pretty JustPos = text "+"
+ pretty StrictPos = text "++"
+
+ -- No syntax has been assigned to GuardPos.
+
+ pretty GuardPos = __IMPOSSIBLE__
+
instance Pretty GenPart where
pretty (IdPart x) = text x
pretty BindHole{} = underscore
@@ -488,20 +505,20 @@ instance Pretty Notation where
pretty = hcat . map pretty
instance Pretty Fixity' where
- pretty (Fixity' fix nota)
+ pretty (Fixity' fix nota _)
| nota == noNotation = pretty fix
| otherwise = text "syntax" <+> pretty nota
-instance Pretty e => Pretty (Arg e) where
-- Andreas 2010-09-21: do not print relevance in general, only in function types!
-- Andreas 2010-09-24: and in record fields
- pretty a = -- pRelevance r $
- -- TODO guilhem: print colors
- prettyHiding (argInfo a) id $ pretty $ unArg a
+instance Pretty a => Pretty (Arg a) where
+ prettyPrec p (Arg ai e) = prettyHiding ai id $ prettyPrec p' e
+ where p' | getHiding ai == NotHidden = p
+ | otherwise = 0
instance Pretty e => Pretty (Named_ e) where
- pretty (Named Nothing e) = pretty e
- pretty (Named (Just s) e) = sep [ text (rawNameToString $ rangedThing s) <+> text "=", pretty e ]
+ prettyPrec p (Named Nothing e) = prettyPrec p e
+ prettyPrec p (Named (Just s) e) = mparens (p > 0) $ sep [ text (rawNameToString $ rangedThing s) <+> text "=", pretty e ]
instance Pretty [Pattern] where
pretty = fsep . map pretty
@@ -518,7 +535,7 @@ instance Pretty Pattern where
ParenP _ p -> parens $ pretty p
WildP _ -> underscore
AsP _ x p -> pretty x <> text "@" <> pretty p
- DotP _ p -> text "." <> pretty p
+ DotP _ _ p -> text "." <> pretty p
AbsurdP _ -> text "()"
LitP l -> pretty l
QuoteP _ -> text "quote"