Lurch validation engine

Namespace

Extensions

This namespace contains extensions of the LogicConcept class and several of its subclasses that are needed or useful for n-compact validation.

Methods

static

Declaration#allProps()

Declarations can only have one prop form, but we need it to be consistent with the previous routine.

Source

static

Declaration#letsInScope()

Compute the array of all of the Let's in the scope of this Let.

Source

static

Declaration#lookup(catalog, ignoresopt)

Look up this declarations's numerical prop form in the catalog

Parameters

  • catalog Array.<string>

    the catalog

  • ignores Array.<LogicConcept> <optional>
     []

    an array of LCs to ignore

Source

static

Declaration#prop(ignoreopt)

Compute the Prop Form string for a Let or ForSome Declaration. We will format both as [s₁ ... sₙ] where $s_i$ is the properName of the $i^\text{th}$ symbol it declares, whether or not it has a body, since interpretation will put a copy of the body after the declaration, which then will get its own propositional form. Declare's don't have a prop form.

Note that the Prop form does not include the leading : for givens.

Compute the Preemie Prop Form string for a Let or ForSome Declaration. This is the same as the ordinary prop form, but is ignored if it is contained on the ignore argument list (of Lets to ignore).

Parameters

  • ignore Array.<LogicConcept> <optional>
     []

    an array of declarations to ignore when computing this propositional form.

Source

static

Environment#cnf(targetopt, checkPreemiesopt)

The cnf of this Environment in satSolve format.

Parameters

  • target LogicConcept <optional>
     this

    the target

  • checkPreemies boolean <optional>
     false

    if true, check for preemies

Source

static

Environment#letInferences()

Compute the array of all Let's in this environment whose parent is an inference in this environment

Source

static

Environment#scopes()

Compute the array of arrays containing the user's various let scopes, labled by their
letAncestors.

Source

static

Expression#allProps()

Compute all of the propositional forms of this expression (both standard and preemie) and return them as a Set. This is not defined for environments.

Source

static

Expression#lookup(catalog, ignoresopt)

Look up this expression's numerical prop form in the catalog.

Parameters

  • catalog Array.<string>

    the catalog

  • ignores Array.<LogicConcept> <optional>
     []

    an array of LCs to ignore

Source

static

Expression#prop(ignoreopt)

Compute the Prop Form string for an expression. This is the .putdown form except that we must use the ProperName for symbols instead of their text. For bound symbols, this is their canonical name so alpha equivalent expressions have the same propositional form. For symbols declared with a body this is the renaming that accounts for the body. Note that the Prop form does not include the leading : for givens.

We cache the results in a .propform js attribute and return them if present.

In order to check for preemies we need a different propositional form in some cases. The optional argument ignore is an array of Let's such that if a symbol in the expression is defined by one of the Let's on the list, we use its text name instead of its ProperName (i.e., no tick marks). These are not cached in the .propform attribute (when ignore is nonempty).

Parameters

  • ignore Array.<LogicConcept> <optional>
     []

    an array of Let's to ignore when computing this propositional form.

Source

static

LogicConcept#attributes() → {Array}

Return an array showing all of the js attributes and LC attributes of this LC, except for those whose key begins with an underscore '_'.

Returns

  • Array
    • the array of key-value pairs

Source

static

LogicConcept#declarations(onlywithbodies) → {Array.<LogicConcept>}

Compute the array of all declarations in this LC If the optional argument onlywithbodies is true, only return declarations with bodies.

Parameters

  • onlywithbodies boolean

    if true, only return declarations with bodies

Returns

  • Array.<LogicConcept>

Source

generatorstatic

LogicConcept#descendantsSatisfyingIterator(includeopt, excludeopt)

A more efficient descendants iterator for finding all descendents satisfying an 'include' predicate when it is known that no descendant of a descendant that satisfies the predicte can also satisfy the predicate. If a second 'exclude' predicate is supplied, that signals that none of its descendants can satisfy the 'include' predicate, so whenever it is true the search can skip that entire branch and move on to its next sibling. The default behavior of this function is to include everything and exclude nothing.

This is useful for finding, say, all statements or declarations or all formulas in an LC. The default is to include everything and exclude nothing.

Parameters

  • include function <optional>
     ()=>true

    the include predicate

  • exclude function <optional>
     ()=>false

    the exclude predicate

Source

static

LogicConcept#environments()

Compute the array of all environments in this LC.

Source

static

LogicConcept#equations(conclusionsOnly)

Compute the array of all equations in this LC. If the first argument is true, only return those that are inferences.

Parameters

  • conclusionsOnly boolean

    if true, only return inferences

Source

static

LogicConcept#find(includeopt, excludeopt)

Find the first occurrence of a descendant of this LC that satisfies the boolean function given by the argument, and return it. Skip over any branch that is excluded by the second argument.

Parameters

  • include function <optional>
     ()=>true

    include - the include predicate

  • exclude function <optional>
     ()=>false

    exclude - the exclude predicate

Source

static

LogicConcept#forSomes()

Compute the array of all ForSomes's in this LC. If the argument is true, only return those with bodies.

Source

static

LogicConcept#formulas(includefinishedopt)

Compute the array of all formulas that are not marked as .finished in this LC the optional argument, if true, tells it to return all formulas, whether they are finished or not.

Parameters

  • includefinished boolean <optional>
     false

    if true, return all formulas

Source

static

LogicConcept#insertAfter(target)

Insert this LC as the next sibling of LC target. You might have to make a copy of 'this' if it is already in the same tree as the target. We don't check that here.

Parameters

  • target LogicConcept

Source

static

LogicConcept#insertBefore(target)

Insert this LC as the previous sibling of LC target. You might have to make a copy of 'this' if it is already in the same tree as the target. We don't check that here.

Parameters

  • target LogicConcept

Source

static

LogicConcept#isAComment()

We say an LC expression is a Comment if it has the form (➤ "Comment string here."). These are ignored when computing prop form, and are converted to actual comments when printing the LC to the Lode terminal.

Source

static

LogicConcept#isADeclaration()

Matching syntactic sugar to isAnEquation for Declarations.

Source

static

LogicConcept#isALet() → {boolean}

A Let is defined to be a given declaration that is not marked as a 'Declare' whether or not it has a body

Returns

  • boolean

Source

static

LogicConcept#isALetEnvironment() → {boolean}

A Let-environment is an environment whose first child is a Let. Check if an LC is a Let-environment.

Returns

  • boolean

Source

static

LogicConcept#isAProposition(ignores) → {boolean}

We say an LC is a Propositon iff it has a .prop form and is not an environment. This includes all Statements but also Let's, and ForSome's. It does not include the bodies inside ForSome declarations since each of those declarations will have atomic propositional forms and a separate copy of the body. It ignores anything flagged with .ignore for defining shortucts and other content that is supposed to be ignored, and ignores anything passed in the argument ignores.

Parameters

  • ignores Array.<LogicConcept>

Returns

  • boolean

Source

static

LogicConcept#isAStatement() → {boolean}

A Statement is any outermost Expression that is not a declaration or a declared symbol inside a declaration. The body of a declaration can contain statements.

Returns

  • boolean

Source

static

LogicConcept#isAnEquation() → {boolean}

An Equation is an outermost Application whose operation is the Symbol whose .text() is '=' and has at least two arguments.

Returns

  • boolean

Source

static

LogicConcept#letAncestors() → {Array.<LogicConcept>}

Get the array of all of the Let ancestors of this LC Note: since everything is its own ancestor by default, the Let that is the first child of a Let environment is considered to be a letAncestor of the Let environment.

Returns

  • Array.<LogicConcept>

Source

static

LogicConcept#lets(onlywithbodies)

Compute the array of all Let's in this LC. If the argument is true, only return those with bodies.

Parameters

  • onlywithbodies boolean

    if true, only return declarations with bodies

Source

static

LogicConcept#mentions()

Compute the array of all instantiations in the document that contain a proposition that has the same propositional form as a given proposition e

Source

static

LogicConcept#propositions()

Compute the array of all propositions in this LC.

Source

static

LogicConcept#results(toolnameopt) → {object}

Replacement for Validation.result() that supports more than one result (up to one for each plugin-tool of global validation). For example, a BIH can be validated separately by the BIH tool and the global propositional tool.

Get the results for this toolname.

Parameters

  • toolname string <optional>

    the name of the tool

Returns

  • object
    • the results

Source

static

LogicConcept#root()

Compute the topmost ancestor of this LC. This corresponds to the Document containing the LC.

Source

static

LogicConcept#setResult(toolnameopt, resultopt, reasonopt)

Replacement for Validation.setResult() that supports more than one result (up to one for each plugin-tool of global validation). For example, a BIH can be validated separately by the BIH tool and the global propositional tool.

Set the result for this toolname.

Parameters

  • toolname string <optional>

    the name of the tool

  • result string <optional>

    the result

  • reason string <optional>

    the reason

Source

static

LogicConcept#slice(startopt, endopt)

Give LCs a .slice() command analogous to what js has for arrays. This returns a copy of the LC, not a 'shallow copy' since separate LCs can't share the same children. It also preserves the LC attributes of the original LC by making a complete copy of it first (rather than e.g. reconstructing it from copies of the children that are being kept)

Parameters

  • start number <optional>
     0

    the start index of the slice

  • end number <optional>
     this.numChildren()

    the end index of the slice

Source

static

LogicConcept#some(predicate)

Efficiently check if an LC has a descendant satisfying some predicate it aborts the search as soon as it finds one. This is analogous to the same method for js arrays.

Parameters

  • predicate function

    the predicate

Source

static

LogicConcept#toAlgebraic(modeopt, targetopt, checkPreemiesopt)

See the Propositional Form for details. Convert an LC to its algebraic propositional form. Modes are the strings 'raw', 'simplify', or 'cnf'. The 'raw' mode just converts t he LC to algebraic form. The 'simplify' mode distributes negations by DeMorgan. The 'cnf' mode expands all the way to cnf.

Parameters

  • mode 'raw' | 'simplify' | 'cnf' <optional>
     'raw'

    the mode

  • target LogicConcept <optional>
     this

    the target

  • checkPreemies boolean <optional>
     false

    if true, check for preemies

Source

static

LogicConcept#toEnglish(targetopt, checkPreemiesopt)

See the Propositional Form for details. Convert an LC to its English propositional form.

Parameters

  • target LogicConcept <optional>
     this

    the target

  • checkPreemies boolean <optional>
     false

    if true, check for preemies

Source

static

LogicConcept#toNice(targetopt, checkPreemiesopt)

Produces a string representation of this LC's propositional form in a nice format that is useful for viewing it in Lode or a console.

Parameters

  • target LogicConcept <optional>
     this

    the target

  • checkPreemies boolean <optional>
     false

    if true, check for preemies

Source

static

LurchSymbol#properName()

Return the Proper Name for a Lurch symbol if it has one, otherwise just return the name of the symbol.

Source

static

LurchSymbol#rename(newname)

Rename this Lurch symbol (in place).

Parameters

  • newname string

Source