ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport System.IO

ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport System.Environment

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport System.Process

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederimport Static.DevGraph

ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport Static.GTheory

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maederimport Static.AnalysisStructured

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederimport Logic.Prover

ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport Logic.Grothendieck

79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maederimport Logic.ExtSign

ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport Logic.Logic

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport Maude.AS_Maude

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport Maude.Sign

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maederimport Maude.Printing

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport Maude.Sentence

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport Maude.Morphism

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport Maude.Logic_Maude

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport Maude.Language

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport Maude.Shellout

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport qualified Maude.Meta.HasName as HasName

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder

ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport Data.Maybe

ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport qualified Data.Map as Map

ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport qualified Data.Set as Set

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Data.Graph.Inductive.Graph

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Common.AS_Annotation

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.Result

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederimport Common.Id

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- Borrar despues de las pruebas

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederimport GUI.ShowGraph

e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maederimport Driver.Options

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.LibName

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maedermaude_cmd :: String

53301de22afd7190981b363b57c48df86fcb50f7Christian Maedermaude_cmd = "/Applications/maude-darwin/maude.intelDarwin -interactive -no-banner"

028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder

975642b989852fc24119c59cf40bc1af653608ffChristian Maederdata ImportType = Pr | Ex | Inc

53301de22afd7190981b363b57c48df86fcb50f7Christian Maedertype ModExpProc = (Token, TokenInfoMap, Morphism, [ParamSort], DGraph)

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maedertype ImportProc = (ImportType, Token, TokenInfoMap, Morphism, [ParamSort], DGraph)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedertype TokenInfoMap = Map.Map Token ProcInfo

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedertype ProcInfo = (Node, Sign, [Token], [(Token, Token, [Token])], [ParamSort])

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedertype ParamInfo = ([(Token, Token, [Token])], TokenInfoMap, [Morphism], DGraph)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- | Map from view identifiers to tuples containing the target node of the

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder-- view, the morphism, and a Boolean value indicating if the view instantiates

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder-- all the values

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedertype ViewMap = Map.Map Token (Node, Morphism, [Renaming], Bool)

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

53301de22afd7190981b363b57c48df86fcb50f7Christian Maedertype InsSpecRes = (TokenInfoMap, ViewMap, [Token], DGraph)

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder-- | Pair of tokens and parameters contained by the token

53301de22afd7190981b363b57c48df86fcb50f7Christian Maedertype ParamSort = (Token, [Token])

da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder

da2b959c50c95309d8eb8b24174249c2847e74b5Christian MaederinsertSpecs :: [Spec] -> TokenInfoMap -> ViewMap -> [Token] -> DGraph -> DGraph

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederinsertSpecs [] _ _ _ dg = dg

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

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

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederinsertSpec :: Spec -> TokenInfoMap -> ViewMap -> [Token] -> DGraph -> InsSpecRes

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederinsertSpec (SpecMod sp_mod) tim vm ths dg = (tim4, vm, ths, dg5)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder where ps = getParams sp_mod

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

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder top_sg = Maude.Sign.fromSpec sp_mod

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder paramSorts = getSortsParameterizedBy (paramNames ps) (Set.toList $ sorts top_sg)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (il, _) = getImportsSorts sp_mod

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder ips = processImports tim1 vm dg1 il

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder (tim2, dg2) = last_da ips (tim1, dg1)

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder sg = sign_union_morphs morphs $ sign_union top_sg ips

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder ext_sg = makeExtSign Maude sg

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

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder sens = toThSens nm_sns

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder gt = G_theory Maude ext_sg startSigId sens startThId

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder tok = HasName.getName sp_mod

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder name = makeName tok

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder (ns, dg3) = insGTheory dg2 name DGBasic gt

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

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

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder dg5 = createEdgesParams tok pl morphs sg tim4 dg4

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian MaederinsertSpec (SpecTh sp_th) tim vm ths dg = (tim3, vm, tok : ths, dg3)

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder where (il, ss1) = getImportsSorts sp_th

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder ips = processImports tim vm dg il

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder ss2 = getThSorts ips

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder (tim1, dg1) = last_da ips (tim, dg)

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder sg = sign_union (Maude.Sign.fromSpec sp_th) ips

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder ext_sg = makeExtSign Maude sg

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

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder sens = toThSens nm_sns

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder gt = G_theory Maude ext_sg startSigId sens startThId

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder tok = HasName.getName sp_th

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder name = makeName tok

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder (ns, dg2) = insGTheory dg1 name DGBasic gt

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

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

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian MaederinsertSpec (SpecView sp_v) tim vm ths dg = (tim2, vm', ths, dg4)

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder where View name from to rnms = sp_v

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder inst = isInstantiated ths to

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder tok_name = HasName.getName name

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

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

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

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

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder morph = fromSignsRenamings (target morph1) (target morph2) rnms

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder morph' = fromJust $ maybeResult $ compose morph1 morph

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

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

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

da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder dg4 = insertThmEdgeMorphism tok_name n3 n1 morph' dg3

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder-- | compute the union of the signatures obtained from the importation list

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maedersign_union :: Sign -> [ImportProc] -> Sign

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maedersign_union sign = foldr (Maude.Sign.union . get_sign) sign

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- | extract the target signature from the morphism in an importation tuple

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederget_sign :: ImportProc -> Sign

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederget_sign (_, _, _, morph, _, _) = target morph

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder

d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | compute the union of the target signatures of a list of morphisms

53301de22afd7190981b363b57c48df86fcb50f7Christian Maedersign_union_morphs :: [Morphism] -> Sign -> Sign

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maedersign_union_morphs morphs sg = foldr (Maude.Sign.union . target) sg morphs

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- | extracts the last (newest) data structures from a list of importation

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- tuples, using the second argument as default value if the list is empty

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederlast_da :: [ImportProc] -> (TokenInfoMap, DGraph) -> (TokenInfoMap, DGraph)

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederlast_da [(_, _, tim, _, _, dg)] _ = (tim, dg)

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederlast_da (_ : ips) p = last_da ips p

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederlast_da _ p = p

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- | generate the edges required by a parameter list in a module instantiation

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedercreateEdgesParams :: Token -> [(Token, Token, [Token])] -> [Morphism] -> Sign

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder -> TokenInfoMap -> DGraph -> DGraph

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedercreateEdgesParams tok1 ((_, tok2, _) : toks) (morph : morphs) sg tim dg =

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder createEdgesParams tok1 toks morphs sg tim dg'

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder where morph' = setTarget sg morph

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder (n1, _, _, _, _) = fromJust $ Map.lookup tok1 tim

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder (n2, _, _, _, _) = fromJust $ Map.lookup tok2 tim

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder dg' = insertDefEdgeMorphism n1 n2 morph' dg

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaedercreateEdgesParams _ _ _ _ _ dg = dg

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- | generate the edges required by the importations

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedercreateEdgesImports :: Token -> [ImportProc] -> Sign -> TokenInfoMap -> DGraph

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -> (TokenInfoMap, DGraph)

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedercreateEdgesImports _ [] _ tim dg = (tim, dg)

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedercreateEdgesImports tok (ip : ips) sg tim dg = createEdgesImports tok ips sg tim' dg'

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder where (tim', dg') = createEdgeImport tok ip sg tim dg

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder

9d75ab580dbf51b7ca60903fb32e7f38d939d326Christian Maeder-- | generate the edge for a concrete importation

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian MaedercreateEdgeImport :: Token -> ImportProc -> Sign -> TokenInfoMap -> DGraph

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder -> (TokenInfoMap, DGraph)

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedercreateEdgeImport tok1 (Pr, tok2, _, morph, _, _) sg tim dg = (tim', dg'')

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder where morph' = setTarget sg morph

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder (tok2', tim', dg') = insertFreeNode tok2 tim dg

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (n1, _, _, _, _) = fromJust $ Map.lookup tok1 tim'

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder (n2, _, _, _, _) = fromJust $ Map.lookup tok2' tim'

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder dg'' = insertDefEdgeMorphism n1 n2 morph' dg'

9d75ab580dbf51b7ca60903fb32e7f38d939d326Christian MaedercreateEdgeImport tok1 (Ex, tok2, _, morph, _, _) sg tim dg = (tim, dg')

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder where morph' = setTarget sg morph

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder (n1, _, _, _, _) = fromJust $ Map.lookup tok1 tim

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (n2, _, _, _, _) = fromJust $ Map.lookup tok2 tim

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder dg' = insertConsEdgeMorphism n1 n2 morph' dg

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedercreateEdgeImport tok1 (Inc, tok2, _, morph, _, _) sg tim dg = (tim, dg')

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder where morph' = setTarget sg morph

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (n1, _, _, _, _) = fromJust $ Map.lookup tok1 tim

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (n2, _, _, _, _) = fromJust $ Map.lookup tok2 tim

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder dg' = insertDefEdgeMorphism n1 n2 morph' dg

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- | extract the sorts provided by the theories

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedergetThSorts :: [ImportProc] -> [Token]

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedergetThSorts [] = []

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian MaedergetThSorts (ip : ips) = getThSortsAux ip ++ getThSorts ips

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian MaedergetThSortsAux :: ImportProc -> [Token]

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedergetThSortsAux (_, tok, tim, _, _, _) = srts

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder where (_, _, srts, _, _) = fromJust $ Map.lookup tok tim

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- | generate the extra signature needed when using term to term renaming in views

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maedersign4renamings :: Sign -> Map.Map Token Token -> [Renaming] -> (Sign, [Sentence])

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maedersign4renamings sg mtt ((TermMap t1 t2) : rnms) = (new_sg, (Equation eq) : sens)

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder where (op_top, ss) = getOpSorts t1

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sg' = newOp sg op_top ss mtt

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder (sg'', sens) = sign4renamings sg mtt rnms

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder eq = Eq (applyRenamingTerm mtt t1) t2 [] []

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder new_sg = Maude.Sign.union sg' sg''

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maedersign4renamings sg mtt (_ : rnms) = sign4renamings sg mtt rnms

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maedersign4renamings sg _ [] = (sg, [])

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder-- | given the identifier of an operator in the given signature, the function

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- generates a new signature with this operator and a renamed profile computed

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- from the renaming given in the mapping

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedernewOp :: Sign -> Token -> [Token] -> Map.Map Token Token -> Sign

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedernewOp sg op ss mtt = Maude.Sign.empty {ops = Map.singleton op $ Set.singleton od}

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder where om = ops sg

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder ods = fromJust $ Map.lookup op om

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder od = getOpDecl ods ss mtt

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- | rename the profile with the given map

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedergetOpDecl :: OpDeclSet -> [Token] -> Map.Map Token Token -> OpDecl

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedergetOpDecl ods ss mtt = od'

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder where f = \ (x, _, _) -> x == ss

3f7009c892b16d172314abbba83d663fa0d87a65Christian Maeder od : _ = Set.toList $ Set.filter f ods

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder od' = applyRenamingOD od mtt

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- | apply the renaming in the map to the operator declaration

53301de22afd7190981b363b57c48df86fcb50f7Christian MaederapplyRenamingOD :: OpDecl -> Map.Map Token Token -> OpDecl

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederapplyRenamingOD (ar, co, ats) mtt = (ar', co', ats)

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder where f = \ x -> if Map.member x mtt

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder then fromJust $ Map.lookup co mtt

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder else x

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder ar' = map f ar

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder co' = if Map.member co mtt

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder then fromJust $ Map.lookup co mtt

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder else co

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- | rename the sorts in a term

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian MaederapplyRenamingTerm :: Map.Map Token Token -> Term -> Term

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaederapplyRenamingTerm mtt (Apply q ts ty) = Apply q (map (applyRenamingTerm mtt) ts)

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder (applyRenamingType mtt ty)

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederapplyRenamingTerm mtt (Const q s) = Const q s'

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder where s' = applyRenamingType mtt s

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaederapplyRenamingTerm mtt (Var q s) = Var q s'

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder where s' = applyRenamingType mtt s

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder-- | rename a type

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederapplyRenamingType :: Map.Map Token Token -> Type -> Type

53301de22afd7190981b363b57c48df86fcb50f7Christian MaederapplyRenamingType mtt (TypeSort s) = TypeSort $ SortId q'

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder where SortId q = s

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder q' = if Map.member q mtt

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder then fromJust $ Map.lookup q mtt

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder else q

669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederapplyRenamingType mtt (TypeKind k) = TypeKind $ KindId q'

669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder where KindId q = k

669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder q' = if Map.member q mtt

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder then fromJust $ Map.lookup q mtt

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder else q

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- | extract the top operator of a term and the names of its sorts

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- if it is applicated to some arguments

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedergetOpSorts :: Term -> (Token, [Token])

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedergetOpSorts (Const q _) = (q, [])

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedergetOpSorts (Var q _) = (q, [])

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian MaedergetOpSorts (Apply q ls _) = (q, getTypes ls)

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedergetTypes :: [Term] -> [Token]

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedergetTypes ((Var _ s) : ts) = HasName.getName s : getTypes ts

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedergetTypes _ = []

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaederprocessImports :: TokenInfoMap -> ViewMap -> DGraph -> [Import] -> [ImportProc]

669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederprocessImports _ _ _ [] = []

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiprocessImports tim vm dg (i : il) = ip : processImports tim' vm dg' il

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder where ip@(_, _, tim', _, _, dg') = processImport tim vm dg i

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederprocessImport :: TokenInfoMap -> ViewMap -> DGraph -> Import -> ImportProc

09249711700a6acbc40a2e337688b434d7aafa28Christian MaederprocessImport tim vm dg (Protecting modExp) = (Pr, tok, tim', morph, ps, dg')

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

53301de22afd7190981b363b57c48df86fcb50f7Christian MaederprocessImport tim vm dg (Extending modExp) = (Ex, tok, tim', morph, ps, dg')

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

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederprocessImport tim vm dg (Including modExp) = (Inc, tok, tim', morph, ps, dg')

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

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederprocessParameters :: [Parameter] -> TokenInfoMap -> DGraph -> ParamInfo

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederprocessParameters ps tim dg = foldr processParameter ([], tim, [], dg) ps

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder

09249711700a6acbc40a2e337688b434d7aafa28Christian MaederprocessParameter :: Parameter -> ParamInfo -> ParamInfo

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederprocessParameter (Parameter sort modExp) (toks, tim, morphs, dg) = (toks', tim', morphs', dg')

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder where (tok, tim', morph, _, dg') = processModExp tim Map.empty dg modExp

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder (_, _, fs, _, _) = fromJust $ Map.lookup tok tim'

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder fs' = renameSorts morph fs

909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder morph' = extendMorphismSorts morph (HasName.getName sort) fs'

f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder toks' = (HasName.getName sort, tok, fs') : toks

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder morphs' = morph' : morphs

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprocessModExp :: TokenInfoMap -> ViewMap -> DGraph -> ModExp -> ModExpProc

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederprocessModExp tim _ dg (ModExp modId) = (tok, tim, morph, ps, dg)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder where tok = HasName.getName modId

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

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder morph = createInclMorph sg sg

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

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

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

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder ps' = deleteRepeated $ ps1 ++ ps2

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder tok = mkSimpleId $ "{" ++ show tok1 ++ " + " ++ show tok2 ++ "}"

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

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

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder ss1' = renameSorts morph1 ss1

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder ss2' = renameSorts morph1 ss2

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder sg1 = target morph1

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder sg2 = target morph2

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder sg = Maude.Sign.union sg1 sg2

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder morph = createInclMorph sg sg

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder morph1' = setTarget sg morph1

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder morph2' = setTarget sg morph2

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

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

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder dg4 = insertDefEdgeMorphism n3 n1 morph1' dg3

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder dg5 = insertDefEdgeMorphism n3 n2 morph2' dg4

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederprocessModExp tim vm dg (RenamingModExp modExp rnms) = (tok, tim', comp_morph, ps', dg')

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

e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder morph' = fromSignRenamings (target morph) rnms

da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder ps' = applyRenamingParamSorts (sortMap morph') ps

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder comp_morph = fromJust $ maybeResult $ compose morph morph'

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaederprocessModExp tim vm dg (InstantiationModExp modExp views) = (tok'', tim'', final_morph, new_param_sorts, dg'')

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

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

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder param_names = map (fstTern) ps

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder view_names = map HasName.getName views

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder (new_param_sorts, ps_morph) = instantiateSorts param_names view_names vm morph paramSorts

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder (tok', morph1, ns, deps) = processViews views (mkSimpleId "") tim' vm ps (ps_morph, [], [])

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder tok'' = mkSimpleId $ show tok ++ "{" ++ show tok' ++ "}"

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder sg2 = target morph1

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder final_morph = createInclMorph sg2 sg2

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

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder then (tim', dg')

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

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederupdateGraphViews :: Token -> Token -> Sign -> Morphism -> [(Node, Sign)] -> TokenInfoMap

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder -> [(Token, Token, [Token])] -> DGraph -> (TokenInfoMap, DGraph)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederupdateGraphViews tok1 tok2 sg morph views tim deps dg = (tim', dg''')

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder where (n1, _, _, _, _) = fromJust $ Map.lookup tok1 tim

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder morph' = setTarget sg morph

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder -- TODO: if the parameter is another theory, the empty list

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder -- must be replaced by the corresponding list of sorts

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder (tim', dg') = insertNode tok2 sg tim [] deps dg

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder (n2, _, _, _, _) = fromJust $ Map.lookup tok2 tim'

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder dg'' = insertDefEdgeMorphism n2 n1 morph' dg'

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder dg''' = insertDefEdgesMorphism n2 views sg dg''

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder

53301de22afd7190981b363b57c48df86fcb50f7Christian MaederprocessViews :: [ViewId] -> Token -> TokenInfoMap -> ViewMap -> [(Token, Token, [Token])]

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder -> (Morphism, [(Node, Sign)], [(Token, Token, [Token])])

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder -> (Token, Morphism, [(Node, Sign)], [(Token, Token, [Token])])

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprocessViews (vi : vis) tok tim vm (p : ps) (morph, lp, dep) =

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder case mn of

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder Just n -> processViews vis tok'' tim vm ps (morph', lp ++ [(n, target morph')], dep ++ new_dep)

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder Nothing -> processViews vis tok'' tim vm ps (morph', lp, dep)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder where (tok', morph', mn, new_dep) = processView vi tok tim vm p morph

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder tok'' = mkSimpleId $ show tok ++ "," ++ show tok'

dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederprocessViews _ tok _ _ _ (morph, nds, deps) = (tok', morph, nds, deps)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder where tok' = mkSimpleId $ drop 1 $ show tok

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder

dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederprocessView :: ViewId -> Token -> TokenInfoMap -> ViewMap -> (Token, Token, [Token]) ->

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Morphism -> (Token, Morphism, Maybe Node, [(Token, Token, [Token])])

dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederprocessView vi tok tim vm (p, _, ss) morph =

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder if Map.member name vm

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder then morphismView name p ss (fromJust $ Map.lookup name vm) morph

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder else paramBinding name p ss morph

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder where name = HasName.getName vi

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedermorphismView :: Token -> Token -> [Token] -> (Node, Morphism, [Renaming], Bool)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder -> Morphism -> (Token, Morphism, Maybe Node, [(Token, Token, [Token])])

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedermorphismView name p _ (n, _, rnms, True) morph = (name, morph', Just n, [])

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder where rnms' = qualifyRenamings p rnms

f1ef1c750f805c1732b01001f2b157c0077b808eChristian Maeder morph' = applyRenamings morph rnms'

ac142c1b088711f911018d8108a64be80b2f2a58Christian MaedermorphismView name p ss (n, morph, rnms, False) morph1 =

f1ef1c750f805c1732b01001f2b157c0077b808eChristian Maeder (name, morph2, Just n, [(p, mkSimpleId "", renameSorts morph ss)])

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder where rnms' = qualifyRenamings2 p rnms

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder morph2 = applyRenamings morph1 rnms'

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- parameter instantiated -> parameter binding -> sorts bound -> current morph

975642b989852fc24119c59cf40bc1af653608ffChristian MaederparamBinding :: Token -> Token -> [Token] -> Morphism -> (Token, Morphism, Maybe Node, [(Token, Token, [Token])])

975642b989852fc24119c59cf40bc1af653608ffChristian MaederparamBinding view p ss morph = (view, morph', Nothing, [])

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder where rnms = createQualifiedSortRenaming p view ss

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder morph' = applyRenamings morph rnms

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

ab0f35d8b9012e459417e086773049ce33dda2a0Christian MaederinsertNode :: Token -> Sign -> TokenInfoMap -> [Token] -> [(Token, Token, [Token])] -> DGraph -> (TokenInfoMap, DGraph)

dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederinsertNode tok sg tim ss deps dg = if Map.member tok tim

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder then (tim, dg)

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder else let

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ext_sg = makeExtSign Maude sg

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder gt = G_theory Maude ext_sg startSigId noSens startThId

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder name = makeName tok

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

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

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder in (tim', dg')

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder

975642b989852fc24119c59cf40bc1af653608ffChristian MaederinsertInnerNode :: Node -> NodeName -> Morphism -> Sign -> [Sentence] -> DGraph

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -> (Node, DGraph)

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederinsertInnerNode nod nm morph sg sens dg =

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder if (isIdentity morph) && (sens == [])

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder then (nod, dg)

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder else let

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder th_sens = toThSens $ map (makeNamed "") sens

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder sg' = Maude.Sign.union sg $ target morph

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder ext_sg = makeExtSign Maude sg'

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder gt = G_theory Maude ext_sg startSigId th_sens startThId

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder (ns, dg') = insGTheory dg (inc nm) DGBasic gt

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder nod2 = getNode ns

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder morph' = setTarget sg' morph

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder dg'' = insertDefEdgeMorphism nod2 nod morph' dg'

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder in (nod2, dg'')

ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- | insert the list of definition edges, building for each node the inclusion morphism

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- between the signatures

insertDefEdgesMorphism :: Node -> [(Node, Sign)] -> Sign -> DGraph -> DGraph

insertDefEdgesMorphism _ [] _ dg = dg

insertDefEdgesMorphism n1 ((n2, sg1) : views) sg2 dg = insertDefEdgesMorphism n1 views sg2 dg'

where morph = createInclMorph sg1 sg2

dg' = insertDefEdgeMorphism n1 n2 morph dg

-- | insert a definition link between the nodes with the given morphism

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

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

where mor = G_morphism Maude morph startMorId

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

insertThmEdgeMorphism :: Token -> Node -> Node -> Morphism -> DGraph -> DGraph

insertThmEdgeMorphism name n1 n2 morph dg = insEdgeDG (n2, n1, edg) dg

where mor = G_morphism Maude morph startMorId

edg = DGLink (gEmbed mor) globalThm (DGLinkView name) $ getNewEdgeId dg

insertConsEdgeMorphism :: Node -> Node -> Morphism -> DGraph -> DGraph

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

where mor = G_morphism Maude morph startMorId

edg = DGLink (gEmbed mor) (globalConsThm PCons) SeeTarget $ getNewEdgeId dg

insertFreeEdge :: Token -> Token -> TokenInfoMap -> DGraph -> DGraph

insertFreeEdge tok1 tok2 tim dg = insEdgeDG (n2, n1, edg) dg

where (n1, sg1, _, _, _) = fromJust $ Map.lookup tok1 tim

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

mor = G_morphism Maude (createInclMorph sg1 sg2) startMorId

dgt = FreeOrCofreeDefLink Free $ EmptyNode (Logic Maude)

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

insertFreeNode :: Token -> TokenInfoMap -> DGraph -> (Token, TokenInfoMap, DGraph)

insertFreeNode t tim dg = (t', tim', dg'')

where t' = mkFreeName t

b = Map.member t' tim

(tim', dg') = if b

then (tim, dg)

else insertFreeNode2 t' tim (fromJust $ Map.lookup t tim) dg

dg'' = if b

then dg'

else insertFreeEdge t' t tim' dg'

insertFreeNode2 :: Token -> TokenInfoMap -> ProcInfo -> DGraph -> (TokenInfoMap, DGraph)

insertFreeNode2 t tim (_, sg, _, _, _) dg = (tim', dg')

where ext_sg = makeExtSign Maude sg

gt = G_theory Maude ext_sg startSigId noSens startThId

name = makeName t

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

tim' = Map.insert t (getNode ns, sg, [], [], []) tim

-- | Given the identifier of a module, generates the identifier for the module

-- with the ``freeness'' constraint

mkFreeName :: Token -> Token

mkFreeName = mkSimpleId . (\ x -> x ++ "'") . show

getParams :: Module -> [Parameter]

getParams (Module _ params _) = params

getImportsSorts :: Module -> ([Import], [Token])

getImportsSorts (Module _ _ stmts) = getImportsSortsStmnts stmts ([],[])

getImportsSortsStmnts :: [Statement] -> ([Import], [Token]) -> ([Import], [Token])

getImportsSortsStmnts [] p = p

getImportsSortsStmnts ((ImportStmnt imp) : stmts) (is, ss) =

getImportsSortsStmnts stmts (imp : is, ss)

getImportsSortsStmnts ((SortStmnt s) : stmts) (is, ss) =

getImportsSortsStmnts stmts (is, (HasName.getName s) : ss)

getImportsSortsStmnts (_ : stmts) p = getImportsSortsStmnts stmts p

directMaudeParsing :: FilePath -> IO DGraph

directMaudeParsing fp = do

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

hPutStrLn hIn $ "load " ++ fp

ns <- parse fp

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

ms <- traverseNames hIn hOut ns'

hPutStrLn hIn "in Maude/hets.prj"

psps <- predefinedSpecs hIn hOut

sps <- traverseSpecs hIn hOut ms

hClose hIn

hClose hOut

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

main :: IO ()

main = getArgs >>= mapM_ directMaudeParsing2

directMaudeParsing2 :: FilePath -> IO ()

directMaudeParsing2 fp = do

dg <- directMaudeParsing fp

showGraph fp maudeHetcatsOpts

(Just (Lib_id (Direct_link "" nullRange),

Map.singleton (Lib_id (Direct_link "" nullRange)) dg ))

traverseSpecs :: Handle -> Handle -> [String] -> IO [Spec]

traverseSpecs _ _ [] = return []

traverseSpecs hIn hOut (m : ms) = do

hPutStrLn hIn m

hFlush hIn

sOutput <- getAllSpec hOut "" False

ss <- traverseSpecs hIn hOut ms

let stringSpec = findSpec sOutput

let spec = read stringSpec :: Spec

return $ spec : ss

traverseNames :: Handle -> Handle -> [NamedSpec] -> IO [String]

traverseNames _ _ [] = return []

traverseNames hIn hOut (ModName q : ns) = do

hPutStrLn hIn $ "show module " ++ q ++ " ."

hFlush hIn

sOutput <- getAllOutput hOut "" False

rs <- traverseNames hIn hOut ns

return $ sOutput : rs

traverseNames hIn hOut (ViewName q : ns) = do

hPutStrLn hIn $ "show view " ++ q ++ " ."

hFlush hIn

sOutput <- getAllOutput hOut "" False

rs <- traverseNames hIn hOut ns

return $ sOutput : rs

getAllOutput :: Handle -> String -> Bool -> IO String

getAllOutput hOut s False = do

ss <- hGetLine hOut

getAllOutput hOut (s ++ "\n" ++ ss) (final ss)

getAllOutput _ s True = return $ prepare s

getAllSpec :: Handle -> String -> Bool -> IO String

getAllSpec hOut s False = do

ss <- hGetLine hOut

getAllSpec hOut (s ++ "\n" ++ ss) (finalSpec ss)

getAllSpec _ s True = return s

final :: String -> Bool

final "endfm" = True

final "endm" = True

final "endth" = True

final "endfth" = True

final "endv" = True

final _ = False

prepare :: String -> String

prepare s = "(" ++ (drop 8 s) ++ ")"

finalSpec :: String -> Bool

finalSpec "@#$endHetsSpec$#@" = True

finalSpec _ = False

predefined :: [NamedSpec]

predefined = [ModName "TRUTH-VALUE", ModName "TRUTH", ModName "BOOL", ModName "EXT-BOOL",

ModName "NAT",

ModName "INT", ModName "RAT", ModName "FLOAT", ModName "STRING", ModName "CONVERSION",

ModName "RANDOM", ModName "QID", ModName "TRIV", ViewName "TRIV", ViewName "Bool",

ViewName "Nat", ViewName "Int", ViewName "Rat", ViewName "Float", ViewName "String",

ViewName "Qid", ModName "STRICT-WEAK-ORDER", ViewName "STRICT-WEAK-ORDER",

ModName "STRICT-TOTAL-ORDER", ViewName "STRICT-TOTAL-ORDER", ViewName "Nat<",

ViewName "Int<", ViewName "Rat<", ViewName "Float<", ViewName "String<",

ModName "TOTAL-PREORDER", ViewName "TOTAL-PREORDER", ModName "TOTAL-ORDER",

ViewName "TOTAL-ORDER", ViewName "Nat<=", ViewName "Int<=", ViewName "Rat<=",

ViewName "Float<=", ViewName "String<=", ModName "DEFAULT", ViewName "DEFAULT",

ViewName "Nat0", ViewName "Int0", ViewName "Rat0", ViewName "Float0",

ViewName "String0", ViewName "Qid0", ModName "LIST", ModName "WEAKLY-SORTABLE-LIST",

ModName "SORTABLE-LIST", ModName "WEAKLY-SORTABLE-LIST'",

ModName "SORTABLE-LIST'", ModName "SET", ModName "LIST-AND-SET",

ModName "SORTABLE-LIST-AND-SET", ModName "SORTABLE-LIST-AND-SET'",

ModName "LIST*", ModName "SET*", ModName "MAP", ModName "ARRAY",

ModName "NAT-LIST", ModName "QID-LIST", ModName "QID-SET", ModName "META-TERM",

ModName "META-MODULE", ModName "META-LEVEL", ModName "COUNTER", ModName "LOOP-MODE",

ModName "CONFIGURATION"]

predefinedSpecs :: Handle -> Handle -> IO [Spec]

predefinedSpecs hIn hOut = traversePredefined hIn hOut predefined

traversePredefined :: Handle -> Handle -> [NamedSpec] -> IO [Spec]

traversePredefined _ _ [] = return []

traversePredefined hIn hOut (ModName n : ns) = do

hPutStrLn hIn $ "(hets " ++ n ++ " .)"

hFlush hIn

sOutput <- getAllSpec hOut "" False

ss <- traversePredefined hIn hOut ns

let stringSpec = findSpec sOutput

let spec = read stringSpec :: Spec

return $ spec : ss

traversePredefined hIn hOut (ViewName n : ns) = do

hPutStrLn hIn $ "(hetsView " ++ n ++ " .)"

hFlush hIn

sOutput <- getAllSpec hOut "" False

ss <- traversePredefined hIn hOut ns

let stringSpec = findSpec sOutput

let spec = read stringSpec :: Spec

return $ spec : ss

-- | return the parameter names

paramNames :: [Parameter] -> [Token]

paramNames = map f

where f = \ (Parameter s _) -> HasName.getName s

-- | return the sorts (second argument of the pair) that contain any of the parameters

-- given as first argument

getSortsParameterizedBy :: [Token] -> [Token] -> [(Token, [Token])]

getSortsParameterizedBy ps = filter f . map (g ps)

where f = \ (_, l) -> l /= []

g = \ pss x -> let

params = getSortParams x

in (x, intersec params pss)

intersec :: [Token] -> [Token] -> [Token]

intersec [] _ = []

intersec (e : es) l = case elem e l of

False -> intersec es l

True -> e : intersec es l

-- | extracts the parameters of the given sort

-- For example, getSortParams List{X} = [X]

-- List{X}{Y, Y} = [Y,Z]

getSortParams :: Token -> [Token]

getSortParams t = getSortParamsString $ show t

getSortParamsString :: String -> [Token]

getSortParamsString [] = []

getSortParamsString ('{' : cs) = if sps == []

then getSortParamsStringAux cs ""

else sps

where sps = getSortParamsString cs

getSortParamsString (_ : cs) = getSortParamsString cs

getSortParamsStringAux :: String -> String -> [Token]

getSortParamsStringAux ('`' : ',' : cs) st = mkSimpleId st : getSortParamsStringAux cs ""

getSortParamsStringAux ('`' : '}' : []) st = [mkSimpleId st]

getSortParamsStringAux (' ' : cs) st = getSortParamsStringAux cs st

getSortParamsStringAux (c : cs) st = getSortParamsStringAux cs (st ++ [c])

getSortParamsStringAux [] st = [mkSimpleId st]

-- | check if the target of the view is completely instantiated (to modules)

isInstantiated :: [Token] -> ModExp -> Bool

isInstantiated ths (ModExp modExp) = notElem (HasName.getName modExp) ths

isInstantiated ths (SummationModExp me1 me2) = isInstantiated ths me1 &&

isInstantiated ths me2

isInstantiated ths (RenamingModExp modExp _) = isInstantiated ths modExp

isInstantiated _ (InstantiationModExp _ _) = True

-- | rename the parameterized sorts and computes if they are still parameterized

applyRenamingParamSorts :: Map.Map Token Token -> [ParamSort] -> [ParamSort]

applyRenamingParamSorts mtt = foldr (applyRenamingParamSort mtt) []

applyRenamingParamSort :: Map.Map Token Token -> ParamSort -> [ParamSort]

-> [ParamSort]

applyRenamingParamSort mtt (tok, params) acc = case Map.member tok mtt of

False -> (tok, params) : acc

True -> let

tok' = fromJust $ Map.lookup tok mtt

ps = getSortsParameterizedBy params [tok']

in ps ++ acc

deleteRepeated :: [ParamSort] -> [ParamSort]

deleteRepeated [] = []

deleteRepeated (p : ps) = if elem p ps

then deleteRepeated ps

else p : deleteRepeated ps

fstTern :: (a, b, c) -> a

fstTern (a, _, _) = a

-- | instantiate the parametric sorts

-- ParamNames -> ViewName -> Map of views -> Parametricsorts

instantiateSorts :: [Token] -> [Token] -> ViewMap -> Morphism -> [ParamSort]

-> ([ParamSort], Morphism)

instantiateSorts _ _ _ morph [] = ([], morph)

instantiateSorts params views vm morph (ps : pss) = (nps'' ++ res_ps, res_morph)

where np4s = newParamers4sorts params views vm

nps = instantiateSort ps params views

nps' = addNewParams2sort nps np4s

nps'' = if snd nps' == [] then [] else [nps']

morph' = extendWithSortRenaming (fst ps) (fst nps') morph

(res_ps, res_morph) = instantiateSorts params views vm morph' pss

-- | compute the theories that have to be further instantiated

newParamers4sorts :: [Token] -> [Token] -> ViewMap -> [Token]

newParamers4sorts (param : ps) (view : vs) vm = case Map.member view vm of

False -> newParamers4sorts ps vs vm

True -> let

(_, _, _, inst) = fromJust $ Map.lookup view vm

param' = if inst

then []

else [param]

in param' ++ newParamers4sorts ps vs vm

newParamers4sorts _ _ _ = []

addNewParams2sort :: ParamSort -> [Token] -> ParamSort

addNewParams2sort (tok, _) [] = (tok, [])

addNewParams2sort (tok, _) lps = (tok', lps)

where tok' = mkSimpleId $ show tok ++ "`{" ++ printNewParams4sort lps ++ "`}"

printNewParams4sort :: [Token] -> String

printNewParams4sort [] = ""

printNewParams4sort [p] = show p

printNewParams4sort (p : ps) = show p ++ "`," ++ printNewParams4sort ps

-- | instantiate a sort

-- Params: Parameterized sort -> Parameter to be replaced -> New name of the parameter

instantiateSort :: ParamSort -> [Token] -> [Token] -> ParamSort

instantiateSort sp@(tok, tok_params) (p : ps) (v : vs) = case elem p tok_params of

False -> instantiateSort sp ps vs

True -> let

tok' = mkSimpleId $ instantiateSortString (show tok) (show p) (show v)

in instantiateSort (tok', tok_params) ps vs

instantiateSort ps _ _ = ps

-- | replace one param by one view in a sort identifier

-- sort id -> param id -> view id

instantiateSortString :: String -> String -> String -> String

instantiateSortString ('{' : cs) param view = case elem '{' cs of

False -> '{' : instantiateSortStringAux cs param view ""

True -> '{' : instantiateSortString cs param view

instantiateSortString (c : cs) param view = c : instantiateSortString cs param view

instantiateSortString [] _ _ = ""

-- | replace one param by one view in the list of parameters

-- parameters list -> param id -> view id

instantiateSortStringAux :: String -> String -> String -> String -> String

instantiateSortStringAux ('`' : ',' : ps) param view acc = value ++ "`," ++

instantiateSortStringAux ps param view ""

where value = if acc == param

then view

else acc

instantiateSortStringAux ('`' : '}' : _) param view acc = value ++ "`}"

where value = if acc == param

then view

else acc

instantiateSortStringAux (p : ps) param view acc =

instantiateSortStringAux ps param view (acc ++ [p])

instantiateSortStringAux _ _ _ acc = acc

qualifyRenamings :: Token -> [Renaming] -> [Renaming]

qualifyRenamings t = map (qualifyRenaming t)

qualifyRenaming :: Token -> Renaming -> Renaming

qualifyRenaming p rnm = case rnm of

OpRenaming2 from ar co to -> OpRenaming2 from (map (qualifyType p) ar)

((qualifyType p) co) to

SortRenaming from to -> SortRenaming ((qualifySort p) from) to

_ -> rnm

qualifyRenamings2 :: Token -> [Renaming] -> [Renaming]

qualifyRenamings2 t = map (qualifyRenaming2 t)

qualifyRenaming2 :: Token -> Renaming -> Renaming

qualifyRenaming2 p rnm = case rnm of

OpRenaming2 from ar co to -> OpRenaming2 from (map (qualifyType p) ar)

((qualifyType p) co) to

SortRenaming from to -> SortRenaming ((qualifySort p) from) ((qualifySort p) to)

_ -> rnm

qualifyType :: Token -> Type -> Type

qualifyType p (TypeSort (SortId s)) = TypeSort (SortId $ mkSimpleId $ show p ++ "$" ++ show s)

qualifyType _ ty = ty

qualifySort :: Token -> Sort -> Sort

qualifySort p (SortId s) = SortId $ mkSimpleId $ show p ++ "$" ++ show s

createQualifiedSortRenaming :: Token -> Token -> [Token] -> [Renaming]

createQualifiedSortRenaming _ _ [] = []

createQualifiedSortRenaming old new (s : ss) = case old == new of

True -> []

False -> rnm : createQualifiedSortRenaming old new ss

where rnm = SortRenaming (qualifiedSort old s)

(qualifiedSort new s)

qualifiedSort :: Token -> Token -> Sort

qualifiedSort param sort = SortId $ mkSimpleId $ show param ++ "$" ++ show sort

-- DELETE ONCE TESTS ARE FINISHED

maudeHetcatsOpts :: HetcatsOpts

maudeHetcatsOpts = HcOpt

{ analysis = Basic

, guiType = UseGui

, infiles = []

, specNames = []

, transNames = []

, intype = GuessIn

, libdir = ""

, modelSparQ = ""

, outdir = ""

, outtypes = [] -- no default

, recurse = False

, defLogic = "Maude"

, verbose = 1

, outputToStdout = True

, caslAmalg = []

, interactive = False

, connectP = -1

, connectH = ""

, uncolored = False

, xmlFlag = False

, computeNormalForm = False

, dumpOpts = []

, listen = -1 }

-- insertNode tiene que recibir tambien la lista de sorts parametrizados que se

-- calculen para la module expression