{- |

Module : $Header$

Description : static analysis for CoCASL

Copyright : (c) Till Mossakowski, Uni Bremen 2004-2005

License : GPLv2 or higher, see LICENSE.txt

Maintainer : hausmann@informatik.uni-bremen.de

Stability : provisional

Portability : portable

static analysis for CoCASL

-}

module CoCASL.StatAna where

import CoCASL.AS_CoCASL

import CoCASL.Print_AS ()

import CoCASL.CoCASLSign

import CASL.Sign

import CASL.MixfixParser

import CASL.ShowMixfix

import CASL.StaticAna

import CASL.AS_Basic_CASL

import CASL.Overload

import CASL.Quantification

import CASL.Fold

import Common.AS_Annotation

import Common.GlobalAnnotations

import qualified Data.Set as Set

import qualified Common.Lib.Rel as Rel

import Common.Lib.State

import Common.Id

import Common.Result

import Common.DocUtils

import Common.ExtSign

import Control.Monad

import Data.Maybe

import Data.List (partition)

type CSign = Sign C_FORMULA CoCASLSign

instance TermExtension C_FORMULA where

freeVarsOfExt sign cf = case cf of

BoxOrDiamond _ _ f _ -> freeVars sign f

_ -> Set.empty

basicCoCASLAnalysis

:: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,

Sign C_FORMULA CoCASLSign, GlobalAnnos)

-> Result (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,

ExtSign (Sign C_FORMULA CoCASLSign) Symbol,

[Named (FORMULA C_FORMULA)])

basicCoCASLAnalysis =

basicAnalysis minExpForm ana_C_BASIC_ITEM ana_C_SIG_ITEM ana_CMix

-- analyses cocasl sentences only

co_sen_analysis ::

(BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA, CSign, (FORMULA C_FORMULA))

-> Result (FORMULA C_FORMULA)

co_sen_analysis (bs,s,f) = let

mix = emptyMix

allIds = unite $

ids_BASIC_SPEC (getBaseIds mix) (getSigIds mix) bs

: getExtIds mix (extendedInfo s) :

[mkIdSets (allConstIds s) (allOpIds s)

$ allPredIds s]

mix' = mix { mixRules = makeRules emptyGlobalAnnos allIds}

in (liftM fst) $ anaForm minExpForm mix' s f

ana_CMix :: Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign

ana_CMix = emptyMix

{ getBaseIds = ids_C_BASIC_ITEM

, getSigIds = ids_C_SIG_ITEM

, getExtIds = \ e -> let c = constructors e in

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

, putParen = mapC_FORMULA

, mixResolve = resolveC_FORMULA

}

ids_C_BASIC_ITEM :: C_BASIC_ITEM -> IdSets

ids_C_BASIC_ITEM ci = case ci of

CoFree_datatype al _ ->

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

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

ids_C_SIG_ITEM :: C_SIG_ITEM -> IdSets

ids_C_SIG_ITEM (CoDatatype_items al _) =

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

ids_CODATATYPE_DECL :: CODATATYPE_DECL -> (Set.Set Id, Set.Set Id)

ids_CODATATYPE_DECL (CoDatatype_decl _ al _) =

unite2 $ map (ids_COALTERNATIVE . item) al

ids_COALTERNATIVE :: COALTERNATIVE -> (Set.Set Id, Set.Set Id)

ids_COALTERNATIVE a = let e = Set.empty in case a of

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

if null cs then (s, e) else

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

CoSubsorts _ _ -> (e, e)

ids_COCOMPONENTS :: COCOMPONENTS -> Set.Set Id

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

data CoRecord a b c d = CoRecord

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

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

, foldTerm_mod :: MODALITY -> b -> d

, foldSimple_mod :: MODALITY -> SIMPLE_ID -> d

}

foldC_Formula :: Record C_FORMULA a b -> CoRecord a b c d -> C_FORMULA -> c

foldC_Formula r cr c = case c of

BoxOrDiamond b m f ps ->

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

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

foldModality :: Record C_FORMULA a b -> CoRecord a b c d -> MODALITY -> d

foldModality r cr m = case m of

Term_mod t -> foldTerm_mod cr m $ foldTerm r t

Simple_mod i -> foldSimple_mod cr m i

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 "")

$ mkForallRange 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 "") $

mkForallRange (v1 ++ v2)

(Relation (Equation t1 Strong t2 p) Equivalence

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

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

in conjunctRange 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 "")

$ mkForallRange (v1 ++ v2) (Negation (Equation t1 Strong 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 (isTotal . 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.insertDiffPair` t) r $ getCoSubsorts a)

Rel.empty subs

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