{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GADTs #-}
module Agda.Syntax.Concrete.Definitions
( NiceDeclaration(..)
, NiceConstructor, NiceTypeSignature
, Clause(..)
, DeclarationException(..)
, DeclarationWarning(..)
, Nice, runNice
, niceDeclarations
, notSoNiceDeclarations
, niceHasAbstract
, Measure
, declarationWarningName
) where
import Prelude hiding (null)
import Control.Arrow ((***), first, second)
import Control.Applicative hiding (empty)
import Control.Monad.State
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Maybe
import Data.Monoid ( Monoid, mempty, mappend )
import Data.Semigroup ( Semigroup, (<>) )
import qualified Data.List as List
import qualified Data.Set as Set
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.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Concrete.Pretty ()
import Agda.Interaction.Options.Warnings
import Agda.TypeChecking.Positivity.Occurrence
import Agda.Utils.AffineHole
import Agda.Utils.Except ( MonadError(throwError,catchError) )
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List (caseList, headMaybe, isSublistOf)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.Pretty as Pretty
import Agda.Utils.Pretty hiding ((<>))
import Agda.Utils.Singleton
import Agda.Utils.Tuple
import Agda.Utils.Update
#include "undefined.h"
import Agda.Utils.Impossible
data NiceDeclaration
= Axiom Range Fixity' Access IsAbstract IsInstance ArgInfo (Maybe [Occurrence]) Name Expr
| 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]
| NiceModuleMacro Range Access Name ModuleApplication OpenShortHand ImportDirective
| NiceOpen Range QName ImportDirective
| NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
| NicePragma Range Pragma
| NiceRecSig Range Fixity' Access IsAbstract PositivityCheck Name [LamBinding] Expr
| NiceDataSig Range Fixity' Access IsAbstract PositivityCheck Name [LamBinding] Expr
| NiceFunClause Range Access IsAbstract TerminationCheck Catchall Declaration
| FunSig Range Fixity' Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck Name Expr
| FunDef Range [Declaration] Fixity' IsAbstract IsInstance TerminationCheck Name [Clause]
| DataDef Range Fixity' IsAbstract PositivityCheck Name [LamBinding] [NiceConstructor]
| RecDef Range Fixity' IsAbstract PositivityCheck Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (ThingWithFixity Name, IsInstance)) [LamBinding] [NiceDeclaration]
| NicePatternSyn Range Fixity' Name [Arg Name] Pattern
| NiceUnquoteDecl Range [Fixity'] Access IsAbstract IsInstance TerminationCheck [Name] Expr
| NiceUnquoteDef Range [Fixity'] Access IsAbstract TerminationCheck [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
= MultipleFixityDecls [(Name, [Fixity'])]
| MultiplePolarityPragmas [Name]
| MultipleEllipses Pattern
| InvalidName Name
| DuplicateDefinition Name
| MissingDefinition Name
| MissingWithClauses Name
| WrongDefinition Name DataRecOrFun DataRecOrFun
| WrongParameters Name Params Params
| NotAllowedInMutual NiceDeclaration
| Codata Range
| DeclarationPanic String
| WrongContentBlock KindOfBlock Range
| AmbiguousFunClauses LHS [Name]
| InvalidMeasureMutual Range
| PragmaNoTerminationCheck Range
| UnquoteDefRequiresSignature [Name]
| BadMacroDef NiceDeclaration
deriving (Data, Show)
data DeclarationWarning
= UnknownNamesInFixityDecl [Name]
| UnknownFixityInMixfixDecl [Name]
| UnknownNamesInPolarityPragmas [Name]
| PolarityPragmasButNotPostulates [Name]
| UselessPrivate Range
| UselessAbstract Range
| UselessInstance Range
| EmptyMutual Range
| EmptyAbstract Range
| EmptyPrivate Range
| EmptyInstance Range
| EmptyMacro Range
| EmptyPostulate Range
| InvalidTerminationCheckPragma Range
| InvalidNoPositivityCheckPragma Range
| InvalidCatchallPragma Range
deriving (Data, Show)
declarationWarningName :: DeclarationWarning -> WarningName
declarationWarningName dw = case dw of
UnknownNamesInFixityDecl{} -> UnknownNamesInFixityDecl_
UnknownFixityInMixfixDecl{} -> UnknownFixityInMixfixDecl_
UnknownNamesInPolarityPragmas{} -> UnknownNamesInPolarityPragmas_
PolarityPragmasButNotPostulates{} -> PolarityPragmasButNotPostulates_
UselessPrivate{} -> UselessPrivate_
UselessAbstract{} -> UselessAbstract_
UselessInstance{} -> UselessInstance_
EmptyMutual{} -> EmptyMutual_
EmptyAbstract{} -> EmptyAbstract_
EmptyPrivate{} -> EmptyPrivate_
EmptyInstance{} -> EmptyInstance_
EmptyMacro{} -> EmptyMacro_
EmptyPostulate{} -> EmptyPostulate_
InvalidTerminationCheckPragma{} -> InvalidTerminationCheckPragma_
InvalidNoPositivityCheckPragma{} -> InvalidNoPositivityCheckPragma_
InvalidCatchallPragma{} -> InvalidCatchallPragma_
data KindOfBlock
= PostulateBlock
| PrimitiveBlock
| InstanceBlock
| FieldBlock
| DataBlock
deriving (Data, Eq, Ord, Show)
instance HasRange DeclarationException where
getRange (MultipleFixityDecls xs) = getRange (fst $ head xs)
getRange (MultiplePolarityPragmas xs) = getRange (head xs)
getRange (MultipleEllipses d) = getRange d
getRange (InvalidName x) = getRange x
getRange (DuplicateDefinition x) = getRange x
getRange (MissingDefinition x) = getRange x
getRange (MissingWithClauses 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 (Codata r) = r
getRange (DeclarationPanic _) = noRange
getRange (WrongContentBlock _ r) = r
getRange (InvalidMeasureMutual r) = r
getRange (PragmaNoTerminationCheck r) = r
getRange (UnquoteDefRequiresSignature x) = getRange x
getRange (BadMacroDef d) = getRange d
instance HasRange DeclarationWarning where
getRange (UnknownNamesInFixityDecl xs) = getRange . head $ xs
getRange (UnknownFixityInMixfixDecl xs) = getRange . head $ xs
getRange (UnknownNamesInPolarityPragmas xs) = getRange . head $ xs
getRange (PolarityPragmasButNotPostulates xs) = getRange . head $ xs
getRange (UselessPrivate r) = 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 (InvalidTerminationCheckPragma r) = r
getRange (InvalidNoPositivityCheckPragma r) = r
getRange (InvalidCatchallPragma r) = r
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 (DataDef r _ _ _ _ _ _) = r
getRange (RecDef r _ _ _ _ _ _ _ _ _) = r
getRange (NiceRecSig r _ _ _ _ _ _ _) = r
getRange (NiceDataSig r _ _ _ _ _ _ _) = r
getRange (NicePatternSyn r _ _ _ _) = r
getRange (NiceFunClause r _ _ _ _ _) = r
getRange (NiceUnquoteDecl r _ _ _ _ _ _ _) = r
getRange (NiceUnquoteDef r _ _ _ _ _ _) = r
instance Pretty DeclarationException where
pretty (MultipleFixityDecls xs) =
sep [ fsep $ pwords "Multiple fixity or syntax declarations for"
, vcat $ map f xs
]
where
f (x, fs) = pretty x Pretty.<> text ": " <+> fsep (map pretty fs)
pretty (MultiplePolarityPragmas xs) = fsep $
pwords "Multiple polarity pragmas for" ++ map pretty xs
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 (MissingDefinition x) = fsep $
pwords "Missing definition for" ++ [pretty x]
pretty (MissingWithClauses x) = 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 (WrongParameters x sig def) = fsep $
pwords "List of parameters " ++ map pretty def ++
pwords " does not match parameters " ++ map pretty sig ++
pwords " of previous signature for " ++ [pretty x]
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 (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 (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 (NotAllowedInMutual nd) = fsep $
[text $ declName nd] ++ pwords "are not allowed in mutual blocks"
pretty (Codata _) = text $
"The codata construction has been removed. " ++
"Use the INFINITY builtin instead."
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):" ++ map pretty xs
pretty (UnknownFixityInMixfixDecl xs) = fsep $
pwords "The following mixfix names do not have an associated fixity declaration:" ++ 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 $
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 (InvalidTerminationCheckPragma _) = fsep $
pwords "Termination 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."
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 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 RecDef{} = "Records"
declName DataDef{} = "Data types"
data InMutual
= InMutual
| NotInMutual
deriving (Eq, Show)
data DataRecOrFun
= DataName { kindPosCheck :: PositivityCheck, kindParams :: Params }
| RecName { kindPosCheck :: PositivityCheck, kindParams :: Params }
| FunName TerminationCheck
deriving Data
instance Eq DataRecOrFun where
DataName _ p == DataName _ q = p == q
RecName _ p == RecName _ q = p == q
FunName _ == FunName _ = True
_ == _ = False
type Params = [Arg BoundName]
instance Show DataRecOrFun where
show (DataName _ n) = "data type"
show (RecName _ n) = "record type"
show (FunName{}) = "function"
isFunName :: DataRecOrFun -> Bool
isFunName (FunName{}) = True
isFunName _ = False
sameKind :: DataRecOrFun -> DataRecOrFun -> Bool
sameKind DataName{} DataName{} = True
sameKind RecName{} RecName{} = True
sameKind FunName{} FunName{} = True
sameKind _ _ = False
terminationCheck :: DataRecOrFun -> TerminationCheck
terminationCheck (FunName tc) = tc
terminationCheck _ = TerminationCheck
positivityCheck :: DataRecOrFun -> PositivityCheck
positivityCheck (DataName pc _) = pc
positivityCheck (RecName pc _) = pc
positivityCheck _ = True
combineTermChecks :: Range -> [TerminationCheck] -> Nice TerminationCheck
combineTermChecks 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
matchParameters
:: Name
-> DataRecOrFun
-> DataRecOrFun
-> Nice ()
matchParameters _ FunName{} FunName{} = return ()
matchParameters x sig def = loop (kindParams sig) (kindParams def)
where
failure = throwError $ WrongParameters x (kindParams sig) (kindParams def)
loop hs [] = unless (all notVisible hs) failure
loop [] (_:_) = failure
loop (h:hs) (j:js)
| h == j = loop hs js
| notVisible h, visible j = loop hs (j:js)
| otherwise = failure
newtype Nice a = Nice { unNice :: NiceEnv -> (Either DeclarationException a, NiceEnv) }
instance Functor Nice where
fmap f m = Nice $ \ s ->
let (r, s') = unNice m s in
case r of
Left e -> (Left e, s')
Right a -> (Right (f a), s')
instance Applicative Nice where
pure a = Nice $ \ s -> (Right a, s)
(<*>) = ap
instance Monad Nice where
return = pure
m >>= k = Nice $ \ s ->
let (r, s') = unNice m s in
case r of
Left e -> (Left e, s')
Right a -> unNice (k a) s'
instance MonadState NiceEnv Nice where
state f = Nice $ \ s -> first Right $ f s
instance MonadError DeclarationException Nice where
throwError e = Nice $ \ s -> (Left e, s)
catchError m h = Nice $ \ s ->
let (r, s') = unNice m s in
case r of
Left e -> unNice (h e) s'
Right a -> (Right a, s')
runNice :: Nice a -> (Either DeclarationException a, NiceWarnings)
runNice m = second (reverse . niceWarn) $ unNice m initNiceEnv
data NiceEnv = NiceEnv
{ _loneSigs :: LoneSigs
, _termChk :: TerminationCheck
, _posChk :: PositivityCheck
, _catchall :: Catchall
, fixs :: Fixities
, pols :: Polarities
, niceWarn :: NiceWarnings
}
type LoneSigs = Map Name DataRecOrFun
type Fixities = Map Name Fixity'
type Polarities = Map Name [Occurrence]
type NiceWarnings = [DeclarationWarning]
initNiceEnv :: NiceEnv
initNiceEnv = NiceEnv
{ _loneSigs = empty
, _termChk = TerminationCheck
, _posChk = True
, _catchall = False
, fixs = empty
, pols = empty
, niceWarn = []
}
loneSigs :: Lens' LoneSigs NiceEnv
loneSigs f e = f (_loneSigs e) <&> \ s -> e { _loneSigs = s }
addLoneSig :: Name -> DataRecOrFun -> Nice ()
addLoneSig x k = loneSigs %== \ s -> do
let (mr, s') = Map.insertLookupWithKey (\ k new old -> new) x k s
case mr of
Nothing -> return s'
Just{} -> throwError $ DuplicateDefinition x
removeLoneSig :: Name -> Nice ()
removeLoneSig x = loneSigs %= Map.delete x
getSig :: Name -> Nice (Maybe DataRecOrFun)
getSig x = Map.lookup x <$> use loneSigs
noLoneSigs :: Nice Bool
noLoneSigs = null <$> use loneSigs
checkLoneSigs :: [(Name, a)] -> Nice ()
checkLoneSigs xs =
case xs of
[] -> return ()
(x, _):_ -> throwError $ MissingDefinition x
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
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
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 }
getFixity :: Name -> Nice Fixity'
getFixity x = Map.findWithDefault noFixity' x <$> gets fixs
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
data DeclKind
= LoneSig DataRecOrFun Name
| LoneDefs DataRecOrFun [Name]
| OtherDecl
deriving (Eq, Show)
declKind :: NiceDeclaration -> DeclKind
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 _ _ _ 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
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 NiceUnquoteDecl{} = OtherDecl
parameters :: [LamBinding] -> Params
parameters = List.concatMap $ \case
DomainFree i x -> [Arg i x]
DomainFull (TypedBindings _ (Arg _ TLet{})) -> []
DomainFull (TypedBindings _ (Arg i (TBind _ xs _))) -> for xs $ \ (WithHiding h x) ->
mergeHiding $ WithHiding h $ Arg i x
niceDeclarations :: [Declaration] -> Nice [NiceDeclaration]
niceDeclarations ds = do
(fixs, polarities) <- fixitiesAndPolarities ds
let declared = Set.fromList (concatMap declaredNames ds)
fixs <- ifNull (Map.keysSet fixs Set.\\ declared) (return fixs) $ \ unknownFixs -> do
niceWarning $ UnknownNamesInFixityDecl $ Set.toList unknownFixs
return $ Map.filterWithKey (\ k _ -> Set.member k declared) fixs
polarities <- ifNull (Map.keysSet polarities Set.\\ declared) (return polarities) $
\ unknownPols -> do
niceWarning $ UnknownNamesInPolarityPragmas $ Set.toList unknownPols
return $ Map.filterWithKey (\ k _ -> Set.member k declared) polarities
ifNull (Set.filter isOpenMixfix declared Set.\\ Map.keysSet fixs) (return ()) $
niceWarning . UnknownFixityInMixfixDecl . Set.toList
st <- get
put $ initNiceEnv { fixs = fixs, pols = polarities, niceWarn = niceWarn st }
ds <- nice ds
unlessNullM (Map.keys <$> gets pols) $ \ unusedPolarities -> do
niceWarning $ PolarityPragmasButNotPostulates unusedPolarities
checkLoneSigs . Map.toList =<< use loneSigs
res <- inferMutualBlocks ds
warns <- gets niceWarn
put $ st { niceWarn = warns }
return res
where
declaredNames :: Declaration -> [Name]
declaredNames d = case d of
TypeSig _ x _ -> [x]
Field _ x _ -> [x]
FunClause (LHS p [] []) _ _ _
| IdentP (QName x) <- removeSingletonRawAppP p
-> [x]
FunClause{} -> []
DataSig _ _ x _ _ -> [x]
Data _ _ x _ _ cs -> x : concatMap declaredNames cs
RecordSig _ x _ _ -> [x]
Record _ x _ _ c _ _ _ -> x : foldMap (:[]) (fst <$> c)
Infix _ _ -> []
Syntax _ _ -> []
PatternSyn _ x _ _ -> [x]
Mutual _ ds -> concatMap declaredNames ds
Abstract _ ds -> concatMap declaredNames ds
Private _ _ ds -> concatMap declaredNames ds
InstanceB _ ds -> concatMap declaredNames ds
Macro _ ds -> concatMap declaredNames ds
Postulate _ ds -> concatMap declaredNames ds
Primitive _ ds -> concatMap declaredNames ds
Open{} -> []
Import{} -> []
ModuleMacro{} -> []
Module{} -> []
UnquoteDecl _ xs _ -> xs
UnquoteDef{} -> []
Pragma{} -> []
inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [] = return []
inferMutualBlocks (d : ds) =
case declKind d of
OtherDecl -> (d :) <$> inferMutualBlocks ds
LoneDefs{} -> (d :) <$> inferMutualBlocks ds
LoneSig k x -> do
addLoneSig x k
((tcs, pcs), (ds0, ds1)) <- untilAllDefined ([terminationCheck k], [positivityCheck k]) ds
tc <- combineTermChecks (getRange d) tcs
(NiceMutual (getRange (d : ds0)) tc (and pcs) (d : ds0) :) <$> inferMutualBlocks ds1
where
untilAllDefined :: ([TerminationCheck], [PositivityCheck])
-> [NiceDeclaration]
-> Nice (([TerminationCheck], [PositivityCheck]), ([NiceDeclaration], [NiceDeclaration]))
untilAllDefined (tc, pc) ds = do
done <- noLoneSigs
if done then return ((tc, pc), ([], ds)) else
case ds of
[] -> __IMPOSSIBLE__ <$ (checkLoneSigs . Map.toList =<< use loneSigs)
d : ds -> case declKind d of
LoneSig k x -> do
addLoneSig x k
cons d (untilAllDefined (terminationCheck k : tc, positivityCheck k : pc) ds)
LoneDefs k xs -> do
mapM_ removeLoneSig xs
cons d (untilAllDefined (terminationCheck k : tc, positivityCheck k : pc) ds)
OtherDecl -> cons d (untilAllDefined (tc, pc) 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 x t) -> do
termCheck <- use terminationCheckPragma
fx <- getFixity x
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
fixs <- gets fixs
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 x Nothing [d]
return (d , ds)
_ -> do
return ([NiceFunClause (getRange d) PublicAccess ConcreteDef termCheck catchall d] , ds)
[(x,(fits,rest))] -> do
removeLoneSig x
ds <- expandEllipsis fits
cs <- mkClauses x ds False
fx <- getFixity x
return ([FunDef (getRange fits) fits fx ConcreteDef NotInstanceDef termCheck x cs] , rest)
l -> throwError $ AmbiguousFunClauses lhs $ reverse $ map fst l
Field{} -> (,ds) <$> niceAxioms FieldBlock [ d ]
DataSig r CoInductive _ _ _ -> throwError (Codata r)
Data r CoInductive _ _ _ _ -> throwError (Codata r)
(DataSig r Inductive x tel t) -> do
pc <- use positivityCheckPragma
addLoneSig x (DataName pc $ parameters tel)
(,) <$> dataOrRec pc DataDef NiceDataSig (niceAxioms DataBlock) r x (Just (tel, t)) Nothing
<*> return ds
(Data r Inductive x tel mt cs) -> do
pc <- use positivityCheckPragma
mt <- defaultTypeSig (DataName pc $ parameters tel) x mt
(,) <$> dataOrRec pc DataDef NiceDataSig (niceAxioms DataBlock) r x ((tel,) <$> mt) (Just (tel, 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 mt cs) -> do
pc <- use positivityCheckPragma
mt <- defaultTypeSig (RecName pc $ parameters tel) x mt
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,) <$> mt) (Just (tel, cs))
<*> return ds
Mutual r [] -> justWarning $ EmptyMutual r
Mutual r ds' ->
(,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) <$> (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' -> (,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
fx <- getFixity n
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
tc <- use terminationCheckPragma
return ([NiceUnquoteDecl r fxs PublicAccess ConcreteDef NotInstanceDef tc xs e] , ds)
UnquoteDef r xs e -> do
fxs <- mapM getFixity xs
sigs <- map fst . filter (isFunName . snd) . Map.toList <$> use loneSigs
let missing = filter (`notElem` sigs) xs
if null missing
then do
mapM_ removeLoneSig xs
return ([NiceUnquoteDef r fxs PublicAccess ConcreteDef TerminationCheck 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 =
throwError $ PragmaNoTerminationCheck r
nicePragma (TerminationCheckPragma r tc) ds =
if canHaveTerminationCheckPragma ds then
withTerminationCheckPragma tc $ nice1 ds
else do
niceWarning $ InvalidTerminationCheckPragma 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 False $ nice1 ds
else do
niceWarning $ InvalidNoPositivityCheckPragma r
nice1 ds
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 _ ds -> any (canHaveTerminationCheckPragma . singleton) ds
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 _ ds -> any (canHaveNoPositivityCheckPragma . singleton) ds
(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
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
unless (k == k') $ matchParameters x k' k
Nothing <$ removeLoneSig x
dataOrRec
:: forall a
. PositivityCheck
-> (Range -> Fixity' -> IsAbstract -> PositivityCheck -> Name -> [LamBinding] -> [NiceConstructor] -> NiceDeclaration)
-> (Range -> Fixity' -> Access -> IsAbstract -> PositivityCheck -> Name -> [LamBinding] -> Expr -> NiceDeclaration)
-> ([a] -> Nice [NiceDeclaration])
-> Range
-> Name
-> Maybe ([LamBinding], Expr)
-> Maybe ([LamBinding], [a])
-> Nice [NiceDeclaration]
dataOrRec pc mkDef mkSig niceD r x mt mcs = do
mds <- Trav.forM mcs $ \ (tel, cs) -> (tel,) <$> niceD cs
f <- getFixity x
return $ catMaybes $
[ mt <&> \ (tel, t) -> mkSig (fuseRange x t) f PublicAccess ConcreteDef pc x tel t
, mds <&> \ (tel, ds) -> mkDef r f ConcreteDef pc x (caseMaybe mt tel $ const $ concatMap dropType tel) ds
]
where
dropType :: LamBinding -> [LamBinding]
dropType (DomainFull (TypedBindings _r (Arg ai (TBind _ xs _)))) =
map (mergeHiding . fmap (DomainFree ai)) xs
dropType (DomainFull (TypedBindings _r (Arg _ TLet{}))) = []
dropType b@DomainFree{} = [b]
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 x t -> do
fx <- getFixity x
return [ Axiom (getRange d) fx PublicAccess ConcreteDef NotInstanceDef rel Nothing x t ]
Field i x argt | b == FieldBlock -> do
fx <- getFixity x
return [ NiceField (getRange d) fx PublicAccess ConcreteDef i 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 f p a i rel Nothing x t) = PrimitiveFunction r f p a x t
toPrim _ = __IMPOSSIBLE__
mkFunDef info termCheck x mt ds0 = do
ds <- expandEllipsis ds0
cs <- mkClauses x ds False
f <- getFixity x
return [ FunSig (fuseRange x t) f PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck x t
, FunDef (getRange ds0) ds0 f ConcreteDef NotInstanceDef termCheck 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 _ _) _ _ _) : ds)
| 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) rhs wh ca -> do
case hasEllipsis' p0 of
ManyHoles -> throwError $ MultipleEllipses p0
OneHole cxt -> do
let p1 = cxt p
let d' = FunClause (LHS p1 eqs es) 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
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 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 (headMaybe 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
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
RawAppP _ [p'] -> removeSingletonRawAppP p'
ParenP _ p' -> removeSingletonRawAppP p'
_ -> p
mkOldMutual :: Range -> [NiceDeclaration] -> Nice NiceDeclaration
mkOldMutual r ds = do
checkLoneSigs loneNames
forM_ ds $ \case
Axiom{} -> return ()
NiceFunClause{} -> return ()
NicePatternSyn{} -> return ()
d -> when (declKind d == OtherDecl) $ throwError $ NotAllowedInMutual d
tc0 <- use terminationCheckPragma
let tcs = map termCheck ds
tc <- combineTermChecks r (tc0:tcs)
pc0 <- use positivityCheckPragma
let pc :: PositivityCheck
pc = pc0 && all positivityCheckOldMutual ds
return $ NiceMutual r tc pc $ sigs ++ other
where
(sigs, other) = List.partition isTypeSig ds
isTypeSig Axiom{} = True
isTypeSig d | LoneSig{} <- declKind d = True
isTypeSig _ = False
sigNames = [ (x, k) | LoneSig k x <- map declKind ds ]
defNames = [ (x, k) | LoneDefs k xs <- map declKind ds, x <- xs ]
loneNames = [ (x, k) | (x, k) <- sigNames, List.all ((x /=) . fst) defNames ]
termCheck (FunSig _ _ _ _ _ _ _ tc _ _) = tc
termCheck (FunDef _ _ _ _ _ tc _ _) = tc
termCheck (NiceMutual _ tc _ _) = __IMPOSSIBLE__
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 DataDef{} = TerminationCheck
termCheck RecDef{} = TerminationCheck
termCheck NicePatternSyn{} = TerminationCheck
positivityCheckOldMutual :: NiceDeclaration -> PositivityCheck
positivityCheckOldMutual (DataDef _ _ _ pc _ _ _) = pc
positivityCheckOldMutual (NiceDataSig _ _ _ _ pc _ _ _)= pc
positivityCheckOldMutual (NiceMutual _ _ pc _) = __IMPOSSIBLE__
positivityCheckOldMutual (NiceRecSig _ _ _ _ pc _ _ _) = pc
positivityCheckOldMutual (RecDef _ _ _ pc _ _ _ _ _ _) = pc
positivityCheckOldMutual _ = True
abstractBlock _ [] = return []
abstractBlock r ds = do
let (ds', anyChange) = runChange $ mkAbstract ds
inherited = r == noRange
if anyChange then return ds' else do
unless inherited $ niceWarning $ UselessAbstract r
return ds
privateBlock _ _ [] = return []
privateBlock r o ds = do
let (ds', anyChange) = runChange $ mkPrivate o ds
if anyChange then return ds' else do
when (o == UserWritten) $ niceWarning $ UselessPrivate r
return ds
instanceBlock _ [] = return []
instanceBlock r ds = do
let (ds', anyChange) = runChange $ mapM mkInstance ds
if anyChange then return ds' else do
niceWarning $ UselessInstance r
return ds
mkInstance :: Updater NiceDeclaration
mkInstance d =
case d of
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 r termCheck pc ds -> NiceMutual r termCheck pc <$> mapM mkInstance ds
NiceFunClause{} -> return d
FunDef r ds f a i tc x cs -> (\ i -> FunDef r ds f a i tc x cs) <$> setInstance i
NiceField{} -> return d
PrimitiveFunction{} -> return d
NiceUnquoteDef{} -> return d
NiceRecSig{} -> return d
NiceDataSig{} -> return d
NiceModuleMacro{} -> return d
NiceModule{} -> return d
NicePragma{} -> return d
NiceOpen{} -> return d
NiceImport{} -> return d
DataDef{} -> return d
RecDef{} -> return d
NicePatternSyn{} -> return d
setInstance :: Updater IsInstance
setInstance i = case i of
InstanceDef -> return i
_ -> dirty $ InstanceDef
macroBlock r ds = mapM mkMacro ds
mkMacro :: NiceDeclaration -> Nice NiceDeclaration
mkMacro d =
case d of
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)
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
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 i tc x cs -> (\ a -> FunDef r ds f a i 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
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
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
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 -> 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
instance MakePrivate Access where
mkPrivate o p = case p of
PrivateAccess{} -> return p
_ -> 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
FunDef r ds f a i tc x cls -> FunDef r ds f a i 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
mkPrivate o (AnyWhere ds) = return $ AnyWhere ds
mkPrivate o (SomeWhere m a ds) = mkPrivate o a <&> \ a' -> SomeWhere m a' ds
plusFixities :: Fixities -> Fixities -> Nice Fixities
plusFixities m1 m2
| not (null isect) = throwError $ MultipleFixityDecls isect
| otherwise = return $ Map.unionWithKey mergeFixites m1 m2
where
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__
s | s1 == noNotation = s2
| s2 == noNotation = s1
| otherwise = __IMPOSSIBLE__
isect = [ (x, map (Map.findWithDefault __IMPOSSIBLE__ x) [m1,m2])
| (x, False) <- Map.assocs $ Map.intersectionWith compatible m1 m2 ]
compatible (Fixity' f1 s1 _) (Fixity' f2 s2 _) =
(f1 == noFixity || f2 == noFixity ) &&
(s1 == noNotation || s2 == noNotation)
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)
instance Monoid (Nice (Fixities, Polarities)) where
mempty = return (Map.empty, Map.empty)
mappend = (<>)
fixitiesAndPolarities :: [Declaration] -> Nice (Fixities, Polarities)
fixitiesAndPolarities = foldMap $ \ d -> case d of
Pragma (PolarityPragma _ x occs) -> return (Map.empty, Map.singleton x occs)
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
)
Mutual _ ds' -> fixitiesAndPolarities ds'
Abstract _ ds' -> fixitiesAndPolarities ds'
Private _ _ ds' -> fixitiesAndPolarities ds'
InstanceB _ ds' -> fixitiesAndPolarities ds'
Macro _ ds' -> fixitiesAndPolarities ds'
TypeSig {} -> mempty
Field {} -> mempty
FunClause {} -> mempty
DataSig {} -> mempty
Data {} -> mempty
RecordSig {} -> mempty
Record {} -> mempty
PatternSyn {} -> mempty
Postulate {} -> mempty
Primitive {} -> mempty
Open {} -> mempty
Import {} -> mempty
ModuleMacro {} -> mempty
Module {} -> mempty
UnquoteDecl {} -> mempty
UnquoteDef {} -> mempty
Pragma {} -> mempty
notSoNiceDeclarations :: NiceDeclaration -> [Declaration]
notSoNiceDeclarations d = fixityDecl d ++
case d of
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 _ _ _ 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
fixityDecl d = nameAndFixity >>= \ (x, f) -> infixDecl (theFixity f) x ++ syntaxDecl (theNotation f) x
where
nameAndFixity = case d of
Axiom _ f _ _ _ _ _ x _ -> [(x, f)]
NiceField _ f _ _ _ x _ -> [(x, f)]
PrimitiveFunction _ f _ _ x _ -> [(x, f)]
NiceRecSig _ f _ _ _ x _ _ -> [(x, f)]
NiceDataSig _ f _ _ _ x _ _ -> [(x, f)]
FunSig _ f _ _ _ _ _ _ x _ -> [(x, f)]
NicePatternSyn _ f x _ _ -> [(x, f)]
NiceUnquoteDecl _ fs _ _ _ _ xs _ -> zip xs fs
NiceUnquoteDef _ fs _ _ _ xs _ -> zip xs fs
NiceMutual{} -> []
NiceModule{} -> []
NiceModuleMacro{} -> []
NiceOpen{} -> []
NiceImport{} -> []
NicePragma{} -> []
NiceFunClause{} -> []
FunDef{} -> []
DataDef{} -> []
RecDef{} -> []
infixDecl f x = [Infix f [x] | notElem f [defaultFixity, noFixity]]
syntaxDecl n x = [Syntax x n | not (null n) ]
niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract
niceHasAbstract d =
case d of
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
DataDef _ _ a _ _ _ _ -> Just a
RecDef _ _ a _ _ _ _ _ _ _ -> Just a
NicePatternSyn{} -> Nothing
NiceUnquoteDecl _ _ _ a _ _ _ _ -> Just a
NiceUnquoteDef _ _ _ a _ _ _ -> Just a