diff --git a/docs/content/evaluating.md b/docs/content/evaluating.md index 8ecc0a55..7ff075c1 100644 --- a/docs/content/evaluating.md +++ b/docs/content/evaluating.md @@ -23,7 +23,7 @@ After the relevant handlers are collected, the source model is traversed from th Generated constraint productions constitute the constraints program, which is then executed in the next stage. -### Running constraints program +### Executing constraints program In the second stage the constraints program is executed. @@ -37,12 +37,34 @@ Order of productions 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. -***Feedback predicates example*** +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)_ 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*** +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) +_(example of using an alternative body branch)_ + +### User interface + +The user interface is defined by a plugin responsible for particular language aspect. + +![](img/eval-menu-snapshot.png) +_(context menu with typechecking actions)_ ### Activation trace view -***Activation trace view*** +During execution of a constraints program all activation/suspension/deactivation events, as well as ask/tell queries to predicates can be displayed in a dedicated view. + +![](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. When a row in the left pane side selected, the right pane displays the contents of *constraints store* at this moment in time. + +![](img/eval-atrace-snapshot.png) +_(activation trace view)_ + diff --git a/docs/content/example-controlflow.md b/docs/content/example-controlflow.md index 1affc641..7cae2259 100644 --- a/docs/content/example-controlflow.md +++ b/docs/content/example-controlflow.md @@ -8,4 +8,39 @@ weight: 520 # Control Flow Analysis -***Contents*** +This sample demonstrates how *code rules* can be used for building a complicated analysis, which otherwise requires creating a DSL and runtime library to implement the logic of analysis. The control flow analysis presented here is far from being complete, and serves demo purposes only. + +Language `jetbrains.mps.lang.controlflow` declares an aspect for storing control flow rules. An aspect model `controlflow` in language `jetbrains.mps.baseLanguage.ext` contains the implementation of control flow analysis. + +![](img/ex-cflow-aspect-450.png) +_(controlflow aspect declaration)_ + +Control flow analysis starts with activating constraint `trace/0`. This initiates building of a flow graph, which starts at the first statement of a method’s body. + +![](img/ex-cflow-query-350.png) +_(controlflow query)_ + +Constraint `follow/2` binds together two locations that are adjacent in the control flow graph, and `merge/2` is an auxiliary helper, which is used to mark the «exit point» for a search that goes *depth-first* into subexpressions. + +![](img/ex-cflow-binop-650.png) +_(control flow check of binary operation)_ + +The meaning of `follow(@A, @B)` is «B follows A», and `merge(@X, @Y)` — «X should follow whatever location is last after traversing Y». + +Read and write locations are processed once the control flow graph has been built. This is when `rw/0` constraint activates and starts this phase of the analysis. This phase also consists of two parts, and these are repeated for every method declaration. This is done by putting two constraints in a conjunction, as shown below. + +![](img/ex-cflow-visitall-700.png) +_(initiating collection of «uses» map, then activating «live» analysis)_ + +First, the control flow graph is walked from starting location, which can be a method declaration, for example. During the traversal of the graph a mapping of «uses» is collected — a map where keys are locations that are read, and values are sets of locations where reading happens. Uninitialised reads are detected at this stage. + +Second, all *write* locations are visited again, this time ensuring there is at least one read after a write. + +Finally, the reachability and variable read/write conditions are analysed and the errors are reported in `Check` handler. + +![](img/ex-cflow-reach-650.png) +_(reachability detection)_ + +![](img/ex-cflow-localvar-700.png) +_(local variable read analysis)_ + diff --git a/docs/content/example-lambdacalc.md b/docs/content/example-lambdacalc.md index d8ddb90a..891ac392 100644 --- a/docs/content/example-lambdacalc.md +++ b/docs/content/example-lambdacalc.md @@ -9,7 +9,7 @@ github-path: /tree/master/samples/lambdacalc # Typechecking STLC -Simply Typed Lambda Calculus is a famous example found in almost every textbook on type checking. This sample demonstrates how a classical type checking algorithm (Hindley-Milner[^hm]) designed specifically for this language can be implemented using code rules. This sample has also been demonstrated in an article[^tclc] published online. +Simply Typed Lambda Calculus is a famous example favoured by textbook authors. This sample demonstrates how a classical type checking algorithm (Hindley-Milner[^hm]) designed specifically for this language can be implemented using code rules. This sample has also been demonstrated in an article[^tclc] published online. For purposes of keeping this sample small, we keep the language confined to boolean values. Aside of boolean constants `true` and `false`, the mandatory lambda abstraction and application, `let-in` expression, and `if-then-else`, we have in addition defined `fix` operator to support recursion. diff --git a/docs/content/img/eval-altbody-650.png b/docs/content/img/eval-altbody-650.png new file mode 100644 index 00000000..e522c73c Binary files /dev/null and b/docs/content/img/eval-altbody-650.png differ diff --git a/docs/content/img/eval-atrace-snapshot.png b/docs/content/img/eval-atrace-snapshot.png new file mode 100644 index 00000000..d873bd48 Binary files /dev/null and b/docs/content/img/eval-atrace-snapshot.png differ diff --git a/docs/content/img/eval-menu-snapshot.png b/docs/content/img/eval-menu-snapshot.png new file mode 100644 index 00000000..fbc70e92 Binary files /dev/null and b/docs/content/img/eval-menu-snapshot.png differ diff --git a/docs/content/img/eval-proof-350.png b/docs/content/img/eval-proof-350.png new file mode 100644 index 00000000..be437849 Binary files /dev/null and b/docs/content/img/eval-proof-350.png differ diff --git a/docs/content/img/eval-settype-650.png b/docs/content/img/eval-settype-650.png new file mode 100644 index 00000000..0d581141 Binary files /dev/null and b/docs/content/img/eval-settype-650.png differ diff --git a/docs/content/img/ex-cflow-aspect-450.png b/docs/content/img/ex-cflow-aspect-450.png new file mode 100644 index 00000000..83fe9dc4 Binary files /dev/null and b/docs/content/img/ex-cflow-aspect-450.png differ diff --git a/docs/content/img/ex-cflow-binop-650.png b/docs/content/img/ex-cflow-binop-650.png new file mode 100644 index 00000000..ace6970b Binary files /dev/null and b/docs/content/img/ex-cflow-binop-650.png differ diff --git a/docs/content/img/ex-cflow-localvar-700.png b/docs/content/img/ex-cflow-localvar-700.png new file mode 100644 index 00000000..0a6e5f5f Binary files /dev/null and b/docs/content/img/ex-cflow-localvar-700.png differ diff --git a/docs/content/img/ex-cflow-query-350.png b/docs/content/img/ex-cflow-query-350.png new file mode 100644 index 00000000..e14b60f7 Binary files /dev/null and b/docs/content/img/ex-cflow-query-350.png differ diff --git a/docs/content/img/ex-cflow-reach-650.png b/docs/content/img/ex-cflow-reach-650.png new file mode 100644 index 00000000..1beb1454 Binary files /dev/null and b/docs/content/img/ex-cflow-reach-650.png differ diff --git a/docs/content/img/ex-cflow-visitall-700.png b/docs/content/img/ex-cflow-visitall-700.png new file mode 100644 index 00000000..d4c95dee Binary files /dev/null and b/docs/content/img/ex-cflow-visitall-700.png differ diff --git a/docs/content/img/eval-aspect-400.png b/docs/content/img/language-aspect-400.png similarity index 100% rename from docs/content/img/eval-aspect-400.png rename to docs/content/img/language-aspect-400.png diff --git a/docs/content/img/process-containedin-350.png b/docs/content/img/process-containedin-350.png new file mode 100644 index 00000000..b39463ae Binary files /dev/null and b/docs/content/img/process-containedin-350.png differ diff --git a/docs/content/intro.md b/docs/content/intro.md index d2743012..3771ea74 100644 --- a/docs/content/intro.md +++ b/docs/content/intro.md @@ -6,9 +6,9 @@ weight: 10 # Introduction -This project is an attempt to bring logic programming to JetBrains MPS[^mps] to facilitate tasks related to source code (model) analysis, and which require logical inference of some kind to operate. Examples include type checking and control flow (data flow). +This project is an attempt to bring logic programming to JetBrains MPS[^mps] in order to facilitate tasks related to source mdoel 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 to make logical statements about types, such as «*is a*» or «*is a subtype of*», enabling the internal engine to infer the specific type based on a collection of such statements, referred to as type equations and inequalities. +Type system in MPS is traditionally defined with help of type checking rules, in particular inference rules, which allow to make 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)_ @@ -38,11 +38,11 @@ The following is the list of features made available to users of MPS with *code - 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. + - *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 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 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. + - 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, an initial active constraint, and, optionally, a store of inactive constraints, and yields an updated store after all matched productions have been fired. + - 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. diff --git a/docs/content/language.md b/docs/content/language.md index 0ecf3c6b..9ce3a0e8 100644 --- a/docs/content/language.md +++ b/docs/content/language.md @@ -8,14 +8,14 @@ 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 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`. -![](img/eval-aspect-400.png) +![](img/language-aspect-400.png) _(definition of aspect `types`)_ #### Root concepts -The following table contains the root concepts that belong to code rules definition. +The following table contains root concepts that belong to code rules definition. | Concept | Description | |:-- |:-- | @@ -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 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 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)_ @@ -42,11 +42,11 @@ 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, which 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. +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. -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. +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-vardecl-600.png) _(example of rule matching concept instances with condition block)_ @@ -56,14 +56,14 @@ An applicability condition, if specified, is checked before applying the rule. ![](img/language-hasbound-550.png) _(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. +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 rule’s body. -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 an evaluation session. Suppose a production responsible for typechecking a particular location in source model relies on presence of productions that are only available if some other location is processed as well. To guarantee that a certain model location is processed during the evaluation session, one uses `require` statement. ![](img/language-recoverct-700.png) _(example of using `require` statement)_ -#### Constraint Productions +#### Constraint productions *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. @@ -72,37 +72,44 @@ Both head and body can declare *logical variables*. By default a logical variabl ![](img/language-compatibleWith-300.png) _(constraint production declaring logical variables)_ -A production with an empty head, not declaring any constraints to serve as the input, is considered an *automatic* production and is triggered automatically on start of constraints program evaluation. +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. -In production’s head constraints can be declared as either *kept* or *replaced*. Briefly put, the constraints that are *kept* are left alone after a production is fired, whereas the *replaced* ones are discarded after the head has been matched. Replaced constraints are marked with tilde `~`. +In a production’s head constraints can be declared as either *kept* or *replaced*. Briefly put, the constraints that are *kept* are left alone after a production is fired, whereas the *replaced* ones are discarded after the production’s head has been matched. Replaced constraints are marked with tilde `~`. -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. +A production is triggered when there are constraint occurrences matching all constraints specified in production’s head. These occurrences include the active constraint, plus any additional matching constraints that are currently alive, filling the other vacant slots. -There is 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. +Productions to match a particular constraint are selected from a handler that has declares 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. + +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. +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 location)_ +_(example of constraint argument referring to a model location)_ Whereas the production’s head can only contain constraints, there are also other logical clauses that are used in guard and body. -A *predicate* is a built-in construct that serves two purposes: when used in guard, it serves to query if the condition is satisfied, and when invoked from body, it asserts the condition. An example is `unifies` predicate, displayed as `=`, which tests if its arguments can be unified if used in guard, and invokes the actual unification if called from 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. +A *predicate* is a built-in construct that serves two purposes: when used in guard, it serves to query if the condition is satisfied, and when invoked from body, it asserts the condition. An example is `unifies` predicate, displayed as `=`, which tests that its arguments can be unified — if used in guard, and invokes the actual unification if called from 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. Production’s guard can only contain predicates, and the body can contain both constraints and predicates. ![](img/language-unify-300.png) _(`unifies` predicate used in the guard and in the body)_ -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, such as static method call, which is available in body. +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()` predicate)_ +_(example of using `eval/1` predicate)_ + +In order to make use of macro definitions, which are essentially parameterised production templates extracted to a separate root, one of two pseudo predicates can be used: `expand` and `call`. The former accepts a node, whereas the second expects the argument that are substituted as macro parameters. + +***Examples of expand/call pseudo predicates*** -***Expand/call pseudo predicates*** ***Template fragments within production template body*** diff --git a/docs/content/overview.md b/docs/content/overview.md index 165e639d..817582a4 100644 --- a/docs/content/overview.md +++ b/docs/content/overview.md @@ -8,29 +8,29 @@ weight: 20 Analysis of source code or model with *code rules* can be described as a two-phase process. -In the first phase, the languages used by the model being analysed, and their prototypes (meaning the languages that are being *extended*, but not used directly) are surveyed for the appropriate *code rules* aspect model, which is `types` in case of type checking, for example. Contents of this aspect model is a contribution of this particular language. All rules within this model are applied to the source model, with rules coming from extension languages having higher priority. +In the first phase, languages used by the model being analysed and their prototypes (meaning the languages that are being *extended*, but not used directly) are surveyed for the appropriate *code rules* aspect model, which is `types` in case of type checking, for example. Contents of this aspect model is a contribution of this particular language. All rules within this model are applied to the source model, with rules coming from extension languages having higher priority. -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, it does not have any textual representation. Aside from generating productions, the rules can also process the model normally, reporting errors as usual. +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, it does not have any textual representation. Aside from generating productions, the rules can also process the model normally, reporting errors as usual. -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. +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 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 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 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. +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 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. +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=)`. 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 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. +Here, the first constraint `checkAll/0` fires type checking, whereas the second `recoverAll/0` is responsible for restoring terms 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 partial backtracking was added to the language of constraint productions, 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 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)_ diff --git a/docs/content/processing.md b/docs/content/processing.md index e3b5be21..818c7a3f 100644 --- a/docs/content/processing.md +++ b/docs/content/processing.md @@ -7,15 +7,11 @@ weight: 50 # Constraints Processing System -***Discuss how constraints processing works (abstractly)*** - -- Discuss semantics of constraints processing. -- Loosely follows CHR semantics. -- Influenced heavily by JCHR[^jchr]. +This section briefly overlooks how constraint processing works. The system described here follows loosely the CHR specification, and has been in particular heavily influenced by JCHR[^jchr] implementation. The distinctive features are built-in support for logical variables, terms, and pattern matching. Alternative body branches are a deviation from the standard CHR. ## Terms and unification -Constraints processing relies heavily on the use of terms as data type. Abstractly speaking, terms are functions of 0 or more arguments. Any opaque value captured by a term must be a POJO. +Constraints processing relies heavily on the use of *terms* as data type. Abstractly speaking, terms are functions of 0 or more arguments. Any opaque value captured by a term must be a POJO. ``` f(g(), h(k())) @@ -26,6 +22,8 @@ Constraints processing relies heavily on the use of terms as data type. Abstract ``` _(examples of terms)_ +The unique feature of terms is that they support unification. Unification of two terms is possible with or without *variables* being used as subterms of either participant, but in the latter case the two terms must be equal. + A term variable ranges over terms. A substitution is a mapping of variables to terms. Unification searches for a substitution $\sigma$, such that for two terms being unified, $f$ and $g$, the following holds: $\sigma f = \sigma g$. ``` @@ -34,9 +32,11 @@ A term variable ranges over terms. A substitution is a mapping of variables to t f(X, h(X)) and f(g(), h(k())) can't be unified ``` +Pattern matching is possible when variables are only used by one of the terms, which is then serves as pattern. To test if a pattern matches a given term can be implemented by a linear time algorithm, whereas full unification is slightly more complicated. + ## Logical variables -Logical variables serve to identify an object that is to be determined in the future. They are *monotonic*, in the sense that once a variable is assigned, it stays assigned to that value. In addition, they implement a *union-find data structure*[^uf] a.k.a. «disjoint set». Any free logical variable can be assigned a class by setting its «parent» field to point to the class’s representative. All logical variables belonging to same class are treated as exactly one variable. Logical variables notify observers when they become ground and when their *parent* (class representative) changes. +Logical variables serve to identify an object that is to be determined in the future. They are *monotonic*, in the sense that once a variable is assigned a particular value, it stays assigned to that value. In addition, they implement a *union-find data structure*[^uf] a.k.a. «disjoint set». Any free logical variable can be assigned a class by setting its «parent» field to point to the class’s representative. All logical variables belonging to the same class are treated as exactly one variable. Logical variables notify observers when they become ground and when their *parent* (class representative) changes. ``` val X = Logical("X") @@ -54,7 +54,7 @@ Logical variables serve to identify an object that is to be determined in the fu ``` _(example of using logical variables)_ -Combining logical variables and terms gives a very powerful instrument. A term variable can also be a logical variable, so that when two terms are unified, the substitution has the calculated value for this variable. +A term variable can also be a logical variable, so that when two terms are unified, the substitution already has the calculated value for that variable. ``` val X = Logical("X") @@ -71,30 +71,35 @@ Combining logical variables and terms gives a very powerful instrument. A term v ## Constraints and predicates -Constraints are simple 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, 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 production’s body and stay active until there are no possible matches with 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 production’s body and stay active until there are no possible matches with any of productions’s heads. If a constraint is not discarded by a production, it is stored for future use. Stored constraints represent the program’s state. The following figure shows the lifecycle of a constraint. The big rounded square in the middle contains the states, in which a constraint is considered «alive»: it can be either «active» or «stored», but available for filling up vacant positions in a production’s head. A stored constraint can be reactivated if one of its arguments changes, such as when a logical variable becomes ground. -A successfully fired production, which declares one or more of its head constraints to be «replaced», causes these to be terminated. +A successfully fired production, which declares one or more of constraints in its head to be «replaced», causes these to be terminated. ![](img/constraint-lifecycle.svg) _(lifecycle of a constraint)_ -To illustrate the idea of using *stored* constraints to fill vacant positions when matching a production, let’s consider an example…***unfinished*** +To illustrate the idea of using *stored* constraints to fill vacant positions when matching a production, let’s consider an example — a production resolving `containedIn/2` constraint, which corresponds to *type parameter containment* relation of BaseLanguage types. -***Example of multi-head production*** +![](img/process-containedin-350.png) +_(example of a multi-head production)_ -Whereas a constraint serves to embody a relation among objects simply by being a witness of such a relation, a *predicate*[^pred] helps to establish a relation or check if a relation exists by means of executing a procedure. Same is true for facts and propositions. +When `containedIn/2` constraint is activated, the production above matches, but two slots in its head must be filled in order for production to fire. The processor looks in the *store* for all *different* occurrences of constraint `hasBound/2` that could be matched, and substitutes them in these slots. The production will be fired for every matching triple of constraints. -***Example of a predicate*** +#### Predicates + +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). +***Example of a predicate*** + ***Example of ask/tell*** -## Constraint production (rule) +## Constraint production 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». @@ -108,8 +113,7 @@ 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 | - -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*. +Guard is a conjunction of predicates, which are checked before a production is fired. Predicates in a guard are *queried*. 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. diff --git a/docs/content/todo/todo-evaluating.md b/docs/content/todo/todo-evaluating.md index c56846d5..31234bed 100644 --- a/docs/content/todo/todo-evaluating.md +++ b/docs/content/todo/todo-evaluating.md @@ -6,10 +6,10 @@ - [x] some templates simply report errors - [x] collect constraint productions - [x] build program - - [ ] evaluate program - - [ ] **report problems during evaluation** - - [ ] **handle errors** - - [ ] **UI** + - [x] evaluate program + - [x] report problems during evaluation + - [x] handle failures + - [x] UI - [ ] **facade API** - - [ ] **activation trace view** + - [x] activation trace view diff --git a/docs/content/todo/todo-language.md b/docs/content/todo/todo-language.md index 1d1fb584..df2e1de7 100644 --- a/docs/content/todo/todo-language.md +++ b/docs/content/todo/todo-language.md @@ -62,13 +62,14 @@ - [x] what are getters - [x] extending another term - [ ] terms representing types + - [ ] subst expression - [ ] using terms - - [ ] constructing new terms + - [ ] creating terms with dataform table - [ ] specify subtterms - [ ] specify values - [ ] using terms as patterns - [ ] **copy operation**! -- [ ] constructing term +- [ ] constructing term with primitives - [ ] list term - [ ] dataform concept and subconcepts - [ ] splice \ No newline at end of file