0N/ADescription : Definition of signatures for first-order logic
0N/A with dependent types (DFOL)
0N/ACopyright : (c) Kristina Sojakova, DFKI Bremen 2009
0N/AMaintainer : k.sojakova@jacobs-university.de
0N/AStability : experimental
0N/APortability : portable
data CONTEXT = Context [DECL]
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
getVarType :: NAME -> CONTEXT -> Maybe TYPE
getVarType n (Context ds) = getVarTypeFromDecls n ds
-- adds a symbol declaration to the signature
addSymbolDecl :: DECL -> Sign -> Sign
addSymbolDecl d (Sign ds) = Sign (ds ++ [d])
-- get the set of defined symbols
-- checks if the symbol is defined in the signature
isConstant :: NAME -> Sign -> Bool
getSymbolType :: NAME -> Sign -> Maybe TYPE
getSymbolType n (Sign ds) = getVarTypeFromDecls n ds
getSymbolKind :: NAME -> Sign -> Maybe KIND
getSymbolKind n sig = case (getReturnType n sig) of
Just Sort -> Just SortKind
Just Form -> Just PredKind
getSymbolArity :: NAME -> Sign -> Maybe ARITY
getSymbolArity n sig = case (getArgumentTypes n sig) of
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
Just typ -> Just $ getArgumentTypesH typ
where typM = getSymbolType n sig
getArgumentTypesH :: TYPE -> [TYPE]
getArgumentTypesH (Pi ds t) =
where types1 = concatMap (\ (ns,t1) -> take (length ns) $ repeat t1) ds
types2 = getArgumentTypesH t
getArgumentTypesH (Func ts t) = ts ++ (getArgumentTypesH t)
-- get the return type of a symbol with the given type
getReturnType :: NAME -> Sign -> Maybe TYPE
getReturnType n sig = case typM of
Just typ -> Just $ getReturnTypeH typ
where typM = getSymbolType n sig
getReturnTypeH :: TYPE -> TYPE
getReturnTypeH (Pi _ t) = getReturnTypeH t
getReturnTypeH (Func _ t) = getReturnTypeH t
-- get the argument names
getArgumentNames :: NAME -> Sign -> Maybe [NAME]
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) =
(take (length ts) $ repeat Nothing) ++ getArgumentNamesH t
fillArgumentNames :: [Maybe NAME] -> [NAME]
fillArgumentNames ns = fillArgumentNamesH ns 0
fillArgumentNamesH :: [Maybe NAME] -> Int -> [NAME]
fillArgumentNamesH [] _ = []
fillArgumentNamesH (nameM:namesM) i =
Just name -> name:(fillArgumentNamesH namesM i)
Nothing -> (Token ("gen_x_" ++ show i) nullRange):
(fillArgumentNamesH namesM (i+1))
instance Pretty Sign where
instance Pretty CONTEXT where
pretty (Context xs) = printDecls xs
instance Pretty KIND where
printSig (Sign []) = text "EmptySig"
printSig (Sign ds) = vcat $ map printSigDecl $ compactDecls ds
printSigDecl :: DECL -> Doc
printSigDecl (ns,t) = printNames ns <+> text "::" <+> pretty t
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 sig (Sign ds) = sigUnionH (expandDecls ds) sig
sigUnionH (([n],t):ds) sig =
then let Just t1 = getSymbolType n sig
else let t1 = translate
Map.empty (getSymbols sig) t
sig1 = addSymbolDecl ([n],t1) sig
{- 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
sigIntersection (Sign ds) sig = sigIntersectionH (expandDecls ds) emptySig sig
sigIntersectionH (([n],t):ds) sig sig2 =
let present = if (isConstant n sig2)
then let Just t1 = getSymbolType n sig2
Diagn _ valid = isValidDecl ([n],t) sig emptyContext
in if (and [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
areValidNames :: [NAME] -> Sign -> CONTEXT -> DIAGN Bool
areValidNames names sig cont =
else Diagn [redeclaredNamesError overlap cont] False
where declaredSyms =
Set.union (getSymbols sig) (getVars cont)
-- 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
_ -> 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 =
Nothing -> Diagn diag False
if (inferredType == expectedType)
else Diagn [wrongTypeError expectedType inferredType term cont]
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 sig cont = getTermTypeH (termRecForm term) sig cont
getTermTypeH (Identifier n) sig cont =
Nothing -> case fromSig of
let type2 = renameBoundVars (typeRecForm type1)
where fromSig = getSymbolType n sig
fromContext = getVarType n cont
getTermTypeH (Appl f [a]) sig cont =
Just (Func (dom:doms) cod) ->
Just (Pi [([x],t)] typ) ->
-- 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)
substitute :: NAME -> TERM -> TYPE -> TYPE
redeclaredNamesError ns cont =
++ "\ndeclared previously in the context\n"
++ (show $ pretty cont) ++ "\nor in the signature."
noFunctionTermError term t cont =
++ "\nhas the non-function type\n"
++ "\nin the context\n" ++ (show $ pretty cont)
++ "\nand hence cannot be applied to an argument."
"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."
wrongTypeError type1 type2 term cont =
++ (show $ pretty type1) ++ "\nbut is of type\n"
++ (show $ pretty type2) ++ "\nin context\n"
unknownIdentifierError n cont =
++ "\nin the context\n" ++ (show $ pretty cont)
incompatibleUnionError n t1 t2 =
++ "\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."