1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}
097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina SojakovaDescription : Definition of signatures for first-order logic
097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakova with dependent types (DFOL)
94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaCopyright : (c) Kristina Sojakova, DFKI Bremen 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaMaintainer : k.sojakova@jacobs-university.de
211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaStability : experimental
211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaPortability : portable
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova , CONTEXT (..)
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova , emptyContext
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova , addSymbolDecl
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova , getSymbolType
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova , getSymbolKind
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova , getSymbolArity
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova , getSymbolsByKind
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova , getArgumentTypes
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova , getReturnType
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova , getArgumentNames
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , sigIntersection
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , isValidVarDecl
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova , getSymsOfType
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport qualified Common.Result as Result
2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakovaimport qualified Data.Set as Set
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport qualified Data.Map as Map
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- symbol kinds
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakovadata KIND = SortKind
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Ord, Eq, Typeable, Data)
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakovatype ARITY = Int
2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakova-- contexts for DFOL
4e3744376d584470e1342cbac9ac27032f2045c3Christian Maederdata CONTEXT = Context [DECL]
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Typeable, Data)
2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakova-- the empty context
2ddc9d39235393dca2e40203dde20284db4c3deeKristina SojakovaemptyContext :: CONTEXT
2ddc9d39235393dca2e40203dde20284db4c3deeKristina SojakovaemptyContext = Context []
2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakova-- adds a variable declaration to the context
2ddc9d39235393dca2e40203dde20284db4c3deeKristina SojakovaaddVarDecl :: DECL -> CONTEXT -> CONTEXT
2ddc9d39235393dca2e40203dde20284db4c3deeKristina SojakovaaddVarDecl d (Context ds) = Context (ds ++ [d])
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- get the list of declared variables
2ddc9d39235393dca2e40203dde20284db4c3deeKristina SojakovagetVars :: CONTEXT -> Set.Set NAME
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetVars (Context ds) = Set.fromList $ getVarsFromDecls ds
2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakova-- get the variable type
2ddc9d39235393dca2e40203dde20284db4c3deeKristina SojakovagetVarType :: NAME -> CONTEXT -> Maybe TYPE
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetVarType n (Context ds) = getVarTypeFromDecls n ds
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- signatures for DFOL
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakovadata Sign = Sign [DECL]
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Ord, Eq, Typeable, Data)
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- the empty signature
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaemptySig :: Sign
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaemptySig = Sign []
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- adds a symbol declaration to the signature
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaaddSymbolDecl :: DECL -> Sign -> Sign
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaaddSymbolDecl d (Sign ds) = Sign (ds ++ [d])
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- get the set of defined symbols
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetSymbols :: Sign -> Set.Set NAME
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetSymbols (Sign ds) = Set.fromList $ getVarsFromDecls ds
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- checks if the symbol is defined in the signature
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaisConstant :: NAME -> Sign -> Bool
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaisConstant n sig = Set.member n $ getSymbols sig
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- get the symbol type
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetSymbolType :: NAME -> Sign -> Maybe TYPE
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetSymbolType n (Sign ds) = getVarTypeFromDecls n ds
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- get the symbol kind
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetSymbolKind :: NAME -> Sign -> Maybe KIND
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetSymbolKind n sig = case getReturnType n sig of
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova Nothing -> Nothing
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova Just Sort -> Just SortKind
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova Just Form -> Just PredKind
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova Just _ -> Just FuncKind
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- get the symbol arity
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetSymbolArity :: NAME -> Sign -> Maybe ARITY
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetSymbolArity n sig = case getArgumentTypes n sig of
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova Nothing -> Nothing
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova Just ts -> Just $ length ts
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- get a list of symbols of the given kind
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetSymbolsByKind :: Sign -> KIND -> Set.Set NAME
4cfef84218e908a7db4a0bba0927be1397886315Kristina SojakovagetSymbolsByKind sig kind =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Set.filter (\ n -> getSymbolKind n sig == Just kind) $ getSymbols sig
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- get the list of types of the arguments of the given symbol
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetArgumentTypes :: NAME -> Sign -> Maybe [TYPE]
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetArgumentTypes n sig = case typM of
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova Nothing -> Nothing
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova Just typ -> Just $ getArgumentTypesH typ
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova where typM = getSymbolType n sig
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetArgumentTypesH :: TYPE -> [TYPE]
4cfef84218e908a7db4a0bba0927be1397886315Kristina SojakovagetArgumentTypesH (Pi ds t) =
097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakova types1 ++ types2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder where types1 = concatMap (\ (ns, t1) -> replicate (length ns) t1) ds
4cfef84218e908a7db4a0bba0927be1397886315Kristina Sojakova types2 = getArgumentTypesH t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetArgumentTypesH (Func ts t) = ts ++ getArgumentTypesH t
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetArgumentTypesH _ = []
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- get the return type of a symbol with the given type
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetReturnType :: NAME -> Sign -> Maybe TYPE
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetReturnType n sig = case typM of
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova Nothing -> Nothing
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova Just typ -> Just $ getReturnTypeH typ
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova where typM = getSymbolType n sig
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetReturnTypeH :: TYPE -> TYPE
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetReturnTypeH (Pi _ t) = getReturnTypeH t
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetReturnTypeH (Func _ t) = getReturnTypeH t
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetReturnTypeH t = t
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova-- get the argument names
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetArgumentNames :: NAME -> Sign -> Maybe [NAME]
4cfef84218e908a7db4a0bba0927be1397886315Kristina SojakovagetArgumentNames n sig =
097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakova Nothing -> Nothing
097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakova Just typ -> Just $ fillArgumentNames $ getArgumentNamesH typ
097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakova where typM = getSymbolType n sig
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetArgumentNamesH :: TYPE -> [Maybe NAME]
4cfef84218e908a7db4a0bba0927be1397886315Kristina SojakovagetArgumentNamesH (Pi ds t) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder map Just (getVarsFromDecls ds) ++ getArgumentNamesH t
4cfef84218e908a7db4a0bba0927be1397886315Kristina SojakovagetArgumentNamesH (Func ts t) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder replicate (length ts) Nothing ++ getArgumentNamesH t
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovagetArgumentNamesH _ = []
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovafillArgumentNames :: [Maybe NAME] -> [NAME]
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovafillArgumentNames ns = fillArgumentNamesH ns 0
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovafillArgumentNamesH :: [Maybe NAME] -> Int -> [NAME]
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovafillArgumentNamesH [] _ = []
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederfillArgumentNamesH (nameM : namesM) i =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just name -> name : fillArgumentNamesH namesM i
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> Token ("gen_x_" ++ show i) nullRange :
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder fillArgumentNamesH namesM (i + 1)
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- pretty printing
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovainstance Pretty Sign where
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova pretty = printSig
2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakovainstance Pretty CONTEXT where
4e3744376d584470e1342cbac9ac27032f2045c3Christian Maeder pretty (Context xs) = printDecls xs
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakovainstance Pretty KIND where
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova pretty = printKind
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaprintSig :: Sign -> Doc
2ddc9d39235393dca2e40203dde20284db4c3deeKristina SojakovaprintSig (Sign []) = text "EmptySig"
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaprintSig (Sign ds) = vcat $ map printSigDecl $ compactDecls ds
4e3744376d584470e1342cbac9ac27032f2045c3Christian MaederprintSigDecl :: DECL -> Doc
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederprintSigDecl (ns, t) = printNames ns <+> text "::" <+> pretty t
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaprintKind :: KIND -> Doc
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaprintKind SortKind = text "sort"
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaprintKind FuncKind = text "func"
b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaprintKind PredKind = text "pred"
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova{- Union of signatures. The union of two DFOL signatures Sig1 and Sig2 is
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova defined as the smallest valid signature containing both Sig1 and Sig2 as
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova subsignatures. It is not always defined, namely in the case when the original
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova signatures give conflicting definitions for the same symbol. -}
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasigUnion :: Sign -> Sign -> Result.Result Sign
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasigUnion sig (Sign ds) = sigUnionH (expandDecls ds) sig
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedersigUnionH :: [SDECL] -> Sign -> Result.Result Sign
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasigUnionH [] sig = Result.Result [] $ Just sig
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedersigUnionH ((n, t) : ds) sig =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if isConstant n sig
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then let Just t1 = getSymbolType n sig
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then sigUnionH ds sig
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else Result.Result [incompatibleUnionError n t t1] Nothing
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else let t1 = translate Map.empty (getSymbols sig) t
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder sig1 = addSymbolDecl ([n], t1) sig
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in sigUnionH ds sig1
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova{- Intersection of signatures. The intersection of two DFOL signatures Sig1 and
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Sig2 is defined as the largest valid signature contained both in Sig1 and
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova Sig2 as a subsignature. It is always defined but may be the empty
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasigIntersection :: Sign -> Sign -> Result.Result Sign
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersigIntersection (Sign ds) = sigIntersectionH (expandDecls ds) emptySig
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedersigIntersectionH :: [SDECL] -> Sign -> Sign -> Result.Result Sign
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasigIntersectionH [] sig _ = Result.Result [] $ Just sig
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedersigIntersectionH ((n, t) : ds) sig sig2 =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let present = isConstant n sig2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder && let Just t1 = getSymbolType n sig2
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder Diagn _ valid = isValidDecl ([n], t) sig emptyContext
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if present && valid
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder then let sig1 = addSymbolDecl ([n], t) sig
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in sigIntersectionH ds sig1 sig2
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else sigIntersectionH ds sig sig2
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- determines whether a declaration is valid w.r.t. a signature and a context
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisValidDecl :: DECL -> Sign -> CONTEXT -> DIAGN Bool
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederisValidDecl (ns, t) sig cont = andD [validNames, validType]
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova where validNames = areValidNames ns sig cont
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder validType = isValidType t sig cont
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- checks if a variable declaration is valid w.r.t. a signature and a context
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisValidVarDecl :: DECL -> Sign -> CONTEXT -> DIAGN Bool
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederisValidVarDecl d@(_, t) sig cont = andD [discourseType, validDec]
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova where discourseType = isDiscourseType t
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova validDec = isValidDecl d sig cont
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova{- checks if a list of names in a declaration is valid w.r.t. a signature
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova and a context -}
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaareValidNames :: [NAME] -> Sign -> CONTEXT -> DIAGN Bool
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaareValidNames names sig cont =
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then Diagn [] True
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else Diagn [redeclaredNamesError overlap cont] False
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova where declaredSyms = Set.union (getSymbols sig) (getVars cont)
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder newSyms = Set.fromList names
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder overlap = Set.intersection newSyms declaredSyms
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- determines whether a type is valid w.r.t. a signature and a context
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisValidType :: TYPE -> Sign -> CONTEXT -> DIAGN Bool
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisValidType Sort _ _ = Diagn [] True
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisValidType Form _ _ = Diagn [] True
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisValidType (Univ t) sig cont = hasType t Sort sig cont
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisValidType (Func ts t) sig cont =
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder andD [validDoms, validCod, discourseDoms]
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder where validDoms = andD $ map (\ t1 -> isValidType t1 sig cont) ts
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder validCod = isValidType t sig cont
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova discourseDoms = andD $ map isDiscourseType ts
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisValidType (Pi [] t) sig cont = isValidType t sig cont
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederisValidType (Pi (d : ds) t) sig cont =
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova andD [validDecl, validType]
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova where validDecl = isValidVarDecl d sig cont
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova validType = isValidType (Pi ds t) sig (addVarDecl d cont)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- determines whether a type starts with Univ
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisDiscourseType :: TYPE -> DIAGN Bool
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaisDiscourseType t = case t of
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Univ _ -> Diagn [] True
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova _ -> Diagn [noDiscourseTypeError t] False
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- determines whether a term has the given type w.r.t. a signature and a context
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovahasType :: TERM -> TYPE -> Sign -> CONTEXT -> DIAGN Bool
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovahasType term expectedType sig cont =
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case inferredTypeM of
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> Diagn diag False
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just inferredType ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if inferredType == expectedType
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then Diagn [] True
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else Diagn [wrongTypeError expectedType inferredType term cont]
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova where Result.Result diag inferredTypeM = getTermType term sig cont
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder{- determines the type of a term w.r.t. a signature and a context
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maederreturns the type in recursive form, with bound variables different
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova from signature constants -}
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetTermType :: TERM -> Sign -> CONTEXT -> Result.Result TYPE
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetTermType term = getTermTypeH (termRecForm term)
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedergetTermTypeH :: TERM -> Sign -> CONTEXT -> Result.Result TYPE
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetTermTypeH (Identifier n) sig cont =
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case fromContext of
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder Just _ -> Result.Result [] fromContext
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> case fromSig of
c2a8d1de8526aecb5a1e18e66e7a0209f2d0d600Kristina Sojakova let type2 = renameBoundVars (typeRecForm type1)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in Result.Result [] $ Just type2
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Result [unknownIdentifierError n cont] Nothing
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova where fromSig = getSymbolType n sig
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova fromContext = getVarType n cont
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetTermTypeH (Appl f [a]) sig cont =
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case typeAM of
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> Result.Result diagA Nothing
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case typeFM of
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> Result.Result diagF Nothing
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder Just (Func (dom : doms) cod) ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if dom == typeA
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova then Result.Result [] $ Just $ typeRecForm
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova $ Func doms cod
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else Result.Result [wrongTypeError dom typeA a cont] Nothing
fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder Just (Pi [([x], t)] typ) ->
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then Result.Result [] $ Just $ substitute x a typ
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else Result.Result [wrongTypeError t typeA a cont] Nothing
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Result [noFunctionTermError f typeF cont] Nothing
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova where Result.Result diagF typeFM = getTermType f sig cont
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Result diagA typeAM = getTermType a sig cont
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetTermTypeH _ _ _ = Result.Result [] Nothing
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova-- returns all symbols of the specified type
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovagetSymsOfType :: Sign -> TYPE -> [NAME]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetSymsOfType (Sign ds) = getSymsOfTypeH ds
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovagetSymsOfTypeH :: [DECL] -> TYPE -> [NAME]
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovagetSymsOfTypeH [] _ = []
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovagetSymsOfTypeH ((ns, t1) : ds) t =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then ns ++ getSymsOfTypeH ds t
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova else getSymsOfTypeH ds t
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- renames bound variables in a type to make it valid w.r.t. a sig and a context
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovarenameBoundVars :: TYPE -> Sign -> CONTEXT -> TYPE
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovarenameBoundVars t sig cont =
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let syms = Set.union (getSymbols sig) (getVars cont)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in translate Map.empty syms t
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovasubstitute :: NAME -> TERM -> TYPE -> TYPE
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersubstitute n val = translate (Map.singleton n val) Set.empty
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- ERROR MESSAGES
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaredeclaredNamesError :: Set.Set NAME -> CONTEXT -> Result.Diagnosis
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaredeclaredNamesError ns cont =
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , Result.diagString = "Symbols or variables\n"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (printNames $ Set.toList ns)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\ndeclared previously in the context\n"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty cont) ++ "\nor in the signature."
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovanoFunctionTermError :: TERM -> TYPE -> CONTEXT -> Result.Diagnosis
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovanoFunctionTermError term t cont =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "Term\n" ++ show (pretty term)
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova ++ "\nhas the non-function type\n"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty t)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "\nin the context\n" ++ show (pretty cont)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nand hence cannot be applied to an argument."
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovanoDiscourseTypeError :: TYPE -> Result.Diagnosis
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovanoDiscourseTypeError t =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "Type\n" ++ show (pretty t)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nis a non-discourse type (does not start with Univ) "
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "and hence cannot be used as a type of an argument."
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovawrongTypeError :: TYPE -> TYPE -> TERM -> CONTEXT -> Result.Diagnosis
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovawrongTypeError type1 type2 term cont =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "Term\n" ++ show (pretty term)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nmust be of type "
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty type1) ++ "\nbut is of type\n"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty type2) ++ "\nin context\n"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty cont)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaunknownIdentifierError :: NAME -> CONTEXT -> Result.Diagnosis
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaunknownIdentifierError n cont =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "Unknown identifier\n" ++ show (pretty n)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "\nin the context\n" ++ show (pretty cont)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaincompatibleUnionError :: NAME -> TYPE -> TYPE -> Result.Diagnosis
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaincompatibleUnionError n t1 t2 =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "Symbol\n" ++ show (pretty n)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "\nmust have both type\n" ++ show (pretty t1)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "\nand type\n" ++ show (pretty t2)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nin the signature union and hence "
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "the union is not defined."