[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] Semi-literate specification with PVS



Hello all,

It has been pretty quiet on the list, so I thought I'd share a
little bit of Python that I am using for semi-literate specification
with PVS. It takes a LaTeX file produced by PVS, and chops
it up at lines that match fragmentBoundaryRe. The resulting
fragments are stored in a directory whose name is the name
of the LaTeX file sans the ".tex" extension. One can then use
the fragments to build a fancy LaTeX document out of the
specification.

I use a string starting with two at signs as a boundary. Suppose
I have the following PVS file:

foo : THEORY
BEGIN
   latexfragment1 : string = "@@x-fragment"
   x : integer
   latexfragment2 : string = "@@y-fragment"
   y : boolean
   latexfragment3 : string = "@@epilogue"
END foo

After doing "M-x latex-theory" in PVS, and saying "choppvs foo.tex"
in shell,  I can use the fragments in a LaTeX file as

\chapter{Foo}

This chapter describes foo. The outline of the theory is

\input foo/prologue.tex
{\em For actual contents see below}
\input foo/epilogue.tex

\section{X}

Here we describe x.

\input foo/x-fragment

--------------------------------------------------------------------
#!/usr/bin/python

import sys
import re
import os
import string

if len(sys.argv) != 2:
     print "Usage: choppvslatex latex-file"
     exit(1)


beginAllttRe = re.compile(r"^\\begin\{alltt\}")
endAllttRe = re.compile(r"^(.*)\\end\{alltt\}$")
fragmentBoundaryRe = re.compile(r'"@@([^"]*)"')
initialAllttFound = False

fragments = {}
thisFragment = []
thisFragmentName = "prologue"

# Chop the file
inf = open("%s" % sys.argv[1], "r")
for line in inf:
     if not initialAllttFound:
         if beginAllttRe.match(line) != None:
             initialAllttFound = True
     else:
         b = fragmentBoundaryRe.search(line)
         if b:
             fragments[thisFragmentName] = thisFragment
             thisFragmentName = b.group(1)
             thisFragment = []
         else:
             l = endAllttRe.match(line)
             if l:
                 thisFragment.append(l.group(1))
             else:
                 thisFragment.append(line)

fragments[thisFragmentName] = thisFragment
inf.close()

# Trim the  fragments

whiteSpaceRe = re.compile('^\s+$')

for key in fragments.keys():
     lines = fragments[key]
     while lines:
         if whiteSpaceRe.search(lines[0]):
             lines[0:1] = []
         else:
             break
     lines.reverse()
     while lines:
         if whiteSpaceRe.search(lines[0]):
             lines[0:1] = []
         else:
             break
     lines.reverse()

baseName = re.match('^(.*)\.tex', sys.argv[1]).group(1)
for key in fragments.keys():
     if not os.access(baseName, os.F_OK):
         os.mkdir(baseName)
     f = open("%s/%s.tex" % (baseName, key), "w")
     f.write('\\begin{alltt}\n')
     for l in fragments[key]:
         f.write(l)
     f.write('\\end{alltt}\n')
     f.close()