Update documentation content (rev. 0.9.0)

docs/_config.yml

@@ -8,7 +8,7 @@ baseurl: "/mps-coderules" # the subpath of your site, e.g. /blog
 url: "https://jetbrains.github.io" # the base hostname & protocol for your site, e.g. http://example.com
 twitter_username: jetbrains_mps
 github_username:  jetbrains
-time: 2021-05-21
+time: 2027-05-21
 revision: 0.9.0
 copyright: JetBrains
 copyright_url: "https://jetbrains.com"

docs/content/allpages.md

@@ -1,10 +1,6 @@
 ---
 layout: print
+title: false
 menu: false
+permalink: :basename
 ---
-
-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.

docs/content/constraintrules.md

@@ -0,0 +1,96 @@
+---
+layout: page
+title: Constraint Rules
+parent: content/language.md
+weight: 210
+permalink: :basename
+---
+
+### Constraint Rules
+
+At the core of CodeRules program lies the concept of *constraint rules*, which captures the essence of logical programming. The structure of a constraint rule enables to express a program as a list of logical clauses, each consisting of the *head* — the list of antecedents, and the *body* — the list of consequences. Both the *head* and the *body* are represented as lists of *constraints* and *predicates*. More on the semantics of *constraint rules* can be found in the section on [constraints processing](processing).
+
+![](img/constraintrules-sample-650.png)  
+_(example of a constraint rule in a rule template)_
+
+A *constraint rule* can be created at any place within a rule template’s body with the help of a keyword `on`. A constraint rule within a loop generates a runtime constraint rule on every iteration of this loop. 
+
+A constraint rule must include either a body or a head, no constraint rule can omit both. 
+
+##### Head
+
+Constraints in a constraint rule’s head can be declared as either *kept* or *replaced*. Replaced constraints are marked with a tilde `~`.
+
+There is a certain limitation as to what *constraints* can be used in rule’s head: it can only contain constraints defined by this rule table, or one of the rule tables it extends.[^headlimit] 
+
+A constraint rule with an empty head, not declaring any constraints to serve as its input, is considered an *automatic* rule and is triggered automatically on start of constraint rules program execution.
+
+##### Guard
+
+The *guard* is optional and may contain only predicates or the `$()` expression which evaluates boolean-typed Java expression.
+
+Predicates, also known otherwise as “built-in constraints” are represented either as binary operators, such as `=` for unification or `==` for equality, or they are boolean-valued functions. Unification or equality if used in guard, only tests that its arguments can be unified, otherwise if called from body, it invokes the actual unification or assigns the value to a logical variable.
+
+There are also predicates that can only be queried, such as `isFree/1` or `isAssigned/1`, testing if a logical variable is free or has value assigned. Such predicates can only be used in guard. 
+
+![](img/constraintrules-guard-500.png)  
+_(example of predicates used in guard)_
+
+##### Body
+
+Constraint rule’s body can contain any visible constraints declared by rule tables located in imported models, as well as *predicates*. 
+
+![](img/language-unify-300.png)  
+_(`unifies` predicate used in the guard and in the body)_
+
+A body may contain two or more *alternative branches*, which essentialy capture the idea of evaluating constraint rules with backtracking. Namely, the evaluation starts with the first branch, and in case it is finished without failures, other branches are not evaluated. On failure the second branch is evaluated, etc.
+
+![](img/constraintrules-alt-500.png)  
+_(example of a constraint rule with alternative branches)_
+
+A body may be created with the help of a *template fragment* — a block of code that produces constraints and macro calls via special *emit* statements: `<%…%>`.
+
+![](img/constraintrules-tpl-600.png)  
+_(example of constraint rule with a body template)_
+
+#### Logical variables
+
+A constraint rule can declare *logical variables*. By default a logical variable ranges over *terms*, although any Java object may serve as a value. A logical variable is used whenever a term or a term feature needs to be represented in a logical clause.
+
+![](img/language-compatibleWith-300.png)  
+_(constraint rule declaring logical variables)_
+
+When a constraint with logical variable as one of its arguments is matched, that variable becomes bound to the corresponding argument of the matching occurrence. The scope of such binding is this constraint rule’s guard and the body.
+
+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 terms.
+
+![](img/constraintrules-bind-700.png)  
+_(example of binding the logical variables)_
+
+This constraint rule is triggered when both locations referred to as `ae.lValue` and `ae.rValue` have their types assigned, as both `typeOf/2` constraints must be present for a match to be successful. Once a constraint rule’s head is matched, both logical variables `LType` and `RType` become bound to whatever was the 2nd argument of corresponding `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.
+  
+#### Pattern matching
+
+There is support for pattern matching, using terms as patterns, which may optionally contain logical variables. For this to work, a logical variable that serves as a constraint argument should have a pattern attached.  
+
+The following example illustrates the use of *pattern matching* in a constraint rule’s head. Here, the first argument to constraint `convertsTo/2` in the head is a logical variable with pattern expression. In this case the constraint rule will only be triggered if the active constraint’s first argument is *bound* (is not a free logical variable), and it matches the pattern.
+
+![](img/language-convertsto-500.png)  
+_(constraint rule with pattern matching)_
+
+#### Evaluation of Java expressions
+
+Arbitrary Java code can be called with `$()` predicate. It accepts either an expression of `boolean` type, in which case it can be used in guard, or expression of any type when called from body. In the latter case, the value expression evaluates is ignored.
+
+![](img/constraintrules-eval-400.png)  
+_(example of using `$()` predicate)_
+
+#### Using macros
+
+In order to make use of macro definitions, which are essentially parameterised 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.
+
+[^headlimit]: This limitation has its origin in the way constraint rules are chosen when an active constraint is being processed. Namely, constraint rules to match an active constraint are selected from the rule table declaring this constraint, and rule tables that are its extensions. The order of constraint rules within the rule table matters, the ones declared on top are matched first. Productions from extending rule tables are prepended to the list of constraint rules of the rule table they extend.

docs/content/contacts.md

@@ -1,18 +0,0 @@
----
-layout: page
-title: Contacts
-menu: Contacts
-weight: 800
----
-
-# Contacts
-
-The project is hosted on [GitHub](https://github.com/fisakov/mps-coderules), latest release can be found [here](https://github.com/fisakov/mps-coderules/releases).
-
-The author can be reached by email `fedor.isakov` (AT) `jetbrains.com` or by [Twitter](https://twitter.com/fisakov).
-
-[JetBrains MPS](https://www.jetbrains.com/mps/) is a project developed by [JetBrains](http://www.jetbrains.com/?fromFooter) and is available via [web](https://www.jetbrains.com/mps/) and [Twitter](http://twitter.com/jetbrains_mps).
-
-## Copyright
-
-All contents is copyright © JetBrains s.r.o. 2018. All rights reserved.

docs/content/evaluating.md

@@ -1,52 +1,59 @@
 ---
 layout: page
-title: Evaluating Code Rules
-weight: 40
+title: Evaluating CodeRules
+weight: 300
+id: evaluating
+permalink: :basename
 ---
 
-# Evaluating Code Rules
+## Evaluating CodeRules
 
-The process of evaluating code rules consists of two stages:
+Analysis of source model with CodeRules can be described as a two-phase process.
 
-1. Collecting handlers and applying rules.
-2. Processing constraint productions collected in the first stage.
+1. Collecting rule tables and applying rule templates.
+2. Processing constraint rules 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.
+In the first phase, languages used by the model being analysed and surveyed for the appropriate CodeRules aspect model, which is `types` in case of type checking.
 
-### Applying rules
+The outcome of this phase is a *constraint rules program*, which is a collection of *rule tables*, which in turn represent lists of *constraint rules*. This “program” however, exists in memory only as it does not have any textual representation.
 
-The first stage of evaluating code rules begins with collecting handlers. Handlers are collected from corresponding aspects of all languages imported into the model. In addition to that, all extended languages are also included into the scope.
+In the second phase the constraints program that was created in phase one is evaluated. Evaluation starts with a query, which serves as an entry point to the program. 
 
-All handlers collected in the previous step are sorted, so that the ones coming from extensions appear earlier. This sorting order ensures that when productions are selected to match an active constraint, the productions coming from extensions will have higher priority.
+Queries correspond to usual procedures that analyse the source mode, such as `typeOf` or `convertsTo`, and are declared in the same aspect model.
 
-After the relevant handlers are collected, the source model is traversed from the specified location, and the applicable rules are evaluated. As rules are applied, they produce constraint productions. As well as generating constraint productions, the rules are allowed to report messages to be displayed at source locations.
+![](img/overview-typeofq-550.png)  
+_(example of a query)_
 
-Generated constraint productions constitute the constraints program, which is then executed in the next stage.
+#### Applying rule templates
 
-### Executing constraints program
+The first stage of evaluating CodeRules program begins with collecting rule tables. Rule tables are collected from corresponding aspects of all languages imported into the model. In addition to that, all extended languages are also included into the scope.
+
+All rule tables collected in the previous step are sorted, so that the ones coming from extensions appear earlier. This sorting order ensures that when constraint rules are selected to match an active constraint, the constraint rules coming from extensions will have higher priority.
+
+After the relevant rule tables are collected, the source model is traversed from the specified location, and the applicable rules are evaluated. As rule templates are applied, they produce constraint rules. As well as generating constraint rules, the rule templates are allowed to report messages to be displayed at source locations.
+
+Generated constraint rules constitute the constraints program, which is then executed in the next stage.
+
+#### Executing constraints program
 
 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 (internally 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 constraint rule, which is triggered unconditionally.
 
-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 constraint rules are fired on start of program execution. First, all “on start” constraint rules are triggered. All constraints activated by these constraint rules are processed normally, and after there are no more constraint rules to be triggered, the query is fired.
 
-Order of productions fired:
-1. “on start” productions
-2. query production
+Order of constraint rules fired:
 
-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.
+1. “on start” rules
+2. query
 
-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.
-
-![](img/eval-settype-650.png)  
-_(example showing type assigned from a 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 a constraint rule.
 
 Failures may be encountered during constraints program execution, such as a unification failure, and they are caught with the help of alternative body branches, when 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.
 
-![](img/eval-altbody-650.png)  
+![](img/eval-alt-350.png)  
 _(example of using an alternative body branch)_
 
 ### User interface
@@ -63,7 +70,7 @@ During execution of a constraints program all activation/suspension/deactivation
 ![](img/eval-proof-350.png)  
 _(sample proof in propositional logic)_
 
-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.
+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 constraint rule 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.
 
 ![](img/eval-atrace-snapshot.png)  
 _(activation trace view)_

docs/content/example-controlflow.md

@@ -1,9 +1,8 @@
 ---
 layout: page
 title: Control Flow Analysis of BaseLanguage
-menu: Control Flow BL
-parent: examples
-weight: 520
+menu: false
+permalink: :basename
 ---
 
 # Control Flow Analysis

docs/content/example-lambdacalc-ext.md

@@ -5,9 +5,10 @@ menu: Typechecking STLC
 parent: examples
 weight: 550
 github-path: /tree/master/samples/lambdacalc
+permalink: :basename
 ---
 
-# Typechecking Extended STLC
+## Typechecking Extended STLC
 
 Simply Typed Lambda Calculus (STLC) is a famous example favored by textbook authors.
 This sample demonstrates how a classical type checking algorithm (Hindley-Milner[^hm]) designed for this language can be implemented using Code Rules.

docs/content/example-logic.md

@@ -5,11 +5,12 @@ menu: Fitch Proofs
 parent: examples
 weight: 560
 github-path: /tree/master/samples/fitch
+permalink: :basename
 ---
 
-# Fitch Proof Validation
+## Fitch Proof Validation
 
-This example demonstrates the use of *code rules* to implement validation of logical proofs written using Fitch system. The idea of this implementation originates in the proof checking tool provided as part of an inroductory course on logic by Stanford University[^inlog]. This overview serves for quick introduction, and more detailed information can be found at project’s home page (see the link on top of this page).
+This example demonstrates the use of *CodeRules* to implement validation of logical proofs written using Fitch system. The idea of this implementation originates in the proof checking tool provided as part of an inroductory course on logic by Stanford University[^inlog]. This overview serves for quick introduction, and more detailed information can be found at project’s home page (see the link on top of this page).
 
 The four languages in this example define the structure of proofs (samples.fitch), the structure of three kinds of logic: Propositional logic, Herbrand logic, and First Order logic (samples.fitch.*logic).
 

docs/content/example-typechecking.md

@@ -5,11 +5,12 @@ menu: Typechecking BL
 parent: examples
 weight: 510
 github-path: /tree/master/samples/mpscore
+permalink: :basename
 ---
 
-# Typechecking BaseLanguage
+## Typechecking BaseLanguage
 
-Short explanation of the architecture of BL-specific type system built with *code rules*.
+Short introduction to the architecture of BL-specific type system built with *CodeRules*.
 
 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.
 

docs/content/incremental.md

@@ -1,7 +1,7 @@
 ---
 layout: page
 title: Incremental Algorithm
-weight: 80
+menu: false
 ---
 
 # Incremental Algorithm

docs/content/index.md

@@ -0,0 +1,80 @@
+---
+title: About
+menu: About
+weight: 1
+layout: page
+permalink: :basename
+---
+                                          
+## MPS CodeRules
+
+Type inference and type checking is a problematic area for language authors  — users of [JetBrains MPS](https://jetbrains.com/mps), because of inherent intricacies of the problem itself and sometimes less than adequate support from the framework.
+
+*CodeRules* is a new technology that brings logic programming in the form of constraints processing as a vehicle for implementing type inference.
+
+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.
+
+![](img/intro-assignment-550.png)  
+_(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.  
+
+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.
+
+![](img/intro-methodcall-550.png)  
+_(example of processing method arguments)_
+
+Code rules may have a solution to these and other issues. The core idea is to employ a **constraints processing system** to process facts and relations, collectively known as constraints, with the user being in full control of what constraint rules to generate for given source model. With **logical variables** representing unknowns, and with support for **pattern matching** making use of term algebra and unification, it should be straightforward to define the core of type inference or a similar framework without having to rely on opaque implementation and pre-defined relations.
+
+To illustrate the idea, let’s look at a couple of examples. These are taken from the type system implementation for BaseLanguage.
+
+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.
+
+![](img/intro-assign-700.png)  
+_(type checking assignment with constraint rules)_
+
+Instead of waiting until a type has been finalised in order to access its structure, *pattern matching* is used to trigger constraint rules only on types of certain form. The example below shows how `convertsTo/2` is resolved for an instance of `LowerBoundType`.
+
+![](img/intro-convertslbt-550.png)  
+_(resolution of `convertsTo/2` constraint using pattern matching)_
+
+### Features 
+
+ - A language for constructing rule templates that are applied to source model and may include constraint rules. The rules may be concept-specific or standalone.
+
+ - *Constraint Processing System* — an extension of CHR[^chr] semantics allowing the use of unification in a constraint rule’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. 
+
+ - A framework for executing a constraint rules program, with support for error reporting from rules’s body. The UI also includes a tracing tool for providing insights into how constraints are processed.
+
+Examples are provided that demonstrate the use of this technology for type checking.
+
+    
+### Table of contents
+
+This documentation site is organized as follows:          
+
+- [CodeRules Language](language) discusses the language features
+- [Evaluating CodeRules Program](evaluating) explains the internals of CodeRules
+- Examples include the following:
+  - [Typechecking BaseLanguage](example-typechecking)
+  - [Typechecking lambda calculus with extensions](example-lambdacalc-ext)
+  - [Formal logic — Fitch proofs](example-logic)
+
+- All documentation on [single page](allpages)
+
+### Contacts
+
+The project is hosted on [GitHub](https://github.com/jetbrains/mps-coderules), latest builds can be found [here](https://teamcity.jetbrains.com/viewType.html?buildTypeId=MPS_20211_Distribution_MpsCodeRules).
+
+The author can be reached by email `fedor.isakov`@`jetbrains.com` or on [Twitter](https://twitter.com/fisakov).
+
+[JetBrains MPS](https://www.jetbrains.com/mps/) is a project developed by [JetBrains](http://www.jetbrains.com/?fromFooter) and is available via [web](https://www.jetbrains.com/mps/) and [Twitter](http://twitter.com/jetbrains_mps)
+
+#### Copyright
+
+All contents is copyright © JetBrains 2021. All rights reserved.
+
+
+[^chr]: Constraint Handling Rules [http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/constraint-handling-rules-book.html](http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/constraint-handling-rules-book.html)

docs/content/intro.md

@@ -1,53 +0,0 @@
----
-layout: page
-title: Introduction
-weight: 10
----
-
-# Introduction
-
-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.
-
-![](img/intro-assignment-550.png)  
-_(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.  
-
-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.
-
-![](img/intro-methodcall-550.png)  
-_(example of processing method arguments)_
-
-Code rules may have a solution to these and other issues. The core idea is to employ a **production system** to process facts and relations, collectively known as constraints, with the user being in full control of what productions to generate for given source code (model). With **logical variables** representing unknowns, and with support for **pattern matching** making use of term algebra and unification, it is pretty straightforward to define the core of type inference or a similar framework without having to rely on opaque implementation and pre-defined relations.
-
-To illustrate the idea, let’s look at a couple of examples. These are taken from the type system implementation for BaseLanguage.
-
-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.
-
-![](img/intro-assignprod-700.png)  
-_(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`.
-
-![](img/intro-converts-550.png)  
-_(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. 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.
-
- - A framework for executing a constraints program, with support for error reporting from production’s body, as well as a façade interface for accessing the results of a constraints program execution. The UI also includes a tracing tool for providing insights into how constraints are processed.
-
- - Finally, an embedded engine capable of processing constraints, which accepts a list of productions sorted by handler, an initial active constraint, and, optionally, a store of inactive constraints, and yields an updated store after all matched productions have been fired.
-
-Examples are provided that demonstrate the use of this technology for type checking and other analyses.
-
-
-[^mps]: Meta Programming System [https://jetbrains.com/mps](https://jetbrains.com/mps)
-[^chr]: Constraint Handling Rules [http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/constraint-handling-rules-book.html](http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/constraint-handling-rules-book.html)

docs/content/language.md

@@ -1,167 +1,50 @@
 ---
 layout: page
-title: Code Rules Language
-weight: 30
+title: CodeRules Language
+weight: 200
+id: language
+permalink: :basename
 ---
 
-# Code Rules Language
+## CodeRules Language
+
+The language `jetbrains.mps.lang.coderules` defines the core concepts listed below.
+
+#### Constraint rules
+
+[Constraint rules](constraintrules) are the basic constructs that enable the use of logic programming with constraints and predicates combined into logical clauses.
+
+#### Rule templates
+
+Defined in a [rule table](ruletable) root, these are the fundamental building blocks of CodeRules program. These are either static or concept-specific rules that get applied to appropriate nodes in the source model and are able to use the constraint rules to implement their logic.
+
+#### Macros
+
+Macros extend the expressiveness of constraint rules with the ability to refactor away fragments of a rule’s body. Macros are provided by [macro table](macrotable).
+
+#### Queries
+
+With help of [queries](querytable) one builds integration of CodeRules into the language aspect. Typechecking aspect provides query kinds that correspond to actual use cases implemented by type checker. 
+
+#### Terms
+
+One important feature of CodeRules is the ability to abstract away from type structure defined by the language. For example, one may decide to represent all primitive types of BaseLanguage as a term `primitive(kind=<specific kind>)`. 
+
+[Term table](termtable) contains declarations of *terms* which are used as internal representation of types.
+
+***Lists***
 
 ### Language Aspect
 
-Code rules are defined in handlers, which are root concepts of language `jetbrains.mps.lang.coderules`. Handlers and other related roots should be created in a language’s aspect model corresponding to a specific kind of analysis. For example, language `jetbrains.mps.lang.typechecking` declares the aspect `types`.
+Code rules are defined in tables, which are root concepts of language `jetbrains.mps.lang.coderules`. Rule tables and other related roots should be created in a language’s aspect model corresponding to the specific kind of analysis performed. The language `jetbrains.mps.lang.typechecking` declares the aspect `types`.
 
-![](img/language-aspect-400.png)  
-_(definition of aspect `types`)_
+### Root concepts
 
-#### Root concepts
-
-The following table contains root concepts that belong to code rules definition.
+The following table contains root concepts that belong to CodeRules language structure.
 
 | Concept         | Description |
 |:-- |:-- |
-| *Handler*     | contains rules and constraint declarations |
-| *Query*       | entry point to the constraints program |
-| *MacroTable*  | defines how terms are constructed |
-| *DataFormTable* [^dft]  | defines terms, the data structure that is used in unification |
-
-### Handler
-
-*Handler* serves two purposes: it declares the *constraints* that it processes, and it  also declares *rules*, which are, simply put, procedures applicable to specific concept and (optionally) its subconcepts. 
-
-Constraints declared by a handler are public symbols that serve as its API in the following sense. In *head* of productions of a handler and its extensions only those constraints can be used, that were declared in this handler or any handler it extends. On the other hand, any constraints can be used in *body*, provided the references to constraint declarations are resolved in the usual way.
-
-#### Rules
-
-The aim of rules defined by handlers is to 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).
-
-![](img/language-writelocal-750.png)  
-_(example of rule with production template)_
-
-A handler is a concept in language `jetbrains.mps.lang.coderules`.
-
-![](img/language-handlerhead-300.png)  
-_(example of a handler declaration — without contents)_
-
-Keyword `extends` allows to specify another handler that is to be extended. All constraint productions generated by rules in this handler will have higher priority. This enables to override the original handler’s behaviour.
-
-Only declared constraints are allowed to be used in the heads of productions in rules of this handler or its extensions. Handler should declare one or more constraints, unless it only uses the constraints from handlers which it extends. Constraint declaration consists of name and *arity*, which together constitute a *constraint symbol*. Constraint’s arity is fixed.
-
-An applicability condition, if specified, is checked before applying the rule.
-
-![](img/language-vardecl-600.png)  
-_(example of rule matching concept instances with condition block)_
-
-Rules can specify applicable concept, either exactly or including its subconcepts. One can also declare *standalone* rules, which are applied automatically on every evaluation of code rules.
-
-![](img/language-hasbound-550.png)  
-_(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 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.
-
-![](img/language-recoverct-700.png)  
-_(example of using `require` statement)_
-
-This feature may come in handy for implementing a “partial” type checking. Type checking may be launched either for a whole root, processing all AST tree recursively, in which case it is called called a “total” type checking, or it can be launched for a particular AST node in isolation, and this is then a “partial” type checking. In the latter case, there must be additional information provided by the type system author, which should serve to establish the necessary context by means of following the required dependencies. These may be method and class declarations, for example, if we are to check the type of a particular method parameter. 
-
-#### Production templates
-
-Constraint productions are discussed in details in the section on Constraint Processing System, and here we briefly enumerate the main concepts and their usage. 
-
-*Productions* can be created at any place within a rule’s body, which amounts to creating a production *template*. This means, a production within a loop generates a runtime constraint production on every iteration of this loop. 
-
-A production template has three parts called *head*, *guard*, and *body*. Their meanings correspond precisely to those defined for the constraint productions. 
-
-There is a certain limitation as to what *constraints* can be used in head: it can only contain constraints defined by this handler, or one of the handlers it extends. This limitation has its origin in the way productions are chosen when an active constraint is being processed. Namely, productions to match an active constraint are selected from the handler declaring this constraint, and handlers that are its extensions. The order of productions within the handler matters, the ones declared on top are matched first. Productions from extending handlers are prepended to the list of productions of the handler they extend.
-
-Production’s body can contain any visible constraints declared by handlers located in imported models, as well as *predicates*. A production must include either a body or a head, no production can omit both. Guard is optional, and it can only contain predicates.
-
-A production with an empty head, not declaring any constraints to serve as its input, is considered an *automatic* production and is triggered automatically on start of constraints program execution.
-
-Constraints in a production’s head can be declared as either *kept* or *replaced*. Replaced constraints are marked with a tilde `~`.
-
-Predicates, also known otherwise as “built-in constraints”, are represented either as binary operators, such as `=` for unification or `==` for equality, or they are boolean-valued functions. Unification or equality if used in guard, only tests that its arguments can be unified, otherwise if called from body, it invokes the actual unification or assigns the value to a logical variable.
-
-![](img/language-unify-300.png)  
-_(`unifies` predicate used in the guard and in the body)_
-
-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. Such predicates can only be used in guard. 
-
-Arbitrary Java code can be called with `eval/1` predicate. It accepts either an expression of `boolean` type, in which case it can be used in guard, or expression of any type when called from body. In the latter case the value expression evaluates to is ignored.
-
-![](img/language-recover-500.png)  
-_(example of using `eval/1` predicate)_
-
-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.
-
-![](img/language-compatibleWith-300.png)  
-_(production declaring logical variables)_
-
-When a constraint with logical variable as one of its arguments is matched, that variable becomes bound to the corresponding argument of the matching occurrence. The scope of such binding is this production’s guard and body.
-
-There is support for pattern matching, using terms as patterns, which may optionally contain logical variables. For this to work, a logical variable that serves as a constraint argument should have a pattern attached.  
-
-![](img/language-convertsto-500.png)  
-_(production with pattern matching)_
-
-Everywhere locations in the source code (model) must be referenced, node references are used, which are introduced with the `@` symbol. This is a shortcut for accessing a reference to a node, which is a regular POJO.
-
-![](img/language-typeof-550.png)  
-_(example of constraint argument referring to a model location)_
-
-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***
-
-***Substitution — passing parameters via context***
-
-***Template fragments within production template body***
-
-***Alternative body***
-
-#### Query
-
-Query is the entry point to a constraints program. The only purpose of a query is to activate constraints that trigger computation implemented by constraint productions.
-
-![](img/language-query-350.png)  
-_(example of a query)_
-
-A query is discovered by the API through its *kind*, which is specific to the language aspect. Query kind specifies parameters that can be passed to it. The body of a query can contain same constraints and predicates as regular constraints production.
-
-#### Macro table
-
-Macros allow to have parameterised constructors for terms. They can either create terms using nodes coming from the source model, or use the parameters to fill in values. By contrast with rules, macros are always explicitly invoked.
-
-This feature may come in handy when data types used by the constraints program are complicated and include many levels of containment. For example, type checking with *code rules* relies on types being terms, which means types can contain other types.
-
-Macros are defined in a root `Macro table`. Its contents is made of *macro definitions*.
-
-![](img/language-macro-500.png)  
-_(macro definition in a macro table)_
-
-Macro *expands* instances of specified concept. This means a macro can be invoked on an instance of this concept. In case macro is *expanded*, its parameters are automatically initialised to appropriate values. Otherwise, a macro can be directly *called* with parameters specified explicitly.
-
-***Expand/call from production body***
-
-- Macro body is a template, with every constraint or predicate produced from template fragments being inserted into the production body at the invocation site. There is a special logical variable available within macro body, `macroLogical`, which captures the logical variable on the left side of `expand` or `call` predicate.
-
-***Substitutions***
-
-#### DataForm table
-
-DataForm table contains *dataform* declarations, a.k.a. *terms*. A term is a simple recursive data type that is suitable for implementing unification. Also, terms can model any other data structure, in particular they are suitable for representing types in a programming language.
-
-Dataform is defined by its symbol and its features, which can be a POJO, a child dataform, or a list of dataforms. A feature may have a default value provider. A dataform extending another dataform adds new features or provides default values for existing ones.
-
-![](img/language-classifiertype-300.png)  
-_(example of a dataform definition for classifier type)_
-
-![](img/language-longtype-350.png)  
-_(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
+| [*Rule Table*](ruletable)     | contains rules and constraint declarations |
+| [*Term Table*](termtable)  | defines terms, the data structure that is used in unification |
+| [*Macro Table*](macrotable)  | facilitates the reuse of body template fragments |
+| [*Query Table*](querytable)  | collection of entry points to the constraints program |

docs/content/macrotable.md

@@ -0,0 +1,47 @@
+---
+layout: page
+title: Macro Table
+parent: language
+weight: 240
+permalink: :basename
+---
+
+### Macro table
+
+The motivation behind using macros, and — in a wider context — behind using terms as datatype, is that sometimes it takes more than just an SNode to represent a type. For example, in order to find a solution for a type inference problem, a logical variable representing the inference variable requires a bound, implemented is a constraint on that variable. In other situations, a newly constructed type has to substitute type variables with some other types. It is only convenient to extract such functionality into a separate, reusable fragment.
+
+The two kinds of macros — `expand` and `call` — are provided to refactor portions of constraint rule templates by introducing reusable fragments. Both kinds of macros are only available in *body* part of constraint rule templates. 
+
+#### Expand macro
+
+Expand macro has access to SNode instance on which it was invoked, can access the optional parameters, and either use or assign the logical variables. By contrast with rules, expand macros are always explicitly invoked.
+
+Expand macro declaration must define the applicable concept. It may also contain one or several parameters, which are optionally provided at the usage site and are made available to instances of the macro.
+ 
+ ![](img/macro-expand-550.png)  
+ _(example of an expand macro declaration)_
+ 
+Logical variables declared in angle brackets right after the name of the macro are used to pass IN and OUT parameters. In addition, a macro can define its own logical variables.
+ 
+A specific expand macro is always applicable to SNode instances of particular concept that must extend the concept in the macro declaration, which it refers.
+ 
+Expand macro can be applied recursively to provide more fine-grained reusability. 
+ 
+![](img/macro-recursive-600.png)  
+_(example of a recursive expand macro)_
+
+***Substitution — passing parameters via context***
+
+#### Call macro
+
+A call macro can be most simply described as a method accepting one or several parameters and a list of logical variables. A call macro can be invoked from a constraint rule’s body, as well as from an expand macro or another call macro. 
+
+![](img/macro-call-550.png)  
+_(example of a call macro declaration)_
+
+#### Macro table extensibility
+
+A macro table is able to extend other macro table in order to provide definitions of *expand* macros.
+
+![](img/macro-table-extends-550.png)  
+_(example of a macro table that extends another macro table)_

docs/content/operation.md

@@ -1,14 +1,14 @@
 ---
 layout: page
-title: Reactor Operation
-parent: content/processing.md
-weight: 56
+title: Operation of Constraints Processing System
+menu: false
 ---
-# Reactor Operation
+
+## Operation of Constraints Processing
 
 This section provides an in-depth look into the inner operations of constraints processing. 
 
-## Definitions
+#### Definitions
 
 Program is defined as an ordered set of rules $P = \lbrace r_n \rbrace$. Every rule is defined as a tuple $\langle H^+, H^-, G, B \rangle$, with $H^+$ and $H^-$ corresponding to kept and discarded parts of rule’s head, respectively; $G$ is a conjunction of predicates constituting rule’s guard; $B$ being a conjunction of constraints and predicates defined in rule’s body.
 
@@ -30,7 +30,7 @@ At every moment a state of program evaluation is described by a tuple $S = \lang
 
 State transitions are functions that make modifications to one or several features of a state and produce a new state: $T(S) = S^\prime= S[O \mapsto O^\prime, K \mapsto K^\prime, V_a \mapsto {V_a}^\prime]$
 
-## Basic operations
+#### Basic operations
 
 The operations necessary for transitioning between states are described in terms of following procedures: $\mathtt{ask}$, $\mathtt{tell}$, $\mathtt{new}$, and $\mathtt{findMatch}$. The former two concern only predicates — $\mathtt{ask}$ inquires if the predicate is satisfied, whereas $\mathtt{tell}$ asserts the predicate. In case $\mathtt{tell}$ invokes a non-satisfiable predicate, such as $\mathtt{false}$, an exception is raised. 
 
@@ -50,7 +50,7 @@ The process just described is repeated with active occurrence $c^\star$ as long
 
 As mentioned above, unification predicate can have a side effect which alters the state of some logical variable(s) $x \in V_a$. As all constraint occurrences are observers of their arguments, a change in logical variable’s state causes all alive occurrences that have it as one of their arguments to be re-activated. A re-activated occurrence is processed immediately, exactly as if it has been newly introduced. 
 
-### Summary of findMatch 
+#### Summary of findMatch 
 
 We provide here a compact representation of $\mathtt{findMatch}$ procedure in pseudo-code that combines everything that has been said before. 
 
@@ -126,17 +126,17 @@ c^\star \text{ is discarded} \\\
 \text{end}\\\
 \end{array}$$
 
-## Extended operations
+#### Extended operations
 
-### Alternative body branches
+#### Alternative body branches
 
 ***Alternative body branches***
 
-### Disjunctions in rule’s body
+#### Disjunctions in rule’s body
 
 ***Disjunction-semantics***
 
-### Incremental program evaluation
+#### Incremental program evaluation
 
 ***Incremental evaluation***
 

docs/content/overview.md

@@ -1,52 +0,0 @@
----
-layout: page
-title: Overview
-weight: 20
----
-
-# Overview
-
-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. 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.
-
-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.
-
-![](img/overview-convertsto-500.png)  
-_(example of a query)_
-
-In the above example, the query defines two logical variables (A and B) of type `term`, which serve to represent types internally. First, both query parameters `to` and `from` are *expanded*, meaning that their `SNode` representations are converted to terms, and then constraint `convertsTo(A, B)` is activated, kicking off the processing of constraints, which is the essence of constraints program execution. In case productions triggered by `convertsTo/2` constraint all evaluate to true, the query is deemed successful, and if there is at least one production that evaluates to false, the query fails accordingly.
-
-One nice feature of using code rules is the ability to abstract away from type structure defined by the language. For example, one may decide to represent all primitive types of BaseLanguage as a term `primitive(kind=<specific kind>)`. Terms can also incorporate values as regular Java objects, so creating an inference rule which checks if a particular constant fits the given type, be it an `int` or a `char`, is trivial.  
-
-Having an internal representation for types also means, that if type system is required to represent types as instances of `SNode` to the user, this has to be addressed by the query design. For instance, a type checking query may consist of two constraint activations:
-
-![](img/overview-check-300.png)  
-_(example of a query production)_
-
-Here, the first constraint `checkAll/0` fires type checking, whereas the second `recoverAll/0` is responsible for restoring types to `SNode` instances and assigning them to the source model locations. Joining the two constraints with a conjunction establishes the order in which these are evaluated.
-
-An of course, if something can go wrong, it will. In case type inference is unsuccessful, the second part of the query has no chance of being executed. To account for that, a feature was added to the language of constraint productions, which helps recover from certain failures.
-
-![](img/overview-check2-300.png)  
-_(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.
-
-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.
-
-![](img/overview-assignment-700.png)  
-_(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.
-
-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.
-
-![](img/overview-converts-500.png)  
-_(example of rule with production)_

docs/content/processing.md

@@ -1,11 +1,12 @@
 ---
 layout: page
 title: Constraints Processing System
-menu: Processing Constraints
-weight: 50
+weight: 400
+parent: evaluating
+permalink: :basename
 ---
 
-# Constraints Processing System
+## Constraints Processing System
 
 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.
 
@@ -88,11 +89,11 @@ A term variable can also be a logical variable, so that when two terms are unifi
 
 Constraints are, simply put, tuples with fixed arity and a symbol attached. In some respects constraints correspond to rows in a database table. Logically they can be understood as facts, relations, or propositions. An argument to a constraint can be a term, a logical variable, or any POJO, except another constraint.
 
-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.
+Constraints are activated from a constraint rule’s body and stay active until there are no possible matches with any of constraint rule’s heads. If a constraint is not discarded by a constraint rule, 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 constraint rule’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 constraint rule, which declares one or more of constraints in its head to be “replaced”, causes these to be terminated.
 
 ![](img/constraint-lifecycle.svg)  
 _(lifecycle of a constraint)_
@@ -101,7 +102,7 @@ _(lifecycle of a constraint)_
 
 Whereas a constraint serves to embody a fact or a relation among objects simply by being a witness of such a fact or a relation, a *predicate*[^pred] helps to establish a fact or a relation, or check if one exists, by means of executing a procedure. Same is true for facts and propositions.
 
-Predicates must implement ask/tell protocol. If a predicate is invoked from production’s guard clause, it represents a query (ask), and if it is invoked from the body, it is an assertion (tell).
+Predicates must implement ask/tell protocol. If a predicate is invoked from constraint rule’s guard clause, it represents a query (ask), and if it is invoked from the body, it is an assertion (tell).
 
 ***Example of a predicate***
 
@@ -109,17 +110,17 @@ Predicates must implement ask/tell protocol. If a predicate is invoked from prod
 
 ***Example of failed predicate***
 
-### Constraint productions
+### Constraint rules
 
-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 constraint rules. Each rule has three parts: the part that is responsible for triggering the constraint rule, called “head”, the part that checks for pre-conditions, called “guard”, and the part that is evaluated when constraint rule is fired, which is called “body”.
 
 #### 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 a constraint rule 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 constraint rule 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.
+A constraint rule is triggered when there are constraint occurrences matching all constraints specified in constraint rule’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.
+There is some terminology inherited from CHR that can be useful when discussing the kinds of constraint rules. In the following table `E` and `E'` are the set of constraints in constraint rule’s head, `C` is a conjunction of predicates serving as guard, and `G` is a conjunction of predicates and constraints in constraint rule’s body.
 
 | “kept” set `E` | “replaced” set `E’` | Notation | Designation |
 |:--|:--|:--:|:--|
@@ -127,33 +128,33 @@ There is some terminology inherited from CHR that can be useful when discussing
 | 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 constraint rule 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 constraint rule, an “auto” constraint rule with an empty head. As the name implies, such constraint rule is triggered automatically on start of constraints program execution.
 
 #### Guard
 
-Guard is a conjunction of predicates, which are checked before a production is fired. Predicates in a guard are *queried*.
+Guard is a conjunction of predicates, which are checked before a constraint rule is fired. Predicates in a guard are *queried*.
 
 #### Body
 
-Body is a conjunction of predicates and constraint activations. When triggered, each body clause is evaluated in order, with predicates serving as *assertions* and constraint activations producing new constraints. Each newly activated constraint is checked against any productions that can be fired, and so on.
+Body is a conjunction of predicates and constraint activations. When triggered, each body clause is evaluated in order, with predicates serving as *assertions* and constraint activations producing new constraints. Each newly activated constraint is checked against any constraint rules that can be fired, and so on.
 
-### Triggering a production
+### Triggering a constraint rule
 
 The procedure `processActive()` accepts a constraint occurrence that has been activated and proceeds as follows until this constraint is either discarded or suspended (moved to store). This procedure calls itself recursively on every constraint activation, so there might be many active constraints at any given moment, organised into a stack, which matches exactly the call stack of `processActive()`. 
 
-First, the procedure searches for “relevant” productions that declare a constraint in their heads matching the active constraint occurrence currently being processed. These productions form a FIFO queue, corresponding to the order of productions within a handler.
+First, the procedure searches for “relevant” constraint rules that declare a constraint in their heads matching the active constraint occurrence currently being processed. These constraint rules form a FIFO queue, corresponding to the order of constraint rules within a rule table.
 
-For each “relevant” production, which at least partially matches the currently active constraint occurrence, the vacant slots in production’s head are filled with matching constraints from the store, which were previously suspended. Once a full match with production’s head is established, the guard is checked.
+For each “relevant” constraint rule, which at least partially matches the currently active constraint occurrence, the vacant slots in constraint rule’s head are filled with matching constraints from the store, which were previously suspended. Once a full match with constraint rule’s head is established, the guard is checked.
 
-A production together with a set of constraints matching the ones declared by its head, one of which must be the active constraint, is considered to have been triggered after the guard check returns true. Otherwise this production is skipped. 
+A constraint rule together with a set of constraints matching the ones declared by its head, one of which must be the active constraint, is considered to have been triggered after the guard check returns true. Otherwise this constraint rule is skipped. 
 
-After a production is triggered, first the constraints marked by production’s head as *replaced* are deactivated, and the logical variables defined by patterns are assigned appropriate values by asserting equality through *equals* predicate. Then the constraints and predicates defined in production’s body are activated one-by-one. Every activation of a constraint is a recursive call to `processActive()`. 
+After a constraint rule is triggered, first the constraints marked by constraint rule’s head as *replaced* are deactivated, and the logical variables defined by patterns are assigned appropriate values by asserting equality through *equals* predicate. Then the constraints and predicates defined in constraint rule’s body are activated one-by-one. Every activation of a constraint is a recursive call to `processActive()`. 
 
-If after having processed all items in production’s body the constraint occurrence currently being processed is still “alive”, meaning it has not being discarded during one of the recursive calls to this procedure, the process of matching and triggering productions continues with the next production from the queue.
+If after having processed all items in constraint rule’s body the constraint occurrence currently being processed is still “alive”, meaning it has not being discarded during one of the recursive calls to this procedure, the process of matching and triggering constraint rules continues with the next constraint rule from the queue.
 
-When there are no more productions that can be matched, or the active constraint has been discarded, the procedure `processActive()` finishes. If, when the procedure is finished the active constraint is still “alive”, it is suspended and moved to the store. 
+When there are no more constraint rules that can be matched, or the active constraint has been discarded, the procedure `processActive()` finishes. If, when the procedure is finished the active constraint is still “alive”, it is suspended and moved to the store. 
 
 ***Alternative body***
 
@@ -166,20 +167,20 @@ gcd(0) <=> true
 gcd(N) \ gcd(M) <=> 0 < N, N =< M | gcd(M - N)
 ```
 
-To illustrate the idea of using *stored* constraints to fill vacant slots when matching a production, let’s see what happens when this program is evaluated with 4 and 6 as arguments to `gcd/1` constraint. 
+To illustrate the idea of using *stored* constraints to fill vacant slots when matching a constraint rule, let’s see what happens when this program is evaluated with 4 and 6 as arguments to `gcd/1` constraint. 
 
 | Constraints store | Active constraint | Match | Result |
 |:--|:--|:--|:--|
-| `{}` | `gcd(4)` | no productions matched | suspend `gcd(4)` |
+| `{}` | `gcd(4)` | no constraint rules matched | suspend `gcd(4)` |
 
-On activating `gcd(4)` there are no matching productions, so the constraint is suspended.
+On activating `gcd(4)` there are no matching constraint rules, so the constraint is suspended.
 
 | Constraints store | Active constraint | Match | Result |
 |:--|:--|:--|:--|
 | `{gcd(4)}` | `gcd(6)` | `gcd(6) \ gcd(4)` | guard condition fails |
 | `{gcd(4)}` | `gcd(6)` | `gcd(4) \ gcd(6)` | discard `gcd(6)`, activate `gcd(2)` |
 
-Notice how both combinations of `gcd(4)` and `gcd(6)` constraints are tested. In general, if there are $n$ usages of constraint `foo` in a given production’s head, there will be $n!$ potential matches to be evaluated, so that all permutations are covered.   
+Notice how both combinations of `gcd(4)` and `gcd(6)` constraints are tested. In general, if there are $n$ usages of constraint `foo` in a given constraint rule’s head, there will be $n!$ potential matches to be evaluated, so that all permutations are covered.   
 
 The last activation above is a recursive call to `processActive()`, so the cycle repeats. The active constraint has been deactivated, but contents of the store is unchanged.
 
@@ -188,32 +189,32 @@ The last activation above is a recursive call to `processActive()`, so the cycle
 | `{gcd(4)}` | `gcd(2)` | `gcd(2) \ gcd(4)` | discard `gcd(4)`, activate `gcd(0)` |
 | `{}` | `gcd(0)` | `gcd(0)` | discard `gcd(0)` |
 
-There are no more productions to match for `gcd(2)` as the active constraint, so it is suspended. But the constraint `gcd(6)` has been already discarded, so there are no more active constraints and the process stops. Here is the full trace of this program execution. 
+There are no more constraint rules to match for `gcd(2)` as the active constraint, so it is suspended. But the constraint `gcd(6)` has been already discarded, so there are no more active constraints and the process stops. Here is the full trace of this program execution. 
 
 | Constraints store | Active constraint | Match | Result |
 |:--|:--|:--|:--|
-| `{}` | `gcd(4)` | no productions matched | suspend `gcd(4)` |
+| `{}` | `gcd(4)` | no constraint rules matched | suspend `gcd(4)` |
 | `{gcd(4)}` | `gcd(6)` | `gcd(6) \ gcd(4)` | guard condition fails |
 | `{gcd(4)}` | `gcd(6)` | `gcd(4) \ gcd(6)` | discard `gcd(6)`, activate `gcd(2)` |
 | `{gcd(4)}` | `gcd(2)` | `gcd(2) \ gcd(4)` | discard `gcd(4)`, activate `gcd(0)` |
 | `{}` | `gcd(0)` | `gcd(0)` | discard `gcd(0)` |
-| `{}` | `gcd(2)` | no productions matched | suspend `gcd(2)` |
+| `{}` | `gcd(2)` | no constraint rules matched | suspend `gcd(2)` |
 
 After the program has finished, the constraint store consists of only one constraint `gcd(2)`, which is the *GCD* of 4 and 6.
 
-## Semantics of constraints program
+## Semantics of a constraint rules program
 
 The paper by Betz and Frühwirth[^lls] gives an excellent treatise on semantics of CHR using *linear logic*. Since this 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.
 
-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.
+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 constraint rule’s left-hand side, we can find such substitution $\sigma$, such that we can now assume the set of constraints produced from constraint rule’s body: $\sigma G$. All free variables in this proposition are universally quantified and the proposition itself can be reused infinitely.
 
 \\[  (E \Leftrightarrow C | G)^L :=
          !\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 constraint rule, 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

docs/content/querytable.md

@@ -0,0 +1,19 @@
+---
+layout: page
+title: Query Table
+parent: language
+weight: 250
+permalink: :basename
+---
+
+### Query table
+
+Query is the entry point to a CodeRules program. The only purpose of a query is to activate constraints that trigger computations necessary for the query logic. Essentially a query is a limited constraint rule that only has the *body* part.
+
+![](img/queries-table-600.png)  
+_(example of a query)_
+
+A query is discovered by the API through its *kind*, which is specific to the language aspect, and which is represented as a Java interface. Query declares its kind in the **handle** section. The body of a query can contain same constraints and predicates as regular constraint rules.
+
+![](img/queries-interface-500.png)  
+_(example of a query interface)_

docs/content/reactor.md

@@ -1,26 +1,27 @@
 ---
 layout: page
-title: Constraints Reactor
-parent: content/processing.md
-weight: 55
+title: Reactor
+weight: 420
+parent: evaluating
+permalink: :basename
 ---
 
-# Constraints Reactor
+## Reactor
 
-Constraints reactor is a small library written in Kotlin and Java, which implements the extended semantics of constraints processing. Its main features are:
+Reactor is a small library written in Kotlin and Java, which implements the extended semantics of Constraints Processing System. Its main features are:
 
 - native support for terms and unification
 - observable logical variables
-- fast lookup of matching production from constraint’s arguments
+- fast lookup of matching constraint rule from constraint’s arguments
 - Rete-like algorithm for finding potential matches
 
 ### Implementation notes
 
 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 (a prefix tree) on flattened terms[^trie] is used for indexing productions by constraints and their arguments. 
+A trie (a prefix tree) on flattened terms[^trie] is used for indexing constraint rules by constraint symbol and arguments. 
 
-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.
+Search for matching constraint rules is implemented with a trie, with each node corresponding to a partially matched constraint rule. Each constraint activation or disposal event updates this trie. The leaves correspond to fully matched constraint rules.
 
 Persistent structures used for implementing internal state, which are useful for tracking and restoring the state of constraints program.
 
@@ -32,7 +33,7 @@ Logical variables serving as constraint arguments trigger reactivation of such c
 
 #### Restoring the state of logical variables
 
-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.
+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 constraint rule, 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.

docs/content/ruletable.md

@@ -0,0 +1,51 @@
+---
+layout: page
+title: Rule Table
+parent: language
+weight: 220
+permalink: :basename
+---
+
+### Rule Table
+
+#### Constraint declarations
+
+Constraints declared by a rule table are public symbols that serve as its API in the following sense. In the *head* of constraint rules of a rule table and its extensions, only those constraints can be used that were declared in this rule table or any rule table it extends. On the other hand, any constraints can be used in *body*, provided the references to constraint declarations are resolved in the usual way.
+
+![](img/lang-constraints-350.png)
+
+#### Rule templates
+
+Rule templates defined in rule tables are responsible for implementing the logic of checking the types (or other kind of code analysis), for which they may contribute constraint rules. These are created with a DSL that allows mixing constraints and Java code, and can also include constraint fragments inside a constraint rule template.
+
+A rule table is a concept in language `jetbrains.mps.lang.coderules`.
+
+![](img/lang-ruletable-500.png)  
+_(example of a rule table declaration — without contents)_
+
+Keyword `extends` allows to specify another rule table that is to be extended. All constraint rules generated by templates in this rule table will have higher priority. This enables to override the original rule table’s behaviour.
+
+The following example demonstrates how a constraint rule’s body is constructed using a template. A body template is enclosed into a pair of `%% … %%` symbols and yields constraints wrapped into special `<% … %>` brackets.
+
+![](img/lang-template-800.png)  
+_(example of constraint rule with body template)_
+
+As demonstrated above, a constraint rule can be created depending on the result of evaluating a condition expression. Constraint rules can also be created in a cycle.
+
+![](img/lang-forcycle-650.png)
+
+Only declared constraints are allowed to be used in the heads of constraint rules in the rule table declaring the constraint or the extensions of this rule table. Rule table should declare one or more constraints, unless it only uses the constraints from rule tables which it extends. Constraint declaration consists of name and *arity*, which together constitute a *constraint symbol*. Constraint’s arity is fixed.
+
+Rule templates can specify applicable concept, either exactly or including its subconcepts. One can also declare *standalone* rules, which are applied automatically on every evaluation of CodeRules program.
+
+![](img/lang-standalone-350.png)  
+_(example of standalone rule without input)_
+
+Rule template’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 constraint rule responsible for type checking a particular location in source model relies on presence of constraint rules 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.
+
+![](img/lang-require-750.png)  
+_(example of using `require` statement)_
+
+This feature comes in handy for implementing a “partial” type checking (a.k.a. “local type checking”). Type checking may be launched either for a whole root, processing all AST tree recursively, in which case it may be called a “total” type checking, or it can be launched for a particular AST node in isolation, and this is then a “partial” type checking. In the latter case, there must be additional information provided by the type system author, which should serve to establish the necessary context by means of following the required dependencies. These may be method and class declarations, for example, if we are to check the type of a particular method parameter. 

docs/content/termtable.md

@@ -0,0 +1,31 @@
+---
+layout: page
+title: Term Table
+parent: language
+weight: 230
+permalink: :basename
+---
+
+### Term table
+
+Term table contains term declarations. A term is a simple recursive data type that is suitable for implementing unification. Also, terms can model any other data structure, in particular they are suitable for representing types in a programming language.
+
+A term is defined by its symbol and its features, which can be a child term, a list of children terms or any Java object[^obj]. 
+
+![](img/terms-int-300.png)  
+_(example of a term declaration)_
+
+An *open* term declaration can be *extended* by another term, which helps implement a structural subtyping on terms. A term extending another term can add new features.
+
+![](img/terms-open-300.png)  
+_(example of open term declaration)_
+
+A instance of `classifier()` can always be matched with a pattern `parameterized()`, because the former structurally extends the latter.
+
+A term table can extend another term table, in order  to provide extensions to existing terms. 
+
+![](img/terms-ext-400.png)  
+_(example of a term table extension)_
+
+
+[^obj]: Java object conforming to equals/hashCode contract

docs/content/todo/todo-challenges.md

@@ -1,9 +0,0 @@
-# TODO Challenges
-
-- [ ] multi-head productions
-- [ ] incremental matching
-- [ ] loops and recursion (cons list on terms)
-- [ ] toughness of logic programming
-    - [ ] unexpected (re-)activations
-    - [ ] building totally confluent program is hard
-    - [ ] 

docs/content/todo/todo-evaluating.md

@@ -1,15 +0,0 @@
-# TODO Evaluating Code Rules
-
- - [x] Two stages process
-     - [x] apply all rule templates
-         - [x] sort handlers by language
-         - [x] some templates simply report errors
-         - [x] collect constraint productions
-             - [x] build program
-     - [x] evaluate program
-         - [x] report problems during evaluation
-         - [x] handle failures
- - [x] UI
- - [ ] **facade API**
- - [x] activation trace view
-

docs/content/todo/todo-research.md

@@ -4,17 +4,10 @@
 
 There are a few points that are critical for performance of Reactor library. 
 
-1. Indexing of productions by constraint symbol and arguments;
-2. Dealing with factorial expansion when searching for a match;
-3. Matching of constraint occurrence with production’s constraint;
-4. Unification.
-
-### Incremental processing of code rules
-
-How can we have incremental type checking? 
-
-1. Can a program be analysed and code rules applied in such a way, so that the constraints program is updated incrementally, and
-2. Can we launch constraints program (provided there are some constraints in the store), so that only the necessary productions are triggered as required by the changes.
+1. [x] Indexing of productions by constraint symbol and arguments;
+2. [x] Dealing with factorial expansion when searching for a match;
+3. [x] Matching of constraint occurrence with production’s constraint;
+4. [x] Unification.
 
 ### Properties of user-defined type system