Skip to content

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

Open
yaswanth169 wants to merge 1 commit intoboyland:masterfrom
yaswanth169:fix/issue-137-non-abstract-requires
Open

Fix #137: non-abstract requires components don't need explicit args#139
yaswanth169 wants to merge 1 commit intoboyland:masterfrom
yaswanth169:fix/issue-137-non-abstract-requires

Conversation

@yaswanth169
Copy link
Copy Markdown

Title: Fix #137: Non-abstract components in requires don't need explicit arguments


Description:

Problem

When a module had non-abstract components (syntax, judgments, or theorems with concrete definitions) in its requires section, users were required to pass them as explicit arguments during instantiation. This was unnecessary — non-abstract components are self-contained and don't
need to be "filled in" by the caller.

For example, given a functor:
requires
abstract syntax id
abstract syntax nonid
syntax e ::= id | nonid ← non-abstract, should not need an arg
abstract judgment add: e + e = e

Users had to write:
module m = functor[id-impl, nonid-impl, e-impl, add-impl] ← e-impl was unnecessary

Fix

Only abstract components now require explicit arguments during instantiation. Non-abstract components are automatically moved into the instantiated module's body.

Changes:

  • ModuleComponent.java — added isAbstract() to the interface
  • Syntax.java — declared isAbstract() as abstract on the base class
  • Sugar.java — implemented isAbstract() returning false (sugar is never abstract)
  • Theorem.java — exposed existing isAbstract field via interface method
  • CompUnit.java — filters out non-abstract params when counting expected arguments; moves non-abstract parts from requires to provides during instantiation; applies derived substitutions so that non-abstract syntax types used in abstract judgment forms are correctly renamed

Regression tests updated (modulegood05, modulegood06, test1) to remove the now-unnecessary non-abstract arguments.

New regression tests added:

  • regression/modulegood11/ — functor with a non-abstract judgment in requires, instantiated with only the abstract arg
  • regression/modulebad10/ — verifies that providing too many arguments (including one for a non-abstract component) still raises an error

@boyland
Copy link
Copy Markdown
Owner

boyland commented Mar 30, 2026

This would break my fix to issue #136. Please see why. As I mentioned in my comment on issue #135 and issue #137, changing the order of things is a breaking change.

@yaswanth169
Copy link
Copy Markdown
Author

Thanks for pointing that out. I see the concern about breaking changes related to #136 and ordering.

I will revisit the interaction between this change and the existing behavior to understand where the conflict arises and ensure we don’t break the expected ordering semantics. Will update once I have analyzed it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Are rules permitted in requires/instantiation?

2 participants