From 814baf4bce06a7eab0c5cfed2b0ffc26f5c9fddd Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Thu, 19 Jul 2018 15:12:34 +0200 Subject: [PATCH] Update readme files. --- .mps/.name | 2 +- INSTALL.txt | 20 +++++ README.md | 82 +++++------------- coderules/README.md | 37 ++++++++ .../doc}/img/activation-trace-example.png | Bin {doc => coderules/doc}/img/menu-example.png | Bin .../doc}/img/type-annotation-example.png | Bin .../doc}/img/typing-rule-example.png | Bin doc/img/mps-logo.png | Bin 0 -> 5569 bytes reactor/README.md | 2 - samples/fitch/README.md | 30 +++++-- samples/lambdacalc/README.md | 27 ++++-- samples/mpscore/README.md | 7 +- 13 files changed, 126 insertions(+), 81 deletions(-) create mode 100644 INSTALL.txt create mode 100644 coderules/README.md rename {doc => coderules/doc}/img/activation-trace-example.png (100%) rename {doc => coderules/doc}/img/menu-example.png (100%) rename {doc => coderules/doc}/img/type-annotation-example.png (100%) rename {doc => coderules/doc}/img/typing-rule-example.png (100%) create mode 100644 doc/img/mps-logo.png 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 0000000000000000000000000000000000000000..c713da58d12b29abb1e0acf405210b2054572169 GIT binary patch literal 5569 zcmX9?c{tSH_kYh~H+I<>qdq7#WZ%awvXs6FG04_pNn~g+Gj=7456WJm6(PGZV=R>l zEp}$czGX(lVDR(({{Fc4KF{lU&ONVl&g-7%JU7kR(FVpV%?khk?3}IT#iJAV-^I;& zv{Ouc`T#&Y^_->IB~0P(qI)@FzlwT08e<}2@}Csb=OC6(=w)#Jgwh@^bv4L^_4gXm z=z^x3TD>;%`K3_m%L^9;FXyO#bvT$cP7)}dngOHomi z)PoD#mnUCWtyP7*z84d)9OYONGx@s3vxLFeZr#2dsjY;7>R=sY7I~pMHOIKU^F81= zpAbBd+{^)%oc|wCG;Y_Eui@DatACd9{?|BxI1SfyAME*Q1%$2qS-21I1JA{S$5h8d znoBO%U!SJ@$q{^O{or!FhWlUz$UBM{ISx_3a>MuOwWNzUPWYymCo4U>p{hjz#f^d! zq;<&F5TV`v?aS<&MuQkt{t*5Xytp*EZ7$sDze;CJm-Y+RAT^6p~O?Q{HNZyj48%vZy04X=Qr!Tkd9;Kbz()mtB=V4_3AFh6x9rCc3onzO-g8-5U z?$nAec%2=YQsLS=9zzRvNac>9tBU4e3t6!6`k>6`?_(r*IouMhyVycwNvT6fU_*10nc2p zKXvo?fFeQrh`qK8{c!b(y}Uux&lEH$U*l&sf~~L3E0djq`#$y1b<4R1LFj`BU+TTY z>KF?fto|mylUJwK&qb1oD_DefTW(cOt86WK;Vht0Nh(|z@XrXj*Sr3R4xA)HF&UKUCvxz>^6x2A0zL-!XMAj-x$5*Kbk4Dri;07&gVsrU+MXOM1sb4m;w@6Qw zjqET!9DMQUxBZKSJC8PCEbA&|b)%=N&}ryK5Bh@(&Y#~1rbx&QJ-y~Bo>~fZp;NbM zdGa38qeQV9+8ZAQ-xh66>1w~81d-PZuCFA#bvZ>Q1?{2lsO}T3%Z^Zl%8lu<#EQZg zKgzyf@jAM){+8(z5-AO@T!ta;Z(!bvegw)5X|B2)SD3*FTaktbk~_cGrV1d!V(J`m zthLrw1@!kngA!kBN{&DOh3stSMRQTEy%JzH$*^Br;jXfdTbHT8n8$1UyIzJyZBMmH z-d8|N?nG#SXgaLrlqV$%Grw7unUa&H%IsxJ9GhwO?3ol!8MiIdgRN}c z&P74fUojb1>sV2qkL2#_1CM=5R^|KY+=pqSsEblNb>wOcR7C(?m5snu`>aN_+zV-k z;JI%x8CUB3eiP>9?(?&97i36MP4+Ct%wLS%*1jj*^%5{eAGbnb8huu4t&B}2hY(rJ z%Hlzd>4)0(2Q{V9z2+jrY04Q)#t_YA9OTsHN2SUU^8$DJ#86922jOxl3>c$}B^}u| z!t8}@SwH#<#xdi|YaccWq9R`Dmt;?__>VL?Ny*#Go=A=ZMX|)wfH{h*6^e&evmwsE3FvT=;Ju`;wtr5cW9_}(qYPJ$TR&MA6-$0)8*t5I)md(Z04F~ZO1;G=7 zA9Dp2RL%hhWaSj@m}NoYAI21MMu*?$i1VH5{Nc76a}q=H)V6EIpb|5Qcd_D4qoVKt zG#8vNxi?#`LB@2A8G9c%pycf_bHvCj#u@C*pmbDHNBC%=>6hzc`k4uMJ&Vh;SV)aA zqkxblY?eCPJ#w6#p*y~NP{rJr;(95Iz0;+B;s-gAakssBmrK$dQ9~)&n_cbkRQ^~K zN(uzGQT86SdZp91Zx3!Sbkp{PKqq0;!V1Yvy#Y~^&3m4qQ~Jj(OFKJaMkgu*wAYLr zllO0lRM@@Bi1Mi9_3?;No0^^>Uqi*QZuqHq zQKyAV$Cz{2bi6OA;BRoB#I2TvWBg#@mrP`PSdWXGL+ku95b-U`5p2+Grjr{fxKjKe zlJLEj!Qdbwg@Iow3^DS-Z`ae9nW?A8@QLxA4$7JAo+Ql@liJ(ES3PIh4H`}DlGOrj3*PN_mKIHi*$X>$8{*5aF!`y~)-)7`n25|&v}DFi()%PrS{4F+ z;N<`U)p1nd3Kj)8!)DAONmca|yn-qqqq zl{>4a9dZ)P6Hj0MVS^6a+WZ@wanC?cW6{9kr~mSgr)-Z)zcr$#Z8T0%@?SDyr)chfENVLW)t zi`HV*ikz7fP0*ZuV_tKyGvyV8S!E({eDA=dlgp?PG+WO}dxJ>Dx63|_jvQXu{*M(D zOdQ&$ATy0ORK2!MQe(8yM|bFZxj^OBM28$^Jv{3$EZc zs9KBpZKGR8K&aCX7vDl0^&>y;uESz&!V8WXU!6dzTNC74jIFTLcjo!<oS0?VXUqN&#V2A zlLZHh9}w2I0(%l?Y{EF=hB%1Euvt;7b+Px#hG1l11)+6wzn!wJ2p%aNK6z9RGEQa0 zzD)m=MB7&X-ti+nEcGKLqs+I0u3W z2l@FNT|Th=TnM!>5X{Ag-FcDC|5I=aQP3J5mxfT6!5+quo7^_Wim$_ZEB(q8zj9!| z@iUZLhx1NCqZqpLjmm-~E;j1sV&g4Vob`VxRB2j;efhjoeZY#r2;q4SCD3xF*W&h) zZS^$t`2xtw$q#Tj_yVCen?&>L^rRrJEKt@|UJbI^)#ubofb&<1t0gYZ7fBnrnVv>U zJRBGncoO3~o;)8G{&dH63^)g4j1?3D3No`hqNDKXgMj^3|gki};NwK^8wUt&G#kd#U0I0_@qj8YtGur{_+&4%{N#g4uMYL5o&`<-Pj@&~;C@`>=W>}&2@OxeFuObZ*RCpXnVY8(fnH_4Sy(SKra2v-shzrOp0)GEpJyXO|&hw zl#MSv%F@y4olV#=o8dB<7lg50-H$7_L7_4r@6LQCjFd->+*lwe(xc zMytjORGD{5wexhwN2d}KaA@E^su>;O^fy0Z#c)QSN|TYpCnSYVY#9|{_S0k(nvS7j zw-Y4lKgb*3wg@`>(xs(Q9`O%t+@gK=)4Xt!#;@?9(eA8{b(S?%Yw@b)@)93=8o|r~ zH$kRK6Ol;kLXhQZQbqKz-1fAS^#}Q;mCcsj%|w1J+?~a9sBE7SeG9{cigJ+lrlCus zhx^9@1fb5@CM}^G$Gyi%?biVsL7lW@B+{=CFFevSAMN_(%dMWx-6)bCm($sxa@;>W zg=t1r;5_)oee=nHcTp0btGXnyh`j?MN!g#uzH9`}|JMgTS|j;|nTE$pJ--EQ%XmUF zP>=4A@7wS+`J%|FEj`QoygsNDH1gAwf{|63%U*axZO4g=lS;qs?9lr7PRQ3SmkBIJ zl4dKsINoabdvlZN`%s(oEK;8+$D`!p%?S9iGB$Kx1AIkU>MV0kN0AVvREN5dtRo@3 z_;7AQ%x9K4vFY4233us2KMPJ>=bZ7+)WPjd?;NkP@YxUo&7S*dO%uW+D|v9j%s9Ve zm>eHpm(Zz8w5Rg8!YzWhS$d;P%rzUr_b;{}lcZQA6O`Ewi1%bA2r6~RgpLCZ)&}G~ zDS_ZMZG3W9&Yat2pOzQge3+1Q+ZEVI?sZN1-A!>~BOV^AgpWp$vhYY`&_q+1f|d*- zA8tuI4~ljn+;La8k_3;9MM3qhPft9PCt`?dE+ck9&@m-aRswS28b7=< zLv#~c)Qho1Znsx$3{7*=0XT7FmS=&vlnlDo}!q+iQ4&;*TIZk<;VwcbPlvI z2vVc@okt+~!XvMO-jr0cMs23rNSP6WrDyP!)gIq)v6$fkt$|RO34-s91JvRVDhiTfh;26RA#soVI4d(k8TdH{Az-`4F)gkRe6QhW z*9UFC2h}mq`YhsI$Rmi~NM{O2K|`2FU1kKL^An%|XlZAKo-@10F2XzTKeMs>Ag=4ttI$uh*R|jGD?y7=i zIi@3nIJ}fg^2f6v=3Cu5#`^ zt{XTUEo^f=D^~=yGizJxz96`PG3ngS;!Nj-TPGQ<_}!!i_5y|zkhSC~oKjF?V8#EkR&^P9pX zB!I3GJ-xs9QNZu)3@M_5-6!Gf#(KCbRx=$8h{_6)wz<(c{ugj}HOpC7{HCREz)Wa6 zA*J~z{}rT3;E}^NAOyUC7essMQvB0eTKjV!D7839!{ms?No z%o`lDmnkg|@dnV7Yqgm&*xsnV$I1NW`jH>?D@QsWGw~vv1Tbs)ZeFYrDbGJc!Ybu8 zfX?j;Ek>aJXX3=e^e>7~UsTJv=lDKen+B2RAVFBZ%e78Y%(=K8L%jAKw>5?g)^rR2 zu|JdY!XknOo&>BhknHITrHMA3U08ss)>_T<*DulnpbjA~MX;oec0facq}#X4few}o z4>F-_D}nQik(D592fZ)6NAnr~Q*7_eBs%0pIdD`iGgi2a#9X~m*wO4U0Jh{Yg=soH z0Eq7%WFFlr0Q2@sE4{=z5y4^4^3T$91v;J`!8`mF0aN&|QAYkmOBRZ!gCDGdtImA| z$41{e(=T}P%C~*Jsf)PYMVoS-$W(3-Q9{AKb$Du6-Pymr1!;qW`<60@=`5? zROr2Bm**g?&r#v;?DgkXH+VyE`EG@yQ~NUl)GG`ZB#C$L*%=V~HAOd&>|Emj@55XZ zEKRH=-~r-q!{(tEh2dK}SmqoNsyu7X{Ix&%b;gMTW;HNo-Sfgfk1pIN>*|{66I-e* zS-46soOsMFaX#8LIBi@BKhbW)LY+gVJp+h0JwK}kmLSE6Za?oD_3DQYwH7Sg#sNf+ z|HmbWkwvopU#{urZsb>r36Y}S{EzAZIZ%b`NIfZvf677ZvBc^tJV*Uq3I9(UK-5NG z)ZfFtBXJqsg-A&bRNpVrp_sCKV>MW{zgF&sh?|TyoLUGYDJ$n2G4I5;(aU5DkAe>{ z4*nZnOo<)U%bQ`%zkeIqrQha$0i>?(9e9jYm}8f%?;k$;R(&q#(VLCvxHS&7*`3ep zWB?H@=HEKe>op{89hvh<_0)=A5#@EspUL~Vb^S6-x#2-J@nmphL7U?&uKHHxMC60p zLgM|*Zad~x)=+)^!osB*=aFqF^+Ft)Vlwf0zL@gvsujg#wQnvl76GF(LnWC z&DTkiZy-XP1JF{d^AzS-0QarZ(|j`yT^E3R-CE}?-2%y26i?6i>UZ@+2d?WR_5}~` z55Xr}>#uzK8zFWKbqr;vX3v`Hfq`X$G`$>x!tBZ3ZnZ#@9