ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Propositional/Prop2CASLHelpers.hs
9eb6a481980d81a55898ba418fba72fc3c09d8c8Dominik LueckeDescription : Helper functions for Prop2CASL
ea38173e68c920e0a353cb79f699684a7a401c15Dominik LueckeCopyright : (c) Dominik Luecke and Uni Bremen 2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : luecke@informatik.uni-bremen.de
ea38173e68c920e0a353cb79f699684a7a401c15Dominik LueckeStability : experimental
ea38173e68c920e0a353cb79f699684a7a401c15Dominik LueckePortability : portable (imports Logic.Logic)
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik LueckeThe helpers for translating comorphism from Propositional to CASL.
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke-}
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckemodule Propositional.Prop2CASLHelpers
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke where
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified Data.Set as Set
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified Data.Map as Map
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified Common.AS_Annotation as AS_Anno
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified Common.Id as Id
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified Common.Result as Result
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke-- Propositional
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified Propositional.AS_BASIC_Propositional as PBasic
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified Propositional.Sublogic as PSL
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified Propositional.Sign as PSign
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified Propositional.Morphism as PMor
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified Propositional.Symbol as PSymbol
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke-- CASL
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified CASL.AS_Basic_CASL as CBasic
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified CASL.Sublogic as CSL
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified CASL.Sign as CSign
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Lueckeimport qualified CASL.Morphism as CMor
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
da955132262baab309a50fdffe228c9efe68251dCui Jian-- | Translation of the signature
986d3f255182539098a97ac86da9eeee5b7a72e3Christian MaedermapSig :: PSign.Sign -> CSign.CASLSign
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapSig sign = (CSign.emptySign ())
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder { CSign.predMap = Set.fold (`MapSet.insert` CSign.PredType [])
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder MapSet.empty $ PSign.items sign }
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke-- | Which is the target sublogic?
ea38173e68c920e0a353cb79f699684a7a401c15Dominik LueckemapSub :: PSL.PropSL -> CSL.CASL_Sublogics
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermapSub sl = CSL.bottom
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder { CSL.cons_features = CSL.NoSortGen
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , CSL.sub_features = CSL.NoSub
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , CSL.has_pred = True
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , CSL.has_eq = False
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , CSL.which_logic = if PSL.isHC sl then CSL.Horn else CSL.FOL }
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke-- | Translation of morphisms
986d3f255182539098a97ac86da9eeee5b7a72e3Christian MaedermapMor :: PMor.Morphism -> Result.Result CMor.CASLMor
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapMor mor = Result.Result [] $ Just (CMor.embedMorphism ()
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (mapSig $ PMor.source mor) $ mapSig $ PMor.target mor)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { CMor.pred_map = trMor $ PMor.propMap mor }
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke-- | Mapping of a theory
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermapTheory :: (PSign.Sign, [AS_Anno.Named PBasic.FORMULA])
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -> Result.Result (CSign.CASLSign, [AS_Anno.Named CBasic.CASLFORMULA])
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapTheory (sig, form) = Result.Result [] $
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just (mapSig sig, map trNamedForm form)
da955132262baab309a50fdffe228c9efe68251dCui Jian
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke-- | Translation of symbols
da955132262baab309a50fdffe228c9efe68251dCui JianmapSym :: PSymbol.Symbol -> Set.Set CSign.Symbol
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapSym sym = Set.singleton $
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder CSign.idToPredSymbol (PSymbol.symName sym) $ CSign.PredType []
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke-- | Translation of sentence
986d3f255182539098a97ac86da9eeee5b7a72e3Christian MaedermapSentence :: PSign.Sign -> PBasic.FORMULA -> Result.Result CBasic.CASLFORMULA
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapSentence _ form = Result.Result [] $ Just $ trForm form
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- -----------------------------------------------------------------------------
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederHelpers --
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder----------------------------------------------------------------------------- -}
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke-- | Helper for map theory
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedertrNamedForm :: AS_Anno.Named PBasic.FORMULA -> AS_Anno.Named CBasic.CASLFORMULA
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedertrNamedForm = AS_Anno.mapNamed trForm
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke-- | Helper for map sentence and map theory
986d3f255182539098a97ac86da9eeee5b7a72e3Christian MaedertrForm :: PBasic.FORMULA -> CBasic.CASLFORMULA
da955132262baab309a50fdffe228c9efe68251dCui JiantrForm form =
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke case form of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder PBasic.Negation fn rn -> CBasic.Negation (trForm fn) rn
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder PBasic.Conjunction fn rn ->
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder CBasic.Junction CBasic.Con (map trForm fn) rn
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder PBasic.Disjunction fn rn ->
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder CBasic.Junction CBasic.Dis (map trForm fn) rn
da955132262baab309a50fdffe228c9efe68251dCui Jian PBasic.Implication f1 f2 rn ->
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder CBasic.Relation (trForm f1) CBasic.Implication (trForm f2) rn
da955132262baab309a50fdffe228c9efe68251dCui Jian PBasic.Equivalence f1 f2 rn ->
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder CBasic.Relation (trForm f1) CBasic.Equivalence (trForm f2) rn
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder PBasic.True_atom rn -> CBasic.Atom True rn
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder PBasic.False_atom rn -> CBasic.Atom False rn
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder PBasic.Predication pid -> CBasic.mkPredication
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (CBasic.mkQualPred (Id.simpleIdToId pid)
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke (CBasic.Pred_type [] Id.nullRange)
da955132262baab309a50fdffe228c9efe68251dCui Jian )
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder []
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke-- | Helper for map mor
ea38173e68c920e0a353cb79f699684a7a401c15Dominik LuecketrMor :: Map.Map Id.Id Id.Id -> Map.Map (Id.Id, CSign.PredType) Id.Id
da955132262baab309a50fdffe228c9efe68251dCui JiantrMor mp =
da955132262baab309a50fdffe228c9efe68251dCui Jian let
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder pt = CSign.PredType {CSign.predArgs = []}
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke in
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder Map.foldWithKey
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke (\ k a ->
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke Map.insert (k, pt) a
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke )
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke Map.empty
ea38173e68c920e0a353cb79f699684a7a401c15Dominik Luecke mp