From dceffeacbe0f5d42d9402ac387a6bdd3256fd948 Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Tue, 4 Sep 2018 11:14:06 +0200 Subject: [PATCH] Minor update of docs. Minor fixes and amendments. --- docs/_config.yml | 2 +- docs/content/allpages.md | 2 ++ docs/content/evaluating.md | 2 +- docs/content/intro.md | 2 +- docs/content/language.md | 2 +- docs/content/overview.md | 2 -- docs/content/processing.md | 5 ++++- docs/content/reactor.md | 20 ++++++++++---------- 8 files changed, 20 insertions(+), 17 deletions(-) diff --git a/docs/_config.yml b/docs/_config.yml index df8aa42a..ed81277b 100644 --- a/docs/_config.yml +++ b/docs/_config.yml @@ -8,7 +8,7 @@ baseurl: "/mps-coderules" # the subpath of your site, e.g. /blog url: "https://fisakov.github.io" # the base hostname & protocol for your site, e.g. http://example.com twitter_username: jetbrains_mps github_username: fisakov -time: 2018-09-03 +time: 2018-09-04 revision: 0.5.0 copyright: JetBrains s.r.o. copyright_url: "https://jetbrains.com" diff --git a/docs/content/allpages.md b/docs/content/allpages.md index 266dfd5f..d1009243 100644 --- a/docs/content/allpages.md +++ b/docs/content/allpages.md @@ -6,3 +6,5 @@ menu: false Type inference and type checking is a problematic area for language authors — users of JetBrains MPS, because of inherent intricacies of the problem and sometimes inadequate support from the framework. *Code Rules* is a new technology that brings logic programming in the form of constraints processing as a vehicle for implementing type inference. + +Thanks to its flexibility and independence from any specifics of type checking, this technology can be applied in other areas of model analysis where logical inference can be useful. diff --git a/docs/content/evaluating.md b/docs/content/evaluating.md index 1239ee5f..6c7e55a3 100644 --- a/docs/content/evaluating.md +++ b/docs/content/evaluating.md @@ -42,7 +42,7 @@ For example, type **node** can be assigned to source model location with *set ty ![](img/eval-settype-650.png) _(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. +Failures may be encountered during constraints program execution, such as a unification failure, and they 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. diff --git a/docs/content/intro.md b/docs/content/intro.md index e6591003..cd46f18d 100644 --- a/docs/content/intro.md +++ b/docs/content/intro.md @@ -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. 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. diff --git a/docs/content/language.md b/docs/content/language.md index dd6e86e9..2ede98cd 100644 --- a/docs/content/language.md +++ b/docs/content/language.md @@ -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 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 the 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). diff --git a/docs/content/overview.md b/docs/content/overview.md index f717e6d9..72ded1a8 100644 --- a/docs/content/overview.md +++ b/docs/content/overview.md @@ -10,8 +10,6 @@ Analysis of source code or model with *code rules* can be described as a two-pha 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. -***MPS contributions normally** - 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. diff --git a/docs/content/processing.md b/docs/content/processing.md index 1e1af919..ee1bf8bb 100644 --- a/docs/content/processing.md +++ b/docs/content/processing.md @@ -43,7 +43,8 @@ Unification may fail because the arity or the symbols of the two terms mismatch. ``` f(X, h(X)) and f(g(), h(k())) can't be unified because g != k - f(X, g(X)) and f(g(X), g(h()) can't be unified because of failed occurs check + f(X, g(X)) and f(g(X), g(h()) can't be unified because of + failed occurs check ``` Pattern matching is possible when variables are only used by one of the terms, which then serves as a 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. @@ -106,6 +107,8 @@ Predicates must implement ask/tell protocol. If a predicate is invoked from prod ***Example of ask/tell*** +***Example of failed predicate*** + ### 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”. diff --git a/docs/content/reactor.md b/docs/content/reactor.md index a93e43ba..4491bbf4 100644 --- a/docs/content/reactor.md +++ b/docs/content/reactor.md @@ -7,8 +7,6 @@ weight: 55 # Constraints Reactor -***Details of constraints processing implementation*** - Constraints reactor is a small library written in Kotlin and Java, which implements the extended semantics of constraints processing. Its main features are: - native support for terms and unification @@ -16,23 +14,25 @@ Constraints reactor is a small library written in Kotlin and Java, which impleme - fast lookup of matching production from constraint’s arguments - Rete-like algorithm for finding potential matches -## Implementation notes +### Implementation notes -Unification is implemented according to a “near-constant time” algorithm[^uni]. +Unification is implemented according to a “near-constant time” algorithm[^uni]. Occurs check is done on terms being unified to avoid infinite terms. -A trie[^trie] (a prefix tree) on flattened terms is used for indexing productions by value. +A trie (a prefix tree) on flattened terms[^trie] is used for indexing productions by constraints and their arguments. -Persistent structures used for implementing internal state, which are useful for tracking and restoring the state of the constraints program. +Search for matching productions is implemented with a trie, with each node corresponding to a partially matched production. Each constraint activation or disposal event updates this trie. The leaves correspond to fully matched productions. -## Open questions +Persistent structures used for implementing internal state, which are useful for tracking and restoring the state of constraints program. -### Nested logical variables +### Open questions + +#### Nested logical variables Logical variables serving as constraint arguments trigger reactivation of such constraints on any change, such as value bound or parent changed. Might be a good idea to also trigger reactivation on changed variable contained in a term, which serves as a constraint argument. -### Restoring the state of logical variables +#### Restoring the state of logical variables -One of the extensions supported by this implementation is the *partial rollback*, which allows to declare alternative branches in a production’s body. The implementation is able to restore the state of constraints that is valid for the frame corresponding activation of the body, except for the state of logical variables that may have been changed. This, too, might be worth implementing. +One of the extensions supported by this implementation is the alternative body branches. The state of constraints store that is valid for the stack frame corresponding to triggering a production, before activating body constraints, can be restored, but the state of logical variables is unpredictable. This may lead to unexpected results. [^uni]: Baader, Franz, and Wayne Snyder. "Unification Theory." Handbook of automated reasoning 1 (2001): 445-532. [^trie]: Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier Sci. Pub. B. V., Amsterdam, The Netherlands, The Netherlands. Chapter 26.