55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaederDescription : Coding of a CASL sublogic to Propositional
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaederCopyright : (c) Dominik Luecke and Uni Bremen 2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaederMaintainer : luecke@informatik.uni-bremen.de
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaederStability : experimental
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaederPortability : non-portable (imports Logic.Logic)
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian MaederA comorphism from CASL to Propositional. The CASL sublogic does not precisely
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maedercapture the valid domain of the translation. Sorts, ops and preds with
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maederarguments will be ignored. The translation will fail for non-propositional
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maedermodule Comorphisms.CASL2Prop (CASL2Prop (..)) where
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder-- Propositional
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maederimport qualified Propositional.Logic_Propositional as PLogic
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maederimport qualified Propositional.AS_BASIC_Propositional as PBasic
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maederimport qualified Propositional.Sublogic as PSL
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maederimport qualified Propositional.Sign as PSign
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maederimport qualified Propositional.Morphism as PMor
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maederimport qualified Propositional.Symbol as PSymbol
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maederimport qualified Data.Set as Set
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maederimport qualified Data.Map as Map
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder-- | lid of the morphism
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maederdata CASL2Prop = CASL2Prop deriving Show
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maederinstance Language CASL2Prop where
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder language_name CASL2Prop = "CASL2Propositional"
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maederinstance Comorphism CASL2Prop
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder CASL_Sublogics
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder CASLBasicSpec
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder SYMB_MAP_ITEMS
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder sourceLogic CASL2Prop = CASL
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder sourceSublogic CASL2Prop = sublogics_max need_fol need_pred
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder targetLogic CASL2Prop = PLogic.Propositional
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder mapSublogic CASL2Prop = Just . mapSub
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder map_theory CASL2Prop = mapTheory
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder is_model_transportable CASL2Prop = True
83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu map_symbol CASL2Prop _ = mapSym
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maeder map_sentence CASL2Prop _ = trForm
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder map_morphism CASL2Prop = mapMor
5b65f67382b3df7a09905b792ece64276cd6973cTill Mossakowski has_model_expansion CASL2Prop = False
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder is_weakly_amalgamable CASL2Prop = True
228f49c7667370745d5b07c12e49b06b55e2dab5Christian Maeder isInclusionComorphism CASL2Prop = False
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder-- | Translation of the signature
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaedermapSig :: CASLSign -> PSign.Sign
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder . MapSet.filter (null . predArgs) . predMap
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder-- | Which is the target sublogic?
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaedermapSub :: CASL_Sublogics -> PSL.PropSL
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaedermapSub sl = if which_logic sl <= Horn then PSL.bottom else PSL.top
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder-- | Translation of morphisms
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaedermapMor :: CASLMor -> Result PMor.Morphism
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaedermapMor mor = return PMor.Morphism
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder { PMor.source = mapSig (msource mor)
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder , PMor.target = mapSig (mtarget mor)
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder , PMor.propMap = Map.foldWithKey (\ (i, pt) j ->
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder if null (predArgs pt) then Map.insert i j else id) Map.empty
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder $ pred_map mor }
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder-- | Mapping of a theory
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaedermapTheory :: (CASLSign, [Named CASLFORMULA])
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder -> Result (PSign.Sign, [Named PBasic.FORMULA])
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian MaedermapTheory (sig, form) = do
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maeder sens <- mapM trNamedForm form
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maeder return (mapSig sig, sens)
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder-- | Translation of symbols
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaedermapSym sym = case symbType sym of
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder PredAsItemType pt | null $ predArgs pt ->
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder Set.singleton (PSymbol.Symbol $ symName sym)
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder-- | Helper for map theory
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian MaedertrNamedForm :: Named CASLFORMULA -> Result (Named PBasic.FORMULA)
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian MaedertrNamedForm = mapNamedM trForm
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder-- | Helper for map sentence and map theory
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian MaedertrForm :: CASLFORMULA -> Result PBasic.FORMULA
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian MaedertrForm form = case form of
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maeder Negation fn rn -> do
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maeder t <- trForm fn
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Junction j fn rn -> do
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maeder ts <- mapM trForm fn
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder return $ (case j of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Relation f1 c f2 rn -> do
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maeder t1 <- trForm f1
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maeder t2 <- trForm f2
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder return $ (if c == Equivalence then PBasic.Equivalence else
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Atom b rn -> return $ (if b then PBasic.True_atom else PBasic.False_atom) rn
8196ea89b605d3f0a28768a5eb28623071aeb4f6Christian Maeder Predication (Qual_pred_name pid (Pred_type [] _) _) [] _ ->
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maeder return . PBasic.Predication . mkSimpleId $ show pid
897e4b4d301fd8cedab34ffacf5092a3b47d2a05Christian Maeder _ -> fail $ "not a propositional formula: " ++ showDoc form ""