Given a LogicConcept in which we wish to mark some symbols as implicitly declared, this function writes that data into the appropriate attribute, merging it with any data already there. It is assumed that the implicit symbol declaration data is an array of symbol names, and that the new symbol given here is to be appended to the end of that array, if and only if it wasn't already on the array.

This function is made static so that any client can easily make use of the same convention for storing implicit declarations in a LogicConcept, but the standard way to compute and store such errors is by passing an implicit symbol declaration handler to validate().

Given a LogicConcept in which we wish to save some data about its scoping errors, this function writes that data into the appropriate attribute, merging it with any data already there. It is assumed that the scoping error data is an object containing key-value pairs as is common in JSON data, and that the newData will be merged with any old data already in the target using Object.assign().

This function is made static so that any client can easily make use of the same convention for storing scoping errors in a LogicConcept, but the standard way to compute and store such errors is with validate().

This function clears any data stored by addScopeError(). It could just as easily be done with clearAttributes() and the appropriate key, but this API makes it easy to remain consistent if the underlying data storage method were to change.

After this function has been run on the target, the result of scopeErrors() for that same target is guaranteed to be undefined.

This function clears any data stored by addScopeError(). It could just as easily be done with clearAttributes() and the appropriate key, but this API makes it easy to remain consistent if the underlying data storage method were to change.

After this function has been run on the target, the result of scopeErrors() for that same target is guaranteed to be undefined.

A callback function that can be used with the validate() function, as in Scoping.validate(L,Scoping.declareGlobal). If used in that manner, for every free and undeclared symbol in L, this function will add an implicit declaration of it at the top-level ancestor (the "global" scope) for each free and undeclared symbol. Each symbol is added only once to that global scope, because implicit symbol declaration lists are actually sets, not lists.

A callback function that can be used with the validate() function, as in Scoping.validate(L,Scoping.declareInAncestor). If used in that manner, for every free and undeclared symbol in L, this function will add an implicit declaration of it at the smallest enclosing Environment in which the symbol was used free and undeclared. This behavior is complex enough that it bears illustrating with a few examples.

Example 1: If the symbol appears free and undeclared in only one expression, then that expression's parent environment is the one in which it will be marked implicitly declared.

Example 2: If the symbol appears free and undeclared in an expression, and then also in another expression that sits in an enclosing environment (an ancestor a few levels above the target), then it will be marked implicitly declared in that outer, ancestor environment, and not anywhere else. Because the implicit declaration acts as a declaration at the start of the enclosing ancestor, its scope includes all the descendants, including both expressions in which it appears free and undeclared.

Example 3: If the symbol appears free and undeclared twice, once in an expression in an environment $E_1$ and the other time in an expression in an environment $E_2$, and both $E_1$ and $E_2$ are children of the same parent, then implicit declarations will be added to both $E_1$ and $E_2$, because they are each the smallest enclosing environment for the free and undeclared instance of the symbol within them.

A callback function that can be used with the validate() function, as in Scoping.validate(L,Scoping.declareWhenSeen). If used in that manner, for every free and undeclared symbol in L, this function will add an implicit declaration of it at the first occurrence of that symbol in any given scope. (The validate() routine calls the callback only on the first occurrence in any given scope, so this function just adds an implicit declaration every time it is called.)

A callback function that can be used with the validate() function, as in Scoping.validate(L,Scoping.doNotDeclare). Because this function does absolutely nothing, that code is equivalent to calling Scoping.validate(L), but we provide this function for those times when the caller wishes to make it obvious, in the code, that implicit declarations are being expressly omitted.

This function reads the data stored by addImplicitDeclaration(). It could just as easily be done with getAttribute() and the appropriate key, but this API makes it easy to remain consistent if the underlying data storage method were to change.

The result will be an array of symbol names, possibly empty if no symbols are implicitly declared in the target.

Given a LogicConcept in which we have marked some symbols as implicitly declared, this function modifies data in the target, removing the given symbol from the implicitly declared list in the target. If it isn't already there, this function takes no action.

This function is made static so that any client can easily make use of the same convention for storing implicit declarations in a LogicConcept, but the standard way to compute and store such errors is by passing an implicit symbol declaration handler to validate().

This function reads the data stored by addScopeError(). It could just as easily be done with getAttribute() and the appropriate key, but this API makes it easy to remain consistent if the underlying data storage method were to change.

The result will be an object, JSON data of key-value pairs, the keys of which will be the types of scoping errors, such as "invalid" for invalid symbol declarations or "undeclared" for variables that appear free and undeclared. If any such key is missing, there are no errors of that type.

Refer to the documentation at the top of this page for information on what scoping is in general. This function is the main workhorse that validates symbol scoping inside an arbitrary Environment. It will typically be called on the topmost environment provided as input to Lurch, so that all symbols in the entire input have been analyzed for where their scopes begin and end.

This function can be called in two ways. First, it can be called with just one argument, in which case only the following tasks are done:

• Any symbol declaration (by a BindingEnvironment or a Declaration) that declares a symbol $x$ while sitting in the scope of some other declaration of the same symbol $x$ is marked with a scoping error of the form { redeclared : [ 'x' ] }. If more than one symbol is redeclared, the array may contain multiple entries.
• Any symbol $x$ bound by a BindingExpression in the scope of a declaration of the same symbol $x$ or another binding of the same symbol $x$ is marked with a scoping error of the form { redeclared : [ 'x' ] }. If more than one symbol is redeclared by the binding, the array may contain multiple entries.
• Any symbol $x$ used free in an Expression but not in the scope of any declaration (by a BindingEnvironment or a Declaration) is marked with a scoping error of the form { undeclared : [ 'x' ] }. If more than one symbol is used free and undeclared, the array may contain multiple entries. Such an error is placed only on the first use of the symbol in any given scope; later uses of the same symbol in the same scope are not also marked.

Note that a single LogicConcept might have more than one type of error. For instance, a Declaration that attempts to re-declare a symbol $x$, and whose body contains the symbols $y$ and $z$ free and undeclared might have an error of the form { redeclared : [ 'x' ], undeclared : [ 'y', 'z' ] }.

There are a variety of sensible ways to handle variables that are free and undeclared. On the permissive end of the spectrum, a client may wish to simply ignore them, in which case the error feedback under the undeclared headings can be ignored. On the strict end of the spectrum, a client may refuse to process input that contains free and undeclared symbols. Such clients can pay particular attention to the feedback under the undeclared headings. But many clients will take a middle road of some type, such as treating the first use of the symbol as an implicit declaration of the symbol, either at that location, or at the beginning of its parent environment, or something else.

To help clients who wish to take this middle road, this function has an optional second argument. If a function is provided as the second argument, it will be called on the first instance of every free and undeclared symbol before the validation work described above is executed. The function will be passed two parameters at each call: the name of the symbol that appears free and undeclared, and the LogicConcept in which it appears. These calls will take place in tree-traversal order (that is, earlier nodes first).

The callback function will often want to mark some LogicConcept as the location of the implicit declaration of the symbol in question. It can do so by calling addImplicitDeclaration(). Note that an implicit declaration marked in a LogicConcept L takes effect exactly at L, in the sense that the scope of the declaration includes L itself and continues on through the rest of L's scope.

While callers can provide a callback function for whatever behavior they desire, we also provide some pre-built callback functions, for common actions the caller may desire: declareWhenSeen(), declareInAncestor(), declareGlobal(), and doNotDeclare().