{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.Syntax.Concrete.Definitions
( NiceDeclaration(..)
, NiceConstructor, NiceTypeSignature
, Clause(..)
, DeclarationException(..)
, DeclarationWarning(..), unsafeDeclarationWarning
, Nice, runNice
, niceDeclarations
, notSoNiceDeclarations
, niceHasAbstract
, Measure
, declarationWarningName
) where
import Prelude hiding (null)
import Control.Arrow ((&&&), (***), second)
import Control.Monad.Except
import Control.Monad.State
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Maybe
import qualified Data.List as List
import qualified Data.Foldable as Fold
import Data.Traversable (Traversable, traverse)
import qualified Data.Traversable as Trav
import Data.Data (Data)
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Pattern
import Agda.Syntax.Common hiding (TerminationCheck())
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Position
import Agda.Syntax.Notation
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Concrete.Fixity
import Agda.Interaction.Options.Warnings
import Agda.Utils.AffineHole
import Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List (isSublistOf)
import Agda.Utils.Maybe
import Agda.Utils.Null
import qualified Agda.Utils.Pretty as Pretty
import Agda.Utils.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Three
import Agda.Utils.Tuple
import Agda.Utils.Update
import Agda.Utils.Impossible
data NiceDeclaration
= Axiom Range Access IsAbstract IsInstance ArgInfo Name Expr
| NiceField Range Access IsAbstract IsInstance TacticAttribute Name (Arg Expr)
| PrimitiveFunction Range Access IsAbstract Name Expr
| NiceMutual Range TerminationCheck CoverageCheck PositivityCheck [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 Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
| NiceDataSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
| NiceFunClause Range Access IsAbstract TerminationCheck CoverageCheck Catchall Declaration
| FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck CoverageCheck Name Expr
| FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck CoverageCheck Name [Clause]
| NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]
| NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name (Maybe (Ranged Induction)) (Maybe HasEta)
(Maybe (Name, IsInstance)) [LamBinding] [Declaration]
| NicePatternSyn Range Access Name [Arg Name] Pattern
| NiceGeneralize Range Access ArgInfo TacticAttribute Name Expr
| NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck CoverageCheck [Name] Expr
| NiceUnquoteDef Range Access IsAbstract TerminationCheck CoverageCheck [Name] Expr
deriving (Data, Show)
type TerminationCheck = Common.TerminationCheck Measure
type Measure = Name
type Catchall = Bool
type NiceConstructor = NiceTypeSignature
type NiceTypeSignature = NiceDeclaration
data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
deriving (Data, Show)
data DeclarationException
= MultipleEllipses Pattern
| InvalidName Name
| DuplicateDefinition Name
| MissingWithClauses Name LHS
| WrongDefinition Name DataRecOrFun DataRecOrFun
| DeclarationPanic String
| WrongContentBlock KindOfBlock Range
| AmbiguousFunClauses LHS [Name]
| InvalidMeasureMutual Range
| UnquoteDefRequiresSignature [Name]
| BadMacroDef NiceDeclaration
deriving (Data, Show)
data DeclarationWarning
= EmptyAbstract Range
| EmptyField Range
| EmptyGeneralize Range
| EmptyInstance Range
| EmptyMacro Range
| EmptyMutual Range
| EmptyPostulate Range
| EmptyPrivate Range
| EmptyPrimitive Range
| InvalidCatchallPragma Range
| InvalidCoverageCheckPragma Range
| InvalidNoPositivityCheckPragma Range
| InvalidNoUniverseCheckPragma Range
| InvalidTerminationCheckPragma Range
| MissingDefinitions [(Name, Range)]
| NotAllowedInMutual Range String
| OpenPublicPrivate Range
| OpenPublicAbstract Range
| PolarityPragmasButNotPostulates [Name]
| PragmaNoTerminationCheck Range
| PragmaCompiled Range
| ShadowingInTelescope [(Name, [Range])]
| UnknownFixityInMixfixDecl [Name]
| UnknownNamesInFixityDecl [Name]
| UnknownNamesInPolarityPragmas [Name]
| UselessAbstract Range
| UselessInstance Range
| UselessPrivate Range
deriving (Data, Show)
declarationWarningName :: DeclarationWarning -> WarningName
declarationWarningName = \case
EmptyAbstract{} -> EmptyAbstract_
EmptyField{} -> EmptyField_
EmptyGeneralize{} -> EmptyGeneralize_
EmptyInstance{} -> EmptyInstance_
EmptyMacro{} -> EmptyMacro_
EmptyMutual{} -> EmptyMutual_
EmptyPrivate{} -> EmptyPrivate_
EmptyPostulate{} -> EmptyPostulate_
EmptyPrimitive{} -> EmptyPrimitive_
InvalidCatchallPragma{} -> InvalidCatchallPragma_
InvalidNoPositivityCheckPragma{} -> InvalidNoPositivityCheckPragma_
InvalidNoUniverseCheckPragma{} -> InvalidNoUniverseCheckPragma_
InvalidTerminationCheckPragma{} -> InvalidTerminationCheckPragma_
InvalidCoverageCheckPragma{} -> InvalidCoverageCheckPragma_
MissingDefinitions{} -> MissingDefinitions_
NotAllowedInMutual{} -> NotAllowedInMutual_
OpenPublicPrivate{} -> OpenPublicPrivate_
OpenPublicAbstract{} -> OpenPublicAbstract_
PolarityPragmasButNotPostulates{} -> PolarityPragmasButNotPostulates_
PragmaNoTerminationCheck{} -> PragmaNoTerminationCheck_
PragmaCompiled{} -> PragmaCompiled_
ShadowingInTelescope{} -> ShadowingInTelescope_
UnknownFixityInMixfixDecl{} -> UnknownFixityInMixfixDecl_
UnknownNamesInFixityDecl{} -> UnknownNamesInFixityDecl_
UnknownNamesInPolarityPragmas{} -> UnknownNamesInPolarityPragmas_
UselessAbstract{} -> UselessAbstract_
UselessInstance{} -> UselessInstance_
UselessPrivate{} -> UselessPrivate_
unsafeDeclarationWarning :: DeclarationWarning -> Bool
unsafeDeclarationWarning = \case
EmptyAbstract{} -> False
EmptyField{} -> False
EmptyGeneralize{} -> False
EmptyInstance{} -> False
EmptyMacro{} -> False
EmptyMutual{} -> False
EmptyPrivate{} -> False
EmptyPostulate{} -> False
EmptyPrimitive{} -> False
InvalidCatchallPragma{} -> False
InvalidNoPositivityCheckPragma{} -> False
InvalidNoUniverseCheckPragma{} -> False
InvalidTerminationCheckPragma{} -> False
InvalidCoverageCheckPragma{} -> False
MissingDefinitions{} -> True
NotAllowedInMutual{} -> False
OpenPublicPrivate{} -> False
OpenPublicAbstract{} -> False
PolarityPragmasButNotPostulates{} -> False
PragmaNoTerminationCheck{} -> True
PragmaCompiled{} -> True
ShadowingInTelescope{} -> False
UnknownFixityInMixfixDecl{} -> False
UnknownNamesInFixityDecl{} -> False
UnknownNamesInPolarityPragmas{} -> False
UselessAbstract{} -> False
UselessInstance{} -> False
UselessPrivate{} -> False
data KindOfBlock
= PostulateBlock
| PrimitiveBlock
| InstanceBlock
| FieldBlock
| DataBlock
deriving (Data, Eq, Ord, Show)
instance HasRange DeclarationException where
getRange (MultipleEllipses d) = getRange d
getRange (InvalidName x) = getRange x
getRange (DuplicateDefinition x) = getRange x
getRange (MissingWithClauses x lhs) = getRange lhs
getRange (WrongDefinition x k k') = getRange x
getRange (AmbiguousFunClauses lhs xs) = getRange lhs
getRange (DeclarationPanic _) = noRange
getRange (WrongContentBlock _ r) = r
getRange (InvalidMeasureMutual r) = r
getRange (UnquoteDefRequiresSignature x) = getRange x
getRange (BadMacroDef d) = getRange d
instance HasRange DeclarationWarning where
getRange (UnknownNamesInFixityDecl xs) = getRange xs
getRange (UnknownFixityInMixfixDecl xs) = getRange xs
getRange (UnknownNamesInPolarityPragmas xs) = getRange xs
getRange (PolarityPragmasButNotPostulates xs) = getRange xs
getRange (MissingDefinitions xs) = getRange xs
getRange (UselessPrivate r) = r
getRange (NotAllowedInMutual r x) = r
getRange (UselessAbstract r) = r
getRange (UselessInstance r) = r
getRange (EmptyMutual r) = r
getRange (EmptyAbstract r) = r
getRange (EmptyPrivate r) = r
getRange (EmptyInstance r) = r
getRange (EmptyMacro r) = r
getRange (EmptyPostulate r) = r
getRange (EmptyGeneralize r) = r
getRange (EmptyPrimitive r) = r
getRange (EmptyField r) = r
getRange (InvalidTerminationCheckPragma r) = r
getRange (InvalidCoverageCheckPragma r) = r
getRange (InvalidNoPositivityCheckPragma r) = r
getRange (InvalidCatchallPragma r) = r
getRange (InvalidNoUniverseCheckPragma r) = r
getRange (PragmaNoTerminationCheck r) = r
getRange (PragmaCompiled r) = r
getRange (OpenPublicAbstract r) = r
getRange (OpenPublicPrivate r) = r
getRange (ShadowingInTelescope ns) = getRange ns
instance HasRange NiceDeclaration where
getRange (Axiom r _ _ _ _ _ _) = r
getRange (NiceField r _ _ _ _ _ _) = r
getRange (NiceMutual r _ _ _ _) = r
getRange (NiceModule r _ _ _ _ _ ) = r
getRange (NiceModuleMacro r _ _ _ _ _) = r
getRange (NiceOpen r _ _) = r
getRange (NiceImport r _ _ _ _) = r
getRange (NicePragma r _) = r
getRange (PrimitiveFunction r _ _ _ _) = r
getRange (FunSig r _ _ _ _ _ _ _ _ _) = r
getRange (FunDef r _ _ _ _ _ _ _) = r
getRange (NiceDataDef r _ _ _ _ _ _ _) = r
getRange (NiceRecDef r _ _ _ _ _ _ _ _ _ _) = r
getRange (NiceRecSig r _ _ _ _ _ _ _) = r
getRange (NiceDataSig r _ _ _ _ _ _ _) = r
getRange (NicePatternSyn r _ _ _ _) = r
getRange (NiceGeneralize r _ _ _ _ _) = r
getRange (NiceFunClause r _ _ _ _ _ _) = r
getRange (NiceUnquoteDecl r _ _ _ _ _ _ _) = r
getRange (NiceUnquoteDef r _ _ _ _ _ _) = r
instance Pretty NiceDeclaration where
pretty = \case
Axiom _ _ _ _ _ x _ -> text "postulate" <+> pretty x <+> colon <+> text "_"
NiceField _ _ _ _ _ x _ -> text "field" <+> pretty x
PrimitiveFunction _ _ _ x _ -> text "primitive" <+> pretty x
NiceMutual{} -> text "mutual"
NiceModule _ _ _ x _ _ -> text "module" <+> pretty x <+> text "where"
NiceModuleMacro _ _ x _ _ _ -> text "module" <+> pretty x <+> text "= ..."
NiceOpen _ x _ -> text "open" <+> pretty x
NiceImport _ x _ _ _ -> text "import" <+> pretty x
NicePragma{} -> text "{-# ... #-}"
NiceRecSig _ _ _ _ _ x _ _ -> text "record" <+> pretty x
NiceDataSig _ _ _ _ _ x _ _ -> text "data" <+> pretty x
NiceFunClause{} -> text "<function clause>"
FunSig _ _ _ _ _ _ _ _ x _ -> pretty x <+> colon <+> text "_"
FunDef _ _ _ _ _ _ x _ -> pretty x <+> text "= _"
NiceDataDef _ _ _ _ _ x _ _ -> text "data" <+> pretty x <+> text "where"
NiceRecDef _ _ _ _ _ x _ _ _ _ _ -> text "record" <+> pretty x <+> text "where"
NicePatternSyn _ _ x _ _ -> text "pattern" <+> pretty x
NiceGeneralize _ _ _ _ x _ -> text "variable" <+> pretty x
NiceUnquoteDecl _ _ _ _ _ _ xs _ -> text "<unquote declarations>"
NiceUnquoteDef _ _ _ _ _ xs _ -> text "<unquote definitions>"
instance Pretty DeclarationException where
pretty (MultipleEllipses p) = fsep $
pwords "Multiple ellipses in left-hand side" ++ [pretty p]
pretty (InvalidName x) = fsep $
pwords "Invalid name:" ++ [pretty x]
pretty (DuplicateDefinition x) = fsep $
pwords "Duplicate definition of" ++ [pretty x]
pretty (MissingWithClauses x lhs) = fsep $
pwords "Missing with-clauses for function" ++ [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')
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 (WrongContentBlock b _) = fsep . pwords $
case b of
PostulateBlock -> "A postulate block can only contain type signatures, possibly under keyword instance"
DataBlock -> "A data definition can only contain type signatures, possibly under keyword instance"
_ -> "Unexpected declaration"
pretty (InvalidMeasureMutual _) = fsep $
pwords "In a mutual block, either all functions must have the same (or no) termination checking pragma."
pretty (UnquoteDefRequiresSignature xs) = fsep $
pwords "Missing type signatures for unquoteDef" ++ map pretty xs
pretty (BadMacroDef nd) = fsep $
[text $ declName nd] ++ pwords "are not allowed in macro blocks"
pretty (DeclarationPanic s) = text s
instance Pretty DeclarationWarning 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):"
++ punctuate comma (map pretty xs)
pretty (UnknownFixityInMixfixDecl xs) = fsep $
pwords "The following mixfix names do not have an associated fixity declaration:"
++ punctuate comma (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):"
++ punctuate comma (map pretty xs)
pretty (MissingDefinitions xs) = fsep $
pwords "The following names are declared but not accompanied by a definition:"
++ punctuate comma (map (pretty . fst) xs)
pretty (NotAllowedInMutual r nd) = fsep $
[text nd] ++ pwords "in mutual blocks are not supported. Suggestion: get rid of the mutual block by manually ordering declarations"
pretty (PolarityPragmasButNotPostulates xs) = fsep $
pwords "Polarity pragmas have been given for the following identifiers which are not postulates:"
++ punctuate comma (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 $
pwords "Using abstract here has no effect. Abstract applies to only definitions like data definitions, record type definitions and function clauses."
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."
pretty (EmptyMutual _) = fsep $ pwords "Empty mutual block."
pretty (EmptyAbstract _) = fsep $ pwords "Empty abstract block."
pretty (EmptyPrivate _) = fsep $ pwords "Empty private block."
pretty (EmptyInstance _) = fsep $ pwords "Empty instance block."
pretty (EmptyMacro _) = fsep $ pwords "Empty macro block."
pretty (EmptyPostulate _) = fsep $ pwords "Empty postulate block."
pretty (EmptyGeneralize _) = fsep $ pwords "Empty variable block."
pretty (EmptyPrimitive _) = fsep $ pwords "Empty primitive block."
pretty (EmptyField _) = fsep $ pwords "Empty field block."
pretty (InvalidTerminationCheckPragma _) = fsep $
pwords "Termination checking pragmas can only precede a function definition or a mutual block (that contains a function definition)."
pretty (InvalidCoverageCheckPragma _) = fsep $
pwords "Coverage checking pragmas can only precede a function definition or a mutual block (that contains a function definition)."
pretty (InvalidNoPositivityCheckPragma _) = fsep $
pwords "NO_POSITIVITY_CHECKING pragmas can only precede a data/record definition or a mutual block (that contains a data/record definition)."
pretty (InvalidCatchallPragma _) = fsep $
pwords "The CATCHALL pragma can only precede a function clause."
pretty (InvalidNoUniverseCheckPragma _) = fsep $
pwords "NO_UNIVERSE_CHECKING pragmas can only precede a data/record definition."
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 #-}."
pretty (PragmaCompiled _) = fsep $
pwords "COMPILE pragma not allowed in safe mode."
pretty (OpenPublicAbstract _) = fsep $
pwords "public does not have any effect in an abstract block."
pretty (OpenPublicPrivate _) = fsep $
pwords "public does not have any effect in a private block."
pretty (ShadowingInTelescope nrs) = fsep $
pwords "Shadowing in telescope, repeated variable names:"
++ punctuate comma (map (pretty . fst) nrs)
declName :: NiceDeclaration -> String
declName Axiom{} = "Postulates"
declName NiceField{} = "Fields"
declName NiceMutual{} = "Mutual blocks"
declName NiceModule{} = "Modules"
declName NiceModuleMacro{} = "Modules"
declName NiceOpen{} = "Open declarations"
declName NiceImport{} = "Import statements"
declName NicePragma{} = "Pragmas"
declName PrimitiveFunction{} = "Primitive declarations"
declName NicePatternSyn{} = "Pattern synonyms"
declName NiceGeneralize{} = "Generalized variables"
declName NiceUnquoteDecl{} = "Unquoted declarations"
declName NiceUnquoteDef{} = "Unquoted definitions"
declName NiceRecSig{} = "Records"
declName NiceDataSig{} = "Data types"
declName NiceFunClause{} = "Functions without a type signature"
declName FunSig{} = "Type signatures"
declName FunDef{} = "Function definitions"
declName NiceRecDef{} = "Records"
declName NiceDataDef{} = "Data types"
data InMutual
= InMutual
| NotInMutual
deriving (Eq, Show)
data DataRecOrFun
= DataName
{ _kindPosCheck :: PositivityCheck
, _kindUniCheck :: UniverseCheck
}
| RecName
{ _kindPosCheck :: PositivityCheck
, _kindUniCheck :: UniverseCheck
}
| FunName TerminationCheck CoverageCheck
deriving Data
instance Eq DataRecOrFun where
DataName{} == DataName{} = True
RecName{} == RecName{} = True
FunName{} == FunName{} = True
_ == _ = False
instance Show DataRecOrFun where
show DataName{} = "data type"
show RecName{} = "record type"
show FunName{} = "function"
isFunName :: DataRecOrFun -> Bool
isFunName (FunName{}) = True
isFunName _ = False
sameKind :: DataRecOrFun -> DataRecOrFun -> Bool
sameKind = (==)
terminationCheck :: DataRecOrFun -> TerminationCheck
terminationCheck (FunName tc _) = tc
terminationCheck _ = TerminationCheck
coverageCheck :: DataRecOrFun -> CoverageCheck
coverageCheck (FunName _ cc) = cc
coverageCheck _ = YesCoverageCheck
positivityCheck :: DataRecOrFun -> PositivityCheck
positivityCheck (DataName pc _) = pc
positivityCheck (RecName pc _) = pc
positivityCheck _ = YesPositivityCheck
universeCheck :: DataRecOrFun -> UniverseCheck
universeCheck (DataName _ uc) = uc
universeCheck (RecName _ uc) = uc
universeCheck _ = YesUniverseCheck
combineTerminationChecks :: Range -> [TerminationCheck] -> Nice TerminationCheck
combineTerminationChecks r tcs = loop tcs where
loop :: [TerminationCheck] -> Nice TerminationCheck
loop [] = return TerminationCheck
loop (tc : tcs) = do
let failure r = throwError $ InvalidMeasureMutual r
tc' <- loop tcs
case (tc, tc') of
(TerminationCheck , tc' ) -> return tc'
(tc , TerminationCheck ) -> return tc
(NonTerminating , NonTerminating ) -> return NonTerminating
(NoTerminationCheck , NoTerminationCheck ) -> return NoTerminationCheck
(NoTerminationCheck , Terminating ) -> return Terminating
(Terminating , NoTerminationCheck ) -> return Terminating
(Terminating , Terminating ) -> return Terminating
(TerminationMeasure{} , TerminationMeasure{} ) -> return tc
(TerminationMeasure r _, NoTerminationCheck ) -> failure r
(TerminationMeasure r _, Terminating ) -> failure r
(NoTerminationCheck , TerminationMeasure r _) -> failure r
(Terminating , TerminationMeasure r _) -> failure r
(TerminationMeasure r _, NonTerminating ) -> failure r
(NonTerminating , TerminationMeasure r _) -> failure r
(NoTerminationCheck , NonTerminating ) -> failure r
(Terminating , NonTerminating ) -> failure r
(NonTerminating , NoTerminationCheck ) -> failure r
(NonTerminating , Terminating ) -> failure r
combineCoverageChecks :: [CoverageCheck] -> CoverageCheck
combineCoverageChecks = Fold.fold
combinePositivityChecks :: [PositivityCheck] -> PositivityCheck
combinePositivityChecks = Fold.fold
newtype Nice a = Nice { unNice :: ExceptT DeclarationException (State NiceEnv) a }
deriving ( Functor, Applicative, Monad
, MonadState NiceEnv, MonadError DeclarationException
)
runNice :: Nice a -> (Either DeclarationException a, NiceWarnings)
runNice m = second (reverse . niceWarn) $
runExceptT (unNice m) `runState` initNiceEnv
data NiceEnv = NiceEnv
{ _loneSigs :: LoneSigs
, _termChk :: TerminationCheck
, _posChk :: PositivityCheck
, _uniChk :: UniverseCheck
, _catchall :: Catchall
, _covChk :: CoverageCheck
, niceWarn :: NiceWarnings
}
data LoneSig = LoneSig
{ loneSigRange :: Range
, loneSigName :: Name
, loneSigKind :: DataRecOrFun
}
type LoneSigs = Map Name LoneSig
type NiceWarnings = [DeclarationWarning]
initNiceEnv :: NiceEnv
initNiceEnv = NiceEnv
{ _loneSigs = empty
, _termChk = TerminationCheck
, _posChk = YesPositivityCheck
, _uniChk = YesUniverseCheck
, _catchall = False
, _covChk = YesCoverageCheck
, niceWarn = []
}
loneSigs :: Lens' LoneSigs NiceEnv
loneSigs f e = f (_loneSigs e) <&> \ s -> e { _loneSigs = s }
addLoneSig :: Range -> Name -> DataRecOrFun -> Nice ()
addLoneSig r x k = loneSigs %== \ s -> do
let (mr, s') = Map.insertLookupWithKey (\ _k new _old -> new) x (LoneSig r x k) s
case mr of
Nothing -> return s'
Just{} -> throwError $ DuplicateDefinition x
removeLoneSig :: Name -> Nice ()
removeLoneSig x = loneSigs %= Map.delete x
getSig :: Name -> Nice (Maybe DataRecOrFun)
getSig x = fmap loneSigKind . Map.lookup x <$> use loneSigs
noLoneSigs :: Nice Bool
noLoneSigs = null <$> use loneSigs
forgetLoneSigs :: Nice ()
forgetLoneSigs = loneSigs .= Map.empty
checkLoneSigs :: LoneSigs -> Nice ()
checkLoneSigs xs = do
forgetLoneSigs
unless (Map.null xs) $ niceWarning $ MissingDefinitions $
map (\s -> (loneSigName s , loneSigRange s)) $ Map.elems xs
loneFuns :: LoneSigs -> [Name]
loneFuns = map fst . filter (isFunName . loneSigKind . snd) . Map.toList
loneSigsFromLoneNames :: [(Range, Name, DataRecOrFun)] -> LoneSigs
loneSigsFromLoneNames = Map.fromList . map (\(r,x,k) -> (x, LoneSig r x k))
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
coverageCheckPragma :: Lens' CoverageCheck NiceEnv
coverageCheckPragma f e = f (_covChk e) <&> \ s -> e { _covChk = s }
withCoverageCheckPragma :: CoverageCheck -> Nice a -> Nice a
withCoverageCheckPragma tc f = do
tc_old <- use coverageCheckPragma
coverageCheckPragma .= tc
result <- f
coverageCheckPragma .= tc_old
return result
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
universeCheckPragma :: Lens' UniverseCheck NiceEnv
universeCheckPragma f e = f (_uniChk e) <&> \ s -> e { _uniChk = s }
withUniverseCheckPragma :: UniverseCheck -> Nice a -> Nice a
withUniverseCheckPragma uc f = do
uc_old <- use universeCheckPragma
universeCheckPragma .= uc
result <- f
universeCheckPragma .= uc_old
return result
getUniverseCheckFromSig :: Name -> Nice UniverseCheck
getUniverseCheckFromSig x = maybe YesUniverseCheck universeCheck <$> getSig x
catchallPragma :: Lens' Catchall NiceEnv
catchallPragma f e = f (_catchall e) <&> \ s -> e { _catchall = s }
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
niceWarning :: DeclarationWarning -> Nice ()
niceWarning w = modify $ \ st -> st { niceWarn = w : niceWarn st }
data DeclKind
= LoneSigDecl Range DataRecOrFun Name
| LoneDefs DataRecOrFun [Name]
| OtherDecl
deriving (Eq, Show)
declKind :: NiceDeclaration -> DeclKind
declKind (FunSig r _ _ _ _ _ tc cc x _) = LoneSigDecl r (FunName tc cc) x
declKind (NiceRecSig r _ _ pc uc x pars _) = LoneSigDecl r (RecName pc uc) x
declKind (NiceDataSig r _ _ pc uc x pars _) = LoneSigDecl r (DataName pc uc) x
declKind (FunDef r _ abs ins tc cc x _) = LoneDefs (FunName tc cc) [x]
declKind (NiceDataDef _ _ _ pc uc x pars _) = LoneDefs (DataName pc uc) [x]
declKind (NiceRecDef _ _ _ pc uc x _ _ _ pars _)= LoneDefs (RecName pc uc) [x]
declKind (NiceUnquoteDef _ _ _ tc cc xs _) = LoneDefs (FunName tc cc) xs
declKind Axiom{} = OtherDecl
declKind NiceField{} = OtherDecl
declKind PrimitiveFunction{} = OtherDecl
declKind NiceMutual{} = OtherDecl
declKind NiceModule{} = OtherDecl
declKind NiceModuleMacro{} = OtherDecl
declKind NiceOpen{} = OtherDecl
declKind NiceImport{} = OtherDecl
declKind NicePragma{} = OtherDecl
declKind NiceFunClause{} = OtherDecl
declKind NicePatternSyn{} = OtherDecl
declKind NiceGeneralize{} = OtherDecl
declKind NiceUnquoteDecl{} = OtherDecl
replaceSigs
:: LoneSigs
-> [NiceDeclaration]
-> [NiceDeclaration]
replaceSigs ps = if Map.null ps then id else \case
[] -> __IMPOSSIBLE__
(d:ds) ->
case replaceable d of
Just (x, axiom)
| (Just (LoneSig _ x' _), ps') <- Map.updateLookupWithKey (\ _ _ -> Nothing) x ps
, getRange x == getRange x'
-> axiom : replaceSigs ps' ds
_ -> d : replaceSigs ps ds
where
replaceable :: NiceDeclaration -> Maybe (Name, NiceDeclaration)
replaceable = \case
FunSig r acc abst inst _ argi _ _ x e ->
Just (x, Axiom r acc abst inst argi x e)
NiceRecSig r acc abst _ _ x pars t ->
let e = Generalized $ makePi (lamBindingsToTelescope r pars) t in
Just (x, Axiom r acc abst NotInstanceDef defaultArgInfo x e)
NiceDataSig r acc abst _ _ x pars t ->
let e = Generalized $ makePi (lamBindingsToTelescope r pars) t in
Just (x, Axiom r acc abst NotInstanceDef defaultArgInfo x e)
_ -> Nothing
niceDeclarations :: Fixities -> [Declaration] -> Nice [NiceDeclaration]
niceDeclarations fixs ds = do
st <- get
put $ initNiceEnv { niceWarn = niceWarn st }
nds <- nice ds
ps <- use loneSigs
checkLoneSigs ps
let ds = replaceSigs ps nds
res <- inferMutualBlocks ds
warns <- gets niceWarn
put $ st { niceWarn = warns }
return res
where
inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [] = return []
inferMutualBlocks (d : ds) =
case declKind d of
OtherDecl -> (d :) <$> inferMutualBlocks ds
LoneDefs{} -> (d :) <$> inferMutualBlocks ds
LoneSigDecl r k x -> do
addLoneSig r x k
let tcccpc = ([terminationCheck k], [coverageCheck k], [positivityCheck k])
((tcs, ccs, pcs), (nds0, ds1)) <- untilAllDefined tcccpc ds
ps <- use loneSigs
checkLoneSigs ps
let ds0 = replaceSigs ps (d : nds0)
tc <- combineTerminationChecks (getRange d) tcs
let cc = combineCoverageChecks ccs
let pc = combinePositivityChecks pcs
(NiceMutual (getRange ds0) tc cc pc ds0 :) <$> inferMutualBlocks ds1
where
untilAllDefined :: ([TerminationCheck], [CoverageCheck], [PositivityCheck])
-> [NiceDeclaration]
-> Nice (([TerminationCheck], [CoverageCheck], [PositivityCheck])
, ([NiceDeclaration]
, [NiceDeclaration])
)
untilAllDefined tcccpc@(tc, cc, pc) ds = do
done <- noLoneSigs
if done then return (tcccpc, ([], ds)) else
case ds of
[] -> return (tcccpc, ([], ds))
d : ds -> case declKind d of
LoneSigDecl r k x -> do
addLoneSig r x k
let tcccpc' = (terminationCheck k : tc, coverageCheck k : cc, positivityCheck k : pc)
cons d (untilAllDefined tcccpc' ds)
LoneDefs k xs -> do
mapM_ removeLoneSig xs
let tcccpc' = (terminationCheck k : tc, coverageCheck k : cc, positivityCheck k : pc)
cons d (untilAllDefined tcccpc' ds)
OtherDecl -> cons d (untilAllDefined tcccpc ds)
where
cons d = fmap (id *** (d :) *** id)
notMeasure TerminationMeasure{} = False
notMeasure _ = True
nice :: [Declaration] -> Nice [NiceDeclaration]
nice [] = return []
nice ds = do
(xs , ys) <- nice1 ds
(xs ++) <$> nice ys
nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [] = return ([], [])
nice1 (d:ds) = do
let justWarning w = do niceWarning w; nice1 ds
case d of
TypeSig info _tac x t -> do
termCheck <- use terminationCheckPragma
covCheck <- use coverageCheckPragma
let r = getRange d
addLoneSig r x $ FunName termCheck covCheck
return ([FunSig r PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck covCheck x t] , ds)
FieldSig{} -> __IMPOSSIBLE__
Generalize r [] -> justWarning $ EmptyGeneralize r
Generalize r sigs -> do
gs <- forM sigs $ \case
sig@(TypeSig info tac x t) -> do
return $ NiceGeneralize (getRange sig) PublicAccess info tac x t
_ -> __IMPOSSIBLE__
return (gs, ds)
(FunClause lhs _ _ _) -> do
termCheck <- use terminationCheckPragma
covCheck <- use coverageCheckPragma
catchall <- popCatchallPragma
xs <- loneFuns <$> use loneSigs
case [ (x, (fits, rest))
| x <- xs
, let (fits, rest) =
if isNoName x then ([d], ds)
else span (couldBeFunClauseOf (Map.lookup x fixs) x) (d : ds)
, not (null fits)
] of
[] -> case lhs of
LHS p [] [] _ | Just x <- isSingleIdentifierP p -> do
d <- mkFunDef defaultArgInfo termCheck covCheck x Nothing [d]
return (d , ds)
_ -> do
return ([NiceFunClause (getRange d) PublicAccess ConcreteDef termCheck covCheck catchall d] , ds)
[(x,(fits,rest))] -> do
removeLoneSig x
ds <- expandEllipsis fits
cs <- mkClauses x ds False
return ([FunDef (getRange fits) fits ConcreteDef NotInstanceDef termCheck covCheck x cs] , rest)
l -> throwError $ AmbiguousFunClauses lhs $ reverse $ map fst l
Field r [] -> justWarning $ EmptyField r
Field _ fs -> (,ds) <$> niceAxioms FieldBlock fs
DataSig r x tel t -> do
pc <- use positivityCheckPragma
uc <- use universeCheckPragma
addLoneSig r x $ DataName pc uc
(,) <$> dataOrRec pc uc NiceDataDef NiceDataSig (niceAxioms DataBlock) r x (Just (tel, t)) Nothing
<*> return ds
Data r x tel t cs -> do
pc <- use positivityCheckPragma
uc <- use universeCheckPragma
uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
mt <- defaultTypeSig (DataName pc uc) x (Just t)
(,) <$> dataOrRec pc uc NiceDataDef NiceDataSig (niceAxioms DataBlock) r x ((tel,) <$> mt) (Just (tel, cs))
<*> return ds
DataDef r x tel cs -> do
pc <- use positivityCheckPragma
uc <- use universeCheckPragma
uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
mt <- defaultTypeSig (DataName pc uc) x Nothing
(,) <$> dataOrRec pc uc NiceDataDef NiceDataSig (niceAxioms DataBlock) r x ((tel,) <$> mt) (Just (tel, cs))
<*> return ds
RecordSig r x tel t -> do
pc <- use positivityCheckPragma
uc <- use universeCheckPragma
addLoneSig r x $ RecName pc uc
return ([NiceRecSig r PublicAccess ConcreteDef pc uc x tel t] , ds)
Record r x i e c tel t cs -> do
pc <- use positivityCheckPragma
uc <- use universeCheckPragma
uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
mt <- defaultTypeSig (RecName pc uc) x (Just t)
(,) <$> dataOrRec pc uc (\ r o a pc uc x tel cs -> NiceRecDef r o a pc uc x i e c tel cs) NiceRecSig
return r x ((tel,) <$> mt) (Just (tel, cs))
<*> return ds
RecordDef r x i e c tel cs -> do
pc <- use positivityCheckPragma
uc <- use universeCheckPragma
uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
mt <- defaultTypeSig (RecName pc uc) x Nothing
(,) <$> dataOrRec pc uc (\ r o a pc uc x tel cs -> NiceRecDef r o a pc uc x i e c tel cs) NiceRecSig
return r x ((tel,) <$> mt) (Just (tel, cs))
<*> return ds
Mutual r ds' -> do
forgetLoneSigs
case ds' of
[] -> justWarning $ EmptyMutual r
_ -> (,ds) <$> (singleton <$> (mkOldMutual r =<< nice ds'))
Abstract r [] -> justWarning $ EmptyAbstract r
Abstract r ds' ->
(,ds) <$> (abstractBlock r =<< nice ds')
Private r UserWritten [] -> justWarning $ EmptyPrivate r
Private r o ds' ->
(,ds) <$> (privateBlock r o =<< nice ds')
InstanceB r [] -> justWarning $ EmptyInstance r
InstanceB r ds' ->
(,ds) <$> (instanceBlock r =<< nice ds')
Macro r [] -> justWarning $ EmptyMacro r
Macro r ds' ->
(,ds) <$> (macroBlock r =<< nice ds')
Postulate r [] -> justWarning $ EmptyPostulate r
Postulate _ ds' ->
(,ds) <$> niceAxioms PostulateBlock ds'
Primitive r [] -> justWarning $ EmptyPrimitive r
Primitive _ ds' -> (,ds) <$> (map toPrim <$> niceAxioms PrimitiveBlock ds')
Module r x tel ds' -> return $
([NiceModule r PublicAccess ConcreteDef x tel ds'] , ds)
ModuleMacro r x modapp op is -> return $
([NiceModuleMacro r PublicAccess x modapp op is] , ds)
Infix _ _ -> return ([], ds)
Syntax _ _ -> return ([], ds)
PatternSyn r n as p -> do
return ([NicePatternSyn r PublicAccess 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
tc <- use terminationCheckPragma
cc <- use coverageCheckPragma
return ([NiceUnquoteDecl r PublicAccess ConcreteDef NotInstanceDef tc cc xs e] , ds)
UnquoteDef r xs e -> do
sigs <- loneFuns <$> use loneSigs
let missing = filter (`notElem` sigs) xs
if null missing
then do
mapM_ removeLoneSig xs
return ([NiceUnquoteDef r PublicAccess ConcreteDef TerminationCheck YesCoverageCheck xs e] , ds)
else throwError $ UnquoteDefRequiresSignature missing
Pragma p -> nicePragma p ds
nicePragma :: Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nicePragma (TerminationCheckPragma r (TerminationMeasure _ x)) ds =
if canHaveTerminationMeasure ds then
withTerminationCheckPragma (TerminationMeasure r x) $ nice1 ds
else do
niceWarning $ InvalidTerminationCheckPragma r
nice1 ds
nicePragma (TerminationCheckPragma r NoTerminationCheck) ds = do
niceWarning $ PragmaNoTerminationCheck r
nicePragma (TerminationCheckPragma r NonTerminating) ds
nicePragma (TerminationCheckPragma r tc) ds =
if canHaveTerminationCheckPragma ds then
withTerminationCheckPragma tc $ nice1 ds
else do
niceWarning $ InvalidTerminationCheckPragma r
nice1 ds
nicePragma (NoCoverageCheckPragma r) ds =
if canHaveCoverageCheckPragma ds then
withCoverageCheckPragma NoCoverageCheck $ nice1 ds
else do
niceWarning $ InvalidCoverageCheckPragma r
nice1 ds
nicePragma (CatchallPragma r) ds =
if canHaveCatchallPragma ds then
withCatchallPragma True $ nice1 ds
else do
niceWarning $ InvalidCatchallPragma r
nice1 ds
nicePragma (NoPositivityCheckPragma r) ds =
if canHaveNoPositivityCheckPragma ds then
withPositivityCheckPragma NoPositivityCheck $ nice1 ds
else do
niceWarning $ InvalidNoPositivityCheckPragma r
nice1 ds
nicePragma (NoUniverseCheckPragma r) ds =
if canHaveNoUniverseCheckPragma ds then
withUniverseCheckPragma NoUniverseCheck $ nice1 ds
else do
niceWarning $ InvalidNoUniverseCheckPragma r
nice1 ds
nicePragma p@CompilePragma{} ds = do
niceWarning $ PragmaCompiled (getRange p)
return ([NicePragma (getRange p) p], ds)
nicePragma (PolarityPragma{}) ds = return ([], ds)
nicePragma (BuiltinPragma r str qn@(QName x)) ds = do
return ([NicePragma r (BuiltinPragma r str qn)], 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 _ ds -> any (canHaveTerminationCheckPragma . singleton) ds
TypeSig{} -> True
FunClause{} -> True
UnquoteDecl{} -> True
(Pragma p) | isAttachedPragma p -> canHaveTerminationCheckPragma ds
_ -> False
canHaveCoverageCheckPragma :: [Declaration] -> Bool
canHaveCoverageCheckPragma = canHaveTerminationCheckPragma
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 _ ds -> any (canHaveNoPositivityCheckPragma . singleton) ds
Data{} -> True
DataSig{} -> True
DataDef{} -> True
Record{} -> True
RecordSig{} -> True
RecordDef{} -> True
Pragma p | isAttachedPragma p -> canHaveNoPositivityCheckPragma ds
_ -> False
canHaveNoUniverseCheckPragma :: [Declaration] -> Bool
canHaveNoUniverseCheckPragma [] = False
canHaveNoUniverseCheckPragma (d:ds) = case d of
Data{} -> True
DataSig{} -> True
DataDef{} -> True
Record{} -> True
RecordSig{} -> True
RecordDef{} -> True
Pragma p | isAttachedPragma p -> canHaveNoPositivityCheckPragma ds
_ -> False
isAttachedPragma :: Pragma -> Bool
isAttachedPragma p = case p of
TerminationCheckPragma{} -> True
CatchallPragma{} -> True
NoPositivityCheckPragma{} -> True
NoUniverseCheckPragma{} -> True
_ -> False
defaultTypeSig :: DataRecOrFun -> Name -> Maybe Expr -> Nice (Maybe Expr)
defaultTypeSig k x t@Just{} = return t
defaultTypeSig k x Nothing = do
caseMaybeM (getSig x) (return Nothing) $ \ k' -> do
unless (sameKind k k') $ throwError $ WrongDefinition x k' k
Nothing <$ removeLoneSig x
dataOrRec
:: forall a decl
. PositivityCheck
-> UniverseCheck
-> (Range -> Origin -> IsAbstract -> PositivityCheck -> UniverseCheck -> Name -> [LamBinding] -> [decl] -> NiceDeclaration)
-> (Range -> Access -> IsAbstract -> PositivityCheck -> UniverseCheck -> Name -> [LamBinding] -> Expr -> NiceDeclaration)
-> ([a] -> Nice [decl])
-> Range
-> Name
-> Maybe ([LamBinding], Expr)
-> Maybe ([LamBinding], [a])
-> Nice [NiceDeclaration]
dataOrRec pc uc mkDef mkSig niceD r x mt mcs = do
mds <- Trav.forM mcs $ \ (tel, cs) -> (tel,) <$> niceD cs
let o | isJust mt && isJust mcs = Inserted
| otherwise = UserWritten
return $ catMaybes $
[ mt <&> \ (tel, t) -> mkSig (fuseRange x t) PublicAccess ConcreteDef pc uc x tel t
, mds <&> \ (tel, ds) -> mkDef r o ConcreteDef pc uc x (caseMaybe mt tel $ const $ concatMap dropTypeAndModality tel) ds
]
where
dropTypeAndModality :: LamBinding -> [LamBinding]
dropTypeAndModality (DomainFull (TBind _ xs _)) =
map (DomainFree . setModality defaultModality) xs
dropTypeAndModality (DomainFull TLet{}) = []
dropTypeAndModality (DomainFree x) = [DomainFree $ setModality defaultModality x]
niceAxioms :: KindOfBlock -> [TypeSignatureOrInstanceBlock] -> Nice [NiceDeclaration]
niceAxioms b ds = liftM List.concat $ mapM (niceAxiom b) ds
niceAxiom :: KindOfBlock -> TypeSignatureOrInstanceBlock -> Nice [NiceDeclaration]
niceAxiom b d = case d of
TypeSig rel _tac x t -> do
return [ Axiom (getRange d) PublicAccess ConcreteDef NotInstanceDef rel x t ]
FieldSig i tac x argt | b == FieldBlock -> do
return [ NiceField (getRange d) PublicAccess ConcreteDef i tac x argt ]
InstanceB r decls -> do
instanceBlock r =<< niceAxioms InstanceBlock decls
Pragma p@(RewritePragma r _ _) -> do
return [ NicePragma r p ]
_ -> throwError $ WrongContentBlock b $ getRange d
toPrim :: NiceDeclaration -> NiceDeclaration
toPrim (Axiom r p a i rel x t) = PrimitiveFunction r p a x t
toPrim _ = __IMPOSSIBLE__
mkFunDef info termCheck covCheck x mt ds0 = do
ds <- expandEllipsis ds0
cs <- mkClauses x ds False
return [ FunSig (fuseRange x t) PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck covCheck x t
, FunDef (getRange ds0) ds0 ConcreteDef NotInstanceDef termCheck covCheck x cs ]
where
t = case mt of
Just t -> t
Nothing -> underscore (getRange x)
underscore r = Underscore r Nothing
expandEllipsis :: [Declaration] -> Nice [Declaration]
expandEllipsis [] = return []
expandEllipsis (d@(FunClause lhs@(LHS p _ _ ell) _ _ _) : ds)
| ExpandedEllipsis{} <- ell = __IMPOSSIBLE__
| hasEllipsis p = (d :) <$> expandEllipsis ds
| otherwise = (d :) <$> expand (killRange p) ds
where
expand :: Pattern -> [Declaration] -> Nice [Declaration]
expand _ [] = return []
expand p (d : ds) = do
case d of
Pragma (CatchallPragma _) -> do
(d :) <$> expand p ds
FunClause (LHS p0 eqs es NoEllipsis) rhs wh ca -> do
case hasEllipsis' p0 of
ManyHoles -> throwError $ MultipleEllipses p0
OneHole cxt ~(EllipsisP r) -> do
let p1 = cxt p
let ell = ExpandedEllipsis r (numberOfWithPatterns p)
let d' = FunClause (LHS p1 eqs es ell) rhs wh ca
(d' :) <$> expand (if null es then p else killRange p1) ds
ZeroHoles _ -> do
(d :) <$> expand (if null es then p else killRange p0) ds
_ -> __IMPOSSIBLE__
expandEllipsis _ = __IMPOSSIBLE__
mkClauses :: Name -> [Declaration] -> Catchall -> Nice [Clause]
mkClauses _ [] _ = return []
mkClauses x (Pragma (CatchallPragma r) : cs) True = do
niceWarning $ InvalidCatchallPragma r
mkClauses x cs True
mkClauses x (Pragma (CatchallPragma r) : cs) False = do
when (null cs) $ niceWarning $ InvalidCatchallPragma r
mkClauses x cs True
mkClauses x (FunClause lhs rhs wh ca : cs) catchall
| null (lhsWithExpr lhs) || hasEllipsis lhs =
(Clause x (ca || catchall) lhs rhs wh [] :) <$> mkClauses x cs False
mkClauses x (FunClause lhs rhs wh ca : cs) catchall = do
when (null withClauses) $ throwError $ MissingWithClauses x lhs
wcs <- mkClauses x withClauses False
(Clause x (ca || catchall) lhs rhs wh wcs :) <$> mkClauses x cs' False
where
(withClauses, cs') = subClauses cs
numWith = numberOfWithPatterns p + length (filter visible es) where LHS p _ es _ = lhs
subClauses :: [Declaration] -> ([Declaration],[Declaration])
subClauses (c@(FunClause (LHS p0 _ _ _) _ _ _) : cs)
| isEllipsis p0 ||
numberOfWithPatterns p0 >= numWith = mapFst (c:) (subClauses cs)
| otherwise = ([], c:cs)
subClauses (c@(Pragma (CatchallPragma r)) : cs) = case subClauses cs of
([], cs') -> ([], c:cs')
(cs, cs') -> (c:cs, cs')
subClauses [] = ([],[])
subClauses _ = __IMPOSSIBLE__
mkClauses _ _ _ = __IMPOSSIBLE__
couldBeFunClauseOf :: Maybe Fixity' -> Name -> Declaration -> Bool
couldBeFunClauseOf mFixity x (Pragma (CatchallPragma{})) = True
couldBeFunClauseOf mFixity x (FunClause (LHS p _ _ _) _ _ _) = hasEllipsis p ||
let
pns = patternNames p
xStrings = nameStringParts x
patStrings = concatMap nameStringParts pns
in
case (listToMaybe pns, mFixity) of
(Just y, _) | x == y -> True
_ | xStrings `isSublistOf` patStrings -> True
(_, Just fix) ->
let notStrings = stringParts (theNotation fix)
in
(not $ null notStrings) && (notStrings `isSublistOf` patStrings)
_ -> False
couldBeFunClauseOf _ _ _ = False
mkOldMutual
:: Range
-> [NiceDeclaration]
-> Nice NiceDeclaration
mkOldMutual r ds' = do
let ps = loneSigsFromLoneNames loneNames
checkLoneSigs ps
let ds = replaceSigs ps ds'
(top, bottom, invalid) <- forEither3M ds $ \ d -> do
let top = return (In1 d)
bottom = return (In2 d)
invalid s = In3 d <$ do niceWarning $ NotAllowedInMutual (getRange d) s
case d of
Axiom{} -> top
NiceField{} -> top
PrimitiveFunction{} -> top
NiceMutual{} -> invalid "mutual blocks"
NiceModule{} -> invalid "Module definitions"
NiceModuleMacro{} -> top
NiceOpen{} -> top
NiceImport{} -> top
NiceRecSig{} -> top
NiceDataSig{} -> top
NiceFunClause{} -> bottom
FunSig{} -> top
FunDef{} -> bottom
NiceDataDef{} -> bottom
NiceRecDef{} -> bottom
NicePatternSyn{} -> bottom
NiceGeneralize{} -> top
NiceUnquoteDecl{} -> top
NiceUnquoteDef{} -> bottom
NicePragma r pragma -> case pragma of
OptionsPragma{} -> top
BuiltinPragma{} -> invalid "BUILTIN pragmas"
RewritePragma{} -> invalid "REWRITE pragmas"
ForeignPragma{} -> bottom
CompilePragma{} -> bottom
StaticPragma{} -> bottom
InlinePragma{} -> bottom
ImpossiblePragma{} -> top
EtaPragma{} -> bottom
WarningOnUsage{} -> top
WarningOnImport{} -> top
InjectivePragma{} -> top
DisplayPragma{} -> top
CatchallPragma{} -> __IMPOSSIBLE__
TerminationCheckPragma{} -> __IMPOSSIBLE__
NoPositivityCheckPragma{} -> __IMPOSSIBLE__
PolarityPragma{} -> __IMPOSSIBLE__
NoUniverseCheckPragma{} -> __IMPOSSIBLE__
NoCoverageCheckPragma{} -> __IMPOSSIBLE__
tc0 <- use terminationCheckPragma
let tcs = map termCheck ds
tc <- combineTerminationChecks r (tc0:tcs)
cc0 <- use coverageCheckPragma
let ccs = map covCheck ds
let cc = combineCoverageChecks (cc0:ccs)
pc0 <- use positivityCheckPragma
let pcs = map positivityCheckOldMutual ds
let pc = combinePositivityChecks (pc0:pcs)
return $ NiceMutual r tc cc pc $ top ++ bottom
where
sigNames = [ (r, x, k) | LoneSigDecl r k x <- map declKind ds' ]
defNames = [ (x, k) | LoneDefs k xs <- map declKind ds', x <- xs ]
loneNames = [ (r, x, k) | (r, x, k) <- sigNames, List.all ((x /=) . fst) defNames ]
termCheck :: NiceDeclaration -> TerminationCheck
termCheck (FunSig _ _ _ _ _ _ tc _ _ _) = tc
termCheck (FunDef _ _ _ _ tc _ _ _) = tc
termCheck (NiceMutual _ tc _ _ _) = tc
termCheck (NiceUnquoteDecl _ _ _ _ tc _ _ _) = tc
termCheck (NiceUnquoteDef _ _ _ tc _ _ _) = tc
termCheck Axiom{} = TerminationCheck
termCheck NiceField{} = TerminationCheck
termCheck PrimitiveFunction{} = TerminationCheck
termCheck NiceModule{} = TerminationCheck
termCheck NiceModuleMacro{} = TerminationCheck
termCheck NiceOpen{} = TerminationCheck
termCheck NiceImport{} = TerminationCheck
termCheck NicePragma{} = TerminationCheck
termCheck NiceRecSig{} = TerminationCheck
termCheck NiceDataSig{} = TerminationCheck
termCheck NiceFunClause{} = TerminationCheck
termCheck NiceDataDef{} = TerminationCheck
termCheck NiceRecDef{} = TerminationCheck
termCheck NicePatternSyn{} = TerminationCheck
termCheck NiceGeneralize{} = TerminationCheck
covCheck :: NiceDeclaration -> CoverageCheck
covCheck (FunSig _ _ _ _ _ _ _ cc _ _) = cc
covCheck (FunDef _ _ _ _ _ cc _ _) = cc
covCheck (NiceMutual _ _ cc _ _) = cc
covCheck (NiceUnquoteDecl _ _ _ _ _ cc _ _) = cc
covCheck (NiceUnquoteDef _ _ _ _ cc _ _) = cc
covCheck Axiom{} = YesCoverageCheck
covCheck NiceField{} = YesCoverageCheck
covCheck PrimitiveFunction{} = YesCoverageCheck
covCheck NiceModule{} = YesCoverageCheck
covCheck NiceModuleMacro{} = YesCoverageCheck
covCheck NiceOpen{} = YesCoverageCheck
covCheck NiceImport{} = YesCoverageCheck
covCheck NicePragma{} = YesCoverageCheck
covCheck NiceRecSig{} = YesCoverageCheck
covCheck NiceDataSig{} = YesCoverageCheck
covCheck NiceFunClause{} = YesCoverageCheck
covCheck NiceDataDef{} = YesCoverageCheck
covCheck NiceRecDef{} = YesCoverageCheck
covCheck NicePatternSyn{} = YesCoverageCheck
covCheck NiceGeneralize{} = YesCoverageCheck
positivityCheckOldMutual :: NiceDeclaration -> PositivityCheck
positivityCheckOldMutual (NiceDataDef _ _ _ pc _ _ _ _) = pc
positivityCheckOldMutual (NiceDataSig _ _ _ pc _ _ _ _) = pc
positivityCheckOldMutual (NiceMutual _ _ _ pc _) = pc
positivityCheckOldMutual (NiceRecSig _ _ _ pc _ _ _ _) = pc
positivityCheckOldMutual (NiceRecDef _ _ _ pc _ _ _ _ _ _ _) = pc
positivityCheckOldMutual _ = YesPositivityCheck
abstractBlock _ [] = return []
abstractBlock r ds = do
(ds', anyChange) <- runChangeT $ mkAbstract ds
let inherited = r == noRange
if anyChange then return ds' else do
unless inherited $ niceWarning $ UselessAbstract r
return ds
privateBlock _ _ [] = return []
privateBlock r o ds = do
(ds', anyChange) <- runChangeT $ mkPrivate o ds
if anyChange then return ds' else do
when (o == UserWritten) $ niceWarning $ UselessPrivate r
return ds
instanceBlock
:: Range
-> [NiceDeclaration]
-> Nice [NiceDeclaration]
instanceBlock _ [] = return []
instanceBlock r ds = do
let (ds', anyChange) = runChange $ mapM (mkInstance r) ds
if anyChange then return ds' else do
niceWarning $ UselessInstance r
return ds
mkInstance
:: Range
-> Updater NiceDeclaration
mkInstance r0 = \case
Axiom r p a i rel x e -> (\ i -> Axiom r p a i rel x e) <$> setInstance r0 i
FunSig r p a i m rel tc cc x e -> (\ i -> FunSig r p a i m rel tc cc x e) <$> setInstance r0 i
NiceUnquoteDecl r p a i tc cc x e -> (\ i -> NiceUnquoteDecl r p a i tc cc x e) <$> setInstance r0 i
NiceMutual r tc cc pc ds -> NiceMutual r tc cc pc <$> mapM (mkInstance r0) ds
d@NiceFunClause{} -> return d
FunDef r ds a i tc cc x cs -> (\ i -> FunDef r ds a i tc cc x cs) <$> setInstance r0 i
d@NiceField{} -> return d
d@PrimitiveFunction{} -> return d
d@NiceUnquoteDef{} -> return d
d@NiceRecSig{} -> return d
d@NiceDataSig{} -> return d
d@NiceModuleMacro{} -> return d
d@NiceModule{} -> return d
d@NicePragma{} -> return d
d@NiceOpen{} -> return d
d@NiceImport{} -> return d
d@NiceDataDef{} -> return d
d@NiceRecDef{} -> return d
d@NicePatternSyn{} -> return d
d@NiceGeneralize{} -> return d
setInstance
:: Range
-> Updater IsInstance
setInstance r0 = \case
i@InstanceDef{} -> return i
_ -> dirty $ InstanceDef r0
macroBlock r ds = mapM mkMacro ds
mkMacro :: NiceDeclaration -> Nice NiceDeclaration
mkMacro = \case
FunSig r p a i _ rel tc cc x e -> return $ FunSig r p a i MacroDef rel tc cc x e
d@FunDef{} -> return d
d -> throwError (BadMacroDef d)
class MakeAbstract a where
mkAbstract :: UpdaterT Nice a
default mkAbstract :: (Traversable f, MakeAbstract a', a ~ f a') => UpdaterT Nice a
mkAbstract = traverse mkAbstract
instance MakeAbstract a => MakeAbstract [a] where
instance MakeAbstract IsAbstract where
mkAbstract = \case
a@AbstractDef -> return a
ConcreteDef -> dirty $ AbstractDef
instance MakeAbstract NiceDeclaration where
mkAbstract = \case
NiceMutual r termCheck cc pc ds -> NiceMutual r termCheck cc pc <$> mkAbstract ds
FunDef r ds a i tc cc x cs -> (\ a -> FunDef r ds a i tc cc x) <$> mkAbstract a <*> mkAbstract cs
NiceDataDef r o a pc uc x ps cs -> (\ a -> NiceDataDef r o a pc uc x ps) <$> mkAbstract a <*> mkAbstract cs
NiceRecDef r o a pc uc x i e c ps cs -> (\ a -> NiceRecDef r o a pc uc x i e c ps) <$> mkAbstract a <*> return cs
NiceFunClause r p a tc cc catchall d -> (\ a -> NiceFunClause r p a tc cc catchall d) <$> mkAbstract a
Axiom r p a i rel x e -> return $ Axiom r p AbstractDef i rel x e
FunSig r p a i m rel tc cc x e -> return $ FunSig r p AbstractDef i m rel tc cc x e
NiceRecSig r p a pc uc x ls t -> return $ NiceRecSig r p AbstractDef pc uc x ls t
NiceDataSig r p a pc uc x ls t -> return $ NiceDataSig r p AbstractDef pc uc x ls t
NiceField r p _ i tac x e -> return $ NiceField r p AbstractDef i tac x e
PrimitiveFunction r p _ x e -> return $ PrimitiveFunction r p AbstractDef x e
NiceUnquoteDecl r p _ i tc cc x e -> tellDirty $> NiceUnquoteDecl r p AbstractDef i tc cc x e
NiceUnquoteDef r p _ tc cc x e -> tellDirty $> NiceUnquoteDef r p AbstractDef tc cc x e
d@NiceModule{} -> return d
d@NiceModuleMacro{} -> return d
d@NicePragma{} -> return d
d@(NiceOpen _ _ directives) -> do
whenJust (publicOpen directives) $ lift . niceWarning . OpenPublicAbstract
return d
d@NiceImport{} -> return d
d@NicePatternSyn{} -> return d
d@NiceGeneralize{} -> return d
instance MakeAbstract Clause where
mkAbstract (Clause x catchall lhs rhs wh with) = do
Clause x catchall lhs rhs <$> mkAbstract wh <*> mkAbstract with
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]
class MakePrivate a where
mkPrivate :: Origin -> UpdaterT Nice a
default mkPrivate :: (Traversable f, MakePrivate a', a ~ f a') => Origin -> UpdaterT Nice a
mkPrivate o = traverse $ mkPrivate o
instance MakePrivate a => MakePrivate [a] where
instance MakePrivate Access where
mkPrivate o = \case
p@PrivateAccess{} -> return p
_ -> dirty $ PrivateAccess o
instance MakePrivate NiceDeclaration where
mkPrivate o = \case
Axiom r p a i rel x e -> (\ p -> Axiom r p a i rel x e) <$> mkPrivate o p
NiceField r p a i tac x e -> (\ p -> NiceField r p a i tac x e) <$> mkPrivate o p
PrimitiveFunction r p a x e -> (\ p -> PrimitiveFunction r p a x e) <$> mkPrivate o p
NiceMutual r tc cc pc ds -> (\ ds-> NiceMutual r tc cc pc ds) <$> 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 p a i m rel tc cc x e -> (\ p -> FunSig r p a i m rel tc cc x e) <$> mkPrivate o p
NiceRecSig r p a pc uc x ls t -> (\ p -> NiceRecSig r p a pc uc x ls t) <$> mkPrivate o p
NiceDataSig r p a pc uc x ls t -> (\ p -> NiceDataSig r p a pc uc x ls t) <$> mkPrivate o p
NiceFunClause r p a tc cc catchall d -> (\ p -> NiceFunClause r p a tc cc catchall d) <$> mkPrivate o p
NiceUnquoteDecl r p a i tc cc x e -> (\ p -> NiceUnquoteDecl r p a i tc cc x e) <$> mkPrivate o p
NiceUnquoteDef r p a tc cc x e -> (\ p -> NiceUnquoteDef r p a tc cc x e) <$> mkPrivate o p
NicePatternSyn r p x xs p' -> (\ p -> NicePatternSyn r p x xs p') <$> mkPrivate o p
NiceGeneralize r p i tac x t -> (\ p -> NiceGeneralize r p i tac x t) <$> mkPrivate o p
d@NicePragma{} -> return d
d@(NiceOpen _ _ directives) -> do
whenJust (publicOpen directives) $ lift . niceWarning . OpenPublicPrivate
return d
d@NiceImport{} -> return d
FunDef r ds a i tc cc x cls -> FunDef r ds a i tc cc x <$> mkPrivate o cls
d@NiceDataDef{} -> return d
d@NiceRecDef{} -> 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
mkPrivate o (AnyWhere ds) = return $ AnyWhere ds
mkPrivate o (SomeWhere m a ds) = mkPrivate o a <&> \ a' -> SomeWhere m a' ds
notSoNiceDeclarations :: NiceDeclaration -> [Declaration]
notSoNiceDeclarations = \case
Axiom _ _ _ i rel x e -> inst i [TypeSig rel Nothing x e]
NiceField _ _ _ i tac x argt -> [FieldSig i tac x argt]
PrimitiveFunction r _ _ x e -> [Primitive r [TypeSig defaultArgInfo Nothing 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 x bs e]
NiceFunClause _ _ _ _ _ _ d -> [d]
FunSig _ _ _ i _ rel _ _ x e -> inst i [TypeSig rel Nothing x e]
FunDef _ ds _ _ _ _ _ _ -> ds
NiceDataDef r _ _ _ _ x bs cs -> [DataDef r x bs $ concatMap notSoNiceDeclarations cs]
NiceRecDef r _ _ _ _ x i e c bs ds -> [RecordDef r x i e c bs ds]
NicePatternSyn r _ n as p -> [PatternSyn r n as p]
NiceGeneralize r _ i tac n e -> [Generalize r [TypeSig i tac n e]]
NiceUnquoteDecl r _ _ i _ _ x e -> inst i [UnquoteDecl r x e]
NiceUnquoteDef r _ _ _ _ x e -> [UnquoteDef r x e]
where
inst (InstanceDef r) ds = [InstanceB r ds]
inst NotInstanceDef ds = ds
niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract
niceHasAbstract = \case
Axiom{} -> Nothing
NiceField _ _ a _ _ _ _ -> Just a
PrimitiveFunction _ _ a _ _ -> Just a
NiceMutual{} -> Nothing
NiceModule _ _ a _ _ _ -> Just a
NiceModuleMacro{} -> Nothing
NiceOpen{} -> Nothing
NiceImport{} -> Nothing
NicePragma{} -> Nothing
NiceRecSig{} -> Nothing
NiceDataSig{} -> Nothing
NiceFunClause _ _ a _ _ _ _ -> Just a
FunSig{} -> Nothing
FunDef _ _ a _ _ _ _ _ -> Just a
NiceDataDef _ _ a _ _ _ _ _ -> Just a
NiceRecDef _ _ a _ _ _ _ _ _ _ _ -> Just a
NicePatternSyn{} -> Nothing
NiceGeneralize{} -> Nothing
NiceUnquoteDecl _ _ a _ _ _ _ _ -> Just a
NiceUnquoteDef _ _ a _ _ _ _ -> Just a