More docs fixes. Fix quotes. Fix spellings.
This commit is contained in:
Fedor Isakov
parent
9cd2d67056
commit
bceb1c3b21
|
|
@ -11,7 +11,7 @@ The process of evaluating code rules consists of two stages:
|
|||
1. Collecting handlers and applying rules.
|
||||
2. Processing constraint productions collected in the first stage.
|
||||
|
||||
Stage one is executed in the background in a read action, and is expected to finish quickly. Stage two is executed on a worker thread and does not require reads or writes. After the second stage is finished there is a short write action which «publishes» collected types.
|
||||
Stage one is executed in the background in a read action, and is expected to finish quickly. Stage two is executed on a worker thread and does not require reads or writes. After the second stage is finished there is a short write action which “publishes” collected types.
|
||||
|
||||
### Applying rules
|
||||
|
||||
|
|
@ -27,34 +27,34 @@ Generated constraint productions constitute the constraints program, which is th
|
|||
|
||||
In the second stage the constraints program is executed.
|
||||
|
||||
To begin execution, a *query* is selected, which contains the list of constraints to be activated. Query can be viewed as a regular production, which is triggered unconditionally, but no earlier than all headless productions (marked as «on start») have fired.
|
||||
To begin execution, a *query* is selected, which contains the list of constraints to be activated. Query can be viewed as a regular production, which is triggered unconditionally, but no earlier than all headless productions (internally marked as “on start”) have fired.
|
||||
|
||||
There is a fixed order in which productions are fired on start of program execution. First, all «on start» productions are triggered. All constraints activated by these productions are processed normally, and after there are no more productions to be triggered, the query is fired.
|
||||
There is a fixed order in which productions are fired on start of program execution. First, all “on start” productions are triggered. All constraints activated by these productions are processed normally, and after there are no more productions to be triggered, the query is fired.
|
||||
|
||||
Order of productions fired:
|
||||
1. «on start» productions
|
||||
1. “on start” productions
|
||||
2. query production
|
||||
|
||||
While constraints program is run, it is allowed to report feedback, such as assign calculated types or report problems, using special constructs, that are available as predicates in the body of production.
|
||||
|
||||
For example, type **node** can be assigned to source model location with *set type* operation. Essentially, assigning a type node can be understood as a way of annotating source model with additional information, which can then be reused by subsequent invocations of code rules or displayed to the user.
|
||||
For example, type **node** can be assigned to source model location with *set type* operation. Essentially, assigning a type node can be understood as a way of annotating source model with additional information, which can then be reused by subsequent invocations of code rules or displayed to the user.
|
||||
|
||||
|
||||
_(example showing type assigned from a production)_
|
||||
|
||||
Failures during constraints program execution are caught with the help of alternative body branches, where those are provided. An uncaught failure terminates program execution and is reported to the user.
|
||||
|
||||
In the following example, a potential error is caught in the `else` branch and a corresponding errors is reported. Execution of constraints program is not terminated though, so other problems may still be reported.
|
||||
In the following example, a potential error is caught in the `else` branch and a corresponding errors is reported. Execution of constraints program is not terminated though, so other problems may still be reported.
|
||||
|
||||
|
||||
_(example of using an alternative body branch)_
|
||||
|
||||
### User interface
|
||||
|
||||
The user interface is defined by a plugin responsible for particular language aspect.
|
||||
The user interface is defined by a plugin responsible for particular language aspect.
|
||||
|
||||
|
||||
_(context menu with typechecking actions)_
|
||||
_(context menu with type checking actions)_
|
||||
|
||||
### Activation trace view
|
||||
|
||||
|
|
@ -63,8 +63,7 @@ During execution of a constraints program all activation/suspension/deactivation
|
|||
|
||||
_(sample proof in propositional logic)_
|
||||
|
||||
Above is an example of a proof in propositional logic, the trace of checking which is provided below. When a row in the left pane side selected, the right pane displays the contents of *constraints store* at this moment in time.
|
||||
Above is an example of a proof in propositional logic, the trace of checking which is provided below. The rows in the left pane correspond to events happening during constraints processing, such a constraint activated or suspended, or a production triggered. When a row in the left pane side selected, the right pane displays the contents of *constraints store* captured at the moment the event occurred.
|
||||
|
||||
|
||||
_(activation trace view)_
|
||||
|
||||
|
|
|
|||
|
|
@ -20,19 +20,19 @@ Control flow analysis starts with activating constraint `trace/0`. This initiate
|
|||
|
||||
_(controlflow query)_
|
||||
|
||||
Constraint `follow/2` binds together two locations that are adjacent in the control flow graph, and `merge/2` is an auxiliary helper, which is used to mark the «exit point» for a search that goes *depth-first* into subexpressions.
|
||||
Constraint `follow/2` binds together two locations that are adjacent in the control flow graph, and `merge/2` is an auxiliary helper, which is used to mark the “exit point” for a search that goes *depth-first* into subexpressions.
|
||||
|
||||
|
||||
_(control flow check of binary operation)_
|
||||
|
||||
The meaning of `follow(@A, @B)` is «B follows A», and `merge(@X, @Y)` — «X should follow whatever location is last after traversing Y».
|
||||
The meaning of `follow(@A, @B)` is “B follows A”, and `merge(@X, @Y)` — “X should follow whatever location is last after traversing Y”.
|
||||
|
||||
Read and write locations are processed once the control flow graph has been built. This is when `rw/0` constraint activates and starts this phase of the analysis. This phase also consists of two parts, and these are repeated for every method declaration. This is done by putting two constraints in a conjunction, as shown below.
|
||||
|
||||
|
||||
_(initiating collection of «uses» map, then activating «live» analysis)_
|
||||
_(initiating collection of “uses” map, then activating “live” analysis)_
|
||||
|
||||
First, the control flow graph is walked from starting location, which can be a method declaration, for example. During the traversal of the graph a mapping of «uses» is collected — a map where keys are locations that are read, and values are sets of locations where reading happens. Uninitialised reads are detected at this stage.
|
||||
First, the control flow graph is walked from starting location, which can be a method declaration, for example. During the traversal of the graph a mapping of “uses” is collected — a map where keys are locations that are read, and values are sets of locations where reading happens. Uninitialised reads are detected at this stage.
|
||||
|
||||
Second, all *write* locations are visited again, this time ensuring there is at least one read after a write.
|
||||
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ The dataform table contains obvious declarations for the only primitive type `bo
|
|||
|
||||
_(dataform table)_
|
||||
|
||||
There is only one query of kind `TYPECHECK`, which launches types recovery. All the type checking is done by the automatic productions «on start».
|
||||
There is only one query of kind `TYPECHECK`, which launches types recovery. All the type checking is done by the automatic productions “on start”.
|
||||
|
||||
Handlers are separated into types recovery, operations with universal type, and the rest, which is assigning types to expressions. Type checking follows the program’s syntactic structure.
|
||||
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ _(example of proof in Fitch system)_
|
|||
|
||||
Base inference rules are defined by `samples.fitch.propositionalLogic` language, with two other extending the set of rules appropriately. Herbrand logic extends this language with relations, functions, and quantifiers, whereas First Order logic adds equality. Each of the logics also define their own root proof concept.
|
||||
|
||||
The proof validation is done through type checking with the only type being «Ok». There is one query of kind `TYPECHECKING`, which simply activates `checkAll()`. Every logical formula from reasonings is translated into a dataform, with logical variables taking place of quantifier variables.
|
||||
The proof validation is done through type checking with the only type being “Ok”. There is one query of kind `TYPECHECKING`, which simply activates `checkAll()`. Every logical formula from reasonings is translated into a dataform, with logical variables taking place of quantifier variables.
|
||||
|
||||
Each reasoning has a *conclusion*, which is expanded to term and assigned to the source location with `conclusion()` constraint. In addition, at the start, all proof’s premises are marked as valid using `valid()`. The process then continues recursively, with every inference rule constructed according to a single pattern:
|
||||
- the head ensures the conclusions of all rule’s *bases* (input premises) match the required form,
|
||||
|
|
@ -32,7 +32,7 @@ _(example of an inference rule)_
|
|||
|
||||
The rule’s body activates `valid()` constraint, therefore only reasonings that have met the requirement are marked as valid. Check handler marks reasonings that weren’t validated as erroneous.
|
||||
|
||||
Finally, if the proof’s goal is marked valid, it is assigned «Ok» type, otherwise it is marked with error.
|
||||
Finally, if the proof’s goal is marked valid, it is assigned “Ok” type, otherwise it is marked with error.
|
||||
|
||||
|
||||
[^inlog]: Stanford Introduction to Logic [http://logic.stanford.edu/intrologic/homepage/index.html](http://logic.stanford.edu/intrologic/homepage/index.html)
|
||||
|
|
|
|||
|
|
@ -11,9 +11,9 @@ github-path: /tree/master/samples/mpscore
|
|||
|
||||
Short explanation of the architecture of BL-specific type system built with *code rules*.
|
||||
|
||||
This sample is the main result of developing code rules. It is still work in progress, but the main areas of typechecking BaseLanguage have been covered. Here we briefly touch on the implementation details.
|
||||
This sample is the main result of developing code rules. It is still work in progress, but the main areas of type checking BaseLanguage have been covered. Here we briefly touch on the implementation details.
|
||||
|
||||
First, all the BaseLanguage types have corresponding dataforms, and in addition there are definitions of types that are only ever used during typechecking, such as capture type.
|
||||
First, all the BaseLanguage types have corresponding dataforms, and in addition there are definitions of types that are only ever used during type checking, such as capture type.
|
||||
|
||||
The macros in `Types` macro table define the rules how types are constructed, ensuring, among other things, that bounds on type parameters are correctly processed.
|
||||
|
||||
|
|
@ -25,7 +25,7 @@ Primitive types define allowed ranges, so the dataforms for these types have val
|
|||
|
||||
_(examples of primitive type dataforms)_
|
||||
|
||||
There are two queries defined for typechecking and for converting a type to another type. The latter is used when testing for *subtyping*. ConvertsTo query expands both its parameters before activating `convertsTo()` constraint, which launches the processing of the relation.
|
||||
There are two queries defined for type checking and for converting a type to another type. The latter is used when testing for *subtyping*. ConvertsTo query expands both its parameters before activating `convertsTo()` constraint, which launches the processing of the relation.
|
||||
|
||||
|
||||
_(the production from `ConvertsTo` query)_
|
||||
|
|
@ -45,7 +45,7 @@ An integer literal is simply assigned the type `int` with the value being the va
|
|||
|
||||
_(assigning the type to `int` literal)_
|
||||
|
||||
From these starting points typechecking continues up the syntax tree until there are no more productions left that can be triggered.
|
||||
From these starting points type checking continues up the syntax tree until there are no more productions left that can be triggered.
|
||||
|
||||
A `dot expression` propagates the type from operation to the whole expression.
|
||||
|
||||
|
|
|
|||
|
|
@ -8,14 +8,14 @@ weight: 10
|
|||
|
||||
This project is an attempt to bring logic programming to JetBrains MPS[^mps] in order to facilitate tasks related to source model analysis, and which require logical inference of some kind to operate. Examples include type checking and control flow.
|
||||
|
||||
Type system in MPS is traditionally defined with help of type checking rules, in particular inference rules, which allow for making logical statements about types, such as «*is a*» or «*is a subtype of*», enabling the internal engine to infer the specific type, deriving it from a collection of such statements, which are referred to as type equations and inequalities.
|
||||
Type system in MPS is traditionally defined with help of type checking rules, in particular inference rules, which allow for making logical statements about types, such as “*is a*” or “*is a subtype of*”, enabling the internal engine to infer the specific type, deriving it from a collection of such statements, which are referred to as type equations and inequalities.
|
||||
|
||||
|
||||
_(statement in `j.m.lang.typesystem` language)_
|
||||
|
||||
Albeit brief and concise, this notation leaves many questions unanswered when it comes to how exactly the system of equations and inequalities is processed. In other words, type inference is — for the most part — left up to the internal engine to decide. This limits the options for the author of type system to control how exactly subtyping is defined, and what happens with type parameters when computing sub- or supertype. Java, for instance, has several kinds of «conversions» with clearly defined rules controlling how types are transformed and what types are compatible in certain situations. All of this has to be emulated with «strong» and «weak» subtyping in MPS.
|
||||
Albeit brief and concise, this notation leaves many questions unanswered when it comes to how exactly the system of equations and inequalities is processed. In other words, type inference is — for the most part — left up to the internal engine to decide. This limits the options for the author of type system to control how exactly subtyping is defined, and what happens with type parameters when computing sub- or supertype. Java, for instance, has several kinds of “conversions” with clearly defined rules controlling how types are transformed and what types are compatible in certain situations. All of this has to be emulated with “strong” and “weak” subtyping in MPS.
|
||||
|
||||
Another example is the all too well known *when_concrete*, which is basically a suspended block that gets executed when the type, that serves as its parameter, is computed. Sometimes this never happens during type inference, which results in numerous «*when concrete is never concrete*» warnings, leaving the user wondering what went wrong. This, however, is very much a necessary evil, since there are no other possibilities to hook into the engine in order to spy on types, and knowing the exact form of a type is sometimes required for further inference.
|
||||
Another example is the all too well known *when_concrete*, which is basically a suspended block that gets executed when the type, that serves as its parameter, is computed. Sometimes this never happens during type inference, which results in numerous “*when concrete is never concrete*” warnings, leaving the user wondering what went wrong. This, however, is very much a necessary evil, since there are no other possibilities to hook into the engine in order to spy on types, and knowing the exact form of a type is sometimes required for further inference.
|
||||
|
||||
Consider how type of a method call is calculated: details aside, in essence *when_concrete* has to be applied to types of each argument. Then we should either turn to inequalities and rely on the inference engine, or analyse the type structure and run closing computation when the *last* unknown type is finalised.
|
||||
|
||||
|
|
@ -26,10 +26,10 @@ Code rules may have a solution to these and other issues. The core idea is to em
|
|||
|
||||
To illustrate the idea, let’s look at a couple of examples. These are taken from the type system implementation for BaseLanguage.
|
||||
|
||||
Typechecking assignment expression could look like the following. What the code says is basically: once left and right sides of the assignment have types (not necessarily ground types), test if left side’s type converts to right side’s. Constraint `convertsTo/2` is defined in the same aspect, and the typesystem author has full control how it deals with type parameters, for example.
|
||||
Type checking assignment expression could look like the following. What the code says is basically: once left and right sides of the assignment have types (not necessarily ground types), test if left side’s type converts to right side’s. Constraint `convertsTo/2` is defined in the same aspect, and the typesystem author has full control how it deals with type parameters, for example.
|
||||
|
||||
|
||||
_(typechecking assignment with constraint production)_
|
||||
_(type checking assignment with constraint production)_
|
||||
|
||||
Instead of waiting until a type has been finalised in order to access its structure, *pattern matching* is used to trigger productions only on types of certain form. The example below shows how `convertsTo/2` is resolved for an instance of `LowerBoundType`.
|
||||
|
||||
|
|
@ -38,7 +38,7 @@ _(resolution of `convertsTo/2` constraint using pattern matching)_
|
|||
|
||||
The following is the list of features made available to users of MPS with *code rules* plugin.
|
||||
|
||||
- A language for building rules that serve as production templates, and as regular «checking» rules. The rules may be concept-specific or standalone, if there is a need to provide constraints that are invariant for every invocation.
|
||||
- A language for building rules that serve as production templates, and as regular “checking” rules. The rules may be concept-specific or standalone, if there is a need to provide constraints that are invariant for every invocation.
|
||||
|
||||
- *Constraint Processing System* — an extension of CHR[^chr] semantics allowing the use of unification in production’s head with automatic binding of logical variables on successful match. This extension also supports alternative body branches, as well as calling arbitrary Java code. Representing type inference in the form of logical productions helps achieve extensibility, as productions defined by extension languages can be easily blended in.
|
||||
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ The following table contains root concepts that belong to code rules definition.
|
|||
|
||||
#### Rules
|
||||
|
||||
The aim of rules defined by handlers is again twofold: firstly, they may serve as regular «checking» rules, and also, most importantly, they contribute constraint productions. These are created with a DSL that allows mixing of productions and Java code, and can also include constraint fragments inside a production template.
|
||||
The aim of rules defined by handlers is again twofold: firstly, they may serve as regular “checking” rules, and also, most importantly, they contribute constraint productions. These are created with a DSL that allows mixing of productions and Java code, and can also include constraint fragments inside a production template.
|
||||
|
||||
The following example is from experimental *control flow* aspect for baseLanguage. It demonstrates how a production is constructed using a template. A template is enclosed into a pair of `%% … %%` symbols and yields constraints wrapped into special `<% … %>` brackets. In this particular case `write/2` constraint is optional and is only added to the body of production in case the condition is satisfied (a location corresponding to a local variable is written to only if it has an initialiser).
|
||||
|
||||
|
|
@ -58,7 +58,7 @@ _(example of standalone rule without input)_
|
|||
|
||||
Rule’s contents is a block of code that gets executed when the rule is applied to the source model. If the input is specified, the declared parameter is available in rule’s body.
|
||||
|
||||
Rules may affect the scope of model locations that are processed during an evaluation session. Suppose a production responsible for typechecking a particular location in source model relies on presence of productions that are only available if some other location is processed as well. To guarantee that a certain model location is processed during the evaluation session, one uses `require` statement.
|
||||
Rules may affect the scope of model locations that are processed during an evaluation session. Suppose a production responsible for type checking a particular location in source model relies on presence of productions that are only available if some other location is processed as well. To guarantee that a certain model location is processed during the evaluation session, one uses `require` statement.
|
||||
|
||||
|
||||
_(example of using `require` statement)_
|
||||
|
|
@ -67,7 +67,7 @@ _(example of using `require` statement)_
|
|||
|
||||
*Productions* can be created at any place within rule body. A production has three main parts called *head*, *guard*, and *body*. Head defines what constraints trigger this production, and it can only contain constraints defined by the handler or one of the handlers it extends. Body can contain any visible constraints, as well as *predicates*. A production must include either the body or the head, no production can omit both. Guard is optional, and it can only contain predicates.
|
||||
|
||||
Both head and body can declare *logical variables*. By default a logical variable ranges over *terms*, although any POJO may be serve as a value.
|
||||
Both head and body can declare *logical variables*. By default a logical variable ranges over *terms*, although any POJO[^pojo] may be serve as a value.
|
||||
|
||||
|
||||
_(production declaring logical variables)_
|
||||
|
|
@ -92,7 +92,7 @@ _(example of constraint argument referring to a model location)_
|
|||
|
||||
Whereas the production’s head can only contain constraints, there are also other logical clauses that are used in guard and body.
|
||||
|
||||
A *predicate* is a built-in construct that serves two purposes: when used in guard, it serves to query if the condition is satisfied, and when invoked from body, it asserts the condition. An example is `unifies` predicate, displayed as `=`, which, if used in guard, only tests that its arguments can be unified, otherwise if called from body, it invokes the actual unification. There are also predicates that can only be queries, such as `isFree/1` or `isBound/1`, testing if a logical variable is free or has value assigned.
|
||||
A *predicate* is a built-in construct that serves two purposes: when used in guard, it acts to query if the condition is satisfied, and when invoked from body, it asserts the condition. An example is `unifies` predicate, displayed as `=`, which, if used in guard, only tests that its arguments can be unified, otherwise if called from body, it invokes the actual unification. There are also predicates that can only be queries, such as `isFree/1` or `isBound/1`, testing if a logical variable is free or has value assigned.
|
||||
|
||||
Production’s guard can only contain predicates, and the body can contain both constraints and predicates.
|
||||
|
||||
|
|
@ -104,7 +104,7 @@ Arbitrary Java code can be called with `eval/1` predicate. It accepts either an
|
|||
|
||||
_(example of using `eval/1` predicate)_
|
||||
|
||||
In order to make use of macro definitions, which are essentially parameterised production templates extracted to a separate root, one of two pseudo predicates can be used: `expand` and `call`. The former accepts a node, whereas the second expects the argument that are substituted as macro parameters.
|
||||
In order to make use of macro definitions, which are essentially parameterised production templates extracted to a separate root, one of the two pseudo predicates can be used: `expand` and `call`. The former accepts a node, whereas the second expects the arguments that are substituted as macro parameters.
|
||||
|
||||
***Examples of expand/call pseudo predicates***
|
||||
|
||||
|
|
@ -155,3 +155,4 @@ _(example of a dataform definition for classifier type)_
|
|||
_(examples of dataform definition for long type)_
|
||||
|
||||
[^dft]: this concept is defined in another language, `jetbrains.mps.logic`
|
||||
[^pojo]: Plain Old Java Object — any Java object conforming to equals/hashCode contract
|
||||
|
|
|
|||
|
|
@ -8,11 +8,13 @@ weight: 20
|
|||
|
||||
Analysis of source code or model with *code rules* can be described as a two-phase process.
|
||||
|
||||
In the first phase, languages used by the model being analysed and their prototypes (meaning the languages that are being *extended*, but not used directly) are surveyed for the appropriate *code rules* aspect model, which is `types` in case of type checking, for example. Contents of this aspect model is a contribution of this particular language. All rules within this model are applied to the source model, with rules coming from extension languages having higher priority.
|
||||
In the first phase, languages used by the model being analysed and their prototypes (meaning the languages that are being *extended*, but not used directly) are surveyed for the appropriate *code rules* aspect model, which is `types` in case of type checking, for example. Each language defines its contribution to the rules set by declaring its own *code rules* in the appropriate aspect model. All rules within this aspect model are applied to the source model, with rules coming from extension languages having higher priority.
|
||||
|
||||
The outcome of this phase is a *constraints program*, which is a collection of *handlers*, which in turn represent lists of *productions*. This «program» however, exists in memory only as it does not have any textual representation. Aside from generating productions, the rules can also process the model normally, reporting errors as usual.
|
||||
***MPS contributions normally**
|
||||
|
||||
The first phase runs in «read action», blocking potential writes, which means the editor may become unresponsive if a write action is requested. Ideally the rules should finish quickly and postpone all heavy load to the next phase, which can then be run in the background, as the access to `SModel` is no longer required.
|
||||
The outcome of this phase is a *constraints program*, which is a collection of *handlers*, which in turn represent lists of *productions*. This “program” however, exists in memory only as it does not have any textual representation.
|
||||
|
||||
The first phase runs in “read action”, blocking potential writes, which means the editor may become unresponsive if a write action is requested. Ideally the rules should finish quickly and postpone all heavy load to the next phase, which can then be run in the background, as the access to `SModel` is no longer required.
|
||||
|
||||
In the second phase the constraints program that was created in phase one is executed. Execution starts with a query, which serves as an entry point to the program. For example, type system defines `TYPECHECK` and `CONVERT` queries, intended for running type checking and testing if a type can be converted to another type, correspondingly. Queries are declared in the same aspect model.
|
||||
|
||||
|
|
@ -35,7 +37,7 @@ An of course, if something can go wrong, it will. In case type inference is unsu
|
|||
|
||||
_(example of a query production with alternative body)_
|
||||
|
||||
Here, `recoverAll/0` constraint is moved out to an «*alternative branch*» of production body, which allows it to be activated even if there was an error while processing the main branch.
|
||||
Here, `recoverAll/0` constraint is moved out to an “*alternative branch*” of production body, which allows it to be activated even if there was an error while processing the main branch.
|
||||
|
||||
To illustrate how automatic binding of logical variables work, consider the following example. Constraint `typeOf/2` associates a type with a location in source model, and constraint `convertsTo/2` ensures its 1st argument can be converted to the 2nd, which must both be types.
|
||||
|
||||
|
|
@ -44,7 +46,7 @@ _(example of rule with production)_
|
|||
|
||||
This production is triggered when both locations referred to by `ae.lValue` and `ae.rValue` have their types assigned, as both `typeOf/2` constraints must be present for a match to be successful. Once production’s head is matched, both logical variables `LType` and `RType` become bound to whatever was the 2nd argument of corresponding occurrences of `typeOf/2` constraint.
|
||||
|
||||
It’s important to note, that although on successful match both `lValue` and `rValue` have types, it’s not guaranteed that these types are *ground*. A type may be represented by a free logical variable, or a term containing free variables. Another very important thing to notice is that a logical variable enjoys full privileges of being an argument to a constraint. Which means, if in the above example both variables are free, and `LType = RType`, then both locations will have essentially the *same* type (in the sense of «same instance»), not just matching types.
|
||||
It’s important to note, that although on successful match both `lValue` and `rValue` have types, it’s not guaranteed that these types are *ground*. A type may be represented by a free logical variable, or a term containing free variables. Another very important thing to notice is that a logical variable enjoys full privileges of being an argument to a constraint. Which means, if in the above example both variables are free, and `LType = RType`, then both locations will have essentially the *same* type (in the sense of “same instance”), not just matching types.
|
||||
|
||||
The following example illustrates the use of *pattern matching* in production’s head. Here the first argument to constraint `convertsTo/2` in the head is a logical variable with pattern expression. In this case the production will only be triggered if the active constraint’s first argument is *bound* (is not a free logical variable), and it matches the pattern.
|
||||
|
||||
|
|
|
|||
|
|
@ -7,11 +7,11 @@ weight: 50
|
|||
|
||||
# Constraints Processing System
|
||||
|
||||
This section briefly overlooks how constraint processing works. The system described here follows loosely the CHR specification, and has been in particular heavily influenced by JCHR[^jchr] implementation. The distinctive features are built-in support for logical variables, terms, and pattern matching. Alternative body branches are a deviation from the standard CHR.
|
||||
This section briefly overviews how constraints processing works. The system described here follows loosely the CHR specification, and has been in particular heavily influenced by JCHR[^jchr] implementation. The distinctive features are built-in support for logical variables, terms, and pattern matching. Alternative body branches are a deviation from the standard CHR.
|
||||
|
||||
### Terms and unification
|
||||
|
||||
Constraints processing relies heavily on the use of *terms* as data type. Abstractly speaking, terms are functions of 0 or more arguments. Any opaque value captured by a term must be a POJO.
|
||||
Constraints processing relies heavily on the use of *terms* as data type. Abstractly speaking, terms are functions of zero or more arguments. Any opaque value captured by a term must be a POJO.
|
||||
|
||||
```
|
||||
f(g(), h(k()))
|
||||
|
|
@ -22,7 +22,7 @@ Constraints processing relies heavily on the use of *terms* as data type. Abstra
|
|||
```
|
||||
_(examples of terms)_
|
||||
|
||||
The unique feature of terms is that they support unification. Unification of two terms is possible with or without *variables* being used as subterms of either participant, but in the latter case the two terms must be equal.
|
||||
The unique feature of terms is that they support unification. Unification of two terms is possible with or without *variables* being used as subterms of either participant, but in the latter case the two terms must be equal.
|
||||
|
||||
A term variable ranges over terms. A substitution is a mapping of variables to terms. Unification searches for a substitution $\sigma$, such that for two terms being unified, $f$ and $g$, the following holds: $\sigma f = \sigma g$.
|
||||
|
||||
|
|
@ -32,11 +32,15 @@ A term variable ranges over terms. A substitution is a mapping of variables to t
|
|||
f(X, h(X)) and f(g(), h(k())) can't be unified
|
||||
```
|
||||
|
||||
Pattern matching is possible when variables are only used by one of the terms, which is then serves as pattern. To test if a pattern matches a given term can be implemented by a linear time algorithm, whereas full unification is slightly more complicated.
|
||||
Pattern matching is possible when variables are only used by one of the terms, which is then serves as pattern. To test if a pattern matches a given term can be implemented by a linear time algorithm, whereas full unification is slightly more complicated.
|
||||
|
||||
***MGU***
|
||||
|
||||
***Occurrs check***
|
||||
|
||||
### Logical variables
|
||||
|
||||
Logical variables serve to identify an object that is to be determined in the future. They are *monotonic*, in the sense that once a variable is assigned a particular value, it stays assigned to that value. In addition, they implement a *union-find data structure*[^uf] a.k.a. «disjoint set». Any free logical variable can be assigned a class by setting its «parent» field to point to the class’s representative. All logical variables belonging to the same class are treated as exactly one variable. Logical variables notify observers when they become ground and when their *parent* (class representative) changes.
|
||||
Logical variables serve to identify an object that is to be determined in the future. They are *monotonic*, in the sense that once a variable is assigned a particular value, it stays assigned to that value. In addition, they implement a *union-find data structure*[^uf] a.k.a. “disjoint set”. Any free logical variable can be assigned a class by setting its “parent” field to point to the class’s representative. All logical variables belonging to the same class are treated as exactly one variable. Logical variables notify observers when they become ground and when their *parent* (class representative) changes.
|
||||
|
||||
```
|
||||
val X = Logical("X")
|
||||
|
|
@ -75,9 +79,9 @@ Constraints are, simply put, tuples with fixed arity and a symbol attached. In s
|
|||
|
||||
Constraints are activated from a production’s body and stay active until there are no possible matches with any of productions’s heads. If a constraint is not discarded by a production, it is stored for future use. Stored constraints represent the program’s state.
|
||||
|
||||
The following figure shows the lifecycle of a constraint. The big rounded square in the middle contains the states, in which a constraint is considered «alive»: it can be either «active» or «stored», but available for filling up vacant positions in a production’s head. A stored constraint can be reactivated if one of its arguments changes, such as when a logical variable becomes ground.
|
||||
The following figure shows the lifecycle of a constraint. The big rounded square in the middle contains the states, in which a constraint is considered “alive”: it can be either “active” or “stored”, but available for filling up vacant positions in a production’s head. A stored constraint can be reactivated if one of its arguments changes, such as when a logical variable becomes ground.
|
||||
|
||||
A successfully fired production, which declares one or more of constraints in its head to be «replaced», causes these to be terminated.
|
||||
A successfully fired production, which declares one or more of constraints in its head to be “replaced”, causes these to be terminated.
|
||||
|
||||
|
||||
_(lifecycle of a constraint)_
|
||||
|
|
@ -94,25 +98,25 @@ Predicates must implement ask/tell protocol. If a predicate is invoked from prod
|
|||
|
||||
### Constraint productions
|
||||
|
||||
Constraints program is built from productions. Each production has three parts: the part that is responsible for triggering the production, called «head», the part that checks for pre-conditions, called «guard», and the part that is evaluated when production is fired, which is called «body».
|
||||
Constraints program is built from productions. Each production has three parts: the part that is responsible for triggering the production, called “head”, the part that checks for pre-conditions, called “guard”, and the part that is evaluated when production is fired, which is called “body”.
|
||||
|
||||
#### Head
|
||||
#### Head
|
||||
|
||||
Head is a set of constraints which are all required to be alive in order for production to fire. This set is divided into «kept» part and «replaced» part, the latter containing constraints that are to be discarded as soon as the production fires.
|
||||
Head is a set of constraints which are all required to be alive in order for production to fire. This set is divided into “kept” part and “replaced” part, the latter containing constraints that are to be discarded as soon as the production fires.
|
||||
|
||||
A production is triggered when there are constraint occurrences matching all constraints specified in production’s head. These occurrences include the active constraint, plus any additional matching constraints that are currently alive, filling the other vacant slots.
|
||||
|
||||
There is some terminology inherited from CHR that can be useful when discussing the kinds of productions. In the following table `E` and `E'` are the set of constraints in production’s head, `C` is a conjunction of predicates serving as guard, and `G` is a conjunction of predicates and constraints in production’s body.
|
||||
|
||||
| «kept» set `E` | «replaced» set `E’` | Notation | Designation |
|
||||
| “kept” set `E` | “replaced” set `E’` | Notation | Designation |
|
||||
|:--|:--|:--:|:--|
|
||||
| empty | non-empty | `E’ <=> C | G` | Simplification |
|
||||
| non-empty | empty | `E => C | G` | Propagation |
|
||||
| non-empty | non-empty | `E \ E’ <=> C | G` | Simpagation |
|
||||
|
||||
Essentially, a production with only «kept» constraints in its head is a «propagation», the one with only «replaced» constraints is a «simplification», and the one that has both «kept» and «replaced» constraints is a combination of the two.
|
||||
Essentially, a production with only “kept” constraints in its head is a “propagation”, the one with only “replaced” constraints is a “simplification”, and the one that has both “kept” and “replaced” constraints is a combination of the two.
|
||||
|
||||
In addition, we define a fourth kind of production, an «auto» production with an empty head. As the name implies, such production is triggered automatically on start of constraints program execution.
|
||||
In addition, we define a fourth kind of production, an “auto” production with an empty head. As the name implies, such production is triggered automatically on start of constraints program execution.
|
||||
To illustrate the idea of using *stored* constraints to fill vacant positions when matching a production, let’s consider an example — a production resolving `containedIn/2` constraint, which corresponds to *type parameter containment* relation of BaseLanguage types.
|
||||
|
||||
|
||||
|
|
@ -135,7 +139,7 @@ Body is a conjunction of predicates and constraint activations. When triggered,
|
|||
|
||||
The paper by Betz and Frühwirth[^lls] gives an excellent tretise on semantics of CHR using *linear logic*. Since our constraints processing system is based on CHR, this semantics is valid for it also.
|
||||
|
||||
Linear logic abandons boolean values and replaces them with consumable resources. Consequently, it introduces its own set of connectives, from which we are interested only in the following: $!,\otimes,\multimap$. The *multiplicative conjunction* $\otimes$ combines two or more resources that are all available at the same time. The symbol $!$ (*of course*) marks a resource that can’t be exhausted. And instead of implication $\rightarrow$ one uses $\multimap$ symbol, the meaning of which is a transformation of one resource to another. The formula $A \multimap B$ is read: «consuming $A$, produce $B$ », that is given a resource $A$, we can assume $B$, but $A$ can no longer be used.
|
||||
Linear logic abandons boolean values and replaces them with consumable resources. Consequently, it introduces its own set of connectives, from which we are interested only in the following: $!,\otimes,\multimap$. The *multiplicative conjunction* $\otimes$ combines two or more resources that are all available at the same time. The symbol $!$ (*of course*) marks a resource that can’t be exhausted. And instead of implication $\rightarrow$ one uses $\multimap$ symbol, the meaning of which is a transformation of one resource to another. The formula $A \multimap B$ is read: “consuming $A$, produce $B$ ”, that is given a resource $A$, we can assume $B$, but $A$ can no longer be used.
|
||||
|
||||
Simplification is represented by a proposition stating that from valid guard condition $C$, which can be reused, we can imply the following: given the set of constraints $E$ matching the production’s left-hand side, we can find such substitution $\sigma$, such that we can now assume the set of constraints produced from production’s body: $\sigma G$. All free variables in this proposition are universally quantified and the proposition itself can be reused infinitely.
|
||||
|
||||
|
|
@ -143,7 +147,7 @@ Simplification is represented by a proposition stating that from valid guard con
|
|||
!\forall((!C^L) \multimap
|
||||
(E^L \multimap \exists\bar{y}G^L)) \\]
|
||||
|
||||
Propagation is different from simplification in that the set of constraints $E$, which triggered the production, is made available together with the constraints produced by the body, so the constraints in $E$ are not «consumed».
|
||||
Propagation is different from simplification in that the set of constraints $E$, which triggered the production, is made available together with the constraints produced by the body, so the constraints in $E$ are not “consumed”.
|
||||
|
||||
\\[ (E \Rightarrow C | G)^L :=
|
||||
!\forall((!C^L) \multimap
|
||||
|
|
@ -152,5 +156,5 @@ Propagation is different from simplification in that the set of constraints $E$,
|
|||
|
||||
[^jchr]: K.U.Leuven JCHR System [https://dtai.cs.kuleuven.be/CHR/JCHR/](https://dtai.cs.kuleuven.be/CHR/JCHR/)
|
||||
[^uf]: [https://en.wikipedia.org/wiki/Disjoint-set_data_structure](https://en.wikipedia.org/wiki/Disjoint-set_data_structure)
|
||||
[^pred]: a.k.a. «built-in constraints» in CHR literature
|
||||
[^pred]: a.k.a. “built-in constraints” in CHR literature
|
||||
[^lls]: Betz, H. and Frühwirth, T., 2005, October. A linear-logic semantics for constraint handling rules. In International Conference on Principles and Practice of Constraint Programming (pp. 137-151). Springer, Berlin, Heidelberg.
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ Constraints reactor is a small library written in Kotlin and Java, which impleme
|
|||
|
||||
## Implementation notes
|
||||
|
||||
Unification is implemented according to a «near-constant time» algorithm[^uni].
|
||||
Unification is implemented according to a “near-constant time” algorithm[^uni].
|
||||
|
||||
A trie[^trie] (a prefix tree) on flattened terms is used for indexing productions by value.
|
||||
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@
|
|||
- [x] pattern matching
|
||||
- [x] the '@' syntax
|
||||
- [ ] predicates vs constraints
|
||||
- [ ] **special predicates «expand» and «call»**
|
||||
- [ ] **special predicates “expand” and “call”**
|
||||
- [x] calling arbitrary Java code (eval)
|
||||
- [ ] guard (when)
|
||||
- [x] what operations are available in the guard
|
||||
|
|
@ -44,16 +44,16 @@
|
|||
- [x] macro parameters
|
||||
- [x] parameter initialiser
|
||||
- [ ] how macro can be called
|
||||
- [x] **special predicates «expand» and «call»**
|
||||
- [x] **special predicates “expand” and “call”**
|
||||
- [x] What is the meaning of macro body
|
||||
- [ ] referring logical variables
|
||||
- [x] «macroLogical» expression
|
||||
- [x] “macroLogical” expression
|
||||
- [ ] **$-wrapper for an expression**
|
||||
- [ ] **«substitution from context»**
|
||||
- [ ] **“substitution from context”**
|
||||
- [ ] context parameters
|
||||
- [ ] substitutions
|
||||
- [ ] context parameters
|
||||
- [ ] specifying parameters using «with» statement
|
||||
- [ ] specifying parameters using “with” statement
|
||||
|
||||
## Term table
|
||||
- [x] purpose of this root
|
||||
|
|
|
|||
Loading…
Reference in New Issue