diff --git a/.mps/.name b/.mps/.name index ba33f6a0..8a0509e2 100644 --- a/.mps/.name +++ b/.mps/.name @@ -1 +1 @@ -constraints-typechecking +coderules diff --git a/INSTALL.txt b/INSTALL.txt new file mode 100644 index 00000000..cf766f7b --- /dev/null +++ b/INSTALL.txt @@ -0,0 +1,20 @@ +# INSTALL # + +Prerequisites: + +- Oracle JDK 1.8 +- Maven 3 + +## To fully build and test the project execute: ## + + mvn -Dmaven.javadoc.skip=true -B -f reactor install && ./gradlew check + +This builds the «reactor» project and installs its artefacts into local Maven repository. Then the regular Gradle build is launched. Further launches of Gradle can be done without running the build in «reactor». + +## To install all the dependencies in order to open the project with MPS: ## + + mvn -Dmaven.javadoc.skip=true -B -f reactor install && ./gradlew init + +Once the project is opened, execute «Rebuild», since generated artefacts are excluded from version control + +**NOTE: ** in order to open any of the sample projects follow the steps above for building the whole project, as samples expect the compiled languages to be available in a project library. diff --git a/README.md b/README.md index 05d00e6c..9a0036ba 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,8 @@ -# Type Checking with Constraint Rules +![](doc/img/mps-logo.png) -An experimental feature for [JetBrains MPS](https://jetbrains.com/mps) implementing a better type checking and type inference using constraint rules. +# Code Rules + +An experimental feature of [JetBrains MPS](https://jetbrains.com/mps). Code rules allow to create various code analyses employing constraints handling. The examples are provided, including type checking and control flow analysis of code written using MPS’s baseLanguage. ## Status @@ -10,79 +12,37 @@ The status of this project is **pre-release**. Don’t rely on any of the langua ## Overview -This project is the result of the research done within the MPS team in the area of code analysis using constraint rules, in particular [CHR](http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/constraint-handling-rules-book.html). +This project is the result of ongoing research done within MPS team in the area of code analysis using constraints handling, in particular [CHR](http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/constraint-handling-rules-book.html). -Typing rules serve as templates that produce constraint rules. Both transformation to constraint rules and evaluating is done in-memory at the time type checking is launched. Constraint rules are processed by the embedded [engine](https://github.com/fisakov/conreactor). +Code rules serve as templates that produce constraint rules. Both transformation to constraint rules and evaluating is done in-memory at the time analysis is launched. Constraint rules are processed by the embedded [engine](reactor). -The source code also contains the typing rules for *baseLanguage*, which serve to demonstrate how the various type inference problems are solved. +Samples included with this project demonstrate how *coderules* can be used for solving concrete tasks connected with source code analysis. -## Features +- [Type checking of lambda calculus](samples/lambdacalc) shows the implementation of standard type checking algorithm. +- [Proof validation](samples/fitch) using Fitch system demonstrates how logical inference can be done. +- [Type checking and control flow analysis](samples/mpscore) for core MPS languages. -The language *jetbrains.mps.typesystem2* enables to write typing rules. A custom aspect «types» is used to store the typing rules in the language source code. +*Coderules* allow for extensions to be provided by derived languages. Extensions have higher priority, so it’s easy to override the built-in behaviour. -![Example of a typing rule](/doc/img/typing-rule-example.png) +The semantics of constraints handling is compatible with regular Java semantics, so *coderules* can be safely embedded into the user code. There also exists support for launching arbitrary code from when processing constraints. -Type checking plugin for MPS provides the actions for checking the types in a currently opened root. +Parallel or background execution of *coderules* is possible thanks to the reactive extensions, in particular rxjava, which is used by the implementation. -![](/doc/img/menu-example.png) - -Constraints activation trace view for debugging the process of evaluating constraint rules. - -![Activation trace](/doc/img/activation-trace-example.png) - -Once finished, the constraint rules produce the inferred types and type errors, which are added as highlighter annotations to the editor. - -![](doc/img/type-annotation-example.png) +See [implementation notes](coderules/README.md) for more information. ## Dependencies The source code can be opened with the latest version of JetBrains MPS. The plugin that is created with the build script is also compatible with the same version of MPS. +## Project structure + +- **reactor** - contains the implementation of constraint processing engine +- **coderules** - implementation and tests +- **samples** - sample projects using *coderules* + ## Installation -The easiest way to install the plugin is by using the update mechanism built in to JetBrains MPS. - -1. Open the Preferences dialog and select Plugins on the left -2. In the panel on the right select Browse Repositories… -3. In the dialog that appears select Manage Repositories… -4. Add a new repository with the following url: -``` -https://raw.githubusercontent.com/fisakov/constraints-typechecking/updates/updatePlugins.xml -``` -5. The list of plugins should be refreshed and the new plugin «typechecking» should appear -6. Install the plugin and restart the application. - -Alternatively, the plugin can be installed manually. See the downloads section of the latest release for the plugin archive. This archive has to be unpacked to the MPS plugins folder on your local drive. For example (using macOS): - -`unzip typechecker-0.2.zip -d ~/Library/Application\ Support/MPS2017.2/` - -## Hacking - -The project is built using [gradle](http://www.gradle.org). To work with the source code, follow these steps: - -1. Install JetBrains MPS using [this link](https://jetbrains.com/mps/download). -2. Clone this repository to your local drive. -3. [optional] In the project folder put a *symlink* called «MPS_HOME» that leads to the MPS home folder: - - `ln -s /Applications/MPS\ 2017.1.app/Contents MPS_HOME` - - By doing so you skip unpacking the MPS distribution by the gradle script. - -4. Run gradle using the following command to generate all models: - - `./gradlew generate` - - In order to execute full build, including artefacts, run this command: - - `./gradlew build` - - If you want to run the tests as well as building the project, execute this instead: - - `./gradlew test` - -5. The project is now ready to be opened with MPS. - - NOTE: every time the source tree is cleaned, for example with `git clean` command, the gradle script has to be run in order to download the necessary libraries. +See [INSTALL.txt](INSTALL.txt). ## License diff --git a/coderules/README.md b/coderules/README.md new file mode 100644 index 00000000..d6c37168 --- /dev/null +++ b/coderules/README.md @@ -0,0 +1,37 @@ +# Code Rules - Implementation Notes + + + +## Structure + +The project modules are separated into several groups to separate levels of abstraction. + +#### Logic + +Define fundamental ideas used throughout the implementation, such as «data form» (a.k.a. term), logical variables, and others. + +#### Code rules + +Modules in this group define the core concepts of *coderules* and the logic behind it. This includes constraints, predicates, handlers, as well as code rule templates. + +Constraints activation trace view for debugging the process of evaluating constraint rules. + +![Activation trace](/doc/img/activation-trace-example.png) + +Once finished, constraint rules produce inferred types and type errors, which are added as highlighter annotations to the editor. + +![](doc/img/type-annotation-example.png) + +#### Type checking + +Defines a custom aspect «types», which is used to store the typing rules in the language source code. + +![Example of a typing rule](/doc/img/typing-rule-example.png) + +Type checking plugin for MPS provides the actions for checking the types in a currently opened root. + +![](/doc/img/menu-example.png) + +#### Control flow + +Declares only control flow aspect. All functionality is inherited from *coderules* language. diff --git a/doc/img/activation-trace-example.png b/coderules/doc/img/activation-trace-example.png similarity index 100% rename from doc/img/activation-trace-example.png rename to coderules/doc/img/activation-trace-example.png diff --git a/doc/img/menu-example.png b/coderules/doc/img/menu-example.png similarity index 100% rename from doc/img/menu-example.png rename to coderules/doc/img/menu-example.png diff --git a/doc/img/type-annotation-example.png b/coderules/doc/img/type-annotation-example.png similarity index 100% rename from doc/img/type-annotation-example.png rename to coderules/doc/img/type-annotation-example.png diff --git a/doc/img/typing-rule-example.png b/coderules/doc/img/typing-rule-example.png similarity index 100% rename from doc/img/typing-rule-example.png rename to coderules/doc/img/typing-rule-example.png diff --git a/doc/img/mps-logo.png b/doc/img/mps-logo.png new file mode 100644 index 00000000..c713da58 Binary files /dev/null and b/doc/img/mps-logo.png differ diff --git a/reactor/README.md b/reactor/README.md index 718541e6..402f5d80 100644 --- a/reactor/README.md +++ b/reactor/README.md @@ -4,8 +4,6 @@ An engine for evaluating constraint rules. Written in Kotlin and Java. -[![Build Status](https://travis-ci.org/fisakov/conreactor.svg?branch=master)](https://travis-ci.org/fisakov/conreactor) - This is an implementation of the [Constraint Handling Rules](http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/constraint-handling-rules-book.html) semantics with custom extensions, influenced by [JCHR](https://dtai.cs.kuleuven.be/CHR/JCHR/). The main features are built-in support for **terms** as the data structure, including terms **unification**, and **logical variables**. diff --git a/samples/fitch/README.md b/samples/fitch/README.md index dbc6d091..175ca28b 100644 --- a/samples/fitch/README.md +++ b/samples/fitch/README.md @@ -1,15 +1,15 @@ -# Fitch system +# Fitch proofs This project demonstrates the use of type checking to validate proofs in [Propositional Logic](http://logic.stanford.edu/intrologic/glossary/propositional_logic.html), as well as [Herbrand Logic](http://logic.stanford.edu/intrologic/glossary/herbrand_logic.html) and [First Order Logic](http://logic.stanford.edu/intrologic/extras/fol.html). The proof system is [Fitch](http://logic.stanford.edu/intrologic/glossary/fitch_system.html). -This project is developed with [JetBrains MPS](https://www.jetbrains.com/mps/) using the [plugin](https://github.com/fisakov/constraints-typechecking) that provides an experimental feature: *type checking with constraint rules*. +This project is developed with [JetBrains MPS](https://www.jetbrains.com/mps/) with *coderules* experimental extension. -### Instructions +### Installation -1. Install the latest version of [JetBrains MPS](https://www.jetbrains.com/mps/download). -2. Download the type checking plugin from [this](https://github.com/fisakov/constraints-typechecking) project (follow the instructions there for installing the plugin using either update mechanism or manually) -3. Clone this repository and open the project with MPS -4. Execute 'Rebuild Project' +The code in this project relies on *coderules* languages and solutions to be available, either as a project library or as a plugin. There are two possibilities to install coderules: + +1. Follow the instructions for building the root project, or +2. Install the compiled plugin (see the latest release on GitHub). ### Using the proof checker @@ -227,3 +227,19 @@ The proof’s goal is unified with the last **top-level** reasoning. Since reaso The actual type checking is trivial. The first stage of the constraint rules program does all the job and produces `valid` constraints, which are to be analysed in the second stage. All reasonings are checked in the second stage, and the reasonings that don’t have `valid` constraint are marked with error. There is only one type «OK». Only the goal gets assigned a type in case it marked as `valid`, otherwise an error is produced. + +## License + +Copyright 2014-2018 JetBrains s.r.o. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + +http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. diff --git a/samples/lambdacalc/README.md b/samples/lambdacalc/README.md index 487fe523..66dc0947 100644 --- a/samples/lambdacalc/README.md +++ b/samples/lambdacalc/README.md @@ -2,16 +2,27 @@ This is a demo of type checking simply typed lambda calculus using constraint rules. -This project is made with [JetBrains MPS](https://www.jetbrains.com/mps/) using the [plugin](https://github.com/fisakov/constraints-typechecking) that provides an experimental feature: type checking with constraint rules. +This project is made with [JetBrains MPS](https://www.jetbrains.com/mps/) using *coderules* experimental extension. +### Installation -## Instructions +The code in this project relies on *coderules* languages and solutions to be available, either as a project library or as a plugin. There are two possibilities to install coderules: -1. Install the latest version of [JetBrains MPS](https://www.jetbrains.com/mps/download) (latest release) -2. Download the type checking plugin from [this](https://github.com/fisakov/constraints-typechecking) project (see downloads for the latest release) -3. Install the plugin to your local drive (example for macOS): +1. Follow the instructions for building the root project, or +2. Install the compiled plugin (see the latest release on GitHub). - `unzip typechecking-0.2.zip -d ~/Library/Application\ Support/MPS2017.2/` +## License -4. Clone this repository and open the project with MPS -5. Execute 'Rebuild Project' +Copyright 2014-2018 JetBrains s.r.o. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + +http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. diff --git a/samples/mpscore/README.md b/samples/mpscore/README.md index b2fe3a9f..52eb9f3d 100644 --- a/samples/mpscore/README.md +++ b/samples/mpscore/README.md @@ -7,9 +7,12 @@ The two aspects are implemented here: 1. Type system 2. Control flow -### Build +### Installation -Use the instructions in the root folder of this repository for information on how to build this sample. +The code in this project relies on *coderules* languages and solutions to be available, either as a project library or as a plugin. There are two possibilities to install coderules: + +1. Follow the instructions for building the root project, or +2. Install the compiled plugin (see the latest release on GitHub). ## License