Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 20
    • Merge requests 20
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !609

Qualify all instances with Local or Global

  • Review changes

  • Download
  • Patches
  • Plain diff
Closed Tej Chajed requested to merge tchajed/iris-coq:qualify-instances into master Dec 19, 2020
  • Overview 6
  • Commits 1
  • Pipelines 0
  • Changes 87

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)
Edited Jan 07, 2021 by Ralf Jung
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: qualify-instances