Skip to content

Module imports should disambiguate source modules #281

@tnelson

Description

@tnelson

Currently, opening another module will import sigs, predicates, etc. into the target module. Multiple modules can be imported into a single target. It is reasonable to imagine that both modules bind the same identifier. For example, suppose we are modeling Prim's algorithm: we'd probably have a Node sig. But then if we're modeling Kruskal's algorithm, we'd also have a Node sig. If we then want to reason about these algorithms in (some sort of) composition, we'd import both into a third module.

It is inconvenient to need to manually rename identifiers (e.g., KNode vs. PNode for the two above). Alloy handles this by automatically prepending the imported module name to the identifier imported. We should consider doing the same, or at least doing so when a conflict occurs.

If we do this, we should add an as annotation to open, similar to Alloy's, so a module can control the naming.

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions