957N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

957N/A{- |

957N/AModule : $Header$

957N/ADescription : Coding of a CASL sublogic to Propositional

957N/ACopyright : (c) Dominik Luecke and Uni Bremen 2007

957N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

957N/A

957N/AMaintainer : luecke@informatik.uni-bremen.de

957N/AStability : experimental

957N/APortability : non-portable (imports Logic.Logic)

957N/A

957N/AA comorphism from CASL to Propositional. The CASL sublogic does not precisely

957N/Acapture the valid domain of the translation. Sorts, ops and preds with

957N/Aarguments will be ignored. The translation will fail for non-propositional

957N/Asentences.

957N/A-}

957N/A

957N/Amodule Comorphisms.CASL2Prop (CASL2Prop (..)) where

957N/A

957N/Aimport Common.ProofTree

957N/A

957N/Aimport Logic.Logic

957N/Aimport Logic.Comorphism

957N/A

957N/A-- Propositional

957N/Aimport qualified Propositional.Logic_Propositional as PLogic

957N/Aimport qualified Propositional.AS_BASIC_Propositional as PBasic

957N/Aimport qualified Propositional.Sublogic as PSL

957N/Aimport qualified Propositional.Sign as PSign

957N/Aimport qualified Propositional.Morphism as PMor

957N/Aimport qualified Propositional.Symbol as PSymbol

957N/A

957N/A-- CASL

957N/Aimport CASL.Logic_CASL

957N/Aimport CASL.AS_Basic_CASL

957N/Aimport CASL.Sublogic

957N/Aimport CASL.Sign

957N/Aimport CASL.Morphism

957N/A

957N/Aimport qualified Data.Set as Set

957N/Aimport qualified Data.Map as Map

957N/Aimport Common.AS_Annotation

957N/Aimport 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 ""