{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2Prop.hs
Description :  Coding of a CASL sublogic to Propositional
Copyright   :  (c) Dominik Luecke and Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

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

A comorphism from CASL to Propositional. The CASL sublogic does not precisely
capture the valid domain of the translation. Sorts, ops and preds with
arguments will be ignored. The translation will fail for non-propositional
sentences.
-}

module Comorphisms.CASL2Prop (CASL2Prop (..)) where

import Common.ProofTree

import Logic.Logic
import Logic.Comorphism

-- Propositional
import qualified Propositional.Logic_Propositional as PLogic
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 CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sublogic
import CASL.Sign
import CASL.Morphism

import qualified Data.Set as Set
import qualified Data.Map as Map
import Common.AS_Annotation
import Common.Id
import Common.Result
import Common.DocUtils
import qualified Common.Lib.MapSet as MapSet
import qualified Control.Monad.Fail as Fail

-- | lid of the morphism
data CASL2Prop = CASL2Prop deriving Int -> CASL2Prop -> ShowS
[CASL2Prop] -> ShowS
CASL2Prop -> String
(Int -> CASL2Prop -> ShowS)
-> (CASL2Prop -> String)
-> ([CASL2Prop] -> ShowS)
-> Show CASL2Prop
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2Prop] -> ShowS
$cshowList :: [CASL2Prop] -> ShowS
show :: CASL2Prop -> String
$cshow :: CASL2Prop -> String
showsPrec :: Int -> CASL2Prop -> ShowS
$cshowsPrec :: Int -> CASL2Prop -> ShowS
Show

instance Language CASL2Prop where
  language_name :: CASL2Prop -> String
language_name CASL2Prop = "CASL2Propositional"

instance Comorphism CASL2Prop
    CASL
    CASL_Sublogics
    CASLBasicSpec
    CASLFORMULA
    SYMB_ITEMS
    SYMB_MAP_ITEMS
    CASLSign
    CASLMor
    Symbol
    RawSymbol
    ProofTree
    PLogic.Propositional
    PSL.PropSL
    PBasic.BASIC_SPEC
    PBasic.FORMULA
    PBasic.SYMB_ITEMS
    PBasic.SYMB_MAP_ITEMS
    PSign.Sign
    PMor.Morphism
    PSymbol.Symbol
    PSymbol.Symbol
    ProofTree
    where
      sourceLogic :: CASL2Prop -> CASL
sourceLogic CASL2Prop = CASL
CASL
      sourceSublogic :: CASL2Prop -> CASL_Sublogics
sourceSublogic CASL2Prop = CASL_Sublogics -> CASL_Sublogics -> CASL_Sublogics
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CASL_Sublogics
forall a. Lattice a => CASL_SL a
need_fol CASL_Sublogics
forall a. Lattice a => CASL_SL a
need_pred
      targetLogic :: CASL2Prop -> Propositional
targetLogic CASL2Prop = Propositional
PLogic.Propositional
      mapSublogic :: CASL2Prop -> CASL_Sublogics -> Maybe PropSL
mapSublogic CASL2Prop = PropSL -> Maybe PropSL
forall a. a -> Maybe a
Just (PropSL -> Maybe PropSL)
-> (CASL_Sublogics -> PropSL) -> CASL_Sublogics -> Maybe PropSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASL_Sublogics -> PropSL
mapSub
      map_theory :: CASL2Prop
-> (CASLSign, [Named CASLFORMULA])
-> Result (Sign, [Named FORMULA])
map_theory CASL2Prop = (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA])
mapTheory
      is_model_transportable :: CASL2Prop -> Bool
is_model_transportable CASL2Prop = Bool
True
      map_symbol :: CASL2Prop -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2Prop _ = Symbol -> Set Symbol
mapSym
      map_sentence :: CASL2Prop -> CASLSign -> CASLFORMULA -> Result FORMULA
map_sentence CASL2Prop _ = CASLFORMULA -> Result FORMULA
trForm
      map_morphism :: CASL2Prop -> CASLMor -> Result Morphism
map_morphism CASL2Prop = CASLMor -> Result Morphism
mapMor
      has_model_expansion :: CASL2Prop -> Bool
has_model_expansion CASL2Prop = Bool
False
      is_weakly_amalgamable :: CASL2Prop -> Bool
is_weakly_amalgamable CASL2Prop = Bool
True
      isInclusionComorphism :: CASL2Prop -> Bool
isInclusionComorphism CASL2Prop = Bool
False

-- | Translation of the signature
mapSig :: CASLSign -> PSign.Sign
mapSig :: CASLSign -> Sign
mapSig = Set Id -> Sign
PSign.Sign (Set Id -> Sign) -> (CASLSign -> Set Id) -> CASLSign -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id PredType -> Set Id
forall a b. MapSet a b -> Set a
MapSet.keysSet
  (MapSet Id PredType -> Set Id)
-> (CASLSign -> MapSet Id PredType) -> CASLSign -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PredType -> Bool) -> MapSet Id PredType -> MapSet Id PredType
forall a b.
(Ord a, Ord b) =>
(b -> Bool) -> MapSet a b -> MapSet a b
MapSet.filter ([Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Id] -> Bool) -> (PredType -> [Id]) -> PredType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> [Id]
predArgs) (MapSet Id PredType -> MapSet Id PredType)
-> (CASLSign -> MapSet Id PredType)
-> CASLSign
-> MapSet Id PredType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLSign -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap

-- | Which is the target sublogic?
mapSub :: CASL_Sublogics -> PSL.PropSL
mapSub :: CASL_Sublogics -> PropSL
mapSub sl :: CASL_Sublogics
sl = if CASL_Sublogics -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic CASL_Sublogics
sl CASL_Formulas -> CASL_Formulas -> Bool
forall a. Ord a => a -> a -> Bool
<= CASL_Formulas
Horn then PropSL
PSL.bottom else PropSL
PSL.top

-- | Translation of morphisms
mapMor :: CASLMor -> Result PMor.Morphism
mapMor :: CASLMor -> Result Morphism
mapMor mor :: CASLMor
mor = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism :: Sign -> Sign -> Map Id Id -> Morphism
PMor.Morphism
  { source :: Sign
PMor.source = CASLSign -> Sign
mapSig (CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
msource CASLMor
mor)
  , target :: Sign
PMor.target = CASLSign -> Sign
mapSig (CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
mtarget CASLMor
mor)
  , propMap :: Map Id Id
PMor.propMap = ((Id, PredType) -> Id -> Map Id Id -> Map Id Id)
-> Map Id Id -> Map (Id, PredType) Id -> Map Id Id
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ (i :: Id
i, pt :: PredType
pt) j :: Id
j ->
      if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (PredType -> [Id]
predArgs PredType
pt) then Id -> Id -> Map Id Id -> Map Id Id
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i Id
j else Map Id Id -> Map Id Id
forall a. a -> a
id) Map Id Id
forall k a. Map k a
Map.empty
      (Map (Id, PredType) Id -> Map Id Id)
-> Map (Id, PredType) Id -> Map Id Id
forall a b. (a -> b) -> a -> b
$ CASLMor -> Map (Id, PredType) Id
forall f e m. Morphism f e m -> Map (Id, PredType) Id
pred_map CASLMor
mor }

-- | Mapping of a theory
mapTheory :: (CASLSign, [Named CASLFORMULA])
  -> Result (PSign.Sign, [Named PBasic.FORMULA])
mapTheory :: (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA])
mapTheory (sig :: CASLSign
sig, form :: [Named CASLFORMULA]
form) = do
  [Named FORMULA]
sens <- (Named CASLFORMULA -> Result (Named FORMULA))
-> [Named CASLFORMULA] -> Result [Named FORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Named CASLFORMULA -> Result (Named FORMULA)
trNamedForm [Named CASLFORMULA]
form
  (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign -> Sign
mapSig CASLSign
sig, [Named FORMULA]
sens)

-- | Translation of symbols
mapSym :: Symbol -> Set.Set PSymbol.Symbol
mapSym :: Symbol -> Set Symbol
mapSym sym :: Symbol
sym = case Symbol -> SymbType
symbType Symbol
sym of
  PredAsItemType pt :: PredType
pt | [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Id] -> Bool) -> [Id] -> Bool
forall a b. (a -> b) -> a -> b
$ PredType -> [Id]
predArgs PredType
pt ->
    Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Id -> Symbol
PSymbol.Symbol (Id -> Symbol) -> Id -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> Id
symName Symbol
sym)
  _ -> Set Symbol
forall a. Set a
Set.empty

-- | Helper for map theory
trNamedForm :: Named CASLFORMULA -> Result (Named PBasic.FORMULA)
trNamedForm :: Named CASLFORMULA -> Result (Named FORMULA)
trNamedForm = (CASLFORMULA -> Result FORMULA)
-> Named CASLFORMULA -> Result (Named FORMULA)
forall (m :: * -> *) s t.
Monad m =>
(s -> m t) -> Named s -> m (Named t)
mapNamedM CASLFORMULA -> Result FORMULA
trForm

-- | Helper for map sentence and map theory
trForm :: CASLFORMULA -> Result PBasic.FORMULA
trForm :: CASLFORMULA -> Result FORMULA
trForm form :: CASLFORMULA
form = case CASLFORMULA
form of
  Negation fn :: CASLFORMULA
fn rn :: Range
rn -> do
    FORMULA
t <- CASLFORMULA -> Result FORMULA
trForm CASLFORMULA
fn
    FORMULA -> Result FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> Result FORMULA) -> FORMULA -> Result FORMULA
forall a b. (a -> b) -> a -> b
$ FORMULA -> Range -> FORMULA
PBasic.Negation FORMULA
t Range
rn
  Junction j :: Junctor
j fn :: [CASLFORMULA]
fn rn :: Range
rn -> do
    [FORMULA]
ts <- (CASLFORMULA -> Result FORMULA)
-> [CASLFORMULA] -> Result [FORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CASLFORMULA -> Result FORMULA
trForm [CASLFORMULA]
fn
    FORMULA -> Result FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> Result FORMULA) -> FORMULA -> Result FORMULA
forall a b. (a -> b) -> a -> b
$ (case Junctor
j of
      Con -> [FORMULA] -> Range -> FORMULA
PBasic.Conjunction
      Dis -> [FORMULA] -> Range -> FORMULA
PBasic.Disjunction) [FORMULA]
ts Range
rn
  Relation f1 :: CASLFORMULA
f1 c :: Relation
c f2 :: CASLFORMULA
f2 rn :: Range
rn -> do
    FORMULA
t1 <- CASLFORMULA -> Result FORMULA
trForm CASLFORMULA
f1
    FORMULA
t2 <- CASLFORMULA -> Result FORMULA
trForm CASLFORMULA
f2
    FORMULA -> Result FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> Result FORMULA) -> FORMULA -> Result FORMULA
forall a b. (a -> b) -> a -> b
$ (if Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
Equivalence then FORMULA -> FORMULA -> Range -> FORMULA
PBasic.Equivalence else
      FORMULA -> FORMULA -> Range -> FORMULA
PBasic.Implication) FORMULA
t1 FORMULA
t2 Range
rn
  Atom b :: Bool
b rn :: Range
rn -> FORMULA -> Result FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> Result FORMULA) -> FORMULA -> Result FORMULA
forall a b. (a -> b) -> a -> b
$ (if Bool
b then Range -> FORMULA
PBasic.True_atom else Range -> FORMULA
PBasic.False_atom) Range
rn
  Predication (Qual_pred_name pid :: Id
pid (Pred_type [] _) _) [] _ ->
    FORMULA -> Result FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> Result FORMULA)
-> (String -> FORMULA) -> String -> Result FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> FORMULA
PBasic.Predication (Token -> FORMULA) -> (String -> Token) -> String -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Token
mkSimpleId (String -> Result FORMULA) -> String -> Result FORMULA
forall a b. (a -> b) -> a -> b
$ Id -> String
forall a. Show a => a -> String
show Id
pid
  _ -> String -> Result FORMULA
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result FORMULA) -> String -> Result FORMULA
forall a b. (a -> b) -> a -> b
$ "not a propositional formula: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CASLFORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc CASLFORMULA
form ""