StatAna.hs revision eaf02872307b4578250fbeb9dc371cac177b0924
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
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederMaintainer : luecke@informatik.uni-bremen.de
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : provisional
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : portable
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederstatic analysis of DL parts especially cardinalities, predefined datatypes
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederand additional annottations
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule CASL_DL.StatAna ( basicCASL_DLAnalysis
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , checkSymbolMapDL
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , DLSign) where
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederimport qualified Data.Map as Map
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport qualified Data.Set as Set
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport qualified Common.Lib.Rel as Rel
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 Just f -> freeVars sign f
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
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
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedergenerateSubsorting :: Sign f e -> Sign f e
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedergenerateSubsorting sig =
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder inS = sortSet sig
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder inR = sortRel sig
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder sortRel = Set.fold (\x y -> Rel.insert x topSort y) inR inS
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)
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 processaSor_i aSor_i =
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder case processSor_i (item aSor_i) of
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder x:xs -> replaceAnnoted x aSor_i : map emptyAnno xs
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder processSor_i sor_i =
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 , Subsort_decl [supSort] topSort statAnaMarker]
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder case sor_i of
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Subsort_decl sorts supSort r
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder | supSort == topSort -> if r == statAnaMarker
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder else [Sort_decl sorts r]
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder | otherwise -> [sor_i]
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 * remove predefined symbols from a result of the static analysis
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder * remove all explicit references of Thing from the BSIC_SPEC
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 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 postAna checks the Signature for
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder * all new sorts must be a proper subsort of Thing and
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder must not be related to DATA
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder * no new subsort relations with DATA
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder * all new predicates must have a subsort of Thing as subject (1st argument)
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder * all new operations must have a subsort of Thing as 1st argument
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 selectDATAKernel (sortRel acc_sig))
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder then [Diag Error
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ("\n new subsort relations with data "++
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder "topsort are not allowed") nullRange]
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder chSort s ds = ds ++
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (if Set.member topSort (supersortsOf s acc_sig)
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 selectDATAKernel rel =
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (subsortsOf topSortD predefinedSign)
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 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 chArgs kstr sym args ds = ds ++
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder [] -> if kstr == "op"
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder else [mkDiag Error
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder ("\n propositional symbols are not allowed") sym]
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder if s == topSort ||
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder Set.member topSort (supersortsOf s acc_sig)
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{- sketch of Annotation analysis:
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 Maederana_Mix :: Mix () () DL_FORMULA CASL_DLSign
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maederana_Mix = emptyMix
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder { putParen = mapDL_FORMULA
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder , mixResolve = resolveDL_FORMULA
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maedertype DLSign = Sign DL_FORMULA CASL_DLSign
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
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
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederminDLForm :: Min DL_FORMULA CASL_DLSign
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederminDLForm sign form =
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder Cardinality ct ps varTerm natTerm qualTerm ran ->
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder case predName ps of
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder case Map.findWithDefault Set.empty pn (predMap sign) of
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder | Set.null pn_typeSet ->
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder Result [Diag Error ("Unknown predicate: \""++
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder show pn++"\"") (posOfId pn)]
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder | otherwise ->
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder let pn_RelTypes = Set.filter (\pt -> length (predArgs pt) == 2)
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 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 then [mkDiag Error
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder ("Variable in cardinality constraint\n"
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder ++ " has wrong type")
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) "', '"++
[] -> error "CASL_DL.StatAna: Internal error"
) (Result [] Nothing) $ Set.toList typeSet
use from Logic.Logic.Logic and from CASL:
let syms = Map.foldWithKey checkSourceSymbol [] rsm