8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering{- |

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart PoetteringModule : $Header$

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart PoetteringCopyright : nevrenato@gmail.com

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart PoetteringLicense : GPLv2 or higher, see LICENSE.txt

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart PoetteringMaintainer : Christian.Maeder@dfki.de

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart PoetteringStability : experimental

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart PoetteringPortability : non-portable (imports Logic.Logic)

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart PoetteringComorphism HybridCASL to CASL.

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering-}

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringmodule Comorphisms.Hybrid2CASL

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering ( Hybrid2CASL (..)

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering ) where

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringimport Logic.Logic

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringimport Logic.Comorphism

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringimport Common.ProofTree

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringimport Common.AS_Annotation

d7b8eec7dc7fe307d3a08b32cf1a9ad4276ce6d5Lennart Poetteringimport Common.Result

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringimport qualified Common.Lib.Rel as Rel

4aa4d2ae9717d0f8656528a3197bbc0c256380b1Zbigniew Jędrzejewski-Szmekimport qualified Common.Lib.MapSet as MapSet

4aa4d2ae9717d0f8656528a3197bbc0c256380b1Zbigniew Jędrzejewski-Szmekimport Common.Id

4aa4d2ae9717d0f8656528a3197bbc0c256380b1Zbigniew Jędrzejewski-Szmek

4aa4d2ae9717d0f8656528a3197bbc0c256380b1Zbigniew Jędrzejewski-Szmekimport qualified Data.Set as Set

4aa4d2ae9717d0f8656528a3197bbc0c256380b1Zbigniew Jędrzejewski-Szmekimport qualified Data.Map as Map

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

0a2f9085e29c855ec1aaa996ded00fc36b06210cLennart Poetteringimport Hybrid.Logic_Hybrid

0a2f9085e29c855ec1aaa996ded00fc36b06210cLennart Poetteringimport Hybrid.AS_Hybrid

0a2f9085e29c855ec1aaa996ded00fc36b06210cLennart Poetteringimport Hybrid.HybridSign

0a2f9085e29c855ec1aaa996ded00fc36b06210cLennart Poettering

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringimport CASL.Logic_CASL

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringimport CASL.AS_Basic_CASL

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringimport CASL.Morphism

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringimport CASL.Sign

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringimport CASL.Sublogic as SL

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringdata Hybrid2CASL = Hybrid2CASL deriving Show

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering-- Just to make things easier to understand

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringtype HForm = HybridFORMULA

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringtype CForm = CASLFORMULA

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringtype CSign = CASLSign

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poetteringinstance Language Hybrid2CASL where

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering language_name Hybrid2CASL = "Hybrid2CASL"

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poetteringinstance Comorphism Hybrid2CASL

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering Hybrid ()

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering H_BASIC_SPEC HForm SYMB_ITEMS SYMB_MAP_ITEMS

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering HSign

7dbb1d08f66cd44b1296be3ee8e3629b989e19a8Zbigniew Jędrzejewski-Szmek HybridMor

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering Symbol RawSymbol ()

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering CASL

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering CASL_Sublogics

ecabcf8b6edcc856ec2fd5bd43fc675a8fe04731Lennart Poettering CASLBasicSpec CForm SYMB_ITEMS SYMB_MAP_ITEMS

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering CSign

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering CASLMor

7dbb1d08f66cd44b1296be3ee8e3629b989e19a8Zbigniew Jędrzejewski-Szmek Symbol RawSymbol ProofTree where

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

ecabcf8b6edcc856ec2fd5bd43fc675a8fe04731Lennart Poettering sourceLogic Hybrid2CASL = Hybrid

7dbb1d08f66cd44b1296be3ee8e3629b989e19a8Zbigniew Jędrzejewski-Szmek sourceSublogic Hybrid2CASL = ()

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering targetLogic Hybrid2CASL = CASL

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering mapSublogic Hybrid2CASL _ = Just SL.caslTop

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering { SL.cons_features = SL.emptyMapConsFeature

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering , SL.sub_features = SL.NoSub

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering }

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering map_theory Hybrid2CASL = transTheory

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering has_model_expansion Hybrid2CASL = True

4aa4d2ae9717d0f8656528a3197bbc0c256380b1Zbigniew Jędrzejewski-Szmek is_weakly_amalgamable Hybrid2CASL = True

4aa4d2ae9717d0f8656528a3197bbc0c256380b1Zbigniew Jędrzejewski-Szmek is_model_transportable Hybrid2CASL = True

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering isInclusionComorphism Hybrid2CASL = True

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering-- Translates the given theory in an HybridCASL form to an equivalent

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering-- theory in CASL form

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering-- Question : Why some sentences are in the sig and other sentences are

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering-- in the 2nd argument ? (this is scary)

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering-- fs'' is needed for special sentences, refering about datatypes

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering-- for which hybridization has nothing to do

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart PoetteringtransTheory :: (HSign, [Named HForm]) -> Result (CSign, [Named CForm])

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart PoetteringtransTheory (s,fs) = let

7dbb1d08f66cd44b1296be3ee8e3629b989e19a8Zbigniew Jędrzejewski-Szmek newSig = transSig s

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering fs' = fmap (mapNamed trans) fs

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering fs'' = dataTrans (fs ++ sentences s)

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering newSens = fs' ++ sentences newSig ++ fs''

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering rigidP = applRig (rigidPreds $ extendedInfo s) "RigidPred" gnPCons

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering rigidO = applRig (rigidOps $ extendedInfo s) "RigidOp" gnOCons

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering in return (newSig,rigidP ++ rigidO ++ newSens)

755bde375f4db393ad06e73340bfcf4d0cf91bb2Lennart Poettering

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering-- Special formulas not covered by normal hybridization

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart PoetteringdataTrans :: [Named HForm] -> [Named CForm]

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart PoetteringdataTrans = foldr f []

cc56fafeebf814ef035e549115cf1850e6473fa5WaLyong Cho where

7dbb1d08f66cd44b1296be3ee8e3629b989e19a8Zbigniew Jędrzejewski-Szmek f a b = if sentence x == (Nothing :: Maybe HForm) then b

da927ba997d68401563b927f92e6e40e021a8e5cMichal Schmidt else mapNamed (\(Just x') -> x') x : b

7dbb1d08f66cd44b1296be3ee8e3629b989e19a8Zbigniew Jędrzejewski-Szmek where

7dbb1d08f66cd44b1296be3ee8e3629b989e19a8Zbigniew Jędrzejewski-Szmek x = mapNamed f' a

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering f' h = case h of

7dbb1d08f66cd44b1296be3ee8e3629b989e19a8Zbigniew Jędrzejewski-Szmek (Sort_gen_ax a' b') -> Just $ Sort_gen_ax a' b'

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering _ -> Nothing

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering

7dbb1d08f66cd44b1296be3ee8e3629b989e19a8Zbigniew Jędrzejewski-SzmektransSig :: HSign -> CSign

7dbb1d08f66cd44b1296be3ee8e3629b989e19a8Zbigniew Jędrzejewski-SzmektransSig hs = let workflow = (transSens hs) . (addWrldArg hs)

8ea48dfcd33e8db0c01bf8c57c3bbcfdc3c86d4bLennart Poettering workflow' = (addRels hs) . (addWorlds hs)

in workflow . workflow' $ newSign hs

-- Creates a new CASL signature based on the hybrid Sig

-- Also adds the world sort.

newSign :: HSign -> CSign

newSign hs = (emptySign ())

{ sortRel = Rel.insertKey worldSort $ sortRel hs

,emptySortSet = emptySortSet hs

,assocOps = assocOps hs

,varMap = varMap hs

,declaredSymbols = declaredSymbols hs

,envDiags = envDiags hs

,annoMap = annoMap hs

,globAnnos = globAnnos hs

,opMap = addOpMapSet (rigidOps $ extendedInfo hs) (opMap hs)

,predMap = addMapSet (rigidPreds $ extendedInfo hs) (predMap hs)

}

-- | Adds the World constants, based

-- on the nominals in HSign

addWorlds :: HSign -> CSign -> CSign

addWorlds hs cs =

let getWorld = OpType Total [] worldSort

s = extendedInfo hs

kl = Map.keys $ nomies s

workflow = stringToId . ("Wrl_" ++) . tokStr

il = fmap workflow kl

ins = foldr (\k m -> MapSet.insert k getWorld m) (opMap cs) il

in cs { opMap = ins }

-- | Adds the Accessibility relation, based

-- ono the modalities found in HSign

addRels :: HSign -> CSign -> CSign

addRels hs cs =

let accRelT = PredType [worldSort,worldSort]

s = extendedInfo hs

kl = Map.keys $ modies s

il = fmap (stringToId . ("Acc_" ++) . tokStr) kl

ins = foldl (\m k -> MapSet.insert k accRelT m) (predMap cs) il

in cs { predMap = ins }

-- | Adds one argument of type World to all preds and ops

-- definitions in an hybrid signature and passes them to a caslsig

addWrldArg :: HSign -> CSign -> CSign

addWrldArg hs cs = let

f (OpType a b c) = OpType a (worldSort:b) c

g (PredType a) = PredType (worldSort:a)

ops = addOpMapSet (rigidOps $ extendedInfo hs) (opMap hs)

preds = addMapSet (rigidPreds $ extendedInfo hs) (predMap hs)

ks = Set.elems $ MapSet.keysSet ops

ks' = Set.elems $ MapSet.keysSet preds

in cs

{ opMap = foldr (MapSet.update (Set.map f)) (opMap cs) ks

, predMap = foldr (MapSet.update (Set.map g)) (predMap cs) ks'

}

-- Translates all hybridformulas in a hybridSig to caslformulas

-- Ones are in the declaration of nominals and modalities (however

-- for nows that is forbidden to happen)

-- The others come from the casl sig

transSens :: HSign -> CSign -> CSign

transSens hs cs = let

mods = Map.elems (modies $ extendedInfo hs)

noms = Map.elems (nomies $ extendedInfo hs)

fs = concat $ mods ++ noms

workflow = makeNamed "" . trans . item

fs' = fmap workflow fs

fs'' = fmap (mapNamed trans) (sentences hs)

in cs { sentences = fs' ++ fs'' }

-- Translates an HybridCASL formula to CASL formula

trans :: HForm -> CForm

trans = let w = mkSimpleId "world"

vars = mkVarDecl w worldSort

in (mkForall [vars]) . trForm (QtM w) []

-- | Formula translator

-- The 2nd argument is used to store the reserved words

trForm :: Mode -> [String] -> HForm -> CForm

trForm w s b = case b of

ExtFORMULA f -> alpha w s f

Junction j fs r -> Junction j (fmap (trForm w s) fs) r

Relation f r f' q -> Relation (trForm w s f) r (trForm w s f') q

Negation f _ -> mkNeg $ trForm w s f

Predication p l _ -> mkPredication (mkPName p) $ trTerms w s l

Quantification q l f r ->Quantification q l (trForm w s f) r

Definedness t _ -> Definedness (trTerm w s t) nullRange

Atom a r -> Atom a r

_ -> error "Hybrid2CASL.trForm"

-- | Alpha function, translates pure Hybrid Formulas

alpha :: Mode -> [String] -> H_FORMULA -> CForm

alpha w s b = case (w, b) of

(QtM wm,Here n _) -> mkStEq (mkArg (Right n) s) $ mkVarTerm wm worldSort

(_,Here n _) -> mkStEq (mkArg (Right n) s) $ mkArg (Left w) s

(_,BoxOrDiamond True m f _) -> trBox w m s f

(_,BoxOrDiamond False m f _) -> trForm w s $ toBox m f

(_,At (Simple_nom n) f _) -> trForm (AtM n) s f

(_,Univ n f _) -> trForall w n s f

(_,Exist n f _) -> mkNeg $ trForall w n s (mkNeg f)

where

toBox m f = mkNeg . ExtFORMULA $ BoxOrDiamond True m (mkNeg f) nullRange

-- | Function that takes care of formulas of box type

trBox :: Mode -> MODALITY -> [String] -> HForm -> CForm

trBox m (Simple_mod m') s f = quant $ mkImpl prd $ trForm (QtM v) ss f

where

quant = mkForall [var]

var = mkVarDecl v worldSort

v = mkSimpleId $ head ss

ss = newVarName s

prd = mkPredication predN $ predA m

predN = qp m' t

predA w = [mkArg (Left w) s, mkArg (Left (QtM v)) s]

qp x = mkQualPred (stringToId . ("Acc_" ++) $ show x)

t = Pred_type [worldSort,worldSort] nullRange

trBox _ _ _ _ = trueForm

-- translation function for the quantification of nominals case

trForall :: Mode -> NOMINAL -> [String] -> HForm -> CForm

trForall w n s f = mkForall x f' where

x = return $ mkVarDecl (extId n) worldSort

f' = trForm w (toStr n : s) f

toStr = show . extId

extId = \(Simple_nom a) -> a

-- Function that translates a list of hybrid terms to casl terms

trTerms :: Mode -> [String] -> [TERM H_FORMULA] -> [TERM ()]

trTerms m s l = mkArg (Left m) s : fmap (trTerm m s) l

-- Function that translates hybrid term to casl term

trTerm :: Mode -> [String] -> (TERM H_FORMULA) -> TERM ()

trTerm m s t = case t of

Qual_var v s' x -> Qual_var v s' x

Application o l r -> Application (mkOName o) (trTerms m s l) r

Sorted_term t' s' r -> Sorted_term (trTerm m s t') s' r

_ -> error "Hybrid2CASL.trTerm"

-- **** Auxiliar functions and datatype ****

-- The world sort type

worldSort :: SORT

worldSort = stringToId "World"

mkPName :: PRED_SYMB -> PRED_SYMB

mkPName ~(Qual_pred_name n t _) = mkQualPred n (f t)

where f (Pred_type l r) = Pred_type (worldSort:l) r

mkOName :: OP_SYMB -> OP_SYMB

mkOName ~(Qual_op_name n t _) = mkQualOp n (f t)

where f (Op_type o l s r) = Op_type o (worldSort:l) s r

-- Function that will decide how to create a new argument

-- That argument can be a variable or a nominal (constant)

mkArg :: (Either Mode NOMINAL) -> [String] -> TERM ()

mkArg a l = case a of

Left (QtM w) -> vt w

Left (AtM w) -> ch tokStr w

Right (Simple_nom n) -> ch show n

where

vt x = mkVarTerm x worldSort

ap x = mkAppl (qo x t) []

ch f x = if (f x) `elem` l then (vt x) else (ap x)

qo x = mkQualOp $ stringToId . ("Wrl_" ++) $ show x

t = Op_type Total [] worldSort nullRange

-- Create a new variable name new in the formula

newVarName :: [String] -> [String]

newVarName xs = ("world" ++) (show $ length xs) : xs

-- | Auxiliar datatype to determine wich is the argument of alpha

-- | Quantified Mode or At mode

data Mode = QtM VAR | AtM SIMPLE_ID

-- **** End of auxiliar functions and datatypes section ****************

------- Generation of constraints associated with rigid designators

toName :: (Functor f) => String -> f a -> f (Named a)

toName s = fmap $ makeNamed s

-- Adds the constraints associated with the rigidity

-- of predicates or operations.

applRig :: (Ord k) => MapSet.MapSet k a ->

String ->

(k -> a -> CForm)->

[Named CForm]

applRig m s f = toName s $ glueDs ks f m

where ks = Set.elems $ MapSet.keysSet m

-- Given a list of designators, generates the rigidity constraints

-- associated, and concats them into a single list

glueDs :: (Ord k) => [k] ->

(k -> a -> CForm) ->

MapSet.MapSet k a ->

[CForm]

glueDs ks f m = concat $ foldr (\a b -> (g a) : b) [] ks

where g k = glueDe k (MapSet.lookup k m) f

-- Given a single designator, genereates the rigidity constraints

-- associated, and joins them into a single list

glueDe :: k -> Set.Set a -> (k -> a -> CForm) -> [CForm]

glueDe n s f = foldr (\a b -> (f n) a : b) [] $ Set.elems s

-- Generates a rigid constraint from a single pred name and type

-- We add the extra world argument in mkPredType so that it coincides

-- with the later translated predicate definition

gnPCons :: PRED_NAME -> PredType -> CForm

gnPCons n (PredType ts) = mkForall decls $ mkForall wA $ mkImpl f1 f2

where f1 = mkPredication predName $ terms w1

f2 = mkPredication predName $ terms w2

decls = fromSort ts

terms = \x -> fromDecls $ x : decls

predName = mkPredName n $ mkPredType ts

mkPredName n' t = Qual_pred_name n' t nullRange

mkPredType x = Pred_type (worldSort:x) nullRange

gnOCons :: OP_NAME -> OpType -> CForm

gnOCons n (OpType o ts t) = mkForall decls $ mkForall wA $ f

where f = mkStEq (mkAppl opName $ terms w1) t2

t2 = (mkAppl opName $ terms w2)

decls = fromSort ts

terms = \x -> fromDecls $ x : decls

opName = mkOpName n $ mkOpType o (worldSort:ts) t

mkOpName n' t' = Qual_op_name n' t' nullRange

mkOpType x y z = Op_type x y z nullRange

-- The next functions are auxiliar. They are need for generating the

-- proper variables/terms for the quantifiers,predications and operations.

w1 :: VAR_DECL

w1 = mkVarDecl (mkSimpleId "w") worldSort

w2 :: VAR_DECL

w2 = mkVarDecl (mkSimpleId "w'") worldSort

-- mkVarDecl doesn't support arrays as arg

-- mkForall doesn't support single elements as arg

wA :: [VAR_DECL]

wA = [Var_decl [mkSimpleId "w",mkSimpleId "w'"] worldSort nullRange]

-- Auxiliar function 1

fromSort :: [SORT] -> [VAR_DECL]

fromSort = snd . ( foldr f (0 :: Int,[]) )

where

f so (i,xs) = (i+1,mkVarDecl (str i) so : xs)

str i = mkSimpleId $ "x" ++ (show i)

-- Auxiliar function 2

fromDecls :: [VAR_DECL] -> [TERM f]

fromDecls = concat . (fmap fromDecl)

-- Auxiliar function 3

fromDecl :: VAR_DECL -> [TERM f]

fromDecl (Var_decl vs s _ ) = foldr f [] vs

where f a b = (g a) : b

g a = mkVarTerm a s