4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |

5ba323da9f037264b4a356085e844889aedeac23Christian MaederModule : $Header$

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2003

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : hets@tzi.de

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : provisional

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederPortability : portable

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederCASL signatures and static analysis for basic specifications

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maedermodule CASL.StaticAna where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederimport CASL.AS_Basic_CASL

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport CASL.MixfixParser

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport Common.Lib.State

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.PrettyPrint

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Common.PPUtils

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.Lib.Pretty

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport CASL.Print_AS_Basic

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport qualified Common.Lib.Map as Map

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport qualified Common.Lib.Set as Set

950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maederimport qualified Common.Lib.Rel as Rel

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport Common.Id

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maederimport Common.AS_Annotation

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Common.GlobalAnnotations

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport Common.Named

af621d0066770895fd79562728e93099c8c52060Christian Maederimport Common.Result

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maederimport Data.Maybe

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maederdata FunKind = Total | Partial deriving (Show, Eq, Ord)

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder-- constants have empty argument lists

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederdata OpType = OpType {opKind :: FunKind, opArgs :: [SORT], opRes :: SORT}

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder deriving (Show, Eq, Ord)

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maederdata PredType = PredType {predArgs :: [SORT]} deriving (Show, Eq, Ord)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederdata Env = Env { sortSet :: Set.Set SORT

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , sortRel :: Rel.Rel SORT

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , opMap :: Map.Map Id (Set.Set OpType)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , predMap :: Map.Map Id (Set.Set PredType)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , varMap :: Map.Map SIMPLE_ID (Set.Set SORT)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , sentences :: [Named FORMULA]

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , envDiags :: [Diagnosis]

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder } deriving (Show, Eq)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederemptyEnv :: Env

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederemptyEnv = Env { sortSet = Set.empty

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , sortRel = Rel.empty

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , opMap = Map.empty

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , predMap = Map.empty

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , varMap = Map.empty

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , sentences = []

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , envDiags = [] }

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedersubsortsOf :: SORT -> Env -> Set.Set SORT

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedersubsortsOf s e =

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Map.foldWithKey addSubs (Set.empty) (Rel.toMap $ sortRel e)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder where addSubs sub supers =

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder if s `Set.member` supers

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder then Set.insert sub

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder else id

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedersupersortsOf :: SORT -> Env -> Set.Set SORT

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedersupersortsOf s e =

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder case Map.lookup s $ Rel.toMap $ sortRel e of

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder Nothing -> Set.empty

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Just supers -> supers

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederaddSort :: SORT -> State Env ()

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederaddSort s =

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder do e <- get

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder let m = sortSet e

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder if Set.member s m then

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder addDiags [mkDiag Hint "redeclared sort" s]

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder else put e { sortSet = Set.insert s m }

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaedercheckSort :: SORT -> State Env ()

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedercheckSort s =

eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder do m <- gets sortSet

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder addDiags $ if Set.member s m then [] else

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder [mkDiag Error "unknown sort" s]

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian MaederaddSubsort :: SORT -> SORT -> State Env ()

986e0e9cf8c2358f455460b3fc75ce7c5dcf0973Christian MaederaddSubsort super sub =

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder do e <- get

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder mapM_ checkSort [super, sub]

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder put e { sortRel = Rel.insert sub super $ sortRel e }

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederaddVars :: VAR_DECL -> State Env ()

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian MaederaddVars (Var_decl vs s _) = mapM_ (addVar s) vs

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian MaederaddVar :: SORT -> SIMPLE_ID -> State Env ()

5ba323da9f037264b4a356085e844889aedeac23Christian MaederaddVar s v =

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder do e <- get

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let m = varMap e

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder l = Map.findWithDefault Set.empty v m

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder if Set.member s l then

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder addDiags [mkDiag Hint "redeclared var" v]

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder else put e { varMap = Map.insert v (Set.insert s l) m }

0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder

59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedercheckPlaces :: [SORT] -> Id -> [Diagnosis]

59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedercheckPlaces args i =

0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder if let n = placeCount i in n == 0 || n == length args then []

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder else [mkDiag Error "wrong number of places" i]

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederaddOp :: OpType -> Id -> State Env ()

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederaddOp ty i =

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder do mapM_ checkSort (opRes ty : opArgs ty)

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder e <- get

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let m = opMap e

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder l = Map.findWithDefault Set.empty i m

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder check = addDiags $ checkPlaces (opArgs ty) i

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder store = do put e { opMap = Map.insert i (Set.insert ty l) m }

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder if Set.member ty l then

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder addDiags [mkDiag Hint "redeclared op" i]

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder else case opKind ty of

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Partial -> if Set.member ty {opKind = Total} l then

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder addDiags [mkDiag Warning "partially redeclared" i]

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder else store >> check

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Total -> do store

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder if Set.member ty {opKind = Partial} l then

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder addDiags [mkDiag Hint "redeclared as total" i]

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder else check

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

ad187062b0009820118c1b773a232e29b879a2faChristian MaederaddPred :: PredType -> Id -> State Env ()

ad187062b0009820118c1b773a232e29b879a2faChristian MaederaddPred ty i =

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder do mapM_ checkSort $ predArgs ty

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder e <- get

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder let m = predMap e

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder l = Map.findWithDefault Set.empty i m

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder if Set.member ty l then

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder addDiags [mkDiag Hint "redeclared pred" i]

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder else do put e { predMap = Map.insert i (Set.insert ty l) m }

da5ddac3b07f5910940727d765a4431b8c17cdbbChristian Maeder addDiags $ checkPlaces (predArgs ty) i

997c56f3bc74a703043010978e5013fdb074d659Christian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederallOpIds :: Env -> Set.Set Id

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederallOpIds = Set.fromDistinctAscList . Map.keys . opMap

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

8485da94b57d8b5135ee685b55c982b037ed4140Christian MaederformulaIds :: Env -> Set.Set Id

8485da94b57d8b5135ee685b55c982b037ed4140Christian MaederformulaIds e =

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Set.fromDistinctAscList (map simpleIdToId $ Map.keys $ varMap e)

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder `Set.union` allOpIds e

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederallPredIds :: Env -> Set.Set Id

ad187062b0009820118c1b773a232e29b879a2faChristian MaederallPredIds = Set.fromDistinctAscList . Map.keys . predMap

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederaddDiags :: [Diagnosis] -> State Env ()

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederaddDiags ds =

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder do e <- get

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder put e { envDiags = ds ++ envDiags e }

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian MaederaddSentences :: [Named FORMULA] -> State Env ()

53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddSentences ds =

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder do e <- get

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder put e { sentences = ds ++ sentences e }

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- * traversing all data types of the abstract syntax

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederana_BASIC_SPEC :: GlobalAnnos -> BASIC_SPEC -> State Env BASIC_SPEC

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederana_BASIC_SPEC ga (Basic_spec al) = fmap Basic_spec $

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder mapAnM (ana_BASIC_ITEMS ga) al

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- looseness of a datatype

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maederdata GenKind = Free | Generated | Loose deriving (Show, Eq, Ord)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederana_BASIC_ITEMS :: GlobalAnnos -> BASIC_ITEMS -> State Env BASIC_ITEMS

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maederana_BASIC_ITEMS ga bi =

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder case bi of

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Sig_items sis -> fmap Sig_items $ ana_SIG_ITEMS ga Loose sis

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder Free_datatype al _ ->

f6f2955769bfe80dbb4cca3b3ee33c5a8a0f5355Christian Maeder do let sorts = map (( \ (Datatype_decl s _ _) -> s) . item) al

c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian Maeder mapM_ addSort sorts

fce77b2785912d1abbcc3680088b235f534bdeffChristian Maeder mapAnM (ana_DATATYPE_DECL Free) al

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder return bi

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Sort_gen al ps ->

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder do ul <- mapAnM (ana_SIG_ITEMS ga Generated) al

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder return $ Sort_gen ul ps

ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder Var_items il _ ->

039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder do mapM_ addVars il

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder return bi

3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder Local_var_axioms il afs ps ->

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do e <- get -- save

039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder mapM_ addVars il

ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder ops <- gets formulaIds

3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder put e -- restore

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder preds <- gets allPredIds

021d7137df04ec1834911d99d90243a092841cedChristian Maeder let rfs = map (resolveFormula ga ops preds . item) afs

021d7137df04ec1834911d99d90243a092841cedChristian Maeder ds = concatMap diags rfs

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder arfs = zipWith ( \ a m -> case maybeResult m of

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder Nothing -> Nothing

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Just f -> Just a { item = f }) afs rfs

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder ufs = catMaybes arfs

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder fufs = map ( \ a -> a { item = Quantification Universal il

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder (item a) ps } ) ufs

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder sens = map ( \ a -> NamedSen (getRLabel a) $ item a) fufs

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder addDiags ds

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder addSentences sens

adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder return $ Local_var_axioms il ufs ps

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder Axiom_items afs ps ->

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do ops <- gets formulaIds

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder preds <- gets allPredIds

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder let rfs = map (resolveFormula ga ops preds . item) afs

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder ds = concatMap diags rfs

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder arfs = zipWith ( \ a m -> case maybeResult m of

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder Nothing -> Nothing

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder Just f -> Just a { item = f }) afs rfs

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder ufs = catMaybes arfs

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder sens = map ( \ a -> NamedSen (getRLabel a) $ item a) ufs

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder addDiags ds

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder addSentences sens

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return $ Axiom_items ufs ps

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederana_SIG_ITEMS :: GlobalAnnos -> GenKind -> SIG_ITEMS -> State Env SIG_ITEMS

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederana_SIG_ITEMS ga gk si =

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder case si of

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder Sort_items al ps ->

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do ul <- mapAnM (ana_SORT_ITEM ga) al

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return $ Sort_items ul ps

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Op_items al ps ->

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do ul <- mapAnM (ana_OP_ITEM ga) al

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return $ Op_items ul ps

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder Pred_items al ps ->

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do ul <- mapAnM (ana_PRED_ITEM ga) al

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return $ Pred_items ul ps

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder Datatype_items al _ ->

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do let sorts = map (( \ (Datatype_decl s _ _) -> s) . item) al

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder mapM_ addSort sorts

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder mapAnM (ana_DATATYPE_DECL gk) al

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder return si

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maederana_SORT_ITEM :: GlobalAnnos -> SORT_ITEM -> State Env SORT_ITEM

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederana_SORT_ITEM ga si =

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder case si of

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Sort_decl il _ ->

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder do mapM_ addSort il

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder return si

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder Subsort_decl il i _ ->

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder do mapM_ addSort (i:il)

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder mapM_ (addSubsort i) il

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder return si

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder Subsort_defn sub v super af ps ->

bb3bdd4a260606a6184b5f5a5774ca6632ca597aChristian Maeder do addSort sub

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder ops <- gets allOpIds

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder preds <- gets allPredIds

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder let Result ds mf = resolveFormula ga

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder (Set.insert (simpleIdToId v) ops) preds $ item af

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder addDiags ds

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder addSubsort super sub

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder return $ case mf of

Nothing -> Subsort_decl [sub] super ps

Just f -> Subsort_defn sub v super af { item = f } ps

Iso_decl il _ ->

do mapM_ addSort il

mapM_ ( \ i -> mapM_ (addSubsort i) il) il

return si

toOpType :: OP_TYPE -> OpType

toOpType (Total_op_type args r _) = OpType Total args r

toOpType (Partial_op_type args r _) = OpType Partial args r

ana_OP_ITEM :: GlobalAnnos -> OP_ITEM -> State Env OP_ITEM

ana_OP_ITEM ga oi =

case oi of

Op_decl ops ty il ps ->

do mapM_ (addOp $ toOpType ty) ops

ul <- mapM (ana_OP_ATTR ga) il

return $ Op_decl ops ty (catMaybes ul) ps

Op_defn i par at ps ->

do let ty = headToType par

addOp (toOpType ty) i

ops <- gets allOpIds

preds <- gets allPredIds

let vars = headToVars par

allOps = foldr ( \ v s -> Set.insert (simpleIdToId v) s)

ops vars

Result ds mt = resolveMixfix ga allOps preds False $ item at

addDiags ds

return $ case mt of

Nothing -> Op_decl [i] ty [] ps

Just t -> Op_defn i par at { item = t } ps

where

headToType :: OP_HEAD -> OP_TYPE

headToType (Total_op_head args r ps) =

Total_op_type (sortsOfArgs args) r ps

headToType (Partial_op_head args r ps) =

Partial_op_type (sortsOfArgs args) r ps

headToVars :: OP_HEAD -> [VAR]

headToVars h =

let as = case h of

Total_op_head args _ _ -> args

Partial_op_head args _ _ -> args

in concatMap ( \ (Arg_decl v _ _) -> v) as

sortsOfArgs :: [ARG_DECL] -> [SORT]

sortsOfArgs = concatMap ( \ (Arg_decl l s _) -> map (const s) l)

ana_OP_ATTR :: GlobalAnnos -> OP_ATTR -> State Env (Maybe OP_ATTR)

ana_OP_ATTR ga oa =

case oa of

Unit_op_attr t ->

do ops <- gets allOpIds

preds <- gets allPredIds

let Result ds mt = resolveMixfix ga ops preds False t

addDiags ds

return $ fmap Unit_op_attr mt

_ -> return $ Just oa

toPredType :: PRED_TYPE -> PredType

toPredType (Pred_type args _) = PredType args

ana_PRED_ITEM :: GlobalAnnos -> PRED_ITEM -> State Env PRED_ITEM

ana_PRED_ITEM ga p =

case p of

Pred_decl preds ty _ ->

do mapM (addPred $ toPredType ty) preds

return p

Pred_defn i par at ps ->

do let ty = predHeadToType par

addPred (toPredType ty) i

ops <- gets allOpIds

preds <- gets allPredIds

let vars = predHeadToVars par

allOps = foldr ( \ v s -> Set.insert (simpleIdToId v) s)

ops vars

Result ds mt = resolveFormula ga allOps preds $ item at

addDiags ds

return $ case mt of

Nothing -> Pred_decl [i] ty ps

Just t -> Pred_defn i par at { item = t } ps

where

predHeadToType :: PRED_HEAD -> PRED_TYPE

predHeadToType (Pred_head args ps) =

Pred_type (sortsOfArgs args) ps

predHeadToVars :: PRED_HEAD -> [VAR]

predHeadToVars (Pred_head args _) =

concatMap ( \ (Arg_decl v _ _) -> v) args

-- full function type of a selector (result sort is component sort)

data Component = Component { compId :: Id, compType :: OpType }

deriving (Show)

instance Eq Component where

Component i1 t1 == Component i2 t2 =

(i1, opArgs t1, opRes t1) == (i2, opArgs t2, opRes t2)

instance Ord Component where

Component i1 t1 <= Component i2 t2 =

(i1, opArgs t1, opRes t1) <= (i2, opArgs t2, opRes t2)

instance PrettyPrint Component where

printText0 ga (Component i ty) =

printText0 ga i <+> colon <> printText0 ga ty

instance PosItem Component where

get_pos = Just . posOfId . compId

-- full function type of constructor (result sort is the data type)

data Alternative = Construct Id OpType [Component]

deriving (Show, Eq)

ana_DATATYPE_DECL :: GenKind -> DATATYPE_DECL -> State Env ()

ana_DATATYPE_DECL _gk (Datatype_decl s al _) =

-- GenKind currently unused

do ul <- mapM (ana_ALTERNATIVE s . item) al

let constr = catMaybes ul

if null constr then return ()

else do addDiags $ checkUniqueness $ map fst constr

let totalSels = Set.unions $ map snd constr

wrongConstr = filter ((totalSels /=) . snd) constr

addDiags $ map ( \ (c, _) -> mkDiag Error

("total selectors '" ++ showSepList (showString ",")

showPretty (Set.toList totalSels)

"'\n\tmust appear in alternative") c) wrongConstr

ana_ALTERNATIVE :: SORT -> ALTERNATIVE

-> State Env (Maybe (Component, Set.Set Component))

ana_ALTERNATIVE s c =

case c of

Subsorts ss _ ->

do mapM_ (addSubsort s) ss

return Nothing

_ -> do let (part, i, il) = case c of

Total_construct a l _ -> (Total, a, l)

Partial_construct a l _ -> (Partial, a, l)

_ -> error "ana_ALTERNATIVE"

ty = OpType part (concatMap compSort il) s

addOp ty i

ul <- mapM (ana_COMPONENTS s) il

let ts = concatMap fst ul

addDiags $ checkUniqueness (ts ++ concatMap snd ul)

return $ Just (Component i ty, Set.fromList ts)

where compSort :: COMPONENTS -> [SORT]

compSort (Total_select l cs _) = map (const cs) l

compSort (Partial_select l cs _) = map (const cs) l

compSort (Sort cs) = [cs]

ana_COMPONENTS :: SORT -> COMPONENTS -> State Env ([Component], [Component])

ana_COMPONENTS s c =

case c of

Sort _ -> return ([], [])

_ -> do let (part, is, cs) = case c of

Total_select as bs _ -> (Total, as, bs)

Partial_select as bs _ -> (Partial, as, bs)

_ -> error "ana_COMPONENTS"

ty = OpType part [s] cs

ts = map ( \ i -> Component i ty) is

mapM_ (addOp ty) is

return $ case part of

Total -> (ts, [])

Partial -> ([], ts)

-- wrap it all up for a logic

type Sign = Env -- ignoring vars, sentences and diags

type Sentence = FORMULA

emptySign :: Sign

emptySign = emptyEnv

basicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos)

-> Result (BASIC_SPEC,Sign,Sign,[Named Sentence])

basicAnalysis (bs, inSig, ga) =

let (newBs, accSig) = runState (ana_BASIC_SPEC ga bs) inSig

ds = envDiags accSig

sents = sentences accSig

cleanSig = accSig { envDiags = [], sentences = [], varMap = Map.empty }

diff = diffSig cleanSig inSig

remPartOpsS s = s { opMap = remPartOpsM $ opMap s }

in Result ds $ Just ( newBs

, remPartOpsS diff

, remPartOpsS cleanSig

, sents )

diffSig :: Sign -> Sign -> Sign

diffSig a b =

a { sortSet = sortSet a `Set.difference` sortSet b

, sortRel = fromSet $ Set.difference

(toSet $ sortRel a) $ toSet $ sortRel b

, opMap = opMap a `diffMapSet` opMap b

, predMap = predMap a `diffMapSet` predMap b

}

diffMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b)

-> Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)

diffMapSet =

Map.differenceWith ( \ s t -> let d = Set.difference s t in

if Set.isEmpty d then Nothing

else Just d )

toSet :: (Ord a) => Rel.Rel a -> Set.Set (a, a)

toSet = Set.fromList . Rel.toList

fromSet :: (Ord a) => Set.Set (a, a) -> Rel.Rel a

fromSet = Rel.fromList . Set.toList

addSig :: Sign -> Sign -> Sign

addSig a b =

a { sortSet = sortSet a `Set.union` sortSet b

, sortRel = fromSet $ Set.union

(toSet $ sortRel a) $ toSet $ sortRel b

, opMap = remPartOpsM $ Map.unionWith Set.union (opMap a) $ opMap b

, predMap = Map.unionWith Set.union (predMap a) $ predMap b

}

isEmptySig :: Sign -> Bool

isEmptySig s =

Set.isEmpty (sortSet s) &&

Rel.isEmpty (sortRel s) &&

Map.isEmpty (opMap s) &&

Map.isEmpty (predMap s)

isSubSig :: Sign -> Sign -> Bool

isSubSig sub super = isEmptySig $ diffSig sub super

{ opMap = addPartOpsM $ opMap super }

partOps :: Set.Set OpType -> Set.Set OpType

partOps s = Set.fromDistinctAscList $ map ( \ t -> t { opKind = Partial } )

$ Set.toList $ Set.filter ((==Total) . opKind) s

remPartOps :: Set.Set OpType -> Set.Set OpType

remPartOps s = s Set.\\ partOps s

remPartOpsM :: Ord a => Map.Map a (Set.Set OpType)

-> Map.Map a (Set.Set OpType)

remPartOpsM = Map.map remPartOps

addPartOps :: Set.Set OpType -> Set.Set OpType

addPartOps s = Set.union s $ partOps s

addPartOpsM :: Ord a => Map.Map a (Set.Set OpType)

-> Map.Map a (Set.Set OpType)

addPartOpsM = Map.map addPartOps

toOP_TYPE :: OpType -> OP_TYPE

toOP_TYPE OpType { opArgs = args, opRes = res, opKind = k } =

(case k of

Total -> Total_op_type

Partial -> Partial_op_type) args res []

toPRED_TYPE :: PredType -> PRED_TYPE

toPRED_TYPE PredType { predArgs = args } = Pred_type args []

instance PrettyPrint OpType where

printText0 ga ot = printText0 ga $ toOP_TYPE ot

instance PrettyPrint PredType where

printText0 ga pt = printText0 ga $ toPRED_TYPE pt

instance PrettyPrint Sign where

printText0 ga s =

ptext "sorts" <+> commaT_text ga (Set.toList $ sortSet s)

$$

(if Rel.isEmpty (sortRel s) then empty

else ptext "sorts" <+>

(vcat $ map printRel $ Map.toList $ Rel.toMap $ sortRel s))

$$

vcat (map (\ (i, t) ->

ptext "op" <+>

printText0 ga i <+> colon <>

printText0 ga t)

$ concatMap (\ (o, ts) ->

map ( \ ty -> (o, ty) ) $ Set.toList ts)

$ Map.toList $ opMap s)

$$

vcat (map (\ (i, t) ->

ptext "pred" <+>

printText0 ga i <+> colon <+>

printText0 ga (toPRED_TYPE t))

$ concatMap (\ (o, ts) ->

map ( \ ty -> (o, ty) ) $ Set.toList ts)

$ Map.toList $ predMap s)

where printRel (s,subsorts) =

printText0 ga s <+> ptext "<" <+> printSet ga subsorts