diff --git a/src/kink.md b/src/kink.md index 95cb47d..8852c7d 100644 --- a/src/kink.md +++ b/src/kink.md @@ -110,26 +110,34 @@ module META-ACCESSORS ``` ```k - syntax Bool ::= #isSortDeclared(ModuleName, SortName) [function, withConfig] - rule [[ #isSortDeclared(MNAME:ModuleName, SORT:SortName) => true ]] + syntax Bool ::= #isSortDeclaredMod(ModuleName, SortName) [function] + rule [[ #isSortDeclaredMod(MNAME:ModuleName, SORT:SortName) => true ]] MNAME sort SORT { PARAMS } ATTRS - rule #isSortDeclared(_, _) => false [owise] + rule #isSortDeclaredMod(_, _) => false [owise] + + syntax Bool ::= #isSortDeclared(ModuleName, SortName) [function] + syntax Bool ::= #isSortDeclaredSet(Set, SortName) [function] + rule #isSortDeclared(MNAME, SNAME) + => #isSortDeclaredSet(#getImportedModules(MNAME), SNAME) + rule #isSortDeclaredSet(SetItem(M) Ms, SNAME) + => #isSortDeclaredMod(M, SNAME) orBool #isSortDeclaredSet(Ms, SNAME) + rule #isSortDeclaredSet(.Set, SNAME) => false ``` ```k - syntax Bool ::= #isSymbolDeclaredSingleModule(ModuleName, SymbolName) [function] - rule [[ #isSymbolDeclaredSingleModule(MNAME, SYMBOL) => true ]] + syntax Bool ::= #isSymbolDeclaredMod(ModuleName, SymbolName) [function] + rule [[ #isSymbolDeclaredMod(MNAME, SYMBOL) => true ]] MNAME (symbol SYMBOL { _ } ( _ ) : _ ATTRS) - rule #isSymbolDeclaredSingleModule(_, _) => false [owise] + rule #isSymbolDeclaredMod(_, _) => false [owise] syntax Bool ::= #isSymbolDeclared(ModuleName, SymbolName) [function] syntax Bool ::= #isSymbolDeclaredSet(Set, SymbolName) [function] rule #isSymbolDeclared(MNAME, SNAME) => #isSymbolDeclaredSet(#getImportedModules(MNAME), SNAME) rule #isSymbolDeclaredSet(SetItem(M) Ms, SNAME) - => #isSymbolDeclaredSingleModule(M, SNAME) orBool #isSymbolDeclaredSet(Ms, SNAME) + => #isSymbolDeclaredMod(M, SNAME) orBool #isSymbolDeclaredSet(Ms, SNAME) rule #isSymbolDeclaredSet(.Set, SNAME) => false ```