Fix #137: non-abstract requires components don't need explicit args

regression/modulebad10/functor.slf

@@ -0,0 +1,18 @@
+package regression.modulebad10
+
+module functor
+
+requires
+
+abstract syntax e
+
+judgment eq: e = e
+
+  --- eq-refl
+  e = e
+
+provides
+
+terminals nil
+
+syntax l ::= nil | e, l

regression/modulebad10/test.slf

@@ -0,0 +1,14 @@
+package regression.modulebad10
+
+module test provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+
+judgment nat-eq: n = n
+
+  --- nat-refl
+  n = n
+
+module m = regression.modulebad10.functor[n, nat-eq] //!

regression/modulegood05/test.slf

@@ -82,12 +82,11 @@ end theorem
 
 module boolbt = regression.modulegood05.foldablebt
 [
-  boolid, 
-  boolnonid, 
-  b, 
-  lor, 
-  lor-left-id, 
-  lor-right-id, 
+  boolid,
+  boolnonid,
+  lor,
+  lor-left-id,
+  lor-right-id,
   lor-commutative
 ]
 

regression/modulegood06/test.slf

@@ -76,7 +76,7 @@ theorem lor-total:
   proof by unproved //!
 end theorem
 
-module boolbt = regression.modulegood06.foldablebt[boolid, boolnonid, b, lor, lor-commutative, lor-associative, lor-total]
+module boolbt = regression.modulegood06.foldablebt[boolid, boolnonid, lor, lor-commutative, lor-associative, lor-total]
 
 syntax bt = boolbt.bt ::= Leaf | Node bt b bt
 

regression/modulegood11/functor.slf

@@ -0,0 +1,20 @@
+package regression.modulegood11
+
+module functor
+
+requires
+
+abstract syntax e
+
+judgment eq: e = e
+
+  --- eq-refl
+  e = e
+
+provides
+
+theorem self-equal:
+  forall e1
+  exists e1 = e1
+  proof by rule eq-refl
+end theorem

regression/modulegood11/test.slf

@@ -0,0 +1,17 @@
+package regression.modulegood11
+
+module test provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+
+module m = regression.modulegood11.functor[n]
+
+judgment n-eq = m.eq : n = n
+
+theorem nat-self-equal:
+  forall n1
+  exists n1 = n1
+  proof by rule m.eq-refl
+end theorem

regression/test1/set.slf

@@ -28,7 +28,7 @@ provides
 
 terminals in notin ok
 
-module repm = regression.test1.list[e,elem-eq]
+module repm = regression.test1.list[e]
 
 syntax r = repm.l
   ::= 0

regression/test1/test.slf

@@ -7,7 +7,7 @@ module nat = org.sasylf.util.Natural
 syntax n = nat.n
 
 module setb =
-regression.test1.set[n,nat.equal,nat.notequal,nat.ne-anti-reflexive,nat.eq-or-ne]
+regression.test1.set[n,nat.notequal,nat.ne-anti-reflexive,nat.eq-or-ne]
 
 terminals in
 

src/edu/cmu/cs/sasylf/ast/CompUnit.java

@@ -341,6 +341,10 @@ public Optional<CompUnit> accept(List<ModuleComponent> args, ModulePart mp, Cont
 			param.collectTopLevelAsModuleComponents(moduleParams);
 		});
 
+		// Only abstract components require explicit arguments;
+		// non-abstract components are included in the instantiated module automatically.
+		moduleParams.removeIf(mc -> !mc.isAbstract());
+
 		int numParams = moduleParams.size();
 		int numArgs = args.size();
 
@@ -377,6 +381,23 @@ private boolean doApplication(List<ModuleComponent> args, ModulePart mp, List<Mo
 		Map<Syntax, Syntax> paramToArgSyntax = new IdentityHashMap<Syntax, Syntax>();
 		Map<Judgment, Judgment> paramToArgJudgment = new IdentityHashMap<Judgment, Judgment>();
 
+		// Collect non-abstract syntax objects before moving (needed for derived substitution later)
+		List<Syntax> nonAbstractSyntaxes = new ArrayList<>();
+		for (Part p : this.params) {
+			if (p instanceof SyntaxPart) {
+				for (Syntax s : ((SyntaxPart) p).getSyntax()) {
+					if (!s.isAbstract()) {
+						nonAbstractSyntaxes.add(s);
+					}
+				}
+			}
+		}
+
+		// Move non-abstract Parts from requires (params) to provides (body) so they
+		// are included in the instantiated module and receive abstract-param substitutions
+		List<Part> nonAbstractParts = extractNonAbstractParts(this.params);
+		this.parts.addAll(0, nonAbstractParts);
+
 		this.params.clear();
 
 		for (int i = 0; i < args.size(); i++) {
@@ -395,11 +416,66 @@ private boolean doApplication(List<ModuleComponent> args, ModulePart mp, List<Mo
 			}
 
 		}
-
+
+		// Apply derived substitutions for non-abstract syntax types that were implicitly
+		// mapped through abstract judgment form structure checking.
+		// For example, if abstract judgment "add: e + e = e" is matched against concrete
+		// "lor: b \/ b = b", the form check records e->b. We apply that substitution
+		// so the non-abstract syntax e (now in body) and all references to it use b.
+		for (Syntax nonAbstractSyntax : nonAbstractSyntaxes) {
+			String syntaxName = nonAbstractSyntax.getName();
+			for (Map.Entry<Syntax, Syntax> entry : paramToArgSyntax.entrySet()) {
+				if (!entry.getKey().isAbstract() && entry.getKey().getName().equals(syntaxName)) {
+					Syntax argSyntax = entry.getValue();
+					SubstitutionData derivedSd = new SubstitutionData(
+						syntaxName,
+						argSyntax.getName(),
+						argSyntax.getOriginalDeclaration(),
+						nonAbstractSyntax.getOriginalDeclaration()
+					);
+					this.substitute(derivedSd);
+					break;
+				}
+			}
+		}
+
 		this.moduleName = moduleName;
 
 		return true;
-
+
+	}
+
+	/**
+	 * Extract all Parts containing non-abstract components from the given list of param Parts.
+	 * Creates new Part objects containing only the non-abstract components of each Part.
+	 * These Parts should be moved to the module body so they are included in the instantiation.
+	 * @param paramParts the list of Parts from the requires section
+	 * @return a list of new Parts containing only non-abstract components
+	 */
+	private List<Part> extractNonAbstractParts(List<Part> paramParts) {
+		List<Part> result = new ArrayList<>();
+		for (Part p : paramParts) {
+			if (p instanceof SyntaxPart) {
+				List<Syntax> nonAbstract = new ArrayList<>();
+				for (Syntax s : ((SyntaxPart) p).getSyntax()) {
+					if (!s.isAbstract()) nonAbstract.add(s);
+				}
+				if (!nonAbstract.isEmpty()) result.add(new SyntaxPart(nonAbstract));
+			} else if (p instanceof JudgmentPart) {
+				List<Judgment> nonAbstract = new ArrayList<>();
+				for (Judgment j : ((JudgmentPart) p).judgments) {
+					if (!j.isAbstract()) nonAbstract.add(j);
+				}
+				if (!nonAbstract.isEmpty()) result.add(new JudgmentPart(nonAbstract));
+			} else if (p instanceof TheoremPart) {
+				List<Theorem> nonAbstract = new ArrayList<>();
+				for (Theorem t : ((TheoremPart) p).getTheorems()) {
+					if (!t.isAbstract()) nonAbstract.add(t);
+				}
+				if (!nonAbstract.isEmpty()) result.add(new TheoremPart(nonAbstract));
+			}
+		}
+		return result;
 	}
 
 }

src/edu/cmu/cs/sasylf/ast/ModuleComponent.java

@@ -55,4 +55,14 @@ public Optional<SubstitutionData> matchesParam(
    */
   public ModuleComponent copy(CopyData cd);
 
+  /**
+   * Returns whether this module component is abstract (i.e., requires an explicit argument
+   * during module instantiation).
+   * <br/><br/>
+   * Non-abstract components (those with concrete definitions) are automatically included
+   * in the instantiated module without requiring an explicit argument.
+   * @return true if this component is abstract, false otherwise
+   */
+  public boolean isAbstract();
+
 }

src/edu/cmu/cs/sasylf/ast/Sugar.java

@@ -46,6 +46,11 @@ public Sugar(Element lhs, Clause rhs) {
 		if (rhs != null) this.setEndLocation(rhs.getEndLocation());
 	}
 
+	@Override
+	public boolean isAbstract() {
+		return false;
+	}
+
 	@Override
 	public void prettyPrint(PrintWriter out) {
 		sugar.prettyPrint(out);

src/edu/cmu/cs/sasylf/ast/Syntax.java

@@ -87,6 +87,14 @@ public void checkSubordination() {}
 	 */
 	public abstract SyntaxDeclaration getOriginalDeclaration();
 
+	/**
+	 * Returns whether this syntax is abstract (has no concrete productions).
+	 * Abstract syntax requires an explicit argument during module instantiation.
+	 * @return true if this syntax is abstract, false otherwise
+	 */
+	@Override
+	public abstract boolean isAbstract();
+
 	/**
 	 * Substitute inside of this Syntax according to the given substitution data.
 	 * @param sd substitution data to use

src/edu/cmu/cs/sasylf/ast/Theorem.java

@@ -50,6 +50,8 @@ public Theorem(String n, Location l, boolean abs) {
 
 	public List<Fact> getForalls() { return foralls; }
 	@Override
+	public boolean isAbstract() { return isAbstract; }
+	@Override
 	public List<Element> getPremises() {
 		List<Element> l = new ArrayList<Element>();
 		for (Fact f : foralls) {