50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl{- |
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel ReichlModule : ./CASL_DL/StatAna.hs
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel ReichlDescription : static analysis of DL parts
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel ReichlCopyright : (c) Klaus Luettich, Uni Bremen 2005
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel ReichlLicense : GPLv2 or higher, see LICENSE.txt
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel ReichlMaintainer : luecke@informatik.uni-bremen.de
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel ReichlStability : provisional
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel ReichlPortability : portable
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlstatic analysis of DL parts especially cardinalities, predefined datatypes
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichland additional annottations
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl-}
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlmodule CASL_DL.StatAna ( basicCASL_DLAnalysis
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl , minDLForm
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl , checkSymbolMapDL
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl , DLSign) where
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL_DL.AS_CASL_DL
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL_DL.Print_AS ()
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL_DL.Sign
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL_DL.PredefinedCASLAxioms
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL.Sign
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL.MixfixParser
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL.Morphism
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL.StaticAna
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL.AS_Basic_CASL
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL.ShowMixfix
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL.Overload
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport CASL.Quantification
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport Common.AS_Annotation
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport Common.GlobalAnnotations
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport Common.ConvertGlobalAnnos
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport Common.DocUtils
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport Common.Id
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport Common.Result
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport Common.ConvertLiteral
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport Common.ExtSign
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport qualified Common.Lib.MapSet as MapSet
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport qualified Common.Lib.Rel as Rel
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport qualified Data.Map as Map
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlimport qualified Data.Set as Set
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichlinstance TermExtension DL_FORMULA where
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl freeVarsOfExt sign (Cardinality _ _ t1 t2 mf _) =
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl Set.union (freeTermVars sign t1) $ Set.union (freeTermVars sign t2)
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl $ case mf of
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl Nothing -> Set.empty
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl Just f -> freeVars sign f
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel ReichlbasicCASL_DLAnalysis
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl :: (BASIC_SPEC () () DL_FORMULA, Sign DL_FORMULA CASL_DLSign, GlobalAnnos)
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl -> Result (BASIC_SPEC () () DL_FORMULA,
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl [Named (FORMULA DL_FORMULA)])
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel ReichlbasicCASL_DLAnalysis (bs, sig, ga) =
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl do ga' <- mergeGlobalAnnos ga $ globAnnos predefSign
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl let sig' = addSig addCASL_DLSign sig $ predefinedSign emptyCASL_DLSign
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl bs' = transformSortDeclarations True bs
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl case basicAnalysis minDLForm (const return)
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl (const return) ana_Mix (bs', sig', ga') of
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl r@(Result ds1 mr) ->
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl maybe r (cleanStatAnaResult . postAna ds1 sig') mr
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl{- |
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl True -> extend all sort declarations without a supersort
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl with supersort Thing
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl False -> remove Thing from all sort declarations with supersort Thing
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel Reichl-}
50b8a36b0932a510e825ed1ad8103f81ead2b7d8Pavel ReichlgenerateSubsorting :: Sign f e -> Sign f e
generateSubsorting sig =
let
inS = sortSet sig
inR = sortRel sig
in
sig
{
sortRel = Set.fold (\ x y -> Rel.insertDiffPair x thing y) inR inS
}
transformSortDeclarations :: Bool
-> BASIC_SPEC () () DL_FORMULA
-> BASIC_SPEC () () DL_FORMULA
transformSortDeclarations addThing (Basic_spec aBIs) =
Basic_spec (processBIs aBIs)
where processBIs = map (mapAn processBI)
processBI bi = case bi of
Sig_items sig_i -> Sig_items (processSig_i sig_i)
_ -> bi
processSig_i sig_i =
case sig_i of
Sort_items sk aSor_is r ->
Sort_items sk (concatMap processaSor_i aSor_is) r
_ -> sig_i
processaSor_i aSor_i =
case processSor_i (item aSor_i) of
[] -> []
x : xs -> replaceAnnoted x aSor_i : map emptyAnno xs
processSor_i sor_i =
if addThing
then
case sor_i of
Sort_decl sorts r ->
[Subsort_decl sorts thing r]
Subsort_decl _ supSort _
| supSort == thing -> [sor_i]
| otherwise ->
[ sor_i
, Subsort_decl [supSort] thing statAnaMarker]
_ -> [sor_i]
else
case sor_i of
Subsort_decl sorts supSort r
| supSort == thing -> if r == statAnaMarker
then []
else [Sort_decl sorts r]
| otherwise -> [sor_i]
_ -> [sor_i]
-- | marker for sig items added to a basic spec
statAnaMarker :: Range
statAnaMarker = Range [SourcePos ">:>added for DL.StaticAna<:<" 0 0]
{- |
* remove predefined symbols from a result of the static analysis
* remove all explicit references of Thing from the BSIC_SPEC
-}
cleanStatAnaResult
:: Result (BASIC_SPEC () () DL_FORMULA,
ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
[Named (FORMULA DL_FORMULA)])
-> Result (BASIC_SPEC () () DL_FORMULA,
ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
[Named (FORMULA DL_FORMULA)])
cleanStatAnaResult r@(Result ds1 mr) = maybe r clean mr
where clean (bs, ExtSign sig sys, sen) =
Result ds1 (Just (transformSortDeclarations False bs
, ExtSign (generateSubsorting $ cleanSign sig) $
Set.delete (idToSortSymbol thing) sys
, sen))
cleanSign sig =
diffSig diffCASL_DLSign sig $ predefinedSign emptyCASL_DLSign
{- |
postAna checks the Signature for
* all new sorts must be a proper subsort of Thing and
must not be related to DATA
* no new subsort relations with DATA
* all new predicates must have a subsort of Thing as subject (1st argument)
* all new operations must have a subsort of Thing as 1st argument
-}
postAna :: [Diagnosis]
-> Sign DL_FORMULA CASL_DLSign
-> (BASIC_SPEC () () DL_FORMULA,
ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
[Named (FORMULA DL_FORMULA)])
-> Result (BASIC_SPEC () () DL_FORMULA,
ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
[Named (FORMULA DL_FORMULA)])
postAna ds1 in_sig i@(_, ExtSign acc_sig _, _) =
Result (ds1 ++ ds_sig) $ if null ds_sig then Just i else Nothing
where ds_sig = chkSorts ++ checkPreds ++ checkOps
diff_sig = diffSig diffCASL_DLSign acc_sig in_sig
chkSorts = Set.fold chSort [] (sortSet diff_sig) ++
[Diag Error
("\n new subsort relations with data " ++
"topsort are not allowed") nullRange
| Set.member dataS (supersortsOf thing acc_sig) ||
Set.member dataS (subsortsOf thing acc_sig) ||
supersortsOf dataS predefSign /=
supersortsOf dataS acc_sig ||
selectDATAKernel (sortRel predefSign)
/= selectDATAKernel (sortRel acc_sig)]
chSort s ds = ds ++
[mkDiag Error
("\n new sort is not a subsort of '" ++
showDoc thing "':") s
| not $ Set.member thing $ supersortsOf s acc_sig]
++ [mkDiag Error
("\n new sort must not be a supersort of '" ++
showDoc thing "':") s
| Set.member thing (subsortsOf s acc_sig)]
selectDATAKernel rel =
Rel.intransKernel $ Rel.restrict rel $
Set.insert dataS
(subsortsOf dataS predefSign)
checkPreds = MapSet.foldWithKey chPred [] (predMap diff_sig)
chPred p ty = (chArgs "pred" p (predArgs ty) ++)
checkOps = MapSet.foldWithKey chOp [] (opMap diff_sig)
chOp o ty = (chArgs "op" o (opArgs ty) ++)
chArgs kstr sym args =
case args of
[] -> if kstr == "op"
then []
else [mkDiag Error
"\n propositional symbols are not allowed" sym]
(s : _) ->
if s == thing ||
Set.member thing (supersortsOf s acc_sig)
then []
else [mkDiag Error
("\n the first argument sort of this " ++ kstr ++
" is not a subsort of '" ++ showDoc thing "':")
sym]
{- sketch of Annotation analysis:
where callAna bsRes =
case analyseAnnos ga acc_sig bs of
Result ds2 mESig ->
maybe (Result (ds1++ds2) Nothing)
(integrateExt (ds1++ds2) baRes) mESig
integrateExt ds (bs',dif_sig,acc_sig,sens) eSig =
Result ds (bs',
dif_sig {extendedInfo = dif eSig (extendedInfo sig)},
acc_sig {extendedInfo = eSig},
sens)
-}
ana_Mix :: Mix () () DL_FORMULA CASL_DLSign
ana_Mix = emptyMix
{ putParen = mapDL_FORMULA
, mixResolve = resolveDL_FORMULA
}
type DLSign = Sign DL_FORMULA CASL_DLSign
mapDL_FORMULA :: DL_FORMULA -> DL_FORMULA
mapDL_FORMULA (Cardinality ct pn varTerm natTerm qualTerm ps) =
Cardinality ct pn (mapT varTerm) (mapT natTerm) qualTerm ps
where mapT = mapTerm mapDL_FORMULA
resolveDL_FORMULA :: MixResolve DL_FORMULA
resolveDL_FORMULA ga ids (Cardinality ct ps varTerm natTerm qualTerm ran) =
do vt <- resMixTerm varTerm
nt <- resMixTerm natTerm
mf <- case qualTerm of
Nothing -> return Nothing
Just f -> fmap Just $
resolveMixFrm mapDL_FORMULA resolveDL_FORMULA ga ids f
return $ Cardinality ct ps vt nt mf ran
where resMixTerm = resolveMixTrm mapDL_FORMULA
resolveDL_FORMULA ga ids
minDLForm :: Min DL_FORMULA CASL_DLSign
minDLForm sign form = case form of
Cardinality ct ps varTerm natTerm qualTerm ran ->
let pn = predSymbName ps
pn_RelTypes = Set.filter isBinPredType
$ MapSet.lookup pn (predMap sign)
in
if Set.null pn_RelTypes then
Result [Diag Error ("Unknown binary predicate: \"" ++
show pn ++ "\"") (posOfId pn)]
Nothing
else do
v2 <- oneExpTerm minDLForm sign varTerm
let v_sort = sortOfTerm v2
n2 <- oneExpTerm minDLForm sign natTerm
let n_sort = sortOfTerm n2
ps' <- case sub_sort_of_subj pn v_sort pn_RelTypes of
Result ds mts ->
let ds' =
if null ds
then [mkDiag Error
("Variable in cardinality constraint\n"
++ " has wrong type")
varTerm]
else ds
amigDs ts =
[Diag Error
("Ambiguous types found for\n pred '" ++
showDoc pn "' in cardinalty " ++
"constraint: (showing only two of them)\n" ++
" '" ++ showDoc (head ts) "', '" ++
showDoc (head $ tail ts) "'") ran]
in maybe (Result ds' Nothing)
(\ ts -> case ts of
[] -> error "CASL_DL.StatAna: Internal error"
[x] -> maybe
(return $
Qual_pred_name pn x nullRange)
(\ pt -> if x == pt
then return ps
else noPredTypeErr ps)
(getType ps)
_ -> maybe (Result (amigDs ts) Nothing)
(\ pt -> if pt `elem` ts
then return ps
else noPredTypeErr ps)
(getType ps))
mts
let isNatTerm =
if isNumberTerm (globAnnos sign) n2 &&
show n_sort == "nonNegativeInteger"
then []
else [mkDiag Error
("The second argument of a\n " ++
"cardinality constrain must be a " ++
"number literal\n typeable as " ++
"nonNegativeInteger")
natTerm]
ds = isNatTerm
appendDiags ds
if null ds
then return (Cardinality ct ps' v2 n2 qualTerm ran)
else Result [] Nothing
where
getType ps = case ps of
Pred_name _ -> Nothing
Qual_pred_name _ pType _ -> Just pType
isNumberTerm ga t =
maybe False (uncurry (isNumber ga)) (splitApplM t)
noPredTypeErr ps = Result
[mkDiag Error "no predicate with \n given type found" ps]
Nothing
sub_sort_of_subj pn v_sort typeSet =
foldl (\ (Result ds mv) pt ->
case predArgs pt of
(s : _)
| leqSort sign v_sort s ->
maybe (Result ds $ Just [toPRED_TYPE pt])
(\ l -> Result ds $
Just $ l ++ [toPRED_TYPE pt])
mv
| otherwise ->
Result ds mv
_ -> Result (ds ++ [mkDiag Error
("no propositional " ++
"symbols are allowed\n "
++ "within cardinality " ++
"constraints")
pn]) mv
) (Result [] Nothing) $ Set.toList typeSet
-- | symbol map analysis
checkSymbolMapDL :: RawSymbolMap -> Result RawSymbolMap
{- - implement a symbol mapping that forbids mapping of predefined symbols
from emptySign
use from Logic.Logic.Logic and from CASL:
matches, symOf, statSymbMapItems
-}
checkSymbolMapDL rsm =
let checkSourceSymbol sSym _ =
if any (`matches` sSym) symOfPredefinedSign then
(sSym :) else id
syms = Map.foldWithKey checkSourceSymbol [] rsm
in if null syms
then return rsm
else mkError "Predefined CASL_DL symbols cannot be mapped" syms
symOfPredefinedSign :: [Symbol]
symOfPredefinedSign = Set.toList . Set.unions $ symOf predefSign
isNumber :: GlobalAnnos -> Id -> [TERM f] -> Bool
isNumber = isGenNum splitApplM
splitApplM :: TERM f -> Maybe (Id, [TERM f])
splitApplM t = case t of
Application {} -> Just $ splitAppl t
_ -> Nothing
splitAppl :: TERM f -> (Id, [TERM f])
splitAppl t = case t of
Application oi ts _ -> (op_id oi, ts)
_ -> error "splitAppl: no Application found"
-- | extract the Id from any OP_SYMB
op_id :: OP_SYMB -> Id
op_id op = case op of
Qual_op_name x _ _ -> x
Op_name x -> x