{- |
Module      :  ./Propositional/Prop2CASLHelpers.hs
Description :  Helper functions for Prop2CASL
Copyright   :  (c) Dominik Luecke and Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable (imports Logic.Logic)

The helpers for translating comorphism from Propositional to CASL.

-}

module Propositional.Prop2CASLHelpers
    where

import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Id as Id
import qualified Common.Result as Result
import qualified Common.Lib.MapSet as MapSet

-- Propositional
import qualified Propositional.AS_BASIC_Propositional as PBasic
import qualified Propositional.Sublogic as PSL
import qualified Propositional.Sign as PSign
import qualified Propositional.Morphism as PMor
import qualified Propositional.Symbol as PSymbol

-- CASL
import qualified CASL.AS_Basic_CASL as CBasic
import qualified CASL.Sublogic as CSL
import qualified CASL.Sign as CSign
import qualified CASL.Morphism as CMor

-- | Translation of the signature
mapSig :: PSign.Sign -> CSign.CASLSign
mapSig :: Sign -> CASLSign
mapSig sign :: Sign
sign = (() -> CASLSign
forall e f. e -> Sign f e
CSign.emptySign ())
              { predMap :: PredMap
CSign.predMap = (Id -> PredMap -> PredMap) -> PredMap -> Set Id -> PredMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Id -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
`MapSet.insert` [Id] -> PredType
CSign.PredType [])
                                PredMap
forall a b. MapSet a b
MapSet.empty (Set Id -> PredMap) -> Set Id -> PredMap
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
PSign.items Sign
sign }

-- | Which is the target sublogic?
mapSub :: PSL.PropSL -> CSL.CASL_Sublogics
mapSub :: PropSL -> CASL_Sublogics
mapSub sl :: PropSL
sl = CASL_Sublogics
forall a. Lattice a => CASL_SL a
CSL.bottom
  { cons_features :: SortGenerationFeatures
CSL.cons_features = SortGenerationFeatures
CSL.NoSortGen
  , sub_features :: SubsortingFeatures
CSL.sub_features = SubsortingFeatures
CSL.NoSub
  , has_pred :: Bool
CSL.has_pred = Bool
True
  , has_eq :: Bool
CSL.has_eq = Bool
False
  , which_logic :: CASL_Formulas
CSL.which_logic = if PropSL -> Bool
PSL.isHC PropSL
sl then CASL_Formulas
CSL.Horn else CASL_Formulas
CSL.FOL }

-- | Translation of morphisms
mapMor :: PMor.Morphism -> Result.Result CMor.CASLMor
mapMor :: Morphism -> Result CASLMor
mapMor mor :: Morphism
mor = [Diagnosis] -> Maybe CASLMor -> Result CASLMor
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe CASLMor -> Result CASLMor)
-> Maybe CASLMor -> Result CASLMor
forall a b. (a -> b) -> a -> b
$ CASLMor -> Maybe CASLMor
forall a. a -> Maybe a
Just (() -> CASLSign -> CASLSign -> CASLMor
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
CMor.embedMorphism ()
    (Sign -> CASLSign
mapSig (Sign -> CASLSign) -> Sign -> CASLSign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
PMor.source Morphism
mor) (CASLSign -> CASLMor) -> CASLSign -> CASLMor
forall a b. (a -> b) -> a -> b
$ Sign -> CASLSign
mapSig (Sign -> CASLSign) -> Sign -> CASLSign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
PMor.target Morphism
mor)
    { pred_map :: Pred_map
CMor.pred_map = Map Id Id -> Pred_map
trMor (Map Id Id -> Pred_map) -> Map Id Id -> Pred_map
forall a b. (a -> b) -> a -> b
$ Morphism -> Map Id Id
PMor.propMap Morphism
mor }

-- | Mapping of a theory
mapTheory :: (PSign.Sign, [AS_Anno.Named PBasic.FORMULA])
  -> Result.Result (CSign.CASLSign, [AS_Anno.Named CBasic.CASLFORMULA])
mapTheory :: (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory (sig :: Sign
sig, form :: [Named FORMULA]
form) = [Diagnosis]
-> Maybe (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe (CASLSign, [Named CASLFORMULA])
 -> Result (CASLSign, [Named CASLFORMULA]))
-> Maybe (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall a b. (a -> b) -> a -> b
$
    (CASLSign, [Named CASLFORMULA])
-> Maybe (CASLSign, [Named CASLFORMULA])
forall a. a -> Maybe a
Just (Sign -> CASLSign
mapSig Sign
sig, (Named FORMULA -> Named CASLFORMULA)
-> [Named FORMULA] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map Named FORMULA -> Named CASLFORMULA
trNamedForm [Named FORMULA]
form)

-- | Translation of symbols
mapSym :: PSymbol.Symbol -> Set.Set CSign.Symbol
mapSym :: Symbol -> Set Symbol
mapSym sym :: Symbol
sym = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol) -> Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$
    Id -> PredType -> Symbol
CSign.idToPredSymbol (Symbol -> Id
PSymbol.symName Symbol
sym) (PredType -> Symbol) -> PredType -> Symbol
forall a b. (a -> b) -> a -> b
$ [Id] -> PredType
CSign.PredType []

-- | Translation of sentence
mapSentence :: PSign.Sign -> PBasic.FORMULA -> Result.Result CBasic.CASLFORMULA
mapSentence :: Sign -> FORMULA -> Result CASLFORMULA
mapSentence _ form :: FORMULA
form = [Diagnosis] -> Maybe CASLFORMULA -> Result CASLFORMULA
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe CASLFORMULA -> Result CASLFORMULA)
-> Maybe CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> Maybe CASLFORMULA
forall a. a -> Maybe a
Just (CASLFORMULA -> Maybe CASLFORMULA)
-> CASLFORMULA -> Maybe CASLFORMULA
forall a b. (a -> b) -> a -> b
$ FORMULA -> CASLFORMULA
trForm FORMULA
form

{- -----------------------------------------------------------------------------
Helpers                                                                   --
----------------------------------------------------------------------------- -}

-- | Helper for map theory
trNamedForm :: AS_Anno.Named PBasic.FORMULA -> AS_Anno.Named CBasic.CASLFORMULA
trNamedForm :: Named FORMULA -> Named CASLFORMULA
trNamedForm = (FORMULA -> CASLFORMULA) -> Named FORMULA -> Named CASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
AS_Anno.mapNamed FORMULA -> CASLFORMULA
trForm

-- | Helper for map sentence and map theory
trForm :: PBasic.FORMULA -> CBasic.CASLFORMULA
trForm :: FORMULA -> CASLFORMULA
trForm form :: FORMULA
form =
      case FORMULA
form of
        PBasic.Negation fn :: FORMULA
fn rn :: Range
rn -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
CBasic.Negation (FORMULA -> CASLFORMULA
trForm FORMULA
fn) Range
rn
        PBasic.Conjunction fn :: [FORMULA]
fn rn :: Range
rn ->
            Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
CBasic.Junction Junctor
CBasic.Con ((FORMULA -> CASLFORMULA) -> [FORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> CASLFORMULA
trForm [FORMULA]
fn) Range
rn
        PBasic.Disjunction fn :: [FORMULA]
fn rn :: Range
rn ->
            Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
CBasic.Junction Junctor
CBasic.Dis ((FORMULA -> CASLFORMULA) -> [FORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> CASLFORMULA
trForm [FORMULA]
fn) Range
rn
        PBasic.Implication f1 :: FORMULA
f1 f2 :: FORMULA
f2 rn :: Range
rn ->
            CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
CBasic.Relation (FORMULA -> CASLFORMULA
trForm FORMULA
f1) Relation
CBasic.Implication (FORMULA -> CASLFORMULA
trForm FORMULA
f2) Range
rn
        PBasic.Equivalence f1 :: FORMULA
f1 f2 :: FORMULA
f2 rn :: Range
rn ->
            CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
CBasic.Relation (FORMULA -> CASLFORMULA
trForm FORMULA
f1) Relation
CBasic.Equivalence (FORMULA -> CASLFORMULA
trForm FORMULA
f2) Range
rn
        PBasic.True_atom rn :: Range
rn -> Bool -> Range -> CASLFORMULA
forall f. Bool -> Range -> FORMULA f
CBasic.Atom Bool
True Range
rn
        PBasic.False_atom rn :: Range
rn -> Bool -> Range -> CASLFORMULA
forall f. Bool -> Range -> FORMULA f
CBasic.Atom Bool
False Range
rn
        PBasic.Predication pid :: Token
pid -> PRED_SYMB -> [TERM ()] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
CBasic.mkPredication
                                 (Id -> PRED_TYPE -> PRED_SYMB
CBasic.mkQualPred (Token -> Id
Id.simpleIdToId Token
pid)
                                        ([Id] -> Range -> PRED_TYPE
CBasic.Pred_type [] Range
Id.nullRange)
                                 )
                                 []

-- | Helper for map mor
trMor :: Map.Map Id.Id Id.Id -> Map.Map (Id.Id, CSign.PredType) Id.Id
trMor :: Map Id Id -> Pred_map
trMor mp :: Map Id Id
mp =
    let
        pt :: PredType
pt = PredType :: [Id] -> PredType
CSign.PredType {predArgs :: [Id]
CSign.predArgs = []}
    in
      (Id -> Id -> Pred_map -> Pred_map)
-> Pred_map -> Map Id Id -> Pred_map
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
             (\ k :: Id
k a :: Id
a ->
              (Id, PredType) -> Id -> Pred_map -> Pred_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id
k, PredType
pt) Id
a
             )
      Pred_map
forall k a. Map k a
Map.empty
      Map Id Id
mp