Sublogic.hs revision 1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederDescription : Sublogics for ExtModal logic
5ba323da9f037264b4a356085e844889aedeac23Christian MaederCopyright : (c) DFKI 2012
c58a94c44b76b072ace930f2126c889c0b64cb2aChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederMaintainer : Christian.Maeder@dfki.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : portable
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederSublogics for ExtModal Logic
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport qualified Data.Set as Set
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maederdata Frequency = None | One | Many deriving (Show, Eq, Ord, Enum)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederdata Sublogic = Sublogic
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder { hasModalities :: Frequency
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , hasTermMods :: Bool
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , hasTransClos :: Bool
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , hasNominals :: Bool
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder , hasTimeMods :: Frequency
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , hasFixPoints :: Bool
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder , hasFrameAxioms :: Bool
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder } deriving (Show, Eq, Ord)
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaedermaxSublogic :: Sublogic
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaedermaxSublogic = Sublogic
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder { hasModalities = Many
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , hasTermMods = True
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , hasTransClos = True
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder , hasNominals = True
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , hasTimeMods = Many
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , hasFixPoints = True
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , hasFrameAxioms = True
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian MaederbotSublogic :: Sublogic
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederbotSublogic = Sublogic
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder { hasModalities = None
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , hasTermMods = False
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , hasTransClos = False
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder , hasNominals = False
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , hasTimeMods = None
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , hasFixPoints = False
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , hasFrameAxioms = False
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder-- | the sublogic that can be translated to FOL
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maederfoleml :: Sublogic
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maederfoleml = maxSublogic
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder { hasTimeMods = None
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder , hasFixPoints = False
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , hasTransClos = False
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder , hasFrameAxioms = False
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederjoinSublogic :: Sublogic -> Sublogic -> Sublogic
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederjoinSublogic a b =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder let onMax f = on max f a b
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder termM = onMax hasTermMods
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder timeM = onMax hasTimeMods
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder { hasModalities = minMod termM timeM
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder `max` onMax hasModalities
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , hasTermMods = termM
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder , hasTransClos = onMax hasTransClos
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , hasNominals = onMax hasNominals
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , hasTimeMods = timeM
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , hasFixPoints = onMax hasFixPoints
5ba323da9f037264b4a356085e844889aedeac23Christian Maeder , hasFrameAxioms = onMax hasFrameAxioms
16e124196c6b204769042028c74f533509c9b5d3Christian Maederinstance Lattice Sublogic where
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder cjoin = joinSublogic
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder ctop = maxSublogic
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder bot = botSublogic
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederjoinSublogics :: [Sublogic] -> Sublogic
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederjoinSublogics = foldr joinSublogic botSublogic
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maedertype ExtModalSL = CASL_SL Sublogic
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederminSublogicOfForm :: FORMULA EM_FORMULA -> ExtModalSL
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederminSublogicOfForm = sl_sentence minSublogicOfEM
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederminSublogicOfTerm :: TERM EM_FORMULA -> ExtModalSL
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederminSublogicOfTerm = sl_term minSublogicOfEM
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian MaederminSublogicOfMod :: MODALITY -> ExtModalSL
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian MaederminSublogicOfMod m = case m of
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder SimpleMod _ -> bottom
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder TermMod t -> minSublogicOfTerm t
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder ModOp _ m1 m2 -> on sublogics_max minSublogicOfMod m1 m2
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder TransClos c -> updExtFeature (\ s -> s {hasTransClos = True})
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder (minSublogicOfMod c)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder Guard f -> minSublogicOfForm f
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederminSublogicOfPrefix :: FormPrefix -> ExtModalSL
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederminSublogicOfPrefix fp = case fp of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder BoxOrDiamond _ m _ _ -> minSublogicOfMod m
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Hybrid _ _ -> mkBot botSublogic {hasNominals = True}
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder FixedPoint _ _ -> mkBot botSublogic {hasFixPoints = True}
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder _ -> updExtFeature (setTimeMods True [()]) bottom
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian MaederminSublogicOfEM :: EM_FORMULA -> ExtModalSL
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian MaederminSublogicOfEM ef = case ef of
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder PrefixForm pf f _ -> sublogics_max (minSublogicOfPrefix pf)
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder (minSublogicOfForm f)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder UntilSince _ f1 f2 _ -> updExtFeature (setTimeMods True [()])
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder $ on sublogics_max minSublogicOfForm f1 f2
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ModForm md -> minSublogicOfModDefn md
1a38107941725211e7c3f051f7a8f5e12199f03acmaederminSublogicOfModDefn :: ModDefn -> ExtModalSL
7c57322afb6342e5cc8b1fdc96050b707407fc61Christian MaederminSublogicOfModDefn (ModDefn time term il fl _) =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder updExtFeature (\ s -> s {hasFrameAxioms = not $ null fl})
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder . updExtFeature (setModalities il)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder . updExtFeature (setTermMods term)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder . updExtFeature (setTimeMods time il)
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder . comp_list . map (minSublogicOfForm . item)
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder $ concatMap (frameForms . item) fl
628310b42327ad76ce471caf0dde6563d6fa6307Christian MaederminSublogicEMSign :: EModalSign -> ExtModalSL
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederminSublogicEMSign s = mkBot botSublogic
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder { hasTermMods = not . Set.null $ termMods s
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , hasTimeMods = case Set.size $ timeMods s of
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , hasNominals = not . Set.null $ nominals s
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , hasModalities = case Set.size $ modalities s of
628310b42327ad76ce471caf0dde6563d6fa6307Christian MaederminSublogicEMBasic :: EM_BASIC_ITEM -> ExtModalSL
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederminSublogicEMBasic bi = case bi of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ModItem md -> minSublogicOfModDefn md
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Nominal_decl l _ -> mkBot botSublogic { hasNominals = not $ null l }
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederminSLExtSigItem :: EM_SIG_ITEM -> [ExtModalSL]
1a38107941725211e7c3f051f7a8f5e12199f03acmaederminSLExtSigItem si = case si of
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder Rigid_op_items _ os _ -> map (sl_op_item minSublogicOfEM . item) os
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Rigid_pred_items _ ps _ -> map (sl_pred_item minSublogicOfEM . item) ps
ad187062b0009820118c1b773a232e29b879a2faChristian MaedersetModalities :: [a] -> Sublogic -> Sublogic
ad187062b0009820118c1b773a232e29b879a2faChristian MaedersetModalities il s = case il of
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder [_] -> s {hasModalities = max One (hasModalities s)}
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder _ -> s {hasModalities = Many}
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedersetTermMods :: Bool -> Sublogic -> Sublogic
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedersetTermMods b s = if b then s {hasTermMods = True} else s
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedersetTimeMods :: Bool -> [a] -> Sublogic -> Sublogic
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedersetTimeMods b il s = if b then case il of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder [_] -> s {hasTimeMods = max One (hasTimeMods s)}
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder _ -> s {hasTimeMods = Many}
c9892acbf03a509d874ac6d79b9a2cb09042e0dcChristian MaederminMod :: Bool -> Frequency -> Frequency
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederminMod h_term h_time = if h_term && h_time == None then One
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedersublogicsDim :: [[Sublogic]]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedersublogicsDim = let
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder f = [One, Many]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder in [ [ b { hasModalities = h } | h <- f]
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder , [ b { hasTermMods = t }]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , [ b { hasTransClos = t }]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , [ b { hasNominals = t }]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , [ b { hasModalities = h } | h <- f]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , [ b { hasFixPoints = t }]
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , [ b { hasFrameAxioms = t }] ]
ad187062b0009820118c1b773a232e29b879a2faChristian MaedersublogName :: Sublogic -> String
16e124196c6b204769042028c74f533509c9b5d3Christian MaedersublogName s = (if hasModalities s == Many then "Many" else "One")
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder ++ (if hasTermMods s then "Dyn" else "")
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder ++ (if hasNominals s then "Hybr" else "")
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder ++ (if hasTimeMods s == Many then "Time"
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder else if hasTimeMods s == One then "SingleTime" else "")
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder ++ (if hasFixPoints s then "Fix" else "")
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder ++ (if hasFrameAxioms s then "Frames" else "")
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ++ if hasTransClos s then "*" else ""
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederparseSublog :: String -> (Sublogic, String)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederparseSublog s0 = let
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (m, s1) = case stripPrefix "Many" s0 of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Nothing -> case stripPrefix "One" s0 of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Nothing -> (None, s0)
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder Just r -> (One, r)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Just r -> (Many, r)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (tm, s2) = parseBool "Dyn" s1
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder (n, s3) = parseBool "Hybr" s2
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (ti, s4) = case stripPrefix "Time" s3 of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Just r -> (Many, r)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Nothing -> case stripPrefix "SingleTime" s3 of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Nothing -> (None, s3)
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder Just r -> (One, r)
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maeder (fi, s5) = parseBool "Fix" s4
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maeder (fr, s6) = parseBool "Frames" s5
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maeder (tr, s7) = parseBool "*" s6
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maeder { hasModalities = max m $ minMod tm ti
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , hasTermMods = tm
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , hasTransClos = tr
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , hasNominals = n
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , hasTimeMods = ti
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , hasFixPoints = fi
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , hasFrameAxioms = fr