{- |
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 :: Token -> TokenInfoMap -> ProcInfo
getProcInfo t :: Token
t m :: TokenInfoMap
m = ProcInfo -> Token -> TokenInfoMap -> ProcInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
  ([Char] -> ProcInfo
forall a. HasCallStack => [Char] -> a
error ([Char] -> ProcInfo) -> [Char] -> ProcInfo
forall a b. (a -> b) -> a -> b
$ "Maude2DG.TokenInfo: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Token -> [Char]
forall a. Show a => a -> [Char]
show Token
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ " not found in "
   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Token] -> [Char]
forall a. Show a => a -> [Char]
show (TokenInfoMap -> [Token]
forall k a. Map k a -> [k]
Map.keys TokenInfoMap
m)) Token
t TokenInfoMap
m

tokenNode :: Token -> TokenInfoMap -> Node
tokenNode :: Token -> TokenInfoMap -> Node
tokenNode t :: Token
t m :: TokenInfoMap
m = Node
n where
  (n :: Node
n, _, _, _, _) = Token -> TokenInfoMap -> ProcInfo
getProcInfo Token
t TokenInfoMap
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 :: [Spec]
-> DGraph
-> TokenInfoMap
-> TokenInfoMap
-> ViewMap
-> [Token]
-> DGraph
-> InsSpecRes
insertSpecs [] _ ptim :: TokenInfoMap
ptim tim :: TokenInfoMap
tim vm :: ViewMap
vm tks :: [Token]
tks dg :: DGraph
dg = (TokenInfoMap
ptim, TokenInfoMap
tim, ViewMap
vm, [Token]
tks, DGraph
dg)
insertSpecs (s :: Spec
s : ss :: [Spec]
ss) pdg :: DGraph
pdg ptim :: TokenInfoMap
ptim tim :: TokenInfoMap
tim vm :: ViewMap
vm ths :: [Token]
ths dg :: DGraph
dg =
  [Spec]
-> DGraph
-> TokenInfoMap
-> TokenInfoMap
-> ViewMap
-> [Token]
-> DGraph
-> InsSpecRes
insertSpecs [Spec]
ss DGraph
pdg TokenInfoMap
ptim' TokenInfoMap
tim' ViewMap
vm' [Token]
ths' DGraph
dg'
  where (ptim' :: TokenInfoMap
ptim', tim' :: TokenInfoMap
tim', vm' :: ViewMap
vm', ths' :: [Token]
ths', dg' :: DGraph
dg') = Spec
-> DGraph
-> TokenInfoMap
-> TokenInfoMap
-> ViewMap
-> [Token]
-> DGraph
-> InsSpecRes
insertSpec Spec
s DGraph
pdg TokenInfoMap
ptim TokenInfoMap
tim ViewMap
vm [Token]
ths DGraph
dg

maudeTheory :: ExtSign Sign Symbol -> SigId
  -> ThSens Sentence (AnyComorphism, BasicProof) -> ThId -> G_theory
maudeTheory :: ExtSign Sign Symbol
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
maudeTheory = Maude
-> Maybe IRI
-> ExtSign Sign Symbol
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory Maude
Maude Maybe IRI
forall a. Maybe a
Nothing

{- | inserts the given specification in the development graph, updating
the data structures -}
insertSpec :: Spec -> DGraph -> TokenInfoMap -> TokenInfoMap -> ViewMap
  -> [Token] -> DGraph -> InsSpecRes
insertSpec :: Spec
-> DGraph
-> TokenInfoMap
-> TokenInfoMap
-> ViewMap
-> [Token]
-> DGraph
-> InsSpecRes
insertSpec (SpecMod sp_mod :: Module
sp_mod) pdg :: DGraph
pdg ptim :: TokenInfoMap
ptim tim :: TokenInfoMap
tim vm :: ViewMap
vm ths :: [Token]
ths dg :: DGraph
dg =
  (TokenInfoMap
ptimUp, TokenInfoMap
tim5, ViewMap
vm, [Token]
ths, DGraph
dg6) where
    ps :: [Parameter]
ps = Module -> [Parameter]
getParams Module
sp_mod
    (il :: [Import]
il, _) = Module -> ([Import], Symbols)
getImportsSorts Module
sp_mod
    up :: UpdtPredefs
up = [Import] -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImps [Import]
il DGraph
pdg (TokenInfoMap
ptim, TokenInfoMap
tim, DGraph
dg)
    (ptimUp :: TokenInfoMap
ptimUp, timUp :: TokenInfoMap
timUp, dgUp :: DGraph
dgUp) = [Parameter] -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredParams [Parameter]
ps DGraph
pdg UpdtPredefs
up
    (pl :: [(Token, Token, Symbols)]
pl, tim1 :: TokenInfoMap
tim1, morphs :: [Morphism]
morphs, dg1 :: DGraph
dg1) = [Parameter]
-> TokenInfoMap
-> DGraph
-> ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph)
processParameters [Parameter]
ps TokenInfoMap
timUp DGraph
dgUp
    top_sg :: Sign
top_sg = Module -> Sign
Maude.Sign.fromSpec Module
sp_mod
    paramSorts :: [ParamSort]
paramSorts = [Token] -> Symbols -> [ParamSort]
getSortsParameterizedBy ([Parameter] -> [Token]
paramNames [Parameter]
ps)
      (Symbols -> [ParamSort]) -> Symbols -> [ParamSort]
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Symbols
forall a. Set a -> [a]
Set.toList (Set Symbol -> Symbols) -> Set Symbol -> Symbols
forall a b. (a -> b) -> a -> b
$ Sign -> Set Symbol
sorts Sign
top_sg
    ips :: [ImportProc]
ips = TokenInfoMap -> ViewMap -> DGraph -> [Import] -> [ImportProc]
processImports TokenInfoMap
tim1 ViewMap
vm DGraph
dg1 [Import]
il
    (tim2 :: TokenInfoMap
tim2, dg2 :: DGraph
dg2) = [ImportProc] -> (TokenInfoMap, DGraph) -> (TokenInfoMap, DGraph)
last_da [ImportProc]
ips (TokenInfoMap
tim1, DGraph
dg1)
    sg :: Sign
sg = [Morphism] -> Sign -> Sign
sign_union_morphs [Morphism]
morphs (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Sign -> [ImportProc] -> Sign
sign_union Sign
top_sg [ImportProc]
ips
    ext_sg :: ExtSign Sign Symbol
ext_sg = Maude -> Sign -> ExtSign Sign Symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign Maude
Maude Sign
sg
    nm_sns :: [SenAttr Sentence [Char]]
nm_sns = (Sentence -> SenAttr Sentence [Char])
-> [Sentence] -> [SenAttr Sentence [Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Sentence -> SenAttr Sentence [Char]
forall a s. a -> s -> SenAttr s a
makeNamed "") ([Sentence] -> [SenAttr Sentence [Char]])
-> [Sentence] -> [SenAttr Sentence [Char]]
forall a b. (a -> b) -> a -> b
$ Module -> [Sentence]
Maude.Sentence.fromSpec Module
sp_mod
    sens :: ThSens Sentence b
sens = [SenAttr Sentence [Char]] -> ThSens Sentence b
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [SenAttr Sentence [Char]]
nm_sns
    gt :: G_theory
gt = ExtSign Sign Symbol
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
maudeTheory ExtSign Sign Symbol
ext_sg SigId
startSigId ThSens Sentence (AnyComorphism, BasicProof)
forall b. ThSens Sentence b
sens ThId
startThId
    tok :: Token
tok = Module -> Token
forall a. HasName a => a -> Token
HasName.getName Module
sp_mod
    name :: NodeName
name = IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$ Token -> IRI
simpleIdToIRI Token
tok
    (ns :: NodeSig
ns, dg3 :: DGraph
dg3) = DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory DGraph
dg2 NodeName
name DGOrigin
DGBasic G_theory
gt
    tim3 :: TokenInfoMap
tim3 = Token -> ProcInfo -> TokenInfoMap -> TokenInfoMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
tok (NodeSig -> Node
getNode NodeSig
ns, Sign
sg, [], [(Token, Token, Symbols)]
pl, [ParamSort]
paramSorts) TokenInfoMap
tim2
    (tim4 :: TokenInfoMap
tim4, dg4 :: DGraph
dg4) = Token
-> [ImportProc]
-> Sign
-> TokenInfoMap
-> DGraph
-> (TokenInfoMap, DGraph)
createEdgesImports Token
tok [ImportProc]
ips Sign
sg TokenInfoMap
tim3 DGraph
dg3
    dg5 :: DGraph
dg5 = Token
-> [(Token, Token, Symbols)]
-> [Morphism]
-> Sign
-> TokenInfoMap
-> DGraph
-> DGraph
createEdgesParams Token
tok [(Token, Token, Symbols)]
pl [Morphism]
morphs Sign
sg TokenInfoMap
tim4 DGraph
dg4
    (_, tim5 :: TokenInfoMap
tim5, dg6 :: DGraph
dg6) = Token
-> TokenInfoMap
-> [Morphism]
-> DGraph
-> (Token, TokenInfoMap, DGraph)
insertFreeNode Token
tok TokenInfoMap
tim4 [Morphism]
morphs DGraph
dg5
insertSpec (SpecTh sp_th :: Module
sp_th) pdg :: DGraph
pdg ptim :: TokenInfoMap
ptim tim :: TokenInfoMap
tim vm :: ViewMap
vm ths :: [Token]
ths dg :: DGraph
dg =
  (TokenInfoMap
ptimUp, TokenInfoMap
tim3, ViewMap
vm, Token
tok Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ths, DGraph
dg3) where
    (il :: [Import]
il, ss1 :: Symbols
ss1) = Module -> ([Import], Symbols)
getImportsSorts Module
sp_th
    (ptimUp :: TokenInfoMap
ptimUp, timUp :: TokenInfoMap
timUp, dgUp :: DGraph
dgUp) = [Import] -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImps [Import]
il DGraph
pdg (TokenInfoMap
ptim, TokenInfoMap
tim, DGraph
dg)
    ips :: [ImportProc]
ips = TokenInfoMap -> ViewMap -> DGraph -> [Import] -> [ImportProc]
processImports TokenInfoMap
timUp ViewMap
vm DGraph
dgUp [Import]
il
    ss2 :: Symbols
ss2 = [ImportProc] -> Symbols
getThSorts [ImportProc]
ips
    (tim1 :: TokenInfoMap
tim1, dg1 :: DGraph
dg1) = [ImportProc] -> (TokenInfoMap, DGraph) -> (TokenInfoMap, DGraph)
last_da [ImportProc]
ips (TokenInfoMap
tim, DGraph
dg)
    sg :: Sign
sg = Sign -> [ImportProc] -> Sign
sign_union (Module -> Sign
Maude.Sign.fromSpec Module
sp_th) [ImportProc]
ips
    ext_sg :: ExtSign Sign Symbol
ext_sg = Maude -> Sign -> ExtSign Sign Symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign Maude
Maude Sign
sg
    nm_sns :: [SenAttr Sentence [Char]]
nm_sns = (Sentence -> SenAttr Sentence [Char])
-> [Sentence] -> [SenAttr Sentence [Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Sentence -> SenAttr Sentence [Char]
forall a s. a -> s -> SenAttr s a
makeNamed "") ([Sentence] -> [SenAttr Sentence [Char]])
-> [Sentence] -> [SenAttr Sentence [Char]]
forall a b. (a -> b) -> a -> b
$ Module -> [Sentence]
Maude.Sentence.fromSpec Module
sp_th
    sens :: ThSens Sentence b
sens = [SenAttr Sentence [Char]] -> ThSens Sentence b
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [SenAttr Sentence [Char]]
nm_sns
    gt :: G_theory
gt = ExtSign Sign Symbol
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
maudeTheory ExtSign Sign Symbol
ext_sg SigId
startSigId ThSens Sentence (AnyComorphism, BasicProof)
forall b. ThSens Sentence b
sens ThId
startThId
    tok :: Token
tok = Module -> Token
forall a. HasName a => a -> Token
HasName.getName Module
sp_th
    name :: NodeName
name = IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$ Token -> IRI
simpleIdToIRI Token
tok
    (ns :: NodeSig
ns, dg2 :: DGraph
dg2) = DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory DGraph
dg1 NodeName
name DGOrigin
DGBasic G_theory
gt
    tim2 :: TokenInfoMap
tim2 = Token -> ProcInfo -> TokenInfoMap -> TokenInfoMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
tok (NodeSig -> Node
getNode NodeSig
ns, Sign
sg, Symbols
ss1 Symbols -> Symbols -> Symbols
forall a. [a] -> [a] -> [a]
++ Symbols
ss2, [], []) TokenInfoMap
tim1
    (tim3 :: TokenInfoMap
tim3, dg3 :: DGraph
dg3) = Token
-> [ImportProc]
-> Sign
-> TokenInfoMap
-> DGraph
-> (TokenInfoMap, DGraph)
createEdgesImports Token
tok [ImportProc]
ips Sign
sg TokenInfoMap
tim2 DGraph
dg2
    -- (_, tim4, dg4) = insertFreeNode tok tim3 [] dg3
insertSpec (SpecView sp_v :: View
sp_v) pdg :: DGraph
pdg ptim :: TokenInfoMap
ptim tim :: TokenInfoMap
tim vm :: ViewMap
vm ths :: [Token]
ths dg :: DGraph
dg =
  (TokenInfoMap
ptimUp, TokenInfoMap
tim3, ViewMap
vm', [Token]
ths, DGraph
dg4) where
    View name :: ModId
name from :: ModExp
from to :: ModExp
to rnms :: [Renaming]
rnms = View
sp_v
    (ptimUp :: TokenInfoMap
ptimUp, timUp :: TokenInfoMap
timUp, dgUp :: DGraph
dgUp) = ModExp -> ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredView ModExp
from ModExp
to DGraph
pdg (TokenInfoMap
ptim, TokenInfoMap
tim, DGraph
dg)
    inst :: Bool
inst = [Token] -> ModExp -> Bool
isInstantiated [Token]
ths ModExp
to
    tok_name :: Token
tok_name = ModId -> Token
forall a. HasName a => a -> Token
HasName.getName ModId
name
    (tok1 :: Token
tok1, tim1 :: TokenInfoMap
tim1, morph1 :: Morphism
morph1, _, dg1 :: DGraph
dg1) = TokenInfoMap
-> ViewMap
-> DGraph
-> ModExp
-> (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
processModExp TokenInfoMap
timUp ViewMap
vm DGraph
dgUp ModExp
from
    (tok2 :: Token
tok2, tim2 :: TokenInfoMap
tim2, morph2 :: Morphism
morph2, _, dg2 :: DGraph
dg2) = TokenInfoMap
-> ViewMap
-> DGraph
-> ModExp
-> (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
processModExp TokenInfoMap
tim1 ViewMap
vm DGraph
dg1 ModExp
to
    n1 :: Node
n1 = Token -> TokenInfoMap -> Node
tokenNode Token
tok1 TokenInfoMap
tim2
    n2 :: Node
n2 = Token -> TokenInfoMap -> Node
tokenNode Token
tok2 TokenInfoMap
tim2
    morph :: Morphism
morph = Sign -> Sign -> [Renaming] -> Morphism
fromSignsRenamings (Morphism -> Sign
target Morphism
morph1) (Morphism -> Sign
target Morphism
morph2) [Renaming]
rnms
    Just morph' :: Morphism
morph' = Result Morphism -> Maybe Morphism
forall a. Result a -> Maybe a
maybeResult (Result Morphism -> Maybe Morphism)
-> Result Morphism -> Maybe Morphism
forall a b. (a -> b) -> a -> b
$ Morphism -> Morphism -> Result Morphism
compose Morphism
morph1 Morphism
morph
    (new_sign :: Sign
new_sign, new_sens :: [Sentence]
new_sens) = Sign -> SymbolMap -> [Renaming] -> (Sign, [Sentence])
sign4renamings (Morphism -> Sign
target Morphism
morph1) (Morphism -> SymbolMap
sortMap Morphism
morph) [Renaming]
rnms
    (n3 :: Node
n3, tim3 :: TokenInfoMap
tim3, dg3 :: DGraph
dg3) = Node
-> TokenInfoMap
-> Token
-> Morphism
-> Sign
-> [Sentence]
-> DGraph
-> (Node, TokenInfoMap, DGraph)
insertInnerNode Node
n2 TokenInfoMap
tim2 Token
tok2 Morphism
morph2 Sign
new_sign [Sentence]
new_sens DGraph
dg2
    vm' :: ViewMap
vm' = Token
-> (Node, Token, Morphism, [Renaming], Bool) -> ViewMap -> ViewMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModId -> Token
forall a. HasName a => a -> Token
HasName.getName ModId
name) (Node
n3, Token
tok2, Morphism
morph', [Renaming]
rnms, Bool
inst) ViewMap
vm
    dg4 :: DGraph
dg4 = Token -> Node -> Node -> Morphism -> DGraph -> DGraph
insertThmEdgeMorphism Token
tok_name Node
n3 Node
n1 Morphism
morph' DGraph
dg3

{- | Includes the references used in importations to modules in the maude
prelude in the current DG -}
incPredImps :: [Import] -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImps :: [Import] -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImps [] _ up :: UpdtPredefs
up = UpdtPredefs
up
incPredImps (i :: Import
i : is :: [Import]
is) pdg :: DGraph
pdg up :: UpdtPredefs
up = [Import] -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImps [Import]
is DGraph
pdg UpdtPredefs
up'
          where up' :: UpdtPredefs
up' = Import -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImp Import
i DGraph
pdg UpdtPredefs
up

{- | Includes the references used in parameterizations to modules in the maude
prelude in the current DG -}
incPredParams :: [Parameter] -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredParams :: [Parameter] -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredParams [] _ up :: UpdtPredefs
up = UpdtPredefs
up
incPredParams (i :: Parameter
i : is :: [Parameter]
is) pdg :: DGraph
pdg up :: UpdtPredefs
up = [Parameter] -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredParams [Parameter]
is DGraph
pdg UpdtPredefs
up'
          where up' :: UpdtPredefs
up' = Parameter -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredParam Parameter
i DGraph
pdg UpdtPredefs
up

{- | Includes the references used in views to modules in the maude prelude
in the current DG -}
incPredView :: ModExp -> ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredView :: ModExp -> ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredView from :: ModExp
from to :: ModExp
to pdg :: DGraph
pdg up :: UpdtPredefs
up = UpdtPredefs
up''
          where up' :: UpdtPredefs
up' = ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImpME ModExp
from DGraph
pdg UpdtPredefs
up
                up'' :: UpdtPredefs
up'' = ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImpME ModExp
to DGraph
pdg UpdtPredefs
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 -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredParam (Parameter _ me :: ModExp
me) = ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImpME ModExp
me

{- | Includes the references used in an importation to modules in the maude
prelude in the current DG -}
incPredImp :: Import -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImp :: Import -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImp i :: Import
i up :: DGraph
up = UpdtPredefs -> UpdtPredefs
up'
          where me :: ModExp
me = Import -> ModExp
getModExp Import
i
                up' :: UpdtPredefs -> UpdtPredefs
up' = ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImpME ModExp
me DGraph
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 -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImpME (ModExp m_id :: ModId
m_id) pdg :: DGraph
pdg (ptim :: TokenInfoMap
ptim, tim :: TokenInfoMap
tim, dg :: DGraph
dg) = UpdtPredefs
up where
  ModId q :: Token
q = ModId
m_id
  q' :: Token
q' = Token -> Token
mkFreeName Token
q
  up :: UpdtPredefs
up = if Token -> TokenInfoMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Token
q TokenInfoMap
ptim then let
         (n :: Node
n, sg1 :: Sign
sg1, sys1 :: Symbols
sys1, tts1 :: [(Token, Token, Symbols)]
tts1, ps1 :: [ParamSort]
ps1) = TokenInfoMap
ptim TokenInfoMap -> Token -> ProcInfo
forall k a. Ord k => Map k a -> k -> a
Map.! Token
q
         (n' :: Node
n', sg2 :: Sign
sg2, sys2 :: Symbols
sys2, tts2 :: [(Token, Token, Symbols)]
tts2, ps2 :: [ParamSort]
ps2) = TokenInfoMap
ptim TokenInfoMap -> Token -> ProcInfo
forall k a. Ord k => Map k a -> k -> a
Map.! Token
q'
         refInfo :: DGNodeInfo
refInfo = LibName -> Node -> DGNodeInfo
newRefInfo LibName
preludeLib Node
n
         refInfo' :: DGNodeInfo
refInfo' = LibName -> Node -> DGNodeInfo
newRefInfo LibName
preludeLib Node
n'
         ptim1 :: TokenInfoMap
ptim1 = Token -> TokenInfoMap -> TokenInfoMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Token
q TokenInfoMap
ptim
         ptim2 :: TokenInfoMap
ptim2 = Token -> TokenInfoMap -> TokenInfoMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Token
q' TokenInfoMap
ptim1
         ext_sg1 :: ExtSign Sign Symbol
ext_sg1 = Maude -> Sign -> ExtSign Sign Symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign Maude
Maude Sign
sg1
         gt1 :: G_theory
gt1 = ExtSign Sign Symbol
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
maudeTheory ExtSign Sign Symbol
ext_sg1 SigId
startSigId ThSens Sentence (AnyComorphism, BasicProof)
forall a b. ThSens a b
noSens ThId
startThId
         name1 :: NodeName
name1 = IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$ Token -> IRI
simpleIdToIRI Token
q
         new :: DGNodeLab
new = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
name1 DGNodeInfo
refInfo G_theory
gt1
         newNode :: Node
newNode = DGraph -> Node
getNewNodeDG DGraph
dg
         refLab :: DGNodeLab
refLab = DGraph -> Node -> DGNodeLab
labDG DGraph
pdg Node
n
         nodeCont :: DGNodeLab
nodeCont = DGNodeLab
new { globalTheory :: Maybe G_theory
globalTheory = DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
refLab }
         -- (ns1, dg1) = insGTheory dg name1 DGBasic gt1
         dg1 :: DGraph
dg1 = LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Node
newNode, DGNodeLab
nodeCont) DGraph
dg
         ext_sg2 :: ExtSign Sign Symbol
ext_sg2 = Maude -> Sign -> ExtSign Sign Symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign Maude
Maude Sign
sg2
         gt2 :: G_theory
gt2 = ExtSign Sign Symbol
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
maudeTheory ExtSign Sign Symbol
ext_sg2 SigId
startSigId ThSens Sentence (AnyComorphism, BasicProof)
forall a b. ThSens a b
noSens ThId
startThId
         name2 :: NodeName
name2 = IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$ Token -> IRI
simpleIdToIRI Token
q'
         new' :: DGNodeLab
new' = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
name2 DGNodeInfo
refInfo' G_theory
gt2
         newNode' :: Node
newNode' = DGraph -> Node
getNewNodeDG DGraph
dg1
         refLab' :: DGNodeLab
refLab' = DGraph -> Node -> DGNodeLab
labDG DGraph
pdg Node
n'
         nodeCont' :: DGNodeLab
nodeCont' = DGNodeLab
new' { globalTheory :: Maybe G_theory
globalTheory = DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
refLab' }
         -- (ns2, dg2) = insGTheory dg1 name2 DGBasic gt2
         dg2 :: DGraph
dg2 = LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Node
newNode', DGNodeLab
nodeCont') DGraph
dg1
         tim1 :: TokenInfoMap
tim1 = Token -> ProcInfo -> TokenInfoMap -> TokenInfoMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
q (Node
newNode, Sign
sg1, Symbols
sys1, [(Token, Token, Symbols)]
tts1, [ParamSort]
ps1) TokenInfoMap
tim
         tim2 :: TokenInfoMap
tim2 = Token -> ProcInfo -> TokenInfoMap -> TokenInfoMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
q' (Node
newNode', Sign
sg2, Symbols
sys2, [(Token, Token, Symbols)]
tts2, [ParamSort]
ps2) TokenInfoMap
tim1
         in (TokenInfoMap
ptim2, TokenInfoMap
tim2, DGraph
dg2)
       else (TokenInfoMap
ptim, TokenInfoMap
tim, DGraph
dg)
incPredImpME (SummationModExp me :: ModExp
me me' :: ModExp
me') pdg :: DGraph
pdg up :: UpdtPredefs
up = UpdtPredefs
up''
          where up' :: UpdtPredefs
up' = ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImpME ModExp
me DGraph
pdg UpdtPredefs
up
                up'' :: UpdtPredefs
up'' = ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImpME ModExp
me' DGraph
pdg UpdtPredefs
up'
incPredImpME (RenamingModExp me :: ModExp
me _) pdg :: DGraph
pdg up :: UpdtPredefs
up = ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImpME ModExp
me DGraph
pdg UpdtPredefs
up
incPredImpME (InstantiationModExp me :: ModExp
me _) pdg :: DGraph
pdg up :: UpdtPredefs
up = ModExp -> DGraph -> UpdtPredefs -> UpdtPredefs
incPredImpME ModExp
me DGraph
pdg UpdtPredefs
up

-- | extracts the module expression from an importation statement
getModExp :: Import -> ModExp
getModExp :: Import -> ModExp
getModExp (Including me :: ModExp
me) = ModExp
me
getModExp (Extending me :: ModExp
me) = ModExp
me
getModExp (Protecting me :: ModExp
me) = ModExp
me

-- | computes the union of the signatures obtained from the importation list
sign_union :: Sign -> [ImportProc] -> Sign
sign_union :: Sign -> [ImportProc] -> Sign
sign_union = (ImportProc -> Sign -> Sign) -> Sign -> [ImportProc] -> Sign
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Sign -> Sign -> Sign
Maude.Sign.union (Sign -> Sign -> Sign)
-> (ImportProc -> Sign) -> ImportProc -> Sign -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportProc -> Sign
get_sign)

-- | extracts the target signature from the morphism in an importation tuple
get_sign :: ImportProc -> Sign
get_sign :: ImportProc -> Sign
get_sign (_, _, _, morph :: Morphism
morph, _, _) = Morphism -> Sign
target Morphism
morph

-- | computes the union of the target signatures of a list of morphisms
sign_union_morphs :: [Morphism] -> Sign -> Sign
sign_union_morphs :: [Morphism] -> Sign -> Sign
sign_union_morphs morphs :: [Morphism]
morphs sg :: Sign
sg = (Morphism -> Sign -> Sign) -> Sign -> [Morphism] -> Sign
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Sign -> Sign -> Sign
Maude.Sign.union (Sign -> Sign -> Sign)
-> (Morphism -> Sign) -> Morphism -> Sign -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Sign
target) Sign
sg [Morphism]
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 :: [ImportProc] -> (TokenInfoMap, DGraph) -> (TokenInfoMap, DGraph)
last_da [(_, _, tim :: TokenInfoMap
tim, _, _, dg :: DGraph
dg)] _ = (TokenInfoMap
tim, DGraph
dg)
last_da (_ : ips :: [ImportProc]
ips) p :: (TokenInfoMap, DGraph)
p = [ImportProc] -> (TokenInfoMap, DGraph) -> (TokenInfoMap, DGraph)
last_da [ImportProc]
ips (TokenInfoMap, DGraph)
p
last_da _ p :: (TokenInfoMap, DGraph)
p = (TokenInfoMap, DGraph)
p

-- | generates the edges required by a parameter list in a module instantiation
createEdgesParams :: Token -> [(Token, Token, Symbols)] -> [Morphism] -> Sign
                     -> TokenInfoMap -> DGraph -> DGraph
createEdgesParams :: Token
-> [(Token, Token, Symbols)]
-> [Morphism]
-> Sign
-> TokenInfoMap
-> DGraph
-> DGraph
createEdgesParams tok1 :: Token
tok1 ((_, tok2 :: Token
tok2, _) : toks :: [(Token, Token, Symbols)]
toks) (morph :: Morphism
morph : morphs :: [Morphism]
morphs) sg :: Sign
sg tim :: TokenInfoMap
tim dg :: DGraph
dg =
    Token
-> [(Token, Token, Symbols)]
-> [Morphism]
-> Sign
-> TokenInfoMap
-> DGraph
-> DGraph
createEdgesParams Token
tok1 [(Token, Token, Symbols)]
toks [Morphism]
morphs Sign
sg TokenInfoMap
tim
      (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ Token
-> Token
-> DGLinkType
-> Morphism
-> Sign
-> TokenInfoMap
-> DGraph
-> DGraph
createEdgeMorphism Token
tok1 Token
tok2 DGLinkType
globalDef Morphism
morph Sign
sg TokenInfoMap
tim DGraph
dg
createEdgesParams _ _ _ _ _ dg :: DGraph
dg = DGraph
dg

createEdgeMorphism :: Token -> Token -> DGLinkType -> Morphism -> Sign
  -> TokenInfoMap -> DGraph -> DGraph
createEdgeMorphism :: Token
-> Token
-> DGLinkType
-> Morphism
-> Sign
-> TokenInfoMap
-> DGraph
-> DGraph
createEdgeMorphism tok1 :: Token
tok1 tok2 :: Token
tok2 lt :: DGLinkType
lt morph :: Morphism
morph sg :: Sign
sg tim :: TokenInfoMap
tim =
  Node -> Node -> DGLinkType -> Morphism -> DGraph -> DGraph
insertEdgeMorphism Node
n1 Node
n2 DGLinkType
lt Morphism
morph' where
  morph' :: Morphism
morph' = Sign -> Morphism -> Morphism
setTarget Sign
sg Morphism
morph
  n1 :: Node
n1 = Token -> TokenInfoMap -> Node
tokenNode Token
tok1 TokenInfoMap
tim
  n2 :: Node
n2 = Token -> TokenInfoMap -> Node
tokenNode Token
tok2 TokenInfoMap
tim

-- | generates the edges required by the importations
createEdgesImports :: Token -> [ImportProc] -> Sign -> TokenInfoMap -> DGraph
                      -> (TokenInfoMap, DGraph)
createEdgesImports :: Token
-> [ImportProc]
-> Sign
-> TokenInfoMap
-> DGraph
-> (TokenInfoMap, DGraph)
createEdgesImports _ [] _ tim :: TokenInfoMap
tim dg :: DGraph
dg = (TokenInfoMap
tim, DGraph
dg)
createEdgesImports tok :: Token
tok (ip :: ImportProc
ip : ips :: [ImportProc]
ips) sg :: Sign
sg tim :: TokenInfoMap
tim dg :: DGraph
dg =
    Token
-> [ImportProc]
-> Sign
-> TokenInfoMap
-> DGraph
-> (TokenInfoMap, DGraph)
createEdgesImports Token
tok [ImportProc]
ips Sign
sg TokenInfoMap
tim' DGraph
dg'
               where (tim' :: TokenInfoMap
tim', dg' :: DGraph
dg') = Token
-> ImportProc
-> Sign
-> TokenInfoMap
-> DGraph
-> (TokenInfoMap, DGraph)
createEdgeImport Token
tok ImportProc
ip Sign
sg TokenInfoMap
tim DGraph
dg

-- | generates the edge for a concrete importation
createEdgeImport :: Token -> ImportProc -> Sign -> TokenInfoMap -> DGraph
                    -> (TokenInfoMap, DGraph)
createEdgeImport :: Token
-> ImportProc
-> Sign
-> TokenInfoMap
-> DGraph
-> (TokenInfoMap, DGraph)
createEdgeImport tok1 :: Token
tok1 (ip :: ImportType
ip, tok2 :: Token
tok2, _, morph :: Morphism
morph, _, _) sg :: Sign
sg tim :: TokenInfoMap
tim dg :: DGraph
dg =
  let (tok2' :: Token
tok2', tim' :: TokenInfoMap
tim', dg' :: DGraph
dg') = case ImportType
ip of
        Pr -> Token
-> TokenInfoMap
-> [Morphism]
-> DGraph
-> (Token, TokenInfoMap, DGraph)
insertFreeNode Token
tok2 TokenInfoMap
tim [] DGraph
dg
        _ -> (Token
tok2, TokenInfoMap
tim, DGraph
dg)
  in (TokenInfoMap
tim', Token
-> Token
-> DGLinkType
-> Morphism
-> Sign
-> TokenInfoMap
-> DGraph
-> DGraph
createEdgeMorphism Token
tok1 Token
tok2'
      (case ImportType
ip of
         Ex -> Conservativity -> DGLinkType
globalConsThm Conservativity
PCons -- a PCons link
         _ -> DGLinkType
globalDef) Morphism
morph Sign
sg TokenInfoMap
tim' DGraph
dg')

-- | extracts the sorts provided by the theories
getThSorts :: [ImportProc] -> Symbols
getThSorts :: [ImportProc] -> Symbols
getThSorts = (ImportProc -> Symbols) -> [ImportProc] -> Symbols
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ImportProc -> Symbols
getThSortsAux

-- | extracts the not-bounded-yet sorts related to the given identifier
getThSortsAux :: ImportProc -> Symbols
getThSortsAux :: ImportProc -> Symbols
getThSortsAux (_, tok :: Token
tok, tim :: TokenInfoMap
tim, _, _, _) = Symbols
srts
         where (_, _, srts :: Symbols
srts, _, _) = Token -> TokenInfoMap -> ProcInfo
getProcInfo Token
tok TokenInfoMap
tim

{- | generates the extra signature needed when using term to term renaming in
views -}
sign4renamings :: Sign -> SymbolMap -> [Renaming] -> (Sign, [Sentence])
sign4renamings :: Sign -> SymbolMap -> [Renaming] -> (Sign, [Sentence])
sign4renamings sg :: Sign
sg sm :: SymbolMap
sm (TermMap t1 :: Term
t1 t2 :: Term
t2 : rnms :: [Renaming]
rnms) = (Sign
new_sg, Equation -> Sentence
Equation Equation
eq Sentence -> [Sentence] -> [Sentence]
forall a. a -> [a] -> [a]
: [Sentence]
sens)
         where (op_top :: Token
op_top, ss :: Symbols
ss) = Term -> (Token, Symbols)
getOpSorts Term
t1
               sg' :: Sign
sg' = Sign -> Token -> Symbols -> SymbolMap -> Sign
newOp Sign
sg Token
op_top Symbols
ss SymbolMap
sm
               (sg'' :: Sign
sg'', sens :: [Sentence]
sens) = Sign -> SymbolMap -> [Renaming] -> (Sign, [Sentence])
sign4renamings Sign
sg SymbolMap
sm [Renaming]
rnms
               eq :: Equation
eq = Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq (SymbolMap -> Term -> Term
applyRenamingTerm SymbolMap
sm Term
t1) Term
t2 [] []
               new_sg :: Sign
new_sg = Sign -> Sign -> Sign
Maude.Sign.union Sign
sg' Sign
sg''
sign4renamings sg :: Sign
sg sm :: SymbolMap
sm (_ : rnms :: [Renaming]
rnms) = Sign -> SymbolMap -> [Renaming] -> (Sign, [Sentence])
sign4renamings Sign
sg SymbolMap
sm [Renaming]
rnms
sign4renamings sg :: Sign
sg _ [] = (Sign
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 :: Sign -> Token -> Symbols -> SymbolMap -> Sign
newOp sg :: Sign
sg op :: Token
op ss :: Symbols
ss sm :: SymbolMap
sm = Sign
Maude.Sign.empty {ops :: OpMap
ops = Token -> OpDeclSet -> OpMap
forall k a. k -> a -> Map k a
Map.singleton Token
op OpDeclSet
ods'}
         where om :: OpMap
om = Sign -> OpMap
ops Sign
sg
               Just ods :: OpDeclSet
ods = Token -> OpMap -> Maybe OpDeclSet
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Token
op OpMap
om
               ods' :: OpDeclSet
ods' = OpDeclSet -> Symbols -> SymbolMap -> OpDeclSet
getOpDeclSet OpDeclSet
ods Symbols
ss SymbolMap
sm

-- | renames the profile with the given map
getOpDeclSet :: OpDeclSet -> Symbols -> SymbolMap -> OpDeclSet
getOpDeclSet :: OpDeclSet -> Symbols -> SymbolMap -> OpDeclSet
getOpDeclSet ods :: OpDeclSet
ods ss :: Symbols
ss sm :: SymbolMap
sm = (Set Symbol, [Attr]) -> OpDeclSet
forall a. a -> Set a
Set.singleton (Set Symbol
op_sym', [Attr]
ats)
         where f :: Symbol -> Bool -> Bool
f ~(Operator _ x :: Symbols
x _) b :: Bool
b = Symbols
x Symbols -> Symbols -> Bool
forall a. Eq a => a -> a -> Bool
== Symbols
ss Bool -> Bool -> Bool
|| Bool
b
               g :: (Set Symbol, b) -> Bool
g = (Symbol -> Bool -> Bool) -> Bool -> Set Symbol -> Bool
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Symbol -> Bool -> Bool
f Bool
False (Set Symbol -> Bool)
-> ((Set Symbol, b) -> Set Symbol) -> (Set Symbol, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Symbol, b) -> Set Symbol
forall a b. (a, b) -> a
fst
               (ods' :: Set Symbol
ods', ats :: [Attr]
ats) : _ = OpDeclSet -> [(Set Symbol, [Attr])]
forall a. Set a -> [a]
Set.toList (OpDeclSet -> [(Set Symbol, [Attr])])
-> OpDeclSet -> [(Set Symbol, [Attr])]
forall a b. (a -> b) -> a -> b
$ ((Set Symbol, [Attr]) -> Bool) -> OpDeclSet -> OpDeclSet
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Set Symbol, [Attr]) -> Bool
forall b. (Set Symbol, b) -> Bool
g OpDeclSet
ods
               h :: Symbol -> Bool
h ~(Operator _ y :: Symbols
y _) = Symbols
y Symbols -> Symbols -> Bool
forall a. Eq a => a -> a -> Bool
== Symbols
ss
               ods'' :: Set Symbol
ods'' = (Symbol -> Bool) -> Set Symbol -> Set Symbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Symbol -> Bool
h Set Symbol
ods'
               op_sym :: Symbol
op_sym : _ = Set Symbol -> Symbols
forall a. Set a -> [a]
Set.toList Set Symbol
ods''
               op_sym' :: Set Symbol
op_sym' = Symbol -> SymbolMap -> Set Symbol
applyRenamingOpSymbol Symbol
op_sym SymbolMap
sm

-- | applies the renaming in the map to the operator declaration
applyRenamingOpSymbol :: Symbol -> SymbolMap -> SymbolSet
applyRenamingOpSymbol :: Symbol -> SymbolMap -> Set Symbol
applyRenamingOpSymbol (Operator q :: Token
q ar :: Symbols
ar co :: Symbol
co) sm :: SymbolMap
sm = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol) -> Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Token -> Symbols -> Symbol -> Symbol
Operator Token
q Symbols
ar' Symbol
co'
         where f :: Symbol -> Symbol
f x :: Symbol
x = Symbol -> Symbol -> SymbolMap -> Symbol
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Symbol
x Symbol
x SymbolMap
sm
               ar' :: Symbols
ar' = (Symbol -> Symbol) -> Symbols -> Symbols
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Symbol
f Symbols
ar
               co' :: Symbol
co' = Symbol -> Symbol
f Symbol
co
applyRenamingOpSymbol _ _ = Set Symbol
forall a. Set a
Set.empty

-- | renames the sorts in a term
applyRenamingTerm :: SymbolMap -> Term -> Term
applyRenamingTerm :: SymbolMap -> Term -> Term
applyRenamingTerm sm :: SymbolMap
sm (Apply q :: Token
q ts :: [Term]
ts ty :: Type
ty) = Token -> [Term] -> Type -> Term
Apply Token
q ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (SymbolMap -> Term -> Term
applyRenamingTerm SymbolMap
sm) [Term]
ts)
                                               (SymbolMap -> Type -> Type
applyRenamingType SymbolMap
sm Type
ty)
applyRenamingTerm sm :: SymbolMap
sm (Const q :: Token
q s :: Type
s) = Token -> Type -> Term
Const Token
q Type
s'
         where s' :: Type
s' = SymbolMap -> Type -> Type
applyRenamingType SymbolMap
sm Type
s
applyRenamingTerm sm :: SymbolMap
sm (Var q :: Token
q s :: Type
s) = Token -> Type -> Term
Var Token
q Type
s'
         where s' :: Type
s' = SymbolMap -> Type -> Type
applyRenamingType SymbolMap
sm Type
s

-- | renames a type
applyRenamingType :: SymbolMap -> Type -> Type
applyRenamingType :: SymbolMap -> Type -> Type
applyRenamingType sm :: SymbolMap
sm (TypeSort s :: Sort
s) = Sort -> Type
TypeSort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Token -> Sort
SortId (Token -> Sort) -> Token -> Sort
forall a b. (a -> b) -> a -> b
$ Symbol -> Token
forall a. HasName a => a -> Token
HasName.getName Symbol
q'
         where SortId q :: Token
q = Sort
s
               q' :: Symbol
q' = Symbol -> Symbol -> SymbolMap -> Symbol
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (Token -> Symbol
Sort Token
q) (Token -> Symbol
Sort Token
q) SymbolMap
sm
applyRenamingType sm :: SymbolMap
sm (TypeKind k :: Kind
k) = Kind -> Type
TypeKind (Kind -> Type) -> Kind -> Type
forall a b. (a -> b) -> a -> b
$ Token -> Kind
KindId (Token -> Kind) -> Token -> Kind
forall a b. (a -> b) -> a -> b
$ Symbol -> Token
forall a. HasName a => a -> Token
HasName.getName Symbol
q'
         where KindId q :: Token
q = Kind
k
               q' :: Symbol
q' = Symbol -> Symbol -> SymbolMap -> Symbol
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (Token -> Symbol
Kind Token
q) (Token -> Symbol
Kind Token
q) SymbolMap
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 :: Term -> (Token, Symbols)
getOpSorts (Const q :: Token
q _) = (Token
q, [])
getOpSorts (Var q :: Token
q _) = (Token
q, [])
getOpSorts (Apply q :: Token
q ls :: [Term]
ls _) = (Token
q, [Term] -> Symbols
getTypes [Term]
ls)

-- | extracts the types of the terms while they are variables
getTypes :: [Term] -> Symbols
getTypes :: [Term] -> Symbols
getTypes (Var _ (TypeSort s :: Sort
s) : ts :: [Term]
ts) = Token -> Symbol
Sort (Sort -> Token
forall a. HasName a => a -> Token
HasName.getName Sort
s) Symbol -> Symbols -> Symbols
forall a. a -> [a] -> [a]
: [Term] -> Symbols
getTypes [Term]
ts
getTypes (Var _ (TypeKind s :: Kind
s) : ts :: [Term]
ts) = Token -> Symbol
Kind (Kind -> Token
forall a. HasName a => a -> Token
HasName.getName Kind
s) Symbol -> Symbols -> Symbols
forall a. a -> [a] -> [a]
: [Term] -> Symbols
getTypes [Term]
ts
getTypes _ = []

-- | process the information of the given list of imports
processImports :: TokenInfoMap -> ViewMap -> DGraph -> [Import] -> [ImportProc]
processImports :: TokenInfoMap -> ViewMap -> DGraph -> [Import] -> [ImportProc]
processImports _ _ _ [] = []
processImports tim :: TokenInfoMap
tim vm :: ViewMap
vm dg :: DGraph
dg (i :: Import
i : il :: [Import]
il) = ImportProc
ip ImportProc -> [ImportProc] -> [ImportProc]
forall a. a -> [a] -> [a]
: TokenInfoMap -> ViewMap -> DGraph -> [Import] -> [ImportProc]
processImports TokenInfoMap
tim' ViewMap
vm DGraph
dg' [Import]
il
         where ip :: ImportProc
ip@(_, _, tim' :: TokenInfoMap
tim', _, _, dg' :: DGraph
dg') = TokenInfoMap -> ViewMap -> DGraph -> Import -> ImportProc
processImport TokenInfoMap
tim ViewMap
vm DGraph
dg Import
i

{- | process the module expression and then adds the information about
the type of import -}
processImport :: TokenInfoMap -> ViewMap -> DGraph -> Import -> ImportProc
processImport :: TokenInfoMap -> ViewMap -> DGraph -> Import -> ImportProc
processImport tim :: TokenInfoMap
tim vm :: ViewMap
vm dg :: DGraph
dg (Protecting modExp :: ModExp
modExp) = (ImportType
Pr, Token
tok, TokenInfoMap
tim', Morphism
morph, [ParamSort]
ps, DGraph
dg')
         where (tok :: Token
tok, tim' :: TokenInfoMap
tim', morph :: Morphism
morph, ps :: [ParamSort]
ps, dg' :: DGraph
dg') = TokenInfoMap
-> ViewMap
-> DGraph
-> ModExp
-> (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
processModExp TokenInfoMap
tim ViewMap
vm DGraph
dg ModExp
modExp
processImport tim :: TokenInfoMap
tim vm :: ViewMap
vm dg :: DGraph
dg (Extending modExp :: ModExp
modExp) = (ImportType
Ex, Token
tok, TokenInfoMap
tim', Morphism
morph, [ParamSort]
ps, DGraph
dg')
         where (tok :: Token
tok, tim' :: TokenInfoMap
tim', morph :: Morphism
morph, ps :: [ParamSort]
ps, dg' :: DGraph
dg') = TokenInfoMap
-> ViewMap
-> DGraph
-> ModExp
-> (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
processModExp TokenInfoMap
tim ViewMap
vm DGraph
dg ModExp
modExp
processImport tim :: TokenInfoMap
tim vm :: ViewMap
vm dg :: DGraph
dg (Including modExp :: ModExp
modExp) = (ImportType
Inc, Token
tok, TokenInfoMap
tim', Morphism
morph, [ParamSort]
ps, DGraph
dg')
         where (tok :: Token
tok, tim' :: TokenInfoMap
tim', morph :: Morphism
morph, ps :: [ParamSort]
ps, dg' :: DGraph
dg') = TokenInfoMap
-> ViewMap
-> DGraph
-> ModExp
-> (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
processModExp TokenInfoMap
tim ViewMap
vm DGraph
dg ModExp
modExp

-- | traverses the list of parameters and generates the required data structures
processParameters :: [Parameter] -> TokenInfoMap -> DGraph -> ParamInfo
processParameters :: [Parameter]
-> TokenInfoMap
-> DGraph
-> ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph)
processParameters ps :: [Parameter]
ps tim :: TokenInfoMap
tim dg :: DGraph
dg = (Parameter
 -> ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph)
 -> ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph))
-> ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph)
-> [Parameter]
-> ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Parameter
-> ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph)
-> ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph)
processParameter ([], TokenInfoMap
tim, [], DGraph
dg) [Parameter]
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
-> ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph)
-> ([(Token, Token, Symbols)], TokenInfoMap, [Morphism], DGraph)
processParameter (Parameter sort :: Sort
sort modExp :: ModExp
modExp) (toks :: [(Token, Token, Symbols)]
toks, tim :: TokenInfoMap
tim, morphs :: [Morphism]
morphs, dg :: DGraph
dg) =
    ([(Token, Token, Symbols)]
toks', TokenInfoMap
tim', [Morphism]
morphs', DGraph
dg')
         where (tok :: Token
tok, tim' :: TokenInfoMap
tim', morph :: Morphism
morph, _, dg' :: DGraph
dg') =
                   TokenInfoMap
-> ViewMap
-> DGraph
-> ModExp
-> (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
processModExp TokenInfoMap
tim ViewMap
forall k a. Map k a
Map.empty DGraph
dg ModExp
modExp
               (_, _, fs :: Symbols
fs, _, _) = Token -> TokenInfoMap -> ProcInfo
getProcInfo Token
tok TokenInfoMap
tim'
               fs' :: Symbols
fs' = Morphism -> Symbols -> Symbols
forall a. HasSorts a => Morphism -> a -> a
translateSorts Morphism
morph Symbols
fs
               morph' :: Morphism
morph' = Morphism -> Token -> Symbols -> Morphism
qualifySorts Morphism
morph (Sort -> Token
forall a. HasName a => a -> Token
HasName.getName Sort
sort) Symbols
fs'
               toks' :: [(Token, Token, Symbols)]
toks' = (Sort -> Token
forall a. HasName a => a -> Token
HasName.getName Sort
sort, Token
tok, Symbols
fs') (Token, Token, Symbols)
-> [(Token, Token, Symbols)] -> [(Token, Token, Symbols)]
forall a. a -> [a] -> [a]
: [(Token, Token, Symbols)]
toks
               morphs' :: [Morphism]
morphs' = Morphism
morph' Morphism -> [Morphism] -> [Morphism]
forall a. a -> [a] -> [a]
: [Morphism]
morphs

{- | distinguishes between the different module expressions to compute
the morphisms and update the development graph -}
processModExp :: TokenInfoMap -> ViewMap -> DGraph -> ModExp -> ModExpProc
processModExp :: TokenInfoMap
-> ViewMap
-> DGraph
-> ModExp
-> (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
processModExp tim :: TokenInfoMap
tim _ dg :: DGraph
dg (ModExp modId :: ModId
modId) = (Token
tok, TokenInfoMap
tim, Morphism
morph, [ParamSort]
ps, DGraph
dg)
                     where tok :: Token
tok = ModId -> Token
forall a. HasName a => a -> Token
HasName.getName ModId
modId
                           (_, sg :: Sign
sg, _, _, ps :: [ParamSort]
ps) = Token -> TokenInfoMap -> ProcInfo
getProcInfo Token
tok TokenInfoMap
tim
                           morph :: Morphism
morph = Sign -> Sign -> Morphism
Maude.Morphism.inclusion Sign
sg Sign
sg
processModExp tim :: TokenInfoMap
tim vm :: ViewMap
vm dg :: DGraph
dg (SummationModExp modExp1 :: ModExp
modExp1 modExp2 :: ModExp
modExp2) =
  (Token
tok, TokenInfoMap
tim3, Morphism
morph, [ParamSort]
ps', DGraph
dg5) where
    (tok1 :: Token
tok1, tim1 :: TokenInfoMap
tim1, morph1 :: Morphism
morph1, ps1 :: [ParamSort]
ps1, dg1 :: DGraph
dg1) = TokenInfoMap
-> ViewMap
-> DGraph
-> ModExp
-> (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
processModExp TokenInfoMap
tim ViewMap
vm DGraph
dg ModExp
modExp1
    (tok2 :: Token
tok2, tim2 :: TokenInfoMap
tim2, morph2 :: Morphism
morph2, ps2 :: [ParamSort]
ps2, dg2 :: DGraph
dg2) = TokenInfoMap
-> ViewMap
-> DGraph
-> ModExp
-> (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
processModExp TokenInfoMap
tim1 ViewMap
vm DGraph
dg1 ModExp
modExp2
    ps' :: [ParamSort]
ps' = [ParamSort] -> [ParamSort]
forall a. Ord a => [a] -> [a]
nubOrd ([ParamSort] -> [ParamSort]) -> [ParamSort] -> [ParamSort]
forall a b. (a -> b) -> a -> b
$ [ParamSort]
ps1 [ParamSort] -> [ParamSort] -> [ParamSort]
forall a. [a] -> [a] -> [a]
++ [ParamSort]
ps2
    tok :: Token
tok = [Char] -> Token
mkSimpleId ([Char] -> Token) -> [Char] -> Token
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ["{", Token -> [Char]
forall a. Show a => a -> [Char]
show Token
tok1, " + ", Token -> [Char]
forall a. Show a => a -> [Char]
show Token
tok2, "}"]
    (n1 :: Node
n1, _, ss1 :: Symbols
ss1, _, _) = Token -> TokenInfoMap -> ProcInfo
getProcInfo Token
tok1 TokenInfoMap
tim2
    (n2 :: Node
n2, _, ss2 :: Symbols
ss2, _, _) = Token -> TokenInfoMap -> ProcInfo
getProcInfo Token
tok2 TokenInfoMap
tim2
    ss1' :: Symbols
ss1' = Morphism -> Symbols -> Symbols
forall a. HasSorts a => Morphism -> a -> a
translateSorts Morphism
morph1 Symbols
ss1
    ss2' :: Symbols
ss2' = Morphism -> Symbols -> Symbols
forall a. HasSorts a => Morphism -> a -> a
translateSorts Morphism
morph1 Symbols
ss2
    sg1 :: Sign
sg1 = Morphism -> Sign
target Morphism
morph1
    sg2 :: Sign
sg2 = Morphism -> Sign
target Morphism
morph2
    sg :: Sign
sg = Sign -> Sign -> Sign
Maude.Sign.union Sign
sg1 Sign
sg2
    morph :: Morphism
morph = Sign -> Sign -> Morphism
Maude.Morphism.inclusion Sign
sg Sign
sg
    morph1' :: Morphism
morph1' = Sign -> Morphism -> Morphism
setTarget Sign
sg Morphism
morph1
    morph2' :: Morphism
morph2' = Sign -> Morphism -> Morphism
setTarget Sign
sg Morphism
morph2
    (tim3 :: TokenInfoMap
tim3, dg3 :: DGraph
dg3) = Token
-> Sign
-> TokenInfoMap
-> Symbols
-> [(Token, Token, Symbols)]
-> DGraph
-> (TokenInfoMap, DGraph)
insertNode Token
tok Sign
sg TokenInfoMap
tim2 (Symbols
ss1' Symbols -> Symbols -> Symbols
forall a. [a] -> [a] -> [a]
++ Symbols
ss2') [] DGraph
dg2
    n3 :: Node
n3 = Token -> TokenInfoMap -> Node
tokenNode Token
tok TokenInfoMap
tim3
    dg4 :: DGraph
dg4 = Node -> Node -> Morphism -> DGraph -> DGraph
insertDefEdgeMorphism Node
n3 Node
n1 Morphism
morph1' DGraph
dg3
    dg5 :: DGraph
dg5 = Node -> Node -> Morphism -> DGraph -> DGraph
insertDefEdgeMorphism Node
n3 Node
n2 Morphism
morph2' DGraph
dg4
processModExp tim :: TokenInfoMap
tim vm :: ViewMap
vm dg :: DGraph
dg (RenamingModExp modExp :: ModExp
modExp rnms :: [Renaming]
rnms) =
  (Token
tok, TokenInfoMap
tim', Morphism
comp_morph, [ParamSort]
ps', DGraph
dg') where
    (tok :: Token
tok, tim' :: TokenInfoMap
tim', morph :: Morphism
morph, ps :: [ParamSort]
ps, dg' :: DGraph
dg') = TokenInfoMap
-> ViewMap
-> DGraph
-> ModExp
-> (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
processModExp TokenInfoMap
tim ViewMap
vm DGraph
dg ModExp
modExp
    morph' :: Morphism
morph' = Sign -> [Renaming] -> Morphism
fromSignRenamings (Morphism -> Sign
target Morphism
morph) [Renaming]
rnms
    ps' :: [ParamSort]
ps' = SymbolMap -> [ParamSort] -> [ParamSort]
applyRenamingParamSorts (Morphism -> SymbolMap
sortMap Morphism
morph') [ParamSort]
ps
    Just comp_morph :: Morphism
comp_morph = Result Morphism -> Maybe Morphism
forall a. Result a -> Maybe a
maybeResult (Result Morphism -> Maybe Morphism)
-> Result Morphism -> Maybe Morphism
forall a b. (a -> b) -> a -> b
$ Morphism -> Morphism -> Result Morphism
compose Morphism
morph Morphism
morph'
processModExp tim :: TokenInfoMap
tim vm :: ViewMap
vm dg :: DGraph
dg (InstantiationModExp modExp :: ModExp
modExp views :: [ViewId]
views) =
  (Token
tok'', TokenInfoMap
tim'', Morphism
final_morph, [ParamSort]
new_param_sorts, DGraph
dg'') where
    (tok :: Token
tok, tim' :: TokenInfoMap
tim', morph :: Morphism
morph, paramSorts :: [ParamSort]
paramSorts, dg' :: DGraph
dg') = TokenInfoMap
-> ViewMap
-> DGraph
-> ModExp
-> (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)
processModExp TokenInfoMap
tim ViewMap
vm DGraph
dg ModExp
modExp
    (_, _, _, ps :: [(Token, Token, Symbols)]
ps, _) = Token -> TokenInfoMap -> ProcInfo
getProcInfo Token
tok TokenInfoMap
tim'
    param_names :: [Token]
param_names = ((Token, Token, Symbols) -> Token)
-> [(Token, Token, Symbols)] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (Token, Token, Symbols) -> Token
forall a b c. (a, b, c) -> a
fstTpl [(Token, Token, Symbols)]
ps
    view_names :: [Token]
view_names = (ViewId -> Token) -> [ViewId] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map ViewId -> Token
forall a. HasName a => a -> Token
HasName.getName [ViewId]
views
    (new_param_sorts :: [ParamSort]
new_param_sorts, ps_morph :: Morphism
ps_morph) = [Token]
-> [Token]
-> ViewMap
-> Morphism
-> [ParamSort]
-> ([ParamSort], Morphism)
instantiateSorts [Token]
param_names [Token]
view_names ViewMap
vm
      Morphism
morph [ParamSort]
paramSorts
    (tok' :: Token
tok', morph1 :: Morphism
morph1, ns :: [(Node, Morphism)]
ns, deps :: [(Token, Token, Symbols)]
deps) = [ViewId]
-> Token
-> TokenInfoMap
-> ViewMap
-> [(Token, Token, Symbols)]
-> (Morphism, [(Node, Morphism)], [(Token, Token, Symbols)])
-> (Token, Morphism, [(Node, Morphism)], [(Token, Token, Symbols)])
processViews [ViewId]
views ([Char] -> Token
mkSimpleId "") TokenInfoMap
tim' ViewMap
vm [(Token, Token, Symbols)]
ps
      (Morphism
ps_morph, [], [])
    tok'' :: Token
tok'' = [Char] -> Token
mkSimpleId ([Char] -> Token) -> [Char] -> Token
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Token -> [Char]
forall a. Show a => a -> [Char]
show Token
tok, "{", Token -> [Char]
forall a. Show a => a -> [Char]
show Token
tok', "}"]
    sg2 :: Sign
sg2 = Morphism -> Sign
target Morphism
morph1
    final_morph :: Morphism
final_morph = Sign -> Sign -> Morphism
Maude.Morphism.inclusion Sign
sg2 Sign
sg2
    (tim'' :: TokenInfoMap
tim'', dg'' :: DGraph
dg'') = if Token -> TokenInfoMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Token
tok'' TokenInfoMap
tim then (TokenInfoMap
tim', DGraph
dg') else
      Token
-> Token
-> Sign
-> Morphism
-> [(Node, Morphism)]
-> TokenInfoMap
-> [(Token, Token, Symbols)]
-> DGraph
-> (TokenInfoMap, DGraph)
updateGraphViews Token
tok Token
tok'' Sign
sg2 Morphism
morph1 [(Node, Morphism)]
ns TokenInfoMap
tim' [(Token, Token, Symbols)]
deps DGraph
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 :: Token
-> Token
-> Sign
-> Morphism
-> [(Node, Morphism)]
-> TokenInfoMap
-> [(Token, Token, Symbols)]
-> DGraph
-> (TokenInfoMap, DGraph)
updateGraphViews tok1 :: Token
tok1 tok2 :: Token
tok2 sg :: Sign
sg morph :: Morphism
morph views :: [(Node, Morphism)]
views tim :: TokenInfoMap
tim deps :: [(Token, Token, Symbols)]
deps dg :: DGraph
dg = (TokenInfoMap
tim', DGraph
dg''')
                     where n1 :: Node
n1 = Token -> TokenInfoMap -> Node
tokenNode Token
tok1 TokenInfoMap
tim
                           morph' :: Morphism
morph' = Sign -> Morphism -> Morphism
setTarget Sign
sg Morphism
morph
                           (tim' :: TokenInfoMap
tim', dg' :: DGraph
dg') = Token
-> Sign
-> TokenInfoMap
-> Symbols
-> [(Token, Token, Symbols)]
-> DGraph
-> (TokenInfoMap, DGraph)
insertNode Token
tok2 Sign
sg TokenInfoMap
tim [] [(Token, Token, Symbols)]
deps DGraph
dg
                           n2 :: Node
n2 = Token -> TokenInfoMap -> Node
tokenNode Token
tok2 TokenInfoMap
tim'
                           dg'' :: DGraph
dg'' = Node -> Node -> Morphism -> DGraph -> DGraph
insertDefEdgeMorphism Node
n2 Node
n1 Morphism
morph' DGraph
dg'
                           dg''' :: DGraph
dg''' = Node -> [(Node, Morphism)] -> Sign -> DGraph -> DGraph
insertDefEdgesMorphism Node
n2 [(Node, Morphism)]
views Sign
sg DGraph
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 :: [ViewId]
-> Token
-> TokenInfoMap
-> ViewMap
-> [(Token, Token, Symbols)]
-> (Morphism, [(Node, Morphism)], [(Token, Token, Symbols)])
-> (Token, Morphism, [(Node, Morphism)], [(Token, Token, Symbols)])
processViews (vi :: ViewId
vi : vis :: [ViewId]
vis) tok :: Token
tok tim :: TokenInfoMap
tim vm :: ViewMap
vm (p :: (Token, Token, Symbols)
p : ps :: [(Token, Token, Symbols)]
ps) (morph :: Morphism
morph, lp :: [(Node, Morphism)]
lp, dep :: [(Token, Token, Symbols)]
dep) =
  [ViewId]
-> Token
-> TokenInfoMap
-> ViewMap
-> [(Token, Token, Symbols)]
-> (Morphism, [(Node, Morphism)], [(Token, Token, Symbols)])
-> (Token, Morphism, [(Node, Morphism)], [(Token, Token, Symbols)])
processViews [ViewId]
vis Token
tok'' TokenInfoMap
tim ViewMap
vm [(Token, Token, Symbols)]
ps (Morphism
morph', [(Node, Morphism)]
lp [(Node, Morphism)] -> [(Node, Morphism)] -> [(Node, Morphism)]
forall a. [a] -> [a] -> [a]
++ [(Node
n, Morphism
vmorph)], [(Token, Token, Symbols)]
dep [(Token, Token, Symbols)]
-> [(Token, Token, Symbols)] -> [(Token, Token, Symbols)]
forall a. [a] -> [a] -> [a]
++ [(Token, Token, Symbols)]
new_dep)
      where (tok' :: Token
tok', morph' :: Morphism
morph', vmorph :: Morphism
vmorph, n :: Node
n, new_dep :: [(Token, Token, Symbols)]
new_dep) = ViewId
-> TokenInfoMap
-> ViewMap
-> (Token, Token, Symbols)
-> Morphism
-> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
processView ViewId
vi TokenInfoMap
tim ViewMap
vm (Token, Token, Symbols)
p Morphism
morph
            tok'' :: Token
tok'' = [Char] -> Token
mkSimpleId ([Char] -> Token) -> [Char] -> Token
forall a b. (a -> b) -> a -> b
$ Token -> [Char]
forall a. Show a => a -> [Char]
show Token
tok [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "," [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Token -> [Char]
forall a. Show a => a -> [Char]
show Token
tok'
processViews _ tok :: Token
tok _ _ _ (morph :: Morphism
morph, nds :: [(Node, Morphism)]
nds, deps :: [(Token, Token, Symbols)]
deps) = (Token
tok', Morphism
morph, [(Node, Morphism)]
nds, [(Token, Token, Symbols)]
deps)
      where tok' :: Token
tok' = [Char] -> Token
mkSimpleId ([Char] -> Token) -> [Char] -> Token
forall a b. (a -> b) -> a -> b
$ Node -> [Char] -> [Char]
forall a. Node -> [a] -> [a]
drop 1 ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Token -> [Char]
forall a. Show a => a -> [Char]
show Token
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 :: ViewId
-> TokenInfoMap
-> ViewMap
-> (Token, Token, Symbols)
-> Morphism
-> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
processView vi :: ViewId
vi tim :: TokenInfoMap
tim vm :: ViewMap
vm (p :: Token
p, theory :: Token
theory, ss :: Symbols
ss) morph :: Morphism
morph =
  if Token -> ViewMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Token
name ViewMap
vm
  then Token
-> Token
-> Symbols
-> (Node, Token, Morphism, [Renaming], Bool)
-> Morphism
-> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
morphismView Token
name Token
p Symbols
ss ((Node, Token, Morphism, [Renaming], Bool)
-> Token -> ViewMap -> (Node, Token, Morphism, [Renaming], Bool)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
         ([Char] -> (Node, Token, Morphism, [Renaming], Bool)
forall a. HasCallStack => [Char] -> a
error "Maude2DG.processView") Token
name ViewMap
vm) Morphism
morph
  else Token
-> Token
-> Token
-> Symbols
-> Morphism
-> TokenInfoMap
-> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
paramBinding Token
theory Token
name Token
p Symbols
ss Morphism
morph TokenInfoMap
tim
    where name :: Token
name = ViewId -> Token
forall a. HasName a => a -> Token
HasName.getName ViewId
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 :: Token
-> Token
-> Symbols
-> (Node, Token, Morphism, [Renaming], Bool)
-> Morphism
-> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
morphismView name :: Token
name p :: Token
p _ (n :: Node
n, _, vmorph :: Morphism
vmorph, rnms :: [Renaming]
rnms, True) morph :: Morphism
morph =
  (Token
name, Morphism
morph'', Morphism
vmorph', Node
n, [])
        where rnms' :: [Renaming]
rnms' = Token -> [Renaming] -> [Renaming]
qualifyRenamings Token
p [Renaming]
rnms
              morph' :: Morphism
morph' = Morphism -> [Renaming] -> Morphism
applyRenamings Morphism
morph [Renaming]
rnms'
              tgt :: Sign
tgt = Morphism -> Sign
target Morphism
vmorph
              vmorph' :: Morphism
vmorph' = Sign -> Sign -> Morphism
Maude.Morphism.inclusion Sign
tgt Sign
tgt
              ctgt :: Sign
ctgt = Morphism -> Sign
target Morphism
morph'
              usg :: Sign
usg = Sign -> Sign -> Sign
Maude.Sign.union Sign
ctgt Sign
tgt
              morph'' :: Morphism
morph'' = Sign -> Morphism -> Morphism
setTarget Sign
usg Morphism
morph'
morphismView name :: Token
name p :: Token
p ss :: Symbols
ss (n :: Node
n, th :: Token
th, morph :: Morphism
morph, rnms :: [Renaming]
rnms, False) morph1 :: Morphism
morph1 =
  (Token
name, Morphism
morph4, Morphism
vmorph', Node
n, [(Token
p, Token
th, Morphism -> Symbols -> Symbols
forall a. HasSorts a => Morphism -> a -> a
translateSorts Morphism
morph Symbols
ss)])
        where rnms' :: [Renaming]
rnms' = Token -> [Renaming] -> [Renaming]
qualifyRenamings2 Token
p [Renaming]
rnms
              morph2 :: Morphism
morph2 = Morphism -> [Renaming] -> Morphism
applyRenamings Morphism
morph1 [Renaming]
rnms'
              rnms'' :: [Renaming]
rnms'' = Token -> Symbols -> [Renaming]
createQualificationTh2Mod Token
p Symbols
ss
              morph3 :: Morphism
morph3 = Morphism -> [Renaming] -> Morphism
applyRenamings Morphism
morph2 [Renaming]
rnms''
              tgt :: Sign
tgt = Morphism -> Sign
target Morphism
morph
              vmorph :: Morphism
vmorph = Sign -> Sign -> Morphism
Maude.Morphism.inclusion Sign
tgt Sign
tgt
              vmorph' :: Morphism
vmorph' = Morphism -> [Renaming] -> Morphism
applyRenamings Morphism
vmorph [Renaming]
rnms''
              vtgt :: Sign
vtgt = Morphism -> Sign
target Morphism
vmorph'
              ctgt :: Sign
ctgt = Morphism -> Sign
target Morphism
morph3
              usg :: Sign
usg = Sign -> Sign -> Sign
Maude.Sign.union Sign
vtgt Sign
ctgt
              morph4 :: Morphism
morph4 = Sign -> Morphism -> Morphism
setTarget Sign
usg Morphism
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 :: Token
-> Token
-> Token
-> Symbols
-> Morphism
-> TokenInfoMap
-> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
paramBinding th :: Token
th view :: Token
view p :: Token
p ss :: Symbols
ss morph :: Morphism
morph tim :: TokenInfoMap
tim = (Token
view, Morphism
morph', Morphism
vmorph', Node
n, [])
        where rnms :: [Renaming]
rnms = Token -> Token -> Symbols -> [Renaming]
createQualifiedSortRenaming Token
p Token
view Symbols
ss
              morph' :: Morphism
morph' = Morphism -> [Renaming] -> Morphism
applyRenamings Morphism
morph [Renaming]
rnms
              (n :: Node
n, sg :: Sign
sg, _, _, _) = Token -> TokenInfoMap -> ProcInfo
getProcInfo Token
th TokenInfoMap
tim
              vmorph :: Morphism
vmorph = Sign -> Sign -> Morphism
Maude.Morphism.inclusion Sign
sg Sign
sg
              rnms' :: [Renaming]
rnms' = Token -> Symbols -> [Renaming]
createQualificationTh2Mod Token
p Symbols
ss
              vmorph' :: Morphism
vmorph' = Morphism -> [Renaming] -> Morphism
applyRenamings Morphism
vmorph [Renaming]
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 :: Token
-> Sign
-> TokenInfoMap
-> Symbols
-> [(Token, Token, Symbols)]
-> DGraph
-> (TokenInfoMap, DGraph)
insertNode tok :: Token
tok sg :: Sign
sg tim :: TokenInfoMap
tim ss :: Symbols
ss deps :: [(Token, Token, Symbols)]
deps dg :: DGraph
dg =
  if Token -> TokenInfoMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Token
tok TokenInfoMap
tim then (TokenInfoMap
tim, DGraph
dg) else let
    ext_sg :: ExtSign Sign Symbol
ext_sg = Maude -> Sign -> ExtSign Sign Symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign Maude
Maude Sign
sg
    gt :: G_theory
gt = ExtSign Sign Symbol
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
maudeTheory ExtSign Sign Symbol
ext_sg SigId
startSigId ThSens Sentence (AnyComorphism, BasicProof)
forall a b. ThSens a b
noSens ThId
startThId
    name :: NodeName
name = IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$ Token -> IRI
simpleIdToIRI Token
tok
    (ns :: NodeSig
ns, dg' :: DGraph
dg') = DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory DGraph
dg NodeName
name DGOrigin
DGBasic G_theory
gt
    tim' :: TokenInfoMap
tim' = Token -> ProcInfo -> TokenInfoMap -> TokenInfoMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
tok (NodeSig -> Node
getNode NodeSig
ns, Sign
sg, Symbols
ss, [(Token, Token, Symbols)]
deps, []) TokenInfoMap
tim
  in (TokenInfoMap
tim', DGraph
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 :: Node
-> TokenInfoMap
-> Token
-> Morphism
-> Sign
-> [Sentence]
-> DGraph
-> (Node, TokenInfoMap, DGraph)
insertInnerNode nod :: Node
nod tim :: TokenInfoMap
tim tok :: Token
tok morph :: Morphism
morph sg :: Sign
sg sens :: [Sentence]
sens dg :: DGraph
dg =
  if Morphism -> Bool
forall object morphism.
Category object morphism =>
morphism -> Bool
isIdentity Morphism
morph Bool -> Bool -> Bool
&& [Sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Sentence]
sens
  then let
    (fn :: Token
fn, tim' :: TokenInfoMap
tim', dg' :: DGraph
dg') = Token
-> TokenInfoMap
-> [Morphism]
-> DGraph
-> (Token, TokenInfoMap, DGraph)
insertFreeNode Token
tok TokenInfoMap
tim [] DGraph
dg
    n2 :: Node
n2 = Token -> TokenInfoMap -> Node
tokenNode Token
fn TokenInfoMap
tim'
    in (Node
n2, TokenInfoMap
tim', DGraph
dg')
  else let
    nm :: NodeName
nm = IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$ Token -> IRI
simpleIdToIRI Token
tok
    th_sens :: ThSens Sentence b
th_sens = [SenAttr Sentence [Char]] -> ThSens Sentence b
forall a b. Ord a => [Named a] -> ThSens a b
toThSens ([SenAttr Sentence [Char]] -> ThSens Sentence b)
-> [SenAttr Sentence [Char]] -> ThSens Sentence b
forall a b. (a -> b) -> a -> b
$ (Sentence -> SenAttr Sentence [Char])
-> [Sentence] -> [SenAttr Sentence [Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Sentence -> SenAttr Sentence [Char]
forall a s. a -> s -> SenAttr s a
makeNamed "") [Sentence]
sens
    sg' :: Sign
sg' = Sign -> Sign -> Sign
Maude.Sign.union Sign
sg (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
target Morphism
morph
    ext_sg :: ExtSign Sign Symbol
ext_sg = Maude -> Sign -> ExtSign Sign Symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign Maude
Maude Sign
sg'
    gt :: G_theory
gt = ExtSign Sign Symbol
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
maudeTheory ExtSign Sign Symbol
ext_sg SigId
startSigId ThSens Sentence (AnyComorphism, BasicProof)
forall b. ThSens Sentence b
th_sens ThId
startThId
    nm' :: NodeName
nm' = NodeName -> NodeName
inc NodeName
nm
    (ns :: NodeSig
ns, dg1 :: DGraph
dg1) = DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory DGraph
dg NodeName
nm' DGOrigin
DGBasic G_theory
gt
    nod2 :: Node
nod2 = NodeSig -> Node
getNode NodeSig
ns
    morph' :: Morphism
morph' = Sign -> Morphism -> Morphism
setTarget Sign
sg' Morphism
morph
    dg2 :: DGraph
dg2 = Node -> Node -> Morphism -> DGraph -> DGraph
insertDefEdgeMorphism Node
nod2 Node
nod Morphism
morph' DGraph
dg1
    -- inserting the free node
    gt2 :: G_theory
gt2 = ExtSign Sign Symbol
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
maudeTheory ExtSign Sign Symbol
ext_sg SigId
startSigId ThSens Sentence (AnyComorphism, BasicProof)
forall a b. ThSens a b
noSens ThId
startThId
    (ns2 :: NodeSig
ns2, dg3 :: DGraph
dg3) = DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory DGraph
dg2 (NodeName -> NodeName
inc NodeName
nm') DGOrigin
DGBasic G_theory
gt2
    nod3 :: Node
nod3 = NodeSig -> Node
getNode NodeSig
ns2
    -- inserting the free link
    inc_sg :: Morphism
inc_sg = Sign -> Sign -> Morphism
Maude.Morphism.inclusion Sign
Maude.Sign.empty Sign
sg'
    mor :: G_morphism
mor = Maude -> Morphism -> MorId -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> MorId -> G_morphism
G_morphism Maude
Maude Morphism
inc_sg MorId
startMorId
    dgt :: DGLinkType
dgt = FreeOrCofree -> MaybeNode -> DGLinkType
FreeOrCofreeDefLink FreeOrCofree
NPFree (MaybeNode -> DGLinkType) -> MaybeNode -> DGLinkType
forall a b. (a -> b) -> a -> b
$ AnyLogic -> MaybeNode
EmptyNode (Maude -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic Maude
Maude)
    edg :: DGLinkLab
edg = GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink (G_morphism -> GMorphism
gEmbed G_morphism
mor) DGLinkType
dgt DGLinkOrigin
SeeTarget
    dg4 :: DGraph
dg4 = (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a, b) -> b
snd ((LEdge DGLinkLab, DGraph) -> DGraph)
-> (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Node
nod2, Node
nod3, DGLinkLab
edg) DGraph
dg3
    in (Node
nod3, TokenInfoMap
tim, DGraph
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 :: Node -> [(Node, Morphism)] -> Sign -> DGraph -> DGraph
insertDefEdgesMorphism _ [] _ dg :: DGraph
dg = DGraph
dg
insertDefEdgesMorphism n1 :: Node
n1 ((n2 :: Node
n2, morph :: Morphism
morph) : views :: [(Node, Morphism)]
views) sg2 :: Sign
sg2 dg :: DGraph
dg =
  Node -> [(Node, Morphism)] -> Sign -> DGraph -> DGraph
insertDefEdgesMorphism Node
n1 [(Node, Morphism)]
views Sign
sg2 DGraph
dg'
                  where morph' :: Morphism
morph' = Sign -> Morphism -> Morphism
setTarget Sign
sg2 Morphism
morph
                        dg' :: DGraph
dg' = Node -> Node -> Morphism -> DGraph -> DGraph
insertDefEdgeMorphism Node
n1 Node
n2 Morphism
morph' DGraph
dg

-- | inserts a definition link between the nodes with the given morphism
insertDefEdgeMorphism :: Node -> Node -> Morphism -> DGraph -> DGraph
insertDefEdgeMorphism :: Node -> Node -> Morphism -> DGraph -> DGraph
insertDefEdgeMorphism n1 :: Node
n1 n2 :: Node
n2 = Node -> Node -> DGLinkType -> Morphism -> DGraph -> DGraph
insertEdgeMorphism Node
n1 Node
n2 DGLinkType
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 :: Token -> Node -> Node -> Morphism -> DGraph -> DGraph
insertThmEdgeMorphism name :: Token
name n1 :: Node
n1 n2 :: Node
n2 morph :: Morphism
morph dg :: DGraph
dg = (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a, b) -> b
snd ((LEdge DGLinkLab, DGraph) -> DGraph)
-> (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Node
n2, Node
n1, DGLinkLab
edg) DGraph
dg
                     where mor :: G_morphism
mor = Maude -> Morphism -> MorId -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> MorId -> G_morphism
G_morphism Maude
Maude Morphism
morph MorId
startMorId
                           edg :: DGLinkLab
edg = GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink (G_morphism -> GMorphism
gEmbed G_morphism
mor) DGLinkType
globalThm
                                 (IRI -> Fitted -> DGLinkOrigin
DGLinkView (Token -> IRI
simpleIdToIRI Token
name) (Fitted -> DGLinkOrigin) -> Fitted -> DGLinkOrigin
forall a b. (a -> b) -> a -> b
$ [G_mapping] -> Fitted
Fitted [])

-- | inserts a link between the nodes with the given morphism
insertEdgeMorphism :: Node -> Node -> DGLinkType -> Morphism -> DGraph -> DGraph
insertEdgeMorphism :: Node -> Node -> DGLinkType -> Morphism -> DGraph -> DGraph
insertEdgeMorphism n1 :: Node
n1 n2 :: Node
n2 lt :: DGLinkType
lt morph :: Morphism
morph dg :: DGraph
dg = (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a, b) -> b
snd ((LEdge DGLinkLab, DGraph) -> DGraph)
-> (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Node
n2, Node
n1, DGLinkLab
edg) DGraph
dg
    where mor :: G_morphism
mor = Maude -> Morphism -> MorId -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> MorId -> G_morphism
G_morphism Maude
Maude Morphism
morph MorId
startMorId
          edg :: DGLinkLab
edg = GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink (G_morphism -> GMorphism
gEmbed G_morphism
mor) DGLinkType
lt DGLinkOrigin
SeeTarget

-- | inserts a free definition link between the nodes with the given name
insertFreeEdge :: Token -> Token -> TokenInfoMap -> DGraph -> DGraph
insertFreeEdge :: Token -> Token -> TokenInfoMap -> DGraph -> DGraph
insertFreeEdge tok1 :: Token
tok1 tok2 :: Token
tok2 tim :: TokenInfoMap
tim = Node -> Node -> DGLinkType -> Morphism -> DGraph -> DGraph
insertEdgeMorphism Node
n1 Node
n2
  (FreeOrCofree -> MaybeNode -> DGLinkType
FreeOrCofreeDefLink FreeOrCofree
NPFree (MaybeNode -> DGLinkType) -> MaybeNode -> DGLinkType
forall a b. (a -> b) -> a -> b
$ AnyLogic -> MaybeNode
EmptyNode (AnyLogic -> MaybeNode) -> AnyLogic -> MaybeNode
forall a b. (a -> b) -> a -> b
$ Maude -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic Maude
Maude)
  (Sign -> Sign -> Morphism
Maude.Morphism.inclusion Sign
Maude.Sign.empty Sign
sg2)
    -- currently, the empty sign is used in the inclusion instead of sg1
    where n1 :: Node
n1 = Token -> TokenInfoMap -> Node
tokenNode Token
tok1 TokenInfoMap
tim
          (n2 :: Node
n2, sg2 :: Sign
sg2, _, _, _) = Token -> TokenInfoMap -> ProcInfo
getProcInfo Token
tok2 TokenInfoMap
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 :: Token -> Token -> TokenInfoMap -> Morphism -> DGraph -> DGraph
insertFreeEdgeMor tok1 :: Token
tok1 tok2 :: Token
tok2 tim :: TokenInfoMap
tim mor :: Morphism
mor dg :: DGraph
dg = (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a, b) -> b
snd ((LEdge DGLinkLab, DGraph) -> DGraph)
-> (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Node
n2, Node
n1, DGLinkLab
edg) DGraph
dg
    where n1 :: Node
n1 = Token -> TokenInfoMap -> Node
tokenNode Token
tok1 TokenInfoMap
tim
          n2 :: Node
n2 = Token -> TokenInfoMap -> Node
tokenNode Token
tok2 TokenInfoMap
tim
          mor' :: G_morphism
mor' = Maude -> Morphism -> MorId -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> MorId -> G_morphism
G_morphism Maude
Maude Morphism
mor MorId
startMorId
          dgt :: DGLinkType
dgt = FreeOrCofree -> MaybeNode -> DGLinkType
FreeOrCofreeDefLink FreeOrCofree
NPFree (MaybeNode -> DGLinkType) -> MaybeNode -> DGLinkType
forall a b. (a -> b) -> a -> b
$ AnyLogic -> MaybeNode
EmptyNode (Maude -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic Maude
Maude)
          edg :: DGLinkLab
edg = GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink (G_morphism -> GMorphism
gEmbed G_morphism
mor') DGLinkType
dgt DGLinkOrigin
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 :: Token
-> TokenInfoMap
-> [Morphism]
-> DGraph
-> (Token, TokenInfoMap, DGraph)
insertFreeNode t :: Token
t tim :: TokenInfoMap
tim morphs :: [Morphism]
morphs dg :: DGraph
dg = (Token
t', TokenInfoMap
tim', DGraph
dg'') where
    t' :: Token
t' = Token -> Token
mkFreeName Token
t
    b :: Bool
b = Token -> TokenInfoMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Token
t' TokenInfoMap
tim
    (tim' :: TokenInfoMap
tim', dg' :: DGraph
dg') = if Bool
b then (TokenInfoMap
tim, DGraph
dg) else
      Token
-> TokenInfoMap -> ProcInfo -> DGraph -> (TokenInfoMap, DGraph)
insertFreeNode2 Token
t' TokenInfoMap
tim (Token -> TokenInfoMap -> ProcInfo
getProcInfo Token
t TokenInfoMap
tim) DGraph
dg
    dg'' :: DGraph
dg'' | Bool
b = DGraph
dg'
         | [Morphism] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Morphism]
morphs = Token -> Token -> TokenInfoMap -> DGraph -> DGraph
insertFreeEdge Token
t' Token
t TokenInfoMap
tim' DGraph
dg'
         | Bool
otherwise = Token -> Token -> TokenInfoMap -> Morphism -> DGraph -> DGraph
insertFreeEdgeMor Token
t' Token
t TokenInfoMap
tim' ([Morphism] -> Morphism
morphismUnion [Morphism]
morphs) DGraph
dg'

morphismUnion :: [Morphism] -> Morphism
morphismUnion :: [Morphism] -> Morphism
morphismUnion = (Morphism -> Morphism -> Morphism)
-> Morphism -> [Morphism] -> Morphism
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Morphism -> Morphism -> Morphism
Maude.Morphism.union Morphism
Maude.Morphism.empty

-- | auxiliary function in charge of creating M' when it does not exist
insertFreeNode2 :: Token -> TokenInfoMap -> ProcInfo -> DGraph
  -> (TokenInfoMap, DGraph)
insertFreeNode2 :: Token
-> TokenInfoMap -> ProcInfo -> DGraph -> (TokenInfoMap, DGraph)
insertFreeNode2 t :: Token
t tim :: TokenInfoMap
tim (_, sg :: Sign
sg, _, _, _) dg :: DGraph
dg = (TokenInfoMap
tim', DGraph
dg')
              where ext_sg :: ExtSign Sign Symbol
ext_sg = Maude -> Sign -> ExtSign Sign Symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign Maude
Maude Sign
sg
                    gt :: G_theory
gt = ExtSign Sign Symbol
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
maudeTheory ExtSign Sign Symbol
ext_sg SigId
startSigId ThSens Sentence (AnyComorphism, BasicProof)
forall a b. ThSens a b
noSens ThId
startThId
                    name :: NodeName
name = IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$ Token -> IRI
simpleIdToIRI Token
t
                    (ns :: NodeSig
ns, dg' :: DGraph
dg') = DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory DGraph
dg NodeName
name DGOrigin
DGBasic G_theory
gt
                    tim' :: TokenInfoMap
tim' = Token -> ProcInfo -> TokenInfoMap -> TokenInfoMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
t (NodeSig -> Node
getNode NodeSig
ns, Sign
sg, [], [], []) TokenInfoMap
tim

{- | Given the identifier of a module, generates the identifier for the module
with the ``freeness'' constraint -}
mkFreeName :: Token -> Token
mkFreeName :: Token -> Token
mkFreeName = [Char] -> Token
mkSimpleId ([Char] -> Token) -> (Token -> [Char]) -> Token -> Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "'") ([Char] -> [Char]) -> (Token -> [Char]) -> Token -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> [Char]
forall a. Show a => a -> [Char]
show

-- | extracts the parameters of a Maude module
getParams :: Module -> [Parameter]
getParams :: Module -> [Parameter]
getParams (Module _ params :: [Parameter]
params _) = [Parameter]
params

-- | extracts the importation statements and the sorts from a module definition
getImportsSorts :: Module -> ([Import], Symbols)
getImportsSorts :: Module -> ([Import], Symbols)
getImportsSorts (Module _ _ stmts :: [Statement]
stmts) = [Statement] -> ([Import], Symbols) -> ([Import], Symbols)
getImportsSortsStmnts [Statement]
stmts ([], [])

-- | traverses the statements accumulating the importations and the sorts
getImportsSortsStmnts :: [Statement] -> ([Import], Symbols)
  -> ([Import], Symbols)
getImportsSortsStmnts :: [Statement] -> ([Import], Symbols) -> ([Import], Symbols)
getImportsSortsStmnts [] p :: ([Import], Symbols)
p = ([Import], Symbols)
p
getImportsSortsStmnts (ImportStmnt imp :: Import
imp : stmts :: [Statement]
stmts) (is :: [Import]
is, ss :: Symbols
ss) =
    [Statement] -> ([Import], Symbols) -> ([Import], Symbols)
getImportsSortsStmnts [Statement]
stmts (Import
imp Import -> [Import] -> [Import]
forall a. a -> [a] -> [a]
: [Import]
is, Symbols
ss)
getImportsSortsStmnts (SortStmnt s :: Sort
s : stmts :: [Statement]
stmts) (is :: [Import]
is, ss :: Symbols
ss) =
    [Statement] -> ([Import], Symbols) -> ([Import], Symbols)
getImportsSortsStmnts [Statement]
stmts ([Import]
is, Token -> Symbol
Sort (Sort -> Token
forall a. HasName a => a -> Token
HasName.getName Sort
s) Symbol -> Symbols -> Symbols
forall a. a -> [a] -> [a]
: Symbols
ss)
getImportsSortsStmnts (_ : stmts :: [Statement]
stmts) p :: ([Import], Symbols)
p = [Statement] -> ([Import], Symbols) -> ([Import], Symbols)
getImportsSortsStmnts [Statement]
stmts ([Import], Symbols)
p

-- | builds the development graph of the specified Maude file
directMaudeParsing :: HetcatsOpts -> FilePath -> IO (DGraph, DGraph)
directMaudeParsing :: HetcatsOpts -> [Char] -> IO (DGraph, DGraph)
directMaudeParsing opts :: HetcatsOpts
opts fp :: [Char]
fp = do
    HetcatsOpts -> Node -> [Char] -> IO ()
putIfVerbose HetcatsOpts
opts 2 ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ "Reading file " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fp
    Either ParseError ParseResult
ns <- [Char] -> IO (Either ParseError ParseResult)
parse [Char]
fp
    let ns' :: ParseResult
ns' = (ParseError -> ParseResult)
-> (ParseResult -> ParseResult)
-> Either ParseError ParseResult
-> ParseResult
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (ParseResult -> ParseError -> ParseResult
forall a b. a -> b -> a
const []) ParseResult -> ParseResult
forall a. a -> a
id Either ParseError ParseResult
ns
    (inString :: [Char]
inString, hIn :: Handle
hIn, hOut :: Handle
hOut, hErr :: Handle
hErr, procH :: ProcessHandle
procH) <- IO ([Char], Handle, Handle, Handle, ProcessHandle)
runMaude
    Maybe ExitCode
exitCode <- ProcessHandle -> IO (Maybe ExitCode)
getProcessExitCode ProcessHandle
procH
    case Maybe ExitCode
exitCode of
      Nothing -> do
              Handle -> [Char] -> IO ()
maudePutStrLn Handle
hIn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ "load " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fp
              Handle -> [Char] -> IO ()
maudePutStrLn Handle
hIn [Char]
inString
              [Spec]
psps <- HetcatsOpts -> Handle -> Handle -> IO [Spec]
predefinedSpecs HetcatsOpts
opts Handle
hIn Handle
hOut
              [Spec]
sps <- HetcatsOpts -> Handle -> Handle -> ParseResult -> IO [Spec]
traverseSpecs HetcatsOpts
opts Handle
hIn Handle
hOut ParseResult
ns'
              (ok :: Bool
ok, errs :: [Char]
errs) <- Handle -> IO (Bool, [Char])
getErrors Handle
hErr
              ProcessHandle -> IO ()
terminateProcess ProcessHandle
procH
              if Bool
ok
                  then (DGraph, DGraph) -> IO (DGraph, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ((DGraph, DGraph) -> IO (DGraph, DGraph))
-> (DGraph, DGraph) -> IO (DGraph, DGraph)
forall a b. (a -> b) -> a -> b
$ [Spec] -> [Spec] -> (DGraph, DGraph)
maude2DG [Spec]
psps [Spec]
sps
                  else [Char] -> IO (DGraph, DGraph)
forall a. HasCallStack => [Char] -> a
error [Char]
errs
      Just ExitSuccess -> [Char] -> IO (DGraph, DGraph)
forall a. HasCallStack => [Char] -> a
error "maude terminated immediately"
      Just (ExitFailure i :: Node
i) ->
          [Char] -> IO (DGraph, DGraph)
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO (DGraph, DGraph)) -> [Char] -> IO (DGraph, DGraph)
forall a b. (a -> b) -> a -> b
$ "calling maude failed with exitCode: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Node -> [Char]
forall a. Show a => a -> [Char]
show Node
i

maude2DG :: [Spec] -> [Spec] -> (DGraph, DGraph)
maude2DG :: [Spec] -> [Spec] -> (DGraph, DGraph)
maude2DG psps :: [Spec]
psps sps :: [Spec]
sps = (DGraph
dg1, DGraph
dg2) where
  (_, tim :: TokenInfoMap
tim, vm :: ViewMap
vm, tks :: [Token]
tks, dg1 :: DGraph
dg1) =
    [Spec]
-> DGraph
-> TokenInfoMap
-> TokenInfoMap
-> ViewMap
-> [Token]
-> DGraph
-> InsSpecRes
insertSpecs [Spec]
psps DGraph
emptyDG TokenInfoMap
forall k a. Map k a
Map.empty TokenInfoMap
forall k a. Map k a
Map.empty ViewMap
forall k a. Map k a
Map.empty [] DGraph
emptyDG
  (_, _, _, _, dg2 :: DGraph
dg2) = [Spec]
-> DGraph
-> TokenInfoMap
-> TokenInfoMap
-> ViewMap
-> [Token]
-> DGraph
-> InsSpecRes
insertSpecs [Spec]
sps DGraph
dg1 TokenInfoMap
tim TokenInfoMap
forall k a. Map k a
Map.empty ViewMap
vm [Token]
tks DGraph
emptyDG

-- | list of names of the predefined modules
predefined :: [NamedSpec]
predefined :: ParseResult
predefined =
  [ [Char] -> NamedSpec
ModName "TRUTH-VALUE"
  , [Char] -> NamedSpec
ModName "BOOL-OPS"
  , [Char] -> NamedSpec
ModName "TRUTH"
  , [Char] -> NamedSpec
ModName "BOOL"
  , [Char] -> NamedSpec
ModName "EXT-BOOL"
  , [Char] -> NamedSpec
ModName "NAT"
  , [Char] -> NamedSpec
ModName "INT"
  , [Char] -> NamedSpec
ModName "RAT"
  , [Char] -> NamedSpec
ModName "FLOAT"
  , [Char] -> NamedSpec
ModName "STRING"
  , [Char] -> NamedSpec
ModName "CONVERSION"
  , [Char] -> NamedSpec
ModName "RANDOM"
  , [Char] -> NamedSpec
ModName "QID"
  , [Char] -> NamedSpec
ModName "TRIV"
  , [Char] -> NamedSpec
ViewName "TRIV"
  , [Char] -> NamedSpec
ViewName "Bool"
  , [Char] -> NamedSpec
ViewName "Nat"
  , [Char] -> NamedSpec
ViewName "Int"
  , [Char] -> NamedSpec
ViewName "Rat"
  , [Char] -> NamedSpec
ViewName "Float"
  , [Char] -> NamedSpec
ViewName "String"
  , [Char] -> NamedSpec
ViewName "Qid"
  , [Char] -> NamedSpec
ModName "STRICT-WEAK-ORDER"
  , [Char] -> NamedSpec
ViewName "STRICT-WEAK-ORDER"
  , [Char] -> NamedSpec
ModName "STRICT-TOTAL-ORDER"
  , [Char] -> NamedSpec
ViewName "STRICT-TOTAL-ORDER"
  , [Char] -> NamedSpec
ViewName "Nat<"
  , [Char] -> NamedSpec
ViewName "Int<"
  , [Char] -> NamedSpec
ViewName "Rat<"
  , [Char] -> NamedSpec
ViewName "Float<"
  , [Char] -> NamedSpec
ViewName "String<"
  , [Char] -> NamedSpec
ModName "TOTAL-PREORDER"
  , [Char] -> NamedSpec
ViewName "TOTAL-PREORDER"
  , [Char] -> NamedSpec
ModName "TOTAL-ORDER"
  , [Char] -> NamedSpec
ViewName "TOTAL-ORDER"
  , [Char] -> NamedSpec
ViewName "Nat<="
  , [Char] -> NamedSpec
ViewName "Int<="
  , [Char] -> NamedSpec
ViewName "Rat<="
  , [Char] -> NamedSpec
ViewName "Float<="
  , [Char] -> NamedSpec
ViewName "String<="
  , [Char] -> NamedSpec
ModName "DEFAULT"
  , [Char] -> NamedSpec
ViewName "DEFAULT"
  , [Char] -> NamedSpec
ViewName "Nat0"
  , [Char] -> NamedSpec
ViewName "Int0"
  , [Char] -> NamedSpec
ViewName "Rat0"
  , [Char] -> NamedSpec
ViewName "Float0"
  , [Char] -> NamedSpec
ViewName "String0"
  , [Char] -> NamedSpec
ViewName "Qid0"
  , [Char] -> NamedSpec
ModName "LIST"
  , [Char] -> NamedSpec
ModName "WEAKLY-SORTABLE-LIST"
  , [Char] -> NamedSpec
ModName "SORTABLE-LIST"
  , [Char] -> NamedSpec
ModName "WEAKLY-SORTABLE-LIST'"
  , [Char] -> NamedSpec
ModName "SORTABLE-LIST'"
  , [Char] -> NamedSpec
ModName "SET"
  , [Char] -> NamedSpec
ModName "LIST-AND-SET"
  , [Char] -> NamedSpec
ModName "SORTABLE-LIST-AND-SET"
  , [Char] -> NamedSpec
ModName "SORTABLE-LIST-AND-SET'"
  , [Char] -> NamedSpec
ModName "LIST*"
  , [Char] -> NamedSpec
ModName "SET*"
  , [Char] -> NamedSpec
ModName "MAP"
  , [Char] -> NamedSpec
ModName "ARRAY"
  , [Char] -> NamedSpec
ModName "NAT-LIST"
  , [Char] -> NamedSpec
ModName "QID-LIST"
  , [Char] -> NamedSpec
ModName "QID-SET"
  , [Char] -> NamedSpec
ModName "META-TERM"
  , [Char] -> NamedSpec
ModName "META-MODULE"
  , [Char] -> NamedSpec
ModName "META-VIEW"
  , [Char] -> NamedSpec
ModName "META-LEVEL"
  , [Char] -> NamedSpec
ModName "COUNTER"
  , [Char] -> NamedSpec
ModName "LOOP-MODE"
  , [Char] -> NamedSpec
ModName "CONFIGURATION" ]

{- | returns the specifications of the predefined modules by passing as
parameter the list of names -}
predefinedSpecs :: HetcatsOpts -> Handle -> Handle -> IO [Spec]
predefinedSpecs :: HetcatsOpts -> Handle -> Handle -> IO [Spec]
predefinedSpecs opts :: HetcatsOpts
opts hIn :: Handle
hIn hOut :: Handle
hOut = HetcatsOpts -> Handle -> Handle -> ParseResult -> IO [Spec]
traverseSpecs HetcatsOpts
opts Handle
hIn Handle
hOut ParseResult
predefined

traverseSpecs :: HetcatsOpts -> Handle -> Handle -> [NamedSpec] -> IO [Spec]
traverseSpecs :: HetcatsOpts -> Handle -> Handle -> ParseResult -> IO [Spec]
traverseSpecs opts :: HetcatsOpts
opts hIn :: Handle
hIn hOut :: Handle
hOut = ([Maybe Spec] -> [Spec]) -> IO [Maybe Spec] -> IO [Spec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe Spec] -> [Spec]
forall a. [Maybe a] -> [a]
catMaybes (IO [Maybe Spec] -> IO [Spec])
-> (ParseResult -> IO [Maybe Spec]) -> ParseResult -> IO [Spec]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedSpec -> IO (Maybe Spec)) -> ParseResult -> IO [Maybe Spec]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (HetcatsOpts -> Handle -> Handle -> NamedSpec -> IO (Maybe Spec)
traverseSpec HetcatsOpts
opts Handle
hIn Handle
hOut)

-- | returns the specifications of the predefined modules
traverseSpec :: HetcatsOpts -> Handle -> Handle -> NamedSpec -> IO (Maybe Spec)
traverseSpec :: HetcatsOpts -> Handle -> Handle -> NamedSpec -> IO (Maybe Spec)
traverseSpec opts :: HetcatsOpts
opts hIn :: Handle
hIn hOut :: Handle
hOut ns :: NamedSpec
ns = do
  let args :: [Char]
args = case NamedSpec
ns of
          ModName n :: [Char]
n -> "(hets " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
n
          ViewName n :: [Char]
n -> "(hetsView " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
n
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ " .)"
  HetcatsOpts -> Node -> [Char] -> IO ()
putIfVerbose HetcatsOpts
opts 4 ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ "maude input: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
args
  Handle -> [Char] -> IO ()
maudePutStrLn Handle
hIn [Char]
args
  [Char]
sOutput <- Handle -> [Char] -> Bool -> IO [Char]
getAllSpec Handle
hOut "" Bool
False
  let stringSpec :: [Char]
stringSpec = [Char] -> [Char]
findSpec [Char]
sOutput
  case [Char] -> Maybe Spec
forall a. Read a => [Char] -> Maybe a
readMaybe [Char]
stringSpec of
    Nothing -> do
      [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ "failed to read " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
args [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ":\n"
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ if (Char -> Bool) -> [Char] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace [Char]
stringSpec then [Char]
sOutput else [Char]
stringSpec
      Maybe Spec -> IO (Maybe Spec)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Spec
forall a. Maybe a
Nothing
    ms :: Maybe Spec
ms -> Maybe Spec -> IO (Maybe Spec)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Spec
ms

-- | returns the parameter names
paramNames :: [Parameter] -> [Token]
paramNames :: [Parameter] -> [Token]
paramNames = (Parameter -> Token) -> [Parameter] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map ((Parameter -> Token) -> [Parameter] -> [Token])
-> (Parameter -> Token) -> [Parameter] -> [Token]
forall a b. (a -> b) -> a -> b
$ \ (Parameter s :: Sort
s _) -> Sort -> Token
forall a. HasName a => a -> Token
HasName.getName Sort
s

{- | returns the sorts (second argument of the pair) that contain any of the
parameters given as first argument -}
getSortsParameterizedBy :: [Token] -> Symbols -> [ParamSort]
getSortsParameterizedBy :: [Token] -> Symbols -> [ParamSort]
getSortsParameterizedBy ps :: [Token]
ps = (ParamSort -> Bool) -> [ParamSort] -> [ParamSort]
forall a. (a -> Bool) -> [a] -> [a]
filter ParamSort -> Bool
forall a a. (a, [a]) -> Bool
f ([ParamSort] -> [ParamSort])
-> (Symbols -> [ParamSort]) -> Symbols -> [ParamSort]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> ParamSort) -> Symbols -> [ParamSort]
forall a b. (a -> b) -> [a] -> [b]
map ([Token] -> Symbol -> ParamSort
forall a. HasName a => [Token] -> a -> (a, [Token])
g [Token]
ps)
           where f :: (a, [a]) -> Bool
f = Bool -> Bool
not (Bool -> Bool) -> ((a, [a]) -> Bool) -> (a, [a]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([a] -> Bool) -> ((a, [a]) -> [a]) -> (a, [a]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, [a]) -> [a]
forall a b. (a, b) -> b
snd
                 g :: [Token] -> a -> (a, [Token])
g pss :: [Token]
pss x :: a
x = let
                         params :: [Token]
params = Token -> [Token]
getSortParams (Token -> [Token]) -> Token -> [Token]
forall a b. (a -> b) -> a -> b
$ a -> Token
forall a. HasName a => a -> Token
HasName.getName a
x
                         in (a
x, [Token] -> [Token] -> [Token]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Token]
params [Token]
pss)

{- | extracts the parameters of the given sort
For example, getSortParams List{X} = [X]
List{X}{Y, Y} = [Y,Z] -}
getSortParams :: Token -> [Token]
getSortParams :: Token -> [Token]
getSortParams t :: Token
t = [Char] -> [Token]
getSortParamsString ([Char] -> [Token]) -> [Char] -> [Token]
forall a b. (a -> b) -> a -> b
$ Token -> [Char]
forall a. Show a => a -> [Char]
show Token
t

-- | traverses a String looking for the last curly braces
getSortParamsString :: String -> [Token]
getSortParamsString :: [Char] -> [Token]
getSortParamsString [] = []
getSortParamsString ('{' : cs :: [Char]
cs) = if [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
sps
                                 then [Char] -> [Char] -> [Token]
getSortParamsStringAux [Char]
cs ""
                                 else [Token]
sps
            where sps :: [Token]
sps = [Char] -> [Token]
getSortParamsString [Char]
cs
getSortParamsString (_ : cs :: [Char]
cs) = [Char] -> [Token]
getSortParamsString [Char]
cs

-- | traverses a String keeping the token separated by commas
getSortParamsStringAux :: String -> String -> [Token]
getSortParamsStringAux :: [Char] -> [Char] -> [Token]
getSortParamsStringAux ('`' : ',' : cs :: [Char]
cs) st :: [Char]
st =
  [Char] -> Token
mkSimpleId [Char]
st Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Char] -> [Char] -> [Token]
getSortParamsStringAux [Char]
cs ""
getSortParamsStringAux ('`' : '}' : []) st :: [Char]
st = [[Char] -> Token
mkSimpleId [Char]
st]
getSortParamsStringAux (' ' : cs :: [Char]
cs) st :: [Char]
st = [Char] -> [Char] -> [Token]
getSortParamsStringAux [Char]
cs [Char]
st
getSortParamsStringAux (c :: Char
c : cs :: [Char]
cs) st :: [Char]
st = [Char] -> [Char] -> [Token]
getSortParamsStringAux [Char]
cs ([Char]
st [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char
c])
getSortParamsStringAux [] st :: [Char]
st = [[Char] -> Token
mkSimpleId [Char]
st]

-- | checks if the target of the view is completely instantiated (to modules)
isInstantiated :: [Token] -> ModExp -> Bool
isInstantiated :: [Token] -> ModExp -> Bool
isInstantiated ths :: [Token]
ths (ModExp modExp :: ModId
modExp) = Token -> [Token] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (ModId -> Token
forall a. HasName a => a -> Token
HasName.getName ModId
modExp) [Token]
ths
isInstantiated ths :: [Token]
ths (SummationModExp me1 :: ModExp
me1 me2 :: ModExp
me2) = [Token] -> ModExp -> Bool
isInstantiated [Token]
ths ModExp
me1 Bool -> Bool -> Bool
&&
                                               [Token] -> ModExp -> Bool
isInstantiated [Token]
ths ModExp
me2
isInstantiated ths :: [Token]
ths (RenamingModExp modExp :: ModExp
modExp _) = [Token] -> ModExp -> Bool
isInstantiated [Token]
ths ModExp
modExp
isInstantiated _ (InstantiationModExp _ _) = Bool
True

-- | rename the parameterized sorts and computes if they are still parameterized
applyRenamingParamSorts :: SymbolMap -> [ParamSort] -> [ParamSort]
applyRenamingParamSorts :: SymbolMap -> [ParamSort] -> [ParamSort]
applyRenamingParamSorts sm :: SymbolMap
sm = (ParamSort -> [ParamSort] -> [ParamSort])
-> [ParamSort] -> [ParamSort] -> [ParamSort]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SymbolMap -> ParamSort -> [ParamSort] -> [ParamSort]
applyRenamingParamSort SymbolMap
sm) []

applyRenamingParamSort :: SymbolMap -> ParamSort -> [ParamSort] -> [ParamSort]
applyRenamingParamSort :: SymbolMap -> ParamSort -> [ParamSort] -> [ParamSort]
applyRenamingParamSort sm :: SymbolMap
sm (tok :: Symbol
tok, params :: [Token]
params) acc :: [ParamSort]
acc = case Symbol -> SymbolMap -> Maybe Symbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
tok SymbolMap
sm of
    Nothing -> (Symbol
tok, [Token]
params) ParamSort -> [ParamSort] -> [ParamSort]
forall a. a -> [a] -> [a]
: [ParamSort]
acc
    Just tok' :: Symbol
tok' -> [Token] -> Symbols -> [ParamSort]
getSortsParameterizedBy [Token]
params [Symbol
tok'] [ParamSort] -> [ParamSort] -> [ParamSort]
forall a. [a] -> [a] -> [a]
++ [ParamSort]
acc

-- | returns the first element from the triple
fstTpl :: (a, b, c) -> a
fstTpl :: (a, b, c) -> a
fstTpl (a :: a
a, _, _) = a
a

{- | instantiate the parametric sorts
ParamNames -> ViewName -> Map of views -> Parametricsorts -}
instantiateSorts :: [Token] -> [Token] -> ViewMap -> Morphism -> [ParamSort]
                    -> ([ParamSort], Morphism)
instantiateSorts :: [Token]
-> [Token]
-> ViewMap
-> Morphism
-> [ParamSort]
-> ([ParamSort], Morphism)
instantiateSorts _ _ _ morph :: Morphism
morph [] = ([], Morphism
morph)
instantiateSorts params :: [Token]
params views :: [Token]
views vm :: ViewMap
vm morph :: Morphism
morph (ps :: ParamSort
ps : pss :: [ParamSort]
pss) = ([ParamSort]
nps'' [ParamSort] -> [ParamSort] -> [ParamSort]
forall a. [a] -> [a] -> [a]
++ [ParamSort]
res_ps, Morphism
res_morph)
        where np4s :: [Token]
np4s = [Token] -> [Token] -> ViewMap -> [Token]
newParamers4sorts [Token]
params [Token]
views ViewMap
vm
              nps :: ParamSort
nps = ParamSort -> [Token] -> [Token] -> ParamSort
instantiateSort ParamSort
ps [Token]
params [Token]
views
              nps' :: ParamSort
nps' = ParamSort -> [Token] -> ParamSort
addNewParams2sort ParamSort
nps [Token]
np4s
              nps'' :: [ParamSort]
nps'' = if [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ParamSort -> [Token]
forall a b. (a, b) -> b
snd ParamSort
nps') then [] else [ParamSort
nps']
              morph' :: Morphism
morph' = Symbol -> Symbol -> Morphism -> Morphism
extendWithSortRenaming (ParamSort -> Symbol
forall a b. (a, b) -> a
fst ParamSort
ps) (ParamSort -> Symbol
forall a b. (a, b) -> a
fst ParamSort
nps') Morphism
morph
              (res_ps :: [ParamSort]
res_ps, res_morph :: Morphism
res_morph) = [Token]
-> [Token]
-> ViewMap
-> Morphism
-> [ParamSort]
-> ([ParamSort], Morphism)
instantiateSorts [Token]
params [Token]
views ViewMap
vm Morphism
morph' [ParamSort]
pss

-- | computes the theories that have to be further instantiated
newParamers4sorts :: [Token] -> [Token] -> ViewMap -> [Token]
newParamers4sorts :: [Token] -> [Token] -> ViewMap -> [Token]
newParamers4sorts (param :: Token
param : ps :: [Token]
ps) (view :: Token
view : vs :: [Token]
vs) vm :: ViewMap
vm = case Token -> ViewMap -> Maybe (Node, Token, Morphism, [Renaming], Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Token
view ViewMap
vm of
    Nothing -> [Token] -> [Token] -> ViewMap -> [Token]
newParamers4sorts [Token]
ps [Token]
vs ViewMap
vm
    Just (_, _, _, _, inst :: Bool
inst) -> let
                 param' :: [Token]
param' = if Bool
inst
                          then []
                          else [Token
param]
                in [Token]
param' [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token] -> [Token] -> ViewMap -> [Token]
newParamers4sorts [Token]
ps [Token]
vs ViewMap
vm
newParamers4sorts _ _ _ = []

-- | creates a new parameterized sort
addNewParams2sort :: ParamSort -> [Token] -> ParamSort
addNewParams2sort :: ParamSort -> [Token] -> ParamSort
addNewParams2sort (Sort tok :: Token
tok, _) lps :: [Token]
lps@(_ : _) = (Token -> Symbol
Sort Token
tok', [Token]
lps) where
    tok' :: Token
tok' = [Char] -> Token
mkSimpleId ([Char] -> Token) -> [Char] -> Token
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Token -> [Char]
forall a. Show a => a -> [Char]
show Token
tok, "`{", [Token] -> [Char]
printNewParams4sort [Token]
lps, "`}"]
addNewParams2sort (Kind tok :: Token
tok, _) lps :: [Token]
lps@(_ : _) = (Token -> Symbol
Kind Token
tok', [Token]
lps) where
    tok' :: Token
tok' = [Char] -> Token
mkSimpleId ([Char] -> Token) -> [Char] -> Token
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Token -> [Char]
forall a. Show a => a -> [Char]
show Token
tok, "`{", [Token] -> [Char]
printNewParams4sort [Token]
lps, "`}"]
addNewParams2sort (ps :: Symbol
ps, _) _ = (Symbol
ps, [])

-- | introduces commas between the tokens
printNewParams4sort :: [Token] -> String
printNewParams4sort :: [Token] -> [Char]
printNewParams4sort [] = ""
printNewParams4sort [p :: Token
p] = Token -> [Char]
forall a. Show a => a -> [Char]
show Token
p
printNewParams4sort (p :: Token
p : ps :: [Token]
ps) = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Token -> [Char]
forall a. Show a => a -> [Char]
show Token
p, "`,", [Token] -> [Char]
printNewParams4sort [Token]
ps]

{- | instantiate a sort
Params: Parameterized sort -> Parameter to be replaced -> New name of the
parameter -}
instantiateSort :: ParamSort -> [Token] -> [Token] -> ParamSort
instantiateSort :: ParamSort -> [Token] -> [Token] -> ParamSort
instantiateSort sp :: ParamSort
sp@(Sort tok :: Token
tok, tok_params :: [Token]
tok_params) (p :: Token
p : ps :: [Token]
ps) (v :: Token
v : vs :: [Token]
vs) =
  if Token -> [Token] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Token
p [Token]
tok_params then ParamSort -> [Token] -> [Token] -> ParamSort
instantiateSort ParamSort
sp [Token]
ps [Token]
vs else
    let tok' :: Token
tok' = [Char] -> Token
mkSimpleId ([Char] -> Token) -> [Char] -> Token
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char] -> [Char]
instantiateSortString (Token -> [Char]
forall a. Show a => a -> [Char]
show Token
tok) (Token -> [Char]
forall a. Show a => a -> [Char]
show Token
p) (Token -> [Char]
forall a. Show a => a -> [Char]
show Token
v)
    in ParamSort -> [Token] -> [Token] -> ParamSort
instantiateSort (Token -> Symbol
Sort Token
tok', [Token]
tok_params) [Token]
ps [Token]
vs
instantiateSort sp :: ParamSort
sp@(Kind tok :: Token
tok, tok_params :: [Token]
tok_params) (p :: Token
p : ps :: [Token]
ps) (v :: Token
v : vs :: [Token]
vs) =
  if Token -> [Token] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Token
p [Token]
tok_params then ParamSort -> [Token] -> [Token] -> ParamSort
instantiateSort ParamSort
sp [Token]
ps [Token]
vs else
    let tok' :: Token
tok' = [Char] -> Token
mkSimpleId ([Char] -> Token) -> [Char] -> Token
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char] -> [Char]
instantiateSortString (Token -> [Char]
forall a. Show a => a -> [Char]
show Token
tok) (Token -> [Char]
forall a. Show a => a -> [Char]
show Token
p) (Token -> [Char]
forall a. Show a => a -> [Char]
show Token
v)
    in ParamSort -> [Token] -> [Token] -> ParamSort
instantiateSort (Token -> Symbol
Kind Token
tok', [Token]
tok_params) [Token]
ps [Token]
vs
instantiateSort ps :: ParamSort
ps _ _ = ParamSort
ps

{- | replaces one param by one view in a sort identifier
sort id -> param id -> view id -}
instantiateSortString :: String -> String -> String -> String
instantiateSortString :: [Char] -> [Char] -> [Char] -> [Char]
instantiateSortString ('{' : cs :: [Char]
cs) param :: [Char]
param view :: [Char]
view = '{' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: if Char -> [Char] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem '{' [Char]
cs
    then [Char] -> [Char] -> [Char] -> [Char] -> [Char]
instantiateSortStringAux [Char]
cs [Char]
param [Char]
view ""
    else [Char] -> [Char] -> [Char] -> [Char]
instantiateSortString [Char]
cs [Char]
param [Char]
view
instantiateSortString (c :: Char
c : cs :: [Char]
cs) param :: [Char]
param view :: [Char]
view =
     Char
c Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char] -> [Char] -> [Char]
instantiateSortString [Char]
cs [Char]
param [Char]
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 :: [Char] -> [Char] -> [Char] -> [Char] -> [Char]
instantiateSortStringAux ('`' : ',' : ps :: [Char]
ps) param :: [Char]
param view :: [Char]
view acc :: [Char]
acc =
    [Char]
value [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "`," [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char] -> [Char] -> [Char] -> [Char]
instantiateSortStringAux [Char]
ps [Char]
param [Char]
view ""
             where value :: [Char]
value = if [Char]
acc [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
param
                           then [Char]
view
                           else [Char]
acc
instantiateSortStringAux ('`' : '}' : _) param :: [Char]
param view :: [Char]
view acc :: [Char]
acc = [Char]
value [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "`}"
             where value :: [Char]
value = if [Char]
acc [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
param
                           then [Char]
view
                           else [Char]
acc
instantiateSortStringAux (p :: Char
p : ps :: [Char]
ps) param :: [Char]
param view :: [Char]
view acc :: [Char]
acc =
    [Char] -> [Char] -> [Char] -> [Char] -> [Char]
instantiateSortStringAux [Char]
ps [Char]
param [Char]
view ([Char]
acc [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char
p])
instantiateSortStringAux _ _ _ acc :: [Char]
acc = [Char]
acc

-- | qualifies the source sorts in the renamigs
qualifyRenamings :: Token -> [Renaming] -> [Renaming]
qualifyRenamings :: Token -> [Renaming] -> [Renaming]
qualifyRenamings t :: Token
t = (Renaming -> Renaming) -> [Renaming] -> [Renaming]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> Renaming -> Renaming
qualifyRenaming Token
t)

{- | qualifies the source sort in the renaming. Sorts only appear in operator
mappings with profile and sort mappings -}
qualifyRenaming :: Token -> Renaming -> Renaming
qualifyRenaming :: Token -> Renaming -> Renaming
qualifyRenaming p :: Token
p rnm :: Renaming
rnm = case Renaming
rnm of
    OpRenaming2 from :: OpId
from ar :: [Type]
ar co :: Type
co to :: ToPartRenaming
to -> OpId -> [Type] -> Type -> ToPartRenaming -> Renaming
OpRenaming2 OpId
from ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> Type -> Type
qualifyType Token
p) [Type]
ar)
      (Token -> Type -> Type
qualifyType Token
p Type
co) ToPartRenaming
to
    SortRenaming from :: Sort
from to :: Sort
to -> Sort -> Sort -> Renaming
SortRenaming (Token -> Sort -> Sort
qualifySort Token
p Sort
from) Sort
to
    _ -> Renaming
rnm

-- | qualifies both the source and target sorts in the renamings
qualifyRenamings2 :: Token -> [Renaming] -> [Renaming]
qualifyRenamings2 :: Token -> [Renaming] -> [Renaming]
qualifyRenamings2 t :: Token
t = (Renaming -> Renaming) -> [Renaming] -> [Renaming]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> Renaming -> Renaming
qualifyRenaming2 Token
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 :: Token -> Renaming -> Renaming
qualifyRenaming2 p :: Token
p rnm :: Renaming
rnm = case Renaming
rnm of
    OpRenaming2 from :: OpId
from ar :: [Type]
ar co :: Type
co to :: ToPartRenaming
to -> OpId -> [Type] -> Type -> ToPartRenaming -> Renaming
OpRenaming2 OpId
from ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> Type -> Type
qualifyType Token
p) [Type]
ar)
      (Token -> Type -> Type
qualifyType Token
p Type
co) ToPartRenaming
to
    SortRenaming from :: Sort
from to :: Sort
to -> Sort -> Sort -> Renaming
SortRenaming
      (Token -> Sort -> Sort
qualifySort Token
p Sort
from) (Token -> Sort -> Sort
qualifySort Token
p Sort
to)
    _ -> Renaming
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 :: Token -> Token -> Symbols -> [Renaming]
createQualifiedSortRenaming _ _ [] = []
createQualifiedSortRenaming old :: Token
old new :: Token
new (s :: Symbol
s : ss :: Symbols
ss) = case Token
old Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
new of
                True -> []
                False -> Renaming
rnm Renaming -> [Renaming] -> [Renaming]
forall a. a -> [a] -> [a]
: Token -> Token -> Symbols -> [Renaming]
createQualifiedSortRenaming Token
old Token
new Symbols
ss
                             where rnm :: Renaming
rnm = Sort -> Sort -> Renaming
SortRenaming (Token -> Token -> Sort
qualifiedSort Token
old' Token
s')
                                                      (Token -> Token -> Sort
qualifiedSort Token
new' Token
s')
        where old' :: Token
old' = Token -> Token
forall a. HasName a => a -> Token
HasName.getName Token
old
              new' :: Token
new' = Token -> Token
forall a. HasName a => a -> Token
HasName.getName Token
new
              s' :: Token
s' = Symbol -> Token
forall a. HasName a => a -> Token
HasName.getName Symbol
s

-- | qualifies with the given parameter the token
qualifiedSort :: Token -> Token -> Sort
qualifiedSort :: Token -> Token -> Sort
qualifiedSort param :: Token
param sort :: Token
sort =
    Token -> Sort
SortId (Token -> Sort) -> Token -> Sort
forall a b. (a -> b) -> a -> b
$ [Char] -> Token
mkSimpleId ([Char] -> Token) -> [Char] -> Token
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Token -> [Char]
forall a. Show a => a -> [Char]
show Token
param, "$", Token -> [Char]
forall a. Show a => a -> [Char]
show Token
sort]

-- | qualifies with the given parameter the sort
qualifySort :: Token -> Sort -> Sort
qualifySort :: Token -> Sort -> Sort
qualifySort p :: Token
p (SortId s :: Token
s) = Token -> Token -> Sort
qualifiedSort Token
p Token
s

-- | qualifies with the given parameter the type
qualifyType :: Token -> Type -> Type
qualifyType :: Token -> Type -> Type
qualifyType p :: Token
p (TypeSort (SortId s :: Token
s)) = Sort -> Type
TypeSort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Token -> Token -> Sort
qualifiedSort Token
p Token
s
qualifyType _ ty :: Type
ty = Type
ty

{- | qualifies the symbols in the theory imported with the parameter name
given as first parameter -}
createQualificationTh2Mod :: Token -> Symbols -> [Renaming]
createQualificationTh2Mod :: Token -> Symbols -> [Renaming]
createQualificationTh2Mod _ [] = []
createQualificationTh2Mod par :: Token
par (s :: Symbol
s : ss :: Symbols
ss) =
                Renaming
rnm Renaming -> [Renaming] -> [Renaming]
forall a. a -> [a] -> [a]
: Token -> Symbols -> [Renaming]
createQualificationTh2Mod Token
par Symbols
ss
        where par' :: Token
par' = Token -> Token
forall a. HasName a => a -> Token
HasName.getName Token
par
              s' :: Token
s' = Symbol -> Token
forall a. HasName a => a -> Token
HasName.getName Symbol
s
              rnm :: Renaming
rnm = Sort -> Sort -> Renaming
SortRenaming (Token -> Sort
SortId Token
s') (Token -> Token -> Sort
qualifiedSort Token
par' Token
s')

-- | Library name for Maude prelude
preludeLib :: LibName
preludeLib :: LibName
preludeLib = [Char] -> LibName
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 :: HetcatsOpts -> [Char] -> IO (Maybe (LibName, LibEnv))
anaMaudeFile opts :: HetcatsOpts
opts file :: [Char]
file = do
    (dg1 :: DGraph
dg1, dg2 :: DGraph
dg2) <- HetcatsOpts -> [Char] -> IO (DGraph, DGraph)
directMaudeParsing HetcatsOpts
opts [Char]
file
    let ln :: LibName
ln = [Char] -> LibName
emptyLibName [Char]
file
        lib1 :: LibEnv
lib1 = LibName -> DGraph -> LibEnv
forall k a. k -> a -> Map k a
Map.singleton LibName
preludeLib (DGraph -> LibEnv) -> DGraph -> LibEnv
forall a b. (a -> b) -> a -> b
$
                 LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
forall k a. Map k a
Map.empty LibName
ln (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ LibEnv -> DGraph -> DGraph
markFree LibEnv
forall k a. Map k a
Map.empty (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$
                 LibEnv -> DGraph -> DGraph
markHiding LibEnv
forall k a. Map k a
Map.empty DGraph
dg1
        lib2 :: LibEnv
lib2 = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln
                 (LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
lib1 LibName
ln (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ LibEnv -> DGraph -> DGraph
markFree LibEnv
lib1 (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$
                 LibEnv -> DGraph -> DGraph
markHiding LibEnv
lib1 DGraph
dg2) LibEnv
lib1
    Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv)))
-> Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ (LibName, LibEnv) -> Maybe (LibName, LibEnv)
forall a. a -> Maybe a
Just (LibName
ln, LibEnv
lib2)