-- | Defines local checks, i.e. checks which only look at one declaration at a
--   time.

module Language.Haskell.FreeTheorems.Frontend.CheckLocal (
    checkLocal
  , checkDataAndNewtypeDeclarations
) where



import Data.Generics (Data, everything, mkQ)
import Data.List (group, sort)
import Data.Maybe (mapMaybe, fromJust, isJust)
import qualified Data.Set as Set
    ( Set, union, empty, difference, fromList, null, elems, isSubsetOf
    , singleton)

import Language.Haskell.FreeTheorems.Syntax
import Language.Haskell.FreeTheorems.Frontend.Error
import Language.Haskell.FreeTheorems.Frontend.TypeExpressions





------- Local checks ----------------------------------------------------------


-- | Check validity of every declaration.
--   This includes ensuring that fixed type expressions occur nowhere, that only
--   declared type variables occur in right-hand sides and that no primitive
--   type is declared, among other restrictions.
--
--   Local checks comprise all those which can be down by just looking at a
--   single declaration.

checkLocal :: [Declaration] -> Checked [Declaration]
checkLocal :: [Declaration] -> Checked [Declaration]
checkLocal = forall a b. (a -> ErrorOr b) -> [a] -> Checked [a]
foldChecks Declaration -> ErrorOr ()
checkDecl
  where
    checkDecl :: Declaration -> ErrorOr ()
    checkDecl :: Declaration -> ErrorOr ()
checkDecl (DataDecl DataDeclaration
d)    = DataDeclaration -> ErrorOr ()
checkDataDecl DataDeclaration
d
    checkDecl (NewtypeDecl NewtypeDeclaration
d) = NewtypeDeclaration -> ErrorOr ()
checkNewtypeDecl NewtypeDeclaration
d
    checkDecl (TypeDecl TypeDeclaration
d)    = TypeDeclaration -> ErrorOr ()
checkTypeDecl TypeDeclaration
d
    checkDecl (ClassDecl ClassDeclaration
d)   = ClassDeclaration -> ErrorOr ()
checkClassDecl ClassDeclaration
d
    checkDecl (TypeSig Signature
sig)   = Signature -> ErrorOr ()
checkSignature Signature
sig



-- | Checks a @data@ declaration. The following restrictions must hold:
--   
--   * The declared type constructor is not a primitive type.
--   * The variables occurring on the right-hand side have to be mentioned on
--     the left-hand side, and the left-hand side variables are pairwise
--     distinct.
--   * The declaration is not nested, i.e. if the declared type constructor
--     occurs on the right-hand side, it has only type variables as arguments.
--   * No fixed type expression occurs in any type expression.

checkDataDecl :: DataDeclaration -> ErrorOr ()
checkDataDecl :: DataDeclaration -> ErrorOr ()
checkDataDecl DataDeclaration
d =
  forall a. Declaration -> ErrorOr a -> ErrorOr a
inDecl (DataDeclaration -> Declaration
DataDecl DataDeclaration
d) forall a b. (a -> b) -> a -> b
$ do
    Identifier -> ErrorOr ()
checkNotPrimitive (DataDeclaration -> Identifier
dataName DataDeclaration
d)
    [TypeVariable] -> Set TypeVariable -> ErrorOr ()
checkVariables (DataDeclaration -> [TypeVariable]
dataVars DataDeclaration
d)
                   (forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything forall a. Ord a => Set a -> Set a -> Set a
Set.union
                      (forall a. Set a
Set.empty forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
`mkQ` (TypeExpression -> Set TypeVariable
freeTypeVariables forall b c a. (b -> c) -> (a -> b) -> a -> c
. BangTypeExpression -> TypeExpression
withoutBang)) 
                      (DataDeclaration -> [DataConstructorDeclaration]
dataCons DataDeclaration
d))
    [DataConstructorDeclaration] -> ErrorOr ()
checkNotEmpty (DataDeclaration -> [DataConstructorDeclaration]
dataCons DataDeclaration
d)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Identifier
-> [TypeExpression] -> (Identifier, [TypeExpression]) -> ErrorOr ()
checkNotNested (DataDeclaration -> Identifier
dataName DataDeclaration
d) (forall a b. (a -> b) -> [a] -> [b]
map TypeVariable -> TypeExpression
TypeVar (DataDeclaration -> [TypeVariable]
dataVars DataDeclaration
d)))
          (DataDeclaration -> [(Identifier, [TypeExpression])]
conNamesAndTypes DataDeclaration
d)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> (Identifier, [TypeExpression]) -> ErrorOr ()
checkNoFixedTEsNamed String
"data constructor") (DataDeclaration -> [(Identifier, [TypeExpression])]
conNamesAndTypes DataDeclaration
d)
  where
    conNamesAndTypes :: DataDeclaration -> [(Identifier, [TypeExpression])]
conNamesAndTypes = 
      forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b) -> (a -> c) -> a -> (b, c)
makePair DataConstructorDeclaration -> Identifier
dataConName (forall a b. (a -> b) -> [a] -> [b]
map BangTypeExpression -> TypeExpression
withoutBang forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConstructorDeclaration -> [BangTypeExpression]
dataConTypes)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDeclaration -> [DataConstructorDeclaration]
dataCons



-- | Checks a @newtype@ declaration. The following restrictions must hold:
--   
--   * The declared type constructor is not a primitive type.
--   * The variables occurring on the right-hand side have to be mentioned on
--     the left-hand side, and the left-hand side variables are pairwise
--     distinct.
--   * The declaration is not nested, i.e. if the declared type constructor
--     occurs on the right-hand side, it has only type variables as arguments.
--   * No fixed type expression occurs in the right-hand side type expression.

checkNewtypeDecl :: NewtypeDeclaration -> ErrorOr ()
checkNewtypeDecl :: NewtypeDeclaration -> ErrorOr ()
checkNewtypeDecl NewtypeDeclaration
d =
  forall a. Declaration -> ErrorOr a -> ErrorOr a
inDecl (NewtypeDeclaration -> Declaration
NewtypeDecl NewtypeDeclaration
d) forall a b. (a -> b) -> a -> b
$ do
    Identifier -> ErrorOr ()
checkNotPrimitive (NewtypeDeclaration -> Identifier
newtypeName NewtypeDeclaration
d)
    [TypeVariable] -> Set TypeVariable -> ErrorOr ()
checkVariables (NewtypeDeclaration -> [TypeVariable]
newtypeVars NewtypeDeclaration
d) (TypeExpression -> Set TypeVariable
freeTypeVariables forall a b. (a -> b) -> a -> b
$ NewtypeDeclaration -> TypeExpression
newtypeRhs NewtypeDeclaration
d)
    Identifier
-> [TypeExpression] -> (Identifier, [TypeExpression]) -> ErrorOr ()
checkNotNested (NewtypeDeclaration -> Identifier
newtypeName NewtypeDeclaration
d) (forall a b. (a -> b) -> [a] -> [b]
map TypeVariable -> TypeExpression
TypeVar (NewtypeDeclaration -> [TypeVariable]
newtypeVars NewtypeDeclaration
d)) (NewtypeDeclaration -> (Identifier, [TypeExpression])
conAndType NewtypeDeclaration
d)
    String -> (Identifier, [TypeExpression]) -> ErrorOr ()
checkNoFixedTEsNamed String
"data constructor" (NewtypeDeclaration -> (Identifier, [TypeExpression])
conAndType NewtypeDeclaration
d)
  where
    conAndType :: NewtypeDeclaration -> (Identifier, [TypeExpression])
conAndType = forall a b c. (a -> b) -> (a -> c) -> a -> (b, c)
makePair NewtypeDeclaration -> Identifier
newtypeCon (forall a. a -> [a]
singletonList forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewtypeDeclaration -> TypeExpression
newtypeRhs)



-- | Checks a @type@ declaration. The following restrictions must hold:
--   
--   * The declared type constructor is not a primitive type.
--   * The variables occurring on the right-hand side have to be mentioned on
--     the left-hand side, and the left-hand side variables are pairwise
--     distinct.
--   * The declaration must not be recursive, i.e. the type constructor declared
--     by this declaration must not occur on th right-hand side.
--   * No fixed type expression occurs in the right-hand side type expression.

checkTypeDecl :: TypeDeclaration -> ErrorOr ()
checkTypeDecl :: TypeDeclaration -> ErrorOr ()
checkTypeDecl TypeDeclaration
d = 
  forall a. Declaration -> ErrorOr a -> ErrorOr a
inDecl (TypeDeclaration -> Declaration
TypeDecl TypeDeclaration
d) forall a b. (a -> b) -> a -> b
$ do
    Identifier -> ErrorOr ()
checkNotPrimitive (TypeDeclaration -> Identifier
typeName TypeDeclaration
d)
    [TypeVariable] -> Set TypeVariable -> ErrorOr ()
checkVariables (TypeDeclaration -> [TypeVariable]
typeVars TypeDeclaration
d) (TypeExpression -> Set TypeVariable
freeTypeVariables forall a b. (a -> b) -> a -> b
$ TypeDeclaration -> TypeExpression
typeRhs TypeDeclaration
d)
    Identifier -> TypeExpression -> ErrorOr ()
checkTypeDeclNotRecursive (TypeDeclaration -> Identifier
typeName TypeDeclaration
d) (TypeDeclaration -> TypeExpression
typeRhs TypeDeclaration
d)
    TypeExpression -> ErrorOr ()
checkNoFixedTEs (TypeDeclaration -> TypeExpression
typeRhs TypeDeclaration
d)



-- | Checks a @class@ declaration. The following restrictions must hold:
--   
--   * The declared type class does not equal a primitive type.
--   * The names of the class methods are pairwise distinct. 
--   * The class variable occurs in the type expression of every class method.
--   * The name of the class does not occur in a type expression of any class
--     method.
--   * No fixed type expression occurs in a type expression of any class method.

checkClassDecl :: ClassDeclaration -> ErrorOr ()
checkClassDecl :: ClassDeclaration -> ErrorOr ()
checkClassDecl ClassDeclaration
d =
  forall a. Declaration -> ErrorOr a -> ErrorOr a
inDecl (ClassDeclaration -> Declaration
ClassDecl ClassDeclaration
d) forall a b. (a -> b) -> a -> b
$ do
    Identifier -> ErrorOr ()
checkNotPrimitive (ClassDeclaration -> Identifier
className ClassDeclaration
d)
    [Identifier] -> ErrorOr ()
checkClassMethodsDistinct (forall a b. (a -> b) -> [a] -> [b]
map Signature -> Identifier
signatureName forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClassDeclaration -> [Signature]
classFuns forall a b. (a -> b) -> a -> b
$ ClassDeclaration
d)
    TypeVariable -> [Signature] -> ErrorOr ()
checkClassVarInMethods (ClassDeclaration -> TypeVariable
classVar ClassDeclaration
d) (ClassDeclaration -> [Signature]
classFuns ClassDeclaration
d)
    Identifier -> [Signature] -> ErrorOr ()
checkClassDeclNotRecursive (ClassDeclaration -> Identifier
className ClassDeclaration
d) (ClassDeclaration -> [Signature]
classFuns ClassDeclaration
d)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> (Identifier, [TypeExpression]) -> ErrorOr ()
checkNoFixedTEsNamed String
"class method")
          (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b) -> (a -> c) -> a -> (b, c)
makePair Signature -> Identifier
signatureName (forall a. a -> [a]
singletonList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature -> TypeExpression
signatureType))
               (ClassDeclaration -> [Signature]
classFuns ClassDeclaration
d))



-- | Checks a type signature. The following restrictions must hold:
--   
--   * No fixed type expressions occurs in the type expression of this type
--     signature.

checkSignature :: Signature -> ErrorOr ()
checkSignature :: Signature -> ErrorOr ()
checkSignature Signature
s =
  forall a. Declaration -> ErrorOr a -> ErrorOr a
inDecl (Signature -> Declaration
TypeSig Signature
s) forall a b. (a -> b) -> a -> b
$ do
    TypeExpression -> ErrorOr ()
checkNoFixedTEs (Signature -> TypeExpression
signatureType Signature
s)





------- Special checks for data and newtype declarations ----------------------


-- | Check data and newtype declarations for occurring function type
--   constructors or type abstraction constructors. If any declaration contains
--   one of these, an error message is created. All other declarations are
--   passed.

checkDataAndNewtypeDeclarations :: [Declaration] -> Checked [Declaration]
checkDataAndNewtypeDeclarations :: [Declaration] -> Checked [Declaration]
checkDataAndNewtypeDeclarations = forall a b. (a -> ErrorOr b) -> [a] -> Checked [a]
foldChecks Declaration -> ErrorOr ()
checkDN
  where
    checkDN :: Declaration -> ErrorOr ()
    checkDN :: Declaration -> ErrorOr ()
checkDN Declaration
d = case Declaration
d of
      DataDecl DataDeclaration
d'    -> forall a. Declaration -> ErrorOr a -> ErrorOr a
inDecl Declaration
d (forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Identifier, [TypeExpression]) -> ErrorOr ()
checkAbsFun (DataDeclaration -> [(Identifier, [TypeExpression])]
dataConsAndTypes DataDeclaration
d'))
      NewtypeDecl NewtypeDeclaration
d' -> forall a. Declaration -> ErrorOr a -> ErrorOr a
inDecl Declaration
d ((Identifier, [TypeExpression]) -> ErrorOr ()
checkAbsFun (NewtypeDeclaration -> (Identifier, [TypeExpression])
newtypeConAndType NewtypeDeclaration
d'))
      Declaration
otherwise      -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

    dataConsAndTypes :: DataDeclaration -> [(Identifier, [TypeExpression])]
dataConsAndTypes =
      forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b) -> (a -> c) -> a -> (b, c)
makePair DataConstructorDeclaration -> Identifier
dataConName (forall a b. (a -> b) -> [a] -> [b]
map BangTypeExpression -> TypeExpression
withoutBang forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConstructorDeclaration -> [BangTypeExpression]
dataConTypes)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDeclaration -> [DataConstructorDeclaration]
dataCons
    
    newtypeConAndType :: NewtypeDeclaration -> (Identifier, [TypeExpression])
newtypeConAndType = forall a b c. (a -> b) -> (a -> c) -> a -> (b, c)
makePair NewtypeDeclaration -> Identifier
newtypeCon (forall a. a -> [a]
singletonList forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewtypeDeclaration -> TypeExpression
newtypeRhs)






------- Checking restrictions -------------------------------------------------


-- | Checks if the given identifier is not a name of a primitive type.
--   Otherwise, an error message is created.

checkNotPrimitive :: Identifier -> ErrorOr ()
checkNotPrimitive :: Identifier -> ErrorOr ()
checkNotPrimitive (Ident String
name) =
  Bool -> Doc -> ErrorOr ()
errorIf (String
name forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Int", String
"Integer", String
"Float", String
"Double", String
"Char"]) forall a b. (a -> b) -> a -> b
$
    String -> Doc
pp (String
"A primitive type must not have a declaration.")
  


-- | Checks if the second argument set is contained in the first argument list.
--   If not, an error message is returned.
--
--   Checks also if first argument contains pairwise distinct variables.
--   If not, an error message is returned.

checkVariables :: [TypeVariable] -> Set.Set TypeVariable -> ErrorOr ()
checkVariables :: [TypeVariable] -> Set TypeVariable -> ErrorOr ()
checkVariables [TypeVariable]
vs Set TypeVariable
rvs = do
  let es :: [TypeVariable]
es = forall a. Ord a => [a] -> [a]
extractRepeatingElements [TypeVariable]
vs
  Bool -> Doc -> ErrorOr ()
errorIf (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeVariable]
es) forall a b. (a -> b) -> a -> b
$
    String -> Doc
pp (String
"Type variables must not be given more than once on the left-hand "
        forall a. [a] -> [a] -> [a]
++ String
"side of a declaration. "
        forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
violating String
"variable" (forall a b. (a -> b) -> [a] -> [b]
map TypeVariable -> String
varName forall a b. (a -> b) -> a -> b
$ [TypeVariable]
es))

  let set :: Set TypeVariable
set = Set TypeVariable
rvs forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` forall a. Ord a => [a] -> Set a
Set.fromList [TypeVariable]
vs
  Bool -> Doc -> ErrorOr ()
errorIf (Bool -> Bool
not (forall a. Set a -> Bool
Set.null Set TypeVariable
set)) forall a b. (a -> b) -> a -> b
$
    String -> Doc
pp (String
"Type variables occurring on the right-hand side of a declaration must "
        forall a. [a] -> [a] -> [a]
++ String
"be declared on the left-hand side. "
        forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
violating String
"variable" (forall a b. (a -> b) -> [a] -> [b]
map TypeVariable -> String
varName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.elems forall a b. (a -> b) -> a -> b
$ Set TypeVariable
set))

  where
    varName :: TypeVariable -> String
varName (TV Identifier
v) = Identifier -> String
unpackIdent Identifier
v



-- | Checks that there is at least one data constructor declaration in the the
--   declaration of an algebraic data type.

checkNotEmpty :: [DataConstructorDeclaration] -> ErrorOr ()
checkNotEmpty :: [DataConstructorDeclaration] -> ErrorOr ()
checkNotEmpty [DataConstructorDeclaration]
cons =
  Bool -> Doc -> ErrorOr ()
errorIf (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DataConstructorDeclaration]
cons) forall a b. (a -> b) -> a -> b
$
    String -> Doc
pp (String
"The declaration of an algebraic data type must have at least one "
        forall a. [a] -> [a] -> [a]
++ String
"data constructor.")



-- | Checks if the identifiers occurs in any of the given type expressions as
--   a type constructor. If so, and if the identifier is applied not only to
--   type variables, it is called nested and an error message is created.

checkNotNested :: 
    Identifier -> [TypeExpression] -> (Identifier, [TypeExpression]) 
    -> ErrorOr ()
checkNotNested :: Identifier
-> [TypeExpression] -> (Identifier, [TypeExpression]) -> ErrorOr ()
checkNotNested Identifier
con [TypeExpression]
vs (Identifier
dcon, [TypeExpression]
ts) =
  Bool -> Doc -> ErrorOr ()
errorIf (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a b. (Data a, Data b) => (a -> Bool) -> b -> Bool
satisfiesSomewhere TypeExpression -> Bool
isNested) [TypeExpression]
ts) forall a b. (a -> b) -> a -> b
$
    String -> Doc
pp (String
"Declarations must not be nested."
        forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
violating String
"data constructor" [Identifier -> String
unpackIdent Identifier
dcon])
  where
    isNested :: TypeExpression -> Bool
isNested TypeExpression
t = case TypeExpression
t of
      TypeCon (Con Identifier
c) [TypeExpression]
ts -> Identifier
c forall a. Eq a => a -> a -> Bool
== Identifier
con Bool -> Bool -> Bool
&& [TypeExpression]
ts forall a. Eq a => a -> a -> Bool
/= [TypeExpression]
vs
      TypeExpression
otherwise          -> Bool
False



-- | Checks if a type declaration is recursive, i.e. the identifier occurs in
--   the given type expression as a type constructor.
--   If so, an error message is created.

checkTypeDeclNotRecursive :: Identifier -> TypeExpression -> ErrorOr ()
checkTypeDeclNotRecursive :: Identifier -> TypeExpression -> ErrorOr ()
checkTypeDeclNotRecursive Identifier
ident TypeExpression
t =
  Bool -> Doc -> ErrorOr ()
errorIf (forall a b. (Data a, Data b) => (a -> Bool) -> b -> Bool
satisfiesSomewhere (Identifier -> TypeExpression -> Bool
isCon Identifier
ident) TypeExpression
t) forall a b. (a -> b) -> a -> b
$
    String -> Doc
pp (String
"A type synonym must not be declared recursively.")
  where
    isCon :: Identifier -> TypeExpression -> Bool
isCon Identifier
ident TypeExpression
t = case TypeExpression
t of
      TypeCon (Con Identifier
c) [TypeExpression]
_ -> Identifier
c forall a. Eq a => a -> a -> Bool
== Identifier
ident
      TypeExpression
otherwise         -> Bool
False



-- | Checks that the names of class methods are pairwise distinct.
--   If not, an error message is created.

checkClassMethodsDistinct :: [Identifier] -> ErrorOr ()
checkClassMethodsDistinct :: [Identifier] -> ErrorOr ()
checkClassMethodsDistinct [Identifier]
is =
  let es :: [Identifier]
es = forall a. Ord a => [a] -> [a]
extractRepeatingElements [Identifier]
is
   in Bool -> Doc -> ErrorOr ()
errorIf (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Identifier]
es) forall a b. (a -> b) -> a -> b
$
        String -> Doc
pp (String
"Class methods must not be declared more than once. "
            forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
violating String
"class method" (forall a b. (a -> b) -> [a] -> [b]
map Identifier -> String
unpackIdent [Identifier]
es))



-- | Checks if the given identifier occurs as free type variable in every
--   signature. If not, an error message is created.

checkClassVarInMethods :: TypeVariable -> [Signature] -> ErrorOr ()
checkClassVarInMethods :: TypeVariable -> [Signature] -> ErrorOr ()
checkClassVarInMethods v :: TypeVariable
v@(TV Identifier
vName) [Signature]
ss =
  let setOfv :: Set TypeVariable
setOfv      = forall a. a -> Set a
Set.singleton TypeVariable
v
      vIsFreeIn :: TypeExpression -> Bool
vIsFreeIn TypeExpression
t = Set TypeVariable
setOfv forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` TypeExpression -> Set TypeVariable
freeTypeVariables TypeExpression
t
      ms :: [Signature]
ms          = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeExpression -> Bool
vIsFreeIn forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature -> TypeExpression
signatureType) [Signature]
ss
   in Bool -> Doc -> ErrorOr ()
errorIf (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Signature]
ms) forall a b. (a -> b) -> a -> b
$
        String -> Doc
pp (String
"The type variable `" forall a. [a] -> [a] -> [a]
++ Identifier -> String
unpackIdent Identifier
vName forall a. [a] -> [a] -> [a]
++ String
"' must occur free "
            forall a. [a] -> [a] -> [a]
++ String
"in the type expressions of every class method. "
            forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
violating String
"class method" (forall a b. (a -> b) -> [a] -> [b]
map (Identifier -> String
unpackIdent forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature -> Identifier
signatureName) [Signature]
ms))
    


-- | Checks that the name of a type class does not occur in any of the class
--   methods. Otherwise, an error message is created.
checkClassDeclNotRecursive :: Identifier -> [Signature] -> ErrorOr ()
checkClassDeclNotRecursive :: Identifier -> [Signature] -> ErrorOr ()
checkClassDeclNotRecursive Identifier
ident [Signature]
sigs =
  let hasThisClass :: TypeExpression -> Bool
hasThisClass = forall a b. (Data a, Data b) => (a -> Bool) -> b -> Bool
satisfiesSomewhere (\TypeClass
c -> TypeClass
c forall a. Eq a => a -> a -> Bool
== Identifier -> TypeClass
TC Identifier
ident)
      ms :: [Signature]
ms           = forall a. (a -> Bool) -> [a] -> [a]
filter (TypeExpression -> Bool
hasThisClass forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature -> TypeExpression
signatureType) [Signature]
sigs
   in Bool -> Doc -> ErrorOr ()
errorIf (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Signature]
ms) forall a b. (a -> b) -> a -> b
$
        String -> Doc
pp (String
"The type class `" forall a. [a] -> [a] -> [a]
++ Identifier -> String
unpackIdent Identifier
ident forall a. [a] -> [a] -> [a]
++ String
"' must not occur in a "
            forall a. [a] -> [a] -> [a]
++ String
"type expression of any class method of this class. "
            forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
violating String
"class method" (forall a b. (a -> b) -> [a] -> [b]
map (Identifier -> String
unpackIdent forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature -> Identifier
signatureName) [Signature]
ms))



-- | Checks that no FixedTypeExpression occurs in the given list of named
--   type expressions. The first argument is used in generating a helpful error
--   message and describes what kind of items the second argument contains.

checkNoFixedTEsNamed :: String -> (Identifier, [TypeExpression]) -> ErrorOr ()
checkNoFixedTEsNamed :: String -> (Identifier, [TypeExpression]) -> ErrorOr ()
checkNoFixedTEsNamed String
tag (Identifier
con, [TypeExpression]
ts) =
  let es :: [String]
es = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TypeExpression -> Maybe String
checkNoFixedTEsPlain [TypeExpression]
ts
   in Bool -> Doc -> ErrorOr ()
errorIf (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ [String]
es) forall a b. (a -> b) -> a -> b
$
        String -> Doc
pp (forall a. [a] -> a
head [String]
es forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
violating String
tag [Identifier -> String
unpackIdent Identifier
con])



-- | Checks that no FixedTypeExpression occurs in a type expression.
--   If it does, an error message is created.

checkNoFixedTEs :: TypeExpression -> ErrorOr ()
checkNoFixedTEs :: TypeExpression -> ErrorOr ()
checkNoFixedTEs TypeExpression
t = 
  let e :: Maybe String
e = TypeExpression -> Maybe String
checkNoFixedTEsPlain TypeExpression
t
   in Bool -> Doc -> ErrorOr ()
errorIf (forall a. Maybe a -> Bool
isJust Maybe String
e) (String -> Doc
pp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ Maybe String
e)
  


-- | Returns an error if a FixedTypeExpression occurs in the argument, otherwise
--   returns @Nothing@.

checkNoFixedTEsPlain :: TypeExpression -> Maybe String
checkNoFixedTEsPlain :: TypeExpression -> Maybe String
checkNoFixedTEsPlain TypeExpression
t =
  if (forall a b. (Data a, Data b) => (a -> Bool) -> b -> Bool
satisfiesSomewhere TypeExpression -> Bool
isFixedTE TypeExpression
t)
    then forall a. a -> Maybe a
Just String
"A fixed type expression must not occur in a type expression."
    else forall a. Maybe a
Nothing
  where
    isFixedTE :: TypeExpression -> Bool
isFixedTE TypeExpression
t = case TypeExpression
t of
      TypeExp FixedTypeExpression
_ -> Bool
True
      TypeExpression
otherwise -> Bool
False



-- | Checks that no function type constructor and no type abstraction
--   constructor occur in the given named list of type expressions.

checkAbsFun :: (Identifier, [TypeExpression]) -> ErrorOr ()
checkAbsFun :: (Identifier, [TypeExpression]) -> ErrorOr ()
checkAbsFun (Identifier
con, [TypeExpression]
ts) =
  Bool -> Doc -> ErrorOr ()
errorIf (forall a b. (Data a, Data b) => (a -> Bool) -> b -> Bool
satisfiesSomewhere TypeExpression -> Bool
isAbsOrFun [TypeExpression]
ts) forall a b. (a -> b) -> a -> b
$
    String -> Doc
pp (String
"Algebraic data types and type renamings must be declared without type "
        forall a. [a] -> [a] -> [a]
++ String
"abstractions and function type constructors occurring on the "
        forall a. [a] -> [a] -> [a]
++ String
"right-hand side."
        forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
violating String
"data constructor" [Identifier -> String
unpackIdent Identifier
con])
  where
    isAbsOrFun :: TypeExpression -> Bool
isAbsOrFun TypeExpression
t = case TypeExpression
t of
      TypeFun TypeExpression
_ TypeExpression
_   -> Bool
True
      TypeAbs TypeVariable
_ [TypeClass]
_ TypeExpression
_ -> Bool
True
      TypeExpression
otherwise     -> Bool
False





------- Helper functions ------------------------------------------------------


-- | Applies two functions to a value and creates a pair of the results.

makePair :: (a -> b) -> (a -> c) -> a -> (b, c)
makePair :: forall a b c. (a -> b) -> (a -> c) -> a -> (b, c)
makePair a -> b
f a -> c
g a
x = (a -> b
f a
x, a -> c
g a
x)


-- | Creates a list containing just one element.

singletonList :: a -> [a]
singletonList :: forall a. a -> [a]
singletonList a
x = [a
x]



-- | Filters all elements which occur more than once in the given list.
--   Only one representative is returned for every group of equal items.

extractRepeatingElements :: Ord a => [a] -> [a]
extractRepeatingElements :: forall a. Ord a => [a] -> [a]
extractRepeatingElements =
  forall a b. (a -> b) -> [a] -> [b]
map forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (\[a]
vs -> forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
vs forall a. Ord a => a -> a -> Bool
> Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [[a]]
group forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
sort



-- | Tests if a predicate holds somewhere in an arbitrary tree.

satisfiesSomewhere :: (Data a, Data b) => (a -> Bool) -> b -> Bool
satisfiesSomewhere :: forall a b. (Data a, Data b) => (a -> Bool) -> b -> Bool
satisfiesSomewhere a -> Bool
predicate b
x = forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything Bool -> Bool -> Bool
(||) (Bool
False forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
`mkQ` a -> Bool
predicate) b
x