Sign.hs revision d71bb9deea089887b4fd829c5b766e7e4de9f204
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannModule : $Header$
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannDescription : Definition of signatures for first-order logic
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann with dependent types (DFOL)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannCopyright : (c) Kristina Sojakova, DFKI Bremen 2009
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannLicense : GPLv2 or higher, see LICENSE.txt
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannMaintainer : k.sojakova@jacobs-university.de
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannStability : experimental
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannPortability : portable
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , CONTEXT (..)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , emptyContext
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , addSymbolDecl
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , getSymbolType
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , getSymbolKind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , getSymbolArity
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , getSymbolsByKind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , getArgumentTypes
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , getReturnType
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , getArgumentNames
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , sigIntersection
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , isValidDecl
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , isValidVarDecl
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , getTermType
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , isValidType
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , getSymsOfType
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport qualified Common.Result as Result
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport qualified Data.Set as Set
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport qualified Data.Map as Map
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- symbol kinds
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanndata KIND = SortKind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann deriving (Show, Ord, Eq)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanntype ARITY = Int
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- contexts for DFOL
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanndata CONTEXT = Context [DECL]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann deriving (Show, Eq)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- the empty context
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannemptyContext :: CONTEXT
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannemptyContext = Context []
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- adds a variable declaration to the context
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannaddVarDecl :: DECL -> CONTEXT -> CONTEXT
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannaddVarDecl d (Context ds) = Context (ds ++ [d])
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- get the list of declared variables
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetVars :: CONTEXT -> Set.Set NAME
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetVars (Context ds) = Set.fromList $ getVarsFromDecls ds
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- get the variable type
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetVarType :: NAME -> CONTEXT -> Maybe TYPE
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetVarType n (Context ds) = getVarTypeFromDecls n ds
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- signatures for DFOL
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanndata Sign = Sign [DECL]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann deriving (Show, Ord, Eq)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- the empty signature
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannemptySig :: Sign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannemptySig = Sign []
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- adds a symbol declaration to the signature
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannaddSymbolDecl :: DECL -> Sign -> Sign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannaddSymbolDecl d (Sign ds) = Sign (ds ++ [d])
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- get the set of defined symbols
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymbols :: Sign -> Set.Set NAME
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymbols (Sign ds) = Set.fromList $ getVarsFromDecls ds
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- checks if the symbol is defined in the signature
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisConstant :: NAME -> Sign -> Bool
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisConstant n sig = Set.member n $ getSymbols sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- get the symbol type
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymbolType :: NAME -> Sign -> Maybe TYPE
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymbolType n (Sign ds) = getVarTypeFromDecls n ds
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- get the symbol kind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymbolKind :: NAME -> Sign -> Maybe KIND
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymbolKind n sig = case (getReturnType n sig) of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just Sort -> Just SortKind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just Form -> Just PredKind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just _ -> Just FuncKind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- get the symbol arity
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymbolArity :: NAME -> Sign -> Maybe ARITY
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymbolArity n sig = case (getArgumentTypes n sig) of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just ts -> Just $ length ts
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- get a list of symbols of the given kind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymbolsByKind :: Sign -> KIND -> Set.Set NAME
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymbolsByKind sig kind =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Set.filter (\ n -> (getSymbolKind n sig) == Just kind) $ getSymbols sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- get the list of types of the arguments of the given symbol
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentTypes :: NAME -> Sign -> Maybe [TYPE]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentTypes n sig = case typM of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just typ -> Just $ getArgumentTypesH typ
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where typM = getSymbolType n sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentTypesH :: TYPE -> [TYPE]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentTypesH (Pi ds t) =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann types1 ++ types2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where types1 = concatMap (\ (ns, t1) -> take (length ns) $ repeat t1) ds
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann types2 = getArgumentTypesH t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentTypesH (Func ts t) = ts ++ (getArgumentTypesH t)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentTypesH _ = []
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- get the return type of a symbol with the given type
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetReturnType :: NAME -> Sign -> Maybe TYPE
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetReturnType n sig = case typM of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just typ -> Just $ getReturnTypeH typ
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where typM = getSymbolType n sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetReturnTypeH :: TYPE -> TYPE
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetReturnTypeH (Pi _ t) = getReturnTypeH t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetReturnTypeH (Func _ t) = getReturnTypeH t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetReturnTypeH t = t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- get the argument names
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentNames :: NAME -> Sign -> Maybe [NAME]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentNames n sig =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just typ -> Just $ fillArgumentNames $ getArgumentNamesH typ
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where typM = getSymbolType n sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentNamesH :: TYPE -> [Maybe NAME]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentNamesH (Pi ds t) =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (map Just $ getVarsFromDecls ds) ++ getArgumentNamesH t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentNamesH (Func ts t) =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (take (length ts) $ repeat Nothing) ++ getArgumentNamesH t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetArgumentNamesH _ = []
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannfillArgumentNames :: [Maybe NAME] -> [NAME]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannfillArgumentNames ns = fillArgumentNamesH ns 0
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannfillArgumentNamesH :: [Maybe NAME] -> Int -> [NAME]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannfillArgumentNamesH [] _ = []
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannfillArgumentNamesH (nameM : namesM) i =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann case nameM of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just name -> name : (fillArgumentNamesH namesM i)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> (Token ("gen_x_" ++ show i) nullRange) :
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (fillArgumentNamesH namesM (i + 1))
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- pretty printing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Pretty Sign where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann pretty = printSig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Pretty CONTEXT where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann pretty (Context xs) = printDecls xs
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Pretty KIND where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann pretty = printKind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannprintSig :: Sign -> Doc
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannprintSig (Sign []) = text "EmptySig"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannprintSig (Sign ds) = vcat $ map printSigDecl $ compactDecls ds
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannprintSigDecl :: DECL -> Doc
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannprintSigDecl (ns, t) = printNames ns <+> text "::" <+> pretty t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannprintKind :: KIND -> Doc
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannprintKind SortKind = text "sort"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannprintKind FuncKind = text "func"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannprintKind PredKind = text "pred"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- Union of signatures. The union of two DFOL signatures Sig1 and Sig2 is
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann defined as the smallest valid signature containing both Sig1 and Sig2 as
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann subsignatures. It is not always defined, namely in the case when the original
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann signatures give conflicting definitions for the same symbol. -}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsigUnion :: Sign -> Sign -> Result.Result Sign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsigUnion sig (Sign ds) = sigUnionH (expandDecls ds) sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsigUnionH :: [SDECL] -> Sign -> Result.Result Sign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsigUnionH [] sig = Result.Result [] $ Just sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsigUnionH ((n, t) : ds) sig =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann if (isConstant n sig)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann then let Just t1 = getSymbolType n sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in if (t == t1)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann then sigUnionH ds sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else Result.Result [incompatibleUnionError n t t1] Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else let t1 = translate Map.empty (getSymbols sig) t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sig1 = addSymbolDecl ([n], t1) sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in sigUnionH ds sig1
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- Intersection of signatures. The intersection of two DFOL signatures Sig1 and
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Sig2 is defined as the largest valid signature contained both in Sig1 and
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Sig2 as a subsignature. It is always defined but may be the empty
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann signature. -}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsigIntersection :: Sign -> Sign -> Result.Result Sign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsigIntersection (Sign ds) sig = sigIntersectionH (expandDecls ds) emptySig sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsigIntersectionH :: [SDECL] -> Sign -> Sign -> Result.Result Sign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsigIntersectionH [] sig _ = Result.Result [] $ Just sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsigIntersectionH ((n, t) : ds) sig sig2 =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let present = if (isConstant n sig2)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann then let Just t1 = getSymbolType n sig2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in if (t == t1)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Diagn _ valid = isValidDecl ([n], t) sig emptyContext
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in if (and [present, valid])
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann then let sig1 = addSymbolDecl ([n], t) sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in sigIntersectionH ds sig1 sig2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else sigIntersectionH ds sig sig2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- determines whether a declaration is valid w.r.t. a signature and a context
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisValidDecl :: DECL -> Sign -> CONTEXT -> DIAGN Bool
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisValidDecl (ns, t) sig cont = andD [validNames, validType]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where validNames = areValidNames ns sig cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann validType = isValidType t sig cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- checks if a variable declaration is valid w.r.t. a signature and a context
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisValidVarDecl :: DECL -> Sign -> CONTEXT -> DIAGN Bool
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisValidVarDecl d@(_, t) sig cont = andD [discourseType, validDec]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where discourseType = isDiscourseType t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann validDec = isValidDecl d sig cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- checks if a list of names in a declaration is valid w.r.t. a signature
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann and a context -}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannareValidNames :: [NAME] -> Sign -> CONTEXT -> DIAGN Bool
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannareValidNames names sig cont =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann then Diagn [] True
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else Diagn [redeclaredNamesError overlap cont] False
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where declaredSyms = Set.union (getSymbols sig) (getVars cont)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann newSyms = Set.fromList names
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann overlap = Set.intersection newSyms declaredSyms
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- determines whether a type is valid w.r.t. a signature and a context
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisValidType :: TYPE -> Sign -> CONTEXT -> DIAGN Bool
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisValidType Sort _ _ = Diagn [] True
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisValidType Form _ _ = Diagn [] True
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisValidType (Univ t) sig cont = hasType t Sort sig cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisValidType (Func ts t) sig cont =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann andD [validDoms, validCod, discourseDoms]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where validDoms = andD $ map (\ t1 -> isValidType t1 sig cont) ts
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann validCod = isValidType t sig cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann discourseDoms = andD $ map isDiscourseType ts
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisValidType (Pi [] t) sig cont = isValidType t sig cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisValidType (Pi (d : ds) t) sig cont =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann andD [validDecl, validType]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where validDecl = isValidVarDecl d sig cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann validType = isValidType (Pi ds t) sig (addVarDecl d cont)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- determines whether a type starts with Univ
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisDiscourseType :: TYPE -> DIAGN Bool
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannisDiscourseType t = case t of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Univ _ -> Diagn [] True
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> Diagn [noDiscourseTypeError t] False
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- determines whether a term has the given type w.r.t. a signature and a context
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannhasType :: TERM -> TYPE -> Sign -> CONTEXT -> DIAGN Bool
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannhasType term expectedType sig cont =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann case inferredTypeM of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> Diagn diag False
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just inferredType ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann if (inferredType == expectedType)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann then Diagn [] True
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else Diagn [wrongTypeError expectedType inferredType term cont]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where Result.Result diag inferredTypeM = getTermType term sig cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- determines the type of a term w.r.t. a signature and a context
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannreturns the type in recursive form, with bound variables different
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann from signature constants -}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetTermType :: TERM -> Sign -> CONTEXT -> Result.Result TYPE
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetTermType term sig cont = getTermTypeH (termRecForm term) sig cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetTermTypeH :: TERM -> Sign -> CONTEXT -> Result.Result TYPE
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetTermTypeH (Identifier n) sig cont =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann case fromContext of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just _ -> Result.Result [] fromContext
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> case fromSig of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just type1 ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let type2 = renameBoundVars (typeRecForm type1)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in Result.Result [] $ Just type2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Result.Result [unknownIdentifierError n cont] Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where fromSig = getSymbolType n sig
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann fromContext = getVarType n cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetTermTypeH (Appl f [a]) sig cont =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann case typeAM of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> Result.Result diagA Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just typeA ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann case typeFM of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> Result.Result diagF Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just (Func (dom : doms) cod) ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann if (dom == typeA)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann then Result.Result [] $ Just $ typeRecForm
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ Func doms cod
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else Result.Result [wrongTypeError dom typeA a cont] Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just (Pi [([x], t)] typ) ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann if (t == typeA)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann then Result.Result [] $ Just $ substitute x a typ
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else Result.Result [wrongTypeError t typeA a cont] Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just typeF ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Result.Result [noFunctionTermError f typeF cont] Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where Result.Result diagF typeFM = getTermType f sig cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Result.Result diagA typeAM = getTermType a sig cont
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetTermTypeH _ _ _ = Result.Result [] Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- returns all symbols of the specified type
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymsOfType :: Sign -> TYPE -> [NAME]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymsOfType (Sign ds) t = getSymsOfTypeH ds t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymsOfTypeH :: [DECL] -> TYPE -> [NAME]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymsOfTypeH [] _ = []
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSymsOfTypeH ((ns, t1) : ds) t =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann then ns ++ (getSymsOfTypeH ds t)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else getSymsOfTypeH ds t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- renames bound variables in a type to make it valid w.r.t. a sig and a context
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannrenameBoundVars :: TYPE -> Sign -> CONTEXT -> TYPE
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannrenameBoundVars t sig cont =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let syms = Set.union (getSymbols sig) (getVars cont)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in translate Map.empty syms t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannsubstitute :: NAME -> TERM -> TYPE -> TYPE
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannsubstitute n val t = translate (Map.singleton n val) Set.empty t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- ERROR MESSAGES
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannredeclaredNamesError :: Set.Set NAME -> CONTEXT -> Result.Diagnosis
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannredeclaredNamesError ns cont =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , Result.diagString = "Symbols or variables\n"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ (show $ printNames $ Set.toList ns)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "\ndeclared previously in the context\n"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ (show $ pretty cont) ++ "\nor in the signature."
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannnoFunctionTermError :: TERM -> TYPE -> CONTEXT -> Result.Diagnosis
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannnoFunctionTermError term t cont =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , Result.diagString = "Term\n" ++ (show $ pretty term)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "\nhas the non-function type\n"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ (show $ pretty t)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "\nin the context\n" ++ (show $ pretty cont)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "\nand hence cannot be applied to an argument."
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannnoDiscourseTypeError :: TYPE -> Result.Diagnosis
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannnoDiscourseTypeError t =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann "Type\n" ++ (show $ pretty t)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "\nis a non-discourse type (does not start with Univ) "
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "and hence cannot be used as a type of an argument."
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannwrongTypeError :: TYPE -> TYPE -> TERM -> CONTEXT -> Result.Diagnosis
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannwrongTypeError type1 type2 term cont =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , Result.diagString = "Term\n" ++ (show $ pretty term)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "\nmust be of type "
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ (show $ pretty type1) ++ "\nbut is of type\n"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ (show $ pretty type2) ++ "\nin context\n"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ (show $ pretty cont)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannunknownIdentifierError :: NAME -> CONTEXT -> Result.Diagnosis
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannunknownIdentifierError n cont =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , Result.diagString = "Unknown identifier\n" ++ (show $ pretty n)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "\nin the context\n" ++ (show $ pretty cont)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannincompatibleUnionError :: NAME -> TYPE -> TYPE -> Result.Diagnosis
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannincompatibleUnionError n t1 t2 =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , Result.diagString = "Symbol\n" ++ (show $ pretty n)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "\nmust have both type\n" ++ (show $ pretty t1)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "\nand type\n" ++ (show $ pretty t2)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "\nin the signature union and hence "
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "the union is not defined."