074e084f68dd0b08686612bec695a0cfe249da6dml{- |

074e084f68dd0b08686612bec695a0cfe249da6dmlModule : $Header$

074e084f68dd0b08686612bec695a0cfe249da6dmlDescription : static analysis of DL parts

074e084f68dd0b08686612bec695a0cfe249da6dmlCopyright : (c) Klaus Luettich, Uni Bremen 2005

074e084f68dd0b08686612bec695a0cfe249da6dmlLicense : GPLv2 or higher, see LICENSE.txt

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dmlMaintainer : luecke@informatik.uni-bremen.de

074e084f68dd0b08686612bec695a0cfe249da6dmlStability : provisional

074e084f68dd0b08686612bec695a0cfe249da6dmlPortability : portable

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dmlstatic analysis of DL parts especially cardinalities, predefined datatypes

074e084f68dd0b08686612bec695a0cfe249da6dmland additional annottations

074e084f68dd0b08686612bec695a0cfe249da6dml-}

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dmlmodule CASL_DL.StatAna ( basicCASL_DLAnalysis

074e084f68dd0b08686612bec695a0cfe249da6dml , minDLForm

074e084f68dd0b08686612bec695a0cfe249da6dml , checkSymbolMapDL

074e084f68dd0b08686612bec695a0cfe249da6dml , DLSign) where

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL_DL.AS_CASL_DL

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL_DL.Print_AS ()

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL_DL.Sign

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL_DL.PredefinedSign

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL_DL.PredefinedGlobalAnnos

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL.Sign

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL.MixfixParser

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL.Morphism

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL.StaticAna

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL.AS_Basic_CASL

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL.ShowMixfix

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL.Overload

074e084f68dd0b08686612bec695a0cfe249da6dmlimport CASL.Quantification

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dmlimport qualified Data.Map as Map

074e084f68dd0b08686612bec695a0cfe249da6dmlimport qualified Data.Set as Set

074e084f68dd0b08686612bec695a0cfe249da6dmlimport qualified Common.Lib.Rel as Rel

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dmlimport Common.AS_Annotation

074e084f68dd0b08686612bec695a0cfe249da6dmlimport Common.GlobalAnnotations

074e084f68dd0b08686612bec695a0cfe249da6dmlimport Common.AnalyseAnnos

074e084f68dd0b08686612bec695a0cfe249da6dmlimport Common.DocUtils

074e084f68dd0b08686612bec695a0cfe249da6dmlimport Common.Id

074e084f68dd0b08686612bec695a0cfe249da6dmlimport Common.Result

074e084f68dd0b08686612bec695a0cfe249da6dmlimport Common.ConvertLiteral

074e084f68dd0b08686612bec695a0cfe249da6dmlimport Common.ExtSign

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dmlinstance FreeVars DL_FORMULA where

074e084f68dd0b08686612bec695a0cfe249da6dml freeVarsOfExt sign (Cardinality _ _ t1 t2 mf _) =

074e084f68dd0b08686612bec695a0cfe249da6dml Set.union (freeTermVars sign t1) $ Set.union (freeTermVars sign t2)

074e084f68dd0b08686612bec695a0cfe249da6dml $ case mf of

074e084f68dd0b08686612bec695a0cfe249da6dml Nothing -> Set.empty

074e084f68dd0b08686612bec695a0cfe249da6dml Just f -> freeVars sign f

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dmlinstance TermExtension DL_FORMULA where

074e084f68dd0b08686612bec695a0cfe249da6dml optTermSort = const Nothing

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dmlbasicCASL_DLAnalysis

074e084f68dd0b08686612bec695a0cfe249da6dml :: (BASIC_SPEC () () DL_FORMULA, Sign DL_FORMULA CASL_DLSign, GlobalAnnos)

074e084f68dd0b08686612bec695a0cfe249da6dml -> Result (BASIC_SPEC () () DL_FORMULA,

074e084f68dd0b08686612bec695a0cfe249da6dml ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,

074e084f68dd0b08686612bec695a0cfe249da6dml [Named (FORMULA DL_FORMULA)])

074e084f68dd0b08686612bec695a0cfe249da6dmlbasicCASL_DLAnalysis (bs, sig, ga) =

074e084f68dd0b08686612bec695a0cfe249da6dml do ga' <- addGlobalAnnos ga caslDLGlobalAnnos

074e084f68dd0b08686612bec695a0cfe249da6dml let sig' = addSig addCASL_DLSign sig predefinedSign

074e084f68dd0b08686612bec695a0cfe249da6dml bs' = transformSortDeclarations True bs

074e084f68dd0b08686612bec695a0cfe249da6dml case basicAnalysis minDLForm (const return)

074e084f68dd0b08686612bec695a0cfe249da6dml (const return) ana_Mix (bs', sig', ga') of

074e084f68dd0b08686612bec695a0cfe249da6dml r@(Result ds1 mr) ->

074e084f68dd0b08686612bec695a0cfe249da6dml maybe r (cleanStatAnaResult . postAna ds1 sig') mr

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dml{- |

074e084f68dd0b08686612bec695a0cfe249da6dml True -> extend all sort declarations without a supersort

074e084f68dd0b08686612bec695a0cfe249da6dml with supersort Thing

074e084f68dd0b08686612bec695a0cfe249da6dml False -> remove Thing from all sort declarations with supersort Thing

074e084f68dd0b08686612bec695a0cfe249da6dml-}

074e084f68dd0b08686612bec695a0cfe249da6dmlgenerateSubsorting :: Sign f e -> Sign f e

074e084f68dd0b08686612bec695a0cfe249da6dmlgenerateSubsorting sig =

074e084f68dd0b08686612bec695a0cfe249da6dml let

074e084f68dd0b08686612bec695a0cfe249da6dml inS = sortSet sig

074e084f68dd0b08686612bec695a0cfe249da6dml inR = sortRel sig

074e084f68dd0b08686612bec695a0cfe249da6dml in

074e084f68dd0b08686612bec695a0cfe249da6dml sig

074e084f68dd0b08686612bec695a0cfe249da6dml {

074e084f68dd0b08686612bec695a0cfe249da6dml sortRel = Set.fold (\ x y -> Rel.insert x topSort y) inR inS

074e084f68dd0b08686612bec695a0cfe249da6dml }

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dmltransformSortDeclarations :: Bool

074e084f68dd0b08686612bec695a0cfe249da6dml -> BASIC_SPEC () () DL_FORMULA

074e084f68dd0b08686612bec695a0cfe249da6dml -> BASIC_SPEC () () DL_FORMULA

074e084f68dd0b08686612bec695a0cfe249da6dmltransformSortDeclarations addThing (Basic_spec aBIs) =

074e084f68dd0b08686612bec695a0cfe249da6dml Basic_spec (processBIs aBIs)

074e084f68dd0b08686612bec695a0cfe249da6dml where processBIs = map (mapAn processBI)

074e084f68dd0b08686612bec695a0cfe249da6dml processBI bi = case bi of

074e084f68dd0b08686612bec695a0cfe249da6dml Sig_items sig_i -> Sig_items (processSig_i sig_i)

074e084f68dd0b08686612bec695a0cfe249da6dml _ -> bi

074e084f68dd0b08686612bec695a0cfe249da6dml processSig_i sig_i =

074e084f68dd0b08686612bec695a0cfe249da6dml case sig_i of

074e084f68dd0b08686612bec695a0cfe249da6dml Sort_items sk aSor_is r ->

074e084f68dd0b08686612bec695a0cfe249da6dml Sort_items sk (concatMap processaSor_i aSor_is) r

074e084f68dd0b08686612bec695a0cfe249da6dml _ -> sig_i

074e084f68dd0b08686612bec695a0cfe249da6dml processaSor_i aSor_i =

074e084f68dd0b08686612bec695a0cfe249da6dml case processSor_i (item aSor_i) of

074e084f68dd0b08686612bec695a0cfe249da6dml [] -> []

074e084f68dd0b08686612bec695a0cfe249da6dml x : xs -> replaceAnnoted x aSor_i : map emptyAnno xs

074e084f68dd0b08686612bec695a0cfe249da6dml processSor_i sor_i =

074e084f68dd0b08686612bec695a0cfe249da6dml if addThing

074e084f68dd0b08686612bec695a0cfe249da6dml then

074e084f68dd0b08686612bec695a0cfe249da6dml case sor_i of

074e084f68dd0b08686612bec695a0cfe249da6dml Sort_decl sorts r ->

074e084f68dd0b08686612bec695a0cfe249da6dml [Subsort_decl sorts topSort r]

074e084f68dd0b08686612bec695a0cfe249da6dml Subsort_decl _ supSort _

074e084f68dd0b08686612bec695a0cfe249da6dml | supSort == topSort -> [sor_i]

074e084f68dd0b08686612bec695a0cfe249da6dml | otherwise ->

074e084f68dd0b08686612bec695a0cfe249da6dml [ sor_i

074e084f68dd0b08686612bec695a0cfe249da6dml , Subsort_decl [supSort] topSort statAnaMarker]

074e084f68dd0b08686612bec695a0cfe249da6dml _ -> [sor_i]

074e084f68dd0b08686612bec695a0cfe249da6dml else

074e084f68dd0b08686612bec695a0cfe249da6dml case sor_i of

074e084f68dd0b08686612bec695a0cfe249da6dml Subsort_decl sorts supSort r

074e084f68dd0b08686612bec695a0cfe249da6dml | supSort == topSort -> if r == statAnaMarker

074e084f68dd0b08686612bec695a0cfe249da6dml then []

074e084f68dd0b08686612bec695a0cfe249da6dml else [Sort_decl sorts r]

074e084f68dd0b08686612bec695a0cfe249da6dml | otherwise -> [sor_i]

074e084f68dd0b08686612bec695a0cfe249da6dml _ -> [sor_i]

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dml-- | marker for sig items added to a basic spec

074e084f68dd0b08686612bec695a0cfe249da6dmlstatAnaMarker :: Range

074e084f68dd0b08686612bec695a0cfe249da6dmlstatAnaMarker = Range [SourcePos ">:>added for DL.StaticAna<:<" 0 0]

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dml{- |

074e084f68dd0b08686612bec695a0cfe249da6dml * remove predefined symbols from a result of the static analysis

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dml * remove all explicit references of Thing from the BSIC_SPEC

074e084f68dd0b08686612bec695a0cfe249da6dml-}

074e084f68dd0b08686612bec695a0cfe249da6dmlcleanStatAnaResult

074e084f68dd0b08686612bec695a0cfe249da6dml :: Result (BASIC_SPEC () () DL_FORMULA,

074e084f68dd0b08686612bec695a0cfe249da6dml ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,

074e084f68dd0b08686612bec695a0cfe249da6dml [Named (FORMULA DL_FORMULA)])

074e084f68dd0b08686612bec695a0cfe249da6dml -> Result (BASIC_SPEC () () DL_FORMULA,

074e084f68dd0b08686612bec695a0cfe249da6dml ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,

074e084f68dd0b08686612bec695a0cfe249da6dml [Named (FORMULA DL_FORMULA)])

074e084f68dd0b08686612bec695a0cfe249da6dmlcleanStatAnaResult r@(Result ds1 mr) = maybe r clean mr

074e084f68dd0b08686612bec695a0cfe249da6dml where clean (bs, ExtSign sig sys, sen) =

074e084f68dd0b08686612bec695a0cfe249da6dml Result ds1 (Just (transformSortDeclarations False bs

074e084f68dd0b08686612bec695a0cfe249da6dml , ExtSign (generateSubsorting $ cleanSign sig) $

074e084f68dd0b08686612bec695a0cfe249da6dml Set.delete (idToSortSymbol topSort) sys

074e084f68dd0b08686612bec695a0cfe249da6dml , sen))

074e084f68dd0b08686612bec695a0cfe249da6dml cleanSign sig =

074e084f68dd0b08686612bec695a0cfe249da6dml diffSig diffCASL_DLSign

074e084f68dd0b08686612bec695a0cfe249da6dml (sig {sortRel = Rel.delSet (Set.singleton topSort)

074e084f68dd0b08686612bec695a0cfe249da6dml $ sortRel sig})

074e084f68dd0b08686612bec695a0cfe249da6dml predefinedSign

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dml{- |

074e084f68dd0b08686612bec695a0cfe249da6dml postAna checks the Signature for

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dml * all new sorts must be a proper subsort of Thing and

074e084f68dd0b08686612bec695a0cfe249da6dml must not be related to DATA

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dml * no new subsort relations with DATA

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dml * all new predicates must have a subsort of Thing as subject (1st argument)

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dml * all new operations must have a subsort of Thing as 1st argument

074e084f68dd0b08686612bec695a0cfe249da6dml

074e084f68dd0b08686612bec695a0cfe249da6dml-}

074e084f68dd0b08686612bec695a0cfe249da6dmlpostAna :: [Diagnosis]

074e084f68dd0b08686612bec695a0cfe249da6dml -> Sign DL_FORMULA CASL_DLSign

074e084f68dd0b08686612bec695a0cfe249da6dml -> (BASIC_SPEC () () DL_FORMULA,

074e084f68dd0b08686612bec695a0cfe249da6dml ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,

074e084f68dd0b08686612bec695a0cfe249da6dml [Named (FORMULA DL_FORMULA)])

074e084f68dd0b08686612bec695a0cfe249da6dml -> Result (BASIC_SPEC () () DL_FORMULA,

074e084f68dd0b08686612bec695a0cfe249da6dml ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,

074e084f68dd0b08686612bec695a0cfe249da6dml [Named (FORMULA DL_FORMULA)])

da14cebe459d3275048785f25bd869cb09b5307fEric ChengpostAna ds1 in_sig i@(_, ExtSign acc_sig _, _) =

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng Result (ds1 ++ ds_sig) $ if null ds_sig then Just i else Nothing

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng where ds_sig = chkSorts ++ checkPreds ++ checkOps

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng diff_sig = diffSig diffCASL_DLSign acc_sig in_sig

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng chkSorts = Set.fold chSort [] (sortSet diff_sig) ++

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng [Diag Error

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng ("\n new subsort relations with data " ++

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng "topsort are not allowed") nullRange

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng | Set.member topSortD (supersortsOf topSort acc_sig) ||

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng Set.member topSortD (subsortsOf topSort acc_sig) ||

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng supersortsOf topSortD predefinedSign /=

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng supersortsOf topSortD acc_sig ||

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng selectDATAKernel (sortRel predefinedSign)

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng /= selectDATAKernel (sortRel acc_sig)]

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng chSort s ds = ds ++

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng [mkDiag Error

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng ("\n new sort is not a subsort of '" ++

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng showDoc topSort "':") s

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng | not $ Set.member topSort $ supersortsOf s acc_sig]

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng ++ [mkDiag Error

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng ("\n new sort must not be a supersort of '" ++

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng showDoc topSort "':") s

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng | Set.member topSort (subsortsOf s acc_sig)]

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng selectDATAKernel rel =

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng Rel.intransKernel $ Rel.restrict rel $

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng Set.insert topSortD

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng (subsortsOf topSortD predefinedSign)

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng checkPreds = Map.foldWithKey chPred [] (predMap diff_sig)

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng chPred p ts ds = ds ++

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng Set.fold (chArgs "pred" p . predArgs) [] ts

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng checkOps = Map.foldWithKey chOp [] (opMap diff_sig)

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng chOp o ts ds = ds ++

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng Set.fold (chArgs "op" o . opArgs) [] ts

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng

da14cebe459d3275048785f25bd869cb09b5307fEric Cheng chArgs kstr sym args ds = ds ++

074e084f68dd0b08686612bec695a0cfe249da6dml case args of

074e084f68dd0b08686612bec695a0cfe249da6dml [] -> if kstr == "op"

074e084f68dd0b08686612bec695a0cfe249da6dml then []

074e084f68dd0b08686612bec695a0cfe249da6dml else [mkDiag Error

074e084f68dd0b08686612bec695a0cfe249da6dml "\n propositional symbols are not allowed" sym]

(s : _) ->

if s == topSort ||

Set.member topSort (supersortsOf s acc_sig)

then []

else [mkDiag Error

("\n the first argument sort of this " ++ kstr ++

" is not a subsort of '" ++ showDoc topSort "':")

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

case predName ps of

pn ->

case Map.findWithDefault Set.empty pn (predMap sign) of

pn_typeSet

| Set.null pn_typeSet ->

Result [Diag Error ("Unknown predicate: \"" ++

show pn ++ "\"") (posOfId pn)]

Nothing

| otherwise ->

let pn_RelTypes = Set.filter (\ pt -> length (predArgs pt) == 2)

pn_typeSet

in if Set.null pn_RelTypes

then Result [Diag Error ("No binary predicate \"" ++

show pn ++ "\" declared") (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 predName ps = case ps of

Pred_name pn -> pn

Qual_pred_name pn _pType _ -> pn

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 syms = Map.foldWithKey checkSourceSymbol [] rsm

in if null syms

then return rsm

else Result (ds syms) Nothing

where checkSourceSymbol sSym _ syms =

if Set.fold (\ ps -> (||) $ matches ps sSym) False

symOfPredefinedSign

then syms ++ [sSym]

else syms

-- ds :: [RawSymbol] -> [Diagnosis]

ds syms = [Diag Error

("Predefined CASL_DL symbols\n cannot be mapped: "

++ show (ppWithCommas syms))

$ minimum $ map getRange syms]

symOfPredefinedSign :: SymbolSet

symOfPredefinedSign = symsetOf predefinedSign

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