pfsc files#

Files with .pfsc extension, which are called “Proofscape files,” are one type of file in which you can define Proofscape modules (the other being rst files).

These files are written in the Proofscape language, whose formal grammar can be found below.

Essentially, there are only a couple of things you can do in a pfsc file: define things, and import things defined in other files. The “things” you are defining are any of the various Data Types, except for Sphinx pages (which can only be defined in rst files). Thus, Proofscape files consist of:

  • imports

  • assignments

  • deductions

  • annotations

  • running definitions

Imports#

Import statements in Proofscape modules allow you to access objects defined in other modules (potentially belonging to other repos). They have similar syntax and semantics to import statements in the Python programming language.

When you want to import a single object from another module, there are two basic forms:

Listing 41 from-import format#
from LIBPATH import OBJECT_NAME [as NAME]
Listing 42 plain import format#
import LIBPATH [as NAME]

We can refer to the first form as a from-import, and the second as a plain import.

  • The LIBPATH in an import statement is absolute unless it is preceded by one or more dots, in which case it is relative.

    In a relative libpath, the first dot means “this module,” two dots means the module above this one, three the module above that, and so on. For example, in a module lh.foo.bar.a.b.c.d, the relative libpath ...Thm would mean an object named Thm in lh.foo.bar.a.b.

  • An OBJECT_NAME is simply the name under which the desired object is defined in its own module.

  • The NAME in the optional as NAME clause gives a local name under which the object can be referenced after being imported. It is a string of alphanumerics and underscores that cannot begin with a digit.

Once an object has been imported, it can be referenced locally by a relative libpath \(R\), according to the following rules:

Import type

Using as NAME clause

\(R\) equals…

from-import

Yes

NAME

from-import

No

OBJECT_NAME

plain import

Yes

NAME

plain import

No

LIBPATH

Objects lying under an object imported under relative libpath \(R\) can be referenced by extending \(R\) in the natural way. To give an example, consider the theorem and proof discussed later in this reference manual, when we introduce deductions. These could be defined in two separate modules. As long as Thm was imported into the module where Pf was defined, then the relative libpath Thm.C appearing in the definition of Pf would be a valid way to refer to node C inside of Thm.

Multiple imports#

If you want to import multiple objects from a single module, you can always use multiple import statements. Alternatively, the from-import statement has two additional forms:

from LIBPATH import OBJECT_NAMES [as NAME]

from LIBPATH import *

In the first form, OBJECT_NAMES is a list of object names, separated by commas. If as NAME is used, it will set the local name of the last object in the list, while all other objects keep their original name.

In the second form, every object is imported, under its original name.

Assignments#

In the Proofscape language, an assignment is an expression of the form

NAME = VALUE

where

  • NAME is a string of alphanumerics and underscores which cannot begin with a digit.

  • VALUE is any Proofscape-flavored JSON.

Assignments can occur at various “levels” or “depths”: they can occur inside of node or deduction definitions, and they can also occur up at the top level of the file. Assignments occurring at the top level of a file generally have some special role to play, such as, for example, Doc Info Objects, and Dependency declarations.

Deductions#

Deductions represent theorems, proofs, and expansions on proofs. They are covered in their own section of the reference manual: Deductions.

Annotations#

Annotations define pages of notes, with interactive widgets that do things like navigate proof charts, and provide example explorers via an embedded computer algebra system. They are covered in their own page of the reference manual: Annotations.

Running Definitions#

Running definitions can be used to represent mathematical definitions that are needed in deductions, but that may persist for a whole section, a whole chapter, or even for an entire work, and for which you would therefore not like to repeat the definition over and over, in Intro nodes. Running definitions are covered in their own page of the reference manual: Running Definitions.

Comments#

In pfsc files, comments begin with a # character.

Proofscape grammar#

For completeness, we provide the formal grammar for pfsc files. You don’t really need to study this. It is provided as a reference, but you should learn the language by reading the Tutorials and the more illustrative sections of this reference manual, as well as by simply studying existing Proofscape repos.

The formal grammar for Proofscape files is given in Listing 43. It relies on an auxiliary grammar for Proofscape-flavored JSON, which is shown in Listing 44. These listings define the non-terminal symbols of the language in the syntax of lark-parser, while the set of terminal symbols is given in Listing 45, using raw string Python regex notation.

Before a .pfsc file is parsed, comments are stripped out, and then the file is passed through a chunker, which identifies all annotations (anno blocks), and replaces each one with a stub. The resulting file is then parsed using the grammar below (while annotations are processed separately, by passing them through a custom Markdown renderer that also processes Proofscape widgets).

Listing 43 Formal grammar for Proofscape files#
module : (import|deduc|anno|defn|tla)*

?import : plainimport
        | fromimport
plainimport : "import" (relpath|libpath) ("as" identifier)?
fromimport : "from" (relpath|libpath) "import" (STAR|identlist ("as" identifier)?)

relpath : RELPREFIX libpath?
libpath : identifier ("." identifier)*
identlist : identifier ("," identifier)*

deduc : deducpreamble "{" deduccontents "}"
deducpreamble : "deduc" identifier (OF targets)? (WITH targets)?
targets : libpath ("," libpath)*

deduccontents : (subdeduc|node|clone|assignment)*

subdeduc : "subdeduc" identifier "{" deduccontents "}"

?node : basicnode
      | suppnode
      | wolognode
      | flsenode

basicnode : NODETYPE identifier "{" nodecontents "}"

suppnode : "supp" identifier ("versus" targets)? "{" nodecontents "}"

wolognode : WOLOGTYPE identifier "wolog" "{" nodecontents "}"

flsenode : "flse" identifier ("contra" targets)? "{" nodecontents "}"

nodecontents : (node|assignment)*

clone : "clone" libpath ("as" identifier)?

anno: "anno" identifier ("on" targets)?

defn: "defn" identifier ve_string ve_string

tla : assignment

assignment : identifier "=" json_value

identifier : CNAME
Listing 44 Formal grammar for Proofscape-flavored JSON#
?json_value: json_object
      | json_array
      | ve_string
      | SIGNED_INT         -> json_integer
      | SIGNED_FLOAT       -> json_number
      | ("true"|"True")    -> json_true
      | ("false"|"False")  -> json_false
      | ("null"|"None")    -> json_null
      | json_libpath
json_array  : "[" [json_value ("," json_value)*] ","? "]"
json_object : "{" [json_pair ("," json_pair)*] ","? "}"
json_pair   : (json_cname|ve_string) ":" json_value
ve_string : TRIPLE_QUOTE_STRING.2|TRIPLE_APOS_STRING.2|QUOTE_STRING|APOS_STRING
json_cname: CNAME
json_libpath: CNAME ("." CNAME)*

%ignore WS
Listing 45 Terminal symbols for Proofscape formal grammar, expressed as Python raw strings#
STAR = r'\*'
OF = r'of'
WITH = r'with'
RELPREFIX = r'\.+'
NODETYPE = r'(asrt|cite|exis|intr|mthd|rels|univ|with)'
WOLOGTYPE = r'(mthd|supp)'
TRIPLE_APOS_STRING = r"'''('?'?[^'])*'''"
TRIPLE_QUOTE_STRING = r'"""("?"?[^"])*"""'
APOS_STRING = r"'(\\'|[^'])*'"
QUOTE_STRING = r'"(\\"|[^"])*"'
CNAME = r'[a-zA-Z_]\w*'
SIGNED_INT = r'[+-]?\d+'
SIGNED_FLOAT = r'[+-]?\d+\.\d+'
WS = r'\s+'