Update readme files.

This commit is contained in:
Fedor Isakov 2018-07-19 15:12:34 +02:00
parent 1c33ddca9a
commit 814baf4bce
13 changed files with 126 additions and 81 deletions

View File

@ -1 +1 @@
constraints-typechecking coderules

20
INSTALL.txt Normal file
View File

@ -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.

View File

@ -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 MPSs baseLanguage.
## Status ## Status
@ -10,79 +12,37 @@ The status of this project is **pre-release**. Dont rely on any of the langua
## Overview ## 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 its 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) See [implementation notes](coderules/README.md) for more information.
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)
## Dependencies ## 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. 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 ## Installation
The easiest way to install the plugin is by using the update mechanism built in to JetBrains MPS. See [INSTALL.txt](INSTALL.txt).
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.
## License ## License

37
coderules/README.md Normal file
View File

@ -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.

View File

Before

Width:  |  Height:  |  Size: 66 KiB

After

Width:  |  Height:  |  Size: 66 KiB

View File

Before

Width:  |  Height:  |  Size: 149 KiB

After

Width:  |  Height:  |  Size: 149 KiB

View File

Before

Width:  |  Height:  |  Size: 56 KiB

After

Width:  |  Height:  |  Size: 56 KiB

View File

Before

Width:  |  Height:  |  Size: 59 KiB

After

Width:  |  Height:  |  Size: 59 KiB

BIN
doc/img/mps-logo.png Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 5.4 KiB

View File

@ -4,8 +4,6 @@ An engine for evaluating constraint rules.
Written in Kotlin and Java. 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/). 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**. The main features are built-in support for **terms** as the data structure, including terms **unification**, and **logical variables**.

View File

@ -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 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). 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:
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 1. Follow the instructions for building the root project, or
4. Execute 'Rebuild Project' 2. Install the compiled plugin (see the latest release on GitHub).
### Using the proof checker ### Using the proof checker
@ -227,3 +227,19 @@ The proofs 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 dont have `valid` constraint are marked with error. 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 dont 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. 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.

View File

@ -2,16 +2,27 @@
This is a demo of type checking simply typed lambda calculus using constraint rules. 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) 1. Follow the instructions for building the root project, or
2. Download the type checking plugin from [this](https://github.com/fisakov/constraints-typechecking) project (see downloads for the latest release) 2. Install the compiled plugin (see the latest release on GitHub).
3. Install the plugin to your local drive (example for macOS):
`unzip typechecking-0.2.zip -d ~/Library/Application\ Support/MPS2017.2/` ## License
4. Clone this repository and open the project with MPS Copyright 2014-2018 JetBrains s.r.o.
5. Execute 'Rebuild Project'
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.

View File

@ -7,9 +7,12 @@ The two aspects are implemented here:
1. Type system 1. Type system
2. Control flow 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 ## License