%!TEX root = main.tex

We show in this section the main functions used to implement the comorphism

from Maude to CASL. The main function in this transformation is

\verb"maude2casl", that computes the signature and sentences of CASL

given the Maude signature and sentences

{\codesize

\begin{verbatim}

maude2casl :: MSign.Sign -> [Named MSentence.Sentence]

-> (CSign.CASLSign, [Named CAS.CASLFORMULA])

\end{verbatim}

}

This function splits the work into different stages:

\begin{itemize}

\item First, given the sorts and the subsort relations, a map is built

with the function \verb"arrangeKinds" were each sort is related to its

kind. These kinds are used to:

\begin{itemize}

\item Generate the predicates described in Section \ref{sec:comoprh}

that assign a concrete sort to each term with \verb"kindPredicates" .

\item Generate the \verb"rew" predicates described in Section

\ref{sec:comoprh} to define the rewrite rules between term of each

kind with \verb"rewPredicates".

\item Create the formulas associated to the \verb"rew" predicates

shown above, stating that they are reflexive and transitive, with

\verb"rewPredicatesSens".

\end{itemize}

\item Then CASL operators are obtained from the Maude operators:

\begin{itemize}

\item The function \verb"translateOps" translates the Maude operator map

into a tuple of CASL operators, CASL associative operators,

the membership axioms (i.e. CASL predicates) induced by each Maude operator,

and a set of operators with the \verb"ctor" attribute, that will be

used to generate the sentence about datatypes with \verb"ctorSen".

\item Since CASL does not allow the definition

of polymorphic operators, these operators are removed from the map

with \verb"deleteUniversal" and for each one of these Maude operators we

create a set of CASL operators with all the possible profiles with

\verb"universalOps".

\end{itemize}

\item CASL sentences are obtained from the Maude sentences and from

predefined CASL libraries:

\begin{itemize}

\item In the computation of the CASL formulas we split Maude sentences in

equations defined without the \verb"owise" attribute, equations defined

with \verb"owise", and the rest of statements with the function

\verb"splitOwiseEqs".

\item The equations defined without the \verb"owise" attribute are

translated as universally quantified equations, as shown in Section

\ref{sec:comoprh}, with \verb"noOwiseSen2Formula".

\item Equations with the \verb"owise" attribute are translated using

a negative existential quantification, as we will show later, with

the function \verb"owiseSen2Formula". This function requires as additional

parameter the definition of the formulas defined without the \verb"owise"

attribute, in order to state that they are applied when the rest of

possible formulas cannot be applied.

\item The rest of statements, namely memberships and rules, as translated

as predicates as described in Section \ref{sec:comoprh} with the function

\verb"mb_rl2formula".

\item There are some built-in operators in Maude that are not defined by

means of equations. To allow the user to reason about them, we provide

some libraries with the definitions of these operators with CASL formulas,

that are loaded with \verb"loadLibraries".

\end{itemize}

\item Finally, the CASL symbols are created:

\begin{itemize}

\item The kinds are translated to symbols with \verb"kinds2syms".

\item The operators are translated with \verb"ops2symbols".

\item The symbol predicates are obtained with \verb"preds2syms".

\end{itemize}

\end{itemize}

{\codesize

\begin{verbatim}

maude2casl msign nsens = (csign { CSign.sortSet = cs,

CSign.opMap = cops',

CSign.assocOps = assoc_ops,

CSign.predMap = preds,

CSign.declaredSymbols = syms }, new_sens)

where csign = CSign.emptySign ()

mk = arrangeKinds (MSign.sorts msign) (MSign.subsorts msign)

cs = kindsFromMap mk

ks = kindPredicates mk

rp = rewPredicates ks cs

rs = rewPredicatesSens cs

ops = deleteUniversal $ MSign.ops msign

ksyms = kinds2syms cs

(cops, assoc_ops, ops_forms, comps) = translateOps mk ops

ctor_sen = [ctorSen False (cs, Rel.empty, comps)]

cops' = universalOps cs cops $ booleanImported ops

pred_forms = loadLibraries (MSign.sorts msign) ops

ops_syms = ops2symbols cops'

(no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens

no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens

mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens

preds = Map.unionWith (Set.union) ks rp

preds_syms = preds2syms preds

syms = Set.union ksyms $ Set.union ops_syms preds_syms

new_sens = concat [rs, ops_forms, no_owise_forms, owise_forms,

mb_rl_forms, ctor_sen, pred_forms]

\end{verbatim}

}

Given a map of \verb"Id" with keys the sorts in the specification and

value its associated kind, the function \verb"kindPredicates" computes

the predicates that assign the proper sort to each term.

\verb"kindPredicates" traverses the map applying the function

\verb"kindPredicate":

{\codesize

\begin{verbatim}

kindPredicates :: IdMap -> Map.Map Id (Set.Set CSign.PredType)

kindPredicates = Map.foldWithKey kindPredicate Map.empty

\end{verbatim}

}

\noindent Where \verb"kindPredicate" receives the identifier of a sort,

the identifier of its kind and the accumulated map of CASL predicates

and then distinguishes if the sort is \verb"Universal", and thus have to be

skipped, or it is any other sort and the map has to be extended with a

new unary predicate named as the sort and with arity the kind:

{\codesize

\begin{verbatim}

kindPredicate :: Id -> Id -> Map.Map Id (Set.Set CSign.PredType)

-> Map.Map Id (Set.Set CSign.PredType)

kindPredicate sort kind mis = case sort == (str2id "Universal") of

True -> mis

False -> let ar = Set.singleton $ CSign.PredType [kind]

in Map.insertWith (Set.union) sort ar mis

\end{verbatim}

}

Once the \verb"rew" predicates has been declared, we have to introduce

formulas to state their properties. The function \verb"rewPredicatesSens"

accomplishes this task by traversing the set of kinds and applying

\verb"rewPredicateSens":

{\codesize

\begin{verbatim}

rewPredicatesSens :: Set.Set Id -> [Named CAS.CASLFORMULA]

rewPredicatesSens = Set.fold rewPredicateSens []

\end{verbatim}

}

This function generates the formulas for each kind:

{\codesize

\begin{verbatim}

rewPredicateSens :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

rewPredicateSens kind acc = ref : trans : acc

where ref = reflSen kind

trans = transSen kind

\end{verbatim}

}

We describe the formula for the reflexivity, being the transitivity

analogous. A new variable of the required kind is created with

the auxiliary function \verb"newVar", then the qualified predicate

name is created, where \verb"rewID" is a constant specifying the

name of the \verb"rew" predicate, and applied twice to the same

variable. Finally, the formula is named with the prefix \verb"rew_refl_"

followed by the name of the kind:

{\codesize

\begin{verbatim}

reflSen :: Id -> Named CAS.CASLFORMULA

reflSen kind = makeNamed name $ quantifyUniversally form

where v = newVar kind

pred_type = CAS.Pred_type [kind, kind] nullRange

pn = CAS.Qual_pred_name rewID pred_type nullRange

form = CAS.Predication pn [v, v] nullRange

name = "rew_refl_" ++ show kind

\end{verbatim}

}

The function \verb"translateOps" traverses the map of Maude operators,

applying to each of them the function \verb"translateOpDeclSet":

{\codesize

\begin{verbatim}

translateOps :: IdMap -> MSign.OpMap -> OpTransTuple

translateOps im = Map.fold (translateOpDeclSet im) (Map.empty, Map.empty, [], Set.empty)

\end{verbatim}

}

Since the values in the Maude operator map are set of operator declarations

(see Section \ref{sec:da} for details),

the function \verb"translateOpDeclSet" traverses this set, applying

\verb"translateOpDecl" to each operator declaration:

{\codesize

\begin{verbatim}

translateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple

translateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods

\end{verbatim}

}

The function \verb"translateOpDecl" receives an operator declaration,

that consists of all the operators declared with the same profile at

the kind level, thus from all these declarations only one CASL operator

must be generated, although we still need the memberships associated

to each profile. First, these memberships are translated into CASL

predicates with the function \verb"ops2pred", explained below.

Then, we take the first profile in the set and transform

it with \verb"maudeSym2CASLOp", that returns a pair with a valid CASL

operator identifier and the operator type; we use these values

to expand the operator map. Finally, the function checks if the operator

has the attributes \texttt{assoc} or \texttt{ctor} to add the

operator to the corresponding accumulators:

{\codesize

\begin{verbatim}

translateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple

translateOpDecl im (syms, ats) (ops, assoc_ops, forms, cs) = (ops', assoc_ops', forms', cs')

where predOps = ops2pred im syms

sym = head $ Set.toList syms

(cop_id, ot) = fromJust $ maudeSym2CASLOp im sym

cop_type = Set.singleton ot

forms' = forms ++ predOps

ops' = Map.insertWith (Set.union) cop_id cop_type ops

assoc_ops' = if any MAS.assoc ats

then Map.insertWith (Set.union) cop_id cop_type assoc_ops

else assoc_ops

cs' = if any MAS.ctor ats

then Set.insert (Component cop_id ot) cs

else cs

\end{verbatim}

}

We describe in detail how the predicates obtained from the membership

axioms associated to each operator declaration are obtained. The function

\verb"ops2pred" traverses the set of operator symbols, applying

the function \verb"op2pred":

{\codesize

\begin{verbatim}

ops2pred :: IdMap -> MSym.SymbolSet -> [Named CAS.CASLFORMULA]

ops2pred im = Set.fold (op2pred im) []

\end{verbatim}

}

When the symbol is an operator declaration, the function distinguishes

if the result type if a sort, and thus a membership has to be generated,

or it is a kind and only the accumulator is returned. In the first

case, the list of arguments is traversed with the auxiliary

\verb"ops2predPremises" to compute the premises of the predicate

and the variables used. Note that only the arguments declared at the

sort level generate premises, while the ones declared at the kind

are skipped. We apply these variables to the operator to create the

conclusion, and finally an implication is created and universally

quantified to obtain the final formula:

{\codesize

\begin{verbatim}

op2pred :: IdMap -> MSym.Symbol -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

op2pred im (MSym.Operator op ar co) acc = case co of

MSym.Sort s -> let

co' = token2id s

kind = Map.findWithDefault (errorId "op-mb to predicate") co' im

f = \ m x -> Map.lookup (token2id $ getName x) m

ar' = mapMaybe (f im) ar

op_type = CAS.Op_type CAS.Total ar' kind nullRange

op' = CAS.Qual_op_name (token2id op) op_type nullRange

(vars, prems) = ops2predPremises im ar 0

pred_type = CAS.Pred_type [kind] nullRange

pred_name = CAS.Qual_pred_name co' pred_type nullRange

op_term = CAS.Application op' vars nullRange

op_pred = CAS.Predication pred_name [op_term] nullRange

conj_form = createConjForm prems

imp_form = if null prems

then op_pred

else CAS.Implication conj_form op_pred True nullRange

q_form = quantifyUniversally imp_form

final_form = makeNamed "" q_form

in final_form : acc

_ -> acc

\end{verbatim}

}

When the received symbol is not an operator declaration the accumulator

is returned:

{\codesize

\begin{verbatim}

op2pred _ _ acc = acc

\end{verbatim}

}

As said above, Maude equations that are not defined with the \verb"owise"

attribute are translated to CASL with \verb"noOwiseSen2Formula". This

function extracts the current equation from the named sentence, translates

it with \verb"noOwiseEq2Formula" and creates a new named sentence

with the resulting formula:

{\codesize

\begin{verbatim}

noOwiseSen2Formula :: IdMap -> Named MSentence.Sentence

-> Named CAS.CASLFORMULA

noOwiseSen2Formula im s = s'

where MSentence.Equation eq = sentence s

sen' = noOwiseEq2Formula im eq

s' = s { sentence = sen' }

\end{verbatim}

}

The function \verb"noOwiseEq2Formula" distinguishes whether the equation

is conditional or not. In both cases, the Maude terms in the equation

are translated into CASL terms with \verb"maudeTerm2caslTerm", and a

strong equation is used to create a formula. If the equation has no

conditions this formula is universally quantified and returned as result,

while if it has conditions each of them generates a formula, and their

conjunction, computed with \verb"conds2formula", will be used as premise

of the equality formula:

{\codesize

\begin{verbatim}

noOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA

noOwiseEq2Formula im (MAS.Eq t t' conds@(_:_) _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

conds_form = conds2formula im conds

concl_form = CAS.Strong_equation ct ct' nullRange

form = CAS.Implication conds_form concl_form True nullRange

noOwiseEq2Formula im (MAS.Eq t t' [] _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

form = CAS.Strong_equation ct ct' nullRange

\end{verbatim}

}

\verb"maudeTerm2caslTerm" is defined for each Maude term:

\begin{itemize}

\item Variables are translated into qualified CASL variables, and their

sort is changed to the corresponding kind:

{\codesize

\begin{verbatim}

maudeTerm2caslTerm :: IdMap -> MAS.Term -> CAS.CASLTERM

maudeTerm2caslTerm im (MAS.Var q ty) = CAS.Qual_var q kind nullRange

where kind = Map.findWithDefault (errorId "maude_term2CASL_term")

(token2id $ getName ty) im

\end{verbatim}

}

\item Constants are translated into the applications of the constant

name to the empty list of arguments, using again the kind of the

given sort:

{\codesize

\begin{verbatim}

maudeTerm2caslTerm im (MAS.Const q ty) = CAS.Application op [] nullRange

where name = token2id q

ty' = token2id $ getName ty

kind = Map.findWithDefault (errorId "maude term to CASL term") ty' im

op_type = CAS.Op_type CAS.Total [] kind nullRange

op = CAS.Qual_op_name name op_type nullRange

\end{verbatim}

}

\item The application of an operator to a list of terms is translated

into another application, translating recursively the arguments into

valid CASL terms:

{\codesize

\begin{verbatim}

maudeTerm2caslTerm im (MAS.Apply q ts ty) = CAS.Application op tts nullRange

where name = token2id q

tts = map (maudeTerm2caslTerm im) ts

ty' = token2id $ getName ty

kind = Map.findWithDefault (errorId "maude_term2CASL_term") ty' im

types_tts = getTypes tts

op_type = CAS.Op_type CAS.Total types_tts kind nullRange

op = CAS.Qual_op_name name op_type nullRange

\end{verbatim}

}

\end{itemize}

The conditions are translated into a conjunction with \verb"conds2formula",

that traverses the conditions applying \verb"cond2formula" to each of them,

and then creates the conjunction of the obtained formulas:

{\codesize

\begin{verbatim}

conds2formula :: IdMap -> [MAS.Condition] -> CAS.CASLFORMULA

conds2formula im conds = CAS.Conjunction forms nullRange

where forms = map (cond2formula im) conds

\end{verbatim}

}

\begin{itemize}

\item Both equality and matching conditions are translated as

strong equations:

{\codesize

\begin{verbatim}

cond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA

cond2formula im (MAS.EqCond t t') = CAS.Strong_equation ct ct' nullRange

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

cond2formula im (MAS.MatchCond t t') = CAS.Strong_equation ct ct' nullRange

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

\end{verbatim}

}

\item Membership conditions are translated into formulas by using the sort

as the predicate name and its kind as the argument type:

{\codesize

\begin{verbatim}

cond2formula im (MAS.MbCond t s) = CAS.Predication pred_name [ct] nullRange

where ct = maudeTerm2caslTerm im t

s' = token2id $ getName s

kind = Map.findWithDefault (errorId "mb cond to formula") s' im

pred_type = CAS.Pred_type [kind] nullRange

pred_name = CAS.Qual_pred_name s' pred_type nullRange

\end{verbatim}

}

\item Rewrite conditions are translated into formulas by using both terms

as arguments of the \verb"rew" predicate:

{\codesize

\begin{verbatim}

cond2formula im (MAS.RwCond t t') = CAS.Predication pred_name [ct, ct'] nullRange

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

ty = token2id $ getName $ MAS.getTermType t

kind = Map.findWithDefault (errorId "rw cond to formula") ty im

pred_type = CAS.Pred_type [kind, kind] nullRange

pred_name = CAS.Qual_pred_name rewID pred_type nullRange

\end{verbatim}

}

\end{itemize}

The equations defined with the \verb"owise" attribute are translated

with \verb"owiseSen2Formula", that traverses them and applies

\verb"owiseEq2Formula" to the inner formula:

{\codesize

\begin{verbatim}

owiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]

-> Named MSentence.Sentence -> Named CAS.CASLFORMULA

owiseSen2Formula im owise_forms s = s'

where MSentence.Equation eq = sentence s

sen' = owiseEq2Formula im owise_forms eq

s' = s { sentence = sen' }

\end{verbatim}

}

This function receives all the formulas defined without the \verb"owise"

attribute and, for each formula with the same operator in the lefthand

side that the current equation (obtained with \verb"getLeftApp"), it

generates with \verb"existencialNegationOtherEqs" a negative existential

quantification stating that the arguments do not match or the condition

does not hold that is used as premise of the equation:

{\codesize

\begin{verbatim}

owiseEq2Formula :: IdMap -> [Named CAS.CASLFORMULA] -> MAS.Equation

-> CAS.CASLFORMULA

owiseEq2Formula im no_owise_form eq = form

where (eq_form, vars) = noQuantification $ noOwiseEq2Formula im eq

(op, ts, _) = fromJust $ getLeftApp eq_form

ex_form = existencialNegationOtherEqs op ts no_owise_form

imp_form = CAS.Implication ex_form eq_form True nullRange

form = CAS.Quantification CAS.Universal vars imp_form nullRange

\end{verbatim}

}

The rest of Maude sentences are translated in a similar way to the one

shown for the conditions above.

The rest of the sentences generated in the comorphism are obtained

from external libraries with the function \verb"readLib". We describe

below how sentences defining the behavior of the natural numbers are

loaded: once the library is obtained, we transform the theory sentences

into named sentences with \verb"toNamedList" and then we ``coerce''

them with \verb"coerceSens" to indicate that they are CASL sentences.

Finally, the sentence about the generators is filtered and the result

returned:

{\codesize

\begin{verbatim}

loadNaturalNatSens :: [Named CAS.CASLFORMULA]

loadNaturalNatSens =

let lib = head $ unsafePerformIO $ readLib "Maude/MaudeNumbers.casl"

in case lib of

G_theory lid _ _ thSens _ -> let sens = toNamedList thSens

in do

sens' <- coerceSens lid CASL "" sens

filter (not . ctorCons) sens'

\end{verbatim}

}

The translation from sorts, operators and predicates works in a similar

way to the transformations shown above, so we only describe the

how the symbols corresponding with predicates are obtained. The function

\verb"preds2syms" traverses the map of predicates and inserts each

obtained symbol into the set with \verb"pred2sym":

{\codesize

\begin{verbatim}

preds2syms :: Map.Map Id (Set.Set CSign.PredType) -> Set.Set CSign.Symbol

preds2syms = Map.foldWithKey pred2sym Set.empty

\end{verbatim}

}

This function traverses the set of predicate types and creates the

symbol corresponding to each one with \verb"createSym4id":

{\codesize

\begin{verbatim}

pred2sym :: Id -> Set.Set CSign.PredType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol

pred2sym pn spt acc = Set.fold (createSym4id pn) acc spt

\end{verbatim}

}

\verb"createSym4id" generates the symbol and inserts it into the

accumulated set:

{\codesize

\begin{verbatim}

createSym4id :: Id -> CSign.PredType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol

createSym4id pn pt acc = Set.insert sym acc

where sym = CSign.Symbol pn $ CSign.PredAsItemType pt

\end{verbatim}

}