From 427ec8f4efb9115c87d338eaaa3ee79a912b405c Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Thu, 23 Aug 2018 15:02:19 +0200 Subject: [PATCH] Cleanup and reorder docs for printing all pages. Metadata --- docs/_assets/mdl.css | 7 +++++++ docs/_config.yml | 3 ++- docs/_layouts/print.html | 2 ++ docs/_layouts/welcome.html | 4 ++++ docs/content/allpages.md | 8 ++++++++ docs/content/contacts.md | 2 +- docs/content/evaluating.md | 15 +++++++------- docs/content/example-controlflow.md | 2 +- docs/content/example-logic.md | 16 +++++++-------- docs/content/example-typechecking.md | 23 +++++++++++----------- docs/content/intro.md | 2 ++ docs/content/language.md | 1 + docs/content/overview.md | 1 + docs/content/processing.md | 29 ++++++++++++++-------------- docs/content/reactor.md | 11 ++++++----- 15 files changed, 77 insertions(+), 49 deletions(-) create mode 100644 docs/content/allpages.md diff --git a/docs/_assets/mdl.css b/docs/_assets/mdl.css index 3923fc73..bbbe4a14 100644 --- a/docs/_assets/mdl.css +++ b/docs/_assets/mdl.css @@ -47,6 +47,13 @@ font-size: 16px; } +.metadata { + text-align: right; + line-height: 8px; + padding-bottom: 0px; + color: rgb(158,158,158); +} + .homepage { display: flex; position: relative; diff --git a/docs/_config.yml b/docs/_config.yml index 4288fb9c..5d306be0 100644 --- a/docs/_config.yml +++ b/docs/_config.yml @@ -8,7 +8,8 @@ baseurl: "/mps-coderules" # the subpath of your site, e.g. /blog url: "https://fisakov.github.io" # the base hostname & protocol for your site, e.g. http://example.com twitter_username: jetbrains_mps github_username: fisakov -time: 2018-08-05 +time: 2018-08-23 +revision: 0.5.0 copyright: JetBrains s.r.o. copyright_url: "https://jetbrains.com" homepage: "https://jetbrains.com/mps" diff --git a/docs/_layouts/print.html b/docs/_layouts/print.html index e01441aa..8b612c21 100644 --- a/docs/_layouts/print.html +++ b/docs/_layouts/print.html @@ -15,6 +15,8 @@ {{ content }} +

Revision: {{ site.revision }}

+

Date: {{ site.time | date: "%-d %b, %Y" }}

{% assign sorted_pages = site.pages | sort: 'weight' %} {% for p in sorted_pages %} {% if p.menu != false and p.weight != nil %} diff --git a/docs/_layouts/welcome.html b/docs/_layouts/welcome.html index 08605cf7..65e162dc 100644 --- a/docs/_layouts/welcome.html +++ b/docs/_layouts/welcome.html @@ -28,3 +28,7 @@ layout: default +
+

Revision: {{ site.revision }}

+

Date: {{ site.time | date: "%-d %b, %Y" }}

+
diff --git a/docs/content/allpages.md b/docs/content/allpages.md new file mode 100644 index 00000000..b6eccf0e --- /dev/null +++ b/docs/content/allpages.md @@ -0,0 +1,8 @@ +--- +layout: print +menu: false +--- + +Revision: 0.5.0 + +Date: Aug 23, 2018 diff --git a/docs/content/contacts.md b/docs/content/contacts.md index c6070dbe..bf992030 100644 --- a/docs/content/contacts.md +++ b/docs/content/contacts.md @@ -2,7 +2,7 @@ layout: page title: Contacts menu: Contacts -weight: 890 +weight: 800 --- # Contacts diff --git a/docs/content/evaluating.md b/docs/content/evaluating.md index 4a56370f..3dd7d86f 100644 --- a/docs/content/evaluating.md +++ b/docs/content/evaluating.md @@ -3,23 +3,24 @@ layout: page title: Evaluating Code Rules weight: 40 --- + # Evaluating Code Rules ***Two stage process*** - + ## Aspects ***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. +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 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. +Generated productions constitute the constraints program, which is then executed. ## Running constraints program @@ -27,11 +28,11 @@ In the second stage the constraints program is run. To begin execution, a query ***Order of productions firing*** -Order of productions fired: - - on start +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. +While constraints program is run, it is allowed to report feedback, such as assign calculated types or report problems, using special predicates. ***Feedback predicates example*** diff --git a/docs/content/example-controlflow.md b/docs/content/example-controlflow.md index 1fbffc76..1affc641 100644 --- a/docs/content/example-controlflow.md +++ b/docs/content/example-controlflow.md @@ -3,7 +3,7 @@ layout: page title: Control Flow Analysis of BaseLanguage menu: Control Flow BL parent: examples -weight: 510 +weight: 520 --- # Control Flow Analysis diff --git a/docs/content/example-logic.md b/docs/content/example-logic.md index 9d5acb2d..0c765bbe 100644 --- a/docs/content/example-logic.md +++ b/docs/content/example-logic.md @@ -11,28 +11,28 @@ github-path: /tree/master/samples/fitch This example demonstrates the use of *code rules* to implement validation of logical proofs written using Fitch system. The idea of this implementation originates in the proof checking tool provided as part of an inroductory course on logic by Stanford University[^inlog]. This overview serves for quick introduction, and more detailed information can be found at project’s home page (see the link on top of this page). -The four languages in this example define the structure of proofs (samples.fitch), the structure of three kinds of logic: Propositional logic, Herbrand logic, and First Order logic (samples.fitch.*logic). +The four languages in this example define the structure of proofs (samples.fitch), the structure of three kinds of logic: Propositional logic, Herbrand logic, and First Order logic (samples.fitch.*logic). -The proof structure allows for building hierarchical proof trees, which are necessary for Implication Introduction rule, and interprets the leafs as reasonings, which can be either assumptions or judgements. The beginning of the proof contains all the premises, and the final top-level node is the goal. +The proof structure allows for building hierarchical proof trees, which are necessary for Implication Introduction rule, and interprets the leafs as reasonings, which can be either assumptions or judgements. The beginning of the proof contains all the premises, and the final top-level node is the goal. ![](img/ex-logic-contrapositive-450.png) _(example of proof in Fitch system)_ -Base inference rules are defined by `samples.fitch.propositionalLogic` language, with two other extending the set of rules appropriately. Herbrand logic extends this language with relations, functions, and quantifiers, whereas First Order logic adds equality. Each of the logics also define their own root proof concept. +Base inference rules are defined by `samples.fitch.propositionalLogic` language, with two other extending the set of rules appropriately. Herbrand logic extends this language with relations, functions, and quantifiers, whereas First Order logic adds equality. Each of the logics also define their own root proof concept. -The proof validation is done through type checking with the only type being «Ok». There is one query of kind `TYPECHECKING`, which simply activates `checkAll()`. Every logical formula from reasonings is translated into a dataform, with logical variables taking place of quantifier variables. +The proof validation is done through type checking with the only type being «Ok». There is one query of kind `TYPECHECKING`, which simply activates `checkAll()`. Every logical formula from reasonings is translated into a dataform, with logical variables taking place of quantifier variables. -Each reasoning has a *conclusion*, which is expanded to term and assigned to the source location with `conclusion()` constraint. In addition, at the start, all proof’s premises are marked as valid using `valid()`. The process then continues recursively, with every inference rule constructed according to a single pattern: -- the head ensures the conclusions of all rule’s *bases* (input premises) match the required form, +Each reasoning has a *conclusion*, which is expanded to term and assigned to the source location with `conclusion()` constraint. In addition, at the start, all proof’s premises are marked as valid using `valid()`. The process then continues recursively, with every inference rule constructed according to a single pattern: +- the head ensures the conclusions of all rule’s *bases* (input premises) match the required form, - the rule’s conclusion matches the required form, and - all the bases are *valid*. ![](img/ex-logic-andintro-650.png) _(example of an inference rule)_ -The rule’s body activates `valid()` constraint, therefore only reasonings that have met the requirement are marked as valid. Check handler marks reasonings that weren’t validated as erroneous. +The rule’s body activates `valid()` constraint, therefore only reasonings that have met the requirement are marked as valid. Check handler marks reasonings that weren’t validated as erroneous. -Finally, if the proof’s goal is marked valid, it is assigned «Ok» type, otherwise it is marked with error. +Finally, if the proof’s goal is marked valid, it is assigned «Ok» type, otherwise it is marked with error. [^inlog]: Stanford Introduction to Logic http://logic.stanford.edu/intrologic/homepage/index.html diff --git a/docs/content/example-typechecking.md b/docs/content/example-typechecking.md index 16b379b8..62b02ea3 100644 --- a/docs/content/example-typechecking.md +++ b/docs/content/example-typechecking.md @@ -3,19 +3,19 @@ layout: page title: Typechecking BaseLanguage menu: Typechecking BL parent: examples -weight: 500 +weight: 510 github-path: /tree/master/samples/mpscore --- # Typechecking BaseLanguage -Short explanation of the architecture of BL-specific type system built with *code rules*. +Short explanation of the architecture of BL-specific type system built with *code rules*. This sample is the main result of developing code rules. It is still work in progress, but the main areas of typechecking BaseLanguage have been covered. Here we briefly touch on the implementation details. First, all the BaseLanguage types have corresponding dataforms, and in addition there are definitions of types that are only ever used during typechecking, such as capture type. -The macros in `Types` macro table define the rules how types are constructed, ensuring, among other things, that bounds on type parameters are correctly processed. +The macros in `Types` macro table define the rules how types are constructed, ensuring, among other things, that bounds on type parameters are correctly processed. ![](img/ex-typecheck-terms-300.png) _(examples of type dataforms)_ @@ -35,7 +35,7 @@ _(the production from `Typecheck` query)_ Typechecking itself starts with activating of `checkAll()` constraint, triggering the productions responsible for assigning types to literals, `this` expression, as well as processing type annotations — ensuring that these are built without violating bounds. -The rule for variable declaration is quite trivial: the type annotation gets expanded to dataform and assigned to the source location with `typeOf()` constraint. +The rule for variable declaration is quite trivial: the type annotation gets expanded to dataform and assigned to the source location with `typeOf()` constraint. ![](img/ex-typecheck-vardecl-750.png) _(assigning the type to a variable declaration)_ @@ -45,7 +45,7 @@ An integer literal is simply assigned the type `int` with the value being the va ![](img/ex-typecheck-intliteral-700.png) _(assigning the type to `int` literal)_ -From these starting points typechecking continues up the syntax tree until there are no more productions left that can be triggered. +From these starting points typechecking continues up the syntax tree until there are no more productions left that can be triggered. A `dot expression` propagates the type from operation to the whole expression. @@ -59,7 +59,7 @@ _(typechecking of assignment expression)_ ## Type Relations -Several kinds of relations on types are defined, surveyed in the following table. +Several kinds of relations on types are defined, surveyed in the following table. | Relation | Constraint | Description | |:--|:--|:--| @@ -83,16 +83,16 @@ _(`convertsTo()` delegates to `promote()` for classifier type)_ ### Subclassing -Resolution of `promote()` constraint, which represents subtyping among classifier types, is implemented around a simple idea of representing all subclass paths the root (Object) to a classifier as a set of lists. This representation deliberately ignores the class parameters. As a first step, the shortest path from supertype’s classifier to subtype’s one is selected. This path is then reversed and represented as a dataform list. This makes it possible to pattern-match on this list, since it is nothing more than a cons list represented as a dataform. +Resolution of `promote()` constraint, which represents subtyping among classifier types, is implemented around a simple idea of representing all subclass paths the root (Object) to a classifier as a set of lists. This representation deliberately ignores the class parameters. As a first step, the shortest path from supertype’s classifier to subtype’s one is selected. This path is then reversed and represented as a dataform list. This makes it possible to pattern-match on this list, since it is nothing more than a cons list represented as a dataform. Subtyping is a reflexive and transitive relation, so `promote()` is replaced with another constraint `dpromote()`, which triggers one of the two productions responsible for either aspect of the relation. Transitivity is solved by advancing up the supertype path keeping track of all type variables and ensuring all bounds on type parameter are satisfied. Reflexivity delegates to `containedIn()` to ensure parameters are within bounds, which in its turn delegates to `convertsTo()`. -Take a simple example of `Long` classifier type — the boxed `long`. Its superclasses are written as follows. +Take a simple example of `Long` classifier type — the boxed `long`. Its superclasses are written as follows. ``` Long : Comparable : Object Long : Number : Serializable : Object -``` +``` Suppose we need to decide if `Long <: Serializable`, that is if `Long` is a subtype of `Serializable`. The shortest path between those consists of three nodes : `[Long, Number, Serializable]`. Constraint `dpromote()` is activated with this list as the 3rd parameter, and it requires two steps of inductive production and one step of reflexive to solve this relation. @@ -129,7 +129,7 @@ Suppose we need to decide if `Long <: Serializable`, that is if `Long` is a subt - method call - **type parameter substitutions** - equals/assignment/+assignment - - + - - ??? - method declaration - type relations @@ -144,5 +144,4 @@ Suppose we need to decide if `Long <: Serializable`, that is if `Long` is a subt - type annotations - classifier type - type parameters: type var, bound type, wildcard - - - + - diff --git a/docs/content/intro.md b/docs/content/intro.md index 3ba09bf4..2fb62954 100644 --- a/docs/content/intro.md +++ b/docs/content/intro.md @@ -3,6 +3,7 @@ layout: page title: Introduction 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). @@ -36,3 +37,4 @@ Finally, an embedded engine capable of processing constraints, which accepts a l [^mps]: Meta Programming System [https://jetbrains.com/mps](https://jetbrains.com/mps) [^chr]: Constraint Handling Rules [http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/constraint-handling-rules-book.html](http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/constraint-handling-rules-book.html) + diff --git a/docs/content/language.md b/docs/content/language.md index 25e1642b..6065eccf 100644 --- a/docs/content/language.md +++ b/docs/content/language.md @@ -3,6 +3,7 @@ layout: page title: Code Rules Language weight: 30 --- + # Code Rules Language ***This section should teach how to use the language*** diff --git a/docs/content/overview.md b/docs/content/overview.md index 7760531d..8c4f242e 100644 --- a/docs/content/overview.md +++ b/docs/content/overview.md @@ -3,6 +3,7 @@ layout: page title: Overview weight: 20 --- + # 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 612e34eb..175bb3e0 100644 --- a/docs/content/processing.md +++ b/docs/content/processing.md @@ -4,6 +4,7 @@ title: Constraints Processing System menu: Processing Constraints weight: 50 --- + # Constraints Processing System ***Discuss how constraints processing works (abstractly)*** @@ -70,13 +71,13 @@ 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 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. +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 its head constraints to be «replaced», causes these to be terminated. ![](img/constraint-lifecycle.svg) _(lifecycle of a constraint)_ @@ -89,15 +90,15 @@ Whereas a constraint serves to embody a relation among objects simply by being a ***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). +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 ask/tell*** ## Constraint production (rule) -Constraints program is built from productions. Each production has three parts: the part that is responsible for triggering the production, called «head», the part that checks for pre-conditions, called «guard», and the part that is evaluated when production is fired, which is called «body». +Constraints program is built from 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. +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. @@ -110,7 +111,7 @@ There is some terminology inherited from CHR that can be useful when discussing Guard is a conjunction of predicates, which are checked before a match of available constraints with the production’s head is considered successful. Predicates in a guard are *queried*. -Body is a conjunction of predicates and constraint activations. When evaluated, each body clause is evaluated in order, with predicates serving as *assertions* and constraint activations producing new constraints. Each newly activated constraint is checked against any productions that can be fired, and so on. +Body is a conjunction of predicates and constraint activations. When 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. ***Alternative body*** @@ -118,22 +119,22 @@ Body is a conjunction of predicates and constraint activations. When evaluated, 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. +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 \Leftrightarrow C | G)^L := + !\forall((!C^L) \multimap (E^L \multimap \exists\bar{y}G^L)) \\] -Propagation is different from simplification in that the set of constraints $E$, which triggered the production, is made available together with the constraints produced by the body, so the constraints in $E$ are not «consumed». +Propagation is different from simplification in that the set of constraints $E$, which triggered the 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 \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 +[^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. diff --git a/docs/content/reactor.md b/docs/content/reactor.md index 9a8ece01..00f876c8 100644 --- a/docs/content/reactor.md +++ b/docs/content/reactor.md @@ -4,22 +4,23 @@ title: Constraints Reactor parent: content/processing.md weight: 55 --- + # Constraints Reactor ***Details of constraints processing implementation*** 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]. +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. +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. @@ -34,4 +35,4 @@ Logical variables serving as constraint arguments trigger reactivation of such c 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 +[^trie]: Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier Sci. Pub. B. V., Amsterdam, The Netherlands, The Netherlands. Chapter 26.