Sign.hs revision 1a38107941725211e7c3f051f7a8f5e12199f03a
{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module : $Header$
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 (Show, Ord, Eq, Typeable, Data)
type ARITY = Int
-- contexts for DFOL
data CONTEXT = Context [DECL]
deriving (Show, Eq, Typeable, Data)
-- the empty context
emptyContext :: CONTEXT
emptyContext = Context []
-- adds a variable declaration to the context
addVarDecl :: DECL -> CONTEXT -> CONTEXT
addVarDecl d (Context ds) = Context (ds ++ [d])
-- get the list of declared variables
getVars :: CONTEXT -> Set.Set NAME
getVars (Context ds) = Set.fromList $ getVarsFromDecls ds
-- get the variable type
getVarType :: NAME -> CONTEXT -> Maybe TYPE
getVarType n (Context ds) = getVarTypeFromDecls n ds
-- signatures for DFOL
data Sign = Sign [DECL]
deriving (Show, Ord, Eq, Typeable, Data)
-- the empty signature
emptySig :: Sign
emptySig = Sign []
-- adds a symbol declaration to the signature
addSymbolDecl :: DECL -> Sign -> Sign
addSymbolDecl d (Sign ds) = Sign (ds ++ [d])
-- get the set of defined symbols
getSymbols :: Sign -> Set.Set NAME
getSymbols (Sign ds) = Set.fromList $ getVarsFromDecls ds
-- checks if the symbol is defined in the signature
isConstant :: NAME -> Sign -> Bool
isConstant n sig = Set.member n $ getSymbols sig
-- get the symbol type
getSymbolType :: NAME -> Sign -> Maybe TYPE
getSymbolType n (Sign ds) = getVarTypeFromDecls n ds
-- get the symbol kind
getSymbolKind :: NAME -> Sign -> Maybe KIND
getSymbolKind n sig = case getReturnType n sig of
Nothing -> Nothing
Just Sort -> Just SortKind
Just Form -> Just PredKind
Just _ -> Just FuncKind
-- get the symbol arity
getSymbolArity :: NAME -> Sign -> Maybe ARITY
getSymbolArity n sig = case getArgumentTypes n sig of
Nothing -> Nothing
Just ts -> Just $ length ts
-- get a list of symbols of the given kind
getSymbolsByKind :: Sign -> KIND -> Set.Set NAME
getSymbolsByKind sig kind =
Set.filter (\ n -> getSymbolKind n sig == Just kind) $ getSymbols sig
-- get the list of types of the arguments of the given symbol
getArgumentTypes :: NAME -> Sign -> Maybe [TYPE]
getArgumentTypes n sig = case typM of
Nothing -> Nothing
Just typ -> Just $ getArgumentTypesH typ
where typM = getSymbolType n sig
getArgumentTypesH :: TYPE -> [TYPE]
getArgumentTypesH (Pi ds t) =
types1 ++ types2
where types1 = concatMap (\ (ns, t1) -> replicate (length ns) t1) ds
types2 = getArgumentTypesH t
getArgumentTypesH (Func ts t) = ts ++ getArgumentTypesH t
getArgumentTypesH _ = []
-- get the return type of a symbol with the given type
getReturnType :: NAME -> Sign -> Maybe TYPE
getReturnType n sig = case typM of
Nothing -> Nothing
Just typ -> Just $ getReturnTypeH typ
where typM = getSymbolType n sig
getReturnTypeH :: TYPE -> TYPE
getReturnTypeH (Pi _ t) = getReturnTypeH t
getReturnTypeH (Func _ t) = getReturnTypeH t
getReturnTypeH t = t
-- get the argument names
getArgumentNames :: NAME -> Sign -> Maybe [NAME]
getArgumentNames n sig =
case typM of
Nothing -> Nothing
Just typ -> Just $ fillArgumentNames $ getArgumentNamesH typ
where typM = getSymbolType n sig
getArgumentNamesH :: TYPE -> [Maybe NAME]
getArgumentNamesH (Pi ds t) =
map Just (getVarsFromDecls ds) ++ getArgumentNamesH t
getArgumentNamesH (Func ts t) =
replicate (length ts) Nothing ++ getArgumentNamesH t
getArgumentNamesH _ = []
fillArgumentNames :: [Maybe NAME] -> [NAME]
fillArgumentNames ns = fillArgumentNamesH ns 0
fillArgumentNamesH :: [Maybe NAME] -> Int -> [NAME]
fillArgumentNamesH [] _ = []
fillArgumentNamesH (nameM : namesM) i =
case nameM of
Just name -> name : fillArgumentNamesH namesM i
Nothing -> Token ("gen_x_" ++ show i) nullRange :
fillArgumentNamesH namesM (i + 1)
-- pretty printing
instance Pretty Sign where
pretty = printSig
instance Pretty CONTEXT where
pretty (Context xs) = printDecls xs
instance Pretty KIND where
pretty = printKind
printSig :: Sign -> Doc
printSig (Sign []) = text "EmptySig"
printSig (Sign ds) = vcat $ map printSigDecl $ compactDecls ds
printSigDecl :: DECL -> Doc
printSigDecl (ns, t) = printNames ns <+> text "::" <+> pretty t
printKind :: KIND -> Doc
printKind SortKind = text "sort"
printKind FuncKind = text "func"
printKind PredKind = 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 sig (Sign ds) = sigUnionH (expandDecls ds) sig
sigUnionH :: [SDECL] -> Sign -> Result.Result Sign
sigUnionH [] sig = Result.Result [] $ Just sig
sigUnionH ((n, t) : ds) sig =
if isConstant n sig
then let Just t1 = getSymbolType n sig
in if t == t1
then sigUnionH ds sig
else Result.Result [incompatibleUnionError n t t1] Nothing
else let t1 = translate Map.empty (getSymbols sig) t
sig1 = addSymbolDecl ([n], t1) sig
in sigUnionH ds 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 ds) = sigIntersectionH (expandDecls ds) emptySig
sigIntersectionH :: [SDECL] -> Sign -> Sign -> Result.Result Sign
sigIntersectionH [] sig _ = Result.Result [] $ Just sig
sigIntersectionH ((n, t) : ds) sig sig2 =
let present = isConstant n sig2
&& let Just t1 = getSymbolType n sig2
in t == t1
Diagn _ valid = isValidDecl ([n], t) sig emptyContext
in if present && valid
then let sig1 = addSymbolDecl ([n], t) sig
in sigIntersectionH ds sig1 sig2
else sigIntersectionH ds sig sig2
-- determines whether a declaration is valid w.r.t. a signature and a context
isValidDecl :: DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidDecl (ns, t) sig cont = andD [validNames, validType]
where validNames = areValidNames ns sig cont
validType = isValidType t sig cont
-- checks if a variable declaration is valid w.r.t. a signature and a context
isValidVarDecl :: DECL -> Sign -> CONTEXT -> DIAGN Bool
isValidVarDecl d@(_, t) sig cont = andD [discourseType, validDec]
where discourseType = isDiscourseType t
validDec = isValidDecl d sig 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 names sig cont =
if Set.null overlap
then Diagn [] True
else Diagn [redeclaredNamesError overlap cont] False
where declaredSyms = Set.union (getSymbols sig) (getVars cont)
newSyms = Set.fromList names
overlap = Set.intersection newSyms declaredSyms
-- determines whether a type is valid w.r.t. a signature and a context
isValidType :: TYPE -> Sign -> CONTEXT -> DIAGN Bool
isValidType Sort _ _ = Diagn [] True
isValidType Form _ _ = Diagn [] True
isValidType (Univ t) sig cont = hasType t Sort sig cont
isValidType (Func ts t) sig cont =
andD [validDoms, validCod, discourseDoms]
where validDoms = andD $ map (\ t1 -> isValidType t1 sig cont) ts
validCod = isValidType t sig cont
discourseDoms = andD $ map isDiscourseType ts
isValidType (Pi [] t) sig cont = isValidType t sig cont
isValidType (Pi (d : ds) t) sig cont =
andD [validDecl, validType]
where validDecl = isValidVarDecl d sig cont
validType = isValidType (Pi ds t) sig (addVarDecl d cont)
-- determines whether a type starts with Univ
isDiscourseType :: TYPE -> DIAGN Bool
isDiscourseType t = case t of
Univ _ -> Diagn [] True
_ -> Diagn [noDiscourseTypeError t] 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 expectedType sig cont =
case inferredTypeM of
Nothing -> Diagn diag False
Just inferredType ->
if inferredType == expectedType
then Diagn [] True
else Diagn [wrongTypeError expectedType inferredType term cont]
False
where Result.Result diag inferredTypeM = getTermType term sig 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 = getTermTypeH (termRecForm term)
getTermTypeH :: TERM -> Sign -> CONTEXT -> Result.Result TYPE
getTermTypeH (Identifier n) sig cont =
case fromContext of
Just _ -> Result.Result [] fromContext
Nothing -> case fromSig of
Just type1 ->
let type2 = renameBoundVars (typeRecForm type1)
sig cont
in Result.Result [] $ Just type2
Nothing ->
Result.Result [unknownIdentifierError n cont] Nothing
where fromSig = getSymbolType n sig
fromContext = getVarType n cont
getTermTypeH (Appl f [a]) sig cont =
case typeAM of
Nothing -> Result.Result diagA Nothing
Just typeA ->
case typeFM of
Nothing -> Result.Result diagF Nothing
Just (Func (dom : doms) cod) ->
if dom == typeA
then Result.Result [] $ Just $ typeRecForm
$ Func doms cod
else Result.Result [wrongTypeError dom typeA a cont] Nothing
Just (Pi [([x], t)] typ) ->
if t == typeA
then Result.Result [] $ Just $ substitute x a typ
else Result.Result [wrongTypeError t typeA a cont] Nothing
Just typeF ->
Result.Result [noFunctionTermError f typeF cont] Nothing
where Result.Result diagF typeFM = getTermType f sig cont
Result.Result diagA typeAM = getTermType a sig cont
getTermTypeH _ _ _ = Result.Result [] Nothing
-- returns all symbols of the specified type
getSymsOfType :: Sign -> TYPE -> [NAME]
getSymsOfType (Sign ds) = getSymsOfTypeH ds
getSymsOfTypeH :: [DECL] -> TYPE -> [NAME]
getSymsOfTypeH [] _ = []
getSymsOfTypeH ((ns, t1) : ds) t =
if t1 == t
then ns ++ getSymsOfTypeH ds t
else getSymsOfTypeH ds 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 t sig cont =
let syms = Set.union (getSymbols sig) (getVars cont)
in translate Map.empty syms t
substitute :: NAME -> TERM -> TYPE -> TYPE
substitute n val = translate (Map.singleton n val) Set.empty
-- ERROR MESSAGES
redeclaredNamesError :: Set.Set NAME -> CONTEXT -> Result.Diagnosis
redeclaredNamesError ns cont =
, Result.diagString = "Symbols or variables\n"
++ show (printNames $ Set.toList ns)
++ "\ndeclared previously in the context\n"
++ show (pretty cont) ++ "\nor in the signature."
, Result.diagPos = nullRange
}
noFunctionTermError :: TERM -> TYPE -> CONTEXT -> Result.Diagnosis
noFunctionTermError term t cont =
, Result.diagString = "Term\n" ++ show (pretty term)
++ "\nhas the non-function type\n"
++ show (pretty t)
++ "\nin the context\n" ++ show (pretty cont)
++ "\nand hence cannot be applied to an argument."
, Result.diagPos = nullRange
}
noDiscourseTypeError :: TYPE -> Result.Diagnosis
noDiscourseTypeError t =
"Type\n" ++ show (pretty t)
++ "\nis a non-discourse type (does not start with Univ) "
++ "and hence cannot be used as a type of an argument."
, Result.diagPos = nullRange
}
wrongTypeError :: TYPE -> TYPE -> TERM -> CONTEXT -> Result.Diagnosis
wrongTypeError type1 type2 term cont =
, Result.diagString = "Term\n" ++ show (pretty term)
++ "\nmust be of type "
++ show (pretty type1) ++ "\nbut is of type\n"
++ show (pretty type2) ++ "\nin context\n"
++ show (pretty cont)
, Result.diagPos = nullRange
}
unknownIdentifierError :: NAME -> CONTEXT -> Result.Diagnosis
unknownIdentifierError n cont =
, Result.diagString = "Unknown identifier\n" ++ show (pretty n)
++ "\nin the context\n" ++ show (pretty cont)
, Result.diagPos = nullRange
}
incompatibleUnionError :: NAME -> TYPE -> TYPE -> Result.Diagnosis
incompatibleUnionError n t1 t2 =
, Result.diagString = "Symbol\n" ++ show (pretty n)
++ "\nmust have both type\n" ++ show (pretty t1)
++ "\nand type\n" ++ show (pretty t2)
++ "\nin the signature union and hence "
++ "the union is not defined."
, Result.diagPos = nullRange
}