Evolog Modules: Parsing of module definitions

alpha-asp · Jul 24, 2024 · fd9f6a7 · fd9f6a7
1 parent aad5520
commit fd9f6a7
Show file tree

Hide file tree

Showing 12 changed files with 254 additions and 25 deletions.
diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/programs/InputProgram.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/programs/InputProgram.java
@@ -1,5 +1,6 @@
 package at.ac.tuwien.kr.alpha.api.programs;
 
+import at.ac.tuwien.kr.alpha.api.programs.modules.Module;
 import at.ac.tuwien.kr.alpha.api.programs.rules.Rule;
 import at.ac.tuwien.kr.alpha.api.programs.rules.heads.Head;
 import at.ac.tuwien.kr.alpha.api.programs.tests.TestCase;
@@ -13,4 +14,6 @@ public interface InputProgram extends Program<Rule<Head>> {
 	 */
 	List<TestCase> getTestCases();
 
+	List<Module> getModules();
+
 }
diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/programs/modules/Module.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/programs/modules/Module.java
@@ -0,0 +1,18 @@
+package at.ac.tuwien.kr.alpha.api.programs.modules;
+
+import at.ac.tuwien.kr.alpha.api.programs.InputProgram;
+import at.ac.tuwien.kr.alpha.api.programs.Predicate;
+
+import java.util.Set;
+
+public interface Module {
+
+	String getName();
+
+	Predicate getInputSpec();
+
+	Set<Predicate> getOutputSpec();
+
+	InputProgram getImplementation();
+
+}
diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/InputProgramImpl.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/InputProgramImpl.java
@@ -33,6 +33,7 @@
 import at.ac.tuwien.kr.alpha.api.programs.rules.Rule;
 import at.ac.tuwien.kr.alpha.api.programs.rules.heads.Head;
 import at.ac.tuwien.kr.alpha.api.programs.tests.TestCase;
+import at.ac.tuwien.kr.alpha.api.programs.modules.Module;
 import at.ac.tuwien.kr.alpha.commons.util.Util;
 
 import java.util.Collections;
@@ -46,20 +47,26 @@
 // TODO rename this to InputProgramImpl or some such
 class InputProgramImpl extends AbstractProgram<Rule<Head>> implements InputProgram {
 
-	static final InputProgramImpl EMPTY = new InputProgramImpl(Collections.emptyList(), Collections.emptyList(), new InlineDirectivesImpl(), Collections.emptyList());
+	static final InputProgramImpl EMPTY = new InputProgramImpl(Collections.emptyList(), Collections.emptyList(), new InlineDirectivesImpl(), Collections.emptyList(), Collections.emptyList());
 
 	private final List<TestCase> testCases;
+	private final List<Module> modules;
 
-	InputProgramImpl(List<Rule<Head>> rules, List<Atom> facts, InlineDirectives inlineDirectives, List<TestCase> testCases) {
+	InputProgramImpl(List<Rule<Head>> rules, List<Atom> facts, InlineDirectives inlineDirectives, List<TestCase> testCases, List<Module> modules) {
 		super(rules, facts, inlineDirectives);
 		this.testCases = testCases;
+		this.modules = modules;
 	}
 
 	@Override
 	public List<TestCase> getTestCases() {
 		return testCases;
 	}
 
+	public List<Module> getModules() {
+		return modules;
+	}
+
 	@Override
 	public String toString() {
 		String ls = System.lineSeparator();

diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/Programs.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/Programs.java
@@ -8,6 +8,7 @@
 import at.ac.tuwien.kr.alpha.api.programs.InlineDirectives;
 import at.ac.tuwien.kr.alpha.api.programs.NormalProgram;
 import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
+import at.ac.tuwien.kr.alpha.api.programs.modules.Module;
 import at.ac.tuwien.kr.alpha.api.programs.rules.NormalRule;
 import at.ac.tuwien.kr.alpha.api.programs.rules.Rule;
 import at.ac.tuwien.kr.alpha.api.programs.rules.heads.Head;
@@ -24,14 +25,18 @@ public static InputProgram emptyProgram() {
 		return InputProgramImpl.EMPTY;
 	}
 
+	public static InputProgram newInputProgram(List<Rule<Head>> rules, List<Atom> facts, InlineDirectives inlineDirectives, List<TestCase> testCases, List<Module> modules) {
+		return new InputProgramImpl(rules, facts, inlineDirectives, testCases, modules);
+	}
+
 	// TODO rename method
 	public static InputProgram newInputProgram(List<Rule<Head>> rules, List<Atom> facts, InlineDirectives inlineDirectives, List<TestCase> testCases) {
-		return new InputProgramImpl(rules, facts, inlineDirectives, testCases);
+		return new InputProgramImpl(rules, facts, inlineDirectives, testCases, Collections.emptyList());
 	}
 
 	// TODO rename method
 	public static InputProgram newInputProgram(List<Rule<Head>> rules, List<Atom> facts, InlineDirectives inlineDirectives) {
-		return new InputProgramImpl(rules, facts, inlineDirectives, Collections.emptyList());
+		return new InputProgramImpl(rules, facts, inlineDirectives, Collections.emptyList(), Collections.emptyList());
 	}
 
 	public static InputProgramBuilder builder() {
@@ -69,6 +74,7 @@ public static class InputProgramBuilder {
 		private InlineDirectives inlineDirectives = new InlineDirectivesImpl();
 
 		private List<TestCase> testCases = new ArrayList<>();
+		private List<Module> modules = new ArrayList<>();
 
 		public InputProgramBuilder(InputProgram prog) {
 			this.addRules(prog.getRules());
@@ -116,12 +122,22 @@ public InputProgramBuilder addTestCases(List<TestCase> testCases) {
 			return this;
 		}
 
+		public InputProgramBuilder addModule(Module module) {
+			this.modules.add(module);
+			return this;
+		}
+
+		public InputProgramBuilder addModules(List<Module> modules) {
+			this.modules.addAll(modules);
+			return this;
+		}
+
 		public InputProgramBuilder accumulate(InputProgram prog) {
-			return this.addRules(prog.getRules()).addFacts(prog.getFacts()).addInlineDirectives(prog.getInlineDirectives()).addTestCases(prog.getTestCases());
+			return this.addRules(prog.getRules()).addFacts(prog.getFacts()).addInlineDirectives(prog.getInlineDirectives()).addTestCases(prog.getTestCases()).addModules(prog.getModules());
 		}
 
 		public InputProgram build() {
-			return Programs.newInputProgram(this.rules, this.facts, this.inlineDirectives, this.testCases);
+			return Programs.newInputProgram(this.rules, this.facts, this.inlineDirectives, this.testCases, this.modules);
 		}
 
 	}

diff --git a/...ns/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/literals/ExternalLiteralImpl.java b/...ns/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/literals/ExternalLiteralImpl.java
@@ -27,24 +27,19 @@
  */
 package at.ac.tuwien.kr.alpha.commons.programs.literals;
 
-import java.util.ArrayList;
-import java.util.Collections;
-import java.util.HashSet;
-import java.util.List;
-import java.util.Set;
-
 import at.ac.tuwien.kr.alpha.api.grounder.Substitution;
 import at.ac.tuwien.kr.alpha.api.programs.atoms.ExternalAtom;
 import at.ac.tuwien.kr.alpha.api.programs.literals.ExternalLiteral;
 import at.ac.tuwien.kr.alpha.api.programs.literals.Literal;
 import at.ac.tuwien.kr.alpha.api.programs.terms.ConstantTerm;
 import at.ac.tuwien.kr.alpha.api.programs.terms.Term;
 import at.ac.tuwien.kr.alpha.api.programs.terms.VariableTerm;
-import at.ac.tuwien.kr.alpha.commons.programs.atoms.AbstractAtom;
 import at.ac.tuwien.kr.alpha.commons.substitutions.BasicSubstitution;
 
+import java.util.*;
+
 /**
- * Contains a potentially negated {@link ExternalAtomImpl}.
+ * Contains a potentially negated {@link ExternalAtom}.
  */
 class ExternalLiteralImpl extends AbstractLiteral implements ExternalLiteral {
 
@@ -67,7 +62,7 @@ public ExternalLiteralImpl negate() {
 	}
 
 	/**
-	 * @see AbstractAtom#substitute(BasicSubstitution)
+	 * @see Literal#substitute(Substitution)
 	 */
 	@Override
 	public ExternalLiteralImpl substitute(Substitution substitution) {

diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/modules/ModuleImpl.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/modules/ModuleImpl.java
@@ -0,0 +1,43 @@
+package at.ac.tuwien.kr.alpha.commons.programs.modules;
+
+import at.ac.tuwien.kr.alpha.api.programs.InputProgram;
+import at.ac.tuwien.kr.alpha.api.programs.Predicate;
+import at.ac.tuwien.kr.alpha.api.programs.modules.Module;
+
+import java.util.Set;
+
+class ModuleImpl implements Module {
+
+	private final String name;
+	private final Predicate inputSpec;
+	private final Set<Predicate> outputSpec;
+	private final InputProgram implementation;
+
+	ModuleImpl(String name, Predicate inputSpec, Set<Predicate> outputSpec, InputProgram implementation) {
+		this.name = name;
+		this.inputSpec = inputSpec;
+		this.outputSpec = outputSpec;
+		this.implementation = implementation;
+	}
+
+	@Override
+	public String getName() {
+		return this.name;
+	}
+
+	@Override
+	public Predicate getInputSpec() {
+		return this.inputSpec;
+	}
+
+	@Override
+	public Set<Predicate> getOutputSpec() {
+		return this.outputSpec;
+	}
+
+	@Override
+	public InputProgram getImplementation() {
+		return this.implementation;
+	}
+
+}
diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/modules/Modules.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/modules/Modules.java
@@ -0,0 +1,19 @@
+package at.ac.tuwien.kr.alpha.commons.programs.modules;
+
+import at.ac.tuwien.kr.alpha.api.programs.InputProgram;
+import at.ac.tuwien.kr.alpha.api.programs.Predicate;
+import at.ac.tuwien.kr.alpha.api.programs.modules.Module;
+
+import java.util.Set;
+
+public final class Modules {
+
+	private Modules() {
+		throw new AssertionError("Cannot instantiate utility class!");
+	}
+
+	public static Module newModule(final String name, final Predicate inputSpec, final Set<Predicate> outputSpec, final InputProgram implementation) {
+		return new ModuleImpl(name, inputSpec, outputSpec, implementation);
+	}
+
+}
diff --git a/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPCore2.g4 b/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPCore2.g4
@@ -56,6 +56,10 @@ classical_literal : MINUS? basic_atom;
 
 builtin_atom : term binop term;
 
+predicate_spec: id '/' NUMBER;
+
+predicate_specs: predicate_spec (COMMA predicate_specs)?;
+
 binop : EQUAL | UNEQUAL | LESS | GREATER | LESS_OR_EQ | GREATER_OR_EQ;
 
 terms : term (COMMA terms)?;
@@ -83,13 +87,16 @@ interval_bound : numeral | VARIABLE;
 
 external_atom : MINUS? AMPERSAND id (SQUARE_OPEN input = terms SQUARE_CLOSE)? (PAREN_OPEN output = terms PAREN_CLOSE)?; // NOT Core2 syntax.
 
-directive : directive_enumeration | directive_test;  // NOT Core2 syntax, allows solver specific directives. Further directives shall be added here.
+directive : directive_enumeration | directive_test | directive_module;  // NOT Core2 syntax, allows solver specific directives. Further directives shall be added here.
 
 directive_enumeration :  SHARP DIRECTIVE_ENUM id DOT;  // NOT Core2 syntax, used for aggregate translation.
 
 // Alpha-specific language extension: Unit Tests (-> https://github.com/alpha-asp/Alpha/issues/237)
 directive_test : SHARP DIRECTIVE_TEST id PAREN_OPEN test_satisfiability_condition PAREN_CLOSE CURLY_OPEN test_input test_assert* CURLY_CLOSE;
 
+// Alpha-specific language extension: Program Modularization (-> https://github.com/madmike200590/evolog-thesis)
+directive_module: SHARP DIRECTIVE_MODULE id PAREN_OPEN module_signature PAREN_CLOSE CURLY_OPEN statements CURLY_CLOSE;
+
 basic_terms : basic_term (COMMA basic_terms)? ;
 
 basic_term : ground_term | variable_term;
@@ -112,3 +119,5 @@ test_assert_all : TEST_ASSERT_ALL CURLY_OPEN statements? CURLY_CLOSE;
 
 test_assert_some : TEST_ASSERT_SOME CURLY_OPEN statements? CURLY_CLOSE;
 
+module_signature : predicate_spec ARROW CURLY_OPEN ('*' | predicate_specs) CURLY_CLOSE;
+
diff --git a/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPLexer.g4 b/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPLexer.g4
@@ -28,6 +28,7 @@ SQUARE_OPEN : '[';
 SQUARE_CLOSE : ']';
 CURLY_OPEN : '{';
 CURLY_CLOSE : '}';
+ARROW : '=>';
 EQUAL : '=';
 UNEQUAL : '<>' | '!=';
 LESS : '<';
@@ -49,6 +50,8 @@ TEST_GIVEN : 'given';
 TEST_ASSERT_ALL : 'assertForAll';
 TEST_ASSERT_SOME : 'assertForSome';
 
+DIRECTIVE_MODULE : 'module';
+
 
 ID : ('a'..'z') ( 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' )*;
 VARIABLE : ('A'..'Z') ( 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' )*;

diff --git a/.../src/main/java/at/ac/tuwien/kr/alpha/core/grounder/instantiation/LiteralInstantiator.java b/.../src/main/java/at/ac/tuwien/kr/alpha/core/grounder/instantiation/LiteralInstantiator.java
@@ -112,7 +112,7 @@ private LiteralInstantiationResult instantiateFixedInterpretationLiteral(FixedIn
 	}
 
 	/**
-	 * Calculates a substitution that adds an enumeration index (see {@link EnumerationLiteral#addEnumerationIndexToSubstitution(BasicSubstitution)})
+	 * Calculates a substitution that adds an enumeration index (see {@link EnumerationLiteral#addEnumerationIndexToSubstitution(Substitution)})
 	 * to the given partial substitution. Due to the special nature of enumeration literals, this method will always return
 	 * {@link LiteralInstantiationResult.Type#CONTINUE} as its result type. This method assumes that the partial substitution has
 	 * <emph>not</emph> been applied to the passed literal.

diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ParseTreeVisitor.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ParseTreeVisitor.java
@@ -50,6 +50,7 @@
 import at.ac.tuwien.kr.alpha.commons.programs.Programs.InputProgramBuilder;
 import at.ac.tuwien.kr.alpha.commons.programs.atoms.Atoms;
 import at.ac.tuwien.kr.alpha.commons.programs.literals.Literals;
+import at.ac.tuwien.kr.alpha.commons.programs.modules.Modules;
 import at.ac.tuwien.kr.alpha.commons.programs.rules.Rules;
 import at.ac.tuwien.kr.alpha.commons.programs.rules.heads.Heads;
 import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms;
@@ -58,6 +59,7 @@
 import at.ac.tuwien.kr.alpha.core.antlr.ASPCore2Parser;
 import org.antlr.v4.runtime.RuleContext;
 import org.antlr.v4.runtime.tree.TerminalNode;
+import org.apache.commons.lang3.tuple.ImmutablePair;
 
 import java.util.*;
 import java.util.function.IntPredicate;
@@ -306,6 +308,9 @@ public Object visitDirective_enumeration(ASPCore2Parser.Directive_enumerationCon
 
 	@Override
 	public Object visitDirective_test(ASPCore2Parser.Directive_testContext ctx) {
+		if (!programBuilders.empty()) {
+			throw new IllegalStateException("Test directives are not allowed in nested programs!");
+		}
 		// directive_test : DIRECTIVE_TEST id PAREN_OPEN test_satisfiability_condition PAREN_CLOSE CURLY_OPEN test_input test_assert* CURLY_CLOSE;
 		String name = visitId(ctx.id());
 		IntPredicate answerSetCountVerifier = visitTest_satisfiability_condition(ctx.test_satisfiability_condition());
@@ -324,6 +329,44 @@ public Object visitDirective_test(ASPCore2Parser.Directive_testContext ctx) {
 		return null;
 	}
 
+	public Object visitDirective_module(ASPCore2Parser.Directive_moduleContext ctx) {
+		if (!programBuilders.empty()) {
+			throw new IllegalStateException("Module directives are not allowed in nested programs!");
+		}
+		// directive_module: SHARP DIRECTIVE_MODULE id PAREN_OPEN module_signature PAREN_CLOSE CURLY_OPEN statements CURLY_CLOSE;
+		String name = visitId(ctx.id());
+		ImmutablePair<Predicate, Set<Predicate>> moduleSignature = visitModule_signature(ctx.module_signature());
+		startNestedProgram();
+		visitStatements(ctx.statements());
+		InputProgram moduleImplementation = endNestedProgram();
+		currentLevelProgramBuilder.addModule(Modules.newModule(name, moduleSignature.getLeft(), moduleSignature.getRight(), moduleImplementation));
+		return null;
+	}
+
+	public ImmutablePair<Predicate, Set<Predicate>> visitModule_signature(ASPCore2Parser.Module_signatureContext ctx) {
+		Predicate inputPredicate = visitPredicate_spec(ctx.predicate_spec());
+		Set<Predicate> outputPredicates = ctx.predicate_specs() != null ? visitPredicate_specs(ctx.predicate_specs()) : Collections.emptySet();
+		return ImmutablePair.of(inputPredicate, outputPredicates);
+	}
+
+	@Override
+	public Set<Predicate> visitPredicate_specs(ASPCore2Parser.Predicate_specsContext ctx) {
+		// predicate_specs : predicate_spec (COMMA predicate_specs)?;
+		Set<Predicate> result = new LinkedHashSet<>();
+		result.add(visitPredicate_spec(ctx.predicate_spec()));
+		if (ctx.predicate_specs() != null) {
+			result.addAll(visitPredicate_specs(ctx.predicate_specs()));
+		}
+		return result;
+	}
+
+	@Override
+	public Predicate visitPredicate_spec(ASPCore2Parser.Predicate_specContext ctx) {
+		String symbol = visitId(ctx.id());
+		int arity = Integer.parseInt(ctx.NUMBER().getText());
+		return Predicates.getPredicate(symbol, arity);
+	}
+
 	@Override
 	public Set<Literal> visitBody(ASPCore2Parser.BodyContext ctx) {
 		// body : ( naf_literal | aggregate ) (COMMA body)?;
@@ -710,14 +753,23 @@ public Assertion visitTestVerifier(Assertion.Mode assertionMode, ASPCore2Parser.
 			return Tests.newAssertion(assertionMode, Programs.emptyProgram());
 		}
 		List<ASPCore2Parser.StatementContext> stmts = ctx.statement();
-		programBuilders.push(currentLevelProgramBuilder);
-		currentLevelProgramBuilder = new InputProgramBuilder();
+		startNestedProgram();
 		for (ASPCore2Parser.StatementContext stmtCtx : stmts) {
 			visit(stmtCtx);
 		}
-		InputProgram verifier = currentLevelProgramBuilder.build();
-		currentLevelProgramBuilder = programBuilders.pop();
+		InputProgram verifier = endNestedProgram();
 		return Tests.newAssertion(assertionMode, verifier);
 	}
 
+	private void startNestedProgram() {
+		programBuilders.push(currentLevelProgramBuilder);
+		currentLevelProgramBuilder = new InputProgramBuilder();
+	}
+
+	private InputProgram endNestedProgram() {
+		InputProgram result = currentLevelProgramBuilder.build();
+		currentLevelProgramBuilder = programBuilders.pop();
+		return result;
+	}
+
 }