content: {- |
  Module      :  ./Maude/Maude2DG.hs
  Description :  Maude Development Graphs
  Copyright   :  (c) Adrian Riesco, Facultad de Informatica UCM 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  ariesco@fdi.ucm.es
  Stability   :  experimental
  Portability :  portable
  
  Conversion of Maude to Development Graphs.
  -}
  
  module Maude.Maude2DG (anaMaudeFile) where
  
  import System.Exit
  import System.IO
  import System.Process
  
  import Static.GTheory
  import Static.DevGraph
  import Static.DgUtils
  import Static.ComputeTheory
  import Static.AnalysisStructured
  
  import Logic.Logic
  import Logic.Prover
  import Logic.ExtSign
  import Logic.Comorphism
  import Logic.Grothendieck
  
  import Maude.Sign
  import Maude.Symbol
  import Maude.AS_Maude
  import Maude.Sentence
  import Maude.Morphism
  import Maude.Language
  import Maude.Shellout
  import Maude.Logic_Maude
  import qualified Maude.Meta.HasName as HasName
  
  import Data.Char
  import Data.Maybe
  import Data.List (intersect)
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import Data.Graph.Inductive.Graph
  
  import Common.Consistency
  import Common.ExtSign
  import Common.Id
  import Common.IRI (simpleIdToIRI)
  import Common.Result
  import Common.LibName
  import Common.AS_Annotation
  import Common.Utils
  
  import Driver.Options
  
  -- | Maude importation types: Protecting, Extending and Including
  data ImportType = Pr | Ex | Inc
  
  {- | Pair of tokens and parameters contained by the token.
  For example, (List{X,Y}, [X,Y]) -}
  type ParamSort = (Symbol, [Token])
  
  {- | Tuple with information about a module expression:
  The corresponding node in the development graph.
  The signature in this node.
  The sorts not bound yet, defined in theories.
  The data from parameters: the parameter id, its module expression and
  the list of sorts imported.
  The list of sorts "parameterized" (of the form List{X}). -}
  type ProcInfo = (Node, Sign, Symbols, [(Token, Token, Symbols)], [ParamSort])
  
  -- | map from module expression identifiers to ProcInfo
  type TokenInfoMap = Map.Map Token ProcInfo
  
  getProcInfo :: Token -> TokenInfoMap -> ProcInfo
  getProcInfo t m = Map.findWithDefault
    (error $ "Maude2DG.TokenInfo: " ++ show t ++ " not found in "
     ++ show (Map.keys m)) t m
  
  tokenNode :: Token -> TokenInfoMap -> Node
  tokenNode t m = n where
    (n, _, _, _, _) = getProcInfo t m
  
  {- | Data structure used to parse module expressions, it keeps:
  The identifier of the module expression.
  The map with the information associated with each module expression.
  The morphism associated to the module expression.
  The list of sorts parameterized in this module expression.
  The development graph thus far. -}
  type ModExpProc = (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
  
  {- | Information related to an importation:
  The type of importation.
  The module expression imported.
  The map with the information associated with each module expression.
  The morphism associated to the module expression.
  The list of sorts parameterized in this module expression.
  The development graph thus far. -}
  type ImportProc =
    (ImportType, Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
  
  {- | Information related to the parameters:
  The list of parameters information:
   (parameter name, theory name, not instantiated sorts)
  The updated TokenInfoMap map.
  The list of morphisms associated with each parameter.
  The updated development graph. -}
  type 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
  all the values -}
  type ViewMap = Map.Map Token (Node, Token, Morphism, [Renaming], Bool)
  
  {- | Tuple of data structures updated when a specification is introduced into
  a development graph -}
  type InsSpecRes = (TokenInfoMap, TokenInfoMap, ViewMap, [Token], DGraph)
  
  {- | Tuple of data structures to introduce in the current DG the predefined
  modules used -}
  type UpdtPredefs = (TokenInfoMap, TokenInfoMap, DGraph)
  
  {- | inserts the list of specifications in the development graph, updating
  the data structures -}
  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
  the data structures -}
  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
      ps = getParams sp_mod
      (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
      top_sg = Maude.Sign.fromSpec sp_mod
      paramSorts = getSortsParameterizedBy (paramNames ps)
        $ Set.toList $ sorts top_sg
      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 = maudeTheory ext_sg startSigId sens startThId
      tok = HasName.getName sp_mod
      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
      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 = maudeTheory ext_sg startSigId sens startThId
      tok = HasName.getName sp_th
      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
      tok_name = HasName.getName name
      (tok1, tim1, morph1, _, dg1) = processModExp timUp vm dgUp from
      (tok2, tim2, morph2, _, dg2) = processModExp tim1 vm dg1 to
      n1 = tokenNode tok1 tim2
      n2 = tokenNode tok2 tim2
      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
      vm' = Map.insert (HasName.getName name) (n3, tok2, morph', rnms, inst) vm
      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 [] _ up = up
  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
  in the current DG -}
  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
  in the current DG -}
  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
  incPredImp i up = up'
            where me = getModExp i
                  up' = incPredImpME me up
  
  {- | 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
    ModId q = m_id
    q' = mkFreeName q
    up = if Map.member q ptim then let
           (n, sg1, sys1, tts1, ps1) = ptim Map.! q
           (n', sg2, sys2, tts2, ps2) = ptim Map.! q'
           refInfo = newRefInfo preludeLib n
           refInfo' = newRefInfo preludeLib n'
           ptim1 = Map.delete q ptim
           ptim2 = Map.delete q' ptim1
           ext_sg1 = makeExtSign Maude sg1
           gt1 = maudeTheory ext_sg1 startSigId noSens startThId
           name1 = makeName $ simpleIdToIRI q
           new = newInfoNodeLab name1 refInfo gt1
           newNode = getNewNodeDG dg
           refLab = labDG pdg n
           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
           refLab' = labDG pdg n'
           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
           in (ptim2, tim2, dg2)
         else (ptim, tim, dg)
  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
  sign_union = foldr (Maude.Sign.union . get_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
  sign_union_morphs morphs sg = foldr (Maude.Sign.union . target) sg morphs
  
  {- | 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
  last_da _ p = 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
    n1 = tokenNode tok1 tim
    n2 = tokenNode tok2 tim
  
  -- | 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
          _ -> (tok2, tim, dg)
    in (tim', createEdgeMorphism tok1 tok2'
        (case ip of
           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
  views -}
  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 [] []
                 new_sg = Maude.Sign.union sg' sg''
  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
  newOp sg op ss sm = Maude.Sign.empty {ops = Map.singleton op ods'}
           where om = ops sg
                 Just ods = Map.lookup op om
                 ods' = getOpDeclSet ods ss sm
  
  -- | renames the profile with the given map
  getOpDeclSet :: OpDeclSet -> Symbols -> SymbolMap -> OpDeclSet
  getOpDeclSet ods ss sm = Set.singleton (op_sym', ats)
           where f ~(Operator _ x _) b = x == ss || b
                 g = Set.fold f False . fst
                 (ods', ats) : _ = Set.toList $ Set.filter g ods
                 h ~(Operator _ y _) = y == ss
                 ods'' = Set.filter h ods'
                 op_sym : _ = Set.toList ods''
                 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'
           where f x = Map.findWithDefault x x sm
                 ar' = map f ar
                 co' = f co
  applyRenamingOpSymbol _ _ = Set.empty
  
  -- | 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
  
  -- | renames a type
  applyRenamingType :: SymbolMap -> Type -> Type
  applyRenamingType sm (TypeSort s) = TypeSort $ SortId $ HasName.getName q'
           where SortId q = s
                 q' = Map.findWithDefault (Sort q) (Sort q) sm
  applyRenamingType sm (TypeKind k) = TypeKind $ KindId $ HasName.getName q'
           where KindId q = k
                 q' = Map.findWithDefault (Kind q) (Kind q) sm
  
  {- | 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
  getTypes _ = []
  
  -- | 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
  the type of import -}
  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') =
                     processModExp tim Map.empty dg modExp
                 (_, _, fs, _, _) = getProcInfo tok tim'
                 fs' = translateSorts morph fs
                 morph' = qualifySorts morph (HasName.getName sort) fs'
                 toks' = (HasName.getName sort, tok, fs') : toks
                 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)
                       where tok = HasName.getName modId
                             (_, sg, _, _, ps) = getProcInfo tok tim
                             morph = Maude.Morphism.inclusion sg sg
  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
      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 = tokenNode tok tim3
      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
      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'
  
  {- | 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
                             n2 = tokenNode tok2 tim'
                             dg'' = insertDefEdgeMorphism n2 n1 morph' dg'
                             dg''' = insertDefEdgesMorphism n2 views sg dg''
  
  {- | traverses a list of views obtained in an instantiation module expression
  and return a tuple with:
  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
  development graph.
  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 =
    if Map.member name vm
    then morphismView name p ss (Map.findWithDefault
           (error "Maude2DG.processView") name vm) morph
    else paramBinding theory name p ss morph tim
      where name = HasName.getName vi
  
  {- | 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'
                tgt = target vmorph
                vmorph' = Maude.Morphism.inclusion tgt tgt
                ctgt = target morph'
                usg = Maude.Sign.union ctgt tgt
                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''
                tgt = target morph
                vmorph = Maude.Morphism.inclusion tgt tgt
                vmorph' = applyRenamings vmorph rnms''
                vtgt = target vmorph'
                ctgt = target morph3
                usg = Maude.Sign.union vtgt ctgt
                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
                vmorph = Maude.Morphism.inclusion sg sg
                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 =
    if Map.member tok tim then (tim, dg) else let
      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
    in (tim', dg')
  
  {- | 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
    then let
      (fn, tim', dg') = insertFreeNode tok tim [] dg
      n2 = tokenNode fn tim'
      in (n2, tim', dg')
    else let
      nm = makeName $ simpleIdToIRI tok
      th_sens = toThSens $ map (makeNamed "") sens
      sg' = Maude.Sign.union sg $ target morph
      ext_sg = makeExtSign Maude sg'
      gt = maudeTheory ext_sg startSigId th_sens startThId
      nm' = inc nm
      (ns, dg1) = insGTheory dg nm' DGBasic gt
      nod2 = getNode ns
      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
      nod3 = getNode ns2
      -- inserting the free link
      inc_sg = Maude.Morphism.inclusion Maude.Sign.empty sg'
      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
      in (nod3, tim, dg4)
  
  {- | 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)
    (Maude.Morphism.inclusion Maude.Sign.empty sg2)
      -- 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
    -> DGraph
  insertFreeEdgeMor tok1 tok2 tim mor dg = snd $ insLEdgeDG (n2, n1, edg) dg
      where n1 = tokenNode tok1 tim
            n2 = tokenNode tok2 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
  exist -}
  insertFreeNode :: Token -> TokenInfoMap -> [Morphism] -> DGraph
    -> (Token, TokenInfoMap, DGraph)
  insertFreeNode t tim morphs dg = (t', tim', dg'') where
      t' = mkFreeName t
      b = Map.member t' tim
      (tim', dg') = if b then (tim, dg) else
        insertFreeNode2 t' tim (getProcInfo t tim) dg
      dg'' | b = dg'
           | null morphs = insertFreeEdge t' t tim' dg'
           | otherwise = insertFreeEdgeMor t' t tim' (morphismUnion morphs) dg'
  
  morphismUnion :: [Morphism] -> Morphism
  morphismUnion = foldr Maude.Morphism.union Maude.Morphism.empty
  
  -- | 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)
    -> ([Import], Symbols)
  getImportsSortsStmnts [] p = p
  getImportsSortsStmnts (ImportStmnt imp : stmts) (is, ss) =
      getImportsSortsStmnts stmts (imp : is, ss)
  getImportsSortsStmnts (SortStmnt s : stmts) (is, ss) =
      getImportsSortsStmnts stmts (is, Sort (HasName.getName s) : 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
      ns <- parse fp
      let ns' = either (const []) id ns
      (inString, hIn, hOut, hErr, procH) <- runMaude
      exitCode <- getProcessExitCode procH
      case exitCode of
        Nothing -> do
                maudePutStrLn hIn $ "load " ++ fp
                maudePutStrLn hIn inString
                psps <- predefinedSpecs opts hIn hOut
                sps <- traverseSpecs opts hIn hOut ns'
                (ok, errs) <- getErrors hErr
                terminateProcess procH
                if ok
                    then return $ maude2DG psps sps
                    else error errs
        Just ExitSuccess -> error "maude terminated immediately"
        Just (ExitFailure i) ->
            error $ "calling maude failed with exitCode: " ++ show i
  
  maude2DG :: [Spec] -> [Spec] -> (DGraph, DGraph)
  maude2DG psps sps = (dg1, dg2) where
    (_, tim, vm, tks, dg1) =
      insertSpecs psps emptyDG Map.empty Map.empty Map.empty [] emptyDG
    (_, _, _, _, dg2) = insertSpecs sps dg1 tim Map.empty vm tks emptyDG
  
  -- | list of names of the predefined modules
  predefined :: [NamedSpec]
  predefined =
    [ ModName "TRUTH-VALUE"
    , ModName "BOOL-OPS"
    , ModName "TRUTH"
    , ModName "BOOL"
    , ModName "EXT-BOOL"
    , ModName "NAT"
    , ModName "INT"
    , ModName "RAT"
    , ModName "FLOAT"
    , ModName "STRING"
    , ModName "CONVERSION"
    , ModName "RANDOM"
    , ModName "QID"
    , ModName "TRIV"
    , ViewName "TRIV"
    , ViewName "Bool"
    , ViewName "Nat"
    , ViewName "Int"
    , ViewName "Rat"
    , ViewName "Float"
    , ViewName "String"
    , ViewName "Qid"
    , ModName "STRICT-WEAK-ORDER"
    , ViewName "STRICT-WEAK-ORDER"
    , ModName "STRICT-TOTAL-ORDER"
    , ViewName "STRICT-TOTAL-ORDER"
    , ViewName "Nat<"
    , ViewName "Int<"
    , ViewName "Rat<"
    , ViewName "Float<"
    , ViewName "String<"
    , ModName "TOTAL-PREORDER"
    , ViewName "TOTAL-PREORDER"
    , ModName "TOTAL-ORDER"
    , ViewName "TOTAL-ORDER"
    , ViewName "Nat<="
    , ViewName "Int<="
    , ViewName "Rat<="
    , ViewName "Float<="
    , ViewName "String<="
    , ModName "DEFAULT"
    , ViewName "DEFAULT"
    , ViewName "Nat0"
    , ViewName "Int0"
    , ViewName "Rat0"
    , ViewName "Float0"
    , ViewName "String0"
    , ViewName "Qid0"
    , ModName "LIST"
    , ModName "WEAKLY-SORTABLE-LIST"
    , ModName "SORTABLE-LIST"
    , ModName "WEAKLY-SORTABLE-LIST'"
    , ModName "SORTABLE-LIST'"
    , ModName "SET"
    , ModName "LIST-AND-SET"
    , ModName "SORTABLE-LIST-AND-SET"
    , ModName "SORTABLE-LIST-AND-SET'"
    , ModName "LIST*"
    , ModName "SET*"
    , ModName "MAP"
    , ModName "ARRAY"
    , ModName "NAT-LIST"
    , ModName "QID-LIST"
    , ModName "QID-SET"
    , ModName "META-TERM"
    , ModName "META-MODULE"
    , ModName "META-VIEW"
    , ModName "META-LEVEL"
    , ModName "COUNTER"
    , ModName "LOOP-MODE"
    , 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
    let args = case ns of
            ModName n -> "(hets " ++ n
            ViewName n -> "(hetsView " ++ n
          ++ " .)"
    putIfVerbose opts 4 $ "maude input: " ++ args
    maudePutStrLn hIn args
    sOutput <- getAllSpec hOut "" False
    let stringSpec = findSpec sOutput
    case readMaybe stringSpec of
      Nothing -> do
        putStrLn $ "failed to read " ++ args ++ ":\n"
          ++ if all isSpace stringSpec then sOutput else stringSpec
        return Nothing
      ms -> return ms
  
  -- | returns the parameter names
  paramNames :: [Parameter] -> [Token]
  paramNames = map $ \ (Parameter s _) -> HasName.getName s
  
  {- | 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
                   g pss x = let
                           params = getSortParams $ HasName.getName x
                           in (x, intersect params pss)
  
  {- | extracts the parameters of the given sort
  For example, getSortParams List{X} = [X]
  List{X}{Y, Y} = [Y,Z] -}
  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 ""
                                   else sps
              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 (ModExp modExp) = notElem (HasName.getName modExp) ths
  isInstantiated ths (SummationModExp me1 me2) = isInstantiated ths me1 &&
                                                 isInstantiated ths me2
  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
  fstTpl :: (a, b, c) -> a
  fstTpl (a, _, _) = a
  
  {- | 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
                   param' = if inst
                            then []
                            else [param]
                  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]
  
  {- | instantiate a sort
  Params: Parameterized sort -> Parameter to be replaced -> New name of the
  parameter -}
  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
                             then view
                             else acc
  instantiateSortStringAux ('`' : '}' : _) param view acc = value ++ "`}"
               where value = if acc == param
                             then view
                             else acc
  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)
        (qualifyType p co) to
      SortRenaming from to -> SortRenaming (qualifySort p from) to
      _ -> rnm
  
  -- | 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)
        (qualifyType p co) to
      SortRenaming from to -> SortRenaming
        (qualifySort p from) (qualifySort p to)
      _ -> rnm
  
  {- | 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
                  True -> []
                  False -> rnm : createQualifiedSortRenaming old new ss
                               where rnm = SortRenaming (qualifiedSort old' s')
                                                        (qualifiedSort new' s')
          where old' = HasName.getName old
                new' = HasName.getName new
                s' = HasName.getName 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
  qualifyType _ ty = ty
  
  {- | 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
          where par' = HasName.getName par
                s' = HasName.getName s
                rnm = SortRenaming (SortId s') (qualifiedSort par' s')
  
  -- | Library name for Maude prelude
  preludeLib :: LibName
  preludeLib = emptyLibName "Maude_Prelude"
  
  {- | generates the library and the development graph from the path of the
  maude file -}
  anaMaudeFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
  anaMaudeFile opts file = do
      (dg1, dg2) <- directMaudeParsing opts file
      let ln = emptyLibName file
          lib1 = Map.singleton preludeLib $
                   computeDGraphTheories Map.empty ln $ markFree Map.empty $
                   markHiding Map.empty dg1
          lib2 = Map.insert ln
                   (computeDGraphTheories lib1 ln $ markFree lib1 $
                   markHiding lib1 dg2) lib1
      return $ Just (ln, lib2)
  