StatAna.hs revision bec7e681b0ba4d085638ec7af0cf7ae5068840ca
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorriniModule : $Header$
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorriniCopyright : (c) Till Mossakowski, Uni Bremen 2004
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorriniLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorriniMaintainer : till@tzi.de
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorriniStability : provisional
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederPortability : portable
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder static analysis for CoCASL
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder correct map_C_FORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder translation of cogen ax
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder analysis of modal formulas
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Add cofree axioms
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder remove disjointness axioms
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder leave out sorts/profiles for pretty printing
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport qualified Common.Lib.Set as Set
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype CSign = Sign C_FORMULA CoCASLSign
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederbasicCoCASLAnalysis :: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini Sign C_FORMULA CoCASLSign, GlobalAnnos)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> Result (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Sign C_FORMULA CoCASLSign,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Sign C_FORMULA CoCASLSign,
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini [Named (FORMULA C_FORMULA)])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederbasicCoCASLAnalysis =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder basicAnalysis minExpForm ana_C_BASIC_ITEM ana_C_SIG_ITEM diffCoCASLSign
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torriniinstance Resolver C_FORMULA where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder putParen = mapC_FORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mixResolve = resolveC_FORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder checkMix = noExtMixfixCo
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder putInj = injC_FORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapMODALITY :: MODALITY -> MODALITY
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapMODALITY m = case m of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Term_mod t -> Term_mod $ mapTerm mapC_FORMULA t
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrinimapC_FORMULA :: C_FORMULA -> C_FORMULA
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrinimapC_FORMULA cf = case cf of
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini BoxOrDiamond b m f ps -> let
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nm = mapMODALITY m
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nf = mapFormula mapC_FORMULA f
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in BoxOrDiamond b nm nf ps
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinjMODALITY :: MODALITY -> MODALITY
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinjMODALITY m = case m of
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini Term_mod t -> Term_mod $ injTerm injC_FORMULA t
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorriniinjC_FORMULA :: C_FORMULA -> C_FORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinjC_FORMULA cf = case cf of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder BoxOrDiamond b m f ps -> let
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini nm = injMODALITY m
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini nf = injFormula injC_FORMULA f
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini in BoxOrDiamond b nm nf ps
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorriniresolveMODALITY :: MixResolve MODALITY
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorriniresolveMODALITY ga ids m = case m of
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini Term_mod t ->
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini fmap Term_mod $ resolveMixTrm mapC_FORMULA resolveC_FORMULA ga ids t
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini _ -> return m
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederresolveC_FORMULA :: MixResolve C_FORMULA
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorriniresolveC_FORMULA ga ids cf = case cf of
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini BoxOrDiamond b m f ps -> do
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini nm <- resolveMODALITY ga ids m
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nf <- resolveMixFrm mapC_FORMULA resolveC_FORMULA ga ids f
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return $ BoxOrDiamond b nm nf ps
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini _ -> error "resolveC_FORMULA"
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrininoExtMixfixCo :: C_FORMULA -> Bool
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedernoExtMixfixCo cf =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let noInner = noMixfixF noExtMixfixCo in
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini BoxOrDiamond _ _ f _ -> noInner f
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederminExpForm :: Min C_FORMULA CoCASLSign
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorriniminExpForm ga s form =
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini let ops = formulaIds s
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini minMod md ps = case md of
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini Term_mod t -> let
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ts <- minExpTerm minExpForm ga s t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder t2 <- is_unambiguous t ts ps
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini let srt = term_sort t2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder trm = Term_mod t2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then return trm
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini else Result [mkDiag Error
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini ("unknown modality '"
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini ++ showId srt "' for term") t ]
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini Mixfix_token tm ->
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini if Set.member (simpleIdToId tm) ops
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then return $ Simple_mod tm
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else case maybeResult r of
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini Nothing -> Result
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [mkDiag Error "unknown modality" tm]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $ Just $ Simple_mod tm
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in case form of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder BoxOrDiamond b m f ps ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do nm <- minMod m ps
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini f2 <- minExpFORMULA minExpForm ga s f
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return $ BoxOrDiamond b nm f2 ps
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder phi -> return phi
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torriniana_C_SIG_ITEM :: Ana C_SIG_ITEM C_FORMULA CoCASLSign
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederana_C_SIG_ITEM _ mi =
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini CoDatatype_items al _ ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do let sorts = map (( \ (CoDatatype_decl s _ _) -> s) . item) al
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapM_ addSort sorts
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini mapAnM (ana_CODATATYPE_DECL Loose) al
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder closeSubsortRel
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini-- | return list of constructors
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torriniana_CODATATYPE_DECL :: GenKind -> CODATATYPE_DECL -> State CSign [Component]
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torriniana_CODATATYPE_DECL gk (CoDatatype_decl s al _) =
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini do ul <- mapM (ana_COALTERNATIVE s . item) al
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let constr = catMaybes ul
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder cs = map fst constr
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if null constr then return ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else do addDiags $ checkUniqueness cs
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini let totalSels = Set.unions $ map snd constr
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder wrongConstr = filter ((totalSels /=) . snd) constr
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder addDiags $ map ( \ (c, _) -> mkDiag Error
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ("total selectors '" ++ showSepList (showString ",")
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini showPretty (Set.toList totalSels)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "'\n must appear in alternative") c) wrongConstr
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini let allts = map item al
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini (alts, subs) = partition ( \ a -> case a of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder CoSubsorts _ _ -> False
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> True) allts
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini sbs = concatMap ( \ (CoSubsorts ss _) -> ss) subs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder comps = map (getCoConsType s) alts
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ttrips = map ( \ (a, vs, ses) -> (a, vs, catSels ses))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $ map (coselForms1 "X") $ comps
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini sels = concatMap ( \ (_, _, ses) -> ses) ttrips
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder addSentences $ catMaybes $ map comakeInjective
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $ filter ( \ (_, _, ces) -> not $ null ces)
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini addSentences $ catMaybes $ concatMap ( \ as -> map (comakeDisjToSort as) sbs)
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini addSentences $ comakeDisjoint comps
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini let ttrips' = [(a,vs,t,ses) | (Just(a,t),vs,ses) <- ttrips]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder addSentences $ catMaybes $ concatMap
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder map (makeUndefForm ses) ttrips') sels
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini _ -> return ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetCoConsType :: SORT -> COALTERNATIVE -> (Maybe Id, OpType, [COCOMPONENTS])
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrinigetCoConsType s c =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let (part, i, il) = case c of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder CoSubsorts _ _ -> error "getConsType"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Co_construct k a l _ -> (k, a, l)
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini in (i, OpType part (concatMap
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini (map (opRes . snd) . getCoCompType s) il) s, il)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetCoCompType :: SORT -> COCOMPONENTS -> [(Maybe Id, OpType)]
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrinigetCoCompType s (CoSelect l (Op_type k args res _) _) =
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini map (\ i -> (Just i, OpType k (args++[s]) res)) l
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercoselForms :: (Maybe Id, OpType, [COCOMPONENTS]) -> [Named (FORMULA f)]
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrinicoselForms x =
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini case coselForms1 "X" x of
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini (Just (i,f),vs,cs) -> makeSelForms 1 (i,vs,f,cs)
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrinicoselForms1 :: String -> (Maybe Id, OpType, [COCOMPONENTS])
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini -> (Maybe (Id, TERM f), [VAR_DECL], [(Maybe Id, OpType)])
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrinicoselForms1 str (i, ty, il) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let cs = concatMap (getCoCompType $ opRes ty) il
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder vs = genSelVars str 1 cs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> Nothing
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini Just i' -> Just (i',Application (Qual_op_name i'
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (toOP_TYPE ty) [])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (map toQualVar vs) [])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in (it, vs, cs)
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrinicomakeDisjToSort :: (Maybe Id, OpType, [COCOMPONENTS]) -> SORT
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> Maybe (Named (FORMULA f))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercomakeDisjToSort a s = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let (i, v, _) = coselForms1 "X" a
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder p = [posOfId s]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return $ NamedSen ("ga_disjoint_" ++ showId c "_sort_" ++ showId s "") $
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mkForall v (Negation (Membership t s p) p) p
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrinicomakeInjective :: (Maybe Id, OpType, [COCOMPONENTS])
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini -> Maybe (Named (FORMULA f))
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrinicomakeInjective a = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let (i1, v1, _) = coselForms1 "X" a
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (i2, v2, _) = coselForms1 "Y" a
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini let p = [posOfId c]
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini return $ NamedSen ("ga_injective_" ++ showId c "") $
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mkForall (v1 ++ v2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Equivalence (Strong_equation t1 t2 p)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (let ces = zipWith ( \ w1 w2 -> Strong_equation
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (toQualVar w1) (toQualVar w2) p) v1 v2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if isSingle ces then head ces else Conjunction ces p)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercomakeDisjoint :: [(Maybe Id, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercomakeDisjoint [] = []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercomakeDisjoint (a:as) = catMaybes (map (comakeDisj a) as) ++ comakeDisjoint as
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercomakeDisj :: (Maybe Id, OpType, [COCOMPONENTS])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> (Maybe Id, OpType, [COCOMPONENTS])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> Maybe (Named (FORMULA f))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercomakeDisj a1 a2 = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let (i1, v1, _) = coselForms1 "X" a1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (i2, v2, _) = coselForms1 "Y" a2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let p = [posOfId c1, posOfId c2]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return $ NamedSen ("ga_disjoint_" ++ showId c1 "_" ++ showId c2 "") $
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mkForall (v1 ++ v2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Negation (Strong_equation t1 t2 p) p) p
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | return the constructor and the set of total selectors
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederana_COALTERNATIVE :: SORT -> COALTERNATIVE
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> State CSign (Maybe (Component, Set.Set Component))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederana_COALTERNATIVE s c =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder CoSubsorts ss _ ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do mapM_ (addSubsort s) ss
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> do let cons@(i, ty, il) = getCoConsType s c
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ul <- mapM (ana_COCOMPONENTS s) il
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let ts = concatMap fst ul
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder addDiags $ checkUniqueness (ts ++ concatMap snd ul)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder addSentences $ coselForms cons
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> return Nothing
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return $ Just (Component i' ty, Set.fromList ts)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | return total and partial selectors
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederana_COCOMPONENTS :: SORT -> COCOMPONENTS
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> State CSign ([Component], [Component])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederana_COCOMPONENTS s c = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let cs = getCoCompType s c
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sels <- mapM ( \ (mi, ty) ->
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini Nothing -> return Nothing
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just i -> do addOp ty i
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini return $ Just $ Component i ty) cs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return $ partition ((==Total) . opKind . compType) $ catMaybes sels
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederana_C_BASIC_ITEM :: Ana C_BASIC_ITEM C_FORMULA CoCASLSign
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederana_C_BASIC_ITEM ga bi = do
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini CoFree_datatype al ps ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do let sorts = map (( \ (CoDatatype_decl s _ _) -> s) . item) al
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapM_ addSort sorts
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini mapAnM (ana_CODATATYPE_DECL Free) al
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder toCoSortGenAx ps True $ getCoDataGenSig al
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder closeSubsortRel
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini CoSort_gen al ps ->
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini do (gs,ul) <- ana_CoGenerated ana_C_SIG_ITEM ga ([], al)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder toCoSortGenAx ps False
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Set.unions $ map fst gs, Set.unions $ map snd gs)
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini return $ CoSort_gen ul ps
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo TorrinitoCoSortGenAx :: [Pos] -> Bool ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Set.Set Id, Set.Set Component) -> State CSign ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertoCoSortGenAx ps isFree (sorts, ops) = do
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini let sortList = Set.toList sorts
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder opSyms = map ( \ c -> Qual_op_name (compId c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (toOP_TYPE $ compType c) []) $ Set.toList ops
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder f = ExtFORMULA $ CoSort_gen_ax sortList opSyms isFree
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini if null sortList then
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder addDiags[Diag Error "missing cogenerated sort" (headPos ps)]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder addSentences [NamedSen ("ga_cogenerated_" ++
28ff4d4c01dc43440f7e6fde73ab783e7e0999d6Paolo Torrini showSepList (showString "_") showId sortList "") f]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederana_CoGenerated :: Ana C_SIG_ITEM C_FORMULA e
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> Ana ([(Set.Set Id, Set.Set Component)],
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]) C_FORMULA e
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederana_CoGenerated anaf ga (_, al) = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ul <- mapAnM (ana_SIG_ITEMS mapC_FORMULA resolveC_FORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder noExtMixfixCo anaf ga Generated) al
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (map (getCoGenSig . item) ul,ul)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetCoGenSig :: SIG_ITEMS C_SIG_ITEM C_FORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetCoGenSig si = case si of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Sort_items al _ -> (Set.unions (map (getSorts . item) al), Set.empty)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Op_items al _ -> (Set.empty, Set.unions (map (getOps . item) al))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Datatype_items dl _ -> getDataGenSig dl
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Ext_SIG_ITEMS (CoDatatype_items dl _) -> getCoDataGenSig dl
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetCoDataGenSig :: [Annoted CODATATYPE_DECL] -> (Set.Set Id, Set.Set Component)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetCoDataGenSig dl =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let get_sel1 s al = case al of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder CoSubsorts _ _ -> []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Co_construct _ _ l _ -> concatMap (getCoCompType s) l
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder get_sel (s,als) = concatMap (get_sel1 s . item) als
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder alts = map (( \ (CoDatatype_decl s al _) -> (s, al)) . item) dl
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sorts = map fst alts
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sels = concatMap computeComp $ concatMap get_sel alts
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder computeComp (Just i,ot) = [Component i ot]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder computeComp _ = []