{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

{- |

Module : $Header$

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

-- | lid of the morphism

data CASL2Prop = CASL2Prop deriving Show

instance Language CASL2Prop where

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

sourceSublogic CASL2Prop = sublogics_max need_fol need_pred

targetLogic CASL2Prop = PLogic.Propositional

mapSublogic CASL2Prop = Just . mapSub

map_theory CASL2Prop = mapTheory

is_model_transportable CASL2Prop = True

map_symbol CASL2Prop _ = mapSym

map_sentence CASL2Prop _ = trForm

map_morphism CASL2Prop = mapMor

has_model_expansion CASL2Prop = True

is_weakly_amalgamable CASL2Prop = True

isInclusionComorphism CASL2Prop = False

-- | Translation of the signature

mapSig :: CASLSign -> PSign.Sign

mapSig = PSign.Sign . Map.keysSet . Map.filter (not . Set.null)

. Map.map (Set.filter (null . predArgs)) . predMap

-- | Which is the target sublogic?

mapSub :: CASL_Sublogics -> PSL.PropSL

mapSub sl = if which_logic sl <= Horn then PSL.bottom else PSL.top

-- | Translation of morphisms

mapMor :: CASLMor -> Result PMor.Morphism

mapMor mor = return PMor.Morphism

{ PMor.source = mapSig (msource mor)

, PMor.target = mapSig (mtarget mor)

, PMor.propMap = Map.foldWithKey (\ (i, pt) j ->

if null (predArgs pt) then Map.insert i j else id) Map.empty

$ pred_map mor }

-- | Mapping of a theory

mapTheory :: (CASLSign, [Named CASLFORMULA])

-> Result (PSign.Sign, [Named PBasic.FORMULA])

mapTheory (sig, form) = do

sens <- mapM trNamedForm form

return (mapSig sig, sens)

-- | Translation of symbols

mapSym :: Symbol -> Set.Set PSymbol.Symbol

mapSym sym = case symbType sym of

PredAsItemType pt | null $ predArgs pt ->

Set.singleton (PSymbol.Symbol $ symName sym)

_ -> Set.empty

-- | Helper for map theory

trNamedForm :: Named CASLFORMULA -> Result (Named PBasic.FORMULA)

trNamedForm = mapNamedM trForm

-- | Helper for map sentence and map theory

trForm :: CASLFORMULA -> Result PBasic.FORMULA

trForm form = case form of

Negation fn rn -> do

t <- trForm fn

return $ PBasic.Negation t rn

Conjunction fn rn -> do

ts <- mapM trForm fn

return $ PBasic.Conjunction ts rn

Disjunction fn rn -> do

ts <- mapM trForm fn

return $ PBasic.Disjunction ts rn

Implication f1 f2 b rn -> do

t1 <- trForm f1

t2 <- trForm f2

return $ if b then PBasic.Implication t1 t2 rn else

PBasic.Implication t2 t1 rn

Equivalence f1 f2 rn -> do

t1 <- trForm f1

t2 <- trForm f2

return $ PBasic.Equivalence t1 t2 rn

True_atom rn -> return $ PBasic.True_atom rn

False_atom rn -> return $ PBasic.False_atom rn

Predication (Qual_pred_name pid (Pred_type [] _) _) [] _ ->

return . PBasic.Predication . mkSimpleId $ show pid

_ -> fail $ "not a propositional formula: " ++ showDoc form ""