imp-comorph.tex revision c2b9205d94467085f8b07c294c86493d55427074
%!TEX root = main.tex
We show in this section the main functions used to implement the comorphism
from Maude to CASL described in Section \ref{sec:comoprh}.
The main function in this transformation is
\verb"maude2casl", that computes the CASL signature and sentences
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
that assign a concrete sort to each term with \verb"kindPredicates" .
\item Generate the \verb"rew" predicates to define the rewrite rules
between terms 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 the equations defined with \verb"owise"
are applied when the rest of possible equations cannot.
\item The rest of statements, namely memberships and rules, are 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 as CASL formulas,
obtained 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.sortRel = sbs',
CSign.opMap = cops',
CSign.assocOps = assoc_ops,
CSign.predMap = preds,
CSign.declaredSymbols = syms }, new_sens)
where csign = CSign.emptySign ()
ss = MSign.sorts msign
ss' = Set.map sym2id ss
mk = kindMapId $ MSign.kindRel msign
sbs = MSign.subsorts msign
sbs' = maudeSbs2caslSbs sbs mk
cs = Set.union ss' $ kindsFromMap mk
preds = rewPredicates cs
rs = rewPredicatesSens cs
ops = deleteUniversal $ MSign.ops msign
ksyms = kinds2syms cs
(cops, assoc_ops, _) = translateOps mk ops
ctor_sen = []
cops' = universalOps cs cops $ booleanImported ops
rs' = rewPredicatesCongSens cops'
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_syms = preds2syms preds
new_sens = concat [rs, rs', 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 Maude specification and
value their 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 = Map.foldWithKey kindPredicate Map.empty
\end{verbatim}
}
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 has 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 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}
}
The \verb"rew" predicates are declared with the function
\verb"rewPredicates", that traverses the set of kinds applying
the function \verb"rewPredicate":
{\codesize
\begin{verbatim}
\end{verbatim}
}
This function defines a binary predicate using as name the constant
\verb"rewID" and the kind as type of the arguments:
{\codesize
\begin{verbatim}
rewPredicate kind m = Map.insertWith (Set.union) rewID ar m
where ar = Set.singleton $ CSign.PredType [kind, kind]
\end{verbatim}
}
Once these 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 with the \verb"rewID" constant and applied to the
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
\end{verbatim}
}
Since the values in the Maude operator map are sets of operator declarations
(see Section \ref{sec:da} for details)
the function \verb"translateOpDeclSet" has to traverse these sets, 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, cs) = case tl of
[] -> (ops', assoc_ops', cs')
_ -> translateOpDecl im (syms', ats) (ops', assoc_ops', cs')
where sym = head $ Set.toList syms
tl = tail $ Set.toList syms
syms' = Set.fromList tl
(cop_id, ot, _) = fromJust $ maudeSym2CASLOp im sym
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}
}
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' [] _) = quantifyUniversally form
where ct = maudeTerm2caslTerm im t
ct' = maudeTerm2caslTerm im t'
form = CAS.Strong_equation ct ct' nullRange
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 = createImpForm conds_form concl_form
\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 ty' nullRange
where ty' = maudeType2caslSort 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' = maudeType2caslSort ty im
op_type = CAS.Op_type CAS.Total [] ty' 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' = maudeType2caslSort ty im
types_tts = getTypes tts
op_type = CAS.Op_type CAS.Total types_tts ty' 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 into
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 CASL memberships by translating
the term and the sort:
{\codesize
\begin{verbatim}
cond2formula im (MAS.MbCond t s) = CAS.Membership ct s' nullRange
where ct = maudeTerm2caslTerm im t
s' = token2id $ getName s
\end{verbatim}
}
\item Rewrite conditions are translated into formulas by using both terms
as arguments of the corresponding \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 equation:
{\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
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 = createImpForm ex_form eq_form
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 to symbols
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.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 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 pn pt acc = Set.insert sym acc
where sym = CSign.Symbol pn $ CSign.PredAsItemType pt
\end{verbatim}
}