GitLab

Added Local within a section and Global outside. This was done automatically with the following Python script, which tracks whether a section is open. The script handles nested sections but makes no attempt to fully handle Coq sentences or comments, so multiple section commands on one line or section commands in comments will confuse it. I also manually fixed some Instances in example code in documentation.

EDIT: See stdpp!207 (merged) for a newer version of this script.

#!/usr/bin/env python3

# Add Local or Global to any unqualified Instance declarations. Tracks whether
# a section is open and adds Global outside any section and Local inside one.

import sys
import re

SECTION_RE = re.compile("""\s*Section\s+(?P<name>\w*).*\..*""")
END_RE = re.compile("""\s*End\s+(?P<name>\w*).*\..*""")
INSTANCE_RE = re.compile("""(?P<indent>\s*)(?P<instance>Instance.*)""")

def qualify_lines(lines):
    """Qualify instances in text given as a list of lines."""
    # tracks the list of sections open
    section_stack = []
    out = []
    for line in lines:
        m = SECTION_RE.match(line)
        if m:
            name = m.group("name")
            section_stack.append(name)
        m = END_RE.match(line)
        if m:
            name = m.group("name")
            # close a section if it's open (name may not match because End is
            # for a module instead)
            if len(section_stack) > 0 and section_stack[-1] == name:
                section_stack.pop()
        m = INSTANCE_RE.match(line)
        if m:
            indent = m.group("indent")
            modifier = "Local" if section_stack else "Global"
            instance = m.group("instance")
            line = f"{indent}{modifier} {instance}\n"
        out.append(line)
    if section_stack:
        print(f"oops {section_stack} remaining", file=sys.stderr)
        sys.exit(1)
    return out

for fname in sys.argv[1:]:
    with open(fname) as f:
        lines = f.readlines()
    with open(fname, "w") as f:
        lines = qualify_lines(lines)
        f.writelines(lines)