module Agda.Syntax.Concrete.Definitions.Types where
import Control.DeepSeq
import Data.Data
import Data.Map (Map)
import Data.Semigroup ( Semigroup(..) )
import GHC.Generics (Generic)
import Agda.Syntax.Position
import Agda.Syntax.Common hiding (TerminationCheck())
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Concrete.Pretty
import Agda.Utils.Pretty
import Agda.Utils.Impossible
data NiceDeclaration
= Axiom Range Access IsAbstract IsInstance ArgInfo Name Expr
| NiceField Range Access IsAbstract IsInstance TacticAttribute Name (Arg Expr)
| PrimitiveFunction Range Access IsAbstract Name (Arg Expr)
| NiceMutual Range TerminationCheck CoverageCheck PositivityCheck [NiceDeclaration]
| NiceModule Range Access IsAbstract QName Telescope [Declaration]
| NiceModuleMacro Range Access Name ModuleApplication OpenShortHand ImportDirective
| NiceOpen Range QName ImportDirective
| NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
| NicePragma Range Pragma
| NiceRecSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
| NiceDataSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
| NiceFunClause Range Access IsAbstract TerminationCheck CoverageCheck Catchall Declaration
| FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck CoverageCheck Name Expr
| FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck CoverageCheck Name [Clause]
| NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]
| NiceLoneConstructor Range [NiceConstructor]
| NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name RecordDirectives [LamBinding] [Declaration]
| NicePatternSyn Range Access Name [Arg Name] Pattern
| NiceGeneralize Range Access ArgInfo TacticAttribute Name Expr
| NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck CoverageCheck [Name] Expr
| NiceUnquoteDef Range Access IsAbstract TerminationCheck CoverageCheck [Name] Expr
deriving (Typeable NiceDeclaration
DataType
Constr
Typeable NiceDeclaration
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NiceDeclaration)
-> (NiceDeclaration -> Constr)
-> (NiceDeclaration -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NiceDeclaration))
-> ((forall b. Data b => b -> b)
-> NiceDeclaration -> NiceDeclaration)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r)
-> (forall u.
(forall d. Data d => d -> u) -> NiceDeclaration -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration)
-> Data NiceDeclaration
NiceDeclaration -> DataType
NiceDeclaration -> Constr
(forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NiceDeclaration
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u
forall u. (forall d. Data d => d -> u) -> NiceDeclaration -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NiceDeclaration
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NiceDeclaration)
$cNiceUnquoteDef :: Constr
$cNiceUnquoteDecl :: Constr
$cNiceGeneralize :: Constr
$cNicePatternSyn :: Constr
$cNiceRecDef :: Constr
$cNiceLoneConstructor :: Constr
$cNiceDataDef :: Constr
$cFunDef :: Constr
$cFunSig :: Constr
$cNiceFunClause :: Constr
$cNiceDataSig :: Constr
$cNiceRecSig :: Constr
$cNicePragma :: Constr
$cNiceImport :: Constr
$cNiceOpen :: Constr
$cNiceModuleMacro :: Constr
$cNiceModule :: Constr
$cNiceMutual :: Constr
$cPrimitiveFunction :: Constr
$cNiceField :: Constr
$cAxiom :: Constr
$tNiceDeclaration :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
gmapMp :: (forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
gmapM :: (forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
gmapQi :: Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u
gmapQ :: (forall d. Data d => d -> u) -> NiceDeclaration -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> NiceDeclaration -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
gmapT :: (forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration
$cgmapT :: (forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NiceDeclaration)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NiceDeclaration)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration)
dataTypeOf :: NiceDeclaration -> DataType
$cdataTypeOf :: NiceDeclaration -> DataType
toConstr :: NiceDeclaration -> Constr
$ctoConstr :: NiceDeclaration -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NiceDeclaration
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NiceDeclaration
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration
$cp1Data :: Typeable NiceDeclaration
Data, Int -> NiceDeclaration -> ShowS
[NiceDeclaration] -> ShowS
NiceDeclaration -> String
(Int -> NiceDeclaration -> ShowS)
-> (NiceDeclaration -> String)
-> ([NiceDeclaration] -> ShowS)
-> Show NiceDeclaration
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NiceDeclaration] -> ShowS
$cshowList :: [NiceDeclaration] -> ShowS
show :: NiceDeclaration -> String
$cshow :: NiceDeclaration -> String
showsPrec :: Int -> NiceDeclaration -> ShowS
$cshowsPrec :: Int -> NiceDeclaration -> ShowS
Show, (forall x. NiceDeclaration -> Rep NiceDeclaration x)
-> (forall x. Rep NiceDeclaration x -> NiceDeclaration)
-> Generic NiceDeclaration
forall x. Rep NiceDeclaration x -> NiceDeclaration
forall x. NiceDeclaration -> Rep NiceDeclaration x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NiceDeclaration x -> NiceDeclaration
$cfrom :: forall x. NiceDeclaration -> Rep NiceDeclaration x
Generic)
instance NFData NiceDeclaration
type TerminationCheck = Common.TerminationCheck Measure
type Measure = Name
type Catchall = Bool
type NiceConstructor = NiceTypeSignature
type NiceTypeSignature = NiceDeclaration
data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
deriving (Typeable Clause
DataType
Constr
Typeable Clause
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause)
-> (Clause -> Constr)
-> (Clause -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Clause))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause))
-> ((forall b. Data b => b -> b) -> Clause -> Clause)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Clause -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Clause -> r)
-> (forall u. (forall d. Data d => d -> u) -> Clause -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause)
-> Data Clause
Clause -> DataType
Clause -> Constr
(forall b. Data b => b -> b) -> Clause -> Clause
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u
forall u. (forall d. Data d => d -> u) -> Clause -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Clause)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
$cClause :: Constr
$tClause :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Clause -> m Clause
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
gmapMp :: (forall d. Data d => d -> m d) -> Clause -> m Clause
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
gmapM :: (forall d. Data d => d -> m d) -> Clause -> m Clause
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u
gmapQ :: (forall d. Data d => d -> u) -> Clause -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Clause -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause
$cgmapT :: (forall b. Data b => b -> b) -> Clause -> Clause
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Clause)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Clause)
dataTypeOf :: Clause -> DataType
$cdataTypeOf :: Clause -> DataType
toConstr :: Clause -> Constr
$ctoConstr :: Clause -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause
$cp1Data :: Typeable Clause
Data, Int -> Clause -> ShowS
[Clause] -> ShowS
Clause -> String
(Int -> Clause -> ShowS)
-> (Clause -> String) -> ([Clause] -> ShowS) -> Show Clause
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Clause] -> ShowS
$cshowList :: [Clause] -> ShowS
show :: Clause -> String
$cshow :: Clause -> String
showsPrec :: Int -> Clause -> ShowS
$cshowsPrec :: Int -> Clause -> ShowS
Show, (forall x. Clause -> Rep Clause x)
-> (forall x. Rep Clause x -> Clause) -> Generic Clause
forall x. Rep Clause x -> Clause
forall x. Clause -> Rep Clause x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Clause x -> Clause
$cfrom :: forall x. Clause -> Rep Clause x
Generic)
instance NFData Clause
data MutualChecks = MutualChecks
{ MutualChecks -> [TerminationCheck]
mutualTermination :: [TerminationCheck]
, MutualChecks -> [CoverageCheck]
mutualCoverage :: [CoverageCheck]
, MutualChecks -> [PositivityCheck]
mutualPositivity :: [PositivityCheck]
}
instance Semigroup MutualChecks where
MutualChecks [TerminationCheck]
a [CoverageCheck]
b [PositivityCheck]
c <> :: MutualChecks -> MutualChecks -> MutualChecks
<> MutualChecks [TerminationCheck]
a' [CoverageCheck]
b' [PositivityCheck]
c'
= [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks ([TerminationCheck]
a [TerminationCheck] -> [TerminationCheck] -> [TerminationCheck]
forall a. Semigroup a => a -> a -> a
<> [TerminationCheck]
a') ([CoverageCheck]
b [CoverageCheck] -> [CoverageCheck] -> [CoverageCheck]
forall a. Semigroup a => a -> a -> a
<> [CoverageCheck]
b') ([PositivityCheck]
c [PositivityCheck] -> [PositivityCheck] -> [PositivityCheck]
forall a. Semigroup a => a -> a -> a
<> [PositivityCheck]
c')
instance Monoid MutualChecks where
mempty :: MutualChecks
mempty = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [] [] []
mappend :: MutualChecks -> MutualChecks -> MutualChecks
mappend = MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
(<>)
data InferredMutual = InferredMutual
{ InferredMutual -> MutualChecks
inferredChecks :: MutualChecks
, InferredMutual -> [NiceDeclaration]
inferredBlock :: [NiceDeclaration]
, InferredMutual -> [NiceDeclaration]
inferredLeftovers :: [NiceDeclaration]
}
extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock NiceDeclaration
d (InferredMutual MutualChecks
cs [NiceDeclaration]
ds [NiceDeclaration]
left) = MutualChecks
-> [NiceDeclaration] -> [NiceDeclaration] -> InferredMutual
InferredMutual MutualChecks
cs (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: [NiceDeclaration]
ds) [NiceDeclaration]
left
type InterleavedMutual = Map Name InterleavedDecl
data InterleavedDecl
= InterleavedData
{ InterleavedDecl -> (Int, NiceDeclaration)
infixDataSig :: (Int, NiceDeclaration)
, InterleavedDecl -> Maybe (Int, [[NiceDeclaration]])
infixDataCons :: Maybe (Int, [[NiceConstructor]])
}
| InterleavedFun
{ InterleavedDecl -> (Int, NiceDeclaration)
infixFunSig :: (Int, NiceDeclaration)
, InterleavedDecl -> Maybe (Int, [([Declaration], [Clause])])
infixFunClauses :: Maybe (Int, [([Declaration],[Clause])])
}
isInterleavedFun :: InterleavedDecl -> Maybe ()
isInterleavedFun :: InterleavedDecl -> Maybe ()
isInterleavedFun InterleavedFun{} = () -> Maybe ()
forall a. a -> Maybe a
Just ()
isInterleavedFun InterleavedDecl
_ = Maybe ()
forall a. Maybe a
Nothing
isInterleavedData :: InterleavedDecl -> Maybe ()
isInterleavedData :: InterleavedDecl -> Maybe ()
isInterleavedData InterleavedData{} = () -> Maybe ()
forall a. a -> Maybe a
Just ()
isInterleavedData InterleavedDecl
_ = Maybe ()
forall a. Maybe a
Nothing
interleavedDecl :: Name -> InterleavedDecl -> [(Int, NiceDeclaration)]
interleavedDecl :: Name -> InterleavedDecl -> [(Int, NiceDeclaration)]
interleavedDecl Name
k = \case
InterleavedData (Int
i, d :: NiceDeclaration
d@(NiceDataSig Range
_ Access
acc IsAbstract
abs PositivityCheck
pc UniverseCheck
uc Name
_ [LamBinding]
pars Expr
_)) Maybe (Int, [[NiceDeclaration]])
ds ->
let fpars :: [LamBinding]
fpars = (LamBinding -> [LamBinding]) -> [LamBinding] -> [LamBinding]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LamBinding -> [LamBinding]
dropTypeAndModality [LamBinding]
pars
ddef :: [NiceDeclaration] -> NiceDeclaration
ddef = Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> [NiceDeclaration]
-> NiceDeclaration
NiceDataDef Range
forall a. Range' a
noRange Origin
UserWritten IsAbstract
abs PositivityCheck
pc UniverseCheck
uc Name
k [LamBinding]
fpars
in (Int
i,NiceDeclaration
d) (Int, NiceDeclaration)
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. a -> [a] -> [a]
: [(Int, NiceDeclaration)]
-> ((Int, [[NiceDeclaration]]) -> [(Int, NiceDeclaration)])
-> Maybe (Int, [[NiceDeclaration]])
-> [(Int, NiceDeclaration)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\ (Int
j, [[NiceDeclaration]]
dss) -> [(Int
j, [NiceDeclaration] -> NiceDeclaration
ddef ([[NiceDeclaration]] -> [NiceDeclaration]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[NiceDeclaration]] -> [[NiceDeclaration]]
forall a. [a] -> [a]
reverse [[NiceDeclaration]]
dss)))]) Maybe (Int, [[NiceDeclaration]])
ds
InterleavedFun (Int
i, d :: NiceDeclaration
d@(FunSig Range
r Access
acc IsAbstract
abs IsInstance
inst IsMacro
mac ArgInfo
info TerminationCheck
tc CoverageCheck
cc Name
n Expr
e)) Maybe (Int, [([Declaration], [Clause])])
dcs ->
let fdef :: [([Declaration], [Clause])] -> NiceDeclaration
fdef [([Declaration], [Clause])]
dcss = let ([[Declaration]]
dss, [[Clause]]
css) = [([Declaration], [Clause])] -> ([[Declaration]], [[Clause]])
forall a b. [(a, b)] -> ([a], [b])
unzip [([Declaration], [Clause])]
dcss in
Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> [Clause]
-> NiceDeclaration
FunDef Range
r ([[Declaration]] -> [Declaration]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Declaration]]
dss) IsAbstract
abs IsInstance
inst TerminationCheck
tc CoverageCheck
cc Name
n ([[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Clause]]
css)
in (Int
i,NiceDeclaration
d) (Int, NiceDeclaration)
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. a -> [a] -> [a]
: [(Int, NiceDeclaration)]
-> ((Int, [([Declaration], [Clause])]) -> [(Int, NiceDeclaration)])
-> Maybe (Int, [([Declaration], [Clause])])
-> [(Int, NiceDeclaration)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\ (Int
j, [([Declaration], [Clause])]
dcss) -> [(Int
j, [([Declaration], [Clause])] -> NiceDeclaration
fdef ([([Declaration], [Clause])] -> [([Declaration], [Clause])]
forall a. [a] -> [a]
reverse [([Declaration], [Clause])]
dcss))]) Maybe (Int, [([Declaration], [Clause])])
dcs
InterleavedDecl
_ -> [(Int, NiceDeclaration)]
forall a. HasCallStack => a
__IMPOSSIBLE__
data KindOfBlock
= PostulateBlock
| PrimitiveBlock
| InstanceBlock
| FieldBlock
| DataBlock
| ConstructorBlock
deriving (Typeable KindOfBlock
DataType
Constr
Typeable KindOfBlock
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindOfBlock)
-> (KindOfBlock -> Constr)
-> (KindOfBlock -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KindOfBlock))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c KindOfBlock))
-> ((forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r)
-> (forall u. (forall d. Data d => d -> u) -> KindOfBlock -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock)
-> Data KindOfBlock
KindOfBlock -> DataType
KindOfBlock -> Constr
(forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindOfBlock
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u
forall u. (forall d. Data d => d -> u) -> KindOfBlock -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindOfBlock
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KindOfBlock)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c KindOfBlock)
$cConstructorBlock :: Constr
$cDataBlock :: Constr
$cFieldBlock :: Constr
$cInstanceBlock :: Constr
$cPrimitiveBlock :: Constr
$cPostulateBlock :: Constr
$tKindOfBlock :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
gmapMp :: (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
gmapM :: (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
gmapQi :: Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u
gmapQ :: (forall d. Data d => d -> u) -> KindOfBlock -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> KindOfBlock -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
gmapT :: (forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock
$cgmapT :: (forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c KindOfBlock)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c KindOfBlock)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c KindOfBlock)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KindOfBlock)
dataTypeOf :: KindOfBlock -> DataType
$cdataTypeOf :: KindOfBlock -> DataType
toConstr :: KindOfBlock -> Constr
$ctoConstr :: KindOfBlock -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindOfBlock
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindOfBlock
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock
$cp1Data :: Typeable KindOfBlock
Data, KindOfBlock -> KindOfBlock -> Bool
(KindOfBlock -> KindOfBlock -> Bool)
-> (KindOfBlock -> KindOfBlock -> Bool) -> Eq KindOfBlock
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: KindOfBlock -> KindOfBlock -> Bool
$c/= :: KindOfBlock -> KindOfBlock -> Bool
== :: KindOfBlock -> KindOfBlock -> Bool
$c== :: KindOfBlock -> KindOfBlock -> Bool
Eq, Eq KindOfBlock
Eq KindOfBlock
-> (KindOfBlock -> KindOfBlock -> Ordering)
-> (KindOfBlock -> KindOfBlock -> Bool)
-> (KindOfBlock -> KindOfBlock -> Bool)
-> (KindOfBlock -> KindOfBlock -> Bool)
-> (KindOfBlock -> KindOfBlock -> Bool)
-> (KindOfBlock -> KindOfBlock -> KindOfBlock)
-> (KindOfBlock -> KindOfBlock -> KindOfBlock)
-> Ord KindOfBlock
KindOfBlock -> KindOfBlock -> Bool
KindOfBlock -> KindOfBlock -> Ordering
KindOfBlock -> KindOfBlock -> KindOfBlock
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: KindOfBlock -> KindOfBlock -> KindOfBlock
$cmin :: KindOfBlock -> KindOfBlock -> KindOfBlock
max :: KindOfBlock -> KindOfBlock -> KindOfBlock
$cmax :: KindOfBlock -> KindOfBlock -> KindOfBlock
>= :: KindOfBlock -> KindOfBlock -> Bool
$c>= :: KindOfBlock -> KindOfBlock -> Bool
> :: KindOfBlock -> KindOfBlock -> Bool
$c> :: KindOfBlock -> KindOfBlock -> Bool
<= :: KindOfBlock -> KindOfBlock -> Bool
$c<= :: KindOfBlock -> KindOfBlock -> Bool
< :: KindOfBlock -> KindOfBlock -> Bool
$c< :: KindOfBlock -> KindOfBlock -> Bool
compare :: KindOfBlock -> KindOfBlock -> Ordering
$ccompare :: KindOfBlock -> KindOfBlock -> Ordering
$cp1Ord :: Eq KindOfBlock
Ord, Int -> KindOfBlock -> ShowS
[KindOfBlock] -> ShowS
KindOfBlock -> String
(Int -> KindOfBlock -> ShowS)
-> (KindOfBlock -> String)
-> ([KindOfBlock] -> ShowS)
-> Show KindOfBlock
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [KindOfBlock] -> ShowS
$cshowList :: [KindOfBlock] -> ShowS
show :: KindOfBlock -> String
$cshow :: KindOfBlock -> String
showsPrec :: Int -> KindOfBlock -> ShowS
$cshowsPrec :: Int -> KindOfBlock -> ShowS
Show)
instance HasRange NiceDeclaration where
getRange :: NiceDeclaration -> Range
getRange (Axiom Range
r Access
_ IsAbstract
_ IsInstance
_ ArgInfo
_ Name
_ Expr
_) = Range
r
getRange (NiceField Range
r Access
_ IsAbstract
_ IsInstance
_ TacticAttribute
_ Name
_ Arg Expr
_) = Range
r
getRange (NiceMutual Range
r TerminationCheck
_ CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
_) = Range
r
getRange (NiceModule Range
r Access
_ IsAbstract
_ QName
_ Telescope
_ [Declaration]
_ ) = Range
r
getRange (NiceModuleMacro Range
r Access
_ Name
_ ModuleApplication
_ OpenShortHand
_ ImportDirective
_) = Range
r
getRange (NiceOpen Range
r QName
_ ImportDirective
_) = Range
r
getRange (NiceImport Range
r QName
_ Maybe AsName
_ OpenShortHand
_ ImportDirective
_) = Range
r
getRange (NicePragma Range
r Pragma
_) = Range
r
getRange (PrimitiveFunction Range
r Access
_ IsAbstract
_ Name
_ Arg Expr
_) = Range
r
getRange (FunSig Range
r Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
_ CoverageCheck
_ Name
_ Expr
_) = Range
r
getRange (FunDef Range
r [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ [Clause]
_) = Range
r
getRange (NiceDataDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ [NiceDeclaration]
_) = Range
r
getRange (NiceLoneConstructor Range
r [NiceDeclaration]
_) = Range
r
getRange (NiceRecDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ RecordDirectives
_ [LamBinding]
_ [Declaration]
_) = Range
r
getRange (NiceRecSig Range
r Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_) = Range
r
getRange (NiceDataSig Range
r Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_) = Range
r
getRange (NicePatternSyn Range
r Access
_ Name
_ [Arg Name]
_ Pattern
_) = Range
r
getRange (NiceGeneralize Range
r Access
_ ArgInfo
_ TacticAttribute
_ Name
_ Expr
_) = Range
r
getRange (NiceFunClause Range
r Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ Bool
_ Declaration
_) = Range
r
getRange (NiceUnquoteDecl Range
r Access
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_) = Range
r
getRange (NiceUnquoteDef Range
r Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_) = Range
r
instance Pretty NiceDeclaration where
pretty :: NiceDeclaration -> Doc
pretty = \case
Axiom Range
_ Access
_ IsAbstract
_ IsInstance
_ ArgInfo
_ Name
x Expr
_ -> String -> Doc
text String
"postulate" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> String -> Doc
text String
"_"
NiceField Range
_ Access
_ IsAbstract
_ IsInstance
_ TacticAttribute
_ Name
x Arg Expr
_ -> String -> Doc
text String
"field" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
PrimitiveFunction Range
_ Access
_ IsAbstract
_ Name
x Arg Expr
_ -> String -> Doc
text String
"primitive" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
NiceMutual{} -> String -> Doc
text String
"mutual"
NiceModule Range
_ Access
_ IsAbstract
_ QName
x Telescope
_ [Declaration]
_ -> String -> Doc
text String
"module" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"where"
NiceModuleMacro Range
_ Access
_ Name
x ModuleApplication
_ OpenShortHand
_ ImportDirective
_ -> String -> Doc
text String
"module" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"= ..."
NiceOpen Range
_ QName
x ImportDirective
_ -> String -> Doc
text String
"open" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
NiceImport Range
_ QName
x Maybe AsName
_ OpenShortHand
_ ImportDirective
_ -> String -> Doc
text String
"import" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
NicePragma{} -> String -> Doc
text String
"{-# ... #-}"
NiceRecSig Range
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
_ Expr
_ -> String -> Doc
text String
"record" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
NiceDataSig Range
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
_ Expr
_ -> String -> Doc
text String
"data" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
NiceFunClause{} -> String -> Doc
text String
"<function clause>"
FunSig Range
_ Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
_ CoverageCheck
_ Name
x Expr
_ -> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> String -> Doc
text String
"_"
FunDef Range
_ [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
x [Clause]
_ -> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"= _"
NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
_ [NiceDeclaration]
_ -> String -> Doc
text String
"data" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"where"
NiceLoneConstructor Range
_ [NiceDeclaration]
ds -> String -> Doc
text String
"constructor"
NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x RecordDirectives
_ [LamBinding]
_ [Declaration]
_ -> String -> Doc
text String
"record" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"where"
NicePatternSyn Range
_ Access
_ Name
x [Arg Name]
_ Pattern
_ -> String -> Doc
text String
"pattern" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
NiceGeneralize Range
_ Access
_ ArgInfo
_ TacticAttribute
_ Name
x Expr
_ -> String -> Doc
text String
"variable" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
NiceUnquoteDecl Range
_ Access
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ [Name]
xs Expr
_ -> String -> Doc
text String
"<unquote declarations>"
NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ [Name]
xs Expr
_ -> String -> Doc
text String
"<unquote definitions>"
declName :: NiceDeclaration -> String
declName :: NiceDeclaration -> String
declName Axiom{} = String
"Postulates"
declName NiceField{} = String
"Fields"
declName NiceMutual{} = String
"Mutual blocks"
declName NiceModule{} = String
"Modules"
declName NiceModuleMacro{} = String
"Modules"
declName NiceOpen{} = String
"Open declarations"
declName NiceImport{} = String
"Import statements"
declName NicePragma{} = String
"Pragmas"
declName PrimitiveFunction{} = String
"Primitive declarations"
declName NicePatternSyn{} = String
"Pattern synonyms"
declName NiceGeneralize{} = String
"Generalized variables"
declName NiceUnquoteDecl{} = String
"Unquoted declarations"
declName NiceUnquoteDef{} = String
"Unquoted definitions"
declName NiceRecSig{} = String
"Records"
declName NiceDataSig{} = String
"Data types"
declName NiceFunClause{} = String
"Functions without a type signature"
declName FunSig{} = String
"Type signatures"
declName FunDef{} = String
"Function definitions"
declName NiceRecDef{} = String
"Records"
declName NiceDataDef{} = String
"Data types"
declName NiceLoneConstructor{} = String
"Constructors"
data InMutual
= InMutual
| NotInMutual
deriving (InMutual -> InMutual -> Bool
(InMutual -> InMutual -> Bool)
-> (InMutual -> InMutual -> Bool) -> Eq InMutual
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InMutual -> InMutual -> Bool
$c/= :: InMutual -> InMutual -> Bool
== :: InMutual -> InMutual -> Bool
$c== :: InMutual -> InMutual -> Bool
Eq, Int -> InMutual -> ShowS
[InMutual] -> ShowS
InMutual -> String
(Int -> InMutual -> ShowS)
-> (InMutual -> String) -> ([InMutual] -> ShowS) -> Show InMutual
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InMutual] -> ShowS
$cshowList :: [InMutual] -> ShowS
show :: InMutual -> String
$cshow :: InMutual -> String
showsPrec :: Int -> InMutual -> ShowS
$cshowsPrec :: Int -> InMutual -> ShowS
Show)
data DataRecOrFun
= DataName
{ DataRecOrFun -> PositivityCheck
_kindPosCheck :: PositivityCheck
, DataRecOrFun -> UniverseCheck
_kindUniCheck :: UniverseCheck
}
| RecName
{ _kindPosCheck :: PositivityCheck
, _kindUniCheck :: UniverseCheck
}
| FunName TerminationCheck CoverageCheck
deriving (Typeable DataRecOrFun
DataType
Constr
Typeable DataRecOrFun
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataRecOrFun)
-> (DataRecOrFun -> Constr)
-> (DataRecOrFun -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataRecOrFun))
-> ((forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r)
-> (forall u. (forall d. Data d => d -> u) -> DataRecOrFun -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun)
-> Data DataRecOrFun
DataRecOrFun -> DataType
DataRecOrFun -> Constr
(forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataRecOrFun
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u
forall u. (forall d. Data d => d -> u) -> DataRecOrFun -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataRecOrFun
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataRecOrFun)
$cFunName :: Constr
$cRecName :: Constr
$cDataName :: Constr
$tDataRecOrFun :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
gmapMp :: (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
gmapM :: (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
gmapQi :: Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u
gmapQ :: (forall d. Data d => d -> u) -> DataRecOrFun -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataRecOrFun -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
gmapT :: (forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun
$cgmapT :: (forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataRecOrFun)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataRecOrFun)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun)
dataTypeOf :: DataRecOrFun -> DataType
$cdataTypeOf :: DataRecOrFun -> DataType
toConstr :: DataRecOrFun -> Constr
$ctoConstr :: DataRecOrFun -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataRecOrFun
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataRecOrFun
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun
$cp1Data :: Typeable DataRecOrFun
Data, Int -> DataRecOrFun -> ShowS
[DataRecOrFun] -> ShowS
DataRecOrFun -> String
(Int -> DataRecOrFun -> ShowS)
-> (DataRecOrFun -> String)
-> ([DataRecOrFun] -> ShowS)
-> Show DataRecOrFun
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataRecOrFun] -> ShowS
$cshowList :: [DataRecOrFun] -> ShowS
show :: DataRecOrFun -> String
$cshow :: DataRecOrFun -> String
showsPrec :: Int -> DataRecOrFun -> ShowS
$cshowsPrec :: Int -> DataRecOrFun -> ShowS
Show)
instance Eq DataRecOrFun where
DataName{} == :: DataRecOrFun -> DataRecOrFun -> Bool
== DataName{} = Bool
True
RecName{} == RecName{} = Bool
True
FunName{} == FunName{} = Bool
True
DataRecOrFun
_ == DataRecOrFun
_ = Bool
False
instance Pretty DataRecOrFun where
pretty :: DataRecOrFun -> Doc
pretty DataName{} = Doc
"data type"
pretty RecName{} = Doc
"record type"
pretty FunName{} = Doc
"function"
isFunName :: DataRecOrFun -> Bool
isFunName :: DataRecOrFun -> Bool
isFunName (FunName{}) = Bool
True
isFunName DataRecOrFun
_ = Bool
False
sameKind :: DataRecOrFun -> DataRecOrFun -> Bool
sameKind :: DataRecOrFun -> DataRecOrFun -> Bool
sameKind = DataRecOrFun -> DataRecOrFun -> Bool
forall a. Eq a => a -> a -> Bool
(==)
terminationCheck :: DataRecOrFun -> TerminationCheck
terminationCheck :: DataRecOrFun -> TerminationCheck
terminationCheck (FunName TerminationCheck
tc CoverageCheck
_) = TerminationCheck
tc
terminationCheck DataRecOrFun
_ = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
coverageCheck :: DataRecOrFun -> CoverageCheck
coverageCheck :: DataRecOrFun -> CoverageCheck
coverageCheck (FunName TerminationCheck
_ CoverageCheck
cc) = CoverageCheck
cc
coverageCheck DataRecOrFun
_ = CoverageCheck
YesCoverageCheck
positivityCheck :: DataRecOrFun -> PositivityCheck
positivityCheck :: DataRecOrFun -> PositivityCheck
positivityCheck (DataName PositivityCheck
pc UniverseCheck
_) = PositivityCheck
pc
positivityCheck (RecName PositivityCheck
pc UniverseCheck
_) = PositivityCheck
pc
positivityCheck (FunName TerminationCheck
_ CoverageCheck
_) = PositivityCheck
YesPositivityCheck
mutualChecks :: DataRecOrFun -> MutualChecks
mutualChecks :: DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [DataRecOrFun -> TerminationCheck
terminationCheck DataRecOrFun
k] [DataRecOrFun -> CoverageCheck
coverageCheck DataRecOrFun
k] [DataRecOrFun -> PositivityCheck
positivityCheck DataRecOrFun
k]
universeCheck :: DataRecOrFun -> UniverseCheck
universeCheck :: DataRecOrFun -> UniverseCheck
universeCheck (DataName PositivityCheck
_ UniverseCheck
uc) = UniverseCheck
uc
universeCheck (RecName PositivityCheck
_ UniverseCheck
uc) = UniverseCheck
uc
universeCheck (FunName TerminationCheck
_ CoverageCheck
_) = UniverseCheck
YesUniverseCheck