-- 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
type ViewMap =
Map.Map Token (Node, Token, Morphism, [Renaming], Bool)
-- | Tuple of data structures updated when a specification is introduced into
type InsSpecRes = (TokenInfoMap, ViewMap, [Token], DGraph)
-- | inserts the list of specifications in the development graph, updating
insertSpecs :: [Spec] -> TokenInfoMap -> ViewMap -> [Token] -> DGraph -> DGraph
insertSpecs [] _ _ _ dg = dg
insertSpecs (s : ss) tim vm ths dg = insertSpecs ss tim' vm' ths' dg'
where (tim', vm', ths', dg') = insertSpec s tim vm ths dg
-- | inserts the given specification in the development graph, updating
insertSpec :: Spec -> TokenInfoMap -> ViewMap -> [Token] -> DGraph -> InsSpecRes
insertSpec (SpecMod sp_mod) tim vm ths dg = (tim4, vm, ths, dg5)
where ps = getParams sp_mod
(pl, tim1, morphs, dg1) = processParameters ps tim dg
paramSorts = getSortsParameterizedBy (paramNames ps) (
Set.toList $ sorts top_sg)
(il, _) = getImportsSorts sp_mod
ips = processImports tim1 vm dg1 il
(tim2, dg2) = last_da ips (tim1, dg1)
sg = sign_union_morphs morphs $ sign_union top_sg ips
ext_sg = makeExtSign Maude sg
gt = G_theory Maude ext_sg startSigId sens startThId
(ns, dg3) = insGTheory dg2 name DGBasic gt
tim3 =
Map.insert tok (getNode ns, sg, [], pl, paramSorts) tim2
(tim4, dg4) = createEdgesImports tok ips sg tim3 dg3
dg5 = createEdgesParams tok pl morphs sg tim4 dg4
insertSpec (SpecTh sp_th) tim vm ths dg = (tim3, vm, tok : ths, dg3)
where (il, ss1) = getImportsSorts sp_th
ips = processImports tim vm dg il
(tim1, dg1) = last_da ips (tim, dg)
ext_sg = makeExtSign Maude sg
gt = G_theory Maude ext_sg startSigId sens startThId
(ns, dg2) = insGTheory dg1 name DGBasic gt
tim2 =
Map.insert tok (getNode ns, sg, ss1 ++ ss2, [], []) tim1
(tim3, dg3) = createEdgesImports tok ips sg tim2 dg2
insertSpec (SpecView sp_v) tim vm ths dg = (tim2, vm', ths, dg4)
where View name from to rnms = sp_v
inst = isInstantiated ths to
(tok1, tim1, morph1, _, dg1) = processModExp tim vm dg from
(tok2, tim2, morph2, _, dg2) = processModExp tim1 vm dg1 to
(n1, _, _, _, _) = fromJust $
Map.lookup tok1 tim2
(n2, _, _, _, _) = fromJust $
Map.lookup tok2 tim2
morph = fromSignsRenamings (target morph1) (target morph2) rnms
morph' = fromJust $ maybeResult $ compose morph1 morph
(new_sign, new_sens) = sign4renamings (target morph1) (sortMap morph) rnms
(n3, dg3) = insertInnerNode n2 (makeName tok2) morph2 new_sign new_sens dg2
dg4 = insertThmEdgeMorphism tok_name n3 n1 morph' dg3
-- | computes the union of the signatures obtained from the importation list
sign_union :: Sign -> [ImportProc] -> Sign
-- | extracts the target signature from the morphism in an importation tuple
get_sign :: ImportProc -> Sign
get_sign (_, _, _, morph, _, _) = target morph
-- | computes the union of the target signatures of a list of morphisms
sign_union_morphs :: [Morphism] -> Sign -> Sign
-- | extracts the last (newest) data structures from a list of importation
-- tuples, using the second argument as default value if the list is empty
last_da :: [ImportProc] -> (TokenInfoMap, DGraph) -> (TokenInfoMap, DGraph)
last_da [(_, _, tim, _, _, dg)] _ = (tim, dg)
last_da (_ : ips) p = last_da ips p
-- | generates the edges required by a parameter list in a module instantiation
createEdgesParams :: Token -> [(Token, Token, Symbols)] -> [Morphism] -> Sign
-> TokenInfoMap -> DGraph -> DGraph
createEdgesParams tok1 ((_, tok2, _) : toks) (morph : morphs) sg tim dg =
createEdgesParams tok1 toks morphs sg tim dg'
where morph' = setTarget sg morph
dg' = insertDefEdgeMorphism n1 n2 morph' dg
createEdgesParams _ _ _ _ _ dg = dg
-- | generates the edges required by the importations
createEdgesImports :: Token -> [ImportProc] -> Sign -> TokenInfoMap -> DGraph
-> (TokenInfoMap, DGraph)
createEdgesImports _ [] _ tim dg = (tim, dg)
createEdgesImports tok (ip : ips) sg tim dg = createEdgesImports tok ips sg tim' dg'
where (tim', dg') = createEdgeImport tok ip sg tim dg
-- | generates the edge for a concrete importation
createEdgeImport :: Token -> ImportProc -> Sign -> TokenInfoMap -> DGraph
-> (TokenInfoMap, DGraph)
createEdgeImport tok1 (Pr, tok2, _, morph, _, _) sg tim dg = (tim', dg'')
where morph' = setTarget sg morph
(tok2', tim', dg') = insertFreeNode tok2 tim dg
(n1, _, _, _, _) = fromJust $
Map.lookup tok1 tim'
(n2, _, _, _, _) = fromJust $
Map.lookup tok2' tim'
dg'' = insertDefEdgeMorphism n1 n2 morph' dg'
createEdgeImport tok1 (Ex, tok2, _, morph, _, _) sg tim dg = (tim, dg')
where morph' = setTarget sg morph
dg' = insertConsEdgeMorphism n1 n2 morph' dg
createEdgeImport tok1 (Inc, tok2, _, morph, _, _) sg tim dg = (tim, dg')
where morph' = setTarget sg morph
dg' = insertDefEdgeMorphism n1 n2 morph' dg
-- | extracts the sorts provided by the theories
getThSorts :: [ImportProc] -> Symbols
getThSorts (ip : ips) = getThSortsAux ip ++ getThSorts ips
-- | extracts the not-bounded-yet sorts related to the given identifier
getThSortsAux :: ImportProc -> Symbols
getThSortsAux (_, tok, tim, _, _, _) = srts
where (_, _, srts, _, _) = fromJust $
Map.lookup tok tim
-- | generates the extra signature needed when using term to term renaming in views
sign4renamings :: Sign -> SymbolMap -> [Renaming] -> (Sign, [Sentence])
sign4renamings sg sm ((TermMap t1 t2) : rnms) = (new_sg, (Equation eq) : sens)
where (op_top, ss) = getOpSorts t1
sg' = newOp sg op_top ss sm
(sg'', sens) = sign4renamings sg sm rnms
eq = Eq (applyRenamingTerm sm t1) t2 [] []
sign4renamings sg sm (_ : rnms) = sign4renamings sg sm rnms
sign4renamings sg _ [] = (sg, [])
-- | given the identifier of an operator in the given signature, the function
-- generates a new signature with this operator and a renamed profile computed
-- from the renaming given in the mapping
newOp :: Sign -> Token -> Symbols -> SymbolMap -> Sign
ods' = getOpDeclSet ods ss sm
-- | renames the profile with the given map
getOpDeclSet :: OpDeclSet -> Symbols -> SymbolMap -> OpDeclSet
where f = \ (Operator _ x _) b -> x == ss || b
h = \ (Operator _ y _) -> y == ss
op_sym' = applyRenamingOpSymbol op_sym sm
-- | applies the renaming in the map to the operator declaration
applyRenamingOpSymbol :: Symbol -> SymbolMap -> SymbolSet
applyRenamingOpSymbol (Operator q ar co) sm =
Set.singleton $ Operator q ar' co'
-- | renames the sorts in a term
applyRenamingTerm :: SymbolMap -> Term -> Term
applyRenamingTerm sm (Apply q ts ty) = Apply q (map (applyRenamingTerm sm) ts)
(applyRenamingType sm ty)
applyRenamingTerm sm (Const q s) = Const q s'
where s' = applyRenamingType sm s
applyRenamingTerm sm (Var q s) = Var q s'
where s' = applyRenamingType sm s
applyRenamingType :: SymbolMap -> Type -> Type
-- | extracts the top operator of a term and the names of its sorts
-- if it is applicated to some arguments
getOpSorts :: Term -> (Token, Symbols)
getOpSorts (Const q _) = (q, [])
getOpSorts (Var q _) = (q, [])
getOpSorts (Apply q ls _) = (q, getTypes ls)
-- | extracts the types of the terms while they are variables
getTypes :: [Term] -> Symbols
getTypes ((Var _ (TypeSort s)) : ts) = Sort (
HasName.getName s) : getTypes ts
getTypes ((Var _ (TypeKind s)) : ts) = Kind (
HasName.getName s) : getTypes ts
-- | process the information of the given list of imports
processImports :: TokenInfoMap -> ViewMap -> DGraph -> [Import] -> [ImportProc]
processImports _ _ _ [] = []
processImports tim vm dg (i : il) = ip : processImports tim' vm dg' il
where ip@(_, _, tim', _, _, dg') = processImport tim vm dg i
-- | process the module expression and then adds the information about
processImport :: TokenInfoMap -> ViewMap -> DGraph -> Import -> ImportProc
processImport tim vm dg (Protecting modExp) = (Pr, tok, tim', morph, ps, dg')
where (tok, tim', morph, ps, dg') = processModExp tim vm dg modExp
processImport tim vm dg (Extending modExp) = (Ex, tok, tim', morph, ps, dg')
where (tok, tim', morph, ps, dg') = processModExp tim vm dg modExp
processImport tim vm dg (Including modExp) = (Inc, tok, tim', morph, ps, dg')
where (tok, tim', morph, ps, dg') = processModExp tim vm dg modExp
-- | traverses the list of parameters and generates the required data structures
processParameters :: [Parameter] -> TokenInfoMap -> DGraph -> ParamInfo
processParameters ps tim dg = foldr processParameter ([], tim, [], dg) ps
-- | given a parameter, the function processes the module expression associated
-- to it, qualifies the not-bound-yet sorts and creates the morphism
processParameter :: Parameter -> ParamInfo -> ParamInfo
processParameter (Parameter sort modExp) (toks, tim, morphs, dg) =
(toks', tim', morphs', dg')
where (tok, tim', morph, _, dg') = processModExp tim
Map.empty dg modExp
fs' = translateSorts morph fs
morphs' = morph' : morphs
-- | distinguishes between the different module expressions to compute
-- the morphisms and update the development graph
processModExp :: TokenInfoMap -> ViewMap -> DGraph -> ModExp -> ModExpProc
processModExp tim _ dg (ModExp modId) = (tok, tim, morph, ps, dg)
processModExp tim vm dg (SummationModExp modExp1 modExp2) = (tok, tim3, morph, ps', dg5)
where (tok1, tim1, morph1, ps1, dg1) = processModExp tim vm dg modExp1
(tok2, tim2, morph2, ps2, dg2) = processModExp tim1 vm dg1 modExp2
ps' = deleteRepeated $ ps1 ++ ps2
tok = mkSimpleId $ concat ["{", show tok1, " + ", show tok2, "}"]
(n1, _, ss1, _, _) = fromJust $
Map.lookup tok1 tim2
(n2, _, ss2, _, _) = fromJust $
Map.lookup tok2 tim2
ss1' = translateSorts morph1 ss1
ss2' = translateSorts morph1 ss2
morph1' = setTarget sg morph1
morph2' = setTarget sg morph2
(tim3, dg3) = insertNode tok sg tim2 (ss1' ++ ss2') [] dg2
dg4 = insertDefEdgeMorphism n3 n1 morph1' dg3
dg5 = insertDefEdgeMorphism n3 n2 morph2' dg4
processModExp tim vm dg (RenamingModExp modExp rnms) = (tok, tim', comp_morph, ps', dg')
where (tok, tim', morph, ps, dg') = processModExp tim vm dg modExp
morph' = fromSignRenamings (target morph) rnms
ps' = applyRenamingParamSorts (sortMap morph') ps
comp_morph = fromJust $ maybeResult $ compose morph morph'
processModExp tim vm dg (InstantiationModExp modExp views) = (tok'', tim'', final_morph, new_param_sorts, dg'')
where (tok, tim', morph, paramSorts, dg') = processModExp tim vm dg modExp
param_names = map fstTpl ps
(new_param_sorts, ps_morph) = instantiateSorts param_names view_names vm morph paramSorts
(tok', morph1, ns, deps) = processViews views (mkSimpleId "") tim' vm ps (ps_morph, [], [])
tok'' = mkSimpleId $ concat [show tok, "{", show tok', "}"]
else updateGraphViews tok tok'' sg2 morph1 ns tim' deps dg'
-- | generates a edge between the source and the target of a view, inserting
-- a new node if the view contained a term to term renaming, and thus updating
-- the map from module expression to its info and the development graph
updateGraphViews :: Token -> Token -> Sign -> Morphism -> [(Node, Morphism)] -> TokenInfoMap
-> [(Token, Token, Symbols)] -> DGraph -> (TokenInfoMap, DGraph)
updateGraphViews tok1 tok2 sg morph views tim deps dg = (tim', dg''')
where (n1, _, _, _, _) = fromJust $
Map.lookup tok1 tim
morph' = setTarget sg morph
(tim', dg') = insertNode tok2 sg tim [] deps dg
(n2, _, _, _, _) = fromJust $
Map.lookup tok2 tim'
dg'' = insertDefEdgeMorphism n2 n1 morph' dg'
dg''' = insertDefEdgesMorphism n2 views sg dg''
-- | traverses a list of views obtained in an instantiation module expression
-- and return a tuple with:
-- The accumulated identifier of the module expression.
-- The accumulated morphism thus far.
-- A list of nodes and morphisms to create the appropriate edges in the
-- The not-bound-yet sorts.
processViews :: [ViewId] -> Token -> TokenInfoMap -> ViewMap -> [(Token, Token, Symbols)]
-> (Morphism, [(Node, Morphism)], [(Token, Token, Symbols)])
-> (Token, Morphism, [(Node, Morphism)], [(Token, Token, Symbols)])
processViews (vi : vis) tok tim vm (p : ps) (morph, lp, dep) =
processViews vis tok'' tim vm ps (morph', lp ++ [(n, vmorph)], dep ++ new_dep)
where (tok', morph', vmorph, n, new_dep) = processView vi tim vm p morph
tok'' = mkSimpleId $ show tok ++ "," ++ show tok'
processViews _ tok _ _ _ (morph, nds, deps) = (tok', morph, nds, deps)
where tok' = mkSimpleId $ drop 1 $ show tok
-- | this function distinguishes whether the view is an instantiation (and thus)
-- the view is in the map of views and the function morphismView is used
-- or it is just a parameter binding and paramBinding is used
processView :: ViewId -> TokenInfoMap -> ViewMap -> (Token, Token, Symbols) ->
Morphism -> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
processView vi tim vm (p, theory, ss) morph =
then morphismView name p ss (fromJust $
Map.lookup name vm) morph
else paramBinding theory name p ss morph tim
-- | the function distinguishes if the instantiation is from a module, and thus
-- all the symbols are instantiated, or it is a theory and the symbols are not
-- completely instantiated.
morphismView :: Token -> Token -> Symbols -> (Node, Token, Morphism, [Renaming], Bool)
-> Morphism -> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
morphismView name p _ (n, _, vmorph, rnms, True) morph = (name, morph'', vmorph', n, [])
where rnms' = qualifyRenamings p rnms
morph' = applyRenamings morph rnms'
morph'' = setTarget usg morph'
morphismView name p ss (n, th, morph, rnms, False) morph1 =
(name, morph4, vmorph', n, [(p, th, translateSorts morph ss)])
where rnms' = qualifyRenamings2 p rnms
morph2 = applyRenamings morph1 rnms'
rnms'' = createQualificationTh2Mod p ss
morph3 = applyRenamings morph2 rnms''
vmorph' = applyRenamings vmorph rnms''
morph4 = setTarget usg morph3
-- this function is applied when two parameters are linked, it updates the qualifications
-- of the sorts. The parameters are:
-- theory -> parameter instantiated -> parameter binding -> sorts bound -> current morph
paramBinding :: Token -> Token -> Token -> Symbols -> Morphism -> TokenInfoMap
-> (Token, Morphism, Morphism, Node, [(Token, Token, Symbols)])
paramBinding th view p ss morph tim = (view, morph', vmorph', n, [])
where rnms = createQualifiedSortRenaming p view ss
morph' = applyRenamings morph rnms
rnms' = createQualificationTh2Mod p ss
vmorph' = applyRenamings vmorph rnms'
-- | inserts the node into the development graph if it does not already exist
insertNode :: Token -> Sign -> TokenInfoMap -> Symbols -> [(Token, Token, Symbols)]
-> DGraph -> (TokenInfoMap, DGraph)
insertNode tok sg tim ss deps dg = if
Map.member tok tim
ext_sg = makeExtSign Maude sg
gt = G_theory Maude ext_sg startSigId noSens startThId
(ns, dg') = insGTheory dg name DGBasic gt
tim' =
Map.insert tok (getNode ns, sg, ss, deps, []) tim
-- | inserts an inner node. This function is used when a view defines a map
-- between terms, so it is neccesary to extend the signature of the target
-- module in order to have the appropriate map.
insertInnerNode :: Node -> NodeName -> Morphism -> Sign -> [Sentence] -> DGraph
insertInnerNode nod nm morph sg sens dg =
if (isIdentity morph) && null sens
th_sens = toThSens $ map (makeNamed "") sens
ext_sg = makeExtSign Maude sg'
gt = G_theory Maude ext_sg startSigId th_sens startThId
(ns, dg') = insGTheory dg (inc nm) DGBasic gt
morph' = setTarget sg' morph
dg'' = insertDefEdgeMorphism nod2 nod morph' dg'
-- | inserts the list of definition edges, building for each node the inclusion morphism
-- between the signatures
insertDefEdgesMorphism :: Node -> [(Node, Morphism)] -> Sign -> DGraph -> DGraph
insertDefEdgesMorphism _ [] _ dg = dg
insertDefEdgesMorphism n1 ((n2, morph) : views) sg2 dg = insertDefEdgesMorphism n1 views sg2 dg'
where morph' = setTarget sg2 morph
dg' = insertDefEdgeMorphism n1 n2 morph' dg
-- | inserts a definition link between the nodes with the given morphism
insertDefEdgeMorphism :: Node -> Node -> Morphism -> DGraph -> DGraph
insertDefEdgeMorphism n1 n2 morph dg = insEdgeDG (n2, n1, edg) dg
where mor = G_morphism Maude morph startMorId
edg = DGLink (gEmbed mor) globalDef SeeTarget $ getNewEdgeId dg
-- | inserts a theorem link, labeled with the name of the view, between the nodes
-- with the given morphism in the development graph
insertThmEdgeMorphism :: Token -> Node -> Node -> Morphism -> DGraph -> DGraph
insertThmEdgeMorphism name n1 n2 morph dg = insEdgeDG (n2, n1, edg) dg
where mor = G_morphism Maude morph startMorId
edg = DGLink (gEmbed mor) globalThm (DGLinkView name) $ getNewEdgeId dg
-- | inserts a PCons link between the nodes with the given morphism
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
-- | inserts a free definition link between the nodes with the given name
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
dgt = FreeOrCofreeDefLink Free $ EmptyNode (Logic Maude)
edg = DGLink (gEmbed mor) dgt SeeTarget $ getNewEdgeId dg
-- | the importation mode "protecting M" generates a new node M' and a free link
-- between M and M'. This function is in charge of creating such M' if it does not
insertFreeNode :: Token -> TokenInfoMap -> DGraph -> (Token, TokenInfoMap, DGraph)
insertFreeNode t tim dg = (t', tim', dg'')
else insertFreeNode2 t' tim (fromJust $
Map.lookup t tim) dg
else insertFreeEdge t' t tim' dg'
-- | auxiliary function in charge of creating M' when it does not exist
insertFreeNode2 :: Token -> TokenInfoMap -> ProcInfo -> DGraph -> (TokenInfoMap, DGraph)
insertFreeNode2 t tim (_, sg, _, _, _) dg = (tim', dg')
where ext_sg = makeExtSign Maude sg
gt = G_theory Maude ext_sg startSigId noSens startThId
(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
-- | extracts the parameters of a Maude module
getParams :: Module -> [Parameter]
getParams (Module _ params _) = params
-- | extracts the importation statements and the sorts from a module definition
getImportsSorts :: Module -> ([Import], Symbols)
getImportsSorts (Module _ _ stmts) = getImportsSortsStmnts stmts ([],[])
-- | traverses the statements accumulating the importations and the sorts
getImportsSortsStmnts :: [Statement] -> ([Import], Symbols) -> ([Import], Symbols)
getImportsSortsStmnts [] p = p
getImportsSortsStmnts ((ImportStmnt imp) : stmts) (is, ss) =
getImportsSortsStmnts stmts (imp : is, ss)
getImportsSortsStmnts ((SortStmnt s) : stmts) (is, ss) =
getImportsSortsStmnts (_ : stmts) p = getImportsSortsStmnts stmts p
-- | builds the development graph of the specified Maude file
directMaudeParsing :: FilePath -> IO DGraph
directMaudeParsing fp = do
let ns' = either (\ _ -> []) id ns
runInteractiveProcess maudeProg maudeArgs Nothing Nothing
exitCode <- getProcessExitCode procH
hPutStrLn hIn $ "load " ++ fp
ms <- traverseNames hIn hOut ns'
psps <- predefinedSpecs hIn hOut
sps <- traverseSpecs hIn hOut ms
Just ExitSuccess -> error "maude terminated immediately"
error $ "calling maude failed with exitCode: " ++ show i
-- | given input and output handlers and a list of strings, this method
-- traverses the list transforming each string into a Maude specification
traverseSpecs :: Handle -> Handle -> [String] -> IO [Spec]
traverseSpecs _ _ [] = return []
traverseSpecs hIn hOut (m : ms) = do
sOutput <- getAllSpec hOut "" False
ss <- traverseSpecs hIn hOut ms
let stringSpec = findSpec sOutput
let spec = read stringSpec :: Spec
-- | given a list of names of views and specifications, a list of
-- string with the real specifications is extracted.
traverseNames :: Handle -> Handle -> [NamedSpec] -> IO [String]
traverseNames _ _ [] = return []
traverseNames hIn hOut (ModName q : ns) = do
hPutStrLn hIn $ concat ["show module ", q, " ."]
sOutput <- getAllOutput hOut "" False
rs <- traverseNames hIn hOut ns
traverseNames hIn hOut (ViewName q : ns) = do
hPutStrLn hIn $ concat ["show view ", q, " ."]
sOutput <- getAllOutput hOut "" False
rs <- traverseNames hIn hOut ns
-- | list of names of the predefined modules
predefined :: [NamedSpec]
predefined = [ModName "TRUTH-VALUE", ModName "TRUTH", ModName "BOOL", ModName "EXT-BOOL",
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",
-- | returns the specifications of the predefined modules by passing as
-- parameter the list of names
predefinedSpecs :: Handle -> Handle -> IO [Spec]
predefinedSpecs hIn hOut = traversePredefined hIn hOut predefined
-- | returns the specifications of the predefined modules
traversePredefined :: Handle -> Handle -> [NamedSpec] -> IO [Spec]
traversePredefined _ _ [] = return []
traversePredefined hIn hOut (ModName n : ns) = do
hPutStrLn hIn $ concat ["(hets ", n, " .)"]
sOutput <- getAllSpec hOut "" False
ss <- traversePredefined hIn hOut ns
let stringSpec = findSpec sOutput
let spec = read stringSpec :: Spec
traversePredefined hIn hOut (ViewName n : ns) = do
hPutStrLn hIn $ concat ["(hetsView ", n, " .)"]
sOutput <- getAllSpec hOut "" False
ss <- traversePredefined hIn hOut ns
let stringSpec = findSpec sOutput
let spec = read stringSpec :: Spec
-- | returns the parameter names
paramNames :: [Parameter] -> [Token]
-- | returns the sorts (second argument of the pair) that contain any of the parameters
-- given as first argument
getSortsParameterizedBy :: [Token] -> Symbols -> [ParamSort]
getSortsParameterizedBy ps = filter f . map (g ps)
where f = \ (_, l) -> l /= []
in (x, intersec params pss)
-- | computes the intersection of the two list (considers them as sorts)
intersec :: [Token] -> [Token] -> [Token]
intersec (e : es) l = case elem e l of
True -> e : intersec es l
-- | extracts the parameters of the given sort
-- For example, getSortParams List{X} = [X]
getSortParams :: Token -> [Token]
getSortParams t = getSortParamsString $ show t
-- | traverses a String looking for the last curly braces
getSortParamsString :: String -> [Token]
getSortParamsString [] = []
getSortParamsString ('{' : cs) = if null sps
then getSortParamsStringAux cs ""
where sps = getSortParamsString cs
getSortParamsString (_ : cs) = getSortParamsString cs
-- | traverses a String keeping the token separated by commas
getSortParamsStringAux :: String -> String -> [Token]
getSortParamsStringAux ('`' : ',' : cs) st = mkSimpleId st : getSortParamsStringAux cs ""
getSortParamsStringAux ('`' : '}' : []) st = [mkSimpleId st]
getSortParamsStringAux (' ' : cs) st = getSortParamsStringAux cs st
getSortParamsStringAux (c : cs) st = getSortParamsStringAux cs (st ++ [c])
getSortParamsStringAux [] st = [mkSimpleId st]
-- | checks if the target of the view is completely instantiated (to modules)
isInstantiated :: [Token] -> ModExp -> Bool
isInstantiated ths (SummationModExp me1 me2) = isInstantiated ths me1 &&
isInstantiated ths (RenamingModExp modExp _) = isInstantiated ths modExp
isInstantiated _ (InstantiationModExp _ _) = True
-- | rename the parameterized sorts and computes if they are still parameterized
applyRenamingParamSorts :: SymbolMap -> [ParamSort] -> [ParamSort]
applyRenamingParamSorts sm = foldr (applyRenamingParamSort sm) []
applyRenamingParamSort :: SymbolMap -> ParamSort -> [ParamSort]
applyRenamingParamSort sm (tok, params) acc = case
Map.member tok sm of
False -> (tok, params) : acc
ps = getSortsParameterizedBy params [tok']
-- | removes the repetitions from a list
deleteRepeated :: [ParamSort] -> [ParamSort]
deleteRepeated (p : ps) = if elem p ps
else p : deleteRepeated ps
-- | returns the first element from the triple
-- | instantiate the parametric sorts
-- ParamNames -> ViewName -> Map of views -> Parametricsorts
instantiateSorts :: [Token] -> [Token] -> ViewMap -> Morphism -> [ParamSort]
-> ([ParamSort], Morphism)
instantiateSorts _ _ _ morph [] = ([], morph)
instantiateSorts params views vm morph (ps : pss) = (nps'' ++ res_ps, res_morph)
where np4s = newParamers4sorts params views vm
nps = instantiateSort ps params views
nps' = addNewParams2sort nps np4s
nps'' = if null (snd nps') then [] else [nps']
morph' = extendWithSortRenaming (fst ps) (fst nps') morph
(res_ps, res_morph) = instantiateSorts params views vm morph' pss
-- | computes the theories that have to be further instantiated
newParamers4sorts :: [Token] -> [Token] -> ViewMap -> [Token]
newParamers4sorts (param : ps) (view : vs) vm = case
Map.member view vm of
False -> newParamers4sorts ps vs vm
(_, _, _, _, inst) = fromJust $
Map.lookup view vm
in param' ++ newParamers4sorts ps vs vm
newParamers4sorts _ _ _ = []
-- | creates a new parameterized sort
addNewParams2sort :: ParamSort -> [Token] -> ParamSort
addNewParams2sort (Sort tok, _) lps@(_:_) = (Sort tok', lps)
where tok' = mkSimpleId $ concat [show tok, "`{", printNewParams4sort lps, "`}"]
addNewParams2sort (Kind tok, _) lps@(_:_) = (Kind tok', lps)
where tok' = mkSimpleId $ concat [show tok, "`{", printNewParams4sort lps, "`}"]
addNewParams2sort (ps, _) _ = (ps, [])
-- | introduces commas between the tokens
printNewParams4sort :: [Token] -> String
printNewParams4sort [] = ""
printNewParams4sort [p] = show p
printNewParams4sort (p : ps) = concat [show p, "`,", printNewParams4sort ps]
-- Params: Parameterized sort -> Parameter to be replaced -> New name of the parameter
instantiateSort :: ParamSort -> [Token] -> [Token] -> ParamSort
instantiateSort sp@(Sort tok, tok_params) (p : ps) (v : vs) = case elem p tok_params of
False -> instantiateSort sp ps vs
tok' = mkSimpleId $ instantiateSortString (show tok) (show p) (show v)
in instantiateSort (Sort tok', tok_params) ps vs
instantiateSort sp@(Kind tok, tok_params) (p : ps) (v : vs) = case elem p tok_params of
False -> instantiateSort sp ps vs
tok' = mkSimpleId $ instantiateSortString (show tok) (show p) (show v)
in instantiateSort (Kind tok', tok_params) ps vs
instantiateSort ps _ _ = ps
-- | replaces one param by one view in a sort identifier
-- sort id -> param id -> view id
instantiateSortString :: String -> String -> String -> String
instantiateSortString ('{' : cs) param view = 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 [] _ _ = ""
-- | replaces one param by one view in the list of parameters
-- parameters list -> param id -> view id
instantiateSortStringAux :: String -> String -> String -> String -> String
instantiateSortStringAux ('`' : ',' : ps) param view acc = value ++ "`," ++
instantiateSortStringAux ps param view ""
where value = if acc == param
instantiateSortStringAux ('`' : '}' : _) param view acc = value ++ "`}"
where value = if acc == param
instantiateSortStringAux (p : ps) param view acc =
instantiateSortStringAux ps param view (acc ++ [p])
instantiateSortStringAux _ _ _ acc = acc
-- | qualifies the source sorts in the renamigs
qualifyRenamings :: Token -> [Renaming] -> [Renaming]
qualifyRenamings t = map (qualifyRenaming t)
-- | qualifies the source sort in the renaming. Sorts only appear in operator mappings
-- with profile and sort mappings
qualifyRenaming :: Token -> Renaming -> Renaming
qualifyRenaming p rnm = case rnm of
OpRenaming2 from ar co to -> OpRenaming2 from (map (qualifyType p) ar)
SortRenaming from to -> SortRenaming ((qualifySort p) from) to
-- | qualifies both the source and target sorts in the renamings
qualifyRenamings2 :: Token -> [Renaming] -> [Renaming]
qualifyRenamings2 t = map (qualifyRenaming2 t)
-- | qualifies both the source and target sorts in the renaming.
-- Sorts only appear in operator mappings with profile and sort mappings
qualifyRenaming2 :: Token -> Renaming -> Renaming
qualifyRenaming2 p rnm = case rnm of
OpRenaming2 from ar co to -> OpRenaming2 from (map (qualifyType p) ar)
SortRenaming from to -> SortRenaming ((qualifySort p) from) ((qualifySort p) to)
-- | creates a renaming to substitute the sorts qualified by a parameter name
-- with a new parameter name due to a parameter binding
createQualifiedSortRenaming :: Token -> Token -> Symbols -> [Renaming]
createQualifiedSortRenaming _ _ [] = []
createQualifiedSortRenaming old new (s : ss) = case old == new of
False -> rnm : createQualifiedSortRenaming old new ss
where rnm = SortRenaming (qualifiedSort old' s')
-- | qualifies with the given parameter the token
qualifiedSort :: Token -> Token -> Sort
qualifiedSort param sort = SortId $ mkSimpleId $ concat [show param, "$", show sort]
-- | qualifies with the given parameter the sort
qualifySort :: Token -> Sort -> Sort
qualifySort p (SortId s) = qualifiedSort p s
-- | qualifies with the given parameter the type
qualifyType :: Token -> Type -> Type
qualifyType p (TypeSort (SortId s)) = TypeSort $ qualifiedSort p s
-- | qualifies the symbols in the theory imported with the parameter name
-- given as first parameter
createQualificationTh2Mod :: Token -> Symbols -> [Renaming]
createQualificationTh2Mod _ [] = []
createQualificationTh2Mod par (s : ss) =
rnm : createQualificationTh2Mod par ss
rnm = SortRenaming (SortId s') (qualifiedSort par' s')
-- | generates the library and the development graph from the path of the
anaMaudeFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
dg <- directMaudeParsing file
let name = emptyLibName "Maude_Module"