Lurch Deductive Engine

Namespace

Database

The testing database is built from a hierarchy of folders in the source code repository, containing .putdown and .smackdown files. The functions in this namespace are for querying that database. They are used in some of our testing suite, so that a library of large expressions, even large proofs, can be created outside of code, and just loaded from disk.

The documentation of each function below assumes you have imported the database using the code import Database from '/path/to/database.js'. For example, importing it from a script in the /tests folder would use import Database from '../src/database.js'. Thus when the identifier Database appears in the documentation below, it is referring to the database module itself, as documented in this namespace.

The source code file database.js is not intended to be imported into application code with the LDE itself, because it contains a large block of JSON in the code itself that is the entire contents of the database; that would significantly bloat the size of any app that used the LDE. However, that file is available for use in all of our testing scripts, and it is very useful in that regard.

Members

staticconstant

filterByMetadata

Get the list of all keys in the database that refer to entries whose metadata satisfies a given predicate. For details on metadata content, see getMetadata().

Source

staticconstant

getCode

Look up the original code associated with a database entry, which will be in either putdown or smackdown notation. The result will a string containing whatever was in the original .putdown or .smackdown file on disk when the database was created, or undefined if the key is invalid.

If the entry's metadata has an "includes" member, the database build process respects this and includes other .putdown or .smackdown files as headers within this one. The result of this function will include the full .putdown or .smackdown code for this entry, which includes any code that was imported using the "includes" member of the metadata. To get just the original code without the other included files, see getCodeWithoutIncludes().

The return value includes only putdown or smackdown code, not the YAML header that was converted into metadata. To get access to that information, see * getMetadata().

The return value is just the code, not the actual objects signified by that code. To get access to those objects, see getObjects().

Source

staticconstant

getCodeWithoutIncludes

This function works exactly the same as getCode(), except that any code included from a separate file using the "includes" member of the metadata object will not be included here. Thus the return value from this function is always a terminal substring of the return value of getCode().

Source

staticconstant

getMetadata

Look up the metadata associated with a database entry. The result will be a JavaScript Object instance, as if produced by JSON.parse(), possibly the empty object {} if the entry had no metadata, or undefined if the given key is invalid.

The metadata of any entry in the database is a JSON object extracted from the (optional) YAML header in the original .putdown or .smackdown file. It can contain any information the original author put there. For example, it might state that the contents of the file are (or are not) valid .putdown (or .smackdown) syntax, so that the file can be used for testing the putdown (or smackdown) parser. Or it might be used to include other .putdown or .smackdown files as headers. The list of uses for this metadata is intended to grow over time, and thus not be fully specified in advance.

The object returned is the actual metadata stored in the database, not a copy, so altering it will alter the contents of the database in memory (but not on the filesystem).

Source

staticconstant

getObject

This function works exactly the same as getObjects(), with one exception: If the putdown or smackdown source code parses into an array of length one, this function just returns the sole entry of that array, but if instead the array has any other length, this function throws an error, whose message states that it expected an array of length one.

Source

staticconstant

getObjects

This function works exactly the same as getCode(), with two exceptions.

  1. In addition to fetching the putdown or smackdown code, it also interprets it if possible, yielding an array of MathConcepts or LogicConcepts as the result. (Putdown notation produces LogicConcepts and smackdown notation produces MathConcepts, although since every LogicConcept is a MathConcept, smackdown notation may produce either type, but putdown notation always produces LogicConcepts.)
  2. Such results are cached so that future calls to this function with the same arguments will return the exact same MathConcept or LogicConcepts instances. In particular, this means that if you manipulate the copies you get, you are mainpulating the copies in the cache. If this is not what you want, make separate copies.

If the putdown or smackdown code fetched for the entry is not valid, then this function will instead throw a parsing error. If the key is an invalid key for the database, this function will return undefined. If the file contains the putdown or smackdown code for zero actual objects (e.g., only whitespace and comments) then this function will return an empty array.

If you know that there is only one object in the file, and you want to get it without bothering to do getObjects(key)[0], you can just call getObject() instead.

Source

staticconstant

keys

Each entry in the database has a unique name by which it is identified, and we call those names "keys." You can get a list of all keys using this function.

The keys are simply the paths in the filesystem from which the data was loaded. So you might get a response of the form ['/folder1/file1.putdown','/folder2/subfolder/file2.smackdown'] and so on, containing as many files as there are in the database. If you think of the database as a filesystem, this function is like a recursive directory listing, filtering for only the .putdown and .smackdown files.

Source

staticconstant

keysPaths

Since the keys in the database are file paths, we might want to ask for the list of files inside a certain folder. We can do so recursively with keysStartingWith(), but this function lets us do so non-recursively.

For example, if we call Database.keysPaths('/example'), we might get a response like ['one','two','x.putdown'] if indeed there were three things in the /example folder, including subfolders one and two and a file x.putdown. If the database is viewed as a filesystem, this function is like a directory listing.

Source

staticconstant

keysStartingWith

This is a convenience function that returns just those keys in the database that begin with a certain prefix. You can use this to get all files recursively beneath a certain folder, for example, with a call like Database.keysStartingWith('/my/folder/name/').

Source