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 |