Fedor Isakov
|
cd0e7cc1b1
|
Introduce a language for propositional logic. Move relevant stuff there.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
5353654e31
|
Migrate to MPS 2017.3.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
db40250922
|
Proofread README file.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
1d272127f9
|
Update the instructions for installing the typechecking plugin.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
8683c18479
|
Completing the documentation. Fixed a sample. Some cosmetic improvements.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
197241d37d
|
A few more samples.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
4a9b422acd
|
Add README file.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
08350e6c68
|
Cosmetic changes, some comments.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
15d5a08bce
|
Completing the typesystem (OrElim, IffIntro, IffElim). Another couple of samples. Fix the Reiteration editor.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
64c0318489
|
Completing the typesystem (IfElim, AndIntro, AndElim).
Basis for IfIntro is a SubProof.
Fix goal validation.
Editor fixes.
Another couple of samples.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
b4f3ae1ef6
|
Introduce reiteration. Assumption to be used only as a subproof start.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
4c42629555
|
Rewritten the proof checker without the typeOf constraint, only assign type to the goal.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
784a1cedd0
|
Refactor "conclusion" out to Reasoning.
Add typechecking (incomplete).
Optimize the editor.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
d09373eaa9
|
Initial import
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
0d4d61d5f9
|
Change the sample project name to lambdacalc.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
78a0601625
|
Include lambdacalc sample into the common build.
|
2018-07-18 15:54:50 +02:00 |
Fedor Isakov
|
95d836df85
|
Auto-update after switching to the latest plugin.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
7ae9c936a6
|
Re-save everything after switching to the newest typechecking plugin.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
4e669b5412
|
Automatically migrated to the latest typechecking plugin. Drop second stage.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
f6121832a7
|
Switch to the latest typechecking plugin. Introduce Typecheck query. Drop automatic activation of "recoverAll".
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
08beb2ce13
|
Drop usages of a deprecated concept, replace with custom constraint. Fix imports.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
67ebe51be1
|
Applied the migration.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
e140342a4c
|
Replace custom constraints with reporting operations.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
2e3cb6278c
|
Migrated to the latest MPS release and typechecking plugin.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
d0b457dc4f
|
Migrated to the latest MPS release.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
2be2fbc58a
|
Switch to the latest plugin version. Clean up the term definitions.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
893b130933
|
Migrate to the latest typechecking plugin.
Move constraint declarations to the handlers, drop constraints root.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
3a186e38f4
|
Drop unused code.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
55b9e903a1
|
Switch to using CopyItem instead of ad-hoc solution, drop unused Util class.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
f8fec5c44f
|
Update README.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
231f92707f
|
Drop unused class. Drop unnecessary utility method, replace ad-hoc code with valueOf and equals predicate.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
791df0fe19
|
Replace ad-hoc logic value access with valueOf. Replace static method calls with equals constraints. Remove dead code.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
0d28fd939d
|
Switch to the latest release of typechecking plugin, apply migrations, manually update the logical data types.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
36e6a10e20
|
Updated to the latest release of typechecking plugin: applied migrations, manual fix of term getter blocks.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
07d31d93f6
|
Updated to the latest version of typechecking plugin, migrated the code to work correctly.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
3a82312055
|
Fix the typing rule for if-then-else
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
cbc3c5b106
|
Add back the generalization of the let-bound variable type.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
2041873c35
|
Add readme file.
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
58c4272111
|
Rename the language to sample.lambdacalc
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
dee0c7b8eb
|
Fix the wrong expression (contextNode).
|
2018-07-18 15:54:49 +02:00 |
Fedor Isakov
|
2347d0c572
|
Remove unused generator.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
3d2be367a8
|
Implemented if-then-else expression.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
ec840b0ee7
|
Don't generalize the type of let-bound variable.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
9d83b265eb
|
Re-save all models after refactorings in the language.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
9a34afceaa
|
Cleaning up the code.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
54153b57a6
|
Simplify unification, drop unifies constraint, drop trace constraint.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
8a932dafa6
|
Fix operator (general recursion)
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
de688f7cd1
|
Delete unused concept
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
a1a8d4934b
|
Ensure no model check errors in the types model
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
6f1b068a7b
|
Re-save models to update resolve info.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
2b114aba55
|
Refactor the types model adopting to the latest language changes. Re-saved all models.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
68a37091ae
|
More samples
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
cb2d735528
|
Introduce Forall type. Refactor the typesystem to support forall/gen/inst, get rid of varname for every type var. Better editor.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
2f32a72527
|
Switched to the latest RC build, applied the migrations.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
cea6f82b78
|
Refactor the language structure to better reflect the syntax of lambda calculus. Forbid patterns to the left of = sign. Use VarRef and scopes. Forbid let rec.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
4338ee2a50
|
Sample fix operator.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
dcabb36044
|
Correctly identify the var's binder. Typeof rule for let..in expression.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
8f1abd0388
|
Migrated to the latest MPS EAP build.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
6b16c682e6
|
More demo using S and K combinators.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
b74a7f0927
|
Collect bound vars from preceding let clauses
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
6c16c4a8f2
|
Another example of an impossible (non-typeable) term.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
9900cd91f3
|
Report error on catching a cyclic term
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
8146709a68
|
Ensure names are assigned to all type variables
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
0d648afda8
|
S, K, and I combinators
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
1d1b00cc6a
|
Intoruce error reporting to the types aspect. Replace all obsolete constructs with the new ones.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
05f3c8fe8c
|
Cleanup the demo samples.
|
2018-07-18 15:54:48 +02:00 |
Fedor Isakov
|
81a8c4abec
|
Fix the editor. Enable type presentation as text. Bool and Var types. Fix the types aspect and adapt to the changed metamodel.
|
2018-07-18 15:54:47 +02:00 |
Fedor Isakov
|
28b4862b67
|
Fimplifying the language: allow only boolean constants. Visualize lambda abstractions. Fix application order visualization with parenthises.
|
2018-07-18 15:54:47 +02:00 |
Fedor Isakov
|
773fa2eaaa
|
Union-find for Var nodes.
|
2018-07-18 15:54:47 +02:00 |
Fedor Isakov
|
7fcb2fa333
|
Types aspect. Simple typesystem based on Hindley-Milner.
|
2018-07-18 15:54:47 +02:00 |
Fedor Isakov
|
e9c3191a59
|
Initial commit. A simple functional language with numeric and string constants, single-argument abstractions and let bindings.
|
2018-07-18 15:54:47 +02:00 |
Fedor Isakov
|
3763f3dfe8
|
README for mpscore sample.
|
2018-07-18 11:17:43 +02:00 |
Fedor Isakov
|
46b8e5153f
|
Simplify and fix controlflow sample implementation.
|
2018-07-18 10:42:32 +02:00 |
Fedor Isakov
|
63788c9cca
|
Virtual folders for project modules.
|
2018-07-18 10:42:13 +02:00 |
Fedor Isakov
|
8294e8d702
|
Switch to MPS 2018.1.5
|
2018-07-17 15:29:02 +02:00 |
Fedor Isakov
|
2d3f4126b8
|
Add a "check" task for testing all projects at once. Switch travis build to 'gradle check'.
|
2018-07-17 15:09:47 +02:00 |
Fedor Isakov
|
c12bf0d96a
|
Ensure extracted baseLanguageExt stuff can be built from command line.
|
2018-07-17 15:09:47 +02:00 |
Fedor Isakov
|
473644e389
|
Extract baseLanguageExt and its related tests to a separate project.
|
2018-07-16 18:56:36 +02:00 |
Fedor Isakov
|
4f6b8a002a
|
Auto-updated descriptors. (Again!)
|
2018-07-16 16:40:09 +02:00 |
Fedor Isakov
|
d4477c519b
|
Auto-updated descriptors.
|
2018-07-16 13:44:02 +02:00 |
Fedor Isakov
|
92c6ba3e12
|
Restructuring the project: consolidate code, moving samples away.
|
2018-07-14 17:22:07 +02:00 |