module Agda.Syntax.Concrete.Definitions
( NiceDeclaration(..)
, NiceConstructor, NiceTypeSignature
, Clause(..)
, DeclarationException(..)
, DeclarationWarning(..), DeclarationWarning'(..), unsafeDeclarationWarning
, Nice, NiceEnv(..), runNice
, niceDeclarations
, notSoNiceDeclarations
, niceHasAbstract
, Measure
, declarationWarningName
) where
import Prelude hiding (null)
import Control.Monad ( forM, guard, unless, void, when )
import Control.Monad.Except ( )
import Control.Monad.Reader ( asks )
import Control.Monad.State ( MonadState(..), gets, StateT, runStateT )
import Control.Monad.Trans ( lift )
import Data.Bifunctor
import Data.Either (isLeft, isRight)
import Data.Function (on)
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Maybe
import Data.Semigroup ( Semigroup(..) )
import qualified Data.List as List
import qualified Data.Foldable as Fold
import qualified Data.Traversable as Trav
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.Syntax.Common.Pretty
import Agda.Syntax.Concrete.Definitions.Errors
import Agda.Syntax.Concrete.Definitions.Monad
import Agda.Syntax.Concrete.Definitions.Types
import Agda.Utils.AffineHole
import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List (isSublistOf, spanJust)
import Agda.Utils.List1 (List1, pattern (:|), (<|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Three
import Agda.Utils.Tuple
import Agda.Utils.Update
import Agda.Utils.Impossible
combineTerminationChecks :: Range -> [TerminationCheck] -> Nice TerminationCheck
combineTerminationChecks :: Range -> [TerminationCheck] -> Nice TerminationCheck
combineTerminationChecks Range
r = [TerminationCheck] -> Nice TerminationCheck
loop
where
loop :: [TerminationCheck] -> Nice TerminationCheck
loop :: [TerminationCheck] -> Nice TerminationCheck
loop [] = TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
TerminationCheck
loop (TerminationCheck
tc : [TerminationCheck]
tcs) = do
tc' <- [TerminationCheck] -> Nice TerminationCheck
loop [TerminationCheck]
tcs
case (tc, tc') of
(TerminationCheck
TerminationCheck , TerminationCheck
tc' ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
tc'
(TerminationCheck
tc , TerminationCheck
TerminationCheck ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
tc
(TerminationCheck
NonTerminating , TerminationCheck
NonTerminating ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
NonTerminating
(TerminationCheck
NoTerminationCheck , TerminationCheck
NoTerminationCheck ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
NoTerminationCheck
(TerminationCheck
NoTerminationCheck , TerminationCheck
Terminating ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
Terminating
(TerminationCheck
Terminating , TerminationCheck
NoTerminationCheck ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
Terminating
(TerminationCheck
Terminating , TerminationCheck
Terminating ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
Terminating
(TerminationMeasure{} , TerminationMeasure{} ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
tc
(TerminationMeasure Range
r Name
_, TerminationCheck
NoTerminationCheck ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
(TerminationMeasure Range
r Name
_, TerminationCheck
Terminating ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
(TerminationCheck
NoTerminationCheck , TerminationMeasure Range
r Name
_) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
(TerminationCheck
Terminating , TerminationMeasure Range
r Name
_) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
(TerminationMeasure Range
r Name
_, TerminationCheck
NonTerminating ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
(TerminationCheck
NonTerminating , TerminationMeasure Range
r Name
_) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
(TerminationCheck
NoTerminationCheck , TerminationCheck
NonTerminating ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
(TerminationCheck
Terminating , TerminationCheck
NonTerminating ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
(TerminationCheck
NonTerminating , TerminationCheck
NoTerminationCheck ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
(TerminationCheck
NonTerminating , TerminationCheck
Terminating ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
failure :: Range -> Nice a
failure Range
r = DeclarationException' -> Nice a
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice a)
-> DeclarationException' -> Nice a
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationException'
InvalidMeasureMutual Range
r
combineCoverageChecks :: [CoverageCheck] -> CoverageCheck
combineCoverageChecks :: [CoverageCheck] -> CoverageCheck
combineCoverageChecks = [CoverageCheck] -> CoverageCheck
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold
combinePositivityChecks :: [PositivityCheck] -> PositivityCheck
combinePositivityChecks :: [PositivityCheck] -> PositivityCheck
combinePositivityChecks = [PositivityCheck] -> PositivityCheck
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold
data DeclKind
= LoneSigDecl Range DataRecOrFun Name
| LoneDefs DataRecOrFun [Name]
| OtherDecl
deriving (DeclKind -> DeclKind -> Bool
(DeclKind -> DeclKind -> Bool)
-> (DeclKind -> DeclKind -> Bool) -> Eq DeclKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DeclKind -> DeclKind -> Bool
== :: DeclKind -> DeclKind -> Bool
$c/= :: DeclKind -> DeclKind -> Bool
/= :: DeclKind -> DeclKind -> Bool
Eq, Int -> DeclKind -> ShowS
[DeclKind] -> ShowS
DeclKind -> String
(Int -> DeclKind -> ShowS)
-> (DeclKind -> String) -> ([DeclKind] -> ShowS) -> Show DeclKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DeclKind -> ShowS
showsPrec :: Int -> DeclKind -> ShowS
$cshow :: DeclKind -> String
show :: DeclKind -> String
$cshowList :: [DeclKind] -> ShowS
showList :: [DeclKind] -> ShowS
Show)
declKind :: NiceDeclaration -> DeclKind
declKind :: NiceDeclaration -> DeclKind
declKind (FunSig Range
r Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
tc CoverageCheck
cc Name
x Expr
_) = Range -> DataRecOrFun -> Name -> DeclKind
LoneSigDecl Range
r (TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName TerminationCheck
tc CoverageCheck
cc) Name
x
declKind (NiceRecSig Range
r Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
_ Expr
_) = Range -> DataRecOrFun -> Name -> DeclKind
LoneSigDecl Range
r (PositivityCheck -> UniverseCheck -> DataRecOrFun
RecName PositivityCheck
pc UniverseCheck
uc) Name
x
declKind (NiceDataSig Range
r Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
_ Expr
_) = Range -> DataRecOrFun -> Name -> DeclKind
LoneSigDecl Range
r (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) Name
x
declKind (FunDef Range
r [Declaration]
_ IsAbstract
abs IsInstance
ins TerminationCheck
tc CoverageCheck
cc Name
x [Clause]
_) = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName TerminationCheck
tc CoverageCheck
cc) [Name
x]
declKind (NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
pars [NiceDeclaration]
_) = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) [Name
x]
declKind (NiceUnquoteData Range
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [Name]
_ Expr
_) = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) [Name
x]
declKind (NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
_ [LamBinding]
pars [Declaration]
_) = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
RecName PositivityCheck
pc UniverseCheck
uc) [Name
x]
declKind (NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
cc [Name]
xs Expr
_) = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName TerminationCheck
tc CoverageCheck
cc) [Name]
xs
declKind Axiom{} = DeclKind
OtherDecl
declKind NiceField{} = DeclKind
OtherDecl
declKind PrimitiveFunction{} = DeclKind
OtherDecl
declKind NiceMutual{} = DeclKind
OtherDecl
declKind NiceModule{} = DeclKind
OtherDecl
declKind NiceModuleMacro{} = DeclKind
OtherDecl
declKind NiceOpen{} = DeclKind
OtherDecl
declKind NiceImport{} = DeclKind
OtherDecl
declKind NicePragma{} = DeclKind
OtherDecl
declKind NiceFunClause{} = DeclKind
OtherDecl
declKind NicePatternSyn{} = DeclKind
OtherDecl
declKind NiceGeneralize{} = DeclKind
OtherDecl
declKind NiceUnquoteDecl{} = DeclKind
OtherDecl
declKind NiceLoneConstructor{} = DeclKind
OtherDecl
declKind NiceOpaque{} = DeclKind
OtherDecl
replaceSigs
:: LoneSigs
-> [NiceDeclaration]
-> [NiceDeclaration]
replaceSigs :: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps = if LoneSigs -> Bool
forall k a. Map k a -> Bool
Map.null LoneSigs
ps then [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> a
id else \case
[] -> [NiceDeclaration]
forall a. HasCallStack => a
__IMPOSSIBLE__
(NiceDeclaration
d:[NiceDeclaration]
ds) ->
case NiceDeclaration -> Maybe (Name, NiceDeclaration)
replaceable NiceDeclaration
d of
Just (Name
x, NiceDeclaration
axiom)
| (Just (LoneSig Range
_ Name
x' DataRecOrFun
_), LoneSigs
ps') <- (Name -> LoneSig -> Maybe LoneSig)
-> Name -> LoneSigs -> (Maybe LoneSig, LoneSigs)
forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (\ Name
_ LoneSig
_ -> Maybe LoneSig
forall a. Maybe a
Nothing) Name
x LoneSigs
ps
, Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x'
-> NiceDeclaration
axiom NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps' [NiceDeclaration]
ds
Maybe (Name, NiceDeclaration)
_ -> NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps [NiceDeclaration]
ds
where
replaceable :: NiceDeclaration -> Maybe (Name, NiceDeclaration)
replaceable :: NiceDeclaration -> Maybe (Name, NiceDeclaration)
replaceable = \case
FunSig Range
r Access
acc IsAbstract
abst IsInstance
inst IsMacro
_ ArgInfo
argi TerminationCheck
_ CoverageCheck
_ Name
x' Expr
e ->
let x :: Name
x = if Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x' then Range -> Name
noName (Name -> Range
nameRange Name
x') else Name
x' in
(Name, NiceDeclaration) -> Maybe (Name, NiceDeclaration)
forall a. a -> Maybe a
Just (Name
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
acc IsAbstract
abst IsInstance
inst ArgInfo
argi Name
x' Expr
e)
NiceRecSig Range
r Erased
erased Access
acc IsAbstract
abst PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
pars Expr
t ->
let e :: Expr
e = Expr -> Expr
Generalized (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Telescope -> Expr -> Expr
makePi (Range -> [LamBinding] -> Telescope
lamBindingsToTelescope Range
r [LamBinding]
pars) Expr
t in
(Name, NiceDeclaration) -> Maybe (Name, NiceDeclaration)
forall a. a -> Maybe a
Just (Name
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
acc IsAbstract
abst IsInstance
NotInstanceDef
(Quantity -> ArgInfo -> ArgInfo
forall a. LensQuantity a => Quantity -> a -> a
setQuantity (Erased -> Quantity
asQuantity Erased
erased) ArgInfo
defaultArgInfo) Name
x Expr
e)
NiceDataSig Range
r Erased
erased Access
acc IsAbstract
abst PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
pars Expr
t ->
let e :: Expr
e = Expr -> Expr
Generalized (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Telescope -> Expr -> Expr
makePi (Range -> [LamBinding] -> Telescope
lamBindingsToTelescope Range
r [LamBinding]
pars) Expr
t in
(Name, NiceDeclaration) -> Maybe (Name, NiceDeclaration)
forall a. a -> Maybe a
Just (Name
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
acc IsAbstract
abst IsInstance
NotInstanceDef
(Quantity -> ArgInfo -> ArgInfo
forall a. LensQuantity a => Quantity -> a -> a
setQuantity (Erased -> Quantity
asQuantity Erased
erased) ArgInfo
defaultArgInfo) Name
x Expr
e)
NiceDeclaration
_ -> Maybe (Name, NiceDeclaration)
forall a. Maybe a
Nothing
niceDeclarations :: Fixities -> [Declaration] -> Nice [NiceDeclaration]
niceDeclarations :: Fixities -> [Declaration] -> Nice [NiceDeclaration]
niceDeclarations Fixities
fixs [Declaration]
ds = do
st <- Nice NiceState
forall s (m :: * -> *). MonadState s m => m s
get
put $ initNiceState { niceWarn = niceWarn st }
nds <- nice ds
ps <- use loneSigs
checkLoneSigs ps
let ds = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps [NiceDeclaration]
nds
res <- inferMutualBlocks ds
warns <- gets niceWarn
put $ st { niceWarn = warns }
return res
where
inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [] = [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []
inferMutualBlocks (NiceDeclaration
d : [NiceDeclaration]
ds) =
case NiceDeclaration -> DeclKind
declKind NiceDeclaration
d of
DeclKind
OtherDecl -> (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
:) ([NiceDeclaration] -> [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [NiceDeclaration]
ds
LoneDefs{} -> (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
:) ([NiceDeclaration] -> [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [NiceDeclaration]
ds
LoneSigDecl Range
r DataRecOrFun
k Name
x -> do
_ <- Range -> Name -> DataRecOrFun -> Nice Name
addLoneSig Range
r Name
x DataRecOrFun
k
InferredMutual checks nds0 ds1 <- untilAllDefined (mutualChecks k) ds
ps <- use loneSigs
checkLoneSigs ps
let ds0 = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: [NiceDeclaration]
nds0)
tc <- combineTerminationChecks (getRange d) (mutualTermination checks)
let cc = [CoverageCheck] -> CoverageCheck
combineCoverageChecks (MutualChecks -> [CoverageCheck]
mutualCoverage MutualChecks
checks)
let pc = [PositivityCheck] -> PositivityCheck
combinePositivityChecks (MutualChecks -> [PositivityCheck]
mutualPositivity MutualChecks
checks)
(NiceMutual empty tc cc pc ds0 :) <$> inferMutualBlocks ds1
where
untilAllDefined :: MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined :: MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined MutualChecks
checks [NiceDeclaration]
ds = do
done <- Nice Bool
noLoneSigs
if done then return (InferredMutual checks [] ds) else
case ds of
[] -> InferredMutual -> Nice InferredMutual
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (MutualChecks
-> [NiceDeclaration] -> [NiceDeclaration] -> InferredMutual
InferredMutual MutualChecks
checks [] [NiceDeclaration]
ds)
NiceDeclaration
d : [NiceDeclaration]
ds -> case NiceDeclaration -> DeclKind
declKind NiceDeclaration
d of
LoneSigDecl Range
r DataRecOrFun
k Name
x -> do
Nice Name -> Nice ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Nice Name -> Nice ()) -> Nice Name -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> Name -> DataRecOrFun -> Nice Name
addLoneSig Range
r Name
x DataRecOrFun
k
NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock NiceDeclaration
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined (DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) [NiceDeclaration]
ds
LoneDefs DataRecOrFun
k [Name]
xs -> do
(Name -> Nice ()) -> [Name] -> Nice ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Name -> Nice ()
removeLoneSig [Name]
xs
NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock NiceDeclaration
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined (DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) [NiceDeclaration]
ds
DeclKind
OtherDecl -> NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock NiceDeclaration
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined MutualChecks
checks [NiceDeclaration]
ds
nice :: [Declaration] -> Nice [NiceDeclaration]
nice :: [Declaration] -> Nice [NiceDeclaration]
nice [] = [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []
nice [Declaration]
ds = do
(xs , ys) <- [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
(xs ++) <$> nice ys
nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [] = ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
nice1 (Declaration
d:[Declaration]
ds) = do
let justWarning :: HasCallStack => DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning :: HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning DeclarationWarning'
w = do
(CallStack -> Nice ()) -> Nice ()
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> Nice ()) -> Nice ())
-> (CallStack -> Nice ()) -> Nice ()
forall a b. (a -> b) -> a -> b
$ DeclarationWarning' -> CallStack -> Nice ()
declarationWarning' DeclarationWarning'
w
[Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
case Declaration
d of
TypeSig ArgInfo
info TacticAttribute
_tac Name
x Expr
t -> do
termCheck <- Lens' NiceState TerminationCheck -> Nice TerminationCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (TerminationCheck -> f TerminationCheck)
-> NiceState -> f NiceState
Lens' NiceState TerminationCheck
terminationCheckPragma
covCheck <- use coverageCheckPragma
let r = Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x
x' <- addLoneSig r x $ FunName termCheck covCheck
return ([FunSig r PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck covCheck x' t] , ds)
FieldSig{} -> Nice ([NiceDeclaration], [Declaration])
forall a. HasCallStack => a
__IMPOSSIBLE__
Generalize KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyGeneralize KwRange
r
Generalize KwRange
_ [Declaration]
sigs -> do
gs <- [Declaration]
-> (Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Declaration]
sigs ((Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration])
-> (Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ \case
sig :: Declaration
sig@(TypeSig ArgInfo
info TacticAttribute
tac Name
x Expr
t) -> do
Bool -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
Hidden) (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$
HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
HiddenGeneralize (Range -> DeclarationWarning') -> Range -> DeclarationWarning'
forall a b. (a -> b) -> a -> b
$ Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x
NiceDeclaration -> Nice NiceDeclaration
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration -> Nice NiceDeclaration)
-> NiceDeclaration -> Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> ArgInfo
-> TacticAttribute
-> Name
-> Expr
-> NiceDeclaration
NiceGeneralize (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
sig) Access
PublicAccess ArgInfo
info TacticAttribute
tac Name
x Expr
t
Declaration
_ -> Nice NiceDeclaration
forall a. HasCallStack => a
__IMPOSSIBLE__
return (gs, ds)
(FunClause LHS
lhs RHS
_ WhereClause
_ Bool
_) -> do
termCheck <- Lens' NiceState TerminationCheck -> Nice TerminationCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (TerminationCheck -> f TerminationCheck)
-> NiceState -> f NiceState
Lens' NiceState TerminationCheck
terminationCheckPragma
covCheck <- use coverageCheckPragma
catchall <- popCatchallPragma
xs <- loneFuns <$> use loneSigs
case [ (x, (x', fits, rest))
| (x, 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
lhs of
LHS Pattern
p [] [] | Just Name
x <- Pattern -> Maybe Name
isSingleIdentifierP Pattern
p -> do
d <- ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Maybe Expr
-> [Declaration]
-> Nice [NiceDeclaration]
mkFunDef (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
defaultArgInfo) TerminationCheck
termCheck CoverageCheck
covCheck Name
x Maybe Expr
forall a. Maybe a
Nothing [Declaration
d]
return (d , ds)
LHS
_ -> do
([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Bool
-> Declaration
-> NiceDeclaration
NiceFunClause (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef TerminationCheck
termCheck CoverageCheck
covCheck Bool
catchall Declaration
d] , [Declaration]
ds)
[(Name
x,(Name
x',[Declaration]
fits,[Declaration]
rest))] -> do
Name -> Nice ()
removeLoneSig Name
x
ds <- [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
fits
cs <- mkClauses x' ds False
return ([FunDef (getRange fits) fits ConcreteDef NotInstanceDef termCheck covCheck x' cs] , rest)
(Name, (Name, [Declaration], [Declaration]))
xf:[(Name, (Name, [Declaration], [Declaration]))]
xfs -> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ LHS -> List1 Name -> DeclarationException'
AmbiguousFunClauses LHS
lhs (List1 Name -> DeclarationException')
-> List1 Name -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ List1 Name -> List1 Name
forall a. NonEmpty a -> NonEmpty a
List1.reverse (List1 Name -> List1 Name) -> List1 Name -> List1 Name
forall a b. (a -> b) -> a -> b
$ ((Name, (Name, [Declaration], [Declaration])) -> Name)
-> NonEmpty (Name, (Name, [Declaration], [Declaration]))
-> List1 Name
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, (Name, [Declaration], [Declaration])) -> Name
forall a b. (a, b) -> a
fst (NonEmpty (Name, (Name, [Declaration], [Declaration]))
-> List1 Name)
-> NonEmpty (Name, (Name, [Declaration], [Declaration]))
-> List1 Name
forall a b. (a -> b) -> a -> b
$ (Name, (Name, [Declaration], [Declaration]))
xf (Name, (Name, [Declaration], [Declaration]))
-> [(Name, (Name, [Declaration], [Declaration]))]
-> NonEmpty (Name, (Name, [Declaration], [Declaration]))
forall a. a -> [a] -> NonEmpty a
:| [(Name, (Name, [Declaration], [Declaration]))]
xfs
Field KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyField KwRange
r
Field KwRange
_ [Declaration]
fs -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
FieldBlock [Declaration]
fs
DataSig Range
r Erased
erased Name
x [LamBinding]
tel Expr
t -> do
pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma
uc <- use universeCheckPragma
_ <- addLoneSig r x $ DataName pc uc
(,ds) <$> dataOrRec pc uc NiceDataDef
(flip NiceDataSig erased) (niceAxioms DataBlock) r
x (Just (tel, t)) Nothing
Data Range
r Erased
erased Name
x [LamBinding]
tel Expr
t [Declaration]
cs -> do
pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma
uc <- use universeCheckPragma
uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
mt <- defaultTypeSig (DataName pc uc) x (Just t)
(,ds) <$> dataOrRec pc uc NiceDataDef
(flip NiceDataSig erased) (niceAxioms DataBlock) r
x ((tel,) <$> mt) (Just (tel, cs))
DataDef Range
r Name
x [LamBinding]
tel [Declaration]
cs -> do
pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma
uc <- use universeCheckPragma
uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
mt <- defaultTypeSig (DataName pc uc) x Nothing
(,ds) <$> dataOrRec pc uc NiceDataDef
(flip NiceDataSig defaultErased)
(niceAxioms DataBlock) r x ((tel,) <$> mt)
(Just (tel, cs))
RecordSig Range
r Erased
erased Name
x [LamBinding]
tel Expr
t -> do
pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma
uc <- use universeCheckPragma
_ <- addLoneSig r x $ RecName pc uc
return ( [NiceRecSig r erased PublicAccess ConcreteDef pc uc x
tel t]
, ds
)
Record Range
r Erased
erased Name
x [RecordDirective]
dir [LamBinding]
tel Expr
t [Declaration]
cs -> do
pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma
uc <- use universeCheckPragma
uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
mt <- defaultTypeSig (RecName pc uc) x (Just t)
(,ds) <$> dataOrRec pc uc
(\Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
tel [Declaration]
cs ->
Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> NiceDeclaration
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir [LamBinding]
tel [Declaration]
cs)
(flip NiceRecSig erased) return r x
((tel,) <$> mt) (Just (tel, cs))
RecordDef Range
r Name
x [RecordDirective]
dir [LamBinding]
tel [Declaration]
cs -> do
pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma
uc <- use universeCheckPragma
uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
mt <- defaultTypeSig (RecName pc uc) x Nothing
(,ds) <$> dataOrRec pc uc
(\Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
tel [Declaration]
cs ->
Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> NiceDeclaration
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir [LamBinding]
tel [Declaration]
cs)
(flip NiceRecSig defaultErased) return r x
((tel,) <$> mt) (Just (tel, cs))
Mutual KwRange
r [Declaration]
ds' -> do
KwRange -> String -> Nice ()
breakImplicitMutualBlock KwRange
r String
"`mutual` blocks"
case [Declaration]
ds' of
[] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyMutual KwRange
r
[Declaration]
_ -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> [NiceDeclaration]
forall el coll. Singleton el coll => el -> coll
singleton (NiceDeclaration -> [NiceDeclaration])
-> Nice NiceDeclaration -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
mkOldMutual KwRange
r ([NiceDeclaration] -> Nice NiceDeclaration)
-> Nice [NiceDeclaration] -> Nice NiceDeclaration
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds'))
InterleavedMutual KwRange
r [Declaration]
ds' -> do
KwRange -> String -> Nice ()
breakImplicitMutualBlock KwRange
r String
"`interleaved mutual` blocks"
case [Declaration]
ds' of
[] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyMutual KwRange
r
[Declaration]
_ -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> [NiceDeclaration]
forall el coll. Singleton el coll => el -> coll
singleton (NiceDeclaration -> [NiceDeclaration])
-> Nice NiceDeclaration -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
mkInterleavedMutual KwRange
r ([NiceDeclaration] -> Nice NiceDeclaration)
-> Nice [NiceDeclaration] -> Nice NiceDeclaration
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds'))
LoneConstructor KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyConstructor KwRange
r
LoneConstructor KwRange
r [Declaration]
ds' ->
((,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> ([NiceDeclaration] -> [NiceDeclaration])
-> [NiceDeclaration]
-> ([NiceDeclaration], [Declaration])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NiceDeclaration -> [NiceDeclaration]
forall el coll. Singleton el coll => el -> coll
singleton (NiceDeclaration -> [NiceDeclaration])
-> ([NiceDeclaration] -> NiceDeclaration)
-> [NiceDeclaration]
-> [NiceDeclaration]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KwRange -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor KwRange
r) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
ConstructorBlock [Declaration]
ds'
Abstract KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyAbstract KwRange
r
Abstract KwRange
r [Declaration]
ds' ->
(,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
abstractBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds')
Private KwRange
r Origin
UserWritten [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyPrivate KwRange
r
Private KwRange
r Origin
o [Declaration]
ds' ->
(,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
privateBlock KwRange
r Origin
o ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds')
InstanceB KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyInstance KwRange
r
InstanceB KwRange
r [Declaration]
ds' ->
(,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
instanceBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds')
Macro KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyMacro KwRange
r
Macro KwRange
r [Declaration]
ds' ->
(,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
macroBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds')
Postulate KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyPostulate KwRange
r
Postulate KwRange
_ [Declaration]
ds' ->
(,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
PostulateBlock [Declaration]
ds'
Primitive KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyPrimitive KwRange
r
Primitive KwRange
_ [Declaration]
ds' -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((NiceDeclaration -> NiceDeclaration)
-> [NiceDeclaration] -> [NiceDeclaration]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> NiceDeclaration
toPrim ([NiceDeclaration] -> [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
PrimitiveBlock [Declaration]
ds')
Module Range
r Erased
erased QName
x Telescope
tel [Declaration]
ds' -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration]))
-> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$
([Range
-> Access
-> IsAbstract
-> Erased
-> QName
-> Telescope
-> [Declaration]
-> NiceDeclaration
NiceModule Range
r Access
PublicAccess IsAbstract
ConcreteDef Erased
erased QName
x Telescope
tel [Declaration]
ds'], [Declaration]
ds)
ModuleMacro Range
r Erased
erased Name
x ModuleApplication
modapp OpenShortHand
op ImportDirective
is -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration]))
-> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$
([Range
-> Access
-> Erased
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> NiceDeclaration
NiceModuleMacro Range
r Access
PublicAccess Erased
erased Name
x ModuleApplication
modapp OpenShortHand
op ImportDirective
is], [Declaration]
ds)
Infix Fixity
_ List1 Name
_ -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Declaration]
ds)
Syntax Name
_ Notation
_ -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Declaration]
ds)
PatternSyn Range
r Name
n [WithHiding Name]
as Pattern
p -> do
([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> Name
-> [WithHiding Name]
-> Pattern
-> NiceDeclaration
NicePatternSyn Range
r Access
PublicAccess Name
n [WithHiding Name]
as Pattern
p] , [Declaration]
ds)
Open Range
r QName
x ImportDirective
is -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> QName -> ImportDirective -> NiceDeclaration
NiceOpen Range
r QName
x ImportDirective
is] , [Declaration]
ds)
Import Range
r QName
x Maybe AsName
as OpenShortHand
op ImportDirective
is -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> QName
-> Maybe AsName
-> OpenShortHand
-> ImportDirective
-> NiceDeclaration
NiceImport Range
r QName
x Maybe AsName
as OpenShortHand
op ImportDirective
is] , [Declaration]
ds)
UnquoteDecl Range
r [Name]
xs Expr
e -> do
tc <- Lens' NiceState TerminationCheck -> Nice TerminationCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (TerminationCheck -> f TerminationCheck)
-> NiceState -> f NiceState
Lens' NiceState TerminationCheck
terminationCheckPragma
cc <- use coverageCheckPragma
return ([NiceUnquoteDecl r PublicAccess ConcreteDef NotInstanceDef tc cc xs e] , ds)
UnquoteDef Range
r [Name]
xs Expr
e -> do
sigs <- ((Name, Name) -> Name) -> [(Name, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> Name
forall a b. (a, b) -> a
fst ([(Name, Name)] -> [Name])
-> (LoneSigs -> [(Name, Name)]) -> LoneSigs -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LoneSigs -> [(Name, Name)]
loneFuns (LoneSigs -> [Name]) -> Nice LoneSigs -> Nice [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' NiceState LoneSigs -> Nice LoneSigs
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
Lens' NiceState LoneSigs
loneSigs
List1.ifNotNull (filter (`notElem` sigs) xs)
(declarationException . UnquoteDefRequiresSignature)
$ do
mapM_ removeLoneSig xs
return ([NiceUnquoteDef r PublicAccess ConcreteDef TerminationCheck YesCoverageCheck xs e] , ds)
UnquoteData Range
r Name
xs [Name]
cs Expr
e -> do
pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma
uc <- use universeCheckPragma
return ([NiceUnquoteData r PublicAccess ConcreteDef pc uc xs cs e], ds)
Pragma Pragma
p -> do
Nice Bool -> Nice () -> Nice ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((NiceEnv -> Bool) -> Nice Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks NiceEnv -> Bool
safeButNotBuiltin) (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$
Maybe DeclarationWarning'
-> (DeclarationWarning' -> Nice ()) -> Nice ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Pragma -> Maybe DeclarationWarning'
forall m. CMaybe DeclarationWarning' m => Pragma -> m
unsafePragma Pragma
p) ((DeclarationWarning' -> Nice ()) -> Nice ())
-> (DeclarationWarning' -> Nice ()) -> Nice ()
forall a b. (a -> b) -> a -> b
$ \ DeclarationWarning'
w ->
HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning DeclarationWarning'
w
Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nicePragma Pragma
p [Declaration]
ds
Opaque KwRange
r [Declaration]
ds' -> do
KwRange -> String -> Nice ()
breakImplicitMutualBlock KwRange
r String
"`opaque` blocks"
let
([[QName]]
unfoldings, [Declaration]
body) = ((Declaration -> Maybe [QName])
-> [Declaration] -> ([[QName]], [Declaration]))
-> [Declaration]
-> (Declaration -> Maybe [QName])
-> ([[QName]], [Declaration])
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Declaration -> Maybe [QName])
-> [Declaration] -> ([[QName]], [Declaration])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
spanMaybe [Declaration]
ds' ((Declaration -> Maybe [QName]) -> ([[QName]], [Declaration]))
-> (Declaration -> Maybe [QName]) -> ([[QName]], [Declaration])
forall a b. (a -> b) -> a -> b
$ \case
Unfolding KwRange
_ [QName]
ns -> [QName] -> Maybe [QName]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [QName]
ns
Declaration
_ -> Maybe [QName]
forall a. Maybe a
Nothing
decls0 <- [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
body
ps <- use loneSigs
checkLoneSigs ps
let decls = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps [NiceDeclaration]
decls0
body <- inferMutualBlocks decls
pure ([NiceOpaque r (concat unfoldings) body], ds)
Unfolding KwRange
r [QName]
_ -> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationException'
UnfoldingOutsideOpaque KwRange
r
nicePragma :: Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nicePragma :: Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nicePragma (TerminationCheckPragma Range
r (TerminationMeasure Range
_ Name
x)) [Declaration]
ds =
if [Declaration] -> Bool
canHaveTerminationMeasure [Declaration]
ds then
TerminationCheck
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. TerminationCheck -> Nice a -> Nice a
withTerminationCheckPragma (Range -> Name -> TerminationCheck
forall m. Range -> m -> TerminationCheck m
TerminationMeasure Range
r Name
x) (Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
else do
HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidTerminationCheckPragma Range
r
[Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
nicePragma (TerminationCheckPragma Range
r TerminationCheck
NoTerminationCheck) [Declaration]
ds = do
HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
PragmaNoTerminationCheck Range
r
Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nicePragma (Range -> TerminationCheck -> Pragma
TerminationCheckPragma Range
r TerminationCheck
forall m. TerminationCheck m
NonTerminating) [Declaration]
ds
nicePragma (TerminationCheckPragma Range
r TerminationCheck
tc) [Declaration]
ds =
if [Declaration] -> Bool
canHaveTerminationCheckPragma [Declaration]
ds then
TerminationCheck
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. TerminationCheck -> Nice a -> Nice a
withTerminationCheckPragma TerminationCheck
tc (Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
else do
HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidTerminationCheckPragma Range
r
[Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
nicePragma (NoCoverageCheckPragma Range
r) [Declaration]
ds =
if [Declaration] -> Bool
canHaveCoverageCheckPragma [Declaration]
ds then
CoverageCheck
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. CoverageCheck -> Nice a -> Nice a
withCoverageCheckPragma CoverageCheck
NoCoverageCheck (Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
else do
HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidCoverageCheckPragma Range
r
[Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
nicePragma (CatchallPragma Range
r) [Declaration]
ds =
if [Declaration] -> Bool
canHaveCatchallPragma [Declaration]
ds then
Bool
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. Bool -> Nice a -> Nice a
withCatchallPragma Bool
True (Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
else do
HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidCatchallPragma Range
r
[Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
nicePragma (NoPositivityCheckPragma Range
r) [Declaration]
ds =
if [Declaration] -> Bool
canHaveNoPositivityCheckPragma [Declaration]
ds then
PositivityCheck
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. PositivityCheck -> Nice a -> Nice a
withPositivityCheckPragma PositivityCheck
NoPositivityCheck (Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
else do
HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidNoPositivityCheckPragma Range
r
[Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
nicePragma (NoUniverseCheckPragma Range
r) [Declaration]
ds =
if [Declaration] -> Bool
canHaveNoUniverseCheckPragma [Declaration]
ds then
UniverseCheck
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. UniverseCheck -> Nice a -> Nice a
withUniverseCheckPragma UniverseCheck
NoUniverseCheck (Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
else do
HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidNoUniverseCheckPragma Range
r
[Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
nicePragma p :: Pragma
p@CompilePragma{} [Declaration]
ds = do
([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma (Pragma -> Range
forall a. HasRange a => a -> Range
getRange Pragma
p) Pragma
p], [Declaration]
ds)
nicePragma (PolarityPragma{}) [Declaration]
ds = ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Declaration]
ds)
nicePragma (BuiltinPragma Range
r RString
str qn :: QName
qn@(QName Name
x)) [Declaration]
ds = do
([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma Range
r (Range -> RString -> QName -> Pragma
BuiltinPragma Range
r RString
str QName
qn)], [Declaration]
ds)
nicePragma p :: Pragma
p@RewritePragma{} [Declaration]
ds = ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma (Pragma -> Range
forall a. HasRange a => a -> Range
getRange Pragma
p) Pragma
p], [Declaration]
ds)
nicePragma Pragma
p [Declaration]
ds = ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma (Pragma -> Range
forall a. HasRange a => a -> Range
getRange Pragma
p) Pragma
p], [Declaration]
ds)
canHaveTerminationMeasure :: [Declaration] -> Bool
canHaveTerminationMeasure :: [Declaration] -> Bool
canHaveTerminationMeasure [] = Bool
False
canHaveTerminationMeasure (Declaration
d:[Declaration]
ds) = case Declaration
d of
TypeSig{} -> Bool
True
(Pragma Pragma
p) | Pragma -> Bool
isAttachedPragma Pragma
p -> [Declaration] -> Bool
canHaveTerminationMeasure [Declaration]
ds
Declaration
_ -> Bool
False
canHaveTerminationCheckPragma :: [Declaration] -> Bool
canHaveTerminationCheckPragma :: [Declaration] -> Bool
canHaveTerminationCheckPragma [] = Bool
False
canHaveTerminationCheckPragma (Declaration
d:[Declaration]
ds) = case Declaration
d of
Mutual KwRange
_ [Declaration]
ds -> (Declaration -> Bool) -> [Declaration] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Declaration] -> Bool
canHaveTerminationCheckPragma ([Declaration] -> Bool)
-> (Declaration -> [Declaration]) -> Declaration -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Declaration -> [Declaration]
forall el coll. Singleton el coll => el -> coll
singleton) [Declaration]
ds
TypeSig{} -> Bool
True
FunClause{} -> Bool
True
UnquoteDecl{} -> Bool
True
(Pragma Pragma
p) | Pragma -> Bool
isAttachedPragma Pragma
p -> [Declaration] -> Bool
canHaveTerminationCheckPragma [Declaration]
ds
Declaration
_ -> Bool
False
canHaveCoverageCheckPragma :: [Declaration] -> Bool
canHaveCoverageCheckPragma :: [Declaration] -> Bool
canHaveCoverageCheckPragma = [Declaration] -> Bool
canHaveTerminationCheckPragma
canHaveCatchallPragma :: [Declaration] -> Bool
canHaveCatchallPragma :: [Declaration] -> Bool
canHaveCatchallPragma [] = Bool
False
canHaveCatchallPragma (Declaration
d:[Declaration]
ds) = case Declaration
d of
FunClause{} -> Bool
True
(Pragma Pragma
p) | Pragma -> Bool
isAttachedPragma Pragma
p -> [Declaration] -> Bool
canHaveCatchallPragma [Declaration]
ds
Declaration
_ -> Bool
False
canHaveNoPositivityCheckPragma :: [Declaration] -> Bool
canHaveNoPositivityCheckPragma :: [Declaration] -> Bool
canHaveNoPositivityCheckPragma [] = Bool
False
canHaveNoPositivityCheckPragma (Declaration
d:[Declaration]
ds) = case Declaration
d of
Mutual KwRange
_ [Declaration]
ds -> (Declaration -> Bool) -> [Declaration] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Declaration] -> Bool
canHaveNoPositivityCheckPragma ([Declaration] -> Bool)
-> (Declaration -> [Declaration]) -> Declaration -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Declaration -> [Declaration]
forall el coll. Singleton el coll => el -> coll
singleton) [Declaration]
ds
Data{} -> Bool
True
DataSig{} -> Bool
True
DataDef{} -> Bool
True
Record{} -> Bool
True
RecordSig{} -> Bool
True
RecordDef{} -> Bool
True
Pragma Pragma
p | Pragma -> Bool
isAttachedPragma Pragma
p -> [Declaration] -> Bool
canHaveNoPositivityCheckPragma [Declaration]
ds
Declaration
_ -> Bool
False
canHaveNoUniverseCheckPragma :: [Declaration] -> Bool
canHaveNoUniverseCheckPragma :: [Declaration] -> Bool
canHaveNoUniverseCheckPragma [] = Bool
False
canHaveNoUniverseCheckPragma (Declaration
d:[Declaration]
ds) = case Declaration
d of
Data{} -> Bool
True
DataSig{} -> Bool
True
DataDef{} -> Bool
True
Record{} -> Bool
True
RecordSig{} -> Bool
True
RecordDef{} -> Bool
True
Pragma Pragma
p | Pragma -> Bool
isAttachedPragma Pragma
p -> [Declaration] -> Bool
canHaveNoPositivityCheckPragma [Declaration]
ds
Declaration
_ -> Bool
False
isAttachedPragma :: Pragma -> Bool
isAttachedPragma :: Pragma -> Bool
isAttachedPragma = \case
TerminationCheckPragma{} -> Bool
True
CatchallPragma{} -> Bool
True
NoPositivityCheckPragma{} -> Bool
True
NoUniverseCheckPragma{} -> Bool
True
Pragma
_ -> Bool
False
defaultTypeSig :: DataRecOrFun -> Name -> Maybe Expr -> Nice (Maybe Expr)
defaultTypeSig :: DataRecOrFun -> Name -> Maybe Expr -> Nice (Maybe Expr)
defaultTypeSig DataRecOrFun
k Name
x t :: Maybe Expr
t@Just{} = Maybe Expr -> Nice (Maybe Expr)
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
t
defaultTypeSig DataRecOrFun
k Name
x Maybe Expr
Nothing = do
Nice (Maybe DataRecOrFun)
-> Nice (Maybe Expr)
-> (DataRecOrFun -> Nice (Maybe Expr))
-> Nice (Maybe Expr)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Name -> Nice (Maybe DataRecOrFun)
getSig Name
x) (Maybe Expr -> Nice (Maybe Expr)
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing) ((DataRecOrFun -> Nice (Maybe Expr)) -> Nice (Maybe Expr))
-> (DataRecOrFun -> Nice (Maybe Expr)) -> Nice (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ \ DataRecOrFun
k' -> do
Bool -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (DataRecOrFun -> DataRecOrFun -> Bool
sameKind DataRecOrFun
k DataRecOrFun
k') (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice ()
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ())
-> DeclarationException' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Name -> DataRecOrFun -> DataRecOrFun -> DeclarationException'
WrongDefinition Name
x DataRecOrFun
k' DataRecOrFun
k
Maybe Expr
forall a. Maybe a
Nothing Maybe Expr -> Nice () -> Nice (Maybe Expr)
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Name -> Nice ()
removeLoneSig Name
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 :: 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 PositivityCheck
pc UniverseCheck
uc Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> [decl]
-> NiceDeclaration
mkDef Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
mkSig [a] -> Nice [decl]
niceD Range
r Name
x Maybe ([LamBinding], Expr)
mt Maybe ([LamBinding], [a])
mcs = do
mds <- Maybe ([LamBinding], [a])
-> (([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
-> Nice (Maybe ([LamBinding], [decl]))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
Trav.forM Maybe ([LamBinding], [a])
mcs ((([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
-> Nice (Maybe ([LamBinding], [decl])))
-> (([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
-> Nice (Maybe ([LamBinding], [decl]))
forall a b. (a -> b) -> a -> b
$ \ ([LamBinding]
tel, [a]
cs) -> ([LamBinding]
tel,) ([decl] -> ([LamBinding], [decl]))
-> Nice [decl] -> Nice ([LamBinding], [decl])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Nice [decl]
niceD [a]
cs
let o | Maybe ([LamBinding], Expr) -> Bool
forall a. Maybe a -> Bool
isJust Maybe ([LamBinding], Expr)
mt Bool -> Bool -> Bool
&& Maybe ([LamBinding], [a]) -> Bool
forall a. Maybe a -> Bool
isJust Maybe ([LamBinding], [a])
mcs = Origin
Inserted
| Bool
otherwise = Origin
UserWritten
return $ catMaybes $
[ mt <&> \ ([LamBinding]
tel, Expr
t) -> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
mkSig (Name -> Expr -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Name
x Expr
t) Access
PublicAccess IsAbstract
ConcreteDef PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
tel Expr
t
, mds <&> \ ([LamBinding]
tel, [decl]
ds) -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> [decl]
-> NiceDeclaration
mkDef Range
r Origin
o IsAbstract
ConcreteDef PositivityCheck
pc UniverseCheck
uc Name
x (Maybe ([LamBinding], Expr)
-> [LamBinding]
-> (([LamBinding], Expr) -> [LamBinding])
-> [LamBinding]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe ([LamBinding], Expr)
mt [LamBinding]
tel ((([LamBinding], Expr) -> [LamBinding]) -> [LamBinding])
-> (([LamBinding], Expr) -> [LamBinding]) -> [LamBinding]
forall a b. (a -> b) -> a -> b
$ [LamBinding] -> ([LamBinding], Expr) -> [LamBinding]
forall a b. a -> b -> a
const ([LamBinding] -> ([LamBinding], Expr) -> [LamBinding])
-> [LamBinding] -> ([LamBinding], Expr) -> [LamBinding]
forall a b. (a -> b) -> a -> b
$ (LamBinding -> [LamBinding]) -> [LamBinding] -> [LamBinding]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LamBinding -> [LamBinding]
dropTypeAndModality [LamBinding]
tel) [decl]
ds
]
niceAxioms :: KindOfBlock -> [TypeSignatureOrInstanceBlock] -> Nice [NiceDeclaration]
niceAxioms :: KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
b [Declaration]
ds = [[NiceDeclaration]] -> [NiceDeclaration]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
List.concat ([[NiceDeclaration]] -> [NiceDeclaration])
-> Nice [[NiceDeclaration]] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> Nice [NiceDeclaration])
-> [Declaration] -> Nice [[NiceDeclaration]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (KindOfBlock -> Declaration -> Nice [NiceDeclaration]
niceAxiom KindOfBlock
b) [Declaration]
ds
niceAxiom :: KindOfBlock -> TypeSignatureOrInstanceBlock -> Nice [NiceDeclaration]
niceAxiom :: KindOfBlock -> Declaration -> Nice [NiceDeclaration]
niceAxiom KindOfBlock
b = \case
d :: Declaration
d@(TypeSig ArgInfo
rel TacticAttribute
_tac Name
x Expr
t) -> do
[NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef IsInstance
NotInstanceDef ArgInfo
rel Name
x Expr
t ]
d :: Declaration
d@(FieldSig IsInstance
i TacticAttribute
tac Name
x Arg Expr
argt) | KindOfBlock
b KindOfBlock -> KindOfBlock -> Bool
forall a. Eq a => a -> a -> Bool
== KindOfBlock
FieldBlock -> do
[NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceDeclaration
NiceField (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef IsInstance
i TacticAttribute
tac Name
x Arg Expr
argt ]
InstanceB KwRange
r [Declaration]
decls -> do
KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
instanceBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
InstanceBlock [Declaration]
decls
Private KwRange
r Origin
o [Declaration]
decls | KindOfBlock
PostulateBlock <- KindOfBlock
b -> do
KwRange -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
privateBlock KwRange
r Origin
o ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
b [Declaration]
decls
Pragma p :: Pragma
p@(RewritePragma Range
r Range
_ [QName]
_) -> [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Pragma -> NiceDeclaration
NicePragma Range
r Pragma
p ]
Pragma p :: Pragma
p@(OverlapPragma Range
r [QName]
_ OverlapMode
_) -> [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Pragma -> NiceDeclaration
NicePragma Range
r Pragma
p ]
Declaration
d -> DeclarationException' -> Nice [NiceDeclaration]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice [NiceDeclaration])
-> DeclarationException' -> Nice [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ KindOfBlock -> Range -> DeclarationException'
WrongContentBlock KindOfBlock
b (Range -> DeclarationException') -> Range -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d
toPrim :: NiceDeclaration -> NiceDeclaration
toPrim :: NiceDeclaration -> NiceDeclaration
toPrim (Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
t) = Range
-> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
PrimitiveFunction Range
r Access
p IsAbstract
a Name
x (ArgInfo -> Expr -> Arg Expr
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
rel Expr
t)
toPrim NiceDeclaration
_ = NiceDeclaration
forall a. HasCallStack => a
__IMPOSSIBLE__
mkFunDef :: ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Maybe Expr
-> [Declaration]
-> Nice [NiceDeclaration]
mkFunDef ArgInfo
info TerminationCheck
termCheck CoverageCheck
covCheck Name
x Maybe Expr
mt [Declaration]
ds0 = do
ds <- [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
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 :: Expr
t = Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
fromMaybe (Range -> Expr
underscore (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x)) Maybe Expr
mt
underscore :: Range -> Expr
underscore Range
r = Range -> Maybe String -> Expr
Underscore Range
r Maybe String
forall a. Maybe a
Nothing
expandEllipsis :: [Declaration] -> Nice [Declaration]
expandEllipsis :: [Declaration] -> Nice [Declaration]
expandEllipsis [] = [Declaration] -> Nice [Declaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []
expandEllipsis (d :: Declaration
d@(FunClause lhs :: LHS
lhs@(LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_) RHS
_ WhereClause
_ Bool
_) : [Declaration]
ds)
| Pattern -> Bool
forall a. HasEllipsis a => a -> Bool
hasEllipsis Pattern
p = (Declaration
d Declaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> [Declaration])
-> Nice [Declaration] -> Nice [Declaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
ds
| Bool
otherwise = (Declaration
d Declaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> [Declaration])
-> Nice [Declaration] -> Nice [Declaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [Declaration] -> Nice [Declaration]
expand (KillRangeT Pattern
forall a. KillRange a => KillRangeT a
killRange Pattern
p) [Declaration]
ds
where
expand :: Pattern -> [Declaration] -> Nice [Declaration]
expand :: Pattern -> [Declaration] -> Nice [Declaration]
expand Pattern
_ [] = [Declaration] -> Nice [Declaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []
expand Pattern
p (Declaration
d : [Declaration]
ds) = do
case Declaration
d of
Pragma (CatchallPragma Range
_) -> do
(Declaration
d Declaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> [Declaration])
-> Nice [Declaration] -> Nice [Declaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [Declaration] -> Nice [Declaration]
expand Pattern
p [Declaration]
ds
FunClause (LHS Pattern
p0 [RewriteEqn]
eqs [WithExpr]
es) RHS
rhs WhereClause
wh Bool
ca -> do
case Pattern -> AffineHole Pattern Pattern
forall p. CPatternLike p => p -> AffineHole Pattern p
hasEllipsis' Pattern
p0 of
AffineHole Pattern Pattern
ManyHoles -> DeclarationException' -> Nice [Declaration]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice [Declaration])
-> DeclarationException' -> Nice [Declaration]
forall a b. (a -> b) -> a -> b
$ Pattern -> DeclarationException'
MultipleEllipses Pattern
p0
OneHole KillRangeT Pattern
cxt ~(EllipsisP Range
r Maybe Pattern
Nothing) -> do
let p1 :: Pattern
p1 = KillRangeT Pattern
cxt KillRangeT Pattern -> KillRangeT Pattern
forall a b. (a -> b) -> a -> b
$ Range -> Maybe Pattern -> Pattern
EllipsisP Range
r (Maybe Pattern -> Pattern) -> Maybe Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Range -> KillRangeT Pattern
forall a. SetRange a => Range -> a -> a
setRange Range
r Pattern
p
let d' :: Declaration
d' = LHS -> RHS -> WhereClause -> Bool -> Declaration
FunClause (Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
LHS Pattern
p1 [RewriteEqn]
eqs [WithExpr]
es) RHS
rhs WhereClause
wh Bool
ca
(Declaration
d' Declaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> [Declaration])
-> Nice [Declaration] -> Nice [Declaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [Declaration] -> Nice [Declaration]
expand (if [WithExpr] -> Bool
forall a. Null a => a -> Bool
null [WithExpr]
es then Pattern
p else KillRangeT Pattern
forall a. KillRange a => KillRangeT a
killRange Pattern
p1) [Declaration]
ds
ZeroHoles Pattern
_ -> do
(Declaration
d Declaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> [Declaration])
-> Nice [Declaration] -> Nice [Declaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [Declaration] -> Nice [Declaration]
expand (if [WithExpr] -> Bool
forall a. Null a => a -> Bool
null [WithExpr]
es then Pattern
p else KillRangeT Pattern
forall a. KillRange a => KillRangeT a
killRange Pattern
p0) [Declaration]
ds
Declaration
_ -> Nice [Declaration]
forall a. HasCallStack => a
__IMPOSSIBLE__
expandEllipsis [Declaration]
_ = Nice [Declaration]
forall a. HasCallStack => a
__IMPOSSIBLE__
mkClauses :: Name -> [Declaration] -> Catchall -> Nice [Clause]
mkClauses :: Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
_ [] Bool
_ = [Clause] -> Nice [Clause]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []
mkClauses Name
x (Pragma (CatchallPragma Range
r) : [Declaration]
cs) Bool
True = do
HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidCatchallPragma Range
r
Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x [Declaration]
cs Bool
True
mkClauses Name
x (Pragma (CatchallPragma Range
r) : [Declaration]
cs) Bool
False = do
Bool -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Declaration] -> Bool
forall a. Null a => a -> Bool
null [Declaration]
cs) (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidCatchallPragma Range
r
Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x [Declaration]
cs Bool
True
mkClauses Name
x (FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
ca : [Declaration]
cs) Bool
catchall
| [WithExpr] -> Bool
forall a. Null a => a -> Bool
null (LHS -> [WithExpr]
lhsWithExpr LHS
lhs) Bool -> Bool -> Bool
|| LHS -> Bool
forall a. HasEllipsis a => a -> Bool
hasEllipsis LHS
lhs =
(Name -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
Clause Name
x (Bool
ca Bool -> Bool -> Bool
|| Bool
catchall) LHS
lhs RHS
rhs WhereClause
wh [] Clause -> [Clause] -> [Clause]
forall a. a -> [a] -> [a]
:) ([Clause] -> [Clause]) -> Nice [Clause] -> Nice [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x [Declaration]
cs Bool
False
mkClauses Name
x (FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
ca : [Declaration]
cs) Bool
catchall = do
Bool -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Declaration] -> Bool
forall a. Null a => a -> Bool
null [Declaration]
withClauses) (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice ()
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ())
-> DeclarationException' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Name -> LHS -> DeclarationException'
MissingWithClauses Name
x LHS
lhs
wcs <- Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x [Declaration]
withClauses Bool
False
(Clause x (ca || catchall) lhs rhs wh wcs :) <$> mkClauses x cs' False
where
([Declaration]
withClauses, [Declaration]
cs') = [Declaration] -> ([Declaration], [Declaration])
subClauses [Declaration]
cs
numWith :: Int
numWith = Pattern -> Int
forall p. CPatternLike p => p -> Int
numberOfWithPatterns Pattern
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [WithExpr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((WithExpr -> Bool) -> [WithExpr] -> [WithExpr]
forall a. (a -> Bool) -> [a] -> [a]
filter WithExpr -> Bool
forall a. LensHiding a => a -> Bool
visible [WithExpr]
es) where LHS Pattern
p [RewriteEqn]
_ [WithExpr]
es = LHS
lhs
subClauses :: [Declaration] -> ([Declaration],[Declaration])
subClauses :: [Declaration] -> ([Declaration], [Declaration])
subClauses (c :: Declaration
c@(FunClause (LHS Pattern
p0 [RewriteEqn]
_ [WithExpr]
_) RHS
_ WhereClause
_ Bool
_) : [Declaration]
cs)
| Pattern -> Bool
forall a. IsEllipsis a => a -> Bool
isEllipsis Pattern
p0 Bool -> Bool -> Bool
||
Pattern -> Int
forall p. CPatternLike p => p -> Int
numberOfWithPatterns Pattern
p0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
numWith = ([Declaration] -> [Declaration])
-> ([Declaration], [Declaration]) -> ([Declaration], [Declaration])
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> ([Declaration], [Declaration])
subClauses [Declaration]
cs)
| Bool
otherwise = ([], Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:[Declaration]
cs)
subClauses (c :: Declaration
c@(Pragma (CatchallPragma Range
r)) : [Declaration]
cs) = case [Declaration] -> ([Declaration], [Declaration])
subClauses [Declaration]
cs of
([], [Declaration]
cs') -> ([], Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:[Declaration]
cs')
([Declaration]
cs, [Declaration]
cs') -> (Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:[Declaration]
cs, [Declaration]
cs')
subClauses [] = ([],[])
subClauses [Declaration]
_ = ([Declaration], [Declaration])
forall a. HasCallStack => a
__IMPOSSIBLE__
mkClauses Name
_ [Declaration]
_ Bool
_ = Nice [Clause]
forall a. HasCallStack => a
__IMPOSSIBLE__
couldBeCallOf :: Maybe Fixity' -> Name -> Pattern -> Bool
couldBeCallOf :: Maybe Fixity' -> Name -> Pattern -> Bool
couldBeCallOf Maybe Fixity'
mFixity Name
x Pattern
p =
let
pns :: [Name]
pns = Pattern -> [Name]
patternNames Pattern
p
xStrings :: [String]
xStrings = Name -> [String]
nameStringParts Name
x
patStrings :: [String]
patStrings = (Name -> [String]) -> [Name] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Name -> [String]
nameStringParts [Name]
pns
in
case ([Name] -> Maybe Name
forall a. [a] -> Maybe a
listToMaybe [Name]
pns, Maybe Fixity'
mFixity) of
(Just Name
y, Maybe Fixity'
_) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y -> Bool
True
(Maybe Name, Maybe Fixity')
_ | [String]
xStrings [String] -> [String] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSublistOf` [String]
patStrings -> Bool
True
(Maybe Name
_, Just Fixity'
fix) ->
let notStrings :: [String]
notStrings = Notation -> [String]
stringParts (Fixity' -> Notation
theNotation Fixity'
fix)
in
Bool -> Bool
not ([String] -> Bool
forall a. Null a => a -> Bool
null [String]
notStrings) Bool -> Bool -> Bool
&& ([String]
notStrings [String] -> [String] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSublistOf` [String]
patStrings)
(Maybe Name, Maybe Fixity')
_ -> Bool
False
couldBeNiceFunClauseOf :: Maybe Fixity' -> Name -> NiceDeclaration
-> Maybe (MutualChecks, Declaration)
couldBeNiceFunClauseOf :: Maybe Fixity'
-> Name -> NiceDeclaration -> Maybe (MutualChecks, Declaration)
couldBeNiceFunClauseOf Maybe Fixity'
mf Name
n (NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
cc Bool
_ Declaration
d)
= ([TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [TerminationCheck
tc] [CoverageCheck
cc] [], Declaration
d) (MutualChecks, Declaration)
-> Maybe () -> Maybe (MutualChecks, Declaration)
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Maybe Fixity' -> Name -> Declaration -> Bool
couldBeFunClauseOf Maybe Fixity'
mf Name
n Declaration
d)
couldBeNiceFunClauseOf Maybe Fixity'
_ Name
_ NiceDeclaration
_ = Maybe (MutualChecks, Declaration)
forall a. Maybe a
Nothing
couldBeFunClauseOf :: Maybe Fixity' -> Name -> Declaration -> Bool
couldBeFunClauseOf :: Maybe Fixity' -> Name -> Declaration -> Bool
couldBeFunClauseOf Maybe Fixity'
mFixity Name
x (Pragma (CatchallPragma{})) = Bool
True
couldBeFunClauseOf Maybe Fixity'
mFixity Name
x (FunClause (LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_) RHS
_ WhereClause
_ Bool
_) =
Pattern -> Bool
forall a. HasEllipsis a => a -> Bool
hasEllipsis Pattern
p Bool -> Bool -> Bool
|| Maybe Fixity' -> Name -> Pattern -> Bool
couldBeCallOf Maybe Fixity'
mFixity Name
x Pattern
p
couldBeFunClauseOf Maybe Fixity'
_ Name
_ Declaration
_ = Bool
False
mkInterleavedMutual
:: KwRange
-> [NiceDeclaration]
-> Nice NiceDeclaration
mkInterleavedMutual :: KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
mkInterleavedMutual KwRange
kwr [NiceDeclaration]
ds' = do
(other, (m, checks, _)) <- StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> (InterleavedMutual, MutualChecks, Int)
-> Nice
([(Int, NiceDeclaration)], (InterleavedMutual, MutualChecks, Int))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (KwRange
-> [NiceDeclaration]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
groupByBlocks KwRange
kwr [NiceDeclaration]
ds') (InterleavedMutual
forall a. Null a => a
empty, MutualChecks
forall a. Monoid a => a
mempty, Int
0)
let idecls = [(Int, NiceDeclaration)]
other [(Int, NiceDeclaration)]
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. [a] -> [a] -> [a]
++ ((Name, InterleavedDecl) -> [(Int, NiceDeclaration)])
-> [(Name, InterleavedDecl)] -> [(Int, NiceDeclaration)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Name -> InterleavedDecl -> [(Int, NiceDeclaration)])
-> (Name, InterleavedDecl) -> [(Int, NiceDeclaration)]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> InterleavedDecl -> [(Int, NiceDeclaration)]
interleavedDecl) (InterleavedMutual -> [(Name, InterleavedDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList InterleavedMutual
m)
let decls0 = ((Int, NiceDeclaration) -> NiceDeclaration)
-> [(Int, NiceDeclaration)] -> [NiceDeclaration]
forall a b. (a -> b) -> [a] -> [b]
map (Int, NiceDeclaration) -> NiceDeclaration
forall a b. (a, b) -> b
snd ([(Int, NiceDeclaration)] -> [NiceDeclaration])
-> [(Int, NiceDeclaration)] -> [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ ((Int, NiceDeclaration) -> (Int, NiceDeclaration) -> Ordering)
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> ((Int, NiceDeclaration) -> Int)
-> (Int, NiceDeclaration)
-> (Int, NiceDeclaration)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, NiceDeclaration) -> Int
forall a b. (a, b) -> a
fst) [(Int, NiceDeclaration)]
idecls
ps <- use loneSigs
checkLoneSigs ps
let decls = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps [NiceDeclaration]
decls0
let r = KwRange -> [NiceDeclaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [NiceDeclaration]
ds'
tc <- combineTerminationChecks r (mutualTermination checks)
let cc = [CoverageCheck] -> CoverageCheck
combineCoverageChecks (MutualChecks -> [CoverageCheck]
mutualCoverage MutualChecks
checks)
let pc = [PositivityCheck] -> PositivityCheck
combinePositivityChecks (MutualChecks -> [PositivityCheck]
mutualPositivity MutualChecks
checks)
pure $ NiceMutual kwr tc cc pc decls
where
addType :: Name -> (DeclNum -> a) -> MutualChecks
-> StateT (Map Name a, MutualChecks, DeclNum) Nice ()
addType :: forall a.
Name
-> (Int -> a)
-> MutualChecks
-> StateT (Map Name a, MutualChecks, Int) Nice ()
addType Name
n Int -> a
c MutualChecks
mc = do
(m, checks, i) <- StateT
(Map Name a, MutualChecks, Int)
Nice
(Map Name a, MutualChecks, Int)
forall s (m :: * -> *). MonadState s m => m s
get
when (isJust $ Map.lookup n m) $ lift $ declarationException $ DuplicateDefinition n
put (Map.insert n (c i) m, mc <> checks, i + 1)
addFunType :: NiceDeclaration
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addFunType d :: NiceDeclaration
d@(FunSig Range
_ Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
tc CoverageCheck
cc Name
n Expr
_) = do
let checks :: MutualChecks
checks = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [TerminationCheck
tc] [CoverageCheck
cc] []
Name
-> (Int -> InterleavedDecl)
-> MutualChecks
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a.
Name
-> (Int -> a)
-> MutualChecks
-> StateT (Map Name a, MutualChecks, Int) Nice ()
addType Name
n (\ Int
i -> Int
-> NiceDeclaration
-> Maybe (Int, List1 ([Declaration], [Clause]))
-> InterleavedDecl
InterleavedFun Int
i NiceDeclaration
d Maybe (Int, List1 ([Declaration], [Clause]))
forall a. Maybe a
Nothing) MutualChecks
checks
addFunType NiceDeclaration
_ = StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__
addDataType :: NiceDeclaration
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataType d :: NiceDeclaration
d@(NiceDataSig Range
_ Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
n [LamBinding]
_ Expr
_) = do
let checks :: MutualChecks
checks = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [] [] [PositivityCheck
pc]
Name
-> (Int -> InterleavedDecl)
-> MutualChecks
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a.
Name
-> (Int -> a)
-> MutualChecks
-> StateT (Map Name a, MutualChecks, Int) Nice ()
addType Name
n (\ Int
i -> Int
-> NiceDeclaration
-> Maybe (Int, List1 [NiceDeclaration])
-> InterleavedDecl
InterleavedData Int
i NiceDeclaration
d Maybe (Int, List1 [NiceDeclaration])
forall a. Maybe a
Nothing) MutualChecks
checks
addDataType NiceDeclaration
_ = StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__
addDataConstructors :: Maybe Range
-> Maybe Name
-> [NiceConstructor]
-> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice ()
addDataConstructors :: Maybe Range
-> Maybe Name
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataConstructors Maybe Range
mr (Just Name
n) [NiceDeclaration]
ds = do
(m, checks, i) <- StateT
(InterleavedMutual, MutualChecks, Int)
Nice
(InterleavedMutual, MutualChecks, Int)
forall s (m :: * -> *). MonadState s m => m s
get
case Map.lookup n m of
Just (InterleavedData Int
i0 NiceDeclaration
sig Maybe (Int, List1 [NiceDeclaration])
cs) -> do
Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ())
-> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a b. (a -> b) -> a -> b
$ Name -> Nice ()
removeLoneSig Name
n
let ((Int, List1 [NiceDeclaration])
cs', Int
i') = case Maybe (Int, List1 [NiceDeclaration])
cs of
Maybe (Int, List1 [NiceDeclaration])
Nothing -> ((Int
i , [NiceDeclaration]
ds [NiceDeclaration] -> [[NiceDeclaration]] -> List1 [NiceDeclaration]
forall a. a -> [a] -> NonEmpty a
:| [] ), Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
Just (Int
i1, List1 [NiceDeclaration]
ds1) -> ((Int
i1, [NiceDeclaration]
ds [NiceDeclaration]
-> List1 [NiceDeclaration] -> List1 [NiceDeclaration]
forall a. a -> NonEmpty a -> NonEmpty a
<| List1 [NiceDeclaration]
ds1), Int
i)
(InterleavedMutual, MutualChecks, Int)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Name -> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (Int
-> NiceDeclaration
-> Maybe (Int, List1 [NiceDeclaration])
-> InterleavedDecl
InterleavedData Int
i0 NiceDeclaration
sig ((Int, List1 [NiceDeclaration])
-> Maybe (Int, List1 [NiceDeclaration])
forall a. a -> Maybe a
Just (Int, List1 [NiceDeclaration])
cs')) InterleavedMutual
m, MutualChecks
checks, Int
i')
Maybe InterleavedDecl
_ -> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ())
-> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ [(Name, Range)] -> DeclarationWarning'
MissingDeclarations ([(Name, Range)] -> DeclarationWarning')
-> [(Name, Range)] -> DeclarationWarning'
forall a b. (a -> b) -> a -> b
$ case Maybe Range
mr of
Just Range
r -> [(Name
n, Range
r)]
Maybe Range
Nothing -> ((NiceDeclaration -> [(Name, Range)])
-> [NiceDeclaration] -> [(Name, Range)])
-> [NiceDeclaration]
-> (NiceDeclaration -> [(Name, Range)])
-> [(Name, Range)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (NiceDeclaration -> [(Name, Range)])
-> [NiceDeclaration] -> [(Name, Range)]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap [NiceDeclaration]
ds ((NiceDeclaration -> [(Name, Range)]) -> [(Name, Range)])
-> (NiceDeclaration -> [(Name, Range)]) -> [(Name, Range)]
forall a b. (a -> b) -> a -> b
$ \case
Axiom Range
r Access
_ IsAbstract
_ IsInstance
_ ArgInfo
_ Name
n Expr
_ -> [(Name
n, Range
r)]
NiceDeclaration
_ -> [(Name, Range)]
forall a. HasCallStack => a
__IMPOSSIBLE__
addDataConstructors Maybe Range
mr Maybe Name
Nothing [] = () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a. a -> StateT (InterleavedMutual, MutualChecks, Int) Nice a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
addDataConstructors Maybe Range
mr Maybe Name
Nothing (NiceDeclaration
d : [NiceDeclaration]
ds) = do
(m, _, _) <- StateT
(InterleavedMutual, MutualChecks, Int)
Nice
(InterleavedMutual, MutualChecks, Int)
forall s (m :: * -> *). MonadState s m => m s
get
let sigs = ((Name, InterleavedDecl) -> Maybe Name)
-> [(Name, InterleavedDecl)] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (Name
n, InterleavedDecl
d) -> Name
n Name -> Maybe () -> Maybe Name
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ InterleavedDecl -> Maybe ()
isInterleavedData InterleavedDecl
d) ([(Name, InterleavedDecl)] -> [Name])
-> [(Name, InterleavedDecl)] -> [Name]
forall a b. (a -> b) -> a -> b
$ InterleavedMutual -> [(Name, InterleavedDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList InterleavedMutual
m
case isConstructor sigs d of
Right Name
n -> do
let ([NiceDeclaration]
ds0, [NiceDeclaration]
ds1) = (NiceDeclaration -> Bool)
-> [NiceDeclaration] -> ([NiceDeclaration], [NiceDeclaration])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Either (Name, [Name]) Name -> Bool
forall a b. Either a b -> Bool
isRight (Either (Name, [Name]) Name -> Bool)
-> (NiceDeclaration -> Either (Name, [Name]) Name)
-> NiceDeclaration
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> NiceDeclaration -> Either (Name, [Name]) Name
isConstructor [Name
n]) [NiceDeclaration]
ds
Maybe Range
-> Maybe Name
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataConstructors Maybe Range
forall a. Maybe a
Nothing (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n) (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: [NiceDeclaration]
ds0)
Maybe Range
-> Maybe Name
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataConstructors Maybe Range
forall a. Maybe a
Nothing Maybe Name
forall a. Maybe a
Nothing [NiceDeclaration]
ds1
Left (Name
n, [Name]
ns) -> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ())
-> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice ()
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ())
-> DeclarationException' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> Name -> [Name] -> DeclarationException'
AmbiguousConstructor (NiceDeclaration -> Range
forall a. HasRange a => a -> Range
getRange NiceDeclaration
d) Name
n [Name]
ns
addFunDef :: NiceDeclaration -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice ()
addFunDef :: NiceDeclaration
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addFunDef (FunDef Range
_ [Declaration]
ds IsAbstract
_ IsInstance
_ TerminationCheck
tc CoverageCheck
cc Name
n [Clause]
cs) = do
let check :: MutualChecks
check = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [TerminationCheck
tc] [CoverageCheck
cc] []
(m, checks, i) <- StateT
(InterleavedMutual, MutualChecks, Int)
Nice
(InterleavedMutual, MutualChecks, Int)
forall s (m :: * -> *). MonadState s m => m s
get
case Map.lookup n m of
Just (InterleavedFun Int
i0 NiceDeclaration
sig Maybe (Int, List1 ([Declaration], [Clause]))
cs0) -> do
let ((Int, List1 ([Declaration], [Clause]))
cs', Int
i') = case Maybe (Int, List1 ([Declaration], [Clause]))
cs0 of
Maybe (Int, List1 ([Declaration], [Clause]))
Nothing -> ((Int
i, ([Declaration]
ds, [Clause]
cs) ([Declaration], [Clause])
-> [([Declaration], [Clause])] -> List1 ([Declaration], [Clause])
forall a. a -> [a] -> NonEmpty a
:| [] ), Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
Just (Int
i1, List1 ([Declaration], [Clause])
cs1) -> ((Int
i1, ([Declaration]
ds, [Clause]
cs) ([Declaration], [Clause])
-> List1 ([Declaration], [Clause])
-> List1 ([Declaration], [Clause])
forall a. a -> NonEmpty a -> NonEmpty a
<| List1 ([Declaration], [Clause])
cs1), Int
i)
(InterleavedMutual, MutualChecks, Int)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Name -> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (Int
-> NiceDeclaration
-> Maybe (Int, List1 ([Declaration], [Clause]))
-> InterleavedDecl
InterleavedFun Int
i0 NiceDeclaration
sig ((Int, List1 ([Declaration], [Clause]))
-> Maybe (Int, List1 ([Declaration], [Clause]))
forall a. a -> Maybe a
Just (Int, List1 ([Declaration], [Clause]))
cs')) InterleavedMutual
m, MutualChecks
check MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
i')
Maybe InterleavedDecl
_ -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__
addFunDef NiceDeclaration
_ = StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__
addFunClauses ::
KwRange
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice [(DeclNum, NiceDeclaration)]
addFunClauses :: KwRange
-> [NiceDeclaration]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
addFunClauses KwRange
r (nd :: NiceDeclaration
nd@(NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
cc Bool
_ d :: Declaration
d@(FunClause LHS
lhs RHS
_ WhereClause
_ Bool
_)) : [NiceDeclaration]
ds) = do
(m, checks, i) <- StateT
(InterleavedMutual, MutualChecks, Int)
Nice
(InterleavedMutual, MutualChecks, Int)
forall s (m :: * -> *). MonadState s m => m s
get
let sigs = ((Name, InterleavedDecl) -> Maybe Name)
-> [(Name, InterleavedDecl)] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (Name
n, InterleavedDecl
d) -> Name
n Name -> Maybe () -> Maybe Name
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ InterleavedDecl -> Maybe ()
isInterleavedFun InterleavedDecl
d) ([(Name, InterleavedDecl)] -> [Name])
-> [(Name, InterleavedDecl)] -> [Name]
forall a b. (a -> b) -> a -> b
$ InterleavedMutual -> [(Name, InterleavedDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList InterleavedMutual
m
case [ (x, fits, rest)
| x <- sigs
, let (fits, rest) = spanJust (couldBeNiceFunClauseOf (Map.lookup x fixs) x) (nd : ds)
, not (null fits)
] of
[] -> do
let check :: MutualChecks
check = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [TerminationCheck
tc] [CoverageCheck
cc] []
(InterleavedMutual, MutualChecks, Int)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (InterleavedMutual
m, MutualChecks
check MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
((Int
i,NiceDeclaration
nd) (Int, NiceDeclaration)
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. a -> [a] -> [a]
:) ([(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)])
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange
-> [NiceDeclaration]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
groupByBlocks KwRange
r [NiceDeclaration]
ds
[(Name
n, Prefix (MutualChecks, Declaration)
fits0, [NiceDeclaration]
rest)] -> do
let ([MutualChecks]
checkss, [Declaration]
fits) = Prefix (MutualChecks, Declaration)
-> ([MutualChecks], [Declaration])
forall a b. [(a, b)] -> ([a], [b])
unzip Prefix (MutualChecks, Declaration)
fits0
ds <- Nice [Declaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice [Declaration]
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice [Declaration]
-> StateT
(InterleavedMutual, MutualChecks, Int) Nice [Declaration])
-> Nice [Declaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice [Declaration]
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
fits
cs <- lift $ mkClauses n ds False
case Map.lookup n m of
Just (InterleavedFun Int
i0 NiceDeclaration
sig Maybe (Int, List1 ([Declaration], [Clause]))
cs0) -> do
let ((Int, List1 ([Declaration], [Clause]))
cs', Int
i') = case Maybe (Int, List1 ([Declaration], [Clause]))
cs0 of
Maybe (Int, List1 ([Declaration], [Clause]))
Nothing -> ((Int
i, ([Declaration]
fits,[Clause]
cs) ([Declaration], [Clause])
-> [([Declaration], [Clause])] -> List1 ([Declaration], [Clause])
forall a. a -> [a] -> NonEmpty a
:| [] ), Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
Just (Int
i1, List1 ([Declaration], [Clause])
cs1) -> ((Int
i1, ([Declaration]
fits,[Clause]
cs) ([Declaration], [Clause])
-> List1 ([Declaration], [Clause])
-> List1 ([Declaration], [Clause])
forall a. a -> NonEmpty a -> NonEmpty a
<| List1 ([Declaration], [Clause])
cs1), Int
i)
let checks' :: MutualChecks
checks' = [MutualChecks] -> MutualChecks
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold [MutualChecks]
checkss
(InterleavedMutual, MutualChecks, Int)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Name -> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (Int
-> NiceDeclaration
-> Maybe (Int, List1 ([Declaration], [Clause]))
-> InterleavedDecl
InterleavedFun Int
i0 NiceDeclaration
sig ((Int, List1 ([Declaration], [Clause]))
-> Maybe (Int, List1 ([Declaration], [Clause]))
forall a. a -> Maybe a
Just (Int, List1 ([Declaration], [Clause]))
cs')) InterleavedMutual
m, MutualChecks
checks' MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
i')
Maybe InterleavedDecl
_ -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__
groupByBlocks r rest
(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
xf:[(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
xfs -> Nice [(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice [(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)])
-> Nice [(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice [(Int, NiceDeclaration)]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException
(DeclarationException' -> Nice [(Int, NiceDeclaration)])
-> DeclarationException' -> Nice [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ LHS -> List1 Name -> DeclarationException'
AmbiguousFunClauses LHS
lhs
(List1 Name -> DeclarationException')
-> List1 Name -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ List1 Name -> List1 Name
forall a. NonEmpty a -> NonEmpty a
List1.reverse (List1 Name -> List1 Name) -> List1 Name -> List1 Name
forall a b. (a -> b) -> a -> b
$ ((Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
-> Name)
-> NonEmpty
(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
-> List1 Name
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Name
a,Prefix (MutualChecks, Declaration)
_,[NiceDeclaration]
_) -> Name
a) (NonEmpty
(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
-> List1 Name)
-> NonEmpty
(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
-> List1 Name
forall a b. (a -> b) -> a -> b
$ (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
xf (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
-> [(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
-> NonEmpty
(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
forall a. a -> [a] -> NonEmpty a
:| [(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
xfs
addFunClauses KwRange
_ [NiceDeclaration]
_ = StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a. HasCallStack => a
__IMPOSSIBLE__
groupByBlocks ::
KwRange
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice [(DeclNum, NiceDeclaration)]
groupByBlocks :: KwRange
-> [NiceDeclaration]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
groupByBlocks KwRange
kwr [] = [(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a. a -> StateT (InterleavedMutual, MutualChecks, Int) Nice a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
groupByBlocks KwRange
kwr (NiceDeclaration
d : [NiceDeclaration]
ds) = do
let oneOff :: StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
oneOff StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
act = StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
act StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> ([(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)])
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b.
StateT (InterleavedMutual, MutualChecks, Int) Nice a
-> (a -> StateT (InterleavedMutual, MutualChecks, Int) Nice b)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ [(Int, NiceDeclaration)]
ns -> ([(Int, NiceDeclaration)]
ns [(Int, NiceDeclaration)]
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. [a] -> [a] -> [a]
++) ([(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)])
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange
-> [NiceDeclaration]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
groupByBlocks KwRange
kwr [NiceDeclaration]
ds
case NiceDeclaration
d of
NiceDataSig{} -> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
oneOff (StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)])
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b.
a
-> StateT (InterleavedMutual, MutualChecks, Int) Nice b
-> StateT (InterleavedMutual, MutualChecks, Int) Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NiceDeclaration
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataType NiceDeclaration
d
NiceDataDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n [LamBinding]
_ [NiceDeclaration]
ds -> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
oneOff (StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)])
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b.
a
-> StateT (InterleavedMutual, MutualChecks, Int) Nice b
-> StateT (InterleavedMutual, MutualChecks, Int) Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Range
-> Maybe Name
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataConstructors (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n) [NiceDeclaration]
ds
NiceLoneConstructor KwRange
_ [NiceDeclaration]
ds -> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
oneOff (StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)])
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b.
a
-> StateT (InterleavedMutual, MutualChecks, Int) Nice b
-> StateT (InterleavedMutual, MutualChecks, Int) Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Range
-> Maybe Name
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataConstructors Maybe Range
forall a. Maybe a
Nothing Maybe Name
forall a. Maybe a
Nothing [NiceDeclaration]
ds
FunSig{} -> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
oneOff (StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)])
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b.
a
-> StateT (InterleavedMutual, MutualChecks, Int) Nice b
-> StateT (InterleavedMutual, MutualChecks, Int) Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NiceDeclaration
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addFunType NiceDeclaration
d
FunDef Range
_ [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
n [Clause]
cs
| Bool -> Bool
not (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
n) -> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
oneOff (StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)])
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b.
a
-> StateT (InterleavedMutual, MutualChecks, Int) Nice b
-> StateT (InterleavedMutual, MutualChecks, Int) Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NiceDeclaration
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addFunDef NiceDeclaration
d
NiceFunClause{} -> KwRange
-> [NiceDeclaration]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
addFunClauses KwRange
kwr (NiceDeclaration
dNiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
:[NiceDeclaration]
ds)
NiceDeclaration
_ -> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
oneOff (StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)])
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
-> StateT
(InterleavedMutual, MutualChecks, Int)
Nice
[(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ do
(m, c, i) <- StateT
(InterleavedMutual, MutualChecks, Int)
Nice
(InterleavedMutual, MutualChecks, Int)
forall s (m :: * -> *). MonadState s m => m s
get
put (m, c, i + 1)
pure [(i,d)]
isConstructor :: [Name] -> NiceDeclaration -> Either (Name, [Name]) Name
isConstructor :: [Name] -> NiceDeclaration -> Either (Name, [Name]) Name
isConstructor [Name]
ns (Axiom Range
_ Access
_ IsAbstract
_ IsInstance
_ ArgInfo
_ Name
n Expr
e)
| Just Pattern
p <- Expr -> Pattern
exprToPatternWithHoles (Expr -> Pattern) -> Maybe Expr -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Expr
returnExpr Expr
e =
case [ Name
x | Name
x <- [Name]
ns
, Maybe Fixity' -> Name -> Pattern -> Bool
couldBeCallOf (Name -> Fixities -> Maybe Fixity'
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x Fixities
fixs) Name
x Pattern
p
] of
[Name
x] -> Name -> Either (Name, [Name]) Name
forall a b. b -> Either a b
Right Name
x
[Name]
xs -> (Name, [Name]) -> Either (Name, [Name]) Name
forall a b. a -> Either a b
Left (Name
n, [Name]
xs)
| Bool
otherwise = (Name, [Name]) -> Either (Name, [Name]) Name
forall a b. a -> Either a b
Left (Name
n, [])
isConstructor [Name]
_ NiceDeclaration
_ = Either (Name, [Name]) Name
forall a. HasCallStack => a
__IMPOSSIBLE__
mkOldMutual
:: KwRange
-> [NiceDeclaration]
-> Nice NiceDeclaration
mkOldMutual :: KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
mkOldMutual KwRange
kwr [NiceDeclaration]
ds' = do
let ps :: LoneSigs
ps = [(Range, Name, DataRecOrFun)] -> LoneSigs
loneSigsFromLoneNames [(Range, Name, DataRecOrFun)]
loneNames
LoneSigs -> Nice ()
checkLoneSigs LoneSigs
ps
let ds :: [NiceDeclaration]
ds = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps [NiceDeclaration]
ds'
(top, bottom, invalid) <- [NiceDeclaration]
-> (NiceDeclaration
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
-> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration])
forall (m :: * -> *) a b c d.
Applicative m =>
[a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d])
forEither3M [NiceDeclaration]
ds ((NiceDeclaration
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
-> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration]))
-> (NiceDeclaration
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
-> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration])
forall a b. (a -> b) -> a -> b
$ \ NiceDeclaration
d -> do
let top :: Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top = Either3 NiceDeclaration NiceDeclaration NiceDeclaration
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration
-> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
forall a b c. a -> Either3 a b c
In1 NiceDeclaration
d)
bottom :: Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom = Either3 NiceDeclaration NiceDeclaration NiceDeclaration
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration
-> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
forall a b c. b -> Either3 a b c
In2 NiceDeclaration
d)
invalid :: String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
s = NiceDeclaration
-> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
forall a b c. c -> Either3 a b c
In3 NiceDeclaration
d Either3 NiceDeclaration NiceDeclaration NiceDeclaration
-> Nice ()
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> String -> DeclarationWarning'
NotAllowedInMutual (NiceDeclaration -> Range
forall a. HasRange a => a -> Range
getRange NiceDeclaration
d) String
s
case NiceDeclaration
d of
Axiom{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
NiceField{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
PrimitiveFunction{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
NiceMutual{} -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"mutual blocks"
NiceModule{} -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"Module definitions"
NiceLoneConstructor{} -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"Lone constructors"
NiceModuleMacro{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
NiceOpen{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
NiceImport{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
NiceRecSig{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
NiceDataSig{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
NiceFunClause{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
FunSig{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
FunDef{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
NiceDataDef{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
NiceRecDef{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
NicePatternSyn{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
NiceGeneralize{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
NiceUnquoteDecl{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
NiceUnquoteDef{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
NiceUnquoteData{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
NiceOpaque KwRange
r [QName]
_ [NiceDeclaration]
_ ->
NiceDeclaration
-> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
forall a b c. c -> Either3 a b c
In3 NiceDeclaration
d Either3 NiceDeclaration NiceDeclaration NiceDeclaration
-> Nice Any
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do DeclarationException' -> Nice Any
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice Any)
-> DeclarationException' -> Nice Any
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationException'
OpaqueInMutual KwRange
r
NicePragma Range
r Pragma
pragma -> case Pragma
pragma of
OptionsPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
BuiltinPragma{} -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"BUILTIN pragmas"
RewritePragma{} -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"REWRITE pragmas"
ForeignPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
CompilePragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
StaticPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
InlinePragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
NotProjectionLikePragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
OverlapPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
ImpossiblePragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
EtaPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
WarningOnUsage{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
WarningOnImport{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
InjectivePragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
InjectiveForInferencePragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
DisplayPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
CatchallPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
TerminationCheckPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
NoPositivityCheckPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
PolarityPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
NoUniverseCheckPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
NoCoverageCheckPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
tc0 <- use terminationCheckPragma
let tcs = (NiceDeclaration -> TerminationCheck)
-> [NiceDeclaration] -> [TerminationCheck]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> TerminationCheck
termCheck [NiceDeclaration]
ds
let r = KwRange -> [NiceDeclaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [NiceDeclaration]
ds'
tc <- combineTerminationChecks r (tc0:tcs)
cc0 <- use coverageCheckPragma
let ccs = (NiceDeclaration -> CoverageCheck)
-> [NiceDeclaration] -> [CoverageCheck]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> CoverageCheck
covCheck [NiceDeclaration]
ds
let cc = [CoverageCheck] -> CoverageCheck
combineCoverageChecks (CoverageCheck
cc0CoverageCheck -> [CoverageCheck] -> [CoverageCheck]
forall a. a -> [a] -> [a]
:[CoverageCheck]
ccs)
pc0 <- use positivityCheckPragma
let pcs = (NiceDeclaration -> PositivityCheck)
-> [NiceDeclaration] -> [PositivityCheck]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> PositivityCheck
positivityCheckOldMutual [NiceDeclaration]
ds
let pc = [PositivityCheck] -> PositivityCheck
combinePositivityChecks (PositivityCheck
pc0PositivityCheck -> [PositivityCheck] -> [PositivityCheck]
forall a. a -> [a] -> [a]
:[PositivityCheck]
pcs)
return $ NiceMutual kwr tc cc pc $ top ++ bottom
where
sigNames :: [(Range, Name, DataRecOrFun)]
sigNames = [ (Range
r, Name
x, DataRecOrFun
k) | LoneSigDecl Range
r DataRecOrFun
k Name
x <- (NiceDeclaration -> DeclKind) -> [NiceDeclaration] -> [DeclKind]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> DeclKind
declKind [NiceDeclaration]
ds' ]
defNames :: [(Name, DataRecOrFun)]
defNames = [ (Name
x, DataRecOrFun
k) | LoneDefs DataRecOrFun
k [Name]
xs <- (NiceDeclaration -> DeclKind) -> [NiceDeclaration] -> [DeclKind]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> DeclKind
declKind [NiceDeclaration]
ds', Name
x <- [Name]
xs ]
loneNames :: [(Range, Name, DataRecOrFun)]
loneNames = [ (Range
r, Name
x, DataRecOrFun
k) | (Range
r, Name
x, DataRecOrFun
k) <- [(Range, Name, DataRecOrFun)]
sigNames, ((Name, DataRecOrFun) -> Bool) -> [(Name, DataRecOrFun)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.all ((Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Name -> Bool)
-> ((Name, DataRecOrFun) -> Name) -> (Name, DataRecOrFun) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, DataRecOrFun) -> Name
forall a b. (a, b) -> a
fst) [(Name, DataRecOrFun)]
defNames ]
termCheck :: NiceDeclaration -> TerminationCheck
termCheck :: NiceDeclaration -> TerminationCheck
termCheck (FunSig Range
_ Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
tc CoverageCheck
_ Name
_ Expr
_) = TerminationCheck
tc
termCheck (FunDef Range
_ [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
tc CoverageCheck
_ Name
_ [Clause]
_) = TerminationCheck
tc
termCheck (NiceMutual KwRange
_ TerminationCheck
tc CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
_) = TerminationCheck
tc
termCheck (NiceUnquoteDecl Range
_ Access
_ IsAbstract
_ IsInstance
_ TerminationCheck
tc CoverageCheck
_ [Name]
_ Expr
_) = TerminationCheck
tc
termCheck (NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
_ [Name]
_ Expr
_) = TerminationCheck
tc
termCheck Axiom{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceField{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck PrimitiveFunction{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceModule{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceModuleMacro{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceOpen{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceImport{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NicePragma{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceRecSig{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceDataSig{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceFunClause{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceDataDef{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceRecDef{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NicePatternSyn{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceGeneralize{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceLoneConstructor{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceUnquoteData{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
termCheck NiceOpaque{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
covCheck :: NiceDeclaration -> CoverageCheck
covCheck :: NiceDeclaration -> CoverageCheck
covCheck (FunSig Range
_ Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
_ CoverageCheck
cc Name
_ Expr
_) = CoverageCheck
cc
covCheck (FunDef Range
_ [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
cc Name
_ [Clause]
_) = CoverageCheck
cc
covCheck (NiceMutual KwRange
_ TerminationCheck
_ CoverageCheck
cc PositivityCheck
_ [NiceDeclaration]
_) = CoverageCheck
cc
covCheck (NiceUnquoteDecl Range
_ Access
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
cc [Name]
_ Expr
_) = CoverageCheck
cc
covCheck (NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
cc [Name]
_ Expr
_) = CoverageCheck
cc
covCheck Axiom{} = CoverageCheck
YesCoverageCheck
covCheck NiceField{} = CoverageCheck
YesCoverageCheck
covCheck PrimitiveFunction{} = CoverageCheck
YesCoverageCheck
covCheck NiceModule{} = CoverageCheck
YesCoverageCheck
covCheck NiceModuleMacro{} = CoverageCheck
YesCoverageCheck
covCheck NiceOpen{} = CoverageCheck
YesCoverageCheck
covCheck NiceImport{} = CoverageCheck
YesCoverageCheck
covCheck NicePragma{} = CoverageCheck
YesCoverageCheck
covCheck NiceRecSig{} = CoverageCheck
YesCoverageCheck
covCheck NiceDataSig{} = CoverageCheck
YesCoverageCheck
covCheck NiceFunClause{} = CoverageCheck
YesCoverageCheck
covCheck NiceDataDef{} = CoverageCheck
YesCoverageCheck
covCheck NiceRecDef{} = CoverageCheck
YesCoverageCheck
covCheck NicePatternSyn{} = CoverageCheck
YesCoverageCheck
covCheck NiceGeneralize{} = CoverageCheck
YesCoverageCheck
covCheck NiceLoneConstructor{} = CoverageCheck
YesCoverageCheck
covCheck NiceUnquoteData{} = CoverageCheck
YesCoverageCheck
covCheck NiceOpaque{} = CoverageCheck
YesCoverageCheck
positivityCheckOldMutual :: NiceDeclaration -> PositivityCheck
positivityCheckOldMutual :: NiceDeclaration -> PositivityCheck
positivityCheckOldMutual (NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ [LamBinding]
_ [NiceDeclaration]
_) = PositivityCheck
pc
positivityCheckOldMutual (NiceDataSig Range
_ Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_) = PositivityCheck
pc
positivityCheckOldMutual (NiceMutual KwRange
_ TerminationCheck
_ CoverageCheck
_ PositivityCheck
pc [NiceDeclaration]
_) = PositivityCheck
pc
positivityCheckOldMutual (NiceRecSig Range
_ Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_) = PositivityCheck
pc
positivityCheckOldMutual (NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ [RecordDirective]
_ [LamBinding]
_ [Declaration]
_) = PositivityCheck
pc
positivityCheckOldMutual NiceDeclaration
_ = PositivityCheck
YesPositivityCheck
abstractBlock
:: KwRange
-> [NiceDeclaration]
-> Nice [NiceDeclaration]
abstractBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
abstractBlock KwRange
r [NiceDeclaration]
ds = do
(ds', anyChange) <- ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool))
-> ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall a b. (a -> b) -> a -> b
$ UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
ds
let inherited = KwRange -> Bool
forall a. Null a => a -> Bool
null KwRange
r
if anyChange then return ds' else do
unless inherited $ declarationWarning $ UselessAbstract r
return ds
privateBlock
:: KwRange
-> Origin
-> [NiceDeclaration]
-> Nice [NiceDeclaration]
privateBlock :: KwRange -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
privateBlock KwRange
r Origin
o [NiceDeclaration]
ds = do
(ds', anyChange) <- ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool))
-> ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall a b. (a -> b) -> a -> b
$ KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
r Origin
o [NiceDeclaration]
ds
if anyChange then return ds' else do
when (o == UserWritten) $ declarationWarning $ UselessPrivate r
return ds
instanceBlock
:: KwRange
-> [NiceDeclaration]
-> Nice [NiceDeclaration]
instanceBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
instanceBlock KwRange
r [NiceDeclaration]
ds = do
let ([NiceDeclaration]
ds', Bool
anyChange) = Change [NiceDeclaration] -> ([NiceDeclaration], Bool)
forall a. Change a -> (a, Bool)
runChange (Change [NiceDeclaration] -> ([NiceDeclaration], Bool))
-> Change [NiceDeclaration] -> ([NiceDeclaration], Bool)
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> ChangeT Identity NiceDeclaration)
-> [NiceDeclaration] -> Change [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance KwRange
r) [NiceDeclaration]
ds
if Bool
anyChange then [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [NiceDeclaration]
ds' else do
HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
UselessInstance KwRange
r
[NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [NiceDeclaration]
ds
mkInstance
:: KwRange
-> Updater NiceDeclaration
mkInstance :: KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance KwRange
r0 = \case
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e -> (\ IsInstance
i -> Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Updater IsInstance
setInstance KwRange
r0 IsInstance
i
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e -> (\ IsInstance
i -> Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Updater IsInstance
setInstance KwRange
r0 IsInstance
i
NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e -> (\ IsInstance
i -> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Updater IsInstance
setInstance KwRange
r0 IsInstance
i
NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds -> KwRange
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc ([NiceDeclaration] -> NiceDeclaration)
-> Change [NiceDeclaration] -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> ChangeT Identity NiceDeclaration)
-> [NiceDeclaration] -> Change [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance KwRange
r0) [NiceDeclaration]
ds
NiceLoneConstructor KwRange
r [NiceDeclaration]
ds -> KwRange -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor KwRange
r ([NiceDeclaration] -> NiceDeclaration)
-> Change [NiceDeclaration] -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> ChangeT Identity NiceDeclaration)
-> [NiceDeclaration] -> Change [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance KwRange
r0) [NiceDeclaration]
ds
d :: NiceDeclaration
d@NiceFunClause{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x [Clause]
cs -> (\ IsInstance
i -> Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> [Clause]
-> NiceDeclaration
FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x [Clause]
cs) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Updater IsInstance
setInstance KwRange
r0 IsInstance
i
NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
i -> (\ [NiceDeclaration]
i -> KwRange -> [QName] -> [NiceDeclaration] -> NiceDeclaration
NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
i) ([NiceDeclaration] -> NiceDeclaration)
-> Change [NiceDeclaration] -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> ChangeT Identity NiceDeclaration)
-> [NiceDeclaration] -> Change [NiceDeclaration]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance KwRange
r0) [NiceDeclaration]
i
d :: NiceDeclaration
d@NiceField{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@PrimitiveFunction{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceUnquoteDef{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceRecSig{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceDataSig{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceModuleMacro{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceModule{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NicePragma{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceOpen{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceImport{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceDataDef{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceRecDef{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NicePatternSyn{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceGeneralize{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceUnquoteData{} -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
setInstance
:: KwRange
-> Updater IsInstance
setInstance :: KwRange -> Updater IsInstance
setInstance KwRange
r0 = \case
i :: IsInstance
i@InstanceDef{} -> Updater IsInstance
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return IsInstance
i
IsInstance
_ -> Updater IsInstance
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty Updater IsInstance -> Updater IsInstance
forall a b. (a -> b) -> a -> b
$ KwRange -> IsInstance
InstanceDef KwRange
r0
macroBlock
:: KwRange
-> [NiceDeclaration]
-> Nice [NiceDeclaration]
macroBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
macroBlock KwRange
r [NiceDeclaration]
ds = do
(ds', anyChange) <- ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool))
-> ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall a b. (a -> b) -> a -> b
$ UpdaterT Nice [NiceDeclaration]
forall a. MakeMacro a => UpdaterT Nice a
mkMacro [NiceDeclaration]
ds
if anyChange then return ds' else do
declarationWarning $ UselessMacro r
return ds
class MakeMacro a where
mkMacro :: UpdaterT Nice a
default mkMacro :: (Traversable f, MakeMacro a', a ~ f a') => UpdaterT Nice a
mkMacro = (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse a' -> ChangeT Nice a'
forall a. MakeMacro a => UpdaterT Nice a
mkMacro
instance MakeMacro a => MakeMacro [a]
instance MakeMacro NiceDeclaration where
mkMacro :: UpdaterT Nice NiceDeclaration
mkMacro = \case
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
_ ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
MacroDef ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e
d :: NiceDeclaration
d@FunDef{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
NiceDeclaration
d -> Nice NiceDeclaration -> ChangeT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice NiceDeclaration -> ChangeT Nice NiceDeclaration)
-> Nice NiceDeclaration -> ChangeT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice NiceDeclaration
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice NiceDeclaration)
-> DeclarationException' -> Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ NiceDeclaration -> DeclarationException'
BadMacroDef NiceDeclaration
d
class MakeAbstract a where
mkAbstract :: UpdaterT Nice a
default mkAbstract :: (Traversable f, MakeAbstract a', a ~ f a') => UpdaterT Nice a
mkAbstract = (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse a' -> ChangeT Nice a'
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract
instance MakeAbstract a => MakeAbstract [a]
instance MakeAbstract IsAbstract where
mkAbstract :: UpdaterT Nice IsAbstract
mkAbstract = \case
a :: IsAbstract
a@IsAbstract
AbstractDef -> UpdaterT Nice IsAbstract
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return IsAbstract
a
IsAbstract
ConcreteDef -> UpdaterT Nice IsAbstract
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice IsAbstract -> UpdaterT Nice IsAbstract
forall a b. (a -> b) -> a -> b
$ IsAbstract
AbstractDef
instance MakeAbstract NiceDeclaration where
mkAbstract :: UpdaterT Nice NiceDeclaration
mkAbstract = \case
NiceMutual KwRange
r TerminationCheck
termCheck CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds -> KwRange
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual KwRange
r TerminationCheck
termCheck CoverageCheck
cc PositivityCheck
pc ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
ds
NiceLoneConstructor KwRange
r [NiceDeclaration]
ds -> KwRange -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor KwRange
r ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
ds
FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x [Clause]
cs -> (\ IsAbstract
a -> Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> [Clause]
-> NiceDeclaration
FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x) (IsAbstract -> [Clause] -> NiceDeclaration)
-> ChangeT Nice IsAbstract
-> ChangeT Nice ([Clause] -> NiceDeclaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a ChangeT Nice ([Clause] -> NiceDeclaration)
-> ChangeT Nice [Clause] -> ChangeT Nice NiceDeclaration
forall a b.
ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UpdaterT Nice [Clause]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [Clause]
cs
NiceDataDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ps [NiceDeclaration]
cs -> (\ IsAbstract
a -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> [NiceDeclaration]
-> NiceDeclaration
NiceDataDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ps) (IsAbstract -> [NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice IsAbstract
-> ChangeT Nice ([NiceDeclaration] -> NiceDeclaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a ChangeT Nice ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall a b.
ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
cs
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir [LamBinding]
ps [Declaration]
cs -> (\ IsAbstract
a -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> NiceDeclaration
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir [LamBinding]
ps [Declaration]
cs) (IsAbstract -> NiceDeclaration)
-> ChangeT Nice IsAbstract -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a
NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Bool
catchall Declaration
d -> (\ IsAbstract
a -> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Bool
-> Declaration
-> NiceDeclaration
NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Bool
catchall Declaration
d) (IsAbstract -> NiceDeclaration)
-> ChangeT Nice IsAbstract -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
p IsAbstract
AbstractDef IsInstance
i ArgInfo
rel Name
x Expr
e
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig Range
r Access
p IsAbstract
AbstractDef IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e
NiceRecSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig Range
r Erased
er Access
p IsAbstract
AbstractDef PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t
NiceDataSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig Range
r Erased
er Access
p IsAbstract
AbstractDef PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t
NiceField Range
r Access
p IsAbstract
_ IsInstance
i TacticAttribute
tac Name
x Arg Expr
e -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceDeclaration
NiceField Range
r Access
p IsAbstract
AbstractDef IsInstance
i TacticAttribute
tac Name
x Arg Expr
e
PrimitiveFunction Range
r Access
p IsAbstract
_ Name
x Arg Expr
e -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
PrimitiveFunction Range
r Access
p IsAbstract
AbstractDef Name
x Arg Expr
e
NiceUnquoteDecl Range
r Access
p IsAbstract
_ IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e -> ChangeT Nice ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
p IsAbstract
AbstractDef IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e
NiceUnquoteDef Range
r Access
p IsAbstract
_ TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e -> ChangeT Nice ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDef Range
r Access
p IsAbstract
AbstractDef TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e
NiceUnquoteData Range
r Access
p IsAbstract
_ PositivityCheck
tc UniverseCheck
cc Name
x [Name]
xs Expr
e -> ChangeT Nice ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteData Range
r Access
p IsAbstract
AbstractDef PositivityCheck
tc UniverseCheck
cc Name
x [Name]
xs Expr
e
d :: NiceDeclaration
d@NiceModule{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceModuleMacro{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NicePragma{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@(NiceOpen Range
_ QName
_ ImportDirective
directives) -> do
Maybe KwRange -> (KwRange -> ChangeT Nice ()) -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (ImportDirective -> Maybe KwRange
forall n m. ImportDirective' n m -> Maybe KwRange
publicOpen ImportDirective
directives) ((KwRange -> ChangeT Nice ()) -> ChangeT Nice ())
-> (KwRange -> ChangeT Nice ()) -> ChangeT Nice ()
forall a b. (a -> b) -> a -> b
$ Nice () -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> ChangeT Nice ())
-> (KwRange -> Nice ()) -> KwRange -> ChangeT Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ())
-> (KwRange -> DeclarationWarning') -> KwRange -> Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KwRange -> DeclarationWarning'
OpenPublicAbstract
UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceImport{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NicePatternSyn{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceGeneralize{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
ds -> KwRange -> [QName] -> [NiceDeclaration] -> NiceDeclaration
NiceOpaque KwRange
r [QName]
ns ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
ds
instance MakeAbstract Clause where
mkAbstract :: UpdaterT Nice Clause
mkAbstract (Clause Name
x Bool
catchall LHS
lhs RHS
rhs WhereClause
wh [Clause]
with) = do
Name -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
Clause Name
x Bool
catchall LHS
lhs RHS
rhs (WhereClause -> [Clause] -> Clause)
-> ChangeT Nice WhereClause -> ChangeT Nice ([Clause] -> Clause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice WhereClause
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract WhereClause
wh ChangeT Nice ([Clause] -> Clause)
-> ChangeT Nice [Clause] -> ChangeT Nice Clause
forall a b.
ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UpdaterT Nice [Clause]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [Clause]
with
instance MakeAbstract WhereClause where
mkAbstract :: UpdaterT Nice WhereClause
mkAbstract WhereClause
NoWhere = UpdaterT Nice WhereClause
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
forall a b. (a -> b) -> a -> b
$ WhereClause
forall decls. WhereClause' decls
NoWhere
mkAbstract (AnyWhere Range
r [Declaration]
ds) = UpdaterT Nice WhereClause
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
forall a b. (a -> b) -> a -> b
$ Range -> [Declaration] -> WhereClause
forall decls. Range -> decls -> WhereClause' decls
AnyWhere Range
r
[KwRange -> [Declaration] -> Declaration
Abstract KwRange
forall a. Null a => a
empty [Declaration]
ds]
mkAbstract (SomeWhere Range
r Erased
e Name
m Access
a [Declaration]
ds) = UpdaterT Nice WhereClause
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
forall a b. (a -> b) -> a -> b
$ Range -> Erased -> Name -> Access -> [Declaration] -> WhereClause
forall decls.
Range -> Erased -> Name -> Access -> decls -> WhereClause' decls
SomeWhere Range
r Erased
e Name
m Access
a
[KwRange -> [Declaration] -> Declaration
Abstract KwRange
forall a. Null a => a
empty [Declaration]
ds]
class MakePrivate a where
mkPrivate :: KwRange -> Origin -> UpdaterT Nice a
default mkPrivate :: (Traversable f, MakePrivate a', a ~ f a') => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o = (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a'))
-> (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
forall a b. (a -> b) -> a -> b
$ KwRange -> Origin -> a' -> ChangeT Nice a'
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o
instance MakePrivate a => MakePrivate [a]
instance MakePrivate Access where
mkPrivate :: KwRange -> Origin -> UpdaterT Nice Access
mkPrivate KwRange
kwr Origin
o = \case
p :: Access
p@PrivateAccess{} -> UpdaterT Nice Access
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return Access
p
Access
_ -> UpdaterT Nice Access
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice Access -> UpdaterT Nice Access
forall a b. (a -> b) -> a -> b
$ KwRange -> Origin -> Access
PrivateAccess KwRange
kwr Origin
o
instance MakePrivate NiceDeclaration where
mkPrivate :: KwRange -> Origin -> UpdaterT Nice NiceDeclaration
mkPrivate KwRange
kwr Origin
o = \case
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
NiceField Range
r Access
p IsAbstract
a IsInstance
i TacticAttribute
tac Name
x Arg Expr
e -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceDeclaration
NiceField Range
r Access
p IsAbstract
a IsInstance
i TacticAttribute
tac Name
x Arg Expr
e) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
PrimitiveFunction Range
r Access
p IsAbstract
a Name
x Arg Expr
e -> (\ Access
p -> Range
-> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
PrimitiveFunction Range
r Access
p IsAbstract
a Name
x Arg Expr
e) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds -> (\ [NiceDeclaration]
ds-> KwRange
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds) ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [NiceDeclaration]
ds
NiceLoneConstructor KwRange
r [NiceDeclaration]
ds -> KwRange -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor KwRange
r ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [NiceDeclaration]
ds
NiceModule Range
r Access
p IsAbstract
a Erased
e QName
x Telescope
tel [Declaration]
ds -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> Erased
-> QName
-> Telescope
-> [Declaration]
-> NiceDeclaration
NiceModule Range
r Access
p IsAbstract
a Erased
e QName
x Telescope
tel [Declaration]
ds) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
NiceModuleMacro Range
r Access
p Erased
e Name
x ModuleApplication
ma OpenShortHand
op ImportDirective
is -> (\ Access
p -> Range
-> Access
-> Erased
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> NiceDeclaration
NiceModuleMacro Range
r Access
p Erased
e Name
x ModuleApplication
ma OpenShortHand
op ImportDirective
is) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
NiceRecSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t -> (\ Access
p -> Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
NiceDataSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t -> (\ Access
p -> Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Bool
catchall Declaration
d -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Bool
-> Declaration
-> NiceDeclaration
NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Bool
catchall Declaration
d) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
NiceUnquoteDef Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDef Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
NicePatternSyn Range
r Access
p Name
x [WithHiding Name]
xs Pattern
p' -> (\ Access
p -> Range
-> Access
-> Name
-> [WithHiding Name]
-> Pattern
-> NiceDeclaration
NicePatternSyn Range
r Access
p Name
x [WithHiding Name]
xs Pattern
p') (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
NiceGeneralize Range
r Access
p ArgInfo
i TacticAttribute
tac Name
x Expr
t -> (\ Access
p -> Range
-> Access
-> ArgInfo
-> TacticAttribute
-> Name
-> Expr
-> NiceDeclaration
NiceGeneralize Range
r Access
p ArgInfo
i TacticAttribute
tac Name
x Expr
t) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
ds -> (\ [NiceDeclaration]
p -> KwRange -> [QName] -> [NiceDeclaration] -> NiceDeclaration
NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
p) ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [NiceDeclaration]
ds
d :: NiceDeclaration
d@NicePragma{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@(NiceOpen Range
_ QName
_ ImportDirective
directives) -> do
Maybe KwRange -> (KwRange -> ChangeT Nice ()) -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (ImportDirective -> Maybe KwRange
forall n m. ImportDirective' n m -> Maybe KwRange
publicOpen ImportDirective
directives) ((KwRange -> ChangeT Nice ()) -> ChangeT Nice ())
-> (KwRange -> ChangeT Nice ()) -> ChangeT Nice ()
forall a b. (a -> b) -> a -> b
$ Nice () -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> ChangeT Nice ())
-> (KwRange -> Nice ()) -> KwRange -> ChangeT Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ())
-> (KwRange -> DeclarationWarning') -> KwRange -> Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KwRange -> DeclarationWarning'
OpenPublicPrivate
UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceImport{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x [Clause]
cls -> Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> [Clause]
-> NiceDeclaration
FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x ([Clause] -> NiceDeclaration)
-> ChangeT Nice [Clause] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice [Clause]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [Clause]
cls
d :: NiceDeclaration
d@NiceDataDef{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceRecDef{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
d :: NiceDeclaration
d@NiceUnquoteData{} -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
instance MakePrivate Clause where
mkPrivate :: KwRange -> Origin -> UpdaterT Nice Clause
mkPrivate KwRange
kwr Origin
o (Clause Name
x Bool
catchall LHS
lhs RHS
rhs WhereClause
wh [Clause]
with) = do
Name -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
Clause Name
x Bool
catchall LHS
lhs RHS
rhs (WhereClause -> [Clause] -> Clause)
-> ChangeT Nice WhereClause -> ChangeT Nice ([Clause] -> Clause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice WhereClause
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o WhereClause
wh ChangeT Nice ([Clause] -> Clause)
-> ChangeT Nice [Clause] -> ChangeT Nice Clause
forall a b.
ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> KwRange -> Origin -> UpdaterT Nice [Clause]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [Clause]
with
instance MakePrivate WhereClause where
mkPrivate :: KwRange -> Origin -> UpdaterT Nice WhereClause
mkPrivate KwRange
kwr Origin
o = \case
d :: WhereClause
d@WhereClause
NoWhere -> UpdaterT Nice WhereClause
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return WhereClause
d
d :: WhereClause
d@AnyWhere{} -> UpdaterT Nice WhereClause
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return WhereClause
d
SomeWhere Range
r Erased
e Name
m Access
a [Declaration]
ds ->
KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
a ChangeT Nice Access
-> (Access -> WhereClause) -> ChangeT Nice WhereClause
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Access
a' -> Range -> Erased -> Name -> Access -> [Declaration] -> WhereClause
forall decls.
Range -> Erased -> Name -> Access -> decls -> WhereClause' decls
SomeWhere Range
r Erased
e Name
m Access
a' [Declaration]
ds
notSoNiceDeclarations :: NiceDeclaration -> [Declaration]
notSoNiceDeclarations :: NiceDeclaration -> [Declaration]
notSoNiceDeclarations = \case
Axiom Range
_ Access
_ IsAbstract
_ IsInstance
i ArgInfo
rel Name
x Expr
e -> IsInstance -> [Declaration] -> [Declaration]
inst IsInstance
i [ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig ArgInfo
rel TacticAttribute
forall a. Null a => a
empty Name
x Expr
e]
NiceField Range
_ Access
_ IsAbstract
_ IsInstance
i TacticAttribute
tac Name
x Arg Expr
argt -> [IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration
FieldSig IsInstance
i TacticAttribute
tac Name
x Arg Expr
argt]
PrimitiveFunction Range
_ Access
_ IsAbstract
_ Name
x Arg Expr
e -> [KwRange -> [Declaration] -> Declaration
Primitive KwRange
forall a. Null a => a
empty [ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig (Arg Expr -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg Expr
e) TacticAttribute
forall a. Null a => a
empty Name
x (Arg Expr -> Expr
forall e. Arg e -> e
unArg Arg Expr
e)]]
NiceMutual KwRange
r TerminationCheck
_ CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
ds -> [KwRange -> [Declaration] -> Declaration
Mutual KwRange
r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> [Declaration])
-> [NiceDeclaration] -> [Declaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
ds]
NiceLoneConstructor KwRange
r [NiceDeclaration]
ds -> [KwRange -> [Declaration] -> Declaration
LoneConstructor KwRange
r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> [Declaration])
-> [NiceDeclaration] -> [Declaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
ds]
NiceModule Range
r Access
_ IsAbstract
_ Erased
e QName
x Telescope
tel [Declaration]
ds -> [Range
-> Erased -> QName -> Telescope -> [Declaration] -> Declaration
Module Range
r Erased
e QName
x Telescope
tel [Declaration]
ds]
NiceModuleMacro Range
r Access
_ Erased
e Name
x ModuleApplication
ma OpenShortHand
o ImportDirective
dir
-> [Range
-> Erased
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> Declaration
ModuleMacro Range
r Erased
e Name
x ModuleApplication
ma OpenShortHand
o ImportDirective
dir]
NiceOpen Range
r QName
x ImportDirective
dir -> [Range -> QName -> ImportDirective -> Declaration
Open Range
r QName
x ImportDirective
dir]
NiceImport Range
r QName
x Maybe AsName
as OpenShortHand
o ImportDirective
dir -> [Range
-> QName
-> Maybe AsName
-> OpenShortHand
-> ImportDirective
-> Declaration
Import Range
r QName
x Maybe AsName
as OpenShortHand
o ImportDirective
dir]
NicePragma Range
_ Pragma
p -> [Pragma -> Declaration
Pragma Pragma
p]
NiceRecSig Range
r Erased
er Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
bs Expr
e -> [Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
RecordSig Range
r Erased
er Name
x [LamBinding]
bs Expr
e]
NiceDataSig Range
r Erased
er Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
bs Expr
e -> [Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
DataSig Range
r Erased
er Name
x [LamBinding]
bs Expr
e]
NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ Bool
_ Declaration
d -> [Declaration
d]
FunSig Range
_ Access
_ IsAbstract
_ IsInstance
i IsMacro
_ ArgInfo
rel TerminationCheck
_ CoverageCheck
_ Name
x Expr
e -> IsInstance -> [Declaration] -> [Declaration]
inst IsInstance
i [ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig ArgInfo
rel TacticAttribute
forall a. Null a => a
empty Name
x Expr
e]
FunDef Range
_ [Declaration]
ds IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ [Clause]
_ -> [Declaration]
ds
NiceDataDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
bs [NiceDeclaration]
cs -> [Range -> Name -> [LamBinding] -> [Declaration] -> Declaration
DataDef Range
r Name
x [LamBinding]
bs ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> [Declaration])
-> [NiceDeclaration] -> [Declaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
cs]
NiceRecDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [RecordDirective]
dir [LamBinding]
bs [Declaration]
ds -> [Range
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> Declaration
RecordDef Range
r Name
x [RecordDirective]
dir [LamBinding]
bs [Declaration]
ds]
NicePatternSyn Range
r Access
_ Name
n [WithHiding Name]
as Pattern
p -> [Range -> Name -> [WithHiding Name] -> Pattern -> Declaration
PatternSyn Range
r Name
n [WithHiding Name]
as Pattern
p]
NiceGeneralize Range
_ Access
_ ArgInfo
i TacticAttribute
tac Name
n Expr
e -> [KwRange -> [Declaration] -> Declaration
Generalize KwRange
forall a. Null a => a
empty [ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig ArgInfo
i TacticAttribute
tac Name
n Expr
e]]
NiceUnquoteDecl Range
r Access
_ IsAbstract
_ IsInstance
i TerminationCheck
_ CoverageCheck
_ [Name]
x Expr
e -> IsInstance -> [Declaration] -> [Declaration]
inst IsInstance
i [Range -> [Name] -> Expr -> Declaration
UnquoteDecl Range
r [Name]
x Expr
e]
NiceUnquoteDef Range
r Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ [Name]
x Expr
e -> [Range -> [Name] -> Expr -> Declaration
UnquoteDef Range
r [Name]
x Expr
e]
NiceUnquoteData Range
r Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [Name]
xs Expr
e -> [Range -> Name -> [Name] -> Expr -> Declaration
UnquoteData Range
r Name
x [Name]
xs Expr
e]
NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
ds -> [KwRange -> [Declaration] -> Declaration
Opaque KwRange
r (KwRange -> [QName] -> Declaration
Unfolding KwRange
r [QName]
nsDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:(NiceDeclaration -> [Declaration])
-> [NiceDeclaration] -> [Declaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
ds)]
where
inst :: IsInstance -> [Declaration] -> [Declaration]
inst (InstanceDef KwRange
r) [Declaration]
ds = [KwRange -> [Declaration] -> Declaration
InstanceB KwRange
r [Declaration]
ds]
inst IsInstance
NotInstanceDef [Declaration]
ds = [Declaration]
ds
niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract
niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract
niceHasAbstract = \case
Axiom{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
NiceField Range
_ Access
_ IsAbstract
a IsInstance
_ TacticAttribute
_ Name
_ Arg Expr
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
PrimitiveFunction Range
_ Access
_ IsAbstract
a Name
_ Arg Expr
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
NiceMutual{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
NiceLoneConstructor{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
NiceModule Range
_ Access
_ IsAbstract
a Erased
_ QName
_ Telescope
_ [Declaration]
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
NiceModuleMacro{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
NiceOpen{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
NiceImport{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
NicePragma{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
NiceRecSig{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
NiceDataSig{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
NiceFunClause Range
_ Access
_ IsAbstract
a TerminationCheck
_ CoverageCheck
_ Bool
_ Declaration
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
FunSig{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
FunDef Range
_ [Declaration]
_ IsAbstract
a IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ [Clause]
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
NiceDataDef Range
_ Origin
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ [NiceDeclaration]
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
NiceRecDef Range
_ Origin
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Name
_ [RecordDirective]
_ [LamBinding]
_ [Declaration]
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
NicePatternSyn{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
NiceGeneralize{} -> Maybe IsAbstract
forall a. Maybe a
Nothing
NiceUnquoteDecl Range
_ Access
_ IsAbstract
a IsInstance
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
NiceUnquoteDef Range
_ Access
_ IsAbstract
a TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
NiceUnquoteData Range
_ Access
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Name
_ [Name]
_ Expr
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
NiceOpaque{} -> Maybe IsAbstract
forall a. Maybe a
Nothing