diff --git a/regression/modulebad10/functor.slf b/regression/modulebad10/functor.slf new file mode 100644 index 00000000..7009abd0 --- /dev/null +++ b/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 diff --git a/regression/modulebad10/test.slf b/regression/modulebad10/test.slf new file mode 100644 index 00000000..4e00ea22 --- /dev/null +++ b/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] //! diff --git a/regression/modulegood05/test.slf b/regression/modulegood05/test.slf index d2104b6c..a14942d2 100644 --- a/regression/modulegood05/test.slf +++ b/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 ] diff --git a/regression/modulegood06/test.slf b/regression/modulegood06/test.slf index 4cce86de..e0fb896a 100644 --- a/regression/modulegood06/test.slf +++ b/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 diff --git a/regression/modulegood11/functor.slf b/regression/modulegood11/functor.slf new file mode 100644 index 00000000..d2090fc1 --- /dev/null +++ b/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 diff --git a/regression/modulegood11/test.slf b/regression/modulegood11/test.slf new file mode 100644 index 00000000..e98076d8 --- /dev/null +++ b/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 diff --git a/regression/test1/set.slf b/regression/test1/set.slf index 0a88a3bf..db4e44f8 100644 --- a/regression/test1/set.slf +++ b/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 diff --git a/regression/test1/test.slf b/regression/test1/test.slf index 212ca03d..12fd25f9 100644 --- a/regression/test1/test.slf +++ b/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 diff --git a/src/edu/cmu/cs/sasylf/ast/CompUnit.java b/src/edu/cmu/cs/sasylf/ast/CompUnit.java index c0b3ec86..b64cf827 100644 --- a/src/edu/cmu/cs/sasylf/ast/CompUnit.java +++ b/src/edu/cmu/cs/sasylf/ast/CompUnit.java @@ -341,6 +341,10 @@ public Optional accept(List 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 args, ModulePart mp, List paramToArgSyntax = new IdentityHashMap(); Map paramToArgJudgment = new IdentityHashMap(); + // Collect non-abstract syntax objects before moving (needed for derived substitution later) + List 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 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 args, ModulePart mp, Listb. 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 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 extractNonAbstractParts(List paramParts) { + List result = new ArrayList<>(); + for (Part p : paramParts) { + if (p instanceof SyntaxPart) { + List 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 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 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; } } diff --git a/src/edu/cmu/cs/sasylf/ast/ModuleComponent.java b/src/edu/cmu/cs/sasylf/ast/ModuleComponent.java index c4da53eb..0bb785ef 100644 --- a/src/edu/cmu/cs/sasylf/ast/ModuleComponent.java +++ b/src/edu/cmu/cs/sasylf/ast/ModuleComponent.java @@ -55,4 +55,14 @@ public Optional matchesParam( */ public ModuleComponent copy(CopyData cd); + /** + * Returns whether this module component is abstract (i.e., requires an explicit argument + * during module instantiation). + *

+ * 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(); + } \ No newline at end of file diff --git a/src/edu/cmu/cs/sasylf/ast/Sugar.java b/src/edu/cmu/cs/sasylf/ast/Sugar.java index f38f8457..379d8634 100644 --- a/src/edu/cmu/cs/sasylf/ast/Sugar.java +++ b/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); diff --git a/src/edu/cmu/cs/sasylf/ast/Syntax.java b/src/edu/cmu/cs/sasylf/ast/Syntax.java index 64dd5563..60885e73 100644 --- a/src/edu/cmu/cs/sasylf/ast/Syntax.java +++ b/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 diff --git a/src/edu/cmu/cs/sasylf/ast/Theorem.java b/src/edu/cmu/cs/sasylf/ast/Theorem.java index 188aa729..a91c30f6 100644 --- a/src/edu/cmu/cs/sasylf/ast/Theorem.java +++ b/src/edu/cmu/cs/sasylf/ast/Theorem.java @@ -50,6 +50,8 @@ public Theorem(String n, Location l, boolean abs) { public List getForalls() { return foralls; } @Override + public boolean isAbstract() { return isAbstract; } + @Override public List getPremises() { List l = new ArrayList(); for (Fact f : foralls) {