%!TEX root = main.tex

We describe in this section the main functions used to draw the

development graph for Maude specifications. The main function is

\verb"anaMaudeFile", that receives a record of all the options received

from the command line (of type \verb"HetcatsOpts") and the path of

the Maude file to be parsed and return a pair with the library

name and its environment.

{\codesize

\begin{verbatim}

anaMaudeFile :: HetcatsOpts -> FilePath -> IO (Maybe (LIB_NAME, LibEnv))

anaMaudeFile _ file = do

dg <- directMaudeParsing file

let name = Lib_id $ Direct_link "Maude_Module" nullRange

return $ Just (name, Map.singleton name dg)

\end{verbatim}

}

This environment is computed with the function

\verb"directMaudeParsing", that receives the file path and returns

a development graph. This analysis is performed in different stages:

First, the parser described in Section \ref{subsec:lex-parser}

Then, Maude is executed with \verb"runInteractiveCommand" to use

the parser described in Section \ref{subsec:maude-parser}

{\codesize

\begin{verbatim}

directMaudeParsing :: FilePath -> IO DGraph

directMaudeParsing fp = do

ns <- parse fp

let ns' = either (\ _ -> []) id ns

(hIn, hOut, _, _) <- runInteractiveCommand maudeCmd

hPutStrLn hIn $ "load " ++ fp

ms <- traverseNames hIn hOut ns'

hPutStrLn hIn "in Maude/hets.prj"

psps <- predefinedSpecs hIn hOut

sps <- traverseSpecs hIn hOut ms

hClose hIn

hClose hOut

return $ insertSpecs (psps ++ sps) Map.empty Map.empty [] emptyDG

\end{verbatim}

}

We explain briefly the main data structures used during the generation of

the development graph:

\begin{itemize}

\item The type \verb"ParamSort" defines a pair with a symbol representing

a sort and a list of tokens indicating the parameters present in the sort,

so for example the sort \verb"List{X, Y}" generates the pair

\verb"(List{X, Y}, [X,Y])":

{\codesize

\begin{verbatim}

type ParamSort = (Symbol, [Token])

\end{verbatim}

}

\item The information of each node introduced

in the development graph is stored in the tuple \verb"ProcInfo", that

contains the following information:

\begin{itemize}

\item The identifier of the node.

\item The signature of the node.

\item A list of symbols standing for the sorts that are not instantiated.

\item A list of triples with information about the parameters of the

specification, namely the name of the parameter, the name of the theory

and the list of not instantiated sorts from this theory.

\item A list with information about the parameterized sorts.

\end{itemize}

{\codesize

\begin{verbatim}

type ProcInfo = (Node, Sign, Symbols, [(Token, Token, Symbols)], [ParamSort])

\end{verbatim}

}

\item Each \verb"ProcInfo" tuple is associated to its corresponding module

expression in the \verb"TokenInfoMap" map:

{\codesize

\begin{verbatim}

type TokenInfoMap = Map.Map Token ProcInfo

\end{verbatim}

}

\item When a module expression is parsed a \verb"ModExpProc" tuple is

returned, containing the following information:

\begin{itemize}

\item The identifier of the module expression.

\item The \verb"TokenInfoMap" updated with the data in the module

expression.

\item The morphism associated to the module expression.

\item The list of sorts parameterized in this module expression.

\item The development graph thus far.

\end{itemize}

{\codesize

\begin{verbatim}

type ModExpProc = (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)

\end{verbatim}

}

\item We distinguish the type of importation statement with the type

\verb"ImportType":

{\codesize

\begin{verbatim}

data ImportType = Pr | Ex | Inc

\end{verbatim}

}

\item When parsing an importation statement we return a tuple containing:

\begin{itemize}

\item The type of importation.

\item The identifier of the module expression imported.

\item The updated map with the information associated with each

module expression.

\item The morphism associated to the module expression.

\item The list of sorts parameterized in this module expression.

\item The updated development graph.

\end{itemize}

{\codesize

\begin{verbatim}

type ImportProc = (ImportType, Token, TokenInfoMap, Morphism, [ParamSort], DGraph)

\end{verbatim}

}

\item When parsing a list of importation statements we return:

\begin{itemize}

\item The list of parameter information: the name of the parameter,

the name of the theory and the sorts not instantiated.

\item The updated \verb"TokenInfoMap" map.

\item The list of morphisms associated with each parameter.

\item The updated development graph.

\end{itemize}

{\codesize

\begin{verbatim}

type ParamInfo = ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph)

\end{verbatim}

}

\item Data about views is kept in a separated way from data about theories

and modules. The \verb"ViewMap" map associates to each view identifier a

tuple with:

\begin{itemize}

\item The identifier of the target node of the view.

\item The morphism generated by the view.

\item A Boolean value indicating whether the target is a theory

(\verb"True") or a module (\verb"False").

\end{itemize}

{\codesize

\begin{verbatim}

type ViewMap = Map.Map Token (Node, Token, Morphism, [Renaming], Bool)

\end{verbatim}

}

\item Finally, we describe the tuple used to return the data structures

updated when a specification or a view is introduced in the development

graph. It contains:

\begin{itemize}

\item The updated \verb"TokenInfoMap".

\item The updated \verb"ViewMap".

\item A list of tokens indicating

\item The new development graph.

\end{itemize}

{\codesize

\begin{verbatim}

type InsSpecRes = (TokenInfoMap, ViewMap, [Token], DGraph)

\end{verbatim}

}

\end{itemize}

The function \verb"insertSpecs" traverses the specifications updating the

data structures and the development graph with \verb"insertSpec":

{\codesize

\begin{verbatim}

insertSpecs :: [Spec] -> TokenInfoMap -> ViewMap -> [Token] -> DGraph -> DGraph

insertSpecs [] _ _ _ dg = dg

insertSpecs (s : ss) tim vm ths dg = insertSpecs ss tim' vm' ths' dg'

where (tim', vm', ths', dg') = insertSpec s tim vm ths dg

\end{verbatim}

}

The behavior of \verb"insertSpec" is different for each type of Maude

specifications. When the introduced specification is a module, the

following actions are performed:

\begin{itemize}

\item The parameters are parsed as follows:

\begin{itemize}

\item The list of parameters declarations is obtained with the auxiliary

function \verb"getParams".

\item These declarations are processed with \verb"processParameters",

that returns a tuple of type \verb"ParamInfo" shown above.

\item Given the parameters names, we traverse the list of sorts to check

if the module defines parameterized sorts with \verb"getSortsParameterizedBy".

\item The links between the theories in the parameters and the current modules

are created with \verb"createEdgesParams".

\end{itemize}

\item The importations are handled as follows:

\begin{itemize}

\item The importation statements are obtained with \verb"getImportsSorts".

Although this function also returns the sorts declared in the module, in

this case they are not needed and its value is ignored.

\item These importations are handled by \verb"processImports", that

returns a list of \verb"ImportProc" containing the information of each

parameter.

\item The definition link generated by the imports are created with

\verb"createEdgesImports".

\end{itemize}

\item The final signature is obtained with \verb"sign_union_morphs"

by merging the signature in the current module with the one obtained

from the morphisms from the parameters and the imports.

\end{itemize}

{\codesize

\begin{verbatim}

insertSpec :: Spec -> TokenInfoMap -> ViewMap -> [Token] -> DGraph -> InsSpecRes

insertSpec (SpecMod sp_mod) tim vm ths dg = (tim4, vm, ths, dg5)

where ps = getParams sp_mod

(pl, tim1, morphs, dg1) = processParameters ps tim dg

top_sg = Maude.Sign.fromSpec sp_mod

paramSorts = getSortsParameterizedBy (paramNames ps)

(Set.toList $ sorts top_sg)

(il, _) = getImportsSorts sp_mod

ips = processImports tim1 vm dg1 il

(tim2, dg2) = last_da ips (tim1, dg1)

sg = sign_union_morphs morphs $ sign_union top_sg ips

ext_sg = makeExtSign Maude sg

nm_sns = map (makeNamed "") $ Maude.Sentence.fromSpec sp_mod

sens = toThSens nm_sns

gt = G_theory Maude ext_sg startSigId sens startThId

tok = HasName.getName sp_mod

name = makeName tok

(ns, dg3) = insGTheory dg2 name DGBasic gt

tim3 = Map.insert tok (getNode ns, sg, [], pl, paramSorts) tim2

(tim4, dg4) = createEdgesImports tok ips sg tim3 dg3

dg5 = createEdgesParams tok pl morphs sg tim4 dg4

\end{verbatim}

}

When the specification inserted is a theory the process varies slightly:

\begin{itemize}

\item Theories cannot be parameterized in Core Maude, so the parameter

handling is not required.

\item The sorts specified have to be qualified with the parameter

name when used in a parameterized module. These sorts are extracted

with \verb"getImportsSorts" and kept in the corresponding field of

\verb"TokenInfoMap".

\end{itemize}

{\codesize

\begin{verbatim}

insertSpec (SpecTh sp_th) tim vm ths dg = (tim3, vm, tok : ths, dg3)

where (il, ss1) = getImportsSorts sp_th

ips = processImports tim vm dg il

ss2 = getThSorts ips

(tim1, dg1) = last_da ips (tim, dg)

sg = sign_union (Maude.Sign.fromSpec sp_th) ips

ext_sg = makeExtSign Maude sg

nm_sns = map (makeNamed "") $ Maude.Sentence.fromSpec sp_th

sens = toThSens nm_sns

gt = G_theory Maude ext_sg startSigId sens startThId

tok = HasName.getName sp_th

name = makeName tok

(ns, dg2) = insGTheory dg1 name DGBasic gt

tim2 = Map.insert tok (getNode ns, sg, ss1 ++ ss2, [], []) tim1

(tim3, dg3) = createEdgesImports tok ips sg tim2 dg2

\end{verbatim}

}

The introduction of views follows the following steps:

\begin{itemize}

\item The function \verb"isInstantiated" checks whether the target of the

view is a theory or a module. This value will be used to decide if the

sorts have to be qualified when this is view is used.

\item A morphism is generated between the signatures of the source and

target specifications.

\item If there is a renaming between terms the function \verb"sign4renamings"

generates the extra signature and sentences needed. These values, kept in

\verb"new_sign" and \verb"new_sens" are used to create an inner node with

the function \verb"insertInnerNode".

\item Finally, a theorem link stating the proof obligations generated by

the view is introduced between the source and the target of the view with

\verb"insertThmEdgeMorphism".

\end{itemize}

{\codesize

\begin{verbatim}

insertSpec (SpecView sp_v) tim vm ths dg = (tim2, vm', ths, dg4)

where View name from to rnms = sp_v

inst = isInstantiated ths to

tok_name = HasName.getName name

(tok1, tim1, morph1, _, dg1) = processModExp tim vm dg from

(tok2, tim2, morph2, _, dg2) = processModExp tim1 vm dg1 to

(n1, _, _, _, _) = fromJust $ Map.lookup tok1 tim2

(n2, _, _, _, _) = fromJust $ Map.lookup tok2 tim2

morph = fromSignsRenamings (target morph1) (target morph2) rnms

morph' = fromJust $ maybeResult $ compose morph1 morph

(new_sign, new_sens) = sign4renamings (target morph1) (sortMap morph) rnms

(n3, dg3) = insertInnerNode n2 (makeName tok2) morph2 new_sign new_sens dg2

vm' = Map.insert (HasName.getName name) (n3, tok2, morph', rnms, inst) vm

dg4 = insertThmEdgeMorphism tok_name n3 n1 morph' dg3

\end{verbatim}

}

Modules expressions are parsed following the guidelines outlined in

Section \ref{subsec:me}:

\begin{itemize}

\item When the module expression is a simple identifier its signature

and its parameterized sorts are extracted from the \verb"TokenInfoMap"

and returned, while the generated morphism is an inclusion:

{\codesize

\begin{verbatim}

processModExp :: TokenInfoMap -> ViewMap -> DGraph -> ModExp -> ModExpProc

processModExp tim _ dg (ModExp modId) = (tok, tim, morph, ps, dg)

where tok = HasName.getName modId

(_, sg, _, _, ps) = fromJust $ Map.lookup tok tim

morph = Maude.Morphism.inclusion sg sg

\end{verbatim}

}

\item The parsing of the summation expression performs the following

steps:

\begin{itemize}

\item The information about the modules expressions is recursively

computed with \verb"processModExp".

\item The signature of the resulting module expression is obtained

with the \verb"union" of signatures.

\item The morphism generated by the summation is just an inclusion.

\item A new node for the summation is introduced with \verb"insertNode".

\item The target signature of the obtained morphisms is substituted

by this new signature with \verb"setTarget".

\item These new morphisms are used to generate the links between the

summation and its summands in \verb"insertDefEdgeMorphism".

\end{itemize}

{\codesize

\begin{verbatim}

processModExp tim vm dg (SummationModExp modExp1 modExp2) = (tok, tim3, morph, ps', dg5)

where (tok1, tim1, morph1, ps1, dg1) = processModExp tim vm dg modExp1

(tok2, tim2, morph2, ps2, dg2) = processModExp tim1 vm dg1 modExp2

ps' = deleteRepeated $ ps1 ++ ps2

tok = mkSimpleId $ concat ["{", show tok1, " + ", show tok2, "}"]

(n1, _, ss1, _, _) = fromJust $ Map.lookup tok1 tim2

(n2, _, ss2, _, _) = fromJust $ Map.lookup tok2 tim2

ss1' = renameSorts morph1 ss1

ss2' = renameSorts morph1 ss2

sg1 = target morph1

sg2 = target morph2

sg = Maude.Sign.union sg1 sg2

morph = Maude.Morphism.inclusion sg sg

morph1' = setTarget sg morph1

morph2' = setTarget sg morph2

(tim3, dg3) = insertNode tok sg tim2 (ss1' ++ ss2') [] dg2

(n3, _, _, _, _) = fromJust $ Map.lookup tok tim3

dg4 = insertDefEdgeMorphism n3 n1 morph1' dg3

dg5 = insertDefEdgeMorphism n3 n2 morph2' dg4

\end{verbatim}

}

\item The renaming module expression recursively parses the inner expression, computes the morphism from the given renamings with \verb"fromSignRenamings",

taking special care of the renaming of the parameterized sorts with

\verb"applyRenamingParamSorts". Finally, the final morphism is obtained

from the composition of the morphism computed for the inner expression and

the one computed from the renamings:

{\codesize

\begin{verbatim}

processModExp tim vm dg (RenamingModExp modExp rnms) = (tok, tim', comp_morph, ps', dg')

where (tok, tim', morph, ps, dg') = processModExp tim vm dg modExp

morph' = fromSignRenamings (target morph) rnms

ps' = applyRenamingParamSorts (sortMap morph') ps

comp_morph = fromJust $ maybeResult $ compose morph morph'

\end{verbatim}

}

\item The parsing of the instantiation module expression works as follows:

\begin{itemize}

\item The information of the instantiated parameterized module is obtained

with \verb"processModExp".

\item The parameter names are obtained by applying \verb"fstTpl", that

extracts the first component of a triple, to the information about the

parameters of the parameterized module.

\item Parameterized sorts are instantiated with \verb"instantiateSorts",

that returns the new parameterized sorts, in case the target of the view

is a theory, and the morphism associated.

\item The view identifiers are processed with \verb"processViews". This

function returns the token identifying the list of views, the morphism

to be applied from the parameterized module, a list of pairs of nodes

and morphisms, indicating the morphism that has to be used in the link

from each view, and a list with the updated information about the

parameters due to the views with theories as target.

\item The morphism return is the inclusion morphism.

\item The links between the targets of the views and the expression

are created with \verb"updateGraphViews".

\end{itemize}

{\codesize

\begin{verbatim}

processModExp tim vm dg (InstantiationModExp modExp views) =

(tok'', tim'', final_morph, new_param_sorts, dg'')

where (tok, tim', morph, paramSorts, dg') = processModExp tim vm dg modExp

(_, _, _, ps, _) = fromJust $ Map.lookup tok tim'

param_names = map fstTpl ps

view_names = map HasName.getName views

(new_param_sorts, ps_morph) =

instantiateSorts param_names view_names vm morph paramSorts

(tok', morph1, ns, deps) =

processViews views (mkSimpleId "") tim' vm ps (ps_morph, [], [])

tok'' = mkSimpleId $ concat [show tok, "{", show tok', "}"]

sg2 = target morph1

final_morph = Maude.Morphism.inclusion sg2 sg2

(tim'', dg'') = if Map.member tok'' tim

then (tim', dg')

else updateGraphViews tok tok'' sg2 morph1 ns tim' deps dg'

\end{verbatim}

}

\end{itemize}

We present the function \verb"insertNode" to describe how nodes are

introduced in the development graph; the rest of functions that insert

nodes in the graph work in an analogous way. This function receives the

identifier of the node, its signature\footnote{Note that when this

function is used there are no sentences a }, the \verb"TokenInfoMap" map,

a list of sorts, and information about the parameters and

returns the updated map and graph. First, it checks if

the node is already in the development graph. If it is in the graph,

the current map and graph are returned, while in other case the extended

signature is

the current development graph and checks if the node is necessary (the

morphism is not an identity and there is at least one sentence). In that

case, the sentences are made named with \verb"makeNamed" and transformed

into theory sentences with \verb"toThSens", the signature is extended with

\verb"makeExtSign"; the sentences and the signature obtained in this way

are used to create a Hets theory that is introduced in the development

graph with \verb"insGTheory", a function that returns the new node signature

and the updated development graph. Finally, a

{\codesize

\begin{verbatim}

insertNode :: Token -> Sign -> TokenInfoMap -> Symbols -> [(Token, Token, Symbols)]

-> DGraph -> (TokenInfoMap, DGraph)

insertNode tok sg tim ss deps dg = if Map.member tok tim

then (tim, dg)

else let

ext_sg = makeExtSign Maude sg

gt = G_theory Maude ext_sg startSigId noSens startThId

name = makeName tok

(ns, dg') = insGTheory dg name DGBasic gt

tim' = Map.insert tok (getNode ns, sg, ss, deps, []) tim

in (tim', dg')

\end{verbatim}

}

The function

{\codesize

\begin{verbatim}

insertDefEdgeMorphism :: Node -> Node -> Morphism -> DGraph -> DGraph

insertDefEdgeMorphism n1 n2 morph dg = insEdgeDG (n2, n1, edg) dg

where mor = G_morphism Maude morph startMorId

edg = DGLink (gEmbed mor) globalDef SeeTarget $ getNewEdgeId dg

\end{verbatim}

}