0N/ADescription : Maude Development Graphs
0N/ACopyright : (c) Adrian Riesco, Facultad de Informatica UCM 2009
0N/AMaintainer : ariesco@fdi.ucm.es
0N/AStability : experimental
0N/APortability : portable
0N/AConversion of Maude to Development Graphs.
0N/A-- | Maude importation types: Protecting, Extending and Including
0N/Adata ImportType = Pr | Ex | Inc
1178N/A{- | Pair of tokens and parameters contained by the token.
1178N/AFor example, (List{X,Y}, [X,Y]) -}
0N/Atype ParamSort = (Symbol, [Token])
0N/A{- | Tuple with information about a module expression:
1178N/AThe corresponding node in the development graph.
0N/AThe signature in this node.
1178N/AThe sorts not bound yet, defined in theories.
0N/AThe data from parameters: the parameter id, its module expression and
0N/Athe list of sorts imported.
1178N/AThe list of sorts "parameterized" (of the form List{X}). -}
0N/Atype ProcInfo = (Node, Sign, Symbols, [(Token, Token, Symbols)], [ParamSort])
1178N/A-- | map from module expression identifiers to ProcInfo
0N/AgetProcInfo :: Token -> TokenInfoMap -> ProcInfo
0N/AtokenNode :: Token -> TokenInfoMap -> Node
0N/AtokenNode t m = n where
0N/A (n, _, _, _, _) = getProcInfo t m
1178N/A{- | Data structure used to parse module expressions, it keeps:
0N/AThe identifier of the module expression.
0N/AThe map with the information associated with each module expression.
1178N/AThe morphism associated to the module expression.
0N/AThe list of sorts parameterized in this module expression.
0N/AThe development graph thus far. -}
1178N/Atype ModExpProc = (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
0N/A{- | Information related to an importation:
0N/AThe module expression imported.
0N/AThe map with the information associated with each module expression.
1178N/AThe morphism associated to the module expression.
0N/AThe list of sorts parameterized in this module expression.
0N/AThe development graph thus far. -}
0N/A (ImportType, Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
0N/A{- | Information related to the parameters:
0N/AThe list of parameters information:
1178N/A (parameter name, theory name, not instantiated sorts)
1178N/AThe updated TokenInfoMap map.
0N/AThe list of morphisms associated with each parameter.
0N/AThe updated development graph. -}
0N/Atype ParamInfo = ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph)
{- | Map from view identifiers to tuples containing the target node of the
view, the morphism, and a Boolean value indicating if the view instantiates
type ViewMap =
Map.Map Token (Node, Token, Morphism, [Renaming], Bool)
{- | Tuple of data structures updated when a specification is introduced into
type InsSpecRes = (TokenInfoMap, TokenInfoMap, ViewMap, [Token], DGraph)
{- | Tuple of data structures to introduce in the current DG the predefined
type UpdtPredefs = (TokenInfoMap, TokenInfoMap, DGraph)
{- | inserts the list of specifications in the development graph, updating
insertSpecs :: [Spec] -> DGraph -> TokenInfoMap -> TokenInfoMap -> ViewMap
-> [Token] -> DGraph -> InsSpecRes
insertSpecs [] _ ptim tim vm tks dg = (ptim, tim, vm, tks, dg)
insertSpecs (s : ss) pdg ptim tim vm ths dg =
insertSpecs ss pdg ptim' tim' vm' ths' dg'
where (ptim', tim', vm', ths', dg') = insertSpec s pdg ptim tim vm ths dg
maudeTheory :: ExtSign Sign Symbol -> SigId
-> ThSens Sentence (AnyComorphism, BasicProof) -> ThId -> G_theory
maudeTheory = G_theory Maude Nothing
{- | inserts the given specification in the development graph, updating
insertSpec :: Spec -> DGraph -> TokenInfoMap -> TokenInfoMap -> ViewMap
-> [Token] -> DGraph -> InsSpecRes
insertSpec (SpecMod sp_mod) pdg ptim tim vm ths dg =
(ptimUp, tim5, vm, ths, dg6) where
(il, _) = getImportsSorts sp_mod
up = incPredImps il pdg (ptim, tim, dg)
(ptimUp, timUp, dgUp) = incPredParams ps pdg up
(pl, tim1, morphs, dg1) = processParameters ps timUp dgUp
paramSorts = getSortsParameterizedBy (paramNames ps)
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
gt = maudeTheory ext_sg startSigId sens startThId
name = makeName $ simpleIdToIRI 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
(_, tim5, dg6) = insertFreeNode tok tim4 morphs dg5
insertSpec (SpecTh sp_th) pdg ptim tim vm ths dg =
(ptimUp, tim3, vm, tok : ths, dg3) where
(il, ss1) = getImportsSorts sp_th
(ptimUp, timUp, dgUp) = incPredImps il pdg (ptim, tim, dg)
ips = processImports timUp vm dgUp il
(tim1, dg1) = last_da ips (tim, dg)
ext_sg = makeExtSign Maude sg
gt = maudeTheory ext_sg startSigId sens startThId
name = makeName $ simpleIdToIRI 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
-- (_, tim4, dg4) = insertFreeNode tok tim3 [] dg3
insertSpec (SpecView sp_v) pdg ptim tim vm ths dg =
(ptimUp, tim3, vm', ths, dg4) where
View name from to rnms = sp_v
(ptimUp, timUp, dgUp) = incPredView from to pdg (ptim, tim, dg)
inst = isInstantiated ths to
(tok1, tim1, morph1, _, dg1) = processModExp timUp vm dgUp from
(tok2, tim2, morph2, _, dg2) = processModExp tim1 vm dg1 to
morph = fromSignsRenamings (target morph1) (target morph2) rnms
Just morph' = maybeResult $ compose morph1 morph
(new_sign, new_sens) = sign4renamings (target morph1) (sortMap morph) rnms
(n3, tim3, dg3) = insertInnerNode n2 tim2 tok2 morph2 new_sign new_sens dg2
dg4 = insertThmEdgeMorphism tok_name n3 n1 morph' dg3
{- | Includes the references used in importations to modules in the maude
prelude in the current DG -}
incPredImps :: [Import] -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImps (i : is) pdg up = incPredImps is pdg up'
where up' = incPredImp i pdg up
{- | Includes the references used in parameterizations to modules in the maude
prelude in the current DG -}
incPredParams :: [Parameter] -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredParams [] _ up = up
incPredParams (i : is) pdg up = incPredParams is pdg up'
where up' = incPredParam i pdg up
{- | Includes the references used in views to modules in the maude prelude
incPredView :: ModExp -> ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredView from to pdg up = up''
where up' = incPredImpME from pdg up
up'' = incPredImpME to pdg up'
{- | Includes the references used in a parameter to modules in the maude prelude
incPredParam :: Parameter -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredParam (Parameter _ me) = incPredImpME me
{- | Includes the references used in an importation to modules in the maude
prelude in the current DG -}
incPredImp :: Import -> DGraph -> UpdtPredefs -> UpdtPredefs
{- | Includes the references used in a module expression to modules in the
maude prelude in the current DG -}
incPredImpME :: ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImpME (ModExp m_id) pdg (ptim, tim, dg) = up where
(n, sg1, sys1, tts1, ps1) = ptim Map.! q
(n', sg2, sys2, tts2, ps2) = ptim Map.! q'
refInfo = newRefInfo preludeLib n
refInfo' = newRefInfo preludeLib n'
ext_sg1 = makeExtSign Maude sg1
gt1 = maudeTheory ext_sg1 startSigId noSens startThId
name1 = makeName $ simpleIdToIRI q
new = newInfoNodeLab name1 refInfo gt1
newNode = getNewNodeDG dg
nodeCont = new { globalTheory = globalTheory refLab }
-- (ns1, dg1) = insGTheory dg name1 DGBasic gt1
dg1 = insNodeDG (newNode, nodeCont) dg
ext_sg2 = makeExtSign Maude sg2
gt2 = maudeTheory ext_sg2 startSigId noSens startThId
name2 = makeName $ simpleIdToIRI q'
new' = newInfoNodeLab name2 refInfo' gt2
newNode' = getNewNodeDG dg1
nodeCont' = new' { globalTheory = globalTheory refLab' }
-- (ns2, dg2) = insGTheory dg1 name2 DGBasic gt2
dg2 = insNodeDG (newNode', nodeCont') dg1
tim1 =
Map.insert q (newNode, sg1, sys1, tts1, ps1) tim
tim2 =
Map.insert q' (newNode', sg2, sys2, tts2, ps2) tim1
incPredImpME (SummationModExp me me') pdg up = up''
where up' = incPredImpME me pdg up
up'' = incPredImpME me' pdg up'
incPredImpME (RenamingModExp me _) pdg up = incPredImpME me pdg up
incPredImpME (InstantiationModExp me _) pdg up = incPredImpME me pdg up
-- | extracts the module expression from an importation statement
getModExp :: Import -> ModExp
getModExp (Including me) = me
getModExp (Extending me) = me
getModExp (Protecting me) = me
-- | computes the union of the signatures obtained from the importation list
sign_union :: Sign -> [ImportProc] -> Sign
-- | extracts the target signature from the morphism in an importation tuple
get_sign :: ImportProc -> Sign
get_sign (_, _, _, morph, _, _) = target morph
-- | computes the union of the target signatures of a list of morphisms
sign_union_morphs :: [Morphism] -> Sign -> Sign
{- | extracts the last (newest) data structures from a list of importation
tuples, using the second argument as default value if the list is empty -}
last_da :: [ImportProc] -> (TokenInfoMap, DGraph) -> (TokenInfoMap, DGraph)
last_da [(_, _, tim, _, _, dg)] _ = (tim, dg)
last_da (_ : ips) p = last_da ips p
-- | generates the edges required by a parameter list in a module instantiation
createEdgesParams :: Token -> [(Token, Token, Symbols)] -> [Morphism] -> Sign
-> TokenInfoMap -> DGraph -> DGraph
createEdgesParams tok1 ((_, tok2, _) : toks) (morph : morphs) sg tim dg =
createEdgesParams tok1 toks morphs sg tim
$ createEdgeMorphism tok1 tok2 globalDef morph sg tim dg
createEdgesParams _ _ _ _ _ dg = dg
createEdgeMorphism :: Token -> Token -> DGLinkType -> Morphism -> Sign
-> TokenInfoMap -> DGraph -> DGraph
createEdgeMorphism tok1 tok2 lt morph sg tim =
insertEdgeMorphism n1 n2 lt morph' where
morph' = setTarget sg morph
-- | generates the edges required by the importations
createEdgesImports :: Token -> [ImportProc] -> Sign -> TokenInfoMap -> DGraph
-> (TokenInfoMap, DGraph)
createEdgesImports _ [] _ tim dg = (tim, dg)
createEdgesImports tok (ip : ips) sg tim dg =
createEdgesImports tok ips sg tim' dg'
where (tim', dg') = createEdgeImport tok ip sg tim dg
-- | generates the edge for a concrete importation
createEdgeImport :: Token -> ImportProc -> Sign -> TokenInfoMap -> DGraph
-> (TokenInfoMap, DGraph)
createEdgeImport tok1 (ip, tok2, _, morph, _, _) sg tim dg =
let (tok2', tim', dg') = case ip of
Pr -> insertFreeNode tok2 tim [] dg
in (tim', createEdgeMorphism tok1 tok2'
Ex -> globalConsThm PCons -- a PCons link
_ -> globalDef) morph sg tim' dg')
-- | extracts the sorts provided by the theories
getThSorts :: [ImportProc] -> Symbols
getThSorts = concatMap getThSortsAux
-- | extracts the not-bounded-yet sorts related to the given identifier
getThSortsAux :: ImportProc -> Symbols
getThSortsAux (_, tok, tim, _, _, _) = srts
where (_, _, srts, _, _) = getProcInfo tok tim
{- | generates the extra signature needed when using term to term renaming in
sign4renamings :: Sign -> SymbolMap -> [Renaming] -> (Sign, [Sentence])
sign4renamings sg sm (TermMap t1 t2 : rnms) = (new_sg, Equation eq : sens)
where (op_top, ss) = getOpSorts t1
sg' = newOp sg op_top ss sm
(sg'', sens) = sign4renamings sg sm rnms
eq = Eq (applyRenamingTerm sm t1) t2 [] []
sign4renamings sg sm (_ : rnms) = sign4renamings sg sm rnms
sign4renamings sg _ [] = (sg, [])
{- | given the identifier of an operator in the given signature, the function
generates a new signature with this operator and a renamed profile computed
from the renaming given in the mapping -}
newOp :: Sign -> Token -> Symbols -> SymbolMap -> Sign
ods' = getOpDeclSet ods ss sm
-- | renames the profile with the given map
getOpDeclSet :: OpDeclSet -> Symbols -> SymbolMap -> OpDeclSet
where f ~(Operator _ x _) b = x == ss || b
h ~(Operator _ y _) = y == ss
op_sym' = applyRenamingOpSymbol op_sym sm
-- | applies the renaming in the map to the operator declaration
applyRenamingOpSymbol :: Symbol -> SymbolMap -> SymbolSet
applyRenamingOpSymbol (Operator q ar co) sm =
Set.singleton $ Operator q ar' co'
-- | renames the sorts in a term
applyRenamingTerm :: SymbolMap -> Term -> Term
applyRenamingTerm sm (Apply q ts ty) = Apply q (map (applyRenamingTerm sm) ts)
(applyRenamingType sm ty)
applyRenamingTerm sm (Const q s) = Const q s'
where s' = applyRenamingType sm s
applyRenamingTerm sm (Var q s) = Var q s'
where s' = applyRenamingType sm s
applyRenamingType :: SymbolMap -> Type -> Type
{- | extracts the top operator of a term and the names of its sorts
if it is applicated to some arguments -}
getOpSorts :: Term -> (Token, Symbols)
getOpSorts (Const q _) = (q, [])
getOpSorts (Var q _) = (q, [])
getOpSorts (Apply q ls _) = (q, getTypes ls)
-- | extracts the types of the terms while they are variables
getTypes :: [Term] -> Symbols
getTypes (Var _ (TypeSort s) : ts) = Sort (
HasName.getName s) : getTypes ts
getTypes (Var _ (TypeKind s) : ts) = Kind (
HasName.getName s) : getTypes ts
-- | process the information of the given list of imports
processImports :: TokenInfoMap -> ViewMap -> DGraph -> [Import] -> [ImportProc]
processImports _ _ _ [] = []
processImports tim vm dg (i : il) = ip : processImports tim' vm dg' il
where ip@(_, _, tim', _, _, dg') = processImport tim vm dg i
{- | process the module expression and then adds the information about
processImport :: TokenInfoMap -> ViewMap -> DGraph -> Import -> ImportProc
processImport tim vm dg (Protecting modExp) = (Pr, tok, tim', morph, ps, dg')
where (tok, tim', morph, ps, dg') = processModExp tim vm dg modExp
processImport tim vm dg (Extending modExp) = (Ex, tok, tim', morph, ps, dg')
where (tok, tim', morph, ps, dg') = processModExp tim vm dg modExp
processImport tim vm dg (Including modExp) = (Inc, tok, tim', morph, ps, dg')
where (tok, tim', morph, ps, dg') = processModExp tim vm dg modExp
-- | traverses the list of parameters and generates the required data structures
processParameters :: [Parameter] -> TokenInfoMap -> DGraph -> ParamInfo
processParameters ps tim dg = foldr processParameter ([], tim, [], dg) ps
{- | given a parameter, the function processes the module expression associated
to it, qualifies the not-bound-yet sorts and creates the morphism -}
processParameter :: Parameter -> ParamInfo -> ParamInfo
processParameter (Parameter sort modExp) (toks, tim, morphs, dg) =
(toks', tim', morphs', dg')
where (tok, tim', morph, _, dg') =
(_, _, fs, _, _) = getProcInfo tok tim'
fs' = translateSorts morph fs
morphs' = morph' : morphs
{- | distinguishes between the different module expressions to compute
the morphisms and update the development graph -}
processModExp :: TokenInfoMap -> ViewMap -> DGraph -> ModExp -> ModExpProc
processModExp tim _ dg (ModExp modId) = (tok, tim, morph, ps, dg)
(_, sg, _, _, ps) = getProcInfo tok tim
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' = nubOrd $ ps1 ++ ps2
tok = mkSimpleId $ concat ["{", show tok1, " + ", show tok2, "}"]
(n1, _, ss1, _, _) = getProcInfo tok1 tim2
(n2, _, ss2, _, _) = getProcInfo tok2 tim2
ss1' = translateSorts morph1 ss1
ss2' = translateSorts morph1 ss2
morph1' = setTarget sg morph1
morph2' = setTarget sg morph2
(tim3, dg3) = insertNode tok sg tim2 (ss1' ++ ss2') [] dg2
dg4 = insertDefEdgeMorphism n3 n1 morph1' dg3
dg5 = insertDefEdgeMorphism n3 n2 morph2' dg4
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
Just comp_morph = maybeResult $ compose morph morph'
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, _) = getProcInfo tok tim'
param_names = map fstTpl ps
(new_param_sorts, ps_morph) = instantiateSorts param_names view_names vm
(tok', morph1, ns, deps) = processViews views (mkSimpleId "") tim' vm ps
tok'' = mkSimpleId $ concat [show tok, "{", show tok', "}"]
(tim'', dg'') = if
Map.member tok'' tim then (tim', dg') else
updateGraphViews tok tok'' sg2 morph1 ns tim' deps dg'
{- | generates a edge between the source and the target of a view, inserting
a new node if the view contained a term to term renaming, and thus updating
the map from module expression to its info and the development graph -}
updateGraphViews :: Token -> Token -> Sign -> Morphism -> [(Node, Morphism)]
-> TokenInfoMap -> [(Token, Token, Symbols)] -> DGraph
-> (TokenInfoMap, DGraph)
updateGraphViews tok1 tok2 sg morph views tim deps dg = (tim', dg''')
where n1 = tokenNode tok1 tim
morph' = setTarget sg morph
(tim', dg') = insertNode tok2 sg tim [] deps dg
dg'' = insertDefEdgeMorphism n2 n1 morph' dg'
dg''' = insertDefEdgesMorphism n2 views sg dg''
{- | traverses a list of views obtained in an instantiation module expression
The accumulated identifier of the module expression.
The accumulated morphism thus far.
A list of nodes and morphisms to create the appropriate edges in the
The not-bound-yet sorts. -}
processViews :: [ViewId] -> Token -> TokenInfoMap -> ViewMap
-> [(Token, Token, Symbols)]
-> (Morphism, [(Node, Morphism)], [(Token, Token, Symbols)])
-> (Token, Morphism, [(Node, Morphism)], [(Token, Token, Symbols)])
processViews (vi : vis) tok tim vm (p : ps) (morph, lp, dep) =
processViews vis tok'' tim vm ps (morph', lp ++ [(n, vmorph)], dep ++ new_dep)
where (tok', morph', vmorph, n, new_dep) = processView vi tim vm p morph
tok'' = mkSimpleId $ show tok ++ "," ++ show tok'
processViews _ tok _ _ _ (morph, nds, deps) = (tok', morph, nds, deps)
where tok' = mkSimpleId $ drop 1 $ show tok
{- | this function distinguishes whether the view is an instantiation (and thus)
the view is in the map of views and the function morphismView is used
or it is just a parameter binding and paramBinding is used -}
processView :: ViewId -> TokenInfoMap -> ViewMap -> (Token, Token, Symbols)
-> Morphism -> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
processView vi tim vm (p, theory, ss) morph =
else paramBinding theory name p ss morph tim
{- | the function distinguishes if the instantiation is from a module, and thus
all the symbols are instantiated, or it is a theory and the symbols are not
completely instantiated. -}
morphismView :: Token -> Token -> Symbols
-> (Node, Token, Morphism, [Renaming], Bool) -> Morphism
-> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
morphismView name p _ (n, _, vmorph, rnms, True) morph =
(name, morph'', vmorph', n, [])
where rnms' = qualifyRenamings p rnms
morph' = applyRenamings morph rnms'
morph'' = setTarget usg morph'
morphismView name p ss (n, th, morph, rnms, False) morph1 =
(name, morph4, vmorph', n, [(p, th, translateSorts morph ss)])
where rnms' = qualifyRenamings2 p rnms
morph2 = applyRenamings morph1 rnms'
rnms'' = createQualificationTh2Mod p ss
morph3 = applyRenamings morph2 rnms''
vmorph' = applyRenamings vmorph rnms''
morph4 = setTarget usg morph3
{- this function is applied when two parameters are linked, it updates the
qualifications of the sorts. The parameters are:
theory -> parameter instantiated -> parameter binding -> sorts bound ->
current morph map token info -}
paramBinding :: Token -> Token -> Token -> Symbols -> Morphism -> TokenInfoMap
-> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
paramBinding th view p ss morph tim = (view, morph', vmorph', n, [])
where rnms = createQualifiedSortRenaming p view ss
morph' = applyRenamings morph rnms
(n, sg, _, _, _) = getProcInfo th tim
rnms' = createQualificationTh2Mod p ss
vmorph' = applyRenamings vmorph rnms'
-- | inserts the node into the development graph if it does not already exist
insertNode :: Token -> Sign -> TokenInfoMap -> Symbols
-> [(Token, Token, Symbols)] -> DGraph -> (TokenInfoMap, DGraph)
insertNode tok sg tim ss deps dg =
ext_sg = makeExtSign Maude sg
gt = maudeTheory ext_sg startSigId noSens startThId
name = makeName $ simpleIdToIRI tok
(ns, dg') = insGTheory dg name DGBasic gt
tim' =
Map.insert tok (getNode ns, sg, ss, deps, []) tim
{- | inserts an inner node. This function is used when a view defines a map
between terms, so it is neccesary to extend the signature of the target
module in order to have the appropriate map. -}
insertInnerNode :: Node -> TokenInfoMap -> Token -> Morphism -> Sign
-> [Sentence] -> DGraph -> (Node, TokenInfoMap, DGraph)
insertInnerNode nod tim tok morph sg sens dg =
if isIdentity morph && null sens
(fn, tim', dg') = insertFreeNode tok tim [] dg
nm = makeName $ simpleIdToIRI tok
th_sens = toThSens $ map (makeNamed "") sens
ext_sg = makeExtSign Maude sg'
gt = maudeTheory ext_sg startSigId th_sens startThId
(ns, dg1) = insGTheory dg nm' DGBasic gt
morph' = setTarget sg' morph
dg2 = insertDefEdgeMorphism nod2 nod morph' dg1
-- inserting the free node
gt2 = maudeTheory ext_sg startSigId noSens startThId
(ns2, dg3) = insGTheory dg2 (inc nm') DGBasic gt2
-- inserting the free link
mor = G_morphism Maude inc_sg startMorId
dgt = FreeOrCofreeDefLink NPFree $ EmptyNode (Logic Maude)
edg = defDGLink (gEmbed mor) dgt SeeTarget
dg4 = snd $ insLEdgeDG (nod2, nod3, edg) dg3
{- | inserts the list of definition edges, building for each node the inclusion
morphism between the signatures -}
insertDefEdgesMorphism :: Node -> [(Node, Morphism)] -> Sign -> DGraph -> DGraph
insertDefEdgesMorphism _ [] _ dg = dg
insertDefEdgesMorphism n1 ((n2, morph) : views) sg2 dg =
insertDefEdgesMorphism n1 views sg2 dg'
where morph' = setTarget sg2 morph
dg' = insertDefEdgeMorphism n1 n2 morph' dg
-- | inserts a definition link between the nodes with the given morphism
insertDefEdgeMorphism :: Node -> Node -> Morphism -> DGraph -> DGraph
insertDefEdgeMorphism n1 n2 = insertEdgeMorphism n1 n2 globalDef
{- | inserts a theorem link, labeled with the name of the view, between the
nodes with the given morphism in the development graph -}
insertThmEdgeMorphism :: Token -> Node -> Node -> Morphism -> DGraph -> DGraph
insertThmEdgeMorphism name n1 n2 morph dg = snd $ insLEdgeDG (n2, n1, edg) dg
where mor = G_morphism Maude morph startMorId
edg = defDGLink (gEmbed mor) globalThm
(DGLinkView (simpleIdToIRI name) $ Fitted [])
-- | inserts a link between the nodes with the given morphism
insertEdgeMorphism :: Node -> Node -> DGLinkType -> Morphism -> DGraph -> DGraph
insertEdgeMorphism n1 n2 lt morph dg = snd $ insLEdgeDG (n2, n1, edg) dg
where mor = G_morphism Maude morph startMorId
edg = defDGLink (gEmbed mor) lt SeeTarget
-- | inserts a free definition link between the nodes with the given name
insertFreeEdge :: Token -> Token -> TokenInfoMap -> DGraph -> DGraph
insertFreeEdge tok1 tok2 tim = insertEdgeMorphism n1 n2
(FreeOrCofreeDefLink NPFree $ EmptyNode $ Logic Maude)
-- currently, the empty sign is used in the inclusion instead of sg1
where n1 = tokenNode tok1 tim
(n2, sg2, _, _, _) = getProcInfo tok2 tim
{- | inserts a free definition link between the nodes with the given
name. This function is used to create free links when a module is
parameterized, so the morphism is more complicated: It also receives a
morphism, obtained from the parameters. -}
insertFreeEdgeMor :: Token -> Token -> TokenInfoMap -> Morphism -> DGraph
insertFreeEdgeMor tok1 tok2 tim mor dg = snd $ insLEdgeDG (n2, n1, edg) dg
where n1 = tokenNode tok1 tim
mor' = G_morphism Maude mor startMorId
dgt = FreeOrCofreeDefLink NPFree $ EmptyNode (Logic Maude)
edg = defDGLink (gEmbed mor') dgt SeeTarget
{- | the importation mode "protecting M" generates a new node M' and a free link
between M and M'. This function is in charge of creating such M' if it does not
insertFreeNode :: Token -> TokenInfoMap -> [Morphism] -> DGraph
-> (Token, TokenInfoMap, DGraph)
insertFreeNode t tim morphs dg = (t', tim', dg'') where
(tim', dg') = if b then (tim, dg) else
insertFreeNode2 t' tim (getProcInfo t tim) dg
| null morphs = insertFreeEdge t' t tim' dg'
| otherwise = insertFreeEdgeMor t' t tim' (morphismUnion morphs) dg'
morphismUnion :: [Morphism] -> Morphism
-- | auxiliary function in charge of creating M' when it does not exist
insertFreeNode2 :: Token -> TokenInfoMap -> ProcInfo -> DGraph
-> (TokenInfoMap, DGraph)
insertFreeNode2 t tim (_, sg, _, _, _) dg = (tim', dg')
where ext_sg = makeExtSign Maude sg
gt = maudeTheory ext_sg startSigId noSens startThId
name = makeName $ simpleIdToIRI t
(ns, dg') = insGTheory dg name DGBasic gt
tim' =
Map.insert t (getNode ns, sg, [], [], []) tim
{- | Given the identifier of a module, generates the identifier for the module
with the ``freeness'' constraint -}
mkFreeName :: Token -> Token
mkFreeName = mkSimpleId . (++ "'") . show
-- | extracts the parameters of a Maude module
getParams :: Module -> [Parameter]
getParams (Module _ params _) = params
-- | extracts the importation statements and the sorts from a module definition
getImportsSorts :: Module -> ([Import], Symbols)
getImportsSorts (Module _ _ stmts) = getImportsSortsStmnts stmts ([], [])
-- | traverses the statements accumulating the importations and the sorts
getImportsSortsStmnts :: [Statement] -> ([Import], Symbols)
getImportsSortsStmnts [] p = p
getImportsSortsStmnts (ImportStmnt imp : stmts) (is, ss) =
getImportsSortsStmnts stmts (imp : is, ss)
getImportsSortsStmnts (SortStmnt s : stmts) (is, ss) =
getImportsSortsStmnts (_ : stmts) p = getImportsSortsStmnts stmts p
-- | builds the development graph of the specified Maude file
directMaudeParsing :: HetcatsOpts -> FilePath -> IO (DGraph, DGraph)
directMaudeParsing opts fp = do
putIfVerbose opts 2 $ "Reading file " ++ fp
let ns' = either (const []) id ns
(inString, hIn, hOut, hErr, procH) <- runMaude
exitCode <- getProcessExitCode procH
maudePutStrLn hIn $ "load " ++ fp
maudePutStrLn hIn inString
psps <- predefinedSpecs opts hIn hOut
sps <- traverseSpecs opts hIn hOut ns'
(ok, errs) <- getErrors hErr
then return $ maude2DG psps sps
Just ExitSuccess -> error "maude terminated immediately"
error $ "calling maude failed with exitCode: " ++ show i
maude2DG :: [Spec] -> [Spec] -> (DGraph, DGraph)
maude2DG psps sps = (dg1, dg2) where
(_, _, _, _, dg2) = insertSpecs sps dg1 tim
Map.empty vm tks emptyDG
-- | list of names of the predefined modules
predefined :: [NamedSpec]
, ModName "STRICT-WEAK-ORDER"
, ViewName "STRICT-WEAK-ORDER"
, ModName "STRICT-TOTAL-ORDER"
, ViewName "STRICT-TOTAL-ORDER"
, ModName "TOTAL-PREORDER"
, ViewName "TOTAL-PREORDER"
, ModName "WEAKLY-SORTABLE-LIST"
, ModName "SORTABLE-LIST"
, ModName "WEAKLY-SORTABLE-LIST'"
, ModName "SORTABLE-LIST'"
, ModName "SORTABLE-LIST-AND-SET"
, ModName "SORTABLE-LIST-AND-SET'"
, ModName "CONFIGURATION" ]
{- | returns the specifications of the predefined modules by passing as
parameter the list of names -}
predefinedSpecs :: HetcatsOpts -> Handle -> Handle -> IO [Spec]
predefinedSpecs opts hIn hOut = traverseSpecs opts hIn hOut predefined
traverseSpecs :: HetcatsOpts -> Handle -> Handle -> [NamedSpec] -> IO [Spec]
traverseSpecs opts hIn hOut = fmap catMaybes . mapM (traverseSpec opts hIn hOut)
-- | returns the specifications of the predefined modules
traverseSpec :: HetcatsOpts -> Handle -> Handle -> NamedSpec -> IO (Maybe Spec)
traverseSpec opts hIn hOut ns = do
ModName n -> "(hets " ++ n
ViewName n -> "(hetsView " ++ n
putIfVerbose opts 4 $ "maude input: " ++ args
sOutput <- getAllSpec hOut "" False
let stringSpec = findSpec sOutput
case readMaybe stringSpec of
putStrLn $ "failed to read " ++ args ++ ":\n"
++ if all isSpace stringSpec then sOutput else stringSpec
-- | returns the parameter names
paramNames :: [Parameter] -> [Token]
{- | returns the sorts (second argument of the pair) that contain any of the
parameters given as first argument -}
getSortsParameterizedBy :: [Token] -> Symbols -> [ParamSort]
getSortsParameterizedBy ps = filter f . map (g ps)
where f = not . null . snd
in (x, intersect params pss)
{- | extracts the parameters of the given sort
For example, getSortParams List{X} = [X]
getSortParams :: Token -> [Token]
getSortParams t = getSortParamsString $ show t
-- | traverses a String looking for the last curly braces
getSortParamsString :: String -> [Token]
getSortParamsString [] = []
getSortParamsString ('{' : cs) = if null sps
then getSortParamsStringAux cs ""
where sps = getSortParamsString cs
getSortParamsString (_ : cs) = getSortParamsString cs
-- | traverses a String keeping the token separated by commas
getSortParamsStringAux :: String -> String -> [Token]
getSortParamsStringAux ('`' : ',' : cs) st =
mkSimpleId st : getSortParamsStringAux cs ""
getSortParamsStringAux ('`' : '}' : []) st = [mkSimpleId st]
getSortParamsStringAux (' ' : cs) st = getSortParamsStringAux cs st
getSortParamsStringAux (c : cs) st = getSortParamsStringAux cs (st ++ [c])
getSortParamsStringAux [] st = [mkSimpleId st]
-- | checks if the target of the view is completely instantiated (to modules)
isInstantiated :: [Token] -> ModExp -> Bool
isInstantiated ths (SummationModExp me1 me2) = isInstantiated ths me1 &&
isInstantiated ths (RenamingModExp modExp _) = isInstantiated ths modExp
isInstantiated _ (InstantiationModExp _ _) = True
-- | rename the parameterized sorts and computes if they are still parameterized
applyRenamingParamSorts :: SymbolMap -> [ParamSort] -> [ParamSort]
applyRenamingParamSorts sm = foldr (applyRenamingParamSort sm) []
applyRenamingParamSort :: SymbolMap -> ParamSort -> [ParamSort] -> [ParamSort]
applyRenamingParamSort sm (tok, params) acc = case
Map.lookup tok sm of
Nothing -> (tok, params) : acc
Just tok' -> getSortsParameterizedBy params [tok'] ++ acc
-- | returns the first element from the triple
{- | instantiate the parametric sorts
ParamNames -> ViewName -> Map of views -> Parametricsorts -}
instantiateSorts :: [Token] -> [Token] -> ViewMap -> Morphism -> [ParamSort]
-> ([ParamSort], Morphism)
instantiateSorts _ _ _ morph [] = ([], morph)
instantiateSorts params views vm morph (ps : pss) = (nps'' ++ res_ps, res_morph)
where np4s = newParamers4sorts params views vm
nps = instantiateSort ps params views
nps' = addNewParams2sort nps np4s
nps'' = if null (snd nps') then [] else [nps']
morph' = extendWithSortRenaming (fst ps) (fst nps') morph
(res_ps, res_morph) = instantiateSorts params views vm morph' pss
-- | computes the theories that have to be further instantiated
newParamers4sorts :: [Token] -> [Token] -> ViewMap -> [Token]
newParamers4sorts (param : ps) (view : vs) vm = case
Map.lookup view vm of
Nothing -> newParamers4sorts ps vs vm
Just (_, _, _, _, inst) -> let
in param' ++ newParamers4sorts ps vs vm
newParamers4sorts _ _ _ = []
-- | creates a new parameterized sort
addNewParams2sort :: ParamSort -> [Token] -> ParamSort
addNewParams2sort (Sort tok, _) lps@(_ : _) = (Sort tok', lps) where
tok' = mkSimpleId $ concat [show tok, "`{", printNewParams4sort lps, "`}"]
addNewParams2sort (Kind tok, _) lps@(_ : _) = (Kind tok', lps) where
tok' = mkSimpleId $ concat [show tok, "`{", printNewParams4sort lps, "`}"]
addNewParams2sort (ps, _) _ = (ps, [])
-- | introduces commas between the tokens
printNewParams4sort :: [Token] -> String
printNewParams4sort [] = ""
printNewParams4sort [p] = show p
printNewParams4sort (p : ps) = concat [show p, "`,", printNewParams4sort ps]
Params: Parameterized sort -> Parameter to be replaced -> New name of the
instantiateSort :: ParamSort -> [Token] -> [Token] -> ParamSort
instantiateSort sp@(Sort tok, tok_params) (p : ps) (v : vs) =
if notElem p tok_params then instantiateSort sp ps vs else
let tok' = mkSimpleId $ instantiateSortString (show tok) (show p) (show v)
in instantiateSort (Sort tok', tok_params) ps vs
instantiateSort sp@(Kind tok, tok_params) (p : ps) (v : vs) =
if notElem p tok_params then instantiateSort sp ps vs else
let tok' = mkSimpleId $ instantiateSortString (show tok) (show p) (show v)
in instantiateSort (Kind tok', tok_params) ps vs
instantiateSort ps _ _ = ps
{- | replaces one param by one view in a sort identifier
sort id -> param id -> view id -}
instantiateSortString :: String -> String -> String -> String
instantiateSortString ('{' : cs) param view = '{' : if notElem '{' cs
then instantiateSortStringAux cs param view ""
else instantiateSortString cs param view
instantiateSortString (c : cs) param view =
c : instantiateSortString cs param view
instantiateSortString [] _ _ = ""
{- | replaces one param by one view in the list of parameters
parameters list -> param id -> view id -}
instantiateSortStringAux :: String -> String -> String -> String -> String
instantiateSortStringAux ('`' : ',' : ps) param view acc =
value ++ "`," ++ instantiateSortStringAux ps param view ""
where value = if acc == param
instantiateSortStringAux ('`' : '}' : _) param view acc = value ++ "`}"
where value = if acc == param
instantiateSortStringAux (p : ps) param view acc =
instantiateSortStringAux ps param view (acc ++ [p])
instantiateSortStringAux _ _ _ acc = acc
-- | qualifies the source sorts in the renamigs
qualifyRenamings :: Token -> [Renaming] -> [Renaming]
qualifyRenamings t = map (qualifyRenaming t)
{- | qualifies the source sort in the renaming. Sorts only appear in operator
mappings with profile and sort mappings -}
qualifyRenaming :: Token -> Renaming -> Renaming
qualifyRenaming p rnm = case rnm of
OpRenaming2 from ar co to -> OpRenaming2 from (map (qualifyType p) ar)
SortRenaming from to -> SortRenaming (qualifySort p from) to
-- | qualifies both the source and target sorts in the renamings
qualifyRenamings2 :: Token -> [Renaming] -> [Renaming]
qualifyRenamings2 t = map (qualifyRenaming2 t)
{- | qualifies both the source and target sorts in the renaming.
Sorts only appear in operator mappings with profile and sort mappings -}
qualifyRenaming2 :: Token -> Renaming -> Renaming
qualifyRenaming2 p rnm = case rnm of
OpRenaming2 from ar co to -> OpRenaming2 from (map (qualifyType p) ar)
SortRenaming from to -> SortRenaming
(qualifySort p from) (qualifySort p to)
{- | creates a renaming to substitute the sorts qualified by a parameter name
with a new parameter name due to a parameter binding -}
createQualifiedSortRenaming :: Token -> Token -> Symbols -> [Renaming]
createQualifiedSortRenaming _ _ [] = []
createQualifiedSortRenaming old new (s : ss) = case old == new of
False -> rnm : createQualifiedSortRenaming old new ss
where rnm = SortRenaming (qualifiedSort old' s')
-- | qualifies with the given parameter the token
qualifiedSort :: Token -> Token -> Sort
qualifiedSort param sort =
SortId $ mkSimpleId $ concat [show param, "$", show sort]
-- | qualifies with the given parameter the sort
qualifySort :: Token -> Sort -> Sort
qualifySort p (SortId s) = qualifiedSort p s
-- | qualifies with the given parameter the type
qualifyType :: Token -> Type -> Type
qualifyType p (TypeSort (SortId s)) = TypeSort $ qualifiedSort p s
{- | qualifies the symbols in the theory imported with the parameter name
given as first parameter -}
createQualificationTh2Mod :: Token -> Symbols -> [Renaming]
createQualificationTh2Mod _ [] = []
createQualificationTh2Mod par (s : ss) =
rnm : createQualificationTh2Mod par ss
rnm = SortRenaming (SortId s') (qualifiedSort par' s')
-- | Library name for Maude prelude
preludeLib = emptyLibName "Maude_Prelude"
{- | generates the library and the development graph from the path of the
anaMaudeFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaMaudeFile opts file = do
(dg1, dg2) <- directMaudeParsing opts file
let ln = emptyLibName file
(computeDGraphTheories lib1 $ markFree lib1 $
markHiding lib1 dg2) lib1