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

deduc Thm {

    asrt C {
        en = "Some amazing theorem statement."
    }

    meson = "
    C.
    "
}

deduc Pf of Thm.C {

    asrt R {
        en = "Something self-evident"
    }

    asrt S {
        en = "An easy consequence"
    }

    meson = "
    R, so S, therefore Thm.C.
    "
}

Listing 5 A second module

from lh.some.library.mod1 import Pf

# The inference to node S in Pf is not so obvious.
# Here is a clarification.
deduc X1 of Pf.S {

    asrt A1 {
        en = "A thing that helps to clarify"
    }

    asrt A2 {
        en = "Another thing"
    }

    meson = "
    Pf.S by A1 and A2 and Pf.R.
    "
}

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 of the libpath.

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 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.