3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller{- |

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan MmillerModule : $Header$

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan MmillerCopyright : (c) Christian Maeder, Uni Bremen 2004

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan MmillerLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan MmillerMaintainer : hets@tzi.de

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan MmillerStability : provisional

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan MmillerPortability : portable

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller static analysis of modal logic parts

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller-}

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller{- todo:

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller check quantifiers (sorts, variables in body) in ana_M_FORMULA

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller-}

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillermodule Modal.StatAna where

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller--import Debug.Trace

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerimport Modal.AS_Modal

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerimport Modal.Print_AS

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerimport Modal.ModalSign

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerimport CASL.Sign

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerimport CASL.MixfixParser

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerimport CASL.StaticAna

3a666413480ef97101461705e1f47cbab0266301Brendan Mmillerimport CASL.AS_Basic_CASL

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerimport CASL.Overload

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmillerimport CASL.MapSentence

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerimport Common.AS_Annotation

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerimport qualified Common.Lib.Set as Set

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerimport qualified Common.Lib.Map as Map

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmillerimport Common.Lib.State

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmillerimport Common.Id

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmillerimport Common.Result

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan MmillerminExpForm :: Min M_FORMULA ModalSign

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan MmillerminExpForm ga s form =

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller let newGa = addAssocs ga s

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller ops = formulaIds s

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller preds = allPredIds s

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller res = resolveFormula newGa ops preds

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller minMod md ps = case md of

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller Term_mod t -> let

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller r = do

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller t1 <- resolveMixfix newGa (allOpIds s) preds t

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller ts <- minExpTerm minExpForm ga s t1

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller t2 <- is_unambiguous t ts ps

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller let srt = term_sort t2

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller trm = Term_mod t2

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller if Map.member srt $ termModies $ extendedInfo s

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller then return trm

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller else Result [mkDiag Error

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller ("unknown term modality sort '"

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller ++ showId srt "' for term") t ]

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller $ Just trm

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller in case t of

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller Mixfix_token tm ->

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller if Map.member tm $ modies $ extendedInfo s

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller then return $ Simple_mod tm

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller else case maybeResult r of

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller Nothing -> Result

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller [mkDiag Error "unknown modality" tm]

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller $ Just $ Simple_mod tm

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller _ -> r

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller _ -> r

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller in case form of

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller Box m f ps ->

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller do nm <- minMod m ps

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller f1 <- res f

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller f2 <- minExpFORMULA minExpForm ga s f1

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller return $ Box nm f2 ps

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller Diamond m f ps ->

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller do nm <- minMod m ps

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller f1 <- res f

3a666413480ef97101461705e1f47cbab0266301Brendan Mmiller f2 <- minExpFORMULA minExpForm ga s f1

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller return $ Diamond nm f2 ps

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerana_M_SIG_ITEM :: Ana M_SIG_ITEM M_FORMULA ModalSign

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillerana_M_SIG_ITEM ga mi =

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller case mi of

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller Rigid_op_items r al ps ->

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller do ul <- mapM (ana_OP_ITEM ga) al

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller case r of

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmiller Rigid -> mapM_ ( \ aoi -> case item aoi of

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmiller Op_decl ops ty _ _ ->

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmiller mapM_ (updateExtInfo . addRigidOp (toOpType ty)) ops

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmiller Op_defn i par _ _ ->

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller updateExtInfo $ addRigidOp (toOpType $ headToType par)

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller i ) ul

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller _ -> return ()

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller return $ Rigid_op_items r ul ps

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller Rigid_pred_items r al ps ->

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller do ul <- mapM (ana_PRED_ITEM ga) al

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmiller case r of

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller Rigid -> mapM_ ( \ aoi -> case item aoi of

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller Pred_decl ops ty _ ->

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller mapM_ (updateExtInfo . addRigidPred (toPredType ty)) ops

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller Pred_defn i (Pred_head args _) _ _ ->

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller updateExtInfo $ addRigidPred

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmiller (PredType $ sortsOfArgs args) i ) ul

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller _ -> return ()

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller return $ Rigid_pred_items r ul ps

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller

99054f32a1766b8a8f60509cb724359413171d1dBrendan MmilleraddRigidOp :: OpType -> Id -> ModalSign -> Result ModalSign

99054f32a1766b8a8f60509cb724359413171d1dBrendan MmilleraddRigidOp ty i m = return

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller m { rigidOps = addTo i ty { opKind = Partial } $ rigidOps m }

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller

99054f32a1766b8a8f60509cb724359413171d1dBrendan MmilleraddRigidPred :: PredType -> Id -> ModalSign -> Result ModalSign

99054f32a1766b8a8f60509cb724359413171d1dBrendan MmilleraddRigidPred ty i m = return

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller m { rigidPreds = addTo i ty $ rigidPreds m }

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmillerana_M_BASIC_ITEM :: Ana M_BASIC_ITEM M_FORMULA ModalSign

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmillerana_M_BASIC_ITEM _ bi = do

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller e <- get

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller case bi of

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller Simple_mod_decl al fs ps -> do

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller newFs <- mapAnM (resultToState (ana_M_FORMULA False)) fs

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller mapM_ ((updateExtInfo . addModId newFs) . item) al

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller return $ Simple_mod_decl al newFs ps

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller Term_mod_decl al fs ps -> do

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller newFs <- mapAnM (resultToState (ana_M_FORMULA True)) fs

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller mapM_ ((updateExtInfo . addModSort newFs e) . item) al

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller return $ Term_mod_decl al newFs ps

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller

99054f32a1766b8a8f60509cb724359413171d1dBrendan MmillerresultToState :: (a -> Result a) -> a -> State (Sign f e) a

99054f32a1766b8a8f60509cb724359413171d1dBrendan MmillerresultToState f a = do

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller let r = f a

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller addDiags $ reverse $ diags r

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller case maybeResult r of

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller Nothing -> return a

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller Just b -> return b

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan MmilleraddModId :: [AnModFORM] -> SIMPLE_ID -> ModalSign -> Result ModalSign

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan MmilleraddModId frms i m =

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller let ms = modies m in

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller if Map.member i ms then

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller Result [mkDiag Hint "repeated modality" i] $ Just m

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller else return m { modies = Map.insert i frms ms }

ba208d3f0e9d48f3c841cdd627f200a7bb04cea8Brendan Mmiller

99054f32a1766b8a8f60509cb724359413171d1dBrendan MmilleraddModSort :: [AnModFORM] ->

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller Sign M_FORMULA ModalSign -> SORT -> ModalSign -> Result ModalSign

99054f32a1766b8a8f60509cb724359413171d1dBrendan MmilleraddModSort frms e i m =

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller let ms = termModies m

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller ds = hasSort e i

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller in if Map.member i ms || not (null ds) then

99054f32a1766b8a8f60509cb724359413171d1dBrendan Mmiller Result (mkDiag Hint "repeated term modality" i : ds) $ Just m

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller else return m { termModies = Map.insert i frms ms }

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmiller

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillermap_M_FORMULA :: MapSen M_FORMULA ModalSign ()

3f424ffdb194d6ff7ac053c5b3e53211a2de2d64Brendan Mmillermap_M_FORMULA mor frm =

let mapMod m = case m of

Simple_mod _ -> return m

Term_mod t -> do newT <- mapTerm map_M_FORMULA mor t

return $ Term_mod newT

in case frm of

Box m f ps -> do

newF <- mapSen map_M_FORMULA mor f

newM <- mapMod m

return $ Box newM newF ps

Diamond m f ps -> do

newF <- mapSen map_M_FORMULA mor f

newM <- mapMod m

return $ Diamond newM newF ps

ana_M_FORMULA :: Bool -> FORMULA M_FORMULA -> Result (FORMULA M_FORMULA)

ana_M_FORMULA b (Conjunction phis pos) = do

phis' <- mapM (ana_M_FORMULA b) phis

return (Conjunction phis' pos)

ana_M_FORMULA b (Disjunction phis pos) = do

phis' <- mapM (ana_M_FORMULA b) phis

return (Disjunction phis' pos)

ana_M_FORMULA b (Implication phi1 phi2 b1 pos) = do

phi1' <- ana_M_FORMULA b phi1

phi2' <- ana_M_FORMULA b phi2

return (Implication phi1' phi2' b1 pos)

ana_M_FORMULA b (Equivalence phi1 phi2 pos) = do

phi1' <- ana_M_FORMULA b phi1

phi2' <- ana_M_FORMULA b phi2

return (Equivalence phi1' phi2' pos)

ana_M_FORMULA b (Negation phi pos) = do

phi' <- ana_M_FORMULA b phi

return (Negation phi' pos)

ana_M_FORMULA _ phi@(True_atom _) = return phi

ana_M_FORMULA _ phi@(False_atom _) = return phi

ana_M_FORMULA _ (Mixfix_formula (Mixfix_token ident)) =

return (Predication (Qual_pred_name (mkId [ident])

(Pred_type [] []) [])

[] [])

ana_M_FORMULA b (ExtFORMULA (Box m phi pos)) = do

phi' <- ana_M_FORMULA b phi

return(ExtFORMULA (Box m phi' pos))

ana_M_FORMULA b (ExtFORMULA (Diamond m phi pos)) = do

phi' <- ana_M_FORMULA b phi

return(ExtFORMULA (Diamond m phi' pos))

ana_M_FORMULA b phi@(Quantification _ _ phi1 pos) =

if b then ana_M_FORMULA b phi1

else anaError phi pos

ana_M_FORMULA _ phi@(Predication _ _ pos) =

return phi -- should lookup predicate!

ana_M_FORMULA _ phi@(Definedness _ pos) =

anaError phi pos

ana_M_FORMULA _ phi@(Existl_equation _ _ pos) =

anaError phi pos

ana_M_FORMULA _ phi@(Strong_equation _ _ pos) =

anaError phi pos

ana_M_FORMULA _ phi@(Membership _ _ pos) =

anaError phi pos

ana_M_FORMULA _ phi@(Mixfix_formula _) =

return phi -- should do mixfix analysis and lookup predicate!

-- anaError phi [nullPos]

ana_M_FORMULA _ phi@(Unparsed_formula _ pos) =

anaError phi pos

ana_M_FORMULA _ phi@(Sort_gen_ax _ _) =

anaError phi [nullPos]

anaError :: a -> [Pos] -> Result a

anaError phi pos =

plain_error phi

"Modality declarations may only contain propositional axioms"

(headPos pos)