From 341ac0208ec0cc2ea8a4c6e53b60eb3ec1faad6b Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Mon, 27 Aug 2018 11:03:12 +0200 Subject: [PATCH] Fix docs wording. Cleaning up the text --- docs/content/evaluating.md | 16 +++++++-------- docs/content/example-typechecking.md | 5 +---- docs/content/intro.md | 11 +++++----- docs/content/language.md | 30 +++++++++++++--------------- docs/content/overview.md | 6 +++--- docs/content/processing.md | 4 ++-- 6 files changed, 33 insertions(+), 39 deletions(-) diff --git a/docs/content/evaluating.md b/docs/content/evaluating.md index 0e6271c9..8ecc0a55 100644 --- a/docs/content/evaluating.md +++ b/docs/content/evaluating.md @@ -11,25 +11,25 @@ The process of evaluating code rules consists of two stages: 1. Collecting handlers and applying rules. 2. Processing constraint productions collected in the first stage. -Stage one is executed in the background in a read action, and is expected to finish quickly. Stage two is executed on a worker thread and does not require reads or writes. After the second stage is finished there is a short write action which «publishes» collected types. +Stage one is executed in the background in a read action, and is expected to finish quickly. Stage two is executed on a worker thread and does not require reads or writes. After the second stage is finished there is a short write action which «publishes» collected types. -### Applying rule templates +### Applying rules -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. +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. -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, with the productions coming from extensions having higher priority. +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. -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 to source model nodes, they produce constraint productions generated from templates. As well as generating constraint productions, the rules are allowed to report messages to be displayed at source locations. +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. Generated constraint productions constitute the constraints program, which is then executed in the next stage. ### Running constraints program -In the second stage the constraints program is executed. +In the second stage the constraints program is executed. To begin execution, a *query* is selected, which contains the list of constraints to be activated. Query can be viewed as a regular production, which is triggered unconditionally, but no earlier than all headless productions (marked as «on start») have fired. -There is a fixed order in which productions are fired on start of program execution. First, all «on start» productions are triggered. All constraints activated by these productions are processed normally, and after there are no more productions to be triggered, the query is fired. +There is a fixed order in which productions are fired on start of program execution. First, all «on start» productions are triggered. All constraints activated by these productions are processed normally, and after there are no more productions to be triggered, the query is fired. Order of productions fired: 1. «on start» productions @@ -39,7 +39,7 @@ While constraints program is run, it is allowed to report feedback, such as assi ***Feedback predicates example*** -Failures during evaluation 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 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. ***Alternative body example*** diff --git a/docs/content/example-typechecking.md b/docs/content/example-typechecking.md index 5c9c8e57..d43a72a6 100644 --- a/docs/content/example-typechecking.md +++ b/docs/content/example-typechecking.md @@ -25,7 +25,7 @@ Primitive types define allowed ranges, so the dataforms for these types have val ![](img/ex-typecheck-terms2-400.png) _(examples of primitive type dataforms)_ -There are two queries defined for typechecking and for converting a type to another type. The latter is used when testing for *subtyping*. ConvertsTo query expands both its parameters before activating `convertsTo()` constraint, which launches the process of evaluating the relation. +There are two queries defined for typechecking and for converting a type to another type. The latter is used when testing for *subtyping*. ConvertsTo query expands both its parameters before activating `convertsTo()` constraint, which launches the processing of the relation. ![](img/ex-typecheck-convertsto-450.png) _(the production from `ConvertsTo` query)_ @@ -95,6 +95,3 @@ Take a simple example of `Long` classifier type — the boxed `long`. Its superc ``` Suppose we need to decide if `Long <: Serializable`, that is if `Long` is a subtype of `Serializable`. The shortest path between those consists of three nodes : `[Long, Number, Serializable]`. Constraint `dpromote()` is activated with this list as the 3rd parameter, and it requires two steps of inductive production and one step of reflexive to solve this relation. - - - diff --git a/docs/content/intro.md b/docs/content/intro.md index 356455a6..d2743012 100644 --- a/docs/content/intro.md +++ b/docs/content/intro.md @@ -22,31 +22,30 @@ Consider how the type of a method call is calculated: the details aside, in esse ![](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 the ability to use logical variables to represent unknowns, and with support for term algebra and unification, it is pretty straightforward to define the core of type inference or similar framework without having to rely on opaque implementation and pre-defined relations. +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 similar framework without having to rely on opaque implementation and pre-defined relations. Typechecking assignment expression could look like the following. What 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) _(typechecking 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`, which requires contravariance. +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`, which requires contravariance. ![](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 `jetbrains.mps.lang.coderules` with concept definitions for building rules that serve as production templates, and as regular «checking» rules. The templates may be concept-specific or standalone, if there is a need to provide constraints that are invariant for every invocation. + - A language `jetbrains.mps.lang.coderules` with concept definitions for building rules that serve as production templates, and as regular «checking» rules. The rules may be concept-specific or standalone, if there is a need to provide constraints that are invariant for every invocation. - *Constraint Processing System* — an extension of CHR[^chr] semantics allowing the use of unification in production’s head with automatic binding of logical variables on successful match. This extension also supports limited backtracking, as well as calling arbitrary Java code. Representing the inference in the form of logical productions helps achieve extensibility, as productions defined by extension languages can be easily blended in. - - A framework for evaluating a constraints program, enabling reporting of problems from the production body, as well as a façade interface for accessing the results of program evaluation. The UI also includes a tracing tool for providing insights into how constraints are handled. + - A framework for executing a constraints program, with support for reporting of problems from the production body, as well as a façade interface for accessing the results of program execution. The UI also includes a tracing tool for providing insights into how constraints are handled. - Finally, an embedded engine capable of processing constraints, which accepts a list of productions, 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. +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) - diff --git a/docs/content/language.md b/docs/content/language.md index 179bded9..0ecf3c6b 100644 --- a/docs/content/language.md +++ b/docs/content/language.md @@ -8,7 +8,7 @@ weight: 30 ### Language Aspect -Code rules are declared by handlers, which are root concepts of language `jetbrains.mps.lang.coderules`. Handlers and other roots should be created in a language’s aspect model corresponding to a specific kind of analysis. Language `jetbrains.mps.lang.typechecking` declares the aspect `types`. +Code rules are declared by handlers, which are root concepts of language `jetbrains.mps.lang.coderules`. Handlers and other roots should be created in a language’s aspect model corresponding to a specific kind of analysis. Language `jetbrains.mps.lang.typechecking` declares the aspect `types`. ![](img/eval-aspect-400.png) _(definition of aspect `types`)_ @@ -32,7 +32,7 @@ The following table contains the root concepts that belong to code rules definit The aim of rules defined by handlers is again twofold: firstly, they may serve as regular «checking» rules, and also, most importantly, they contribute constraint productions. These are created with a DSL that allows mixing of productions and Java code, and can also include constraint fragments inside a production template. -The following example is from the experimental *control flow* aspect for baseLanguage. It demonstrates how a production is constructed using a template. A production 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 the production in case the condition is satisfied (a location is written to only if the local variable has an initialiser). +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 the production in case the condition is satisfied (a location is written to only if the local variable has an initialiser). ![](img/language-writelocal-750.png) _(example of rule with production template)_ @@ -46,7 +46,7 @@ Keyword `extends` allows to specify another handler, which is to be extended. Al 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. -Rules can specify applicable concept, either exactly or including its subconcepts. One can also declare *standalone* rules, which are triggered automatically on every rules application. +Rules can specify applicable concept, either exactly or including its subconcepts. One can also declare *standalone* rules, which are triggered automatically on every application of code rules. ![](img/language-vardecl-600.png) _(example of rule matching concept instances with condition block)_ @@ -58,16 +58,16 @@ _(example of standalone rule without input)_ Contents of a rule 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 the body. When no input is specified, the rule becomes «standalone» and is automatically executed once per every rules application. -Rules may affect the scope of model locations that are processed during the application session. Suppose a production responsible for typechecking a location 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 application session one uses `require` statement. +Rules may affect the scope of model locations that are processed during the application session. Suppose a production responsible for typechecking a location 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 application session one uses `require` statement. ![](img/language-recoverct-700.png) _(example of using `require` statement)_ #### Constraint Productions -*Constraint productions* can be created at any place within rule body. A production has three main parts called head, guard, and body. The head defines what constraint trigger this production, and it can only contain constraints defined by the handler or one of the handlers it extends. The body can contain any visible constraints, as well as *predicates*. A production must include either the body or the head, no production can omit both. The guard is optional, and it can only contain predicates. +*Constraint productions* can be created at any place within rule body. A production has three main parts called *head*, *guard*, and *body*. Head defines what constraint trigger this production, and it can only contain constraints defined by the handler or one of the handlers it extends. Body can contain any visible constraints, as well as *predicates*. A production must include either the body or the head, no production can omit both. Guard is optional, and it can only contain predicates. -Both the head and the body can declare *logical variables*. By default a logical variable ranges over *terms*, although any POJO may be serve as a value. +Both head and body can declare *logical variables*. By default a logical variable ranges over *terms*, although any POJO may be serve as a value. ![](img/language-compatibleWith-300.png) _(constraint production declaring logical variables)_ @@ -78,12 +78,12 @@ In production’s head constraints can be declared as either *kept* or *replaced A production is triggered when there are constraint occurrences matching all constraints in production’s head. 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 the binding is this production’s guard and body. -Pattern matching is also possible with terms, optionally containing logical variables, serving as patterns. For this to work, a logical variable that serves as a constraint argument should have a pattern attached. +There is support for pattern matching, which relies on terms, optionally containing logical variables, serving as patterns. 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 where locations in the source code (model) must be referenced, node references are used, which are introduced with the `@` symbol. +Everywhere locations in the source code (model) must be referenced, node references are used, which are introduced with the `@` symbol. ![](img/language-typeof-550.png) _(example of constraint argument referring to a location)_ @@ -104,35 +104,35 @@ _(example of using `eval()` predicate)_ ***Expand/call pseudo predicates*** -***Code templates within production body*** +***Template fragments within production template body*** ***Alternative body*** #### Query -Query is the entry point to a constraint program. The only purpose of a query is to activate constraints that trigger computation implemented by constraint productions. +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*. 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. +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 constraint 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. +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 the 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. +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 code template, with every constraint or predicate produced from this template 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. +- 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*** @@ -148,6 +148,4 @@ _(example of a dataform definition for classifier type)_ ![](img/language-longtype-350.png) _(examples of dataform definition for long type)_ -***Terms*** - [^dft]: this concept is defined in another language, `jetbrains.mps.logic` diff --git a/docs/content/overview.md b/docs/content/overview.md index 1802defc..165e639d 100644 --- a/docs/content/overview.md +++ b/docs/content/overview.md @@ -14,12 +14,12 @@ The outcome of this phase is a *constraints program*, which is a collection of * The first phase runs in «read action», therefore 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 be run in the background, as the access to `SModel` is no longer necessary. -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. For example, type system defines `TYPECHECK` and `CONVERT` queries, aimed at running type checking and testing if a type can be converted to another type, correspondingly. Queries are declared in the same aspect model. +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, aimed at 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 the constraint `convertsTo(A, B)` is activated, kicking off the process of evaluating the program. 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. +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 as a term `primitive(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. @@ -30,7 +30,7 @@ _(example of a query production)_ Here, the first constraint `checkAll/0` fires type checking, whereas the second `recoverAll/0` is responsible for restoring terms to `SNode` instances and reporting them back to the user. 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 stage has no chance of being evaluated. To account for that, a partial backtracking was added to the language of production templates, which helps recover from certain failures. +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 partial backtracking 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)_ diff --git a/docs/content/processing.md b/docs/content/processing.md index 175bb3e0..e3b5be21 100644 --- a/docs/content/processing.md +++ b/docs/content/processing.md @@ -111,11 +111,11 @@ There is some terminology inherited from CHR that can be useful when discussing Guard is a conjunction of predicates, which are checked before a match of available constraints with the production’s head is considered successful. Predicates in a guard are *queried*. -Body is a conjunction of predicates and constraint activations. When evaluated, 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 productions that can be fired, and so on. ***Alternative body*** -## Semantics of constraint program +## Semantics of constraints program The paper by Betz and Frühwirth[^lls] gives an excellent tretise on semantics of CHR using *linear logic*. Since our constraints processing system is based on CHR, this semantics is valid for it also.