diff --git a/docs/CodeRules.md b/docs/CodeRules.md deleted file mode 100644 index 60f43031..00000000 --- a/docs/CodeRules.md +++ /dev/null @@ -1,305 +0,0 @@ -# Code Rules - - -## Introduction - -This project is an attempt to bring logic programming to JetBrains MPS[^[https://jetbrains.com/mps](https://jetbrains.com/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). - -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. - -``` -typeOf(assignment.right) :<=: typeof(assignment.left) -``` - -Albeit brief and concise, this notation leaves many questions unanswered when it comes to how exactly the system of equations and inequalities is processed. In other words, type inference is — for the most part — left up to the internal engine to decide. This limits the options for the author of type system to control how exactly subtyping is defined, and what happens with type parameters when computing sub- or supertype. Java, for instance, has several kinds of «conversions» with clearly defined rules controlling how types are transformed and what types are compatible in certain situations. All of this has to be emulated with «strong» and «weak» subtyping in MPS. - -Another example is the all too well known *when_concrete*, which is basically a suspended block that gets executed when the type, that serves as its parameter, is computed. Sometimes this never happens during type inference, which results in numerous «*when concrete is never concrete*» warnings, leaving the user wondering what went wrong. This, however, is very much a necessary evil, since there are no other possibilities to hook into the engine in order to spy on types, and knowing the exact form of a type is sometimes required for further inference. - -Consider how the type of a method call is calculated: the details aside, in essence *when_concrete* has to be applied to the type of each argument. Then we should either turn to inequalities and rely on the inference engine, or analyse the type structure and run closing computation when the *last* unknown type is finalised. - -``` -foreach arg in methodCall.arguments { - when_concrete (typeof(arg) as A) { - // analyse the type of arg, such as extract its parameters, etc - // when all argument types are known, infer the type of call - } -} -``` - -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. - -The following is the list of features made available to users of MPS with *code rules* plugin. - -A language `jetbrains.mps.lang.coderules` containing concept definitions for building rules that serve as production templates, and as regular «checking» rules. The templates may be concept-specific or standalone in order to provide constraints that are invariant for every invocation. - -An extension of 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)] semantics allowing the use of unification in production 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 the program evaluation. 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. - -## Overview - -Analysis of source code (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. The contents of code rules aspect model is a contribution of this particular language. All templates are applied to the source code, with templates 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 textual representation. Aside from generating productions, the rules can also process the model normally, reporting errors as usual. - -This 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 second phase is evaluation of the constraints program that was created in phase one. The 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. - -``` -query ConvertsTo -parameter: node<> from, node<> to -kind: TypecheckingQueryKind.CONVERT - - on start - activate - A := expand from, B := expand to, convertsTo(A, B) -``` - -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()` 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, 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 constraints: - -``` -on start - activate - checkAll(), recoverAll() -``` - -Here, the first constraint `checkAll()` fires type checking, whereas the second `recoverAll()` 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. - -``` -on start - activate - checkAll() - else - recoverAll() -``` - -Here, `recoverAll()` constraint is moved out to an «*alternative branch*» of production body, which allows it to be activated even if there was an error while processing the main branch. - -To illustrate how automatic binding of logical variables work, consider the following example. The constraint `typeOf()` associates a type with a location in source code, and `convertsTo()` ensures its 1st argument can be converted to the 2nd, which must both be types. - -``` -assignmentExpression matching AssignmentExpression ae -{ - on - typeOf(@ae.lValue, LType), typeOf(@ae.rValue, RType) - activate - convertsTo(RType, LType) -} -``` - -The production is triggered when both locations referred to by `ae.lValue` and `ae.rValue` have their types assigned, as both `typeOf()` constraints must be present for a match to be successful. Once production’s head is matched, both logical variables `LType` and `RType` become bound to whatever was the 2nd argument of first and second `typeOf()` constraint, respectively. - -It’s important to note, that although on successful match both `lValue` and `rValue` have types, it’s not guaranteed that these types are *ground*. A type may be represented by a free logical variable, or a term containing free variables. Another very important thing to notice is that a logical variable enjoys full privileges of being an argument to a constraint. Which means, if in the above example both variables are free, and `LType = RType`, then both locations will have essentially the *same* type (in the sense of «same instance»), not just matching types. - -The following example illustrates the use of *pattern matching* in production’s head. Here the first argument to constraint `convertsTo()` in the head is a logical variable with pattern expression. In this case the production will only be triggered if the active constraint’s first argument is not a free variable, and it matches the pattern. - -``` -converts_captureOf_upperBound -{ - on - ~convertsTo(Capture = captureOfType(ubound: UBnd), To) - activate - convertsTo(UBnd, To) -} -``` - - -## Code rules language - -![](img/errorDialog.png) **TODO This section should teach how to use the language** - - -### Root concepts - -| Concept | Description | -|:-- |:-- | -| *Handler* | contains rule templates and constraint declarations | -| *MacroTable* | defines how terms are constructed | -| *Query* | entry point to the constraints program | -| *DataFormTable*[^this concept is defined in another language, `jetbrains.mps.logic`] | defines terms, the data structure that is used in unification | - -### Rule templates - -### Handler - -- Handler - - [x] create handler, optionally extend another handler - - [x] declare constraints - - [ ] define rule template - - [ ] for concept, standalone - - [ ] applicability condition - - [ ] **what features are available in a rule** - - [ ] introduce constraint production - - [ ] declare logical variables - - [ ] on start - - [ ] on … defining *head* - - [ ] keep / replace (~) - - [ ] pattern matching - - [ ] the '@' syntax - - [ ] predicates vs constraints - - [ ] special predicates «expand» and «call» - - [ ] calling arbitrary Java code - - [ ] guard (when) - - [ ] what operations are available in the guard - - [ ] body - - [ ] what operations are available in the body - - [ ] using code templates `%% … %%` - - [ ] alternative body - -*Handler* serves two purposes: it declares the constraints that can be used in the *head* of productions in this handler and its extensions, and it also declares *rule templates*, which are, simply put, procedures applicable to specific concept and (optionally) its subconcepts. - -The aim of rule templates 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 use template fragments (thus «rule templates»). - -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()` 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). - -``` -write_localVarDecl matching LocalVariableDeclaration lvd -{ - on start - activate - %% - <% loc(@lvd) %> - if (lvd.initializer.isNotNull) { - <% write(@lvd, @lvd) %> - } - %% -} -``` - -A handler is a concept in language `jetbrains.mps.lang.coderules`. - -``` -handler CheckAll extends TypeOf - - checkAll() / 0 - - << … >> -``` - -Keyword `extends` allows to specify another handler, which is extended by this one. 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 rule templates. Handler should declare one or more constraints, unless it only uses the constraints from handlers being extended. Constraint declaration consists of name and arity, which together constitute a *constraint symbol*. Constraint’s arity is fixed. - -Rule templates can specify applicable concept, either exactly or including its subconcepts. One can also declare *standalone* templates, which are triggered automatically on every invocation. - -``` -checkLocalVariable matching VariableDeclaration lvd -apply if { lvd.initializer.isNotNull; } -{ - on - typeOf(@lvd, VariableType), typeOf(@lvd.initializer, InizrType) - activate - convertsTo(InizrType, VariableType) -} -``` - -> Rule template matching concept instances with condition block - - -``` -hasBound_captureOf -{ - on - ~hasBound(CapOfType = captureOfType(ubound: CapUBnd), Bnd) - activate - convertsTo(CapUBnd, Bnd) -} -``` - -> Standalone rule template without input - -The contents of a rule template is a block of code that gets executed when the template is applied to the source model. If the input is specified, the declared parameter is available in the body. - -![](img/errorDialog.png) **TODO what other features are available aside from constraint productions?** - -Constraint productions can be created at any place within the body of a rule template. 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. - -#### Query - -- Query - - [ ] Query kind - - [ ] Parameters - - [ ] Executed block - -#### Macro table - - - Macro table - - [ ] applicable to a node of specific concept - - [ ] macro is not applied automatically - - [ ] what means «expand» and «call» - - [ ] macro parameters - - initializer - - [ ] how macro can be called - - [ ] referring logical variables - - [ ] «macroLogical» expression - - [ ] $-wrapper for an expression - - [ ] «substitution from context» - - [ ] substitutions - - [ ] context parameters - - [ ] specifying parameters using «with» statement - -#### Term table - -- Term table - - [ ] what is a term - - [ ] what are features - - [ ] what are getters - - [ ] terms representing types - - [ ] using terms - - [ ] constructing new terms - - [ ] specify subtterms - - [ ] specify values - - [ ] using terms as patterns - - -#### Constraints processing system - - ![](img/errorDialog.png) **TODO Discuss how constraints processing works (abstractly)** - -- [ ] Terms - - [ ] abstract data structure - - [ ] keeping arbitrary POJO - - [ ] unification -- [ ] Logical variables - - [ ] range of logical var - - [ ] Terms with logical vars - - [ ] unification binds logicals -- [ ] Constraint - - What is a constraint. - - [ ] Constraint arguments. - - [ ] POJO - - [ ] Term - - [ ] Logical vars -- [ ] Constraint production (constraint rule) - - [ ] kept constraints vs. replaced constraints - - [ ] constraint store - - [ ] constraint lifecycle - - [ ] condition for firing a production - - [ ] automatic binding of logicals on firing - - [ ] guard condition - - [ ] predicates - - [ ] arbitrary java code - - [ ] body - - [ ] alternate body - - -## Evaluating constraints program - - ![](img/errorDialog.png) ** TODO executing constraints processing from MPS ** - -## Reactor - - ![](img/errorDialog.png) ** TODO details of constraints processing implementation ** - - diff --git a/docs/evaluating.md b/docs/evaluating.md new file mode 100644 index 00000000..6077162e --- /dev/null +++ b/docs/evaluating.md @@ -0,0 +1,4 @@ +## Evaluating constraints program + + ![](img/errorDialog.png) **TODO executing constraints processing from MPS** + \ No newline at end of file diff --git a/docs/full.md b/docs/full.md new file mode 100644 index 00000000..8245c203 --- /dev/null +++ b/docs/full.md @@ -0,0 +1,13 @@ +# Code Rules + +/intro.md + +/overview.md + +/language.md + +/processing.md + +/evaluating.md + +/reactor.md diff --git a/docs/intro.md b/docs/intro.md new file mode 100644 index 00000000..e9c00856 --- /dev/null +++ b/docs/intro.md @@ -0,0 +1,41 @@ + +## 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). + +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. + +``` +typeOf(assignment.right) :<=: typeof(assignment.left) +``` + +Albeit brief and concise, this notation leaves many questions unanswered when it comes to how exactly the system of equations and inequalities is processed. In other words, type inference is — for the most part — left up to the internal engine to decide. This limits the options for the author of type system to control how exactly subtyping is defined, and what happens with type parameters when computing sub- or supertype. Java, for instance, has several kinds of «conversions» with clearly defined rules controlling how types are transformed and what types are compatible in certain situations. All of this has to be emulated with «strong» and «weak» subtyping in MPS. + +Another example is the all too well known *when_concrete*, which is basically a suspended block that gets executed when the type, that serves as its parameter, is computed. Sometimes this never happens during type inference, which results in numerous «*when concrete is never concrete*» warnings, leaving the user wondering what went wrong. This, however, is very much a necessary evil, since there are no other possibilities to hook into the engine in order to spy on types, and knowing the exact form of a type is sometimes required for further inference. + +Consider how the type of a method call is calculated: the details aside, in essence *when_concrete* has to be applied to the type of each argument. Then we should either turn to inequalities and rely on the inference engine, or analyse the type structure and run closing computation when the *last* unknown type is finalised. + +``` +foreach arg in methodCall.arguments { + when_concrete (typeof(arg) as A) { + // analyse the type of arg, such as extract its parameters, etc + // when all argument types are known, infer the type of call + } +} +``` + +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. + +The following is the list of features made available to users of MPS with *code rules* plugin. + +A language `jetbrains.mps.lang.coderules` containing concept definitions for building rules that serve as production templates, and as regular «checking» rules. The templates may be concept-specific or standalone in order to provide constraints that are invariant for every invocation. + +An extension of CHR[^chr] semantics allowing the use of unification in production 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 the program evaluation. 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. + + +[^mps]: 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/language.md b/docs/language.md new file mode 100644 index 00000000..a6fa80b1 --- /dev/null +++ b/docs/language.md @@ -0,0 +1,242 @@ +## Code rules language + +![](img/errorDialog.png) **TODO This section should teach how to use the language** + +### Root concepts + +| Concept | Description | +|:-- |:-- | +| *Handler* | contains rule templates and constraint declarations | +| *MacroTable* | defines how terms are constructed | +| *Query* | entry point to the constraints program | +| *DataFormTable* [^dft] | defines terms, the data structure that is used in unification | + +### Rule templates + +### Handler + +*Handler* serves two purposes: it declares the constraints that can be used in the *head* of productions in this handler and its extensions, and it also declares *rule templates*, which are, simply put, procedures applicable to specific concept and (optionally) its subconcepts. + +The aim of rule templates 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 use template fragments (thus «rule templates»). + +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()` 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). + +``` +write_localVarDecl matching LocalVariableDeclaration lvd +{ + on start + activate + %% + <% loc(@lvd) %> + if (lvd.initializer.isNotNull) { + <% write(@lvd, @lvd) %> + } + %% +} +``` + +A handler is a concept in language `jetbrains.mps.lang.coderules`. + +``` +handler CheckAll extends TypeOf + + checkAll() / 0 + + << … >> +``` + +> (example of a handler declaration) + +Keyword `extends` allows to specify another handler, which is extended by this one. 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 rule templates. Handler should declare one or more constraints, unless it only uses the constraints from handlers being extended. Constraint declaration consists of name and arity, which together constitute a *constraint symbol*. Constraint’s arity is fixed. + +Rule templates can specify applicable concept, either exactly or including its subconcepts. One can also declare *standalone* templates, which are triggered automatically on every invocation of constraints program. + +``` +checkLocalVariable matching VariableDeclaration lvd +apply if { lvd.initializer.isNotNull; } +{ + on + typeOf(@lvd, VariableType), typeOf(@lvd.initializer, InizrType) + activate + convertsTo(InizrType, VariableType) +} +``` + +> (rule template matching concept instances with condition block) + +A condition, is specified, is checked before applying the rule. + +``` +hasBound_captureOf +{ + on + ~hasBound(CapOfType = captureOfType(ubound: CapUBnd), Bnd) + activate + convertsTo(CapUBnd, Bnd) +} +``` + +> (standalone rule template without input) + +The contents of a rule template is a block of code that gets executed when the template 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 application of templates. + +![](img/errorDialog.png) **TODO what other features are available aside from constraint productions?** + +Constraint productions can be created at any place within the body of a rule template. 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. + +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. + +``` + on + ~compatibleWith(S, T) + activate + convertsTo(S, T) +``` + +> (constraint production declaring logical variables) + +A production with an empty head, that is not declaring any constraints to serve as the 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 `~`. + +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 this binding is the guard and the body of the production. + +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. + +``` + on + ~convertsTo(From, Capture = captureOfType(lbound: LBnd)) + activate + convertsTo(From, LBnd) +``` + +> (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. + +``` + on + typeOf(@ifs.condition, Condition) + activate + BoolType := call booleanType<>, convertsTo(Condition, BoolType) +``` + +> (example of a constraint argument referring to a location) + +Whereas the production’s head can only contain constraints, there are also other logical clauses that are used in the guard and the body. + +A *predicate* is a built-in construct that serves two purposes: when used in the guard, it serves to query if a condition is satisfied, and when used in the body it asserts this condition. An example is `unifies` predicate displayed as `=`, which tests if its arguments can be unified. There are also predicates that can only be queries, such as `isFree()` or `isBound()` 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. + +``` + on + ~containedIn(S, T) + when + isBound(S), isBound(T), S = T + activate + S = T +``` + +> (`unifies` predicate used in the guard and in the body) + +Arbitrary Java code can be called with `eval()` predicate. It accepts either an expression of `boolean` type, in which case it can be used in the guard, or expression of any type, such as static method call, which can be inserted in the body. + +``` + on Node, term Type> + recoverAll(), typeOf(@op, Type) + activate + recover(Node, Type), eval(op._type_.set(valueOf(Node))) +``` + +> (example of using `eval()` predicate) + +![](img/errorDialog.png) **TODO Expand/call pseudo predicates** + +![](img/errorDialog.png) **TODO Code templates within production body** + +![](img/errorDialog.png) **TODO Alternative body** + +#### Query + +![](img/errorDialog.png) **TODO** + +Query is the entry point to a constraint program. The only purpose of a query is to activate constraints that trigger computation defined by productions created by handlers. + +``` +query Typecheck +parameter: << ... >> + +kind: TypecheckingQueryKind.TYPECHECK + + check + + on start + activate + checkAll(), recoverAll() +``` + +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. + +#### Macro table + +![](img/errorDialog.png) **TODO** + +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 rule templates, 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. + +Macros are defined in a root `Macro table`. + +``` +macro table Types + +macro classifierType expands node classifierType + node cls1 = classifierType.classifier; + nlist<> arguments = classifierType.parameter; + + produce + %% + … + %% +``` + +> (macro table with a macro definition) + +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. + +![](img/errorDialog.png) **TODO 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. + +![](img/errorDialog.png) **TODO substitutions** + +#### DataForm table + +DataForm table contains *data form* declarations, a.k.a. *terms*. A term is a simple recursive data type that is suitable for implementing unification. Also, terms can model any other data structure, in particular they are suitable for representing types in a programming language. + +Data form is defined by its symbol and its features, which can be a POJO, a child data form, or a list of data forms. A feature may have a default value provider. A data form extending another data form adds new features or provides default values for existing ones. + +``` +classifierType ( + value classifier + value kind + list parameter +) +``` + +``` +longType : primType ( + final value kind = concept/LongType/ + value val = 0L +) +``` + +> (examples of *data form* declarations) + +![](img/errorDialog.png) **TODO terms** + + +[^dft]: this concept is defined in another language, `jetbrains.mps.logic` diff --git a/docs/overview.md b/docs/overview.md new file mode 100644 index 00000000..fc45709f --- /dev/null +++ b/docs/overview.md @@ -0,0 +1,76 @@ +## Overview + +Analysis of source code (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. The contents of code rules aspect model is a contribution of this particular language. All templates are applied to the source code, with templates 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 textual representation. Aside from generating productions, the rules can also process the model normally, reporting errors as usual. + +This 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 second phase is evaluation of the constraints program that was created in phase one. The 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. + +``` +query ConvertsTo +parameter: node<> from, node<> to +kind: TypecheckingQueryKind.CONVERT + + on start + activate + A := expand from, B := expand to, convertsTo(A, B) +``` + +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()` 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, 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 constraints: + +``` +on start + activate + checkAll(), recoverAll() +``` + +Here, the first constraint `checkAll()` fires type checking, whereas the second `recoverAll()` 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. + +``` +on start + activate + checkAll() + else + recoverAll() +``` + +Here, `recoverAll()` constraint is moved out to an «*alternative branch*» of production body, which allows it to be activated even if there was an error while processing the main branch. + +To illustrate how automatic binding of logical variables work, consider the following example. The constraint `typeOf()` associates a type with a location in source code, and `convertsTo()` ensures its 1st argument can be converted to the 2nd, which must both be types. + +``` +assignmentExpression matching AssignmentExpression ae +{ + on + typeOf(@ae.lValue, LType), typeOf(@ae.rValue, RType) + activate + convertsTo(RType, LType) +} +``` + +The production is triggered when both locations referred to by `ae.lValue` and `ae.rValue` have their types assigned, as both `typeOf()` constraints must be present for a match to be successful. Once production’s head is matched, both logical variables `LType` and `RType` become bound to whatever was the 2nd argument of first and second `typeOf()` constraint, respectively. + +It’s important to note, that although on successful match both `lValue` and `rValue` have types, it’s not guaranteed that these types are *ground*. A type may be represented by a free logical variable, or a term containing free variables. Another very important thing to notice is that a logical variable enjoys full privileges of being an argument to a constraint. Which means, if in the above example both variables are free, and `LType = RType`, then both locations will have essentially the *same* type (in the sense of «same instance»), not just matching types. + +The following example illustrates the use of *pattern matching* in production’s head. Here the first argument to constraint `convertsTo()` in the head is a logical variable with pattern expression. In this case the production will only be triggered if the active constraint’s first argument is not a free variable, and it matches the pattern. + +``` +converts_captureOf_upperBound +{ + on + ~convertsTo(Capture = captureOfType(ubound: UBnd), To) + activate + convertsTo(UBnd, To) +} +``` + diff --git a/docs/processing.md b/docs/processing.md new file mode 100644 index 00000000..5ceb6101 --- /dev/null +++ b/docs/processing.md @@ -0,0 +1,81 @@ +## 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]. + +### 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. + +``` + f(g(), h(k())) + + p(val("foo"), q()) + + node(name("List"), arg(node(name("Int"), arg()))) +``` + +> (examples of terms) + +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$. + +``` + [X -> g()] unifies f(X, h(X)) and f(g(), h(g())) + + f(X, h(X)) and f(g(), h(k())) can't be unified +``` + +### 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. + +``` + val X = Logical("X") + val Y = Logical("Y") + + assertTrue(X.isFree() && y.isFree()) + + X.set("foo") + assertTrue(X.value() == "foo")) + + Y.union(X) + + assertTrue(Y.find() == X) + assertTrue(Y.find().value() == "foo") +``` + +> (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. + +``` + val X = Logical("X") + val t1 = term("f", var(X), term("g", var(X))) + val t2 = term("f", term("h"), term("g", term("h"))) + + assertTrue(X.isFree()) + + val substitution = t1.unify(t2) + + assertTrue(substitution.isValid()) + assertTrue(X.find().value() == term("h")) +``` + + +### Constraints and predicates + +![](img/errorDialog.png) **TODO** + + + + + +### Constraint production (rule) + +![](img/errorDialog.png) **TODO** + +[^jchr]: https://dtai.cs.kuleuven.be/CHR/JCHR/ +[^uf]: https://en.wikipedia.org/wiki/Disjoint-set_data_structure \ No newline at end of file diff --git a/docs/reactor.md b/docs/reactor.md new file mode 100644 index 00000000..8f086e41 --- /dev/null +++ b/docs/reactor.md @@ -0,0 +1,10 @@ + +## Reactor + + ![](img/errorDialog.png) **TODO details of constraints processing implementation** + +- [ ] Production matching algorithm + - [ ] Propagation history +- [ ] Constraints store +- [ ] Persistent stack frame +- [ ] Processing of evaluation failuress \ No newline at end of file diff --git a/docs/todo-evaluating.md b/docs/todo-evaluating.md new file mode 100644 index 00000000..8d89543f --- /dev/null +++ b/docs/todo-evaluating.md @@ -0,0 +1,12 @@ +### 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/todo-full.md b/docs/todo-full.md new file mode 100644 index 00000000..4b5c74e1 --- /dev/null +++ b/docs/todo-full.md @@ -0,0 +1,13 @@ +# Code Rules + +/todo-intro.md + +/todo-overview.md + +/todo-language.md + +/todo-processing.md + +/todo-evaluating.md + +/todo-reactor.md diff --git a/docs/todo-language.md b/docs/todo-language.md new file mode 100644 index 00000000..e0ae095e --- /dev/null +++ b/docs/todo-language.md @@ -0,0 +1,62 @@ +### Handler +- [x] create handler, optionally extend another handler +- [x] declare constraints +- [ ] define rule template + - [x] for concept, standalone + - [x] applicability condition + - [ ] what purpose does the body serve + - [ ] **reporting errors** + - [ ] **_require_ statement** + - [ ] **what features are available in a rule** +- [ ] introduce constraint production + - [x] declare logical variables + - [x] on start + - [ ] on … defining *head* + - [x] keep / replace (~) + - [x] pattern matching + - [x] the '@' syntax + - [ ] predicates vs constraints + - [ ] **special predicates «expand» and «call»** + - [x] calling arbitrary Java code (eval) + - [ ] guard (when) + - [x] what operations are available in the guard + - [ ] body + - [x] what operations are available in the body + - [ ] **using code templates** `%% … %%` + - [ ] **alternative body** + +### Query +- [x] Purpose of a query +- [x] Query kind +- [x] Parameters +- [x] Executed block + +### Macro table + - [x] applicable to a node of specific concept + - [x] macro is not applied automatically + - [x] macro parameters + - [x] parameter initialiser + - [ ] how macro can be called + - [ ] **special predicates «expand» and «call»** + - [x] What is the meaning of macro body + - [ ] referring logical variables + - [x] «macroLogical» expression + - [ ] **$-wrapper for an expression** + - [ ] **«substitution from context»** + - [ ] context parameters + - [ ] substitutions + - [ ] context parameters + - [ ] specifying parameters using «with» statement + +### Term table +- [x] purpose of this root +- [ ] what is a term + - [x] what are features + - [x] what are getters + - [x] extending another term +- [ ] terms representing types +- [ ] using terms + - [ ] constructing new terms + - [ ] specify subtterms + - [ ] specify values + - [ ] using terms as patterns diff --git a/docs/todo-processing.md b/docs/todo-processing.md new file mode 100644 index 00000000..64ae0051 --- /dev/null +++ b/docs/todo-processing.md @@ -0,0 +1,35 @@ +### 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 +