StatAna.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsModule : $Header$
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsDescription : static analysis for CoCASL
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsCopyright : (c) Till Mossakowski, Uni Bremen 2004-2005
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsLicense : GPLv2 or higher
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsMaintainer : hausmann@informatik.uni-bremen.de
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsStability : provisional
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsPortability : portable
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsstatic analysis for CoCASL
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsimport qualified Data.Set as Set
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsimport qualified Common.Lib.Rel as Rel
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsimport Data.List (partition)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewstype CSign = Sign C_FORMULA CoCASLSign
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsinstance FreeVars C_FORMULA where
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews freeVarsOfExt sign cf = case cf of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews BoxOrDiamond _ _ f _ -> freeVars sign f
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsbasicCoCASLAnalysis
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews :: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Sign C_FORMULA CoCASLSign, GlobalAnnos)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews -> Result (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews ExtSign (Sign C_FORMULA CoCASLSign) Symbol,
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews [Named (FORMULA C_FORMULA)])
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsbasicCoCASLAnalysis =
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews basicAnalysis minExpForm ana_C_BASIC_ITEM ana_C_SIG_ITEM ana_CMix
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_CMix :: Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_CMix = emptyMix
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews { getBaseIds = ids_C_BASIC_ITEM
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , getSigIds = ids_C_SIG_ITEM
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , getExtIds = \ e -> let c = constructors e in
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews mkIdSets (opMapConsts c) (nonConsts c) Set.empty
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , putParen = mapC_FORMULA
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , mixResolve = resolveC_FORMULA
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsids_C_BASIC_ITEM :: C_BASIC_ITEM -> IdSets
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsids_C_BASIC_ITEM ci = case ci of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoFree_datatype al _ ->
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (unite2 $ map (ids_CODATATYPE_DECL . item) al, Set.empty)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoSort_gen al _ -> unite $ map (ids_SIG_ITEMS ids_C_SIG_ITEM . item) al
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsids_C_SIG_ITEM :: C_SIG_ITEM -> IdSets
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsids_C_SIG_ITEM (CoDatatype_items al _) =
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (unite2 $ map (ids_CODATATYPE_DECL . item) al, Set.empty)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsids_CODATATYPE_DECL :: CODATATYPE_DECL -> (Set.Set Id, Set.Set Id)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsids_CODATATYPE_DECL (CoDatatype_decl _ al _) =
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews unite2 $ map (ids_COALTERNATIVE . item) al
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsids_COALTERNATIVE :: COALTERNATIVE -> (Set.Set Id, Set.Set Id)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsids_COALTERNATIVE a = let e = Set.empty in case a of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Co_construct _ mi cs _ -> let s = maybe Set.empty Set.singleton mi in
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews if null cs then (s, e) else
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (e, Set.unions $ s : map ids_COCOMPONENTS cs)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoSubsorts _ _ -> (e, e)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsids_COCOMPONENTS :: COCOMPONENTS -> Set.Set Id
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsids_COCOMPONENTS (CoSelect l _ _) = Set.unions $ map Set.singleton l
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsdata CoRecord a b c d = CoRecord
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews { foldBoxOrDiamond :: C_FORMULA -> Bool -> d -> a -> Range -> c
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , foldCoSort_gen_ax :: C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> c
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , foldTerm_mod :: MODALITY -> b -> d
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , foldSimple_mod :: MODALITY -> SIMPLE_ID -> d
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsfoldC_Formula :: Record C_FORMULA a b -> CoRecord a b c d -> C_FORMULA -> c
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsfoldC_Formula r cr c = case c of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews BoxOrDiamond b m f ps ->
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews foldBoxOrDiamond cr c b (foldModality r cr m) (foldFormula r f) ps
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoSort_gen_ax s o b -> foldCoSort_gen_ax cr c s o b
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsfoldModality :: Record C_FORMULA a b -> CoRecord a b c d -> MODALITY -> d
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsfoldModality r cr m = case m of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Term_mod t -> foldTerm_mod cr m $ foldTerm r t
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Simple_mod i -> foldSimple_mod cr m i
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsmapCoRecord :: CoRecord (FORMULA C_FORMULA) (TERM C_FORMULA) C_FORMULA MODALITY
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsmapCoRecord = CoRecord
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews { foldBoxOrDiamond = const BoxOrDiamond
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , foldCoSort_gen_ax = const CoSort_gen_ax
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , foldTerm_mod = const Term_mod
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , foldSimple_mod = const Simple_mod
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsconstCoRecord :: ([a] -> a) -> a -> CoRecord a a a a
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsconstCoRecord jn c = CoRecord
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews { foldBoxOrDiamond = \ _ _ m f _ -> jn [m, f]
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , foldCoSort_gen_ax = \ _ _ _ _ -> c
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , foldTerm_mod = \ _ t -> t
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews , foldSimple_mod = \ _ _ -> c
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsmapC_FORMULA :: C_FORMULA -> C_FORMULA
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsmapC_FORMULA = foldC_Formula (mkMixfixRecord mapC_FORMULA) mapCoRecord
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsresolveMODALITY :: MixResolve MODALITY
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsresolveMODALITY ga ids m = case m of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Term_mod t ->
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews fmap Term_mod $ resolveMixTrm mapC_FORMULA resolveC_FORMULA ga ids t
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews _ -> return m
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsresolveC_FORMULA :: MixResolve C_FORMULA
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsresolveC_FORMULA ga ids cf = case cf of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews BoxOrDiamond b m f ps -> do
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews nm <- resolveMODALITY ga ids m
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews nf <- resolveMixFrm mapC_FORMULA resolveC_FORMULA ga ids f
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews return $ BoxOrDiamond b nm nf ps
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews _ -> error "resolveC_FORMULA"
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsminExpForm :: Min C_FORMULA CoCASLSign
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsminExpForm s form =
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let ops = formulaIds s
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews minMod md ps = case md of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Term_mod t -> let
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews t2 <- oneExpTerm minExpForm s t
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let srt = sortOfTerm t2
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews trm = Term_mod t2
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews then return trm
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews else Result [mkDiag Error
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews ("unknown modality '"
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews ++ showId srt "' for term") t ]
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews in case t of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Mixfix_token tm ->
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews if Set.member (simpleIdToId tm) ops
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews then return $ Simple_mod tm
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews else case maybeResult r of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Nothing -> Result
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews [mkDiag Error "unknown modality" tm]
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews $ Just $ Simple_mod tm
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews in case form of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews BoxOrDiamond b m f ps ->
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews do nm <- minMod m ps
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews f2 <- minExpFORMULA minExpForm s f
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews return $ BoxOrDiamond b nm f2 ps
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews phi -> return phi
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_C_SIG_ITEM :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_C_SIG_ITEM _ mi = case mi of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoDatatype_items al _ ->
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews do mapM_ (\ i -> case item i of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoDatatype_decl s _ _ -> addSort NonEmptySorts i s) al
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews mapAnM (ana_CODATATYPE_DECL Loose) al
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews closeSubsortRel
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsisCoConsAlt :: COALTERNATIVE -> Bool
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsisCoConsAlt a = case a of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoSubsorts _ _ -> False
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsgetCoSubsorts :: COALTERNATIVE -> [SORT]
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsgetCoSubsorts c = case c of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoSubsorts cs _ -> cs
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews-- | return list of constructors
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_CODATATYPE_DECL :: GenKind -> CODATATYPE_DECL -> State CSign [Component]
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_CODATATYPE_DECL gk (CoDatatype_decl s al _) = do
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews ul <- mapM (ana_COALTERNATIVE s) al
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let constr = catMaybes ul
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews cs = map fst constr
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews unless (null constr) $ do
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews addDiags $ checkUniqueness cs
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let totalSels = Set.unions $ map snd constr
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews wrongConstr = filter ((totalSels /=) . snd) constr
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews addDiags $ map (\ (c, _) -> mkDiag Error
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews ("total selectors '" ++ showSepList (showString ",")
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews showDoc (Set.toList totalSels)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews "'\n must appear in alternative") c) wrongConstr
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let (alts, subs) = partition isCoConsAlt $ map item al
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews sbs = concatMap getCoSubsorts subs
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews comps = map (getCoConsType s) alts
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews ttrips = map ((\ (a, vs, ses) -> (a, vs, catSels ses))
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews . coselForms1 "X") comps
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews sels = concatMap (\ (_, _, ses) -> ses) ttrips
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews addSentences $ mapMaybe comakeInjective
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews $ filter (\ (_, _, ces) -> not $ null ces)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews addSentences $ makeDisjSubsorts s sbs
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews addSentences $ catMaybes $ concatMap
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (\ c -> map (comakeDisjToSort c) sbs)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews addSentences $ comakeDisjoint comps
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let ttrips' = [(a, vs, t, ses) | (Just (a, t), vs, ses) <- ttrips]
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews addSentences $ catMaybes $ concatMap
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews map (makeUndefForm ses) ttrips') sels
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews _ -> return ()
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsgetCoConsType :: SORT -> COALTERNATIVE -> (Maybe Id, OpType, [COCOMPONENTS])
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsgetCoConsType s c =
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let (part, i, il) = case c of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoSubsorts _ _ -> error "getCoConsType"
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Co_construct k a l _ -> (k, a, l)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews in (i, OpType part (concatMap
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (map (opRes . snd) . getCoCompType s) il) s, il)
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsgetCoCompType :: SORT -> COCOMPONENTS -> [(Id, OpType)]
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsgetCoCompType s (CoSelect l (Op_type k args res _) _) =
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews map (\ i -> (i, OpType k (args ++ [s]) res)) l
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscoselForms :: (Maybe Id, OpType, [COCOMPONENTS]) -> [Named (FORMULA f)]
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscoselForms x = case coselForms1 "X" x of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (Just (i, f), vs, cs) -> makeSelForms 1 (i, vs, f, cs)
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscoselForms1 :: String -> (Maybe Id, OpType, [COCOMPONENTS])
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews -> (Maybe (Id, TERM f), [VAR_DECL], [(Maybe Id, OpType)])
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscoselForms1 str (i, ty, il) =
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let cs = concatMap (getCoCompType $ opRes ty) il
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews vs = genSelVars str 1 $ map snd cs
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews it = case i of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Nothing -> Nothing
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Just i' -> Just (i', Application (Qual_op_name i'
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (toOP_TYPE ty) nullRange)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (map toQualVar vs) nullRange)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews in (it, vs, map (\ (j, typ) -> (Just j, typ)) cs)
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscomakeDisjToSort :: (Maybe Id, OpType, [COCOMPONENTS]) -> SORT
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews -> Maybe (Named (FORMULA f))
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscomakeDisjToSort a s = do
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let (i, v, _) = coselForms1 "X" a
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews p = posOfId s
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews return $ makeNamed ("ga_disjoint_" ++ showId c "_sort_" ++ showId s "")
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews $ mkForall v (Negation (Membership t s p) p) p
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscomakeInjective :: (Maybe Id, OpType, [COCOMPONENTS])
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews -> Maybe (Named (FORMULA f))
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscomakeInjective a = do
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let (i1, v1, _) = coselForms1 "X" a
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (i2, v2, _) = coselForms1 "Y" a
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (c, t1) <- i1
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (_, t2) <- i2
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let p = posOfId c
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews return $ makeNamed ("ga_injective_" ++ showId c "") $
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews mkForall (v1 ++ v2)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (Equivalence (Strong_equation t1 t2 p)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (let ces = zipWith (\ w1 w2 -> Strong_equation
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (toQualVar w1) (toQualVar w2) p) v1 v2
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews in if isSingle ces then head ces else Conjunction ces p)
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscomakeDisjoint :: [(Maybe Id, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)]
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscomakeDisjoint l = case l of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews a : as -> mapMaybe (comakeDisj a) as ++ comakeDisjoint as
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscomakeDisj :: (Maybe Id, OpType, [COCOMPONENTS])
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews -> (Maybe Id, OpType, [COCOMPONENTS])
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews -> Maybe (Named (FORMULA f))
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewscomakeDisj a1 a2 = do
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let (i1, v1, _) = coselForms1 "X" a1
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (i2, v2, _) = coselForms1 "Y" a2
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (c1, t1) <- i1
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (c2, t2) <- i2
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let p = posOfId c1 `appRange` posOfId c2
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews return $ makeNamed ("ga_disjoint_" ++ showId c1 "_" ++ showId c2 "")
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews $ mkForall (v1 ++ v2) (Negation (Strong_equation t1 t2 p) p) p
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews-- | return the constructor and the set of total selectors
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_COALTERNATIVE :: SORT -> Annoted COALTERNATIVE
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews -> State CSign (Maybe (Component, Set.Set Component))
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_COALTERNATIVE s c = case item c of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoSubsorts ss _ -> do
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews mapM_ (addSubsort s) ss
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews return Nothing
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let cons@(i, ty, il) = getCoConsType s ci
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews ul <- mapM (ana_COCOMPONENTS s) il
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let ts = concatMap fst ul
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews addDiags $ checkUniqueness (ts ++ concatMap snd ul)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews addSentences $ coselForms cons
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Nothing -> return Nothing
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Just i' -> do
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews addOp c ty i'
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews return $ Just (Component i' ty, Set.fromList ts)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews-- | return total and partial selectors
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_COCOMPONENTS :: SORT -> COCOMPONENTS
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews -> State CSign ([Component], [Component])
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_COCOMPONENTS s c = do
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let cs = getCoCompType s c
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews sels <- mapM (\ (i, ty) ->
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews do addOp (emptyAnno ()) ty i
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews return $ Just $ Component i ty) cs
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews return $ partition ((== Total) . opKind . compType) $ catMaybes sels
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_C_BASIC_ITEM
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews :: Ana C_BASIC_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_C_BASIC_ITEM mix bi = case bi of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoFree_datatype al ps ->
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews do mapM_ (\ i -> case item i of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoDatatype_decl s _ _ -> addSort NonEmptySorts i s) al
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews mapAnM (ana_CODATATYPE_DECL Free) al
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews toCoSortGenAx ps True $ getCoDataGenSig al
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews closeSubsortRel
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoSort_gen al ps ->
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews do (gs, ul) <- ana_CoGenerated ana_C_SIG_ITEM mix ([], al)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews toCoSortGenAx ps False $ unionGenAx gs
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews return $ CoSort_gen ul ps
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewstoCoSortGenAx :: Range -> Bool -> GenAx -> State CSign ()
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewstoCoSortGenAx ps isFree (sorts, rel, ops) = do
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let sortList = Set.toList sorts
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews opSyms = map (\ c -> let ide = compId c in Qual_op_name ide
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (toOP_TYPE $ compType c) $ posOfId ide) $ Set.toList ops
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews injSyms = map (\ (s, t) -> let p = posOfId s in
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Qual_op_name (mkUniqueInjName s t)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (Op_type Total [s] t p) p) $ Rel.toList rel
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews when (null sortList)
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews $ addDiags [Diag Error "missing cogenerated sort" ps]
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews addSentences [makeNamed ("ga_cogenerated_" ++ showSepList (showString "_")
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews showId sortList "")
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews $ ExtFORMULA $ CoSort_gen_ax sortList
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews (opSyms ++ injSyms) isFree]
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_CoGenerated :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews -> Ana ([GenAx], [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)])
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrewsana_CoGenerated anaf mix (_, al) = do
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews ul <- mapAnM (ana_SIG_ITEMS minExpForm anaf mix Generated) al
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews return (map (getCoGenSig . item) ul, ul)
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsgetCoGenSig :: SIG_ITEMS C_SIG_ITEM C_FORMULA -> GenAx
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsgetCoGenSig si = case si of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Sort_items _ al _ -> unionGenAx $ map (getGenSorts . item) al
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Set.unions (map (getOps . item) al))
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Datatype_items _ dl _ -> getDataGenSig dl
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Ext_SIG_ITEMS (CoDatatype_items dl _) -> getCoDataGenSig dl
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews _ -> emptyGenAx
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsgetCoDataGenSig :: [Annoted CODATATYPE_DECL] -> GenAx
63dd46733010bb9622810faa17d88c3e3c28b730Mark AndrewsgetCoDataGenSig dl =
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews let get_sel (s, a) = case a of
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews CoSubsorts _ _ -> []
63dd46733010bb9622810faa17d88c3e3c28b730Mark Andrews Co_construct _ _ l _ -> concatMap (getCoCompType s) l
rel = foldr (\ (t, a) r -> foldr (`Rel.insert` t) r $ getCoSubsorts a)
Rel.empty subs