6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder{- |

6596e6462e9356ac01f15a6dcada971e1f346b63Christian MaederModule : $Header$

6596e6462e9356ac01f15a6dcada971e1f346b63Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2004

6596e6462e9356ac01f15a6dcada971e1f346b63Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian MaederMaintainer : till@tzi.de

6596e6462e9356ac01f15a6dcada971e1f346b63Christian MaederStability : provisional

96e54b22ad432d658ba790f3800ee8ea2657449fChristian MaederPortability : portable

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder static analysis for CoCASL

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder-}

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder{- todo:

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder correct map_C_FORMULA, getCoDataGenSig

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder-}

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maedermodule CoCASL.StatAna where

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder--import Debug.Trace

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maederimport CoCASL.AS_CoCASL

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport CoCASL.Print_AS

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport CoCASL.CoCASLSign

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport CASL.Sign

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport CASL.MixfixParser

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport CASL.StaticAna

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport CASL.AS_Basic_CASL

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport CASL.Overload

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport CASL.MapSentence

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport Common.AS_Annotation

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport qualified Common.Lib.Set as Set

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport Common.Lib.State

b82427a46050fa32553e722daedf6a364a14f217Christian Maederimport Common.Id

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport Common.Result

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport Data.Maybe

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederimport Data.List

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maedertype CSign = Sign C_FORMULA CoCASLSign

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

b82427a46050fa32553e722daedf6a364a14f217Christian MaederminExpForm :: Min C_FORMULA CoCASLSign

b82427a46050fa32553e722daedf6a364a14f217Christian MaederminExpForm ga s form =

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder let newGa = addAssocs ga s

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder ops = formulaIds s

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder preds = allPredIds s

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder res = resolveFormula newGa ops preds

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder minMod md ps = case md of

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder Term_mod t -> let

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder r = do

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder t1 <- resolveMixfix newGa (allOpIds s) preds False t

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder ts <- minExpTerm minExpForm ga s t1

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder t2 <- is_unambiguous t ts ps

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder let srt = term_sort t2

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder trm = Term_mod t2

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder if Set.member srt ops

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder then return trm

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder else Result [mkDiag Error

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder ("unknown modality '"

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder ++ showId srt "' for term") t ]

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder $ Just trm

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder in case t of

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder Mixfix_token tm ->

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder if Set.member (simpleIdToId tm) ops

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder then return $ Simple_mod tm

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder else case maybeResult r of

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder Nothing -> Result

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder [mkDiag Error "unknown modality" tm]

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder $ Just $ Simple_mod tm

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder _ -> r

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder _ -> r

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder in case form of

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder Box m f ps ->

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder do nm <- minMod m ps

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder f1 <- res f

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder f2 <- minExpFORMULA minExpForm ga s f1

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder return $ Box nm f2 ps

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder Diamond m f ps ->

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder do nm <- minMod m ps

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder f1 <- res f

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder f2 <- minExpFORMULA minExpForm ga s f1

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder return $ Diamond nm f2 ps

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder phi -> return phi

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

96e54b22ad432d658ba790f3800ee8ea2657449fChristian Maederana_C_SIG_ITEM :: Ana C_SIG_ITEM C_FORMULA CoCASLSign

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederana_C_SIG_ITEM ga mi =

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder case mi of

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder CoDatatype_items al _ ->

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder do let sorts = map (( \ (CoDatatype_decl s _ _) -> s) . item) al

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder mapM_ addSort sorts

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder mapAnM (ana_CODATATYPE_DECL Loose) al

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder closeSubsortRel

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder return mi

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder-- | return list of constructors

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederana_CODATATYPE_DECL :: GenKind -> CODATATYPE_DECL -> State CSign [Component]

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederana_CODATATYPE_DECL gk (CoDatatype_decl s al _) =

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder do ul <- mapM (ana_COALTERNATIVE s . item) al

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder let constr = catMaybes ul

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder cs = map fst constr

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder if null constr then return ()

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder else do addDiags $ checkUniqueness cs

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder let totalSels = Set.unions $ map snd constr

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder wrongConstr = filter ((totalSels /=) . snd) constr

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

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder ("total selectors '" ++ showSepList (showString ",")

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder showPretty (Set.toList totalSels)

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder "'\n\tmust appear in alternative") c) wrongConstr

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder case gk of

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder Free -> do

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder let allts = map item al

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder (alts, subs) = partition ( \ a -> case a of

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder CoSubsorts _ _ -> False

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder _ -> True) allts

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder sbs = concatMap ( \ (CoSubsorts ss _) -> ss) subs

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder comps = map (getCoConsType s) alts

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder ttrips = map ( \ (a, vs, t, ses) -> (a, vs, t, catSels ses))

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder $ catMaybes $ map (coselForms1 "X") $ comps

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder sels = concatMap ( \ (_, _, _, ses) -> ses) ttrips

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder addSentences $ catMaybes $ map comakeInjective

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder $ filter ( \ (_, _, ces) -> not $ null ces)

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder comps

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder addSentences $ catMaybes $ concatMap ( \ as -> map (comakeDisjToSort as) sbs)

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder comps

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder addSentences $ comakeDisjoint comps

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder addSentences $ catMaybes $ concatMap

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder ( \ ses ->

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder map (makeUndefForm ses) ttrips) sels

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder _ -> return ()

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder return cs

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian MaedergetCoConsType :: SORT -> COALTERNATIVE -> (Maybe Id, OpType, [COCOMPONENTS])

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian MaedergetCoConsType s c =

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder let (part, i, il) = case c of

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder CoSubsorts _ _ -> error "getConsType"

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder CoTotal_construct a l _ -> (Total, a, l)

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder CoPartial_construct a l _ -> (Partial, a, l)

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder in (i, OpType part (concatMap

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder (map (opRes . snd) . getCoCompType s) il) s, il)

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian MaedergetCoCompType :: SORT -> COCOMPONENTS -> [(Maybe Id, OpType)]

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian MaedergetCoCompType s (CoTotal_select l cs _) =

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder map (\ i -> (Just i, OpType Total [s] cs)) l

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian MaedergetCoCompType s (CoPartial_select l cs _) =

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder map (\ i -> (Just i, OpType Partial [s] cs)) l

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian MaedercoselForms :: (Maybe Id, OpType, [COCOMPONENTS]) -> [Named (FORMULA f)]

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian MaedercoselForms x =

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder case coselForms1 "X" x of

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder Nothing -> []

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder Just y -> makeSelForms 1 y

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian MaedercoselForms1 :: String -> (Maybe Id, OpType, [COCOMPONENTS])

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder -> Maybe (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian MaedercoselForms1 str (Nothing, ty, il) = Nothing

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian MaedercoselForms1 str (Just i, ty, il) =

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder let cs = concatMap (getCoCompType $ opRes ty) il

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder vs = genSelVars str 1 cs

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder in Just $ (i, vs, Application (Qual_op_name i (toOP_TYPE ty) [])

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder (map toQualVar vs) [], cs)

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian MaedercomakeDisjToSort :: (Maybe Id, OpType, [COCOMPONENTS]) -> SORT

fe4d24dddce1322bd8dd24debcca4fec950eb873Christian Maeder -> Maybe (Named (FORMULA f))

6596e6462e9356ac01f15a6dcada971e1f346b63Christian MaedercomakeDisjToSort a s = do

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder (c, v, t, _) <- coselForms1 "X" a

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder let p = [posOfId s]

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder return $ NamedSen ("ga_disjoint_" ++ showId c "_sort_" ++ showId s "") $

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder mkForall v (Negation (Membership t s p) p) p

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian MaedercomakeInjective :: (Maybe Id, OpType, [COCOMPONENTS])

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder -> Maybe (Named (FORMULA f))

6596e6462e9356ac01f15a6dcada971e1f346b63Christian MaedercomakeInjective a = do

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder (c, v1, t1, _) <- coselForms1 "X" a

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder (_, v2, t2, _) <- coselForms1 "Y" a

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder let p = [posOfId c]

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder return $ NamedSen ("ga_injective_" ++ showId c "") $

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder mkForall (v1 ++ v2)

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder (Equivalence (Strong_equation t1 t2 p)

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder (let ces = zipWith ( \ w1 w2 -> Strong_equation

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder (toQualVar w1) (toQualVar w2) p) v1 v2

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder in if isSingle ces then head ces else Conjunction ces p)

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder p) p

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian MaedercomakeDisjoint :: [(Maybe Id, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)]

6596e6462e9356ac01f15a6dcada971e1f346b63Christian MaedercomakeDisjoint [] = []

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian MaedercomakeDisjoint (a:as) = catMaybes (map (comakeDisj a) as) ++ comakeDisjoint as

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian MaedercomakeDisj :: (Maybe Id, OpType, [COCOMPONENTS])

b82427a46050fa32553e722daedf6a364a14f217Christian Maeder -> (Maybe Id, OpType, [COCOMPONENTS])

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder -> Maybe (Named (FORMULA f))

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian MaedercomakeDisj a1 a2 = do

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder (c1, v1, t1, _) <- coselForms1 "X" a1

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder (c2, v2, t2, _) <- coselForms1 "Y" a2

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder let p = [posOfId c1, posOfId c2]

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maeder return $ NamedSen ("ga_disjoint_" ++ showId c1 "_" ++ showId c2 "") $

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder mkForall (v1 ++ v2)

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder (Negation (Strong_equation t1 t2 p) p) p

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder-- | return the constructor and the set of total selectors

bc8dfa8d893d6ba015300cba3960c061ff7a8760Christian Maederana_COALTERNATIVE :: SORT -> COALTERNATIVE

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder -> State CSign (Maybe (Component, Set.Set Component))

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maederana_COALTERNATIVE s c =

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder case c of

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder CoSubsorts ss _ ->

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder do mapM_ (addSubsort s) ss

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder return Nothing

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder _ -> do let cons@(i, ty, il) = getCoConsType s c

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder case i of

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder Nothing -> return Nothing

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder Just i' -> do

6596e6462e9356ac01f15a6dcada971e1f346b63Christian Maeder addOp ty i'

ul <- mapM (ana_COCOMPONENTS s) il

let ts = concatMap fst ul

addDiags $ checkUniqueness (ts ++ concatMap snd ul)

addSentences $ coselForms cons

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

-- | return total and partial selectors

ana_COCOMPONENTS :: SORT -> COCOMPONENTS

-> State CSign ([Component], [Component])

ana_COCOMPONENTS s c = do

let cs = getCoCompType s c

sels <- mapM ( \ (mi, ty) ->

case mi of

Nothing -> return Nothing

Just i -> do addOp ty i

return $ Just $ Component i ty) cs

return $ partition ((==Total) . opKind . compType) $ catMaybes sels

ana_C_BASIC_ITEM :: Ana C_BASIC_ITEM C_FORMULA CoCASLSign

ana_C_BASIC_ITEM ga bi = do

case bi of

CoFree_datatype al ps ->

do let sorts = map (( \ (CoDatatype_decl s _ _) -> s) . item) al

mapM_ addSort sorts

mapAnM (ana_CODATATYPE_DECL Free) al

toCoSortGenAx ps True $ getCoDataGenSig al

closeSubsortRel

return bi

CoSort_gen al ps ->

do (gs,ul) <- ana_CoGenerated ana_C_SIG_ITEM ga al

toCoSortGenAx ps False

(Set.unions $ map fst gs, Set.unions $ map snd gs)

return $ CoSort_gen ul ps

toCoSortGenAx :: [Pos] -> Bool ->

(Set.Set Id, Set.Set Component) -> State CSign ()

toCoSortGenAx ps isFree (sorts, ops) = do

let sortList = Set.toList sorts

opSyms = map ( \ c -> Qual_op_name (compId c)

(toOP_TYPE $ compType c) []) $ Set.toList ops

resType _ (Op_name _) = False

resType s (Qual_op_name _ t _) = res_OP_TYPE t ==s

getIndex s = maybe (-1) id $ findIndex (==s) sortList

addIndices (Op_name _) =

error "CoCASL/StaticAna: Internal error in function addIndices"

addIndices os@(Qual_op_name _ t _) =

(os,map getIndex $ args_OP_TYPE t)

collectOps s =

Constraint s (map addIndices $ filter (resType s) opSyms) s

constrs = map collectOps sortList

f = ExtFORMULA $ CoSort_gen_ax constrs isFree

if null sortList then

addDiags[Diag Error "missing cogenerated sort" (headPos ps)]

else return ()

addSentences [NamedSen ("ga_cogenerated_" ++

showSepList (showString "_") showId sortList "") f]

ana_CoGenerated as ga al = do

ul <- mapAnM (ana_SIG_ITEMS as ga Generated) al

return (map (getCoGenSig . item) ul,ul)

getCoGenSig :: SIG_ITEMS C_SIG_ITEM C_FORMULA

-> (Set.Set Id, Set.Set Component)

getCoGenSig si = case si of

Sort_items al _ -> (Set.unions (map (getSorts . item) al), Set.empty)

Op_items al _ -> (Set.empty, Set.unions (map (getOps . item) al))

Datatype_items dl _ -> getDataGenSig dl

Ext_SIG_ITEMS (CoDatatype_items dl _) -> getCoDataGenSig dl

_ -> (Set.empty, Set.empty)

getCoDataGenSig :: [Annoted CODATATYPE_DECL] -> (Set.Set Id, Set.Set Component)

getCoDataGenSig dl =

let alts = map (( \ (CoDatatype_decl s al _) -> (s, al)) . item) dl

sorts = map fst alts

cs = catMaybes $ concatMap ( \ (s, al) -> map (( \ a ->

let (i, ty, _) = getCoConsType s a

in maybe Nothing (\j -> Just $ Component j ty) i))

$ filter ( \ a ->

case a of

CoSubsorts _ _ -> False

_ -> True)

$ map item al) alts

in (Set.fromList sorts, Set.fromList cs)

resultToState :: (a -> Result a) -> a -> State (Sign f e) a

resultToState f a = do

let r = f a

addDiags $ reverse $ diags r

case maybeResult r of

Nothing -> return a

Just b -> return b

map_C_FORMULA :: MapSen C_FORMULA CoCASLSign ()

map_C_FORMULA mor frm =

let mapMod m = case m of

Simple_mod _ -> return m

Term_mod t -> do newT <- mapTerm map_C_FORMULA mor t

return $ Term_mod newT

in case frm of

Box m f ps -> do

newF <- mapSen map_C_FORMULA mor f

newM <- mapMod m

return $ Box newM newF ps

Diamond m f ps -> do

newF <- mapSen map_C_FORMULA mor f

newM <- mapMod m

return $ Diamond newM newF ps

phi -> return phi