d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- |

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederModule : $Header$

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederDescription : static analysis for CoCASL

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2004-2005

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : hausmann@informatik.uni-bremen.de

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederstatic analysis for CoCASL

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedermodule CoCASL.StatAna where

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CoCASL.AS_CoCASL

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CoCASL.Print_AS ()

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CoCASL.CoCASLSign

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.Sign

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.MixfixParser

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maederimport CASL.ShowMixfix

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maederimport CASL.StaticAna

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maederimport CASL.AS_Basic_CASL

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.Overload

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maederimport CASL.Quantification

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maederimport CASL.Fold

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Common.AS_Annotation

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maederimport Common.GlobalAnnotations

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport qualified Data.Set as Set

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport qualified Common.Lib.Rel as Rel

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maederimport Common.Lib.State

ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torriniimport Common.Id

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Common.Result

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Common.DocUtils

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maederimport Common.ExtSign

ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrini

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Control.Monad

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maederimport Data.Maybe

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maederimport Data.List (partition)

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maedertype CSign = Sign C_FORMULA CoCASLSign

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederinstance FreeVars C_FORMULA where

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder freeVarsOfExt sign cf = case cf of

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder BoxOrDiamond _ _ f _ -> freeVars sign f

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder _ -> Set.empty

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbasicCoCASLAnalysis

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder :: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Sign C_FORMULA CoCASLSign, GlobalAnnos)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -> Result (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder ExtSign (Sign C_FORMULA CoCASLSign) Symbol,

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder [Named (FORMULA C_FORMULA)])

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbasicCoCASLAnalysis =

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder basicAnalysis minExpForm ana_C_BASIC_ITEM ana_C_SIG_ITEM ana_CMix

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maederana_CMix :: Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederana_CMix = emptyMix

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder { getBaseIds = ids_C_BASIC_ITEM

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , getSigIds = ids_C_SIG_ITEM

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder , getExtIds = \ e -> let c = constructors e in

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder mkIdSets (opMapConsts c) (nonConsts c) Set.empty

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , putParen = mapC_FORMULA

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , mixResolve = resolveC_FORMULA

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder }

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederids_C_BASIC_ITEM :: C_BASIC_ITEM -> IdSets

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederids_C_BASIC_ITEM ci = case ci of

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CoFree_datatype al _ ->

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (unite2 $ map (ids_CODATATYPE_DECL . item) al, Set.empty)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CoSort_gen al _ -> unite $ map (ids_SIG_ITEMS ids_C_SIG_ITEM . item) al

10a92a06296c3c8d522543de7e3a4534bf528505Paolo Torrini

10a92a06296c3c8d522543de7e3a4534bf528505Paolo Torriniids_C_SIG_ITEM :: C_SIG_ITEM -> IdSets

10a92a06296c3c8d522543de7e3a4534bf528505Paolo Torriniids_C_SIG_ITEM (CoDatatype_items al _) =

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (unite2 $ map (ids_CODATATYPE_DECL . item) al, Set.empty)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederids_CODATATYPE_DECL :: CODATATYPE_DECL -> (Set.Set Id, Set.Set Id)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederids_CODATATYPE_DECL (CoDatatype_decl _ al _) =

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder unite2 $ map (ids_COALTERNATIVE . item) al

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederids_COALTERNATIVE :: COALTERNATIVE -> (Set.Set Id, Set.Set Id)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederids_COALTERNATIVE a = let e = Set.empty in case a of

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Co_construct _ mi cs _ -> let s = maybe Set.empty Set.singleton mi in

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder if null cs then (s, e) else

eaa2614d79ad5ef6a6b9b08c7e6dde46c5ad1fb3Till Mossakowski (e, Set.unions $ s : map ids_COCOMPONENTS cs)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CoSubsorts _ _ -> (e, e)

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederids_COCOMPONENTS :: COCOMPONENTS -> Set.Set Id

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederids_COCOMPONENTS (CoSelect l _ _) = Set.unions $ map Set.singleton l

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdata CoRecord a b c d = CoRecord

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder { foldBoxOrDiamond :: C_FORMULA -> Bool -> d -> a -> Range -> c

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , foldCoSort_gen_ax :: C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> c

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , foldTerm_mod :: MODALITY -> b -> d

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , foldSimple_mod :: MODALITY -> SIMPLE_ID -> d

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder }

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederfoldC_Formula :: Record C_FORMULA a b -> CoRecord a b c d -> C_FORMULA -> c

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederfoldC_Formula r cr c = case c of

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder BoxOrDiamond b m f ps ->

13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder foldBoxOrDiamond cr c b (foldModality r cr m) (foldFormula r f) ps

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CoSort_gen_ax s o b -> foldCoSort_gen_ax cr c s o b

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederfoldModality :: Record C_FORMULA a b -> CoRecord a b c d -> MODALITY -> d

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederfoldModality r cr m = case m of

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Term_mod t -> foldTerm_mod cr m $ foldTerm r t

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Simple_mod i -> foldSimple_mod cr m i

d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder

mapCoRecord :: CoRecord (FORMULA C_FORMULA) (TERM C_FORMULA) C_FORMULA MODALITY

mapCoRecord = CoRecord

{ foldBoxOrDiamond = const BoxOrDiamond

, foldCoSort_gen_ax = const CoSort_gen_ax

, foldTerm_mod = const Term_mod

, foldSimple_mod = const Simple_mod

}

constCoRecord :: ([a] -> a) -> a -> CoRecord a a a a

constCoRecord jn c = CoRecord

{ foldBoxOrDiamond = \ _ _ m f _ -> jn [m, f]

, foldCoSort_gen_ax = \ _ _ _ _ -> c

, foldTerm_mod = \ _ t -> t

, foldSimple_mod = \ _ _ -> c

}

mapC_FORMULA :: C_FORMULA -> C_FORMULA

mapC_FORMULA = foldC_Formula (mkMixfixRecord mapC_FORMULA) mapCoRecord

resolveMODALITY :: MixResolve MODALITY

resolveMODALITY ga ids m = case m of

Term_mod t ->

fmap Term_mod $ resolveMixTrm mapC_FORMULA resolveC_FORMULA ga ids t

_ -> return m

resolveC_FORMULA :: MixResolve C_FORMULA

resolveC_FORMULA ga ids cf = case cf of

BoxOrDiamond b m f ps -> do

nm <- resolveMODALITY ga ids m

nf <- resolveMixFrm mapC_FORMULA resolveC_FORMULA ga ids f

return $ BoxOrDiamond b nm nf ps

_ -> error "resolveC_FORMULA"

minExpForm :: Min C_FORMULA CoCASLSign

minExpForm s form =

let ops = formulaIds s

minMod md ps = case md of

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

Term_mod t -> let

r = do

t2 <- oneExpTerm minExpForm s t

let srt = sortOfTerm t2

trm = Term_mod t2

if Set.member srt ops

then return trm

else Result [mkDiag Error

("unknown modality '"

++ showId srt "' for term") t ]

$ Just trm

in case t of

Mixfix_token tm ->

if Set.member (simpleIdToId tm) ops

then return $ Simple_mod tm

else case maybeResult r of

Nothing -> Result

[mkDiag Error "unknown modality" tm]

$ Just $ Simple_mod tm

_ -> r

_ -> r

in case form of

BoxOrDiamond b m f ps ->

do nm <- minMod m ps

f2 <- minExpFORMULA minExpForm s f

return $ BoxOrDiamond b nm f2 ps

phi -> return phi

ana_C_SIG_ITEM :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign

ana_C_SIG_ITEM _ mi = case mi of

CoDatatype_items al _ ->

do mapM_ (\ i -> case item i of

CoDatatype_decl s _ _ -> addSort NonEmptySorts i s) al

mapAnM (ana_CODATATYPE_DECL Loose) al

closeSubsortRel

return mi

isCoConsAlt :: COALTERNATIVE -> Bool

isCoConsAlt a = case a of

CoSubsorts _ _ -> False

_ -> True

getCoSubsorts :: COALTERNATIVE -> [SORT]

getCoSubsorts c = case c of

CoSubsorts cs _ -> cs

_ -> []

-- | return list of constructors

ana_CODATATYPE_DECL :: GenKind -> CODATATYPE_DECL -> State CSign [Component]

ana_CODATATYPE_DECL gk (CoDatatype_decl s al _) = do

ul <- mapM (ana_COALTERNATIVE s) al

let constr = catMaybes ul

cs = map fst constr

unless (null constr) $ do

addDiags $ checkUniqueness cs

let totalSels = Set.unions $ map snd constr

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

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

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

showDoc (Set.toList totalSels)

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

case gk of

Free -> do

let (alts, subs) = partition isCoConsAlt $ map item al

sbs = concatMap getCoSubsorts subs

comps = map (getCoConsType s) alts

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

. coselForms1 "X") comps

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

addSentences $ mapMaybe comakeInjective

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

comps

addSentences $ makeDisjSubsorts s sbs

addSentences $ catMaybes $ concatMap

(\ c -> map (comakeDisjToSort c) sbs)

comps

addSentences $ comakeDisjoint comps

let ttrips' = [(a, vs, t, ses) | (Just (a, t), vs, ses) <- ttrips]

addSentences $ catMaybes $ concatMap

(\ ses ->

map (makeUndefForm ses) ttrips') sels

_ -> return ()

return cs

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

getCoConsType s c =

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

CoSubsorts _ _ -> error "getCoConsType"

Co_construct k a l _ -> (k, a, l)

in (i, OpType part (concatMap

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

getCoCompType :: SORT -> COCOMPONENTS -> [(Id, OpType)]

getCoCompType s (CoSelect l (Op_type k args res _) _) =

map (\ i -> (i, OpType k (args ++ [s]) res)) l

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

coselForms x = case coselForms1 "X" x of

(Just (i, f), vs, cs) -> makeSelForms 1 (i, vs, f, cs)

_ -> []

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

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

coselForms1 str (i, ty, il) =

let cs = concatMap (getCoCompType $ opRes ty) il

vs = genSelVars str 1 $ map snd cs

it = case i of

Nothing -> Nothing

Just i' -> Just (i', Application (Qual_op_name i'

(toOP_TYPE ty) nullRange)

(map toQualVar vs) nullRange)

in (it, vs, map (\ (j, typ) -> (Just j, typ)) cs)

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

-> Maybe (Named (FORMULA f))

comakeDisjToSort a s = do

let (i, v, _) = coselForms1 "X" a

p = posOfId s

(c, t) <- i

return $ makeNamed ("ga_disjoint_" ++ showId c "_sort_" ++ showId s "")

$ mkForall v (Negation (Membership t s p) p) p

comakeInjective :: (Maybe Id, OpType, [COCOMPONENTS])

-> Maybe (Named (FORMULA f))

comakeInjective a = do

let (i1, v1, _) = coselForms1 "X" a

(i2, v2, _) = coselForms1 "Y" a

(c, t1) <- i1

(_, t2) <- i2

let p = posOfId c

return $ makeNamed ("ga_injective_" ++ showId c "") $

mkForall (v1 ++ v2)

(Equivalence (Strong_equation t1 t2 p)

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

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

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

p) p

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

comakeDisjoint l = case l of

[] -> []

a : as -> mapMaybe (comakeDisj a) as ++ comakeDisjoint as

comakeDisj :: (Maybe Id, OpType, [COCOMPONENTS])

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

-> Maybe (Named (FORMULA f))

comakeDisj a1 a2 = do

let (i1, v1, _) = coselForms1 "X" a1

(i2, v2, _) = coselForms1 "Y" a2

(c1, t1) <- i1

(c2, t2) <- i2

let p = posOfId c1 `appRange` posOfId c2

return $ makeNamed ("ga_disjoint_" ++ showId c1 "_" ++ showId c2 "")

$ mkForall (v1 ++ v2) (Negation (Strong_equation t1 t2 p) p) p

-- | return the constructor and the set of total selectors

ana_COALTERNATIVE :: SORT -> Annoted COALTERNATIVE

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

ana_COALTERNATIVE s c = case item c of

CoSubsorts ss _ -> do

mapM_ (addSubsort s) ss

return Nothing

ci -> do

let cons@(i, ty, il) = getCoConsType s ci

ul <- mapM (ana_COCOMPONENTS s) il

let ts = concatMap fst ul

addDiags $ checkUniqueness (ts ++ concatMap snd ul)

addSentences $ coselForms cons

case i of

Nothing -> return Nothing

Just i' -> do

addOp c ty i'

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 (\ (i, ty) ->

do addOp (emptyAnno ()) ty i

return $ Just $ Component i ty) cs

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

ana_C_BASIC_ITEM

:: Ana C_BASIC_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign

ana_C_BASIC_ITEM mix bi = case bi of

CoFree_datatype al ps ->

do mapM_ (\ i -> case item i of

CoDatatype_decl s _ _ -> addSort NonEmptySorts i s) al

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 mix ([], al)

toCoSortGenAx ps False $ unionGenAx gs

return $ CoSort_gen ul ps

toCoSortGenAx :: Range -> Bool -> GenAx -> State CSign ()

toCoSortGenAx ps isFree (sorts, rel, ops) = do

let sortList = Set.toList sorts

opSyms = map (\ c -> let ide = compId c in Qual_op_name ide

(toOP_TYPE $ compType c) $ posOfId ide) $ Set.toList ops

injSyms = map (\ (s, t) -> let p = posOfId s in

Qual_op_name (mkUniqueInjName s t)

(Op_type Total [s] t p) p) $ Rel.toList rel

when (null sortList)

$ addDiags [Diag Error "missing cogenerated sort" ps]

addSentences [makeNamed ("ga_cogenerated_" ++ showSepList (showString "_")

showId sortList "")

$ ExtFORMULA $ CoSort_gen_ax sortList

(opSyms ++ injSyms) isFree]

ana_CoGenerated :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign

-> Ana ([GenAx], [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)])

C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign

ana_CoGenerated anaf mix (_, al) = do

ul <- mapAnM (ana_SIG_ITEMS minExpForm anaf mix Generated) al

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

getCoGenSig :: SIG_ITEMS C_SIG_ITEM C_FORMULA -> GenAx

getCoGenSig si = case si of

Sort_items _ al _ -> unionGenAx $ map (getGenSorts . item) al

Op_items al _ -> (Set.empty, Rel.empty,

Set.unions (map (getOps . item) al))

Datatype_items _ dl _ -> getDataGenSig dl

Ext_SIG_ITEMS (CoDatatype_items dl _) -> getCoDataGenSig dl

_ -> emptyGenAx

getCoDataGenSig :: [Annoted CODATATYPE_DECL] -> GenAx

getCoDataGenSig dl =

let get_sel (s, a) = case a of

CoSubsorts _ _ -> []

Co_construct _ _ l _ -> concatMap (getCoCompType s) l

alts = concatMap ((\ (CoDatatype_decl s al _) ->

map (\ a -> (s, item a)) al) . item) dl

sorts = map fst alts

(realAlts, subs) = partition (isCoConsAlt . snd) alts

sels = map (uncurry Component) $ concatMap get_sel realAlts

rel = foldr (\ (t, a) r -> foldr (`Rel.insert` t) r $ getCoSubsorts a)

Rel.empty subs

in (Set.fromList sorts, rel, Set.fromList sels)