Lurch web app user interface

Class

DeclarationType

Declarations of new symbols can be phrased in a wide variety of ways. This class helps detect and work with the essential properties that any of those phrasings will exhibit. Those essential properties are:

  1. Does it declare a variable or a constant?
    • A "variable" declaration is typically used for introducing a new, arbitrary symbol at the start of a proof or subproof, and functions like a hypothesis
    • A "constant" declaration names a concept that is usually known to exist before the declaration, and may be justified by an existential
  2. Does it have a body, and if so, where does it belong?
    • Not every declaration has a body (that is, a corresponding expression). For example, we can write "Let x be arbitrary" and that declares a new variable with no assumptions about it (no expression attached).
    • A declaration like "Let epsilon be arbitrary with epsilon>0" is like the previous case, but now with an attached assumption (its "body" following after the declaration).
    • A declaration like "m=2k for some k" is a declaration of k, with its body preceding the declaration, and may need to be justified by a fact like "m is even".
    • Thus bodies may or may not exist, and if they do exist, they are in one of two places: before or after the declaration.

This class embodies a type of declaration, which includes three pieces of data: the type (variable or constant), the body (none, before, or after), and the template (which is how the declaration is phrased in English, with placeholders, such as "Let [variable] be arbitrary"). This data is redundant in the following ways.

  • If you have the type and body, we can construct a simple template. Common English phrases for every type-body pair are included in this class, and can be filled in where needed.
  • If you have the template, the type and body can be computed from the values and position of its placeholders.

Constructor

new DeclarationType(type, body, templatenullable)

Create a declaration type from a given type and body. The template is optional; if not provided, a simple, English template will be generated that fits the given type and body. If the template is provided, it should contain precisely one copy of the string "[variable]" or the string "[constant]" (depending on the type you're creating) and optionally precisely one copy of "[statement]", which must appear at either the start or end of the template, if it appears at all.

These properties of the third parameter are not validated; the caller must ensure that they hold. Furthermore, the constructor does not verify that the type and body implied by the template match those provided in the first two parameters; the caller must ensure this as well.

Parameters

  • type string

    one of "variable" or "constant" as documented above

  • body string

    one of "none", "before", or "after" as documented above

  • template string <nullable>

    the template in English, with placeholders, as documented above

See

Source

Classes

DeclarationType

Methods

displayForm(symbol) → {string}

A template like "Let [variable] be arbitrary" can be converted into more readable text like "Let x be arbitrary" if we know the name of the symbol being declared (in that case, x). This function performs that replacement, and replaces the [statement] placeholder with an ellipsis, so that, for example, "For some [constant], [statement]" may become "For some c, ...".

Parameters

  • symbol string

    the symbol being declared

See

Returns

  • string

    the template with all placeholders replaced with readable text

Source

documentForm(symbol, bodyHTMLopt) → {string}

Just as displayForm() converts the template into readable text, this function does the same but produces HTML instead, for use in the editor. There are two important differences between this and displayForm().

  1. The symbol being declared will be represented either using LaTeX-style typesetting or fixed-width font, depending on the type of declaration.
  2. The placeholder "[statement]" will be replaced with the provided HTML, which defaults to the empty string, thus removing the body.

Parameters

  • symbol string

    the symbol being declared

  • bodyHTML string <optional>

    the HTML representation of the body of the declaration, if it has a body (optional)

See

Returns

  • string

    the template in HTML, with the symbol placeholder filled in and the body placeholder removed

Source

latexForm(symbol, bodyLatexopt) → {string}

This function is analogous to documentForm(), but produces LaTeX notation instead.

Parameters

  • symbol string

    the symbol being declared

  • bodyLatex string <optional>

    the LaTeX representation of the body of the declaration, if it has a body (optional)

See

Returns

  • string

    the template in LaTeX, with the symbol placeholder filled in and the body placeholder removed

Source

lurchNotationForm(symbol, bodynullable) → {string}

Just as displayForm() converts the template into readable text, this function does the same but produces Lurch notation instead, which could be parsed into a meaningful LogicConcept (which would be a Declaration instance).

Although Lurch notation supports declaring multiple symbols in one declaration, this function only supports one symbol; it could be extended later to support multiple symbols.

Parameters

  • symbol string

    the symbol being declared

  • body string <nullable>

    the body of the declaration, if this declaration type requires one, or omit it if not; this must be in Lurch notation already because it will be used as-is

See

Returns

  • string

    the declaration in Lurch notation, using the given symbol and optional body

Source

match(text) → nullable{string}

When the user enters a dollar sign ($) in the editor, the application will watch for math-like content thereafter. If it sees that the user seems to be typing a declaration, it will offer to autocomplete it. In order for the application to notice that the user seems to be typing a declaration, instances of this class need to evaluate the text the user has typed so far and decide whether it fits (the first part of) the pattern in our template. This function does that work.

Parameters

  • text string

    some text the user has typed into the editor, to be evaluated for whether it triggers autocompletion using this declaration type

Returns

  • string

    either the symbol being declared if a match is found, or undefined if no match is found

Source

toLC(symbol, bodyLCnullable) → {Declaration}

Given a symbol to declare and an optional body of the declaration, create a LogicConcept instance representing a declaration of this type with those data. If you provide a body when one is not required by the type, or you fail to provide a body when one is required, an error is thrown. If the provided body is not a LogicConcept of type Expression, an error is thrown.

Parameters

  • symbol string

    the symbol being declared

  • bodyLC LogicConcept <nullable>

    the body of the declaration, if this declaration type requires one, or omit it if not; if it is provided, it is used as-is, not copied, so pass a copy if you need your original

Returns

  • Declaration

    the declaration as a LogicConcept instance, of type Declaration, as documented in the LDE repository

Source

static

allInSettings(addDefaultsopt) → {Array.<DeclarationType>}

The application settings allows the user to choose a set of phrases that can be used as templates for declaration types. This function fetches those phrases and creates a declaration type instance for each. Also, if the parameter is set to true, it adds in default types for any type-body pair not represented by a phrase in the settings.

Parameters

  • addDefaults boolean <optional>
     false

    whether to add in default types for any type-body pair not included in the settings

Returns

  • Array.<DeclarationType>

    an array of all DeclarationType instances mentioned in the user's settings, plus any default types needed, if the caller requested them with addDefaults

Source

static

defaultTemplate(type, body) → {string}

When we need to create a declaration type given just the type and body information, without a template phrase, we need a simple way to generate a suitable phrase. This function knows six simple English phrases, one suitable for each of the six type-body combinations.

Parameters

  • type string

    one of "variable" or "constant" as documented at the top of this class

  • body string

    one of "none", "before", or "after" as documented at the top of this class

Returns

  • string

    a simple English template for the given type and body

Source

static

existsTemplateFor(type, body, listnullable) → {boolean}

Given a list of declaration types, does one of them have the given type and body? This function determines that. It defaults to searching the list of declaration types in the user's current settings, but you can pass whatever list you want the function to search.

Parameters

  • type string

    one of "variable" or "constant" as documented at the top of this class

  • body string

    one of "none", "before", or "after" as documented at the top of this class

  • list Array.<DeclarationType> <nullable>

    the list of declaration types in which to search (which defaults to the list in the user's current settings)

Returns

  • boolean

    whether a declaration on the list has the given type and body

Source

static

fromTemplate(template) → {DeclarationType}

The constructor for this class expects you to provide a type and body, but if you already have a template phrase, you can use this function to construct a DeclarationType instance from that phrase alone, because the type and body can be computed from the phrase using templateToType() and templateToBody().

Parameters

  • template string

    a template phrase as documented in the constructor

Returns

  • DeclarationType

    a new DeclarationType instance that uses the given template, and has a type and body appropriate to it

Source

static

templateToBody(template) → {string}

Given a template phrase (as documented in the constructor), discern whether it describes a declaration that expects a body before it, after it, or does not expect a body.

Parameters

  • template string

    a template phrase as documented in the constructor

Returns

  • string

    one of "none", "before", or "after"

Source

static

templateToType(template) → {string}

Given a template phrase (as documented in the constructor), discern whether it describes the declaration of a variable or constant.

Parameters

  • template string

    a template phrase as documented in the constructor

Returns

  • string

    one of "variable" or "constant"

Source