diff --git a/docs/content/evaluating.md b/docs/content/evaluating.md index 90d59dca..706253b6 100644 --- a/docs/content/evaluating.md +++ b/docs/content/evaluating.md @@ -1,9 +1,40 @@ --- layout: page -title: Evaluating Constraints Program -weight: 50 +title: Evaluating Code Rules +weight: 40 --- -## Evaluating constraints program +# Evaluating Code Rules - ![](img/errorDialog.png) **TODO executing constraints processing from MPS** + ![](img/errorDialog.png) **TODO two stage process** +## Aspects + ![](img/errorDialog.png) **TODO aspects** + +## Applying rule templates + +The first stage of evaluating code rules is applying handlers. Handlers are collected from corresponding aspects of all languages imported into the model. + +As rules are applied to source model nodes, they produce constraint productions generated from templates. The order of productions is kept as defined by handlers, with handlers from extension languages having higher priority. + +As well as generating constraint productions, the rules are allowed to report messages to be displayed at source locations. + +Generated productions constitute the constraints program, which is then executed. + +## Running constraints program + +In the second stage the constraints program is run. 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 right after all headless productions (marked as «on start») have fired. + +![](img/errorDialog.png) **TODO order of productions firing** +Order of productions fired: + - on start + - query + +While constraints program is run, it is allowed to report feedback, such as assign calculated types or report problems, using special predicates. + +![](img/errorDialog.png) **TODO 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. + +## Activation trace view + + ![](img/errorDialog.png) **TODO activation trace view** diff --git a/docs/content/example-lambdacalc.md b/docs/content/example-lambdacalc.md new file mode 100644 index 00000000..db746e63 --- /dev/null +++ b/docs/content/example-lambdacalc.md @@ -0,0 +1,25 @@ +--- +layout: page +title: Typechecking Simply Typed Lambda Calculus +menu: Typechecking STLC +parent: examples +weight: 550 +--- + +- Types + - bool, fun, forall + - trivial macros +- Query + - typecheck +- Handlers + - constant values + - lambda var bind + - let var bind + - let expr + - var ref + - lambda abs + - fun app + - if-then-else + - fix + - forall type + - gen-inst \ No newline at end of file diff --git a/docs/content/example-typechecking.md b/docs/content/example-typechecking.md new file mode 100644 index 00000000..5382ab22 --- /dev/null +++ b/docs/content/example-typechecking.md @@ -0,0 +1,58 @@ +--- +layout: page +title: Typechecking BaseLanguage +menu: Typechecking BL +parent: examples +weight: 500 +--- + +# Typechecking BaseLanguage + +Short explanation of the architecture of BL-specific type system built with *code rules*. + +- types + - term table for types + - classifier type + - type var type + - capture type + - array/vararity type + - upper/lower bound type + - wildcard type + - primitive type: int, bool, etc. + - void and null + - macro table + - classifier type + - type var type + - bounds + - parameterised types + - types with value +- Query + - Typecheck + - checkall, recoverall + - ConvertsTo + - convertsTo() +- Typechecking + - Constant values + - string + - integer, long, char, … + - expression + - dotexpression, dot operation + - method call + - equals/assignment/+assignment + - + - ??? + - method declaration + - type relations + - boxing + - capture + - coerce + - conversion + - primitive subtyping + - subclassing/promote + - type parameter + - containment, hasbound + - type annotations + - classifier type + - type parameters: type var, bound type, wildcard + - + diff --git a/docs/content/full.md b/docs/content/full.md index 8245c203..5dc2c311 100644 --- a/docs/content/full.md +++ b/docs/content/full.md @@ -11,3 +11,5 @@ /evaluating.md /reactor.md + +/challenges.md diff --git a/docs/content/img/constraint-lifecycle.svg b/docs/content/img/constraint-lifecycle.svg new file mode 100644 index 00000000..fabb5ea3 --- /dev/null +++ b/docs/content/img/constraint-lifecycle.svg @@ -0,0 +1 @@ + \ No newline at end of file diff --git a/docs/content/intro.md b/docs/content/intro.md index a5b88f05..7a10709a 100644 --- a/docs/content/intro.md +++ b/docs/content/intro.md @@ -3,7 +3,7 @@ layout: page title: Introduction weight: 10 --- -## Introduction +# 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). diff --git a/docs/content/language.md b/docs/content/language.md index b56ebc67..0786a5c4 100644 --- a/docs/content/language.md +++ b/docs/content/language.md @@ -3,10 +3,12 @@ layout: page title: Code Rules Language weight: 30 --- -## Code rules language +# Code Rules Language ![](img/errorDialog.png) **TODO This section should teach how to use the language** +Root concepts should be contained by a language aspect model importing the language `jetbrains.mps.lang.coderules`. For example, language `jetbrains.mps.lang.typechecking` defines aspect *types* to contain code rules related to type checking. + ### Root concepts | Concept | Description | diff --git a/docs/content/overview.md b/docs/content/overview.md index 013e4170..2a2bacd2 100644 --- a/docs/content/overview.md +++ b/docs/content/overview.md @@ -3,7 +3,7 @@ layout: page title: Overview weight: 20 --- -## Overview +# Overview Analysis of source code (model) with *code rules* can be described as a two-phase process. diff --git a/docs/content/processing.md b/docs/content/processing.md index b8be0373..e081b891 100644 --- a/docs/content/processing.md +++ b/docs/content/processing.md @@ -1,17 +1,17 @@ --- layout: page title: Processing Constraints -weight: 40 +weight: 50 --- -## Constraints processing system +# Constraints processing system ![](img/errorDialog.png) **TODO Discuss how constraints processing works (abstractly)** -> Discuss semantics of constraints processing. -> Loosely follows CHR semantics. -> Influenced heavily by JCHR[^jchr]. +- Discuss semantics of constraints processing. +- Loosely follows CHR semantics. +- Influenced heavily by JCHR[^jchr]. -### Terms and unification +## 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. @@ -33,9 +33,9 @@ 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 ``` -### Logical variables +## 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]. 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, 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. ``` val X = Logical("X") @@ -70,17 +70,74 @@ Combining logical variables and terms gives a very powerful instrument. A term v ``` -### Constraints and predicates +## 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 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. + +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. + +![](img/constraint-lifecycle.svg) + +To illustrate the idea of using *stored* constraints to fill vacant positions when matching a production, let’s consider an example…**TODO** + +![](img/errorDialog.png) **TODO example of 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. + +![](img/errorDialog.png) **TODO example of a predicate** + +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). + +![](img/errorDialog.png) **TODO example of ask/tell** + +## Constraint production (rule) ![](img/errorDialog.png) **TODO** +Constraints program is built from productions. Each production has three parts: the part that is responsible for triggering the production, called «head», the part that checks for pre-conditions, called «guard», and the part that is evaluated when production is fired, which is called «body». + +Head 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. + +There is some terminology inherited from CHR that can be useful when discussing the kinds of productions. + +| «kept» set `E` | «replaced» set `E’` | Notation | Designation | +|:--|:--|:--:|:--| +| empty | non-empty | `E’ <=> C | G` | Simplification | +| non-empty | empty | `E => C | G` | Propagation | +| non-empty | non-empty | `E \ E’ <=> C | G` | Simpagation | +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. -### Constraint production (rule) +![](img/errorDialog.png) **TODO alternative body** -![](img/errorDialog.png) **TODO** +## Semantics of constraint program -[^jchr]: https://dtai.cs.kuleuven.be/CHR/JCHR/ +The paper by Betz and Frühwirth[^lls] gives an excellent tretise on semantics of CHR using *linear logic*. Since our constraints processing system is based on CHR, this semantics is valid for it also. + +Linear logic abandons boolean values and replaces them with consumable resources. Consequently, it introduces its own set of connectives, from which we are interested only in the following: $!,\otimes,\multimap$. The *multiplicative conjunction* $\otimes$ combines two or more resources that are all available at the same time. The symbol $!$ (*of course*) marks a resource that can’t be exhausted. And instead of implication $\rightarrow$ one uses $\multimap$ symbol, the meaning of which is a transformation of one resource to another. The formula $A \multimap B$ is read: «consuming $A$, produce $B$ », that is given a resource $A$, we can assume $B$, but $A$ can no longer be used. + +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. + +\\[ (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». + +\\[ (E \Rightarrow C | G)^L := + !\forall((!C^L) \multimap + (E^L \multimap E^L\otimes\exists\bar{y}G^L)) \\] + + +[^jchr]: K.U.Leuven JCHR System https://dtai.cs.kuleuven.be/CHR/JCHR/ [^uf]: https://en.wikipedia.org/wiki/Disjoint-set_data_structure +[^pred]: a.k.a. «built-in constraints» in CHR literature +[^lls]: Betz, H. and Frühwirth, T., 2005, October. A linear-logic semantics for constraint handling rules. In International Conference on Principles and Practice of Constraint Programming (pp. 137-151). Springer, Berlin, Heidelberg. \ No newline at end of file diff --git a/docs/content/reactor.md b/docs/content/reactor.md index fbb06d20..0e2972d1 100644 --- a/docs/content/reactor.md +++ b/docs/content/reactor.md @@ -1,14 +1,37 @@ --- layout: page title: Constraints Reactor -weight: 60 +parent: content/processing.md +weight: 55 --- -## Reactor +# Constraints Reactor ![](img/errorDialog.png) **TODO details of constraints processing implementation** -- [ ] Production matching algorithm - - [ ] Propagation history -- [ ] Constraints store -- [ ] Persistent stack frame -- [ ] Processing of evaluation failuress +Constraints reactor is a small library written in Kotlin and Java, which implements the extended semantics of constraints processing. Its main features are: + +- native support for terms and unification +- observable logical variables +- fast lookup of matching production from constraint’s arguments +- Rete-like algorithm for finding potential matches + +## Implementation notes + +Unification is implemented according to a «near-constant time» algorithm[^uni]. + +A trie[^trie] (a prefix tree) on flattened terms is used for indexing productions by value. + +Persistent structures used for implementing internal state, which are useful for tracking and restoring the state of the constraints program. + +## Open questions + +### Nested logical variables + +Logical variables serving as constraint arguments trigger reactivation of such constraints on any change, such as value bound or parent changed. Might be a good idea to also trigger reactivation on changed variable contained in a term, which serves as a constraint argument. + +### Restoring the state of logical variables + +One of the extensions supported by this implementation is the *partial rollback*, which allows to declare alternative branches in a production’s body. The implementation is able to restore the state of constraints that is valid for the frame corresponding activation of the body, except for the state of logical variables that may have been changed. This, too, might be worth implementing. + +[^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. \ No newline at end of file diff --git a/docs/content/todo-evaluating.md b/docs/content/todo-evaluating.md deleted file mode 100644 index 8d89543f..00000000 --- a/docs/content/todo-evaluating.md +++ /dev/null @@ -1,12 +0,0 @@ -### Evaluating constraints program - - - [ ] Two stages process - - [ ] apply all rule templates - - [ ] some templates simply report errors - - [ ] collect constraint productions - - [x] build program - - [x] evaluate program - - [ ] report problems during evaluation - - [ ] handle errors - - [ ] activation trace view - diff --git a/docs/content/todo-processing.md b/docs/content/todo-processing.md deleted file mode 100644 index 64ae0051..00000000 --- a/docs/content/todo-processing.md +++ /dev/null @@ -1,35 +0,0 @@ -### Constraints processing -- [ ] intro -- [x] Terms - - [x] abstract data structure - - [x] keeping arbitrary POJO - - [x] unification -- [x] Logical variables - - [x] monotonic - - [x] Terms with logical vars - - [x] unification binds logicals - - [x] logicals are observable - - [x] parent observer - - [x] value observer -- [ ] Constraints and predicates - - [ ] What is a constraint. - - [ ] Constraint arguments. - - [ ] POJO - - [ ] Term - - [ ] Logical vars - - [ ] what is a predicate - - [ ] tell / ask -- [ ] Constraint production (constraint rule) - - [ ] kept constraints vs. replaced constraints - - [ ] simplification/propagation/simpagation - - [ ] constraint store - - [ ] constraint lifecycle - - [ ] condition for firing a production - - [ ] on start - how it’s actually implemented (main) - - [ ] automatic binding of logicals on firing - - [ ] guard condition - - [ ] predicates - - [ ] arbitrary java code - - [ ] body - - [ ] alternate body - diff --git a/docs/content/todo/todo-challenges.md b/docs/content/todo/todo-challenges.md new file mode 100644 index 00000000..2e18b380 --- /dev/null +++ b/docs/content/todo/todo-challenges.md @@ -0,0 +1,9 @@ +# 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 + - [ ] \ No newline at end of file diff --git a/docs/content/todo/todo-evaluating.md b/docs/content/todo/todo-evaluating.md new file mode 100644 index 00000000..d4630558 --- /dev/null +++ b/docs/content/todo/todo-evaluating.md @@ -0,0 +1,15 @@ +# TODO Evaluating Code Rules + + - [ ] **aspects** + - [ ] **UI** + - [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 + - [ ] evaluate program + - [ ] **report problems during evaluation** + - [x] handle errors + - [ ] **activation trace view** + diff --git a/docs/content/todo-full.md b/docs/content/todo/todo-full.md similarity index 100% rename from docs/content/todo-full.md rename to docs/content/todo/todo-full.md diff --git a/docs/content/todo-language.md b/docs/content/todo/todo-language.md similarity index 88% rename from docs/content/todo-language.md rename to docs/content/todo/todo-language.md index e0ae095e..a5f41e17 100644 --- a/docs/content/todo-language.md +++ b/docs/content/todo/todo-language.md @@ -1,4 +1,13 @@ -### Handler +# TODO Language + +## Intro +- [ ] templates are usual for MPS +- [ ] applicable to concept/+subconcepts +- [ ] standalone +- [ ] can serve as «checking rule» +- [ ] produce productions to be evaluated + +## Handler - [x] create handler, optionally extend another handler - [x] declare constraints - [ ] define rule template @@ -25,13 +34,13 @@ - [ ] **using code templates** `%% … %%` - [ ] **alternative body** -### Query +## Query - [x] Purpose of a query - [x] Query kind - [x] Parameters - [x] Executed block -### Macro table +## Macro table - [x] applicable to a node of specific concept - [x] macro is not applied automatically - [x] macro parameters @@ -48,7 +57,7 @@ - [ ] context parameters - [ ] specifying parameters using «with» statement -### Term table +## Term table - [x] purpose of this root - [ ] what is a term - [x] what are features diff --git a/docs/content/todo/todo-processing.md b/docs/content/todo/todo-processing.md new file mode 100644 index 00000000..f8746d6c --- /dev/null +++ b/docs/content/todo/todo-processing.md @@ -0,0 +1,62 @@ +# TODO Constraints Processing + +- [ ] intro + - [ ] committed choice + - [ ] embeddable + - [ ] call back to Java + - [ ] +- [x] Terms + - [x] abstract data structure + - [x] keeping arbitrary POJO + - [x] unification + - [ ] **example of finding MGU with unification** +- [x] Logical variables + - [x] monotonic + - [x] Terms with logical vars + - [x] unification binds logicals + - [x] logicals are observable + - [x] parent observer + - [x] value observer +- [x] Constraints and predicates + - [x] What is a constraint. + - [x] constraint lifecycle + - [ ] **constraint store** + - [x] Constraint arguments. + - [x] POJO + - [x] Term + - [x] Logical vars + - [ ] **constraint observes its arguments** + - [x] what is a predicate + - [x] tell / ask + - [ ] **unification example** + - [ ] ask - test if unification succeeds (logical context) + - [ ] tell - unify terms, assign logicals, re-activate constraints +- [ ] Constraint production (constraint rule) + - [x] kept constraints vs. replaced constraints + - [x] simplification/propagation/simpagation + - [ ] condition for firing a production + - [ ] on start - how it’s actually implemented (main) + - [ ] automatic binding of logicals on firing + - [ ] pattern matching + - [ ] guard condition + - [ ] predicates + - [ ] arbitrary java code + - [ ] body + - [ ] predicates + - [ ] arbitrary java code + - [ ] alternative body + - [ ] handlers + - [ ] order of productions within a handler +- [ ] Processing a constraint + - [ ] one active constraint at any moment + - [ ] productions selected top-to-bottom + - [ ] aux constraints from store + - [ ] committed choice +- [ ] Extensions (differences to CHR) + - [ ] partial rollback (alternative body) + - [ ] observable logicals reactivate constraints + - [ ] matched head binds logicals + - [ ] +- [ ] Semantics of constraints program + - [ ] **classical semantics**? + - [x] linear logic semantics diff --git a/docs/content/todo/todo-reactor.md b/docs/content/todo/todo-reactor.md new file mode 100644 index 00000000..20817433 --- /dev/null +++ b/docs/content/todo/todo-reactor.md @@ -0,0 +1,12 @@ +# TODO Constraints Reactor + +- [ ] Production matching algorithm + - [ ] Partially matched constraints in a persistent discrimination trie + - [ ] Fired propagations kept as history +- [ ] Persistent Constraints store +- [ ] Persistent stack frame +- [ ] Processing of evaluation failures +- [ ] unification +- [ ] open questions + - [x] reactivate constraint on **nested** logical change + - [x] restore the state of logicals on rollback diff --git a/docs/index.md b/docs/index.md new file mode 100644 index 00000000..75fa26b8 --- /dev/null +++ b/docs/index.md @@ -0,0 +1,10 @@ +--- +title: About +menu: false +weight: 1 +layout: welcome +--- + +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.