Modules#

Deductions are recorded in files with .pfsc extension, called Proofscape modules. For example, the deductions we considered in Deductions might be recorded in two modules, like this:

Listing 4 A first module#
 1deduc Thm {
 2
 3    asrt C {
 4        en = "Some amazing theorem statement."
 5    }
 6
 7    meson = "
 8    C.
 9    "
10}
11
12deduc Pf of Thm.C {
13
14    asrt R {
15        en = "Something self-evident"
16    }
17
18    asrt S {
19        en = "An easy consequence"
20    }
21
22    meson = "
23    R, so S, therefore Thm.C.
24    "
25}
Listing 5 A second module#
 1from lh.some.library.mod1 import Pf
 2
 3# The inference to node S in Pf is not so obvious.
 4# Here is a clarification.
 5deduc X1 of Pf.S {
 6
 7    asrt A1 {
 8        en = "A thing that helps to clarify"
 9    }
10
11    asrt A2 {
12        en = "Another thing"
13    }
14
15    meson = "
16    Pf.S by A1 and A2 and Pf.R.
17    "
18}

Import statements, such as the one visible at the top of Listing 5, allow us to refer to deductions defined in other modules. Their syntax is defined below; but first we have to talk about libpaths.

Libpaths#

A library path, or libpath, is a unique identifier for anything defined in a Proofscape module, such as a deduction or a node. It consists of segments, separated by dots.

The first three segments of a libpath are called the host, owner, and repo segments. The host segment can only take on one of a small set of possible values:

  • gh: GitHub

  • bb: BitBucket

  • lh: localhost

  • test: used in testing

Libpaths starting with gh or bb are like URLs, in that they are universally unique identifiers for Proofscape entities. They refer to objects defined in Proofscape repos hosted at GitHub or BitBucket, under owners and repos given, of course, by the owner and repo segments.

Libpaths starting with lh are not universal, but instead simply point into the directory structure of a local Proofscape installation. This offers a lot of freedom, but also must be used carefully, because modules importing from lh libpaths are not portable.

Finally, the test host segment is simply used for unit testing the Proofscape software.

In Listing 5, we used the libpath lh.some.library.mod1, and we are imagining that Listing 4 has been saved in the file PFSC_ROOT/lib/lh/some/library/mod1.pfsc, where our local Proofscape installation is in the directory PFSC_ROOT on our computer.

Imports#

Import statements in Proofscape modules have similar syntax and semantics to import statements in the Python programming language. There are two basic forms:

from LIBPATH import OBJECT [as NAME]
import LIBPATH [as NAME]

Once an object has been imported, it can be referenced in deduction preambles and meson scripts. Objects lying under it can be referenced by dotted paths. Thus, for example, Pf was imported in Listing 5, and we were then able to refer to its node S as Pf.S.

The LIBPATH in an import statement can be absolute, meaning it begins with a host segment, or can be relative, meaning it begins with one or more dots.

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.

Comments#

In Proofscape modules, comments begin with a #. An example can be seen in Listing 5.