{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
module Comorphisms.CASL2Prop (CASL2Prop (..)) where
import Common.ProofTree
import Logic.Logic
import Logic.Comorphism
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
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
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
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
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
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 }
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)
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
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
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 ""