e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina{- |

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel BřezinaModule : $Header$

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel BřezinaCopyright : (c) Klaus L�ttich and Uni Bremen 2004

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel BřezinaLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel BřezinaMaintainer : luecke@informatik.uni-bremen.de

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel BřezinaStability : provisional

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel BřezinaPortability : non-portable (imports Logic.Logic)

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel BřezinaThe possible world encoding comorphism from ModalCASL to CASL.

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina We use the Relational Translation by adding one extra parameter of

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina type world to each predicate.

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina-}

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinamodule Comorphisms.Modal2CASL (Modal2CASL(..)) where

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport Logic.Logic

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport Logic.Comorphism

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport qualified Data.Set as Set

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport qualified Data.Map as Map

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport Common.AS_Annotation

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport Common.Id

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina-- CASL

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport CASL.Logic_CASL

68f73e56a9b6133f8a9f4b3c0e696df6c30fec91Pavel Březinaimport CASL.Sublogic as SL

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport CASL.Sign

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport CASL.AS_Basic_CASL

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport CASL.Morphism

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport CASL.Utils

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina-- ModalCASL

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport Modal.Logic_Modal

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport Modal.AS_Modal

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport Modal.ModalSign

488b455f6b7881ec108a127840b1c1f1523d937fMichal Židekimport Modal.Utils

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina-- generated function

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport Modal.ModalSystems

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport Data.Maybe

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina-- Debugging

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinaimport Control.Exception (assert)

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina-- | The identity of the comorphism

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinadata Modal2CASL = Modal2CASL deriving (Show)

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinainstance Language Modal2CASL -- default definition is okay

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinainstance Comorphism Modal2CASL

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina Modal ()

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina MSign

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina ModalMor

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina Symbol RawSymbol ()

68f73e56a9b6133f8a9f4b3c0e696df6c30fec91Pavel Březina CASL CASL_Sublogics

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina CASLSign

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina CASLMor

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina Symbol RawSymbol () where

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina sourceLogic Modal2CASL = Modal

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina sourceSublogic Modal2CASL = ()

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina targetLogic Modal2CASL = CASL

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina mapSublogic Modal2CASL _ = Just SL.top

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina map_theory (Modal2CASL) (sig, sens) = case transSig sig of

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina mme -> return (caslSign mme, relFormulas mme

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina ++ map (mapNamed $ transSen sig) sens)

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina map_morphism Modal2CASL = return . mapMor

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina map_sentence Modal2CASL sig = return . transSen sig

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina map_symbol Modal2CASL = Set.singleton . mapSym

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina has_model_expansion Modal2CASL = True

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina is_weakly_amalgamable Modal2CASL = True

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinadata ModName = SimpleM SIMPLE_ID

488b455f6b7881ec108a127840b1c1f1523d937fMichal Židek | SortM SORT

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina deriving (Show,Ord,Eq)

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinatype ModalityRelMap = Map.Map ModName PRED_NAME

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březinadata ModMapEnv = MME { caslSign :: CASLSign,

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina worldSort :: SORT,

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina modalityRelMap :: ModalityRelMap,

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina flexOps :: Map.Map OP_NAME (Set.Set OpType),

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina-- rigOps :: Map.Map OP_NAME (Set.Set OpType),

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina flexPreds :: Map.Map PRED_NAME (Set.Set PredType),

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina-- rigPreds :: Map.Map PRED_NAME (Set.Set PredType),

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina relFormulas :: [Named CASLFORMULA]

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina }

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina-- (CASL signature,World sort introduced,[introduced relations on possible worlds],)

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel BřezinatransSig :: MSign -> ModMapEnv

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel BřezinatransSig sign =

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina {- trace ("Flexible Ops: " ++ show flexibleOps ++

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina "\nRigid Ops: " ++ show rigOps' ++

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina "\nOriginal Ops: " ++ show (opMap sign) ++ "\n" ++

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina "Flexible Preds: " ++ show flexiblePreds ++

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina "\nRigid Preds: " ++ show rigPreds' ++

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina "\nOriginal Preds: " ++ show (predMap sign) ++ "\n"

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina ) -}

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina let sorSet = sortSet sign

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina fws = freshWorldSort sorSet

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina flexOps' = Map.foldWithKey (addWorld_OP fws)

e157b9f6cb370e1b94bcac2044d26ad66d640fbaPavel Březina Map.empty $ flexibleOps

flexPreds' = addWorldRels True relsTermMod $

addWorldRels False relsMod $

Map.foldWithKey (addWorld_PRED fws)

Map.empty $ flexiblePreds

rigOps' = rigidOps $ extendedInfo sign

rigPreds' = rigidPreds $ extendedInfo sign

flexibleOps = diffMapSet (opMap sign) rigOps'

flexiblePreds = diffMapSet (predMap sign) rigPreds'

relations = Map.union relsMod relsTermMod

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

genModFrms f mp = Map.foldWithKey f [] mp

relSymbS me = Id [mkSimpleId "g_R"] [mkId [me]] nullRange

relSymbT me = Id [mkSimpleId "g_R_t"] [me] nullRange

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

(modies $ extendedInfo sign)

relsTermMod = genRels (\ me nm ->

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

(termModies $ extendedInfo sign)

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

transSchemaMFormulas partMME

fws (relSymbS me) frms)

(modies $ extendedInfo sign)

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

transSchemaMFormulas partMME

fws (relSymbT me) frms)

(termModies $ extendedInfo sign)

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 ())

{sortSet = Set.insert fws sorSet

, sortRel = sortRel sign

, opMap = Map.unionWith Set.union flexOps' rigOps'

, assocOps = diffMapSet (assocOps sign) flexibleOps

, predMap = Map.unionWith Set.union flexPreds' rigPreds'},

worldSort = fws,

modalityRelMap = relations,

flexOps = flexibleOps,

-- rigOps = rigOps',

flexPreds = flexiblePreds,

-- rigPreds = rigPreds',

relFormulas = []}

in partMME { relFormulas = relModFrms++relTermModFrms}

{- ModalSign { rigidOps :: Map.Map Id (Set.Set OpType)

, rigidPreds :: Map.Map Id (Set.Set PredType)

, modies :: Set.Set SIMPLE_ID

, termModies :: Set.Set Id --SORT

}

-}

mapMor :: ModalMor -> CASLMor

mapMor m = Morphism {msource = caslSign $ transSig $ msource m

, mtarget = caslSign $ transSig $ mtarget m

, sort_map = sort_map m

, fun_map = fun_map m

, pred_map = pred_map m

, extended_map = ()}

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,flexPreds=fPreds}) vars

f = case f of

Quantification q vs frm ps ->

Quantification q vs (mapSen mapEnv vars frm) ps

Conjunction fs ps ->

Conjunction (map (mapSen mapEnv vars) fs) ps

Disjunction fs ps ->

Disjunction (map (mapSen mapEnv vars) fs) ps

Implication f1 f2 b ps ->

Implication (mapSen mapEnv vars f1) (mapSen mapEnv vars f2) b ps

Equivalence f1 f2 ps ->

Equivalence (mapSen mapEnv vars f1) (mapSen mapEnv vars f2) ps

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

True_atom ps -> True_atom ps

False_atom ps -> False_atom ps

Existl_equation t1 t2 ps ->

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

Strong_equation t1 t2 ps ->

Strong_equation (mapTERM mapEnv vars t1) (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

maybe defTup

(\ ts -> assert (not $ Set.null ts)

(if Set.member (toPredType pType) ts

then addTup

else defTup))

(Map.lookup prn fPreds)

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 nVars =

freshWorldVar (vars) : vars

in (head vars, head nVars, nVars))

getRel mo map' =

Map.findWithDefault

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

(modalityToModName mo)

map'

trans' mTerm propSymb trForm nvs f1 =

replacePropPredication mTerm

propSymb (mapSen mapEnv nvs f1) trForm

mapT = mapTERM mapEnv newVars

in

case f of

BoxOrDiamond True moda f1 _ ->

let rel = getRel moda pwRelMap in

case moda of

Simple_mod _ ->

case map sentence

$ concat [inlineAxioms CASL

" sort fws \n\

\ pred rel : fws * fws; \n\

\ trans_f1 : () \n\

\ vars w1 : fws \n\

\ . forall w2 : fws . rel(w1,w2) => \n\

\ trans_f1"] of

[newFormula] -> trans' Nothing

trans_f1 newFormula newVars f1

_ -> error "Modal2CASL: mapMSen: impossible error"

Term_mod t ->

let tt = getModTermSort rel in

case map sentence

$ concat [inlineAxioms CASL

" sort fws,tt \n\

\ pred rel : tt * fws * fws; \n\

\ trans_f1 : () \n\

\ vars w1 : fws; t_var : tt \n\

\ . forall w2 : fws . rel(t_var,w1,w2) => \n\

\ trans_f1"] of

[newFormula] -> trans' (Just (rel,t_var,mapT t))

trans_f1 newFormula

newVars f1

_ -> error "Modal2CASL: mapMSen: impossible error"

BoxOrDiamond False moda f1 _ ->

let rel = getRel moda pwRelMap in

case moda of

Simple_mod _ ->

case map sentence

$ concat [inlineAxioms CASL

" sort fws \n\

\ pred rel : fws * fws; \n\

\ trans_f1 : () \n\

\ vars w1 : fws \n\

\ . exists w2 : fws . rel(w1,w2) /\\ \n\

\ trans_f1"] of

[newFormula] -> trans' Nothing

trans_f1 newFormula newVars f1

_ -> error "Modal2CASL: mapMSen: impossible error"

Term_mod t ->

let tt = getModTermSort rel in

case map sentence

$ concat [inlineAxioms CASL

" sort fws,tt \n\

\ pred rel : tt * fws * fws; \n\

\ trans_f1 : () \n\

\ vars w1 : fws; t_var:tt \n\

\ . exists w2 : fws . rel(t_var,w1,w2) /\\ \n\

\ trans_f1"] of

[newFormula] -> trans' (Just (rel,t_var,mapT t))

trans_f1 newFormula newVars f1

_ -> error "Modal2CASL: mapMSen: impossible error"

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

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

mapTERM mapEnv@(MME{worldSort=fws,flexOps=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

maybe defTup

(\ ts -> assert (not $ Set.null ts)

(if Set.member (toOpType opType) ts

then addTup

else defTup))

(Map.lookup on fOps)

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"

addPlace :: Id -> Id

addPlace i@(Id ts ids ps)

| isMixfix i = Id ((\ (x,y) -> x++mkSimpleId place:y)

(span (not . isPlace) ts)) ids ps

| otherwise = i

modalityToModName :: MODALITY -> ModName

modalityToModName (Simple_mod sid) = SimpleM sid

modalityToModName (Term_mod t) =

case t of

Sorted_term _ srt _ -> SortM srt

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

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

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

addWorld_OP :: SORT -> OP_NAME -> Set.Set OpType

-> Map.Map OP_NAME (Set.Set OpType)

-> Map.Map OP_NAME (Set.Set OpType)

addWorld_OP = addWorld_ (\ws t -> t { opArgs = ws : opArgs t})

addWorld_PRED :: SORT -> PRED_NAME -> Set.Set PredType

-> Map.Map PRED_NAME (Set.Set PredType)

-> Map.Map PRED_NAME (Set.Set PredType)

addWorld_PRED = addWorld_ (\ws t -> t {predArgs = ws : predArgs t})

addWorld_ :: (Ord a) => (SORT -> a -> a)

-> SORT -> Id -> Set.Set a

-> Map.Map OP_NAME (Set.Set a)

-> Map.Map OP_NAME (Set.Set a)

addWorld_ f fws k set mp = Map.insert (addPlace k) (Set.map (f fws) set) mp

{-

-- List of sort ids for possible Worlds

worldSorts :: [SORT]

worldSorts = map mkSORT ("World":map (\x -> "World" ++ show x) [(1::Int)..])

where mkSORT s = mkId [mkSimpleId s]

-}

freshWorldSort :: Set.Set SORT -> SORT

freshWorldSort _sorSet = mkId [mkSimpleId "g_World"]

-- head . filter notKnown worldSorts

-- where notKnown s = not $ s `Set.member` sorSet

-- List of variables for worlds

worldVars :: [SIMPLE_ID]

worldVars = map mkSimpleId $ map (\ x -> "g_w" ++ show x) [(1::Int)..]

freshWorldVar :: [SIMPLE_ID] -> SIMPLE_ID

freshWorldVar vs = head . (filter notKnown) $ worldVars

where notKnown v = not $ elem v vs

{-

-- construct a relation from a given modality symbol which is new

consRelation :: Pred_map -- ^ map of allready known predicate symbols

->

-}