49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering{- |

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart PoetteringModule : $Header$

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart PoetteringCopyright : (c) Klaus Luettich, Uni Bremen 2004, DFKI GmbH 2011

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart PoetteringLicense : GPLv2 or higher, see LICENSE.txt

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart PoetteringMaintainer : Christian.Maeder@dfki.de

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart PoetteringStability : provisional

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart PoetteringPortability : non-portable (imports Logic.Logic)

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart PoetteringThe possible world encoding comorphism from ModalCASL to CASL.

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering We use the Relational Translation by adding one extra parameter of

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering type world to each predicate.

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering-}

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poetteringmodule Comorphisms.Modal2CASL (Modal2CASL (..)) where

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poetteringimport Logic.Logic

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poetteringimport Logic.Comorphism

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poetteringimport Common.AS_Annotation

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poetteringimport Common.Id

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poetteringimport Common.ProofTree

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poetteringimport qualified Common.Lib.MapSet as MapSet

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poetteringimport qualified Common.Lib.Rel as Rel

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poettering-- CASL

49cf4170d0b586551527ebf4297f8a3fe6bd71a3Lennart Poetteringimport CASL.Logic_CASL

import CASL.Sublogic as SL

import CASL.Sign

import CASL.AS_Basic_CASL

import CASL.Morphism

import CASL.Utils

import CASL.World

-- ModalCASL

import Modal.Logic_Modal

import Modal.AS_Modal

import Modal.ModalSign

import Modal.Utils

-- generated function

import Modal.ModalSystems

import qualified Data.Set as Set

import qualified Data.Map as Map

import Data.Maybe

import Control.Exception (assert)

-- | The identity of the comorphism

data Modal2CASL = Modal2CASL deriving (Show)

instance Language Modal2CASL -- default definition is okay

instance Comorphism Modal2CASL

Modal ()

M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

MSign

ModalMor

Symbol RawSymbol ()

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree where

sourceLogic Modal2CASL = Modal

sourceSublogic Modal2CASL = ()

targetLogic Modal2CASL = CASL

mapSublogic Modal2CASL _ = Just SL.caslTop

map_theory (Modal2CASL) (sig, sens) = case transSig sig of

mme -> return (caslSign mme, relFormulas mme

++ map (mapNamed $ transSen sig) sens)

map_morphism Modal2CASL = return . mapMor

map_sentence Modal2CASL sig = return . transSen sig

map_symbol Modal2CASL _ = Set.singleton . mapSym

has_model_expansion Modal2CASL = True

is_weakly_amalgamable Modal2CASL = True

data ModName = SimpleM SIMPLE_ID

| SortM SORT

deriving (Show, Ord, Eq)

-- | relations on possible worlds

type ModalityRelMap = Map.Map ModName PRED_NAME

data ModMapEnv = MME

{ caslSign :: CASLSign

, worldSort :: SORT

, modalityRelMap :: ModalityRelMap

, flexiOps :: OpMap

, flexiPreds :: PredMap

, relFormulas :: [Named CASLFORMULA] }

transSig :: MSign -> ModMapEnv

transSig sign =

let extInf = extendedInfo sign

flexibleOps = flexOps extInf

flexiblePreds = flexPreds extInf

fws = world

flexOps' = addWorldOp fws addPlace flexibleOps

flexPreds' = MapSet.fromMap . addWorldRels True relsTermMod

. addWorldRels False relsMod . MapSet.toMap

$ addWorldPred fws addPlace flexiblePreds

rigOps' = diffOpMapSet (opMap sign) flexibleOps

rigPreds' = diffMapSet (predMap sign) flexiblePreds

relations = Map.union relsMod relsTermMod

genRels f = Map.foldWithKey (\ me _ nm -> f me nm) Map.empty

genModFrms f = Map.foldWithKey f []

relSymbS me = Id [genToken "R"] [mkId [me]] $ tokPos me

relSymbT me = Id [genToken "R_t"] [me] $ rangeOfId me

modiesInf = modies extInf

trmMods = termModies extInf

relsMod = genRels (\ me nm -> Map.insert (SimpleM me) (relSymbS me) nm)

modiesInf

relsTermMod = genRels (\ me nm ->

Map.insert (SortM me) (relSymbT me) nm)

trmMods

relModFrms = genModFrms (\ me frms trFrms -> trFrms ++

transSchemaMFormulas partMME

fws (relSymbS me) frms)

modiesInf

relTermModFrms = genModFrms (\ me frms trFrms -> trFrms ++

transSchemaMFormulas partMME

fws (relSymbT me) frms)

trmMods

addWorldRels isTermMod rels mp =

let argSorts rs = if isTermMod

then [getModTermSort rs, fws, fws]

else [fws, fws] in

Map.fold (\ rs nm -> Map.insert rs

(Set.singleton $

PredType $ argSorts rs)

nm)

mp rels

partMME = MME {caslSign =

(emptySign ())

{ sortRel = Rel.insertKey fws $ sortRel sign

, opMap = addOpMapSet flexOps' rigOps'

, assocOps = diffOpMapSet (assocOps sign) flexibleOps

, predMap = addMapSet flexPreds' rigPreds'},

worldSort = fws,

modalityRelMap = relations,

flexiOps = flexibleOps,

flexiPreds = flexiblePreds,

relFormulas = []}

in partMME { relFormulas = relModFrms ++ relTermModFrms}

mapMor :: ModalMor -> CASLMor

mapMor m = (embedMorphism ()

(caslSign $ transSig $ msource m)

$ caslSign $ transSig $ mtarget m)

{ sort_map = sort_map m

, op_map = op_map m

, pred_map = pred_map m }

mapSym :: Symbol -> Symbol

mapSym = id -- needs to be changed once modal symbols are added

transSchemaMFormulas :: ModMapEnv -> SORT -> PRED_NAME

-> [AnModFORM] -> [Named CASLFORMULA]

transSchemaMFormulas mapEnv fws relSymb =

mapMaybe (transSchemaMFormula (mapTERM mapEnv) fws relSymb worldVars)

transSen :: MSign -> ModalFORMULA -> CASLFORMULA

transSen msig = mapSenTop (transSig msig)

mapSenTop :: ModMapEnv -> ModalFORMULA -> CASLFORMULA

mapSenTop mapEnv@(MME {worldSort = fws}) f =

case f of

Quantification q@Universal vs frm ps ->

Quantification q (qwv : vs) (mapSen mapEnv wvs frm) ps

f1 -> Quantification Universal [qwv] (mapSen mapEnv wvs f1) nullRange

where qwv = Var_decl wvs fws nullRange

wvs = [head worldVars]

-- head [VAR] is always the current world variable (for predication)

mapSen :: ModMapEnv -> [VAR] -> ModalFORMULA -> CASLFORMULA

mapSen mapEnv@(MME {worldSort = fws, flexiPreds = fPreds}) vars

f = case f of

Quantification q vs frm ps ->

Quantification q vs (mapSen mapEnv vars frm) ps

Junction j fs ps ->

Junction j (map (mapSen mapEnv vars) fs) ps

Relation f1 c f2 ps ->

Relation (mapSen mapEnv vars f1) c (mapSen mapEnv vars f2) ps

Negation frm ps -> Negation (mapSen mapEnv vars frm) ps

Atom b ps -> Atom b ps

Equation t1 e t2 ps -> Equation

(mapTERM mapEnv vars t1) e (mapTERM mapEnv vars t2) ps

Predication pn as qs ->

let as' = map (mapTERM mapEnv vars) as

fwsTerm = sortedWorldTerm fws (head vars)

(pn', as'') =

case pn of

Pred_name _ -> error "Modal2CASL: untyped predication"

Qual_pred_name prn pType@(Pred_type sorts pps) ps ->

let addTup = (Qual_pred_name (addPlace prn)

(Pred_type (fws : sorts) pps) ps,

fwsTerm : as')

defTup = (pn, as') in

if Set.member (toPredType pType)

$ MapSet.lookup prn fPreds

then addTup

else defTup

in Predication pn' as'' qs

Definedness t ps -> Definedness (mapTERM mapEnv vars t) ps

Membership t ty ps -> Membership (mapTERM mapEnv vars t) ty ps

Sort_gen_ax constrs isFree -> Sort_gen_ax constrs isFree

ExtFORMULA mf -> mapMSen mapEnv vars mf

_ -> error "Modal2CASL.transSen->mapSen"

mapMSen :: ModMapEnv -> [VAR] -> M_FORMULA -> CASLFORMULA

mapMSen mapEnv@(MME {worldSort = fws, modalityRelMap = pwRelMap}) vars f

= let trans_f1 = mkId [mkSimpleId "Placeholder for Formula"]

t_var = mkSimpleId "Placeholder for Modality Term"

(w1, w2, newVars) = assert (not (null vars))

(let hd = freshWorldVar vars

in (head vars, hd, hd : vars))

getRel mo =

Map.findWithDefault

(error ("Modal2CASL: Undefined modality " ++ show mo))

(modalityToModName mo)

trans' mTerm propSymb trForm nvs f1 =

replacePropPredication mTerm

propSymb (mapSen mapEnv nvs f1) trForm

mapT = mapTERM mapEnv newVars

vw1 = mkVarDecl w1 fws

vw2 = mkVarDecl w2 fws

mkPredType ts = Pred_type ts nullRange

joinPreds b t1 t2 = if b then mkImpl t1 t2 else conjunct [t1, t2]

quantForm b vs = if b then mkForall vs else

mkForall (init vs) . mkExist [last vs]

transPred = mkPredication (mkQualPred trans_f1 $ mkPredType []) []

in

case f of

BoxOrDiamond b moda f1 _ ->

let rel = getRel moda pwRelMap in

case moda of

Simple_mod _ -> let

newFormula = quantForm b [vw1, vw2]

$ joinPreds b

(mkPredication

(mkQualPred rel $ mkPredType [fws, fws])

[toQualVar vw1, toQualVar vw2])

transPred

in trans' Nothing trans_f1 newFormula newVars f1

Term_mod t ->

let tt = getModTermSort rel

vtt = mkVarDecl t_var tt

newFormula = quantForm b [vtt, vw1, vw2]

$ joinPreds b

(mkPredication

(mkQualPred rel $ mkPredType [tt, fws, fws])

[toQualVar vtt, toQualVar vw1, toQualVar vw2])

transPred

in trans' (Just (rel, t_var, mapT t))

trans_f1 newFormula

newVars f1

-- head [VAR] is always the current world variable (for Application)

mapTERM :: ModMapEnv -> [VAR] -> TERM M_FORMULA -> TERM ()

mapTERM mapEnv@(MME {worldSort = fws, flexiOps = fOps}) vars t = case t of

Qual_var v ty ps -> Qual_var v ty ps

Application opsym as qs ->

let as' = map (mapTERM mapEnv vars) as

fwsTerm = sortedWorldTerm fws (head vars)

addFws (Op_type k sorts res pps) =

Op_type k (fws : sorts) res pps

(opsym', as'') =

case opsym of

Op_name _ -> error "Modal2CASL: untyped prdication"

Qual_op_name on opType ps ->

let addTup = (Qual_op_name (addPlace on)

(addFws opType) ps,

fwsTerm : as')

defTup = (opsym, as') in

if Set.member (toOpType opType)

$ MapSet.lookup on fOps

then addTup

else defTup

in Application opsym' as'' qs

Sorted_term trm ty ps -> Sorted_term (mapTERM mapEnv vars trm) ty ps

Cast trm ty ps -> Cast (mapTERM mapEnv vars trm) ty ps

Conditional t1 f t2 ps ->

Conditional (mapTERM mapEnv vars t1)

(mapSen mapEnv vars f)

(mapTERM mapEnv vars t2) ps

_ -> error "Modal2CASL.mapTERM"

modalityToModName :: MODALITY -> ModName

modalityToModName (Simple_mod sid) = SimpleM sid

modalityToModName (Term_mod t) =

case optTermSort t of

Just srt -> SortM srt

Nothing -> error ("Modal2CASL: modalityToModName: Wrong term: " ++ show t)

sortedWorldTerm :: SORT -> VAR -> TERM ()

sortedWorldTerm fws v = Sorted_term (Qual_var v fws nullRange) fws nullRange

-- List of variables for worlds

worldVars :: [SIMPLE_ID]

worldVars = map (genNumVar "w") [1 ..]

freshWorldVar :: [SIMPLE_ID] -> SIMPLE_ID

freshWorldVar vs = head $ filter notKnown worldVars

where notKnown v = notElem v vs