{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./DFOL/Sign.hs
Description :  Definition of signatures for first-order logic
               with dependent types (DFOL)
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}

module DFOL.Sign
   ( KIND (..)
   , ARITY
   , CONTEXT (..)
   , Sign (..)
   , emptyContext
   , addVarDecl
   , getVars
   , getVarType
   , emptySig
   , addSymbolDecl
   , getSymbols
   , isConstant
   , getSymbolType
   , getSymbolKind
   , getSymbolArity
   , getSymbolsByKind
   , getArgumentTypes
   , getReturnType
   , getArgumentNames
   , sigUnion
   , sigIntersection
   , isValidDecl
   , isValidVarDecl
   , getTermType
   , hasType
   , isValidType
   , getSymsOfType
   ) where

import DFOL.Utils
import DFOL.AS_DFOL

import Common.Id
import Common.Doc
import Common.DocUtils
import qualified Common.Result as Result

import Data.Data
import qualified Data.Set as Set
import qualified Data.Map as Map

-- symbol kinds
data KIND = SortKind
          | FuncKind
          | PredKind
            deriving (Int -> KIND -> ShowS
[KIND] -> ShowS
KIND -> String
(Int -> KIND -> ShowS)
-> (KIND -> String) -> ([KIND] -> ShowS) -> Show KIND
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [KIND] -> ShowS
$cshowList :: [KIND] -> ShowS
show :: KIND -> String
$cshow :: KIND -> String
showsPrec :: Int -> KIND -> ShowS
$cshowsPrec :: Int -> KIND -> ShowS
Show, Eq KIND
Eq KIND =>
(KIND -> KIND -> Ordering)
-> (KIND -> KIND -> Bool)
-> (KIND -> KIND -> Bool)
-> (KIND -> KIND -> Bool)
-> (KIND -> KIND -> Bool)
-> (KIND -> KIND -> KIND)
-> (KIND -> KIND -> KIND)
-> Ord KIND
KIND -> KIND -> Bool
KIND -> KIND -> Ordering
KIND -> KIND -> KIND
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 :: KIND -> KIND -> KIND
$cmin :: KIND -> KIND -> KIND
max :: KIND -> KIND -> KIND
$cmax :: KIND -> KIND -> KIND
>= :: KIND -> KIND -> Bool
$c>= :: KIND -> KIND -> Bool
> :: KIND -> KIND -> Bool
$c> :: KIND -> KIND -> Bool
<= :: KIND -> KIND -> Bool
$c<= :: KIND -> KIND -> Bool
< :: KIND -> KIND -> Bool
$c< :: KIND -> KIND -> Bool
compare :: KIND -> KIND -> Ordering
$ccompare :: KIND -> KIND -> Ordering
$cp1Ord :: Eq KIND
Ord, KIND -> KIND -> Bool
(KIND -> KIND -> Bool) -> (KIND -> KIND -> Bool) -> Eq KIND
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: KIND -> KIND -> Bool
$c/= :: KIND -> KIND -> Bool
== :: KIND -> KIND -> Bool
$c== :: KIND -> KIND -> Bool
Eq, Typeable, Typeable KIND
Constr
DataType
Typeable KIND =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> KIND -> c KIND)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c KIND)
-> (KIND -> Constr)
-> (KIND -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c KIND))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KIND))
-> ((forall b. Data b => b -> b) -> KIND -> KIND)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KIND -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KIND -> r)
-> (forall u. (forall d. Data d => d -> u) -> KIND -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> KIND -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> KIND -> m KIND)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KIND -> m KIND)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KIND -> m KIND)
-> Data KIND
KIND -> Constr
KIND -> DataType
(forall b. Data b => b -> b) -> KIND -> KIND
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KIND -> c KIND
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KIND
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) -> KIND -> u
forall u. (forall d. Data d => d -> u) -> KIND -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KIND -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KIND -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KIND -> m KIND
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KIND -> m KIND
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KIND
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KIND -> c KIND
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KIND)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KIND)
$cPredKind :: Constr
$cFuncKind :: Constr
$cSortKind :: Constr
$tKIND :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> KIND -> m KIND
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KIND -> m KIND
gmapMp :: (forall d. Data d => d -> m d) -> KIND -> m KIND
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KIND -> m KIND
gmapM :: (forall d. Data d => d -> m d) -> KIND -> m KIND
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KIND -> m KIND
gmapQi :: Int -> (forall d. Data d => d -> u) -> KIND -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KIND -> u
gmapQ :: (forall d. Data d => d -> u) -> KIND -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> KIND -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KIND -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KIND -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KIND -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KIND -> r
gmapT :: (forall b. Data b => b -> b) -> KIND -> KIND
$cgmapT :: (forall b. Data b => b -> b) -> KIND -> KIND
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KIND)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KIND)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c KIND)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KIND)
dataTypeOf :: KIND -> DataType
$cdataTypeOf :: KIND -> DataType
toConstr :: KIND -> Constr
$ctoConstr :: KIND -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KIND
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KIND
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KIND -> c KIND
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KIND -> c KIND
$cp1Data :: Typeable KIND
Data)

type ARITY = Int

-- contexts for DFOL
data CONTEXT = Context [DECL]
               deriving (Int -> CONTEXT -> ShowS
[CONTEXT] -> ShowS
CONTEXT -> String
(Int -> CONTEXT -> ShowS)
-> (CONTEXT -> String) -> ([CONTEXT] -> ShowS) -> Show CONTEXT
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CONTEXT] -> ShowS
$cshowList :: [CONTEXT] -> ShowS
show :: CONTEXT -> String
$cshow :: CONTEXT -> String
showsPrec :: Int -> CONTEXT -> ShowS
$cshowsPrec :: Int -> CONTEXT -> ShowS
Show, CONTEXT -> CONTEXT -> Bool
(CONTEXT -> CONTEXT -> Bool)
-> (CONTEXT -> CONTEXT -> Bool) -> Eq CONTEXT
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CONTEXT -> CONTEXT -> Bool
$c/= :: CONTEXT -> CONTEXT -> Bool
== :: CONTEXT -> CONTEXT -> Bool
$c== :: CONTEXT -> CONTEXT -> Bool
Eq, Typeable, Typeable CONTEXT
Constr
DataType
Typeable CONTEXT =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CONTEXT -> c CONTEXT)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CONTEXT)
-> (CONTEXT -> Constr)
-> (CONTEXT -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CONTEXT))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CONTEXT))
-> ((forall b. Data b => b -> b) -> CONTEXT -> CONTEXT)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CONTEXT -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CONTEXT -> r)
-> (forall u. (forall d. Data d => d -> u) -> CONTEXT -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> CONTEXT -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CONTEXT -> m CONTEXT)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CONTEXT -> m CONTEXT)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CONTEXT -> m CONTEXT)
-> Data CONTEXT
CONTEXT -> Constr
CONTEXT -> DataType
(forall b. Data b => b -> b) -> CONTEXT -> CONTEXT
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CONTEXT -> c CONTEXT
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CONTEXT
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) -> CONTEXT -> u
forall u. (forall d. Data d => d -> u) -> CONTEXT -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CONTEXT -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CONTEXT -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CONTEXT -> m CONTEXT
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CONTEXT -> m CONTEXT
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CONTEXT
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CONTEXT -> c CONTEXT
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CONTEXT)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CONTEXT)
$cContext :: Constr
$tCONTEXT :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CONTEXT -> m CONTEXT
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CONTEXT -> m CONTEXT
gmapMp :: (forall d. Data d => d -> m d) -> CONTEXT -> m CONTEXT
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CONTEXT -> m CONTEXT
gmapM :: (forall d. Data d => d -> m d) -> CONTEXT -> m CONTEXT
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CONTEXT -> m CONTEXT
gmapQi :: Int -> (forall d. Data d => d -> u) -> CONTEXT -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CONTEXT -> u
gmapQ :: (forall d. Data d => d -> u) -> CONTEXT -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CONTEXT -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CONTEXT -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CONTEXT -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CONTEXT -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CONTEXT -> r
gmapT :: (forall b. Data b => b -> b) -> CONTEXT -> CONTEXT
$cgmapT :: (forall b. Data b => b -> b) -> CONTEXT -> CONTEXT
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CONTEXT)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CONTEXT)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CONTEXT)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CONTEXT)
dataTypeOf :: CONTEXT -> DataType
$cdataTypeOf :: CONTEXT -> DataType
toConstr :: CONTEXT -> Constr
$ctoConstr :: CONTEXT -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CONTEXT
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CONTEXT
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CONTEXT -> c CONTEXT
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CONTEXT -> c CONTEXT
$cp1Data :: Typeable CONTEXT
Data)

-- the empty context
emptyContext :: CONTEXT
emptyContext :: CONTEXT
emptyContext = [DECL] -> CONTEXT
Context []

-- adds a variable declaration to the context
addVarDecl :: DECL -> CONTEXT -> CONTEXT
addVarDecl :: DECL -> CONTEXT -> CONTEXT
addVarDecl d :: DECL
d (Context ds :: [DECL]
ds) = [DECL] -> CONTEXT
Context ([DECL]
ds [DECL] -> [DECL] -> [DECL]
forall a. [a] -> [a] -> [a]
++ [DECL
d])

-- get the list of declared variables
getVars :: CONTEXT -> Set.Set NAME
getVars :: CONTEXT -> Set NAME
getVars (Context ds :: [DECL]
ds) = [NAME] -> Set NAME
forall a. Ord a => [a] -> Set a
Set.fromList ([NAME] -> Set NAME) -> [NAME] -> Set NAME
forall a b. (a -> b) -> a -> b
$ [DECL] -> [NAME]
getVarsFromDecls [DECL]
ds

-- get the variable type
getVarType :: NAME -> CONTEXT -> Maybe TYPE
getVarType :: NAME -> CONTEXT -> Maybe TYPE
getVarType n :: NAME
n (Context ds :: [DECL]
ds) = NAME -> [DECL] -> Maybe TYPE
getVarTypeFromDecls NAME
n [DECL]
ds

-- signatures for DFOL
data Sign = Sign [DECL]
            deriving (Int -> Sign -> ShowS
[Sign] -> ShowS
Sign -> String
(Int -> Sign -> ShowS)
-> (Sign -> String) -> ([Sign] -> ShowS) -> Show Sign
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sign] -> ShowS
$cshowList :: [Sign] -> ShowS
show :: Sign -> String
$cshow :: Sign -> String
showsPrec :: Int -> Sign -> ShowS
$cshowsPrec :: Int -> Sign -> ShowS
Show, Eq Sign
Eq Sign =>
(Sign -> Sign -> Ordering)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Sign)
-> (Sign -> Sign -> Sign)
-> Ord Sign
Sign -> Sign -> Bool
Sign -> Sign -> Ordering
Sign -> Sign -> Sign
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 :: Sign -> Sign -> Sign
$cmin :: Sign -> Sign -> Sign
max :: Sign -> Sign -> Sign
$cmax :: Sign -> Sign -> Sign
>= :: Sign -> Sign -> Bool
$c>= :: Sign -> Sign -> Bool
> :: Sign -> Sign -> Bool
$c> :: Sign -> Sign -> Bool
<= :: Sign -> Sign -> Bool
$c<= :: Sign -> Sign -> Bool
< :: Sign -> Sign -> Bool
$c< :: Sign -> Sign -> Bool
compare :: Sign -> Sign -> Ordering
$ccompare :: Sign -> Sign -> Ordering
$cp1Ord :: Eq Sign
Ord, Sign -> Sign -> Bool
(Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> Eq Sign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sign -> Sign -> Bool
$c/= :: Sign -> Sign -> Bool
== :: Sign -> Sign -> Bool
$c== :: Sign -> Sign -> Bool
Eq, Typeable, Typeable Sign
Constr
DataType
Typeable Sign =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Sign -> c Sign)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Sign)
-> (Sign -> Constr)
-> (Sign -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Sign))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign))
-> ((forall b. Data b => b -> b) -> Sign -> Sign)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sign -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sign -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Sign -> m Sign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sign -> m Sign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sign -> m Sign)
-> Data Sign
Sign -> Constr
Sign -> DataType
(forall b. Data b => b -> b) -> Sign -> Sign
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
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) -> Sign -> u
forall u. (forall d. Data d => d -> u) -> Sign -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sign)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)
$cSign :: Constr
$tSign :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Sign -> m Sign
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
gmapMp :: (forall d. Data d => d -> m d) -> Sign -> m Sign
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
gmapM :: (forall d. Data d => d -> m d) -> Sign -> m Sign
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sign -> m Sign
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sign -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sign -> u
gmapQ :: (forall d. Data d => d -> u) -> Sign -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sign -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r
gmapT :: (forall b. Data b => b -> b) -> Sign -> Sign
$cgmapT :: (forall b. Data b => b -> b) -> Sign -> Sign
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sign)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sign)
dataTypeOf :: Sign -> DataType
$cdataTypeOf :: Sign -> DataType
toConstr :: Sign -> Constr
$ctoConstr :: Sign -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sign
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sign -> c Sign
$cp1Data :: Typeable Sign
Data)

-- the empty signature
emptySig :: Sign
emptySig :: Sign
emptySig = [DECL] -> Sign
Sign []

-- adds a symbol declaration to the signature
addSymbolDecl :: DECL -> Sign -> Sign
addSymbolDecl :: DECL -> Sign -> Sign
addSymbolDecl d :: DECL
d (Sign ds :: [DECL]
ds) = [DECL] -> Sign
Sign ([DECL]
ds [DECL] -> [DECL] -> [DECL]
forall a. [a] -> [a] -> [a]
++ [DECL
d])

-- get the set of defined symbols
getSymbols :: Sign -> Set.Set NAME
getSymbols :: Sign -> Set NAME
getSymbols (Sign ds :: [DECL]
ds) = [NAME] -> Set NAME
forall a. Ord a => [a] -> Set a
Set.fromList ([NAME] -> Set NAME) -> [NAME] -> Set NAME
forall a b. (a -> b) -> a -> b
$ [DECL] -> [NAME]
getVarsFromDecls [DECL]
ds

-- checks if the symbol is defined in the signature
isConstant :: NAME -> Sign -> Bool
isConstant :: NAME -> Sign -> Bool
isConstant n :: NAME
n sig :: Sign
sig = NAME -> Set NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member NAME
n (Set NAME -> Bool) -> Set NAME -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set NAME
getSymbols Sign
sig

-- get the symbol type
getSymbolType :: NAME -> Sign -> Maybe TYPE
getSymbolType :: NAME -> Sign -> Maybe TYPE
getSymbolType n :: NAME
n (Sign ds :: [DECL]
ds) = NAME -> [DECL] -> Maybe TYPE
getVarTypeFromDecls NAME
n [DECL]
ds

-- get the symbol kind
getSymbolKind :: NAME -> Sign -> Maybe KIND
getSymbolKind :: NAME -> Sign -> Maybe KIND
getSymbolKind n :: NAME
n sig :: Sign
sig = case NAME -> Sign -> Maybe TYPE
getReturnType NAME
n Sign
sig of
                           Nothing -> Maybe KIND
forall a. Maybe a
Nothing
                           Just Sort -> KIND -> Maybe KIND
forall a. a -> Maybe a
Just KIND
SortKind
                           Just Form -> KIND -> Maybe KIND
forall a. a -> Maybe a
Just KIND
PredKind
                           Just _ -> KIND -> Maybe KIND
forall a. a -> Maybe a
Just KIND
FuncKind

-- get the symbol arity
getSymbolArity :: NAME -> Sign -> Maybe ARITY
getSymbolArity :: NAME -> Sign -> Maybe Int
getSymbolArity n :: NAME
n sig :: Sign
sig = case NAME -> Sign -> Maybe [TYPE]
getArgumentTypes NAME
n Sign
sig of
                            Nothing -> Maybe Int
forall a. Maybe a
Nothing
                            Just ts :: [TYPE]
ts -> Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ [TYPE] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TYPE]
ts

-- get a list of symbols of the given kind
getSymbolsByKind :: Sign -> KIND -> Set.Set NAME
getSymbolsByKind :: Sign -> KIND -> Set NAME
getSymbolsByKind sig :: Sign
sig kind :: KIND
kind =
   (NAME -> Bool) -> Set NAME -> Set NAME
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ n :: NAME
n -> NAME -> Sign -> Maybe KIND
getSymbolKind NAME
n Sign
sig Maybe KIND -> Maybe KIND -> Bool
forall a. Eq a => a -> a -> Bool
== KIND -> Maybe KIND
forall a. a -> Maybe a
Just KIND
kind) (Set NAME -> Set NAME) -> Set NAME -> Set NAME
forall a b. (a -> b) -> a -> b
$ Sign -> Set NAME
getSymbols Sign
sig

-- get the list of types of the arguments of the given symbol
getArgumentTypes :: NAME -> Sign -> Maybe [TYPE]
getArgumentTypes :: NAME -> Sign -> Maybe [TYPE]
getArgumentTypes n :: NAME
n sig :: Sign
sig = case Maybe TYPE
typM of
                              Nothing -> Maybe [TYPE]
forall a. Maybe a
Nothing
                              Just typ :: TYPE
typ -> [TYPE] -> Maybe [TYPE]
forall a. a -> Maybe a
Just ([TYPE] -> Maybe [TYPE]) -> [TYPE] -> Maybe [TYPE]
forall a b. (a -> b) -> a -> b
$ TYPE -> [TYPE]
getArgumentTypesH TYPE
typ
                         where typM :: Maybe TYPE
typM = NAME -> Sign -> Maybe TYPE
getSymbolType NAME
n Sign
sig

getArgumentTypesH :: TYPE -> [TYPE]
getArgumentTypesH :: TYPE -> [TYPE]
getArgumentTypesH (Pi ds :: [DECL]
ds t :: TYPE
t) =
  [TYPE]
types1 [TYPE] -> [TYPE] -> [TYPE]
forall a. [a] -> [a] -> [a]
++ [TYPE]
types2
  where types1 :: [TYPE]
types1 = (DECL -> [TYPE]) -> [DECL] -> [TYPE]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (ns :: [NAME]
ns, t1 :: TYPE
t1) -> Int -> TYPE -> [TYPE]
forall a. Int -> a -> [a]
replicate ([NAME] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NAME]
ns) TYPE
t1) [DECL]
ds
        types2 :: [TYPE]
types2 = TYPE -> [TYPE]
getArgumentTypesH TYPE
t
getArgumentTypesH (Func ts :: [TYPE]
ts t :: TYPE
t) = [TYPE]
ts [TYPE] -> [TYPE] -> [TYPE]
forall a. [a] -> [a] -> [a]
++ TYPE -> [TYPE]
getArgumentTypesH TYPE
t
getArgumentTypesH _ = []

-- get the return type of a symbol with the given type
getReturnType :: NAME -> Sign -> Maybe TYPE
getReturnType :: NAME -> Sign -> Maybe TYPE
getReturnType n :: NAME
n sig :: Sign
sig = case Maybe TYPE
typM of
                           Nothing -> Maybe TYPE
forall a. Maybe a
Nothing
                           Just typ :: TYPE
typ -> TYPE -> Maybe TYPE
forall a. a -> Maybe a
Just (TYPE -> Maybe TYPE) -> TYPE -> Maybe TYPE
forall a b. (a -> b) -> a -> b
$ TYPE -> TYPE
getReturnTypeH TYPE
typ
                      where typM :: Maybe TYPE
typM = NAME -> Sign -> Maybe TYPE
getSymbolType NAME
n Sign
sig

getReturnTypeH :: TYPE -> TYPE
getReturnTypeH :: TYPE -> TYPE
getReturnTypeH (Pi _ t :: TYPE
t) = TYPE -> TYPE
getReturnTypeH TYPE
t
getReturnTypeH (Func _ t :: TYPE
t) = TYPE -> TYPE
getReturnTypeH TYPE
t
getReturnTypeH t :: TYPE
t = TYPE
t

-- get the argument names
getArgumentNames :: NAME -> Sign -> Maybe [NAME]
getArgumentNames :: NAME -> Sign -> Maybe [NAME]
getArgumentNames n :: NAME
n sig :: Sign
sig =
  case Maybe TYPE
typM of
       Nothing -> Maybe [NAME]
forall a. Maybe a
Nothing
       Just typ :: TYPE
typ -> [NAME] -> Maybe [NAME]
forall a. a -> Maybe a
Just ([NAME] -> Maybe [NAME]) -> [NAME] -> Maybe [NAME]
forall a b. (a -> b) -> a -> b
$ [Maybe NAME] -> [NAME]
fillArgumentNames ([Maybe NAME] -> [NAME]) -> [Maybe NAME] -> [NAME]
forall a b. (a -> b) -> a -> b
$ TYPE -> [Maybe NAME]
getArgumentNamesH TYPE
typ
  where typM :: Maybe TYPE
typM = NAME -> Sign -> Maybe TYPE
getSymbolType NAME
n Sign
sig

getArgumentNamesH :: TYPE -> [Maybe NAME]
getArgumentNamesH :: TYPE -> [Maybe NAME]
getArgumentNamesH (Pi ds :: [DECL]
ds t :: TYPE
t) =
  (NAME -> Maybe NAME) -> [NAME] -> [Maybe NAME]
forall a b. (a -> b) -> [a] -> [b]
map NAME -> Maybe NAME
forall a. a -> Maybe a
Just ([DECL] -> [NAME]
getVarsFromDecls [DECL]
ds) [Maybe NAME] -> [Maybe NAME] -> [Maybe NAME]
forall a. [a] -> [a] -> [a]
++ TYPE -> [Maybe NAME]
getArgumentNamesH TYPE
t
getArgumentNamesH (Func ts :: [TYPE]
ts t :: TYPE
t) =
  Int -> Maybe NAME -> [Maybe NAME]
forall a. Int -> a -> [a]
replicate ([TYPE] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TYPE]
ts) Maybe NAME
forall a. Maybe a
Nothing [Maybe NAME] -> [Maybe NAME] -> [Maybe NAME]
forall a. [a] -> [a] -> [a]
++ TYPE -> [Maybe NAME]
getArgumentNamesH TYPE
t
getArgumentNamesH _ = []

fillArgumentNames :: [Maybe NAME] -> [NAME]
fillArgumentNames :: [Maybe NAME] -> [NAME]
fillArgumentNames ns :: [Maybe NAME]
ns = [Maybe NAME] -> Int -> [NAME]
fillArgumentNamesH [Maybe NAME]
ns 0

fillArgumentNamesH :: [Maybe NAME] -> Int -> [NAME]
fillArgumentNamesH :: [Maybe NAME] -> Int -> [NAME]
fillArgumentNamesH [] _ = []
fillArgumentNamesH (nameM :: Maybe NAME
nameM : namesM :: [Maybe NAME]
namesM) i :: Int
i =
  case Maybe NAME
nameM of
       Just name :: NAME
name -> NAME
name NAME -> [NAME] -> [NAME]
forall a. a -> [a] -> [a]
: [Maybe NAME] -> Int -> [NAME]
fillArgumentNamesH [Maybe NAME]
namesM Int
i
       Nothing -> String -> Range -> NAME
Token ("gen_x_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) Range
nullRange NAME -> [NAME] -> [NAME]
forall a. a -> [a] -> [a]
:
                  [Maybe NAME] -> Int -> [NAME]
fillArgumentNamesH [Maybe NAME]
namesM (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)

-- pretty printing
instance Pretty Sign where
   pretty :: Sign -> Doc
pretty = Sign -> Doc
printSig
instance Pretty CONTEXT where
   pretty :: CONTEXT -> Doc
pretty (Context xs :: [DECL]
xs) = [DECL] -> Doc
printDecls [DECL]
xs
instance Pretty KIND where
   pretty :: KIND -> Doc
pretty = KIND -> Doc
printKind

printSig :: Sign -> Doc
printSig :: Sign -> Doc
printSig (Sign []) = String -> Doc
text "EmptySig"
printSig (Sign ds :: [DECL]
ds) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (DECL -> Doc) -> [DECL] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map DECL -> Doc
printSigDecl ([DECL] -> [Doc]) -> [DECL] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [DECL] -> [DECL]
compactDecls [DECL]
ds

printSigDecl :: DECL -> Doc
printSigDecl :: DECL -> Doc
printSigDecl (ns :: [NAME]
ns, t :: TYPE
t) = [NAME] -> Doc
printNames [NAME]
ns Doc -> Doc -> Doc
<+> String -> Doc
text "::" Doc -> Doc -> Doc
<+> TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t

printKind :: KIND -> Doc
printKind :: KIND -> Doc
printKind SortKind = String -> Doc
text "sort"
printKind FuncKind = String -> Doc
text "func"
printKind PredKind = String -> Doc
text "pred"

{- Union of signatures. The union of two DFOL signatures Sig1 and Sig2 is
   defined as the smallest valid signature containing both Sig1 and Sig2 as
   subsignatures. It is not always defined, namely in the case when the original
   signatures give conflicting definitions for the same symbol. -}
sigUnion :: Sign -> Sign -> Result.Result Sign
sigUnion :: Sign -> Sign -> Result Sign
sigUnion sig :: Sign
sig (Sign ds :: [DECL]
ds) = [SDECL] -> Sign -> Result Sign
sigUnionH ([DECL] -> [SDECL]
expandDecls [DECL]
ds) Sign
sig

sigUnionH :: [SDECL] -> Sign -> Result.Result Sign
sigUnionH :: [SDECL] -> Sign -> Result Sign
sigUnionH [] sig :: Sign
sig = [Diagnosis] -> Maybe Sign -> Result Sign
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe Sign -> Result Sign) -> Maybe Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Maybe Sign
forall a. a -> Maybe a
Just Sign
sig
sigUnionH ((n :: NAME
n, t :: TYPE
t) : ds :: [SDECL]
ds) sig :: Sign
sig =
  if NAME -> Sign -> Bool
isConstant NAME
n Sign
sig
     then let Just t1 :: TYPE
t1 = NAME -> Sign -> Maybe TYPE
getSymbolType NAME
n Sign
sig
              in if TYPE
t TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
t1
                    then [SDECL] -> Sign -> Result Sign
sigUnionH [SDECL]
ds Sign
sig
                    else [Diagnosis] -> Maybe Sign -> Result Sign
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [NAME -> TYPE -> TYPE -> Diagnosis
incompatibleUnionError NAME
n TYPE
t TYPE
t1] Maybe Sign
forall a. Maybe a
Nothing
     else let t1 :: TYPE
t1 = Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
forall k a. Map k a
Map.empty (Sign -> Set NAME
getSymbols Sign
sig) TYPE
t
              sig1 :: Sign
sig1 = DECL -> Sign -> Sign
addSymbolDecl ([NAME
n], TYPE
t1) Sign
sig
              in [SDECL] -> Sign -> Result Sign
sigUnionH [SDECL]
ds Sign
sig1

{- Intersection of signatures. The intersection of two DFOL signatures Sig1 and
   Sig2 is defined as the largest valid signature contained both in Sig1 and
   Sig2 as a subsignature. It is always defined but may be the empty
   signature. -}
sigIntersection :: Sign -> Sign -> Result.Result Sign
sigIntersection :: Sign -> Sign -> Result Sign
sigIntersection (Sign ds :: [DECL]
ds) = [SDECL] -> Sign -> Sign -> Result Sign
sigIntersectionH ([DECL] -> [SDECL]
expandDecls [DECL]
ds) Sign
emptySig

sigIntersectionH :: [SDECL] -> Sign -> Sign -> Result.Result Sign
sigIntersectionH :: [SDECL] -> Sign -> Sign -> Result Sign
sigIntersectionH [] sig :: Sign
sig _ = [Diagnosis] -> Maybe Sign -> Result Sign
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe Sign -> Result Sign) -> Maybe Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Maybe Sign
forall a. a -> Maybe a
Just Sign
sig
sigIntersectionH ((n :: NAME
n, t :: TYPE
t) : ds :: [SDECL]
ds) sig :: Sign
sig sig2 :: Sign
sig2 =
  let present :: Bool
present = NAME -> Sign -> Bool
isConstant NAME
n Sign
sig2
                Bool -> Bool -> Bool
&& let Just t1 :: TYPE
t1 = NAME -> Sign -> Maybe TYPE
getSymbolType NAME
n Sign
sig2
                   in TYPE
t TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
t1
      Diagn _ valid :: Bool
valid = DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidDecl ([NAME
n], TYPE
t) Sign
sig CONTEXT
emptyContext
      in if Bool
present Bool -> Bool -> Bool
&& Bool
valid
            then let sig1 :: Sign
sig1 = DECL -> Sign -> Sign
addSymbolDecl ([NAME
n], TYPE
t) Sign
sig
                     in [SDECL] -> Sign -> Sign -> Result Sign
sigIntersectionH [SDECL]
ds Sign
sig1 Sign
sig2
            else [SDECL] -> Sign -> Sign -> Result Sign
sigIntersectionH [SDECL]
ds Sign
sig Sign
sig2

-- determines whether a declaration is valid w.r.t. a signature and a context
isValidDecl :: DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidDecl :: DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidDecl (ns :: [NAME]
ns, t :: TYPE
t) sig :: Sign
sig cont :: CONTEXT
cont = [DIAGN Bool] -> DIAGN Bool
andD [DIAGN Bool
validNames, DIAGN Bool
validType]
                              where validNames :: DIAGN Bool
validNames = [NAME] -> Sign -> CONTEXT -> DIAGN Bool
areValidNames [NAME]
ns Sign
sig CONTEXT
cont
                                    validType :: DIAGN Bool
validType = TYPE -> Sign -> CONTEXT -> DIAGN Bool
isValidType TYPE
t Sign
sig CONTEXT
cont

-- checks if a variable declaration is valid w.r.t. a signature and a context
isValidVarDecl :: DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidVarDecl :: DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidVarDecl d :: DECL
d@(_, t :: TYPE
t) sig :: Sign
sig cont :: CONTEXT
cont = [DIAGN Bool] -> DIAGN Bool
andD [DIAGN Bool
discourseType, DIAGN Bool
validDec]
                                  where discourseType :: DIAGN Bool
discourseType = TYPE -> DIAGN Bool
isDiscourseType TYPE
t
                                        validDec :: DIAGN Bool
validDec = DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidDecl DECL
d Sign
sig CONTEXT
cont

{- checks if a list of names in a declaration is valid w.r.t. a signature
   and a context -}
areValidNames :: [NAME] -> Sign -> CONTEXT -> DIAGN Bool
areValidNames :: [NAME] -> Sign -> CONTEXT -> DIAGN Bool
areValidNames names :: [NAME]
names sig :: Sign
sig cont :: CONTEXT
cont =
   if Set NAME -> Bool
forall a. Set a -> Bool
Set.null Set NAME
overlap
      then [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [] Bool
True
      else [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [Set NAME -> CONTEXT -> Diagnosis
redeclaredNamesError Set NAME
overlap CONTEXT
cont] Bool
False
   where declaredSyms :: Set NAME
declaredSyms = Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign -> Set NAME
getSymbols Sign
sig) (CONTEXT -> Set NAME
getVars CONTEXT
cont)
         newSyms :: Set NAME
newSyms = [NAME] -> Set NAME
forall a. Ord a => [a] -> Set a
Set.fromList [NAME]
names
         overlap :: Set NAME
overlap = Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set NAME
newSyms Set NAME
declaredSyms

-- determines whether a type is valid w.r.t. a signature and a context
isValidType :: TYPE -> Sign -> CONTEXT -> DIAGN Bool
isValidType :: TYPE -> Sign -> CONTEXT -> DIAGN Bool
isValidType Sort _ _ = [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [] Bool
True
isValidType Form _ _ = [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [] Bool
True
isValidType (Univ t :: TERM
t) sig :: Sign
sig cont :: CONTEXT
cont = TERM -> TYPE -> Sign -> CONTEXT -> DIAGN Bool
hasType TERM
t TYPE
Sort Sign
sig CONTEXT
cont
isValidType (Func ts :: [TYPE]
ts t :: TYPE
t) sig :: Sign
sig cont :: CONTEXT
cont =
   [DIAGN Bool] -> DIAGN Bool
andD [DIAGN Bool
validDoms, DIAGN Bool
validCod, DIAGN Bool
discourseDoms]
   where validDoms :: DIAGN Bool
validDoms = [DIAGN Bool] -> DIAGN Bool
andD ([DIAGN Bool] -> DIAGN Bool) -> [DIAGN Bool] -> DIAGN Bool
forall a b. (a -> b) -> a -> b
$ (TYPE -> DIAGN Bool) -> [TYPE] -> [DIAGN Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\ t1 :: TYPE
t1 -> TYPE -> Sign -> CONTEXT -> DIAGN Bool
isValidType TYPE
t1 Sign
sig CONTEXT
cont) [TYPE]
ts
         validCod :: DIAGN Bool
validCod = TYPE -> Sign -> CONTEXT -> DIAGN Bool
isValidType TYPE
t Sign
sig CONTEXT
cont
         discourseDoms :: DIAGN Bool
discourseDoms = [DIAGN Bool] -> DIAGN Bool
andD ([DIAGN Bool] -> DIAGN Bool) -> [DIAGN Bool] -> DIAGN Bool
forall a b. (a -> b) -> a -> b
$ (TYPE -> DIAGN Bool) -> [TYPE] -> [DIAGN Bool]
forall a b. (a -> b) -> [a] -> [b]
map TYPE -> DIAGN Bool
isDiscourseType [TYPE]
ts
isValidType (Pi [] t :: TYPE
t) sig :: Sign
sig cont :: CONTEXT
cont = TYPE -> Sign -> CONTEXT -> DIAGN Bool
isValidType TYPE
t Sign
sig CONTEXT
cont
isValidType (Pi (d :: DECL
d : ds :: [DECL]
ds) t :: TYPE
t) sig :: Sign
sig cont :: CONTEXT
cont =
   [DIAGN Bool] -> DIAGN Bool
andD [DIAGN Bool
validDecl, DIAGN Bool
validType]
   where validDecl :: DIAGN Bool
validDecl = DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidVarDecl DECL
d Sign
sig CONTEXT
cont
         validType :: DIAGN Bool
validType = TYPE -> Sign -> CONTEXT -> DIAGN Bool
isValidType ([DECL] -> TYPE -> TYPE
Pi [DECL]
ds TYPE
t) Sign
sig (DECL -> CONTEXT -> CONTEXT
addVarDecl DECL
d CONTEXT
cont)

-- determines whether a type starts with Univ
isDiscourseType :: TYPE -> DIAGN Bool
isDiscourseType :: TYPE -> DIAGN Bool
isDiscourseType t :: TYPE
t = case TYPE
t of
                         Univ _ -> [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [] Bool
True
                         _ -> [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [TYPE -> Diagnosis
noDiscourseTypeError TYPE
t] Bool
False

-- determines whether a term has the given type w.r.t. a signature and a context
hasType :: TERM -> TYPE -> Sign -> CONTEXT -> DIAGN Bool
hasType :: TERM -> TYPE -> Sign -> CONTEXT -> DIAGN Bool
hasType term :: TERM
term expectedType :: TYPE
expectedType sig :: Sign
sig cont :: CONTEXT
cont =
   case Maybe TYPE
inferredTypeM of
        Nothing -> [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [Diagnosis]
diag Bool
False
        Just inferredType :: TYPE
inferredType ->
           if TYPE
inferredType TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
expectedType
              then [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [] Bool
True
              else [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [TYPE -> TYPE -> TERM -> CONTEXT -> Diagnosis
wrongTypeError TYPE
expectedType TYPE
inferredType TERM
term CONTEXT
cont]
                         Bool
False
   where Result.Result diag :: [Diagnosis]
diag inferredTypeM :: Maybe TYPE
inferredTypeM = TERM -> Sign -> CONTEXT -> Result TYPE
getTermType TERM
term Sign
sig CONTEXT
cont

{- determines the type of a term w.r.t. a signature and a context
returns the type in recursive form, with bound variables different
   from signature constants -}
getTermType :: TERM -> Sign -> CONTEXT -> Result.Result TYPE
getTermType :: TERM -> Sign -> CONTEXT -> Result TYPE
getTermType term :: TERM
term = TERM -> Sign -> CONTEXT -> Result TYPE
getTermTypeH (TERM -> TERM
termRecForm TERM
term)

getTermTypeH :: TERM -> Sign -> CONTEXT -> Result.Result TYPE
getTermTypeH :: TERM -> Sign -> CONTEXT -> Result TYPE
getTermTypeH (Identifier n :: NAME
n) sig :: Sign
sig cont :: CONTEXT
cont =
   case Maybe TYPE
fromContext of
        Just _ -> [Diagnosis] -> Maybe TYPE -> Result TYPE
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] Maybe TYPE
fromContext
        Nothing -> case Maybe TYPE
fromSig of
                        Just type1 :: TYPE
type1 ->
                          let type2 :: TYPE
type2 = TYPE -> Sign -> CONTEXT -> TYPE
renameBoundVars (TYPE -> TYPE
typeRecForm TYPE
type1)
                                         Sign
sig CONTEXT
cont
                              in [Diagnosis] -> Maybe TYPE -> Result TYPE
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe TYPE -> Result TYPE) -> Maybe TYPE -> Result TYPE
forall a b. (a -> b) -> a -> b
$ TYPE -> Maybe TYPE
forall a. a -> Maybe a
Just TYPE
type2
                        Nothing ->
                          [Diagnosis] -> Maybe TYPE -> Result TYPE
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [NAME -> CONTEXT -> Diagnosis
unknownIdentifierError NAME
n CONTEXT
cont] Maybe TYPE
forall a. Maybe a
Nothing
   where fromSig :: Maybe TYPE
fromSig = NAME -> Sign -> Maybe TYPE
getSymbolType NAME
n Sign
sig
         fromContext :: Maybe TYPE
fromContext = NAME -> CONTEXT -> Maybe TYPE
getVarType NAME
n CONTEXT
cont
getTermTypeH (Appl f :: TERM
f [a :: TERM
a]) sig :: Sign
sig cont :: CONTEXT
cont =
   case Maybe TYPE
typeAM of
        Nothing -> [Diagnosis] -> Maybe TYPE -> Result TYPE
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Diagnosis]
diagA Maybe TYPE
forall a. Maybe a
Nothing
        Just typeA :: TYPE
typeA ->
          case Maybe TYPE
typeFM of
               Nothing -> [Diagnosis] -> Maybe TYPE -> Result TYPE
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Diagnosis]
diagF Maybe TYPE
forall a. Maybe a
Nothing
               Just (Func (dom :: TYPE
dom : doms :: [TYPE]
doms) cod :: TYPE
cod) ->
                 if TYPE
dom TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
typeA
                    then [Diagnosis] -> Maybe TYPE -> Result TYPE
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe TYPE -> Result TYPE) -> Maybe TYPE -> Result TYPE
forall a b. (a -> b) -> a -> b
$ TYPE -> Maybe TYPE
forall a. a -> Maybe a
Just (TYPE -> Maybe TYPE) -> TYPE -> Maybe TYPE
forall a b. (a -> b) -> a -> b
$ TYPE -> TYPE
typeRecForm
                            (TYPE -> TYPE) -> TYPE -> TYPE
forall a b. (a -> b) -> a -> b
$ [TYPE] -> TYPE -> TYPE
Func [TYPE]
doms TYPE
cod
                    else [Diagnosis] -> Maybe TYPE -> Result TYPE
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [TYPE -> TYPE -> TERM -> CONTEXT -> Diagnosis
wrongTypeError TYPE
dom TYPE
typeA TERM
a CONTEXT
cont] Maybe TYPE
forall a. Maybe a
Nothing
               Just (Pi [([x :: NAME
x], t :: TYPE
t)] typ :: TYPE
typ) ->
                 if TYPE
t TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
typeA
                    then [Diagnosis] -> Maybe TYPE -> Result TYPE
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe TYPE -> Result TYPE) -> Maybe TYPE -> Result TYPE
forall a b. (a -> b) -> a -> b
$ TYPE -> Maybe TYPE
forall a. a -> Maybe a
Just (TYPE -> Maybe TYPE) -> TYPE -> Maybe TYPE
forall a b. (a -> b) -> a -> b
$ NAME -> TERM -> TYPE -> TYPE
substitute NAME
x TERM
a TYPE
typ
                    else [Diagnosis] -> Maybe TYPE -> Result TYPE
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [TYPE -> TYPE -> TERM -> CONTEXT -> Diagnosis
wrongTypeError TYPE
t TYPE
typeA TERM
a CONTEXT
cont] Maybe TYPE
forall a. Maybe a
Nothing
               Just typeF :: TYPE
typeF ->
                 [Diagnosis] -> Maybe TYPE -> Result TYPE
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [TERM -> TYPE -> CONTEXT -> Diagnosis
noFunctionTermError TERM
f TYPE
typeF CONTEXT
cont] Maybe TYPE
forall a. Maybe a
Nothing
    where Result.Result diagF :: [Diagnosis]
diagF typeFM :: Maybe TYPE
typeFM = TERM -> Sign -> CONTEXT -> Result TYPE
getTermType TERM
f Sign
sig CONTEXT
cont
          Result.Result diagA :: [Diagnosis]
diagA typeAM :: Maybe TYPE
typeAM = TERM -> Sign -> CONTEXT -> Result TYPE
getTermType TERM
a Sign
sig CONTEXT
cont
getTermTypeH _ _ _ = [Diagnosis] -> Maybe TYPE -> Result TYPE
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] Maybe TYPE
forall a. Maybe a
Nothing

-- returns all symbols of the specified type
getSymsOfType :: Sign -> TYPE -> [NAME]
getSymsOfType :: Sign -> TYPE -> [NAME]
getSymsOfType (Sign ds :: [DECL]
ds) = [DECL] -> TYPE -> [NAME]
getSymsOfTypeH [DECL]
ds

getSymsOfTypeH :: [DECL] -> TYPE -> [NAME]
getSymsOfTypeH :: [DECL] -> TYPE -> [NAME]
getSymsOfTypeH [] _ = []
getSymsOfTypeH ((ns :: [NAME]
ns, t1 :: TYPE
t1) : ds :: [DECL]
ds) t :: TYPE
t =
  if TYPE
t1 TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
t
     then [NAME]
ns [NAME] -> [NAME] -> [NAME]
forall a. [a] -> [a] -> [a]
++ [DECL] -> TYPE -> [NAME]
getSymsOfTypeH [DECL]
ds TYPE
t
     else [DECL] -> TYPE -> [NAME]
getSymsOfTypeH [DECL]
ds TYPE
t

-- renames bound variables in a type to make it valid w.r.t. a sig and a context
renameBoundVars :: TYPE -> Sign -> CONTEXT -> TYPE
renameBoundVars :: TYPE -> Sign -> CONTEXT -> TYPE
renameBoundVars t :: TYPE
t sig :: Sign
sig cont :: CONTEXT
cont =
  let syms :: Set NAME
syms = Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign -> Set NAME
getSymbols Sign
sig) (CONTEXT -> Set NAME
getVars CONTEXT
cont)
      in Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
forall k a. Map k a
Map.empty Set NAME
syms TYPE
t

substitute :: NAME -> TERM -> TYPE -> TYPE
substitute :: NAME -> TERM -> TYPE -> TYPE
substitute n :: NAME
n val :: TERM
val = Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate (NAME -> TERM -> Map NAME TERM
forall k a. k -> a -> Map k a
Map.singleton NAME
n TERM
val) Set NAME
forall a. Set a
Set.empty

-- ERROR MESSAGES
redeclaredNamesError :: Set.Set NAME -> CONTEXT -> Result.Diagnosis
redeclaredNamesError :: Set NAME -> CONTEXT -> Diagnosis
redeclaredNamesError ns :: Set NAME
ns cont :: CONTEXT
cont =
  Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
    { diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
    , diagString :: String
Result.diagString = "Symbols or variables\n"
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show ([NAME] -> Doc
printNames ([NAME] -> Doc) -> [NAME] -> Doc
forall a b. (a -> b) -> a -> b
$ Set NAME -> [NAME]
forall a. Set a -> [a]
Set.toList Set NAME
ns)
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\ndeclared previously in the context\n"
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (CONTEXT -> Doc
forall a. Pretty a => a -> Doc
pretty CONTEXT
cont) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nor in the signature."
    , diagPos :: Range
Result.diagPos = Range
nullRange
    }

noFunctionTermError :: TERM -> TYPE -> CONTEXT -> Result.Diagnosis
noFunctionTermError :: TERM -> TYPE -> CONTEXT -> Diagnosis
noFunctionTermError term :: TERM
term t :: TYPE
t cont :: CONTEXT
cont =
  Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
    { diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
    , diagString :: String
Result.diagString = "Term\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TERM -> Doc
forall a. Pretty a => a -> Doc
pretty TERM
term)
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nhas the non-function type\n"
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t)
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nin the context\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (CONTEXT -> Doc
forall a. Pretty a => a -> Doc
pretty CONTEXT
cont)
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nand hence cannot be applied to an argument."
    , diagPos :: Range
Result.diagPos = Range
nullRange
    }

noDiscourseTypeError :: TYPE -> Result.Diagnosis
noDiscourseTypeError :: TYPE -> Diagnosis
noDiscourseTypeError t :: TYPE
t =
  Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
    { diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
    , diagString :: String
Result.diagString =
         "Type\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t)
         String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nis a non-discourse type (does not start with Univ) "
         String -> ShowS
forall a. [a] -> [a] -> [a]
++ "and hence cannot be used as a type of an argument."
    , diagPos :: Range
Result.diagPos = Range
nullRange
    }

wrongTypeError :: TYPE -> TYPE -> TERM -> CONTEXT -> Result.Diagnosis
wrongTypeError :: TYPE -> TYPE -> TERM -> CONTEXT -> Diagnosis
wrongTypeError type1 :: TYPE
type1 type2 :: TYPE
type2 term :: TERM
term cont :: CONTEXT
cont =
  Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
    { diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
    , diagString :: String
Result.diagString = "Term\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TERM -> Doc
forall a. Pretty a => a -> Doc
pretty TERM
term)
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nmust be of type "
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
type1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nbut is of type\n"
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
type2) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nin context\n"
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (CONTEXT -> Doc
forall a. Pretty a => a -> Doc
pretty CONTEXT
cont)
    , diagPos :: Range
Result.diagPos = Range
nullRange
    }

unknownIdentifierError :: NAME -> CONTEXT -> Result.Diagnosis
unknownIdentifierError :: NAME -> CONTEXT -> Diagnosis
unknownIdentifierError n :: NAME
n cont :: CONTEXT
cont =
  Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
    { diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
    , diagString :: String
Result.diagString = "Unknown identifier\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
n)
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nin the context\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (CONTEXT -> Doc
forall a. Pretty a => a -> Doc
pretty CONTEXT
cont)
    , diagPos :: Range
Result.diagPos = Range
nullRange
    }

incompatibleUnionError :: NAME -> TYPE -> TYPE -> Result.Diagnosis
incompatibleUnionError :: NAME -> TYPE -> TYPE -> Diagnosis
incompatibleUnionError n :: NAME
n t1 :: TYPE
t1 t2 :: TYPE
t2 =
  Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
    { diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
    , diagString :: String
Result.diagString = "Symbol\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
n)
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nmust have both type\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t1)
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nand type\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t2)
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nin the signature union and hence "
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "the union is not defined."
    , diagPos :: Range
Result.diagPos = Range
nullRange
    }