StatAna.hs revision e071fb22ea9923a2a4ff41184d80ca46b55ee932
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyModule : $Header$
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyDescription : static analysis for CoCASL
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyCopyright : (c) Till Mossakowski, Uni Bremen 2004-2005
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : hausmann@informatik.uni-bremen.de
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyStability : provisional
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyPortability : portable
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillystatic analysis for CoCASL
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederimport qualified Data.Set as Set
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederimport qualified Data.Map as Map
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederimport qualified Common.Lib.Rel as Rel
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederimport Data.Maybe (catMaybes)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport Data.List (partition)
036ecbd8f721096321f47cf6a354a9d1bf3d032fChristian Maedertype CSign = Sign C_FORMULA CoCASLSign
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederbasicCoCASLAnalysis :: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly Sign C_FORMULA CoCASLSign, GlobalAnnos)
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly -> Result (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly Sign C_FORMULA CoCASLSign,
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly [Named (FORMULA C_FORMULA)])
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillybasicCoCASLAnalysis =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly basicAnalysis minExpForm ana_C_BASIC_ITEM ana_C_SIG_ITEM ana_CMix
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederana_CMix :: Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederana_CMix = emptyMix
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder { getBaseIds = ids_C_BASIC_ITEM
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , getSigIds = ids_C_SIG_ITEM
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , getExtIds = \ e -> mkIdSets (Map.keysSet $ constructors e) Set.empty
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , putParen = mapC_FORMULA
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , mixResolve = resolveC_FORMULA
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , checkMix = noExtMixfixCo
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , putInj = injC_FORMULA }
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederids_C_BASIC_ITEM :: C_BASIC_ITEM -> IdSets
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maederids_C_BASIC_ITEM ci = case ci of
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder CoFree_datatype al _ ->
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder (Set.unions $ map (ids_CODATATYPE_DECL . item) al, Set.empty)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly CoSort_gen al _ -> unite $ map (ids_SIG_ITEMS ids_C_SIG_ITEM . item) al
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyids_C_SIG_ITEM :: C_SIG_ITEM -> IdSets
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederids_C_SIG_ITEM (CoDatatype_items al _) =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Set.unions $ map (ids_CODATATYPE_DECL . item) al, Set.empty)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederids_CODATATYPE_DECL :: CODATATYPE_DECL -> Set.Set Id
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maederids_CODATATYPE_DECL (CoDatatype_decl _ al _) =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Set.unions $ map (ids_COALTERNATIVE . item) al
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyids_COALTERNATIVE :: COALTERNATIVE -> Set.Set Id
fa373bc327620e08861294716b4454be8d25669fChristian Maederids_COALTERNATIVE a = case a of
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Co_construct _ mi cs _ -> Set.unions $
fa373bc327620e08861294716b4454be8d25669fChristian Maeder maybe Set.empty single mi : map ids_COCOMPONENTS cs
fa373bc327620e08861294716b4454be8d25669fChristian Maeder CoSubsorts _ _ -> Set.empty
fa373bc327620e08861294716b4454be8d25669fChristian Maederids_COCOMPONENTS :: COCOMPONENTS -> Set.Set Id
fa373bc327620e08861294716b4454be8d25669fChristian Maederids_COCOMPONENTS (CoSelect l _ _) = Set.unions $ map single l
fa373bc327620e08861294716b4454be8d25669fChristian Maederdata CoRecord a b c d = CoRecord
fa373bc327620e08861294716b4454be8d25669fChristian Maeder { foldBoxOrDiamond :: C_FORMULA -> Bool -> d -> a -> Range -> c
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , foldCoSort_gen_ax :: C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> c
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , foldTerm_mod :: MODALITY -> b -> d
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , foldSimple_mod :: MODALITY -> SIMPLE_ID -> d
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian MaederfoldC_Formula :: Record C_FORMULA a b -> CoRecord a b c d -> C_FORMULA -> c
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian MaederfoldC_Formula r cr c = case c of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly BoxOrDiamond b m f ps ->
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder foldBoxOrDiamond cr c b (foldModality r cr m) (foldFormula r f) ps
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder CoSort_gen_ax s o b -> foldCoSort_gen_ax cr c s o b
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederfoldModality :: Record C_FORMULA a b -> CoRecord a b c d -> MODALITY -> d
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederfoldModality r cr m = case m of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Term_mod t -> foldTerm_mod cr m $ foldTerm r t
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Simple_mod i -> foldSimple_mod cr m i
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapCoRecord :: CoRecord (FORMULA C_FORMULA) (TERM C_FORMULA) C_FORMULA MODALITY
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapCoRecord = CoRecord
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder { foldBoxOrDiamond = \ _ -> BoxOrDiamond
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , foldCoSort_gen_ax = \ _ -> CoSort_gen_ax
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , foldTerm_mod = \ _ -> Term_mod
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , foldSimple_mod = \ _ -> Simple_mod
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaederconstCoRecord :: ([a] -> a) -> a -> CoRecord a a a a
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaederconstCoRecord join c = CoRecord
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder { foldBoxOrDiamond = \ _ _ m f _ -> join [m, f]
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , foldCoSort_gen_ax = \ _ _ _ _ -> c
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder , foldTerm_mod = \ _ t -> t
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , foldSimple_mod = \ _ _ -> c
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaedermapC_FORMULA :: C_FORMULA -> C_FORMULA
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedermapC_FORMULA = foldC_Formula (mkMixfixRecord mapC_FORMULA) mapCoRecord
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederinjC_FORMULA :: C_FORMULA -> C_FORMULA
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederinjC_FORMULA = foldC_Formula (injRecord injC_FORMULA) mapCoRecord
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederresolveMODALITY :: MixResolve MODALITY
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaederresolveMODALITY ga ids m = case m of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Term_mod t ->
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder fmap Term_mod $ resolveMixTrm mapC_FORMULA resolveC_FORMULA ga ids t
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder _ -> return m
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederresolveC_FORMULA :: MixResolve C_FORMULA
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederresolveC_FORMULA ga ids cf = case cf of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder BoxOrDiamond b m f ps -> do
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder nm <- resolveMODALITY ga ids m
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder nf <- resolveMixFrm mapC_FORMULA resolveC_FORMULA ga ids f
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder return $ BoxOrDiamond b nm nf ps
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder _ -> error "resolveC_FORMULA"
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaedernoExtMixfixCo :: C_FORMULA -> Bool
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaedernoExtMixfixCo =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder foldC_Formula (noMixfixRecord noExtMixfixCo) (constCoRecord and True)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederminExpForm :: Min C_FORMULA CoCASLSign
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederminExpForm s form =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder let ops = formulaIds s
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder minMod md ps = case md of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Term_mod t -> let
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder t2 <- oneExpTerm minExpForm s t
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder let srt = term_sort t2
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder trm = Term_mod t2
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder then return trm
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder else Result [mkDiag Error
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder ("unknown modality '"
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder ++ showId srt "' for term") t ]
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder Mixfix_token tm ->
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder if Set.member (simpleIdToId tm) ops
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder then return $ Simple_mod tm
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder else case maybeResult r of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Nothing -> Result
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder [mkDiag Error "unknown modality" tm]
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder $ Just $ Simple_mod tm
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly in case form of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder BoxOrDiamond b m f ps ->
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder do nm <- minMod m ps
fa373bc327620e08861294716b4454be8d25669fChristian Maeder f2 <- minExpFORMULA minExpForm s f
fa373bc327620e08861294716b4454be8d25669fChristian Maeder return $ BoxOrDiamond b nm f2 ps
fa373bc327620e08861294716b4454be8d25669fChristian Maeder phi -> return phi
fa373bc327620e08861294716b4454be8d25669fChristian Maederana_C_SIG_ITEM :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
fa373bc327620e08861294716b4454be8d25669fChristian Maederana_C_SIG_ITEM _ mi =
fa373bc327620e08861294716b4454be8d25669fChristian Maeder CoDatatype_items al _ ->
fa373bc327620e08861294716b4454be8d25669fChristian Maeder do mapM_ (\ i -> case item i of
fa373bc327620e08861294716b4454be8d25669fChristian Maeder CoDatatype_decl s _ _ -> addSort i s) al
fa373bc327620e08861294716b4454be8d25669fChristian Maeder mapAnM (ana_CODATATYPE_DECL Loose) al
fa373bc327620e08861294716b4454be8d25669fChristian Maeder closeSubsortRel
fa373bc327620e08861294716b4454be8d25669fChristian MaederisCoConsAlt :: COALTERNATIVE -> Bool
fa373bc327620e08861294716b4454be8d25669fChristian MaederisCoConsAlt a = case a of
fa373bc327620e08861294716b4454be8d25669fChristian Maeder CoSubsorts _ _ -> False
fa373bc327620e08861294716b4454be8d25669fChristian MaedergetCoSubsorts :: COALTERNATIVE -> [SORT]
fa373bc327620e08861294716b4454be8d25669fChristian MaedergetCoSubsorts c = case c of
fa373bc327620e08861294716b4454be8d25669fChristian Maeder CoSubsorts cs _ -> cs
fa373bc327620e08861294716b4454be8d25669fChristian Maeder-- | return list of constructors
fa373bc327620e08861294716b4454be8d25669fChristian Maederana_CODATATYPE_DECL :: GenKind -> CODATATYPE_DECL -> State CSign [Component]
fa373bc327620e08861294716b4454be8d25669fChristian Maederana_CODATATYPE_DECL gk (CoDatatype_decl s al _) =
fa373bc327620e08861294716b4454be8d25669fChristian Maeder do ul <- mapM (ana_COALTERNATIVE s) al
fa373bc327620e08861294716b4454be8d25669fChristian Maeder let constr = catMaybes ul
fa373bc327620e08861294716b4454be8d25669fChristian Maeder cs = map fst constr
fa373bc327620e08861294716b4454be8d25669fChristian Maeder if null constr then return ()
fa373bc327620e08861294716b4454be8d25669fChristian Maeder else do addDiags $ checkUniqueness cs
fa373bc327620e08861294716b4454be8d25669fChristian Maeder let totalSels = Set.unions $ map snd constr
fa373bc327620e08861294716b4454be8d25669fChristian Maeder wrongConstr = filter ((totalSels /=) . snd) constr
fa373bc327620e08861294716b4454be8d25669fChristian Maeder addDiags $ map ( \ (c, _) -> mkDiag Error
fa373bc327620e08861294716b4454be8d25669fChristian Maeder ("total selectors '" ++ showSepList (showString ",")
fa373bc327620e08861294716b4454be8d25669fChristian Maeder showDoc (Set.toList totalSels)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder "'\n must appear in alternative") c) wrongConstr
fa373bc327620e08861294716b4454be8d25669fChristian Maeder let (alts, subs) = partition isCoConsAlt $ map item al
fa373bc327620e08861294716b4454be8d25669fChristian Maeder sbs = concatMap getCoSubsorts subs
fa373bc327620e08861294716b4454be8d25669fChristian Maeder comps = map (getCoConsType s) alts
fa373bc327620e08861294716b4454be8d25669fChristian Maeder ttrips = map ( \ (a, vs, ses) -> (a, vs, catSels ses))
fa373bc327620e08861294716b4454be8d25669fChristian Maeder $ map (coselForms1 "X") $ comps
fa373bc327620e08861294716b4454be8d25669fChristian Maeder sels = concatMap ( \ (_, _, ses) -> ses) ttrips
fa373bc327620e08861294716b4454be8d25669fChristian Maeder addSentences $ catMaybes $ map comakeInjective
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reilly $ filter ( \ (_, _, ces) -> not $ null ces)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder addSentences $ makeDisjSubsorts s sbs
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder addSentences $ catMaybes $ concatMap
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder ( \ c -> map (comakeDisjToSort c) sbs)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder addSentences $ comakeDisjoint comps
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder let ttrips' = [(a,vs,t,ses) | (Just(a,t),vs,ses) <- ttrips]
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder addSentences $ catMaybes $ concatMap
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder map (makeUndefForm ses) ttrips') sels
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder _ -> return ()
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedergetCoConsType :: SORT -> COALTERNATIVE -> (Maybe Id, OpType, [COCOMPONENTS])
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedergetCoConsType s c =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder let (part, i, il) = case c of
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder CoSubsorts _ _ -> error "getCoConsType"
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Co_construct k a l _ -> (k, a, l)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder in (i, OpType part (concatMap
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (map (opRes . snd) . getCoCompType s) il) s, il)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedergetCoCompType :: SORT -> COCOMPONENTS -> [(Id, OpType)]
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillygetCoCompType s (CoSelect l (Op_type k args res _) _) =
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder map (\ i -> (i, OpType k (args++[s]) res)) l
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian MaedercoselForms :: (Maybe Id, OpType, [COCOMPONENTS]) -> [Named (FORMULA f)]
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian MaedercoselForms x =
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder case coselForms1 "X" x of
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder (Just (i,f),vs,cs) -> makeSelForms 1 (i,vs,f,cs)
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian MaedercoselForms1 :: String -> (Maybe Id, OpType, [COCOMPONENTS])
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder -> (Maybe (Id, TERM f), [VAR_DECL], [(Maybe Id, OpType)])
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian MaedercoselForms1 str (i, ty, il) =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder let cs = concatMap (getCoCompType $ opRes ty) il
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder vs = genSelVars str 1 $ map snd cs
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder it = case i of
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Nothing -> Nothing
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Just i' -> Just (i',Application (Qual_op_name i'
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (toOP_TYPE ty) nullRange)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (map toQualVar vs) nullRange)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly in (it, vs, map ( \ (j, typ) -> (Just j, typ)) cs)
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycomakeDisjToSort :: (Maybe Id, OpType, [COCOMPONENTS]) -> SORT
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -> Maybe (Named (FORMULA f))
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian MaedercomakeDisjToSort a s = do
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder let (i, v, _) = coselForms1 "X" a
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder p = posOfId s
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder return $ makeNamed ("ga_disjoint_" ++ showId c "_sort_" ++ showId s "")
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly $ mkForall v (Negation (Membership t s p) p) p
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian MaedercomakeInjective :: (Maybe Id, OpType, [COCOMPONENTS])
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder -> Maybe (Named (FORMULA f))
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian MaedercomakeInjective a = do
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder let (i1, v1, _) = coselForms1 "X" a
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder (i2, v2, _) = coselForms1 "Y" a
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder let p = posOfId c
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder return $ makeNamed ("ga_injective_" ++ showId c "") $
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder mkForall (v1 ++ v2)
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder (Equivalence (Strong_equation t1 t2 p)
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder (let ces = zipWith ( \ w1 w2 -> Strong_equation
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder (toQualVar w1) (toQualVar w2) p) v1 v2
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder in if isSingle ces then head ces else Conjunction ces p)
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian MaedercomakeDisjoint :: [(Maybe Id, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)]
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian MaedercomakeDisjoint [] = []
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian MaedercomakeDisjoint (a:as) = catMaybes (map (comakeDisj a) as) ++ comakeDisjoint as
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian MaedercomakeDisj :: (Maybe Id, OpType, [COCOMPONENTS])
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder -> (Maybe Id, OpType, [COCOMPONENTS])
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder -> Maybe (Named (FORMULA f))
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycomakeDisj a1 a2 = do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let (i1, v1, _) = coselForms1 "X" a1
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (i2, v2, _) = coselForms1 "Y" a2
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (c1,t1) <- i1
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder (c2,t2) <- i2
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder let p = posOfId c1 `appRange` posOfId c2
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly return $ makeNamed ("ga_disjoint_" ++ showId c1 "_" ++ showId c2 "")
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly $ mkForall (v1 ++ v2) (Negation (Strong_equation t1 t2 p) p) p
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | return the constructor and the set of total selectors
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maederana_COALTERNATIVE :: SORT -> Annoted COALTERNATIVE
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -> State CSign (Maybe (Component, Set.Set Component))
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederana_COALTERNATIVE s c =
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder case item c of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly CoSubsorts ss _ -> do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly mapM_ (addSubsort s) ss
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly return Nothing
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let cons@(i, ty, il) = getCoConsType s ci
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ul <- mapM (ana_COCOMPONENTS s) il
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let ts = concatMap fst ul
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly addDiags $ checkUniqueness (ts ++ concatMap snd ul)
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder addSentences $ coselForms cons
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder Nothing -> return Nothing
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Just i' -> do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly addOp c ty i'
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ Just (Component i' ty, Set.fromList ts)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | return total and partial selectors
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyana_COCOMPONENTS :: SORT -> COCOMPONENTS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -> State CSign ([Component], [Component])
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyana_COCOMPONENTS s c = do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let cs = getCoCompType s c
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sels <- mapM ( \ (i, ty) ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly do addOp (emptyAnno ()) ty i
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly return $ Just $ Component i ty) cs
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly return $ partition ((==Total) . opKind . compType) $ catMaybes sels
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyana_C_BASIC_ITEM
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly :: Ana C_BASIC_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyana_C_BASIC_ITEM mix bi = do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly CoFree_datatype al ps ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly do mapM_ (\ i -> case item i of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly CoDatatype_decl s _ _ -> addSort i s) al
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly mapAnM (ana_CODATATYPE_DECL Free) al
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly toCoSortGenAx ps True $ getCoDataGenSig al
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly closeSubsortRel
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly CoSort_gen al ps ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly do (gs,ul) <- ana_CoGenerated ana_C_SIG_ITEM mix ([], al)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly toCoSortGenAx ps False $ unionGenAx gs
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly return $ CoSort_gen ul ps
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillytoCoSortGenAx :: Range -> Bool -> GenAx -> State CSign ()
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillytoCoSortGenAx ps isFree (sorts, rel, ops) = do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let sortList = Set.toList sorts
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly opSyms = map ( \ c -> let ide = compId c in Qual_op_name ide
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (toOP_TYPE $ compType c) $ posOfId ide) $ Set.toList ops
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly injSyms = map ( \ (s, t) -> let p = posOfId s in
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Qual_op_name injName
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder (Op_type Total [s] t p) p) $ Rel.toList rel
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly if null sortList then
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly addDiags[Diag Error "missing cogenerated sort" ps]
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly else return ()
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly addSentences [makeNamed ("ga_cogenerated_" ++ showSepList (showString "_")
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly showId sortList "")
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly $ ExtFORMULA $ CoSort_gen_ax sortList
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (opSyms ++ injSyms) isFree]
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyana_CoGenerated :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -> Ana ([GenAx], [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)])
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyana_CoGenerated anaf mix (_, al) = do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ul <- mapAnM (ana_SIG_ITEMS minExpForm anaf mix Generated) al
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly return (map (getCoGenSig . item) ul, ul)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygetCoGenSig :: SIG_ITEMS C_SIG_ITEM C_FORMULA -> GenAx
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillygetCoGenSig si = case si of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Sort_items al _ -> unionGenAx $ map (getGenSorts . item) al
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.unions (map (getOps . item) al))
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Datatype_items dl _ -> getDataGenSig dl
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Ext_SIG_ITEMS (CoDatatype_items dl _) -> getCoDataGenSig dl
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly _ -> emptyGenAx
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillygetCoDataGenSig :: [Annoted CODATATYPE_DECL] -> GenAx
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillygetCoDataGenSig dl =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let get_sel (s, a) = case a of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly CoSubsorts _ _ -> []
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Co_construct _ _ l _ -> concatMap (getCoCompType s) l
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly alts = concatMap (( \ (CoDatatype_decl s al _) ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly map ( \ a -> (s, item a)) al) . item) dl
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sorts = map fst alts
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (realAlts, subs) = partition (isCoConsAlt . snd) alts
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder sels = map ( \ (i, ot) -> Component i ot) $ concatMap get_sel realAlts
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly rel = foldr ( \ (t, a) r ->
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder foldr ( \ s ->
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder r $ getCoSubsorts a)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder in (Set.fromList sorts, rel, Set.fromList sels)