{- |

Module : ./ExtModal/StatAna.hs

Copyright : DFKI GmbH 2009

License : GPLv2 or higher, see LICENSE.txt

Maintainer : codruta.liliana@gmail.com

Stability : experimental

Portability : portable

static analysis of modal logic parts

-}

module ExtModal.StatAna where

import ExtModal.AS_ExtModal

import ExtModal.Print_AS ()

import ExtModal.ExtModalSign

import CASL.Fold

import CASL.Sign

import CASL.MixfixParser

import CASL.StaticAna

import CASL.AS_Basic_CASL

import CASL.ShowMixfix

import CASL.Overload

import CASL.Quantification

import Common.AS_Annotation

import Common.Doc

import Common.DocUtils

import Common.GlobalAnnotations

import Common.Keywords

import Common.Lib.State

import Common.Id

import Common.Result

import Common.ExtSign

import qualified Common.Lib.MapSet as MapSet

import Data.Function

import qualified Data.Map as Map

import qualified Data.Set as Set

import Control.Monad

instance TermExtension EM_FORMULA where

freeVarsOfExt sign frm = case frm of

PrefixForm p f _ ->

Set.union (freePrefixVars sign p) $ freeVars sign f

UntilSince _ f1 f2 _ -> on Set.union (freeVars sign) f1 f2

ModForm (ModDefn _ _ _ afs _) ->

Set.unions $ map (freeVars sign . item)

$ concatMap (frameForms . item) afs

freePrefixVars :: Sign EM_FORMULA e -> FormPrefix -> Set.Set (VAR, SORT)

freePrefixVars sign fp = case fp of

BoxOrDiamond _ m _ _ -> freeModVars sign m

_ -> Set.empty

freeModVars :: Sign EM_FORMULA e -> MODALITY -> Set.Set (VAR, SORT)

freeModVars sign md = case md of

SimpleMod _ -> Set.empty

TermMod t -> freeTermVars sign t

ModOp _ m1 m2 -> on Set.union (freeModVars sign) m1 m2

TransClos m -> freeModVars sign m

Guard f -> freeVars sign f

basicEModalAnalysis

:: (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA

, Sign EM_FORMULA EModalSign, GlobalAnnos)

-> Result (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA

, ExtSign (Sign EM_FORMULA EModalSign) Symbol

, [Named (FORMULA EM_FORMULA)])

basicEModalAnalysis s = do

a@(_, ExtSign sig _, sens) <-

basicAnalysis frmTypeAna basItemStatAna sigItemStatAna mixfixAna s

checkConstr sig sens

return a

checkConstr :: Sign EM_FORMULA EModalSign -> [Named (FORMULA EM_FORMULA)]

-> Result ()

checkConstr sig sens =

let cs = interOpMapSet

(Set.fold (uncurry addOpTo) MapSet.empty $ getConstructors sens)

$ flexOps $ extendedInfo sig

in unless (MapSet.null cs) $ fail $ "constructors must not be flexible:\n"

++ show (printSetMap empty empty $ MapSet.toMap cs)

frmTypeAna :: Min EM_FORMULA EModalSign

frmTypeAna sign form = let

checkMod term_mod = case term_mod of

SimpleMod s_id ->

if tokStr s_id == emptyS

|| Set.member (simpleIdToId s_id) (modalities $ extendedInfo sign)

then return $ SimpleMod s_id

else Result [mkDiag Error "unknown modality" s_id]

$ Just $ SimpleMod s_id

ModOp o md1 md2 -> do

new_md1 <- checkMod md1

new_md2 <- checkMod md2

return $ ModOp o new_md1 new_md2

TransClos md -> fmap TransClos $ checkMod md

Guard frm -> fmap Guard $ minExpFORMULA frmTypeAna sign frm

TermMod t -> let

ms = modalities $ extendedInfo sign

r = do

t2 <- oneExpTerm frmTypeAna sign t

let srt = sortOfTerm t2

trm = TermMod t2

supers = supersortsOf srt sign

if Set.null $ Set.intersection (Set.insert srt supers) ms

then Result [mkDiag Error

("unknown term modality sort '"

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

$ Just trm

else return trm

in case t of

Mixfix_token tm ->

if Set.member (simpleIdToId tm) ms

|| tokStr tm == emptyS

then return $ SimpleMod tm

else Result

[mkDiag Error "unknown modality" tm]

$ Just $ SimpleMod tm

Application (Op_name (Id [tm] [] _)) [] _ ->

if Set.member (simpleIdToId tm) ms

then return $ SimpleMod tm

else r

_ -> r

checkFrame (FrameForm vs fs r) = do

nfs <- mapAnM (minExpFORMULA frmTypeAna sign . mkForall vs) fs

return $ FrameForm [] nfs r

checkPrefix pf = case pf of

BoxOrDiamond choice md leq_geq number -> do

new_md <- checkMod md

let new_pf = BoxOrDiamond choice new_md leq_geq number

if number >= 0

then return new_pf

else Result [mkDiag Error "negative number grading" number]

$ Just new_pf

Hybrid _ nm ->

if Set.member (nomPId nm) (nominals $ extendedInfo sign)

then return pf

else Result [mkDiag Error "unknown nominal" nm]

$ Just pf

_ -> return pf

in case form of

PrefixForm pf f pos -> do

new_pf <- checkPrefix pf

new_f <- minExpFORMULA frmTypeAna sign f

return $ PrefixForm new_pf new_f pos

UntilSince choice f1 f2 pos -> do

new_f1 <- minExpFORMULA frmTypeAna sign f1

new_f2 <- minExpFORMULA frmTypeAna sign f2

return $ UntilSince choice new_f1 new_f2 pos

ModForm (ModDefn is_time isTerm anno_list forms pos) -> do

new_forms <- mapAnM checkFrame forms

return $ ModForm $ ModDefn is_time isTerm anno_list new_forms pos

anaFrameForm :: Mix b s EM_FORMULA EModalSign -> FrameForm

-> State (Sign EM_FORMULA EModalSign) (FrameForm, FrameForm)

anaFrameForm mix ff@(FrameForm vs fs r) = if null fs then do

mapM_ addVars vs

return (ff, ff)

else do

(resFs, fufs) <- anaLocalVarForms (anaFORMULA mix) vs fs r

return (FrameForm vs resFs r, FrameForm [] fufs r)

clearVarMap :: State (Sign f e) ()

clearVarMap = do

e <- get

put e { varMap = Map.empty }

modItemStatAna

:: Ana ModDefn EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign

modItemStatAna mix (ModDefn is_time isTerm anno_list forms pos) = do

mapM_ ( (updateExtInfo . addMod) . item ) anno_list

clearVarMap -- forget vars beyond this point

new_forms <- mapAnM (anaFrameForm mix) forms

clearVarMap -- forget vars after this point

let res_forms = map (fmap fst) new_forms

ana_forms = filter (not . null . frameForms . item)

$ map (fmap snd) new_forms

unless (null ana_forms)

$ addSentences $ map (\ af ->

(makeNamed (getRLabel af) $ ExtFORMULA $ ModForm

$ ModDefn is_time isTerm anno_list [emptyAnno $ item af] pos)

{ isAxiom = notImplied af })

ana_forms

when is_time $ mapM_ (updateExtInfo . addTimeMod . item ) anno_list

when isTerm $ do

sig <- get

mapM_ ( (updateExtInfo . addTermMod sig) . item ) anno_list

return $ ModDefn is_time isTerm anno_list res_forms pos

basItemStatAna

:: Ana EM_BASIC_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign

basItemStatAna mix basic_item = case basic_item of

ModItem md -> fmap ModItem $ modItemStatAna mix md

Nominal_decl anno_list pos -> do

mapM_ (updateExtInfo . addNom . nomPId . item) anno_list

mapM_ (addPred (emptyAnno ()) nomPType . nomPId . item) anno_list

return $ Nominal_decl anno_list pos

addTermMod :: Sign f e -> Id -> EModalSign -> Result EModalSign

addTermMod fullSign tmi sgn = let

tm = termMods sgn

srts = sortSet fullSign

in if Set.member tmi srts then

if Set.member tmi tm

then Result [mkDiag Hint "repeated term modality" tmi] $ Just sgn

else let sps = Set.intersection tm $ supersortsOf tmi fullSign in

if Set.null sps

then return sgn { termMods = Set.insert tmi tm }

else Result [mkDiag Warning

("term modality known for supersorts " ++ showDoc sps "")

tmi] $ Just sgn

else Result [mkDiag Error "unknown sort in term modality" tmi] $ Just sgn

addTimeMod :: Id -> EModalSign -> Result EModalSign

addTimeMod tmi sgn = let tm = timeMods sgn in

if Set.member tmi tm

then Result [mkDiag Hint "repeated time modality" tmi] $ Just sgn

else if Set.size tm >= 1

then Result [mkDiag Hint "more than one time modality" tmi] $ Just sgn

else return sgn { timeMods = Set.insert tmi tm }

addMod :: Id -> EModalSign -> Result EModalSign

addMod mi sgn =

let m = modalities sgn in

if Set.member mi m then

Result [mkDiag Hint "repeated modality" mi] $ Just sgn

else return sgn { modalities = Set.insert mi m }

addNom :: Id -> EModalSign -> Result EModalSign

addNom ni sgn =

let n = nominals sgn in

if Set.member ni n then

Result [mkDiag Hint "repeated nominal" ni] $ Just sgn

else return sgn { nominals = Set.insert ni n }

sigItemStatAna

:: Ana EM_SIG_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign

sigItemStatAna mix sig_item = case sig_item of

Rigid_op_items rig ann_list pos -> do

new_list <- mapM (ana_OP_ITEM frmTypeAna mix) ann_list

unless rig $ mapM_

(\ nlitem -> case item nlitem of

Op_decl ops typ _ _ ->

mapM_ (updateExtInfo . addFlexOp (toOpType typ)) ops

Op_defn op hd _ _ -> maybe (return ())

(\ ty -> updateExtInfo $ addFlexOp (toOpType ty) op)

$ headToType hd

) new_list

return $ Rigid_op_items rig new_list pos

Rigid_pred_items rig ann_list pos -> do

new_list <- mapM (ana_PRED_ITEM frmTypeAna mix) ann_list

unless rig $ mapM_ ( \ nlitem -> case item nlitem of

Pred_decl preds typ _ ->

mapM_ (updateExtInfo . addFlexPred (toPredType typ) ) preds

Pred_defn prd (Pred_head args _ ) _ _ ->

updateExtInfo $ addFlexPred (PredType $ sortsOfArgs args) prd

) new_list

return $ Rigid_pred_items rig new_list pos

addFlexOp :: OpType -> Id -> EModalSign -> Result EModalSign

addFlexOp typ i sgn = return

sgn { flexOps = addOpTo i typ $ flexOps sgn }

addFlexPred :: PredType -> Id -> EModalSign -> Result EModalSign

addFlexPred typ i sgn = return

sgn { flexPreds = MapSet.insert i typ $ flexPreds sgn }

mixfixAna :: Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign

mixfixAna = emptyMix

{ getSigIds = extraSigItems

, putParen = parenExtForm

, mixResolve = resolveExtForm

}

extraSigItems :: EM_SIG_ITEM -> IdSets

extraSigItems s = let e = Set.empty in case s of

Rigid_op_items _ annoted_list _ ->

(unite2 $ map (ids_OP_ITEM . item) annoted_list, e)

Rigid_pred_items _ annoted_list _ ->

((e, e), Set.unions $ map (ids_PRED_ITEM . item) annoted_list)

parenExtForm :: EM_FORMULA -> EM_FORMULA

parenExtForm = mapExtForm (mapFormula parenExtForm)

mapExtMod :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)

-> MODALITY -> MODALITY

mapExtMod f m = case m of

ModOp o md1 md2 -> on (ModOp o) (mapExtMod f) md1 md2

TransClos md -> TransClos $ mapExtMod f md

Guard frm -> Guard $ f frm

TermMod t -> let Mixfix_formula n = f (Mixfix_formula t) in TermMod n

_ -> m

mapExtPrefix :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)

-> FormPrefix -> FormPrefix

mapExtPrefix f pf = case pf of

BoxOrDiamond choice md leq_geq nr ->

BoxOrDiamond choice (mapExtMod f md) leq_geq nr

_ -> pf

mapExtForm :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)

-> EM_FORMULA -> EM_FORMULA

mapExtForm f ef = case ef of

PrefixForm p frm pos ->

PrefixForm (mapExtPrefix f p) (f frm) pos

UntilSince choice f1 f2 pos ->

UntilSince choice (f f1) (f f2) pos

ModForm (ModDefn ti te is fs pos) -> ModForm $ ModDefn

ti te is (map (fmap $ mapExtFrameForm f) fs) pos

mapExtFrameForm :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)

-> FrameForm -> FrameForm

mapExtFrameForm f (FrameForm vs fs r) = FrameForm vs (map (fmap f) fs) r

resolveMod :: MixResolve MODALITY

resolveMod ga ids m = case m of

ModOp o md1 md2 -> do

new_md1 <- resolveMod ga ids md1

new_md2 <- resolveMod ga ids md2

return $ ModOp o new_md1 new_md2

TransClos md -> fmap TransClos $ resolveMod ga ids md

Guard frm -> fmap Guard

$ resolveMixFrm parenExtForm resolveExtForm ga ids frm

TermMod t -> fmap TermMod

$ resolveMixTrm parenExtForm resolveExtForm ga ids t

_ -> return m

resolvePrefix :: MixResolve FormPrefix

resolvePrefix ga ids pf = case pf of

BoxOrDiamond choice ms leq_geq nr -> do

nms <- resolveMod ga ids ms

return $ BoxOrDiamond choice nms leq_geq nr

_ -> return pf

resolveExtForm :: MixResolve EM_FORMULA

resolveExtForm ga ids f =

let recResolve = resolveMixFrm parenExtForm resolveExtForm ga ids

in case f of

PrefixForm p frm pos -> do

np <- resolvePrefix ga ids p

new_frm <- recResolve frm

return $ PrefixForm np new_frm pos

UntilSince choice f1 f2 pos -> do

new_f1 <- recResolve f1

new_f2 <- recResolve f2

return $ UntilSince choice new_f1 new_f2 pos

ModForm (ModDefn ti te is fs pos) -> do

nfs <- mapAnM (resolveFrameForm ga ids) fs

return $ ModForm $ ModDefn ti te is nfs pos

resolveFrameForm :: MixResolve FrameForm

resolveFrameForm ga ids (FrameForm vs fs r) = do

let ts = varDeclTokens vs

nfs <- mapAnM (resolveMixFrm parenExtForm

(extendMixResolve ts resolveExtForm) ga

$ extendRules ts ids) fs

return $ FrameForm vs nfs r

anaFORMULA :: Mix b s EM_FORMULA EModalSign -> Sign EM_FORMULA EModalSign

-> FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA, FORMULA EM_FORMULA)

anaFORMULA mix sig f = do

let mix2 = extendMix (Map.keysSet $ varMap sig) mix

-- the unknown predicates are not needed for mixfix resolution

r <- resolveFormula parenExtForm

resolveExtForm (globAnnos sig) (mixRules mix2) f

let q = Set.fold

(\ t -> QuantPred (simpleIdToId t) (Pred_type [] $ tokPos t))

r $ getFormPredToks f

n <- minExpFORMULA frmTypeAna sig q

return (r, n)

getEFormPredToks :: EM_FORMULA -> Set.Set Token

getEFormPredToks ef = case ef of

PrefixForm _ f _ -> getFormPredToks f

UntilSince _ f1 f2 _ -> on Set.union getFormPredToks f1 f2

ModForm _ -> Set.empty

getFormPredToks :: FORMULA EM_FORMULA -> Set.Set Token

getFormPredToks = foldFormula

(constRecord getEFormPredToks Set.unions Set.empty)

{ foldMixfix_formula = \ f ts -> case f of

Mixfix_formula (Mixfix_token t) -> Set.singleton t

_ -> ts

, foldQuantPred = \ _ i _ ts -> if isSimpleId i then

Set.delete (idToSimpleId i) ts else ts

}