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 Instance
s 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)