imports FOO.bar

USER_MANUAL.md

@@ -275,6 +275,16 @@ of the import with the `public` or `private` keyword immediately prior to the
 module name. A module imported privately does not export its syntax to modules
 that import the module doing the import.
 
+An import statement can also choose to explicitly hide some or all of the
+syntax being imported. If an import's module name is followed by a `.`
+character followed by an attribute name or klabel, then only sentences that
+have that attribute name or productions that have that klabel attribute will
+be imported by that declaration. For example, if I say `imports FOO.bar`, then
+only productions whose klabel attribute is `bar` or whose attribute list
+contains the `bar` attribute will be visible to the importing module. Note that
+all rules, constructors, and sorts declared in that module will still exist
+in the final interpreter.
+
 Following imports, a module can contain zero or more sentences. A sentence can
 be a syntax declaration, a rule, a configuration declaration, a context, a
 claim, or a context alias. Details on each of these can be found in subsequent

k-distribution/tests/regression-new/checks/partialImport.k

@@ -0,0 +1,27 @@
+module PARTIALIMPORT
+  imports A
+  imports D
+
+  rule foo() => .K
+  rule bar() => .K
+  rule alsoAFoo() => .K
+  rule boo() => .K
+endmodule
+
+module A
+  imports B.foo
+endmodule
+
+module B
+  imports C
+  syntax Foo ::= foo()
+  syntax Bar ::= bar()
+endmodule
+
+module C
+  syntax Foo ::= alsoAFoo() [foo]
+endmodule
+
+module D [private]
+  syntax Boo ::= boo()
+endmodule

k-distribution/tests/regression-new/checks/partialImport.k.out

@@ -0,0 +1,7 @@
+[Error] Inner Parser: Parse error: unexpected token ')'.
+	Source(partialImport.k)
+	Location(6,12,6,13)
+[Error] Inner Parser: Parse error: unexpected token ')'.
+	Source(partialImport.k)
+	Location(8,12,8,13)
+[Error] Compiler: Had 2 parsing errors.

k-distribution/tests/regression-new/import/Makefile

@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/import/test.k

@@ -0,0 +1,20 @@
+module TEST
+  imports A
+
+  rule foo() => .K
+  rule alsoAFoo() => .K
+endmodule
+
+module A
+  imports B.foo
+endmodule
+
+module B
+  imports C
+  syntax Foo ::= foo()
+  syntax Bar ::= bar()
+endmodule
+
+module C
+  syntax Foo ::= alsoAFoo() [foo]
+endmodule

kernel/src/main/java/org/kframework/kil/Import.java

@@ -9,17 +9,20 @@ public class Import extends ModuleItem {
 
     String name;
     boolean isPublic;
+    String tag;
 
-    public Import(String importName, boolean isPublic) {
+    public Import(String importName, boolean isPublic, String tag) {
         super();
         name = importName;
         this.isPublic = isPublic;
+        this.tag = tag;
     }
 
-    public Import(String importName, boolean isPublic, Location loc, Source source) {
+    public Import(String importName, boolean isPublic, String tag, Location loc, Source source) {
         super(loc, source);
         this.name = importName;
         this.isPublic = isPublic;
+        this.tag = tag;
     }
 
     @Override
@@ -31,6 +34,9 @@ public void toString(StringBuilder sb) {
           sb.append("public ");
         }
         sb.append(name);
+        if (tag != null) {
+          sb.append(".").append(tag);
+        }
     }
 
     public String getName() {
@@ -42,10 +48,18 @@ public void setName(String name) {
     }
 
     public boolean isPublic() {
-      return isPublic;
+        return isPublic;
     }
 
     public void setPublic(boolean isPublic) {
-      this.isPublic = isPublic;
+        this.isPublic = isPublic;
+    }
+
+    public String getTag() {
+        return tag;
+    }
+
+    public void setTag() {
+        this.tag = tag;
     }
 }

kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java

@@ -28,6 +28,7 @@
 import java.util.Comparator;
 import java.util.HashSet;
 import java.util.List;
+import java.util.Optional;
 import java.util.Set;
 import java.util.function.Function;
 import java.util.stream.Collectors;
@@ -90,7 +91,11 @@ public FlatModule toFlatModule(Module m) {
     }
 
     public org.kframework.definition.FlatImport apply(Import imp) {
-        return org.kframework.definition.FlatImport.apply(imp.getName(), imp.isPublic(), convertAttributes(imp));
+        return org.kframework.definition.FlatImport.apply(
+            imp.getName(),
+            imp.isPublic(),
+            imp.getTag() == null ? immutable(Optional.empty()) : immutable(Optional.of(Tag(imp.getTag()))),
+            convertAttributes(imp));
     }
 
     public org.kframework.definition.Definition apply(Definition d) {

kernel/src/main/java/org/kframework/parser/inner/generator/RuleGrammarGenerator.java

@@ -152,7 +152,7 @@ public Module getProgramsGrammar(Module mod) {
                 UnaryOperator<Import> f = _import -> {
                     Option<Module> programParsing = baseK.getModule(_import.module().name() + "-PROGRAM-PARSING");
                     if (programParsing.isDefined()) {
-                        return Import(programParsing.get(), _import.isPublic());
+                        return Import(programParsing.get(), _import.isPublic(), _import.tag());
                     }
                     return _import;
                 };

kernel/src/main/java/org/kframework/parser/json/JsonParser.java

@@ -45,9 +45,11 @@
 import java.util.ArrayList;
 import java.util.HashSet;
 import java.util.List;
+import java.util.Optional;
 import java.util.Set;
 
 import static org.kframework.Collections.*;
+import static org.kframework.definition.Constructors.*;
 import static org.kframework.kore.KORE.*;
 
 /**
@@ -147,7 +149,11 @@ public static FlatModule toFlatModule(JsonObject data) throws IOException {
 
         JsonArray jsonimports = data.getJsonArray("imports");
         Set<FlatImport> imports = new HashSet<>();
-        jsonimports.getValuesAs(JsonObject.class).forEach(i -> imports.add(FlatImport.apply(i.getString("name"), i.getBoolean("public"), Att.empty())));
+        jsonimports.getValuesAs(JsonObject.class).forEach(i -> imports.add(FlatImport.apply(
+                i.getString("name"),
+                i.getBoolean("public"),
+                immutable(Optional.ofNullable(i.getString("tag")).map(s -> Tag(s))),
+                Att.empty())));
 
         JsonArray sentences = data.getJsonArray("localSentences");
         Set<Sentence> localSentences = new HashSet<>();

kernel/src/main/java/org/kframework/unparser/ToJson.java

@@ -48,12 +48,13 @@
 
 import javax.json.Json;
 import javax.json.stream.JsonGenerator;
-import javax.json.JsonWriterFactory;
 import javax.json.JsonArrayBuilder;
 import javax.json.JsonObject;
 import javax.json.JsonObjectBuilder;
-import javax.json.JsonWriter;
 import javax.json.JsonStructure;
+import javax.json.JsonValue;
+import javax.json.JsonWriter;
+import javax.json.JsonWriterFactory;
 
 import scala.Enumeration;
 import scala.Option;
@@ -143,8 +144,14 @@ public static JsonStructure toJson(FlatModule mod) {
         JsonArrayBuilder imports = Json.createArrayBuilder();
         stream(mod.imports()).forEach(i -> {
           JsonObjectBuilder jimp = Json.createObjectBuilder();
-          jmod.add("name", i.name());
-          jmod.add("isPublic", i.isPublic());
+          jimp.add("name", i.name());
+          jimp.add("isPublic", i.isPublic());
+          Optional<String> tag = mutable(i.tag()).map(t -> t.name());
+          if (tag.isPresent()) {
+            jimp.add("tag", tag.get());
+          } else {
+            jimp.add("tag", JsonValue.NULL);
+          }
           imports.add(jimp.build());
         });
 

kernel/src/main/javacc/Outer.jj

@@ -425,6 +425,7 @@ PARSER_END(Outer)
 | <MODULE: "module"> : MODNAME_STATE
 | <IMPORTS: "imports"> : MODNAME_STATE
 | <IMPORTS2: "import"> : MODNAME_STATE
+| <IMPORT_DOT: "."> : KLABEL_STATE
 
 | <STRING: "\"" (~["\"", "\\", "\n"] |
                  "\\\"" | "\\n" | "\\r" | "\\t" | "\\\\")* "\"">
@@ -707,10 +708,11 @@ void Module(List<DefinitionItem> items) : { Location loc = startLoc(); }
 }
 
 /** Parses an Import and adds it to module */
-void Import(Module module): { Location loc = startLoc(); boolean isPublic = module.getAttribute("private") == null; }
+void Import(Module module): { Location loc = startLoc(); boolean isPublic = module.getAttribute("private") == null; String tag = null; String modname; }
 {
-  ("imports" | "import") ((<IMPORTSPRIVATE> { isPublic = false; }) | (<IMPORTSPUBLIC> { isPublic = true; }) )? <MODNAME>
-  { module.appendModuleItem(markLoc(loc, new Import(image(), isPublic))); }
+  ("imports" | "import") ((<IMPORTSPRIVATE> { isPublic = false; }) | (<IMPORTSPUBLIC> { isPublic = true; }) )? <MODNAME> { modname = image(); }
+  ("." <KLABEL> { tag = image(); } )?
+  { module.appendModuleItem(markLoc(loc, new Import(modname, isPublic, tag))); }
 }
 
 /** Parses a Sentence and adds it to 'module' */

kernel/src/test/java/org/kframework/parser/outer/OuterParsingTest.java

@@ -0,0 +1,73 @@
+// Copyright (c) 2014-2019 K Team. All Rights Reserved.
+package org.kframework.parser.outer;
+
+import java.util.List;
+
+import junit.framework.Assert;
+
+import org.junit.Test;
+import org.kframework.attributes.Source;
+import org.kframework.kil.DefinitionItem;
+import org.kframework.kil.Import;
+import org.kframework.kil.Module;
+import org.kframework.kil.StringSentence;
+
+public class OuterParsingTest {
+
+    @Test
+    public void testEmptyRules() {
+        String def = "module TEST rule endmodule";
+
+        List<DefinitionItem> defItemList = Outer.parse(Source.apply("generated by OuterParsingTests"), def, null);
+        Assert.assertEquals(1, defItemList.size());
+
+        Module mod = (Module) defItemList.get(0);
+        Assert.assertEquals(1, mod.getItems().size());
+        StringSentence sen = (StringSentence) mod.getItems().get(0);
+        Assert.assertEquals(sen.getContent(), "");
+    }
+
+    @Test
+    public void testClaimKeyword() throws Exception {
+        String def = "module TEST claim X => Y endmodule";
+
+        List<DefinitionItem> defItemList = Outer.parse(Source.apply("generated by OuterParsingTests"), def, null);
+        Assert.assertEquals(1, defItemList.size());
+
+        Module mod = (Module) defItemList.get(0);
+        Assert.assertEquals(1, mod.getItems().size());
+        StringSentence sen = (StringSentence) mod.getItems().get(0);
+        Assert.assertEquals(sen.getContent(), "X => Y");
+        Assert.assertEquals(sen.getType(), "claim");
+    }
+
+    @Test
+    public void testImport() {
+        String def = "module A endmodule module TEST imports A imports private A imports public A imports A.foo endmodule";
+
+        List<DefinitionItem> defItemList = Outer.parse(Source.apply("generated by OuterParsingTestes"), def, null);
+        Assert.assertEquals(2, defItemList.size());
+
+        Module a = (Module) defItemList.get(0);
+        Assert.assertEquals(0, a.getItems().size());
+
+        Module mod = (Module) defItemList.get(1);
+        Assert.assertEquals(4, mod.getItems().size());
+
+        Import sen = (Import) mod.getItems().get(0);
+        Assert.assertEquals(true, sen.isPublic());
+        Assert.assertEquals(null, sen.getTag());
+
+        sen = (Import) mod.getItems().get(1);
+        Assert.assertEquals(false, sen.isPublic());
+        Assert.assertEquals(null, sen.getTag());
+
+        sen = (Import) mod.getItems().get(2);
+        Assert.assertEquals(true, sen.isPublic());
+        Assert.assertEquals(null, sen.getTag());
+
+        sen = (Import) mod.getItems().get(3);
+        Assert.assertEquals(true, sen.isPublic());
+        Assert.assertEquals("foo", sen.getTag());
+    }
+}

kore/src/main/scala/org/kframework/collections.scala

@@ -5,6 +5,7 @@ package org.kframework
 import java.util
 
 import collection.JavaConverters._
+import java.util.Optional
 import java.util.stream.StreamSupport
 import scala.collection.mutable.Builder
 import scala.collection.mutable.ListBuffer
@@ -21,6 +22,7 @@ object Collections {
   def immutable[T](s: java.util.List[T]): Seq[T] = s.asScala
   def immutable[K, V](s: java.util.Map[K, V]): Map[K, V] = s.asScala
   def immutable[T](s: Array[T]): Seq[T] = s
+  def immutable[T](s: java.util.Optional[T]): Option[T] = if (s.isPresent) Some(s.get) else None
 
   def mutable[T](s: scala.List[T]): java.util.List[T] = s.asJava
   def mutable[T](s: Seq[T]): java.util.List[T] = s.asJava
@@ -30,6 +32,7 @@ object Collections {
     x.addAll(s.asJava)
     x
   }
+  def mutable[T](s: Option[T]): java.util.Optional[T] = if (s.isDefined) Optional.of(s.get) else Optional.empty[T]
 
   def iterable[T](c: Iterable[T]): java.lang.Iterable[T] = c.asJava
   def stream[T](c: Iterable[T]): java.util.stream.Stream[T] = StreamSupport.stream(c.asJava.spliterator(), false);

kore/src/main/scala/org/kframework/definition/Constructors.scala

@@ -22,7 +22,10 @@ object Constructors {
     definition.Definition(mainModule, modules, att)
 
   def Import(module: Module, isPublic: Boolean) =
-    definition.Import(module, isPublic)
+    definition.Import(module, isPublic, None)
+
+  def Import(module: Module, isPublic: Boolean, tag: Option[Tag]) =
+    definition.Import(module, isPublic, tag)
 
   def Module(name: String, imports: Set[Import], sentences: Set[Sentence], att: attributes.Att) =
     definition.Module(name, imports, sentences, att)