StatAna.hs revision eaf02872307b4578250fbeb9dc371cac177b0924
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{- |
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederModule : $Header$
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederDescription : static analysis of DL parts
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Klaus Luettich, Uni Bremen 2005
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederMaintainer : luecke@informatik.uni-bremen.de
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : provisional
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : portable
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederstatic analysis of DL parts especially cardinalities, predefined datatypes
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederand additional annottations
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-}
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule CASL_DL.StatAna ( basicCASL_DLAnalysis
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , minDLForm
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , checkSymbolMapDL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , DLSign) where
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder
8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maederimport CASL_DL.AS_CASL_DL
f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maederimport CASL_DL.Print_AS ()
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maederimport CASL_DL.Sign
8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maederimport CASL_DL.PredefinedSign
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport CASL_DL.PredefinedGlobalAnnos
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maederimport CASL.Sign
d42a01c4eb6892fe23ca9eff107bb29f4a229480Christian Maederimport CASL.MixfixParser
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport CASL.Morphism
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport CASL.StaticAna
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederimport CASL.AS_Basic_CASL
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport CASL.ShowMixfix
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederimport CASL.Overload
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CASL.Quantification
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederimport qualified Data.Map as Map
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport qualified Data.Set as Set
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport qualified Common.Lib.Rel as Rel
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.AS_Annotation
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.GlobalAnnotations
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport Common.AnalyseAnnos
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport Common.DocUtils
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport Common.Id
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.Result
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederimport Common.ConvertLiteral
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport Common.ExtSign
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederinstance FreeVars DL_FORMULA where
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder freeVarsOfExt sign (Cardinality _ _ t1 t2 mf _) =
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder Set.union (freeTermVars sign t1) $ Set.union (freeTermVars sign t2)
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder $ case mf of
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder Nothing -> Set.empty
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Just f -> freeVars sign f
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian MaederbasicCASL_DLAnalysis
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder :: (BASIC_SPEC () () DL_FORMULA, Sign DL_FORMULA CASL_DLSign, GlobalAnnos)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -> Result (BASIC_SPEC () () DL_FORMULA,
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder [Named (FORMULA DL_FORMULA)])
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian MaederbasicCASL_DLAnalysis (bs,sig,ga) =
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder do ga' <- addGlobalAnnos ga caslDLGlobalAnnos
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder let sig' = addSig addCASL_DLSign sig predefinedSign
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder bs' = transformSortDeclarations True bs
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder case basicAnalysis minDLForm (const return)
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder (const return) ana_Mix (bs',sig',ga') of
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder r@(Result ds1 mr) ->
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder maybe r (cleanStatAnaResult . postAna ds1 sig') mr
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder{- |
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder True -> extend all sort declarations without a supersort
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder with supersort Thing
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder False -> remove Thing from all sort declarations with supersort Thing
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-}
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedergenerateSubsorting :: Sign f e -> Sign f e
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedergenerateSubsorting sig =
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder let
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder inS = sortSet sig
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder inR = sortRel sig
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder in
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder sig
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder {
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder sortRel = Set.fold (\x y -> Rel.insert x topSort y) inR inS
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder }
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedertransformSortDeclarations :: Bool
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder -> BASIC_SPEC () () DL_FORMULA
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder -> BASIC_SPEC () () DL_FORMULA
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian MaedertransformSortDeclarations addThing (Basic_spec aBIs) =
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder Basic_spec (processBIs aBIs)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder where processBIs = map (mapAn processBI)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder processBI bi = case bi of
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Sig_items sig_i -> Sig_items (processSig_i sig_i)
840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder _ -> bi
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder processSig_i sig_i =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder case sig_i of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Sort_items sk aSor_is r ->
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Sort_items sk (concatMap processaSor_i aSor_is) r
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder _ -> sig_i
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder processaSor_i aSor_i =
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder case processSor_i (item aSor_i) of
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder [] -> []
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder x:xs -> replaceAnnoted x aSor_i : map emptyAnno xs
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder processSor_i sor_i =
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder if addThing
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder then
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder case sor_i of
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Sort_decl sorts r ->
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder [Subsort_decl sorts topSort r]
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Subsort_decl _ supSort _
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder | supSort == topSort -> [sor_i]
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder | otherwise ->
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder [ sor_i
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder , Subsort_decl [supSort] topSort statAnaMarker]
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder _ -> [sor_i]
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder else
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder case sor_i of
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Subsort_decl sorts supSort r
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder | supSort == topSort -> if r == statAnaMarker
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder then []
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder else [Sort_decl sorts r]
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder | otherwise -> [sor_i]
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder _ -> [sor_i]
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | marker for sig items added to a basic spec
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederstatAnaMarker :: Range
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederstatAnaMarker = Range [SourcePos (">:>added for DL.StaticAna<:<") 0 0]
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder{- |
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder * remove predefined symbols from a result of the static analysis
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder * remove all explicit references of Thing from the BSIC_SPEC
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-}
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedercleanStatAnaResult
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder :: Result (BASIC_SPEC () () DL_FORMULA,
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder [Named (FORMULA DL_FORMULA)])
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder -> Result (BASIC_SPEC () () DL_FORMULA,
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder [Named (FORMULA DL_FORMULA)])
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedercleanStatAnaResult r@(Result ds1 mr) = maybe r clean mr
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder where clean (bs, ExtSign sig sys, sen) =
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Result ds1 (Just (transformSortDeclarations False bs
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder , ExtSign (generateSubsorting $ cleanSign sig) $
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Set.delete (idToSortSymbol topSort) sys
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder , sen))
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder cleanSign sig =
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder diffSig diffCASL_DLSign
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (sig {sortRel = Rel.delSet (Set.singleton topSort)
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder $ sortRel sig})
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder predefinedSign
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder{- |
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder postAna checks the Signature for
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder * all new sorts must be a proper subsort of Thing and
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder must not be related to DATA
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder * no new subsort relations with DATA
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder * all new predicates must have a subsort of Thing as subject (1st argument)
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder * all new operations must have a subsort of Thing as 1st argument
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-}
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederpostAna :: [Diagnosis]
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder -> Sign DL_FORMULA CASL_DLSign
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder -> (BASIC_SPEC () () DL_FORMULA,
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder [Named (FORMULA DL_FORMULA)])
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder -> Result (BASIC_SPEC () () DL_FORMULA,
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder [Named (FORMULA DL_FORMULA)])
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederpostAna ds1 in_sig i@(_, ExtSign acc_sig _, _) =
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Result (ds1++ds_sig) $ if null ds_sig then Just i else Nothing
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder where ds_sig = chkSorts ++ checkPreds ++ checkOps
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder diff_sig = diffSig diffCASL_DLSign acc_sig in_sig
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder chkSorts = Set.fold chSort [] (sortSet diff_sig) ++
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (if Set.member topSortD (supersortsOf topSort acc_sig) ||
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Set.member topSortD (subsortsOf topSort acc_sig) ||
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (supersortsOf topSortD predefinedSign /=
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder supersortsOf topSortD acc_sig) ||
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (selectDATAKernel (sortRel predefinedSign)
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder /=
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder selectDATAKernel (sortRel acc_sig))
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder then [Diag Error
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ("\n new subsort relations with data "++
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder "topsort are not allowed") nullRange]
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder else [])
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder chSort s ds = ds ++
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (if Set.member topSort (supersortsOf s acc_sig)
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder then []
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder else [mkDiag Error
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder ("\n new sort is not a subsort of '"++
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder showDoc topSort "':") s]) ++
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (if Set.member topSort (subsortsOf s acc_sig)
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder then [mkDiag Error
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder ("\n new sort must not be a supersort of '"++
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder showDoc topSort "':") s]
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder else [])
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder selectDATAKernel rel =
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder Rel.intransKernel $ Rel.restrict rel $
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder Set.insert topSortD
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (subsortsOf topSortD predefinedSign)
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder checkPreds = Map.foldWithKey chPred [] (predMap diff_sig)
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder chPred p ts ds = ds ++
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder Set.fold (\ t -> chArgs "pred" p $ predArgs t) [] ts
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder checkOps = Map.foldWithKey chOp [] (opMap diff_sig)
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder chOp o ts ds = ds ++
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder Set.fold (\ t -> chArgs "op" o $ opArgs t) [] ts
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder chArgs kstr sym args ds = ds ++
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder case args of
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder [] -> if kstr == "op"
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder then []
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder else [mkDiag Error
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder ("\n propositional symbols are not allowed") sym]
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (s:_) ->
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder if s == topSort ||
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder Set.member topSort (supersortsOf s acc_sig)
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder then []
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder else [mkDiag Error
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder ("\n the first argument sort of this "++kstr++
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder " is not a subsort of '"++ showDoc topSort "':")
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder sym]
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder{- sketch of Annotation analysis:
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder where callAna bsRes =
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder case analyseAnnos ga acc_sig bs of
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder Result ds2 mESig ->
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder maybe (Result (ds1++ds2) Nothing)
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (integrateExt (ds1++ds2) baRes) mESig
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder integrateExt ds (bs',dif_sig,acc_sig,sens) eSig =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Result ds (bs',
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder dif_sig {extendedInfo = dif eSig (extendedInfo sig)},
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder acc_sig {extendedInfo = eSig},
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder sens)
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder-}
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederana_Mix :: Mix () () DL_FORMULA CASL_DLSign
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maederana_Mix = emptyMix
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder { putParen = mapDL_FORMULA
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder , mixResolve = resolveDL_FORMULA
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder }
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maedertype DLSign = Sign DL_FORMULA CASL_DLSign
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermapDL_FORMULA :: DL_FORMULA -> DL_FORMULA
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermapDL_FORMULA (Cardinality ct pn varTerm natTerm qualTerm ps) =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Cardinality ct pn (mapT varTerm) (mapT natTerm) qualTerm ps
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder where mapT = mapTerm mapDL_FORMULA
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederresolveDL_FORMULA :: MixResolve DL_FORMULA
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederresolveDL_FORMULA ga ids (Cardinality ct ps varTerm natTerm qualTerm ran) =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do vt <- resMixTerm varTerm
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder nt <- resMixTerm natTerm
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder mf <- case qualTerm of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Nothing -> return Nothing
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Just f -> fmap Just $
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder resolveMixFrm mapDL_FORMULA resolveDL_FORMULA ga ids f
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder return $ Cardinality ct ps vt nt mf ran
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder where resMixTerm = resolveMixTrm mapDL_FORMULA
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder resolveDL_FORMULA ga ids
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederminDLForm :: Min DL_FORMULA CASL_DLSign
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederminDLForm sign form =
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder case form of
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder Cardinality ct ps varTerm natTerm qualTerm ran ->
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder case predName ps of
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder pn ->
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder case Map.findWithDefault Set.empty pn (predMap sign) of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder pn_typeSet
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder | Set.null pn_typeSet ->
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder Result [Diag Error ("Unknown predicate: \""++
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder show pn++"\"") (posOfId pn)]
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder Nothing
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder | otherwise ->
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder let pn_RelTypes = Set.filter (\pt -> length (predArgs pt) == 2)
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder pn_typeSet
840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder in if Set.null pn_RelTypes
840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder then Result [Diag Error ("No binary predicate \""++
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder show pn++"\" declared") (posOfId pn)]
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder Nothing
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder else do
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder v2 <- oneExpTerm minDLForm sign varTerm
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder let v_sort = sortOfTerm v2
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder n2 <- oneExpTerm minDLForm sign natTerm
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder let n_sort = sortOfTerm n2
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder ps' <- case sub_sort_of_subj pn v_sort pn_RelTypes of
840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder Result ds mts ->
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder let ds' =
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder if null ds
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder then [mkDiag Error
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder ("Variable in cardinality constraint\n"
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder ++ " has wrong type")
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder varTerm]
840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder else ds
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder amigDs ts =
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder [Diag Error
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder ("Ambiguous types found for\n pred '"++
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder showDoc pn "' in cardinalty "++
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder "constraint: (showing only two of them)\n"++
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder " '"++ 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 foldr (\ ps -> (||) $ matches ps sSym) False
$ symOf predefinedSign
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]
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