Fedor Isakov
3e1c9d6e89
Rebuild project.
2019-06-04 18:59:53 +02:00
Fedor Isakov
c11cef9fff
Enable back a temporarily disabled test.
2019-05-17 18:01:34 +02:00
Fedor Isakov
1f6fbd0c0f
Temporarily disable a test consuming way too much memory, and as
...
a result failing b/c of a timeout.
2019-05-16 17:43:01 +02:00
Fedor Isakov
bd1c56d9d0
Rename concept Handler -> RulesList
2019-05-09 17:30:14 +02:00
Fedor Isakov
478b43ce16
Drop usages of deprecated interfaces.
2019-04-26 00:22:02 +02:00
Fedor Isakov
ed6f7a07c2
Remove instances of obsolete concept containingLink, replace with link.
2019-04-24 22:14:24 +02:00
Fedor Isakov
99ea2a7b71
Switch to the latest revision of reactor lib (0.9.9).
2019-04-24 21:21:03 +02:00
Fedor Isakov
55940d2e16
Remove Kotlin libs from reactor module and from distrib. Rebuild project.
...
Kotlin runtime is available from the platform.
2019-04-11 11:10:00 +02:00
Fedor Isakov
ab006cc8d9
Fix missing dependency.
2019-04-10 09:45:47 +02:00
Fedor Isakov
ca0524599d
Switch to latest 2019.1 EAP and rebuild.
2019-04-09 16:51:31 +02:00
Fedor Isakov
396b1fdad3
Move all classes from j.m.typechecking to j.m.typechecking.service. This package name is reserved.
2019-03-22 11:40:32 +01:00
Fedor Isakov
f6374635bb
Rebuild project.
2019-03-22 11:10:08 +01:00
Fedor Isakov
671194c9c3
Switch to the latest EAP of MPS 2019.1. Re-save all models.
2019-03-22 11:09:39 +01:00
Fedor Isakov
41b15f65c4
Replace assert() constraints with fail() together with an error message.
2019-02-18 12:26:05 +01:00
Fedor Isakov
255b7061f7
Reorganize models/packages, restructure code components responsible for program building/evaluation.
2019-02-15 17:15:17 +01:00
Fedor Isakov
83e5ce8c26
Switch to the latest conreactor version.
2019-02-15 17:15:16 +01:00
grigorii.kirgizov
e87c9654c1
lc: minor: Fix missed condition in guard on merging type constraints rule. Could have possibly led to bug in somewhere.
2019-02-06 16:00:31 +03:00
Fedor Isakov
0fcff76308
Re-save all models updated resolve info.
2019-02-06 13:22:32 +01:00
Fedor Isakov
b42d7553c8
Temporarily comment out an instance of let clause that produces different result in local inference.
2019-02-06 12:59:38 +01:00
Fedor Isakov
aa1a29a318
Make all tests in lambdacalc subproject pass including local inference.
2019-02-06 12:58:46 +01:00
grigorii.kirgizov
0cd29c5729
lc: Add type inference dependencies ('require' things) to output the same types for local type inf. Some renames.
...
Types from local & non-local type inf differ in 2 cases:
- different type variables names
- non-local typecheck fails, but some types still get to output
2019-02-05 13:03:51 +03:00
Fedor Isakov
fd94f0a249
Straghten up build tasks: assemble to be the default task. Remove superfluous configure_gradle script, use -P switches instead.
2019-02-04 11:32:13 +01:00
Fedor Isakov
0fb0771ad7
Ensure parent of varRef is included into typechecking. This fixes some locally inferred types mismatch.
2019-02-02 16:11:38 +01:00
Fedor Isakov
6e85a2c4fa
Use custom matching strategy in lambdacalc tests.
2019-02-02 16:10:35 +01:00
Fedor Isakov
ebada478c6
Replace error annotation with suppress error annotation to indicate an expected constraint violation.
2019-02-01 14:17:57 +01:00
Fedor Isakov
e0b856634c
Add java plugin to all gradle scripts.
2019-02-01 14:15:57 +01:00
Fedor Isakov
38777cda51
Ensure failed test means failed build for all sample projects.
2019-02-01 14:15:04 +01:00
Fedor Isakov
ebd4f82514
Specify the value for ${project_home} macrii in sample subprojects. Fix tests being ignored in CI.
2019-02-01 12:08:29 +01:00
Fedor Isakov
5b255f2a02
Fix references and introduce languages engaged on generation to keep compat. w/191 EAP.
2019-02-01 11:31:35 +01:00
Fedor Isakov
080bb0a448
Fix gradle scripts to get rid of deprecated stuff. Default task to build everything without testing. Update INSTALL.txt.
2019-02-01 00:40:59 +01:00
Fedor Isakov
81ee94c342
Fix gradle scripts to ensure model checker is run after everything else has heen built.
2019-01-31 17:39:39 +01:00
Fedor Isakov
a40e50bc53
Temprorarily suppress errors in two locations due to constraints violation (to be fixed).
2019-01-31 12:05:35 +01:00
Fedor Isakov
767444a5c0
Make LetClause able to suppress errors in its children.
2019-01-31 12:05:35 +01:00
Fedor Isakov
012b8963cb
Fix errors found by model checker in lambdacalc sample.
2019-01-31 12:05:21 +01:00
Fedor Isakov
9243c00c65
Fix issues found by model checker (ex typesystem).
2019-01-31 11:30:02 +01:00
grigorii.kirgizov
8d7bdcf173
lc: minor: Remove unneeded checkConstraints in subsumption
...
This case is anyhow handled by typeConstraints_discharge rule, when subsumes_leaves fires up,
even before those removed checks repeat this work.
2019-01-28 17:02:55 +03:00
grigorii.kirgizov
172f74b6f8
lc: minor: Add some comments. Some cleanup.
2019-01-28 16:59:05 +03:00
grigorii.kirgizov
a2012219b7
lc: Fix spurious typeConstraints reactivation on forall gen. Fix recursive case in instanceCheck.
...
As a consequence, there's a simplification of produceTypeConstraints rules.
Also add comments and fix some test cases: some of them are actually typeable.
Now tests are correct (checked against Haskell's typechecker) and all pass.
2019-01-28 13:32:32 +03:00
grigorii.kirgizov
0a5a7ec3c6
lc: minor: in 'typeclasses' restructure rule for Typeclass, add few comments, add Doc for failing type output (TypeclassesTest)
2019-01-28 11:38:33 +03:00
grigorii.kirgizov
41e8d3d96e
lc: Fix forgotten typeOf rule for 'fix' operator. Add typeclasses tests to test suite.
2019-01-28 11:38:33 +03:00
grigorii.kirgizov
2a44bb0ef0
lc: Fix absence of type output in some cases -- match in `produceTypeConstraints` rule in a different way
2019-01-28 11:38:33 +03:00
grigorii.kirgizov
d364dc24e4
lc: add type output (with a workaround) for Constraints in 'recover'
...
Workaround: ConstraintRepr SNode is added specifically for outputting types.
2019-01-28 11:38:33 +03:00
grigorii.kirgizov
4044b7f5e8
lc: Split typeConstraints constraint to two, according to its 2 types of usages: as typevar def and as actual Constraints
2019-01-28 11:38:33 +03:00
grigorii.kirgizov
ecc6c4aed2
lc: Add Constraint check for unified terms. Few fixes for typeclasses. Add typecheck deps for typeclasses. Some tests.
...
Some Constraints checks are not covered by 'subsumed', so, need top rule for discharging those.
Fix Constraint set production in 'types', use new set for each type var. Fix 'instance' constraint.
2019-01-28 11:38:33 +03:00
grigorii.kirgizov
20c9e0aae8
lc: add initial version of Constraints check rules, part of subsumption. Add partial recover rules. Other minor changes.
...
Also a fix to typeOf_PrototypeImpl rule, and a fix to instTypeVars: needed to copy Constraint sets.
2019-01-28 11:38:33 +03:00
Fedor Isakov
37b6afa642
Enable back working tests in lambdacalc
2019-01-26 14:15:30 +01:00
Fedor Isakov
f3c2f53fa6
Temporarily disable failing tests in lambdacalc sample
2019-01-25 15:02:26 +01:00
Fedor Isakov
fc1fcaaf9d
Cleanup a test: better layout of nested lists.
2019-01-21 11:20:30 +01:00
grigorii.kirgizov
5d5a102661
lc: minor: move Cons-list utils to its own handler
2019-01-16 18:19:11 +03:00
grigorii.kirgizov
87cdde5309
lc: 2 fixes for previous commit: walkaround in rules with 'deep' pattern-matching in heads; produce empty typeConstraints on user annos (in types)
2019-01-16 18:16:11 +03:00
grigorii.kirgizov
06623693bf
lc: add rules for Proto & ProtoImpl; modify inst and gen for Constraints in forall; move typeConstraints rule
...
Rule for PrototypeImpl is the heaviest.
Also, it seems that constraint field in Forall DataForm isn't needed.
2019-01-16 17:48:34 +03:00
grigorii.kirgizov
bd8e0ab00c
lc: add handling of Typeclass and Instance clauses, add macro for Constraint collection, add Set for this
2019-01-16 13:27:56 +03:00
grigorii.kirgizov
b0e5edb03a
lc: remove getType rule and translate type annotations to dataforms in macro; also minor changes
2019-01-16 11:48:09 +03:00
grigorii.kirgizov
94659549bc
lc: fix failing test: fix usages of eq rule in subsumption
2019-01-16 11:14:41 +03:00
Fedor Isakov
7f7f290b01
Temporarily comment out two instances of let clause that produced errors in tests
2019-01-13 17:53:06 +01:00
Fedor Isakov
dce532c5c7
Apply automatic migrations in lambdalc project
2019-01-13 17:53:01 +01:00
Fedor Isakov
275070c786
Apply automatic migrations to mpscore subproject
2019-01-13 14:27:38 +01:00
Fedor Isakov
08bed0c578
Apply automatic migrations to FitchProof subproject
2019-01-13 14:27:32 +01:00
grigorii.kirgizov
ce34b598c2
lc: minor: add simple Typeclass examples (it's only structure/editor/scopes example); add one test case to DemoScopes
2019-01-11 19:09:44 +03:00
grigorii.kirgizov
c8233c24d7
lc: move to fully nameless representation of type vars; assign names only in recover
...
It is also a necessary step to bidirectional typechecking and can simplify things in other places
2019-01-11 19:09:44 +03:00
grigorii.kirgizov
eb80329a54
lc: change recover_varRef rule, propagate to recover_Var rule instead of duplicating it
2019-01-11 19:09:44 +03:00
grigorii.kirgizov
fb4fe40973
lc: typeclasses: added structure, editor, constraints (mainly concerned with scoping) aspects
2019-01-11 19:09:44 +03:00
grigorii.kirgizov
cf855fc19b
lc: add test case for correct handling of instantiation scopes in forall. fails now.
2019-01-11 19:09:44 +03:00
grigorii.kirgizov
2cc804079a
lc: add test case in DemoScopes for isomorphism between similar forall type
...
It checks that subsumtion relation is actually a richer 'dsk' relation
from Peyton Jones et al. 2007
2019-01-11 19:09:44 +03:00
grigorii.kirgizov
61e282da6c
lc: minor: remove few commented lines, add few comments; add space between typevars in ForallType editor
2019-01-11 19:09:44 +03:00
Fedor Isakov
134fbb5cdb
Add missing dependency to lambdacalc test model
2019-01-09 14:48:21 +01:00
Fedor Isakov
f226bea8c2
Minor fixes in the BL typechecking templates. Insert manual new lines in the test structures for better visualization.
2019-01-09 13:01:37 +01:00
grigorii.kirgizov
4eab15c0a3
lc: add DemoScopes test case, fix one test example; reverse displayed order of user-supplied type annotations
2019-01-09 12:49:34 +03:00
grigorii.kirgizov
583358dc25
lc: modify name assignment to variables in 'forall'
2019-01-09 11:54:27 +03:00
grigorii.kirgizov
9180f16c25
lc: minor: uncomment typeOf_AnnVarRef rule (not fully tested yet), add dummy test rule
2019-01-09 11:18:20 +03:00
grigorii.kirgizov
8da1f51434
lc: move some examples, add error annotations in DemoScopes and test case for annotations
2019-01-09 11:18:20 +03:00
grigorii.kirgizov
1de24dd83c
lc: minor: editor enhancements
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
47130f794d
lc: add proper type var scopes for AnnExpr
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
b727b375ba
lc: disallow nested annotations on variables definitions
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
c407e29ec4
lc: some refactorings nothing special
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
682ed5b90b
lc: refine subsumption rel; add examples in DemoScope; editor enhancements (amend commit)
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
24ce9e73aa
lc: refine subsumption rel; add examples in DemoScope; editor enhancements
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
7f02d10b62
Add expr annotations; add examples
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
440fcf868a
Intermediate commit: add VarType DF with editor; partial work on subsumed relation
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
2fa00cac72
Minor: move annotation rules to its own handler
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
06baa99da8
Add Var term; use it instead of free var-s in forall for subst.
...
Still not finished: can't pass Var name (see forall, freeTypeVars_isFree).
Also add subsumption relation for annotations.
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
58a518af4f
Partially working forall quantified types
...
Substitution (i.e. forall instantiation) doesn't work in this version.
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
084c4581f0
Bounded type vars: add free type var collection (in typeOf), gen, inst, list utils
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
1be19ffe1e
lc: add pair (without accessors) and its typing to lambda calculus (lc)
2019-01-09 11:17:42 +03:00
grigorii.kirgizov
4ed48e2560
add unquantified type annotations to lambda calculus
2019-01-09 11:17:42 +03:00
Fedor Isakov
b7648ef5c3
Document judgements and reasonings in Fitch sample languages.
2019-01-07 11:03:55 +01:00
Fedor Isakov
54165ad367
Add new samples to the tests
2019-01-06 16:39:15 +01:00
Fedor Isakov
80e2b67d78
A couple of non-trivial examples of proofs.
2019-01-06 16:06:17 +01:00
Fedor Isakov
2078606204
Fitch sample: fix relation name constraint.
2019-01-06 16:05:52 +01:00
Fedor Isakov
cc4b335286
Introduce checking for instances of RuntimeErrorType during tests. Refactor test typechecking launcher.
2019-01-04 17:47:44 +01:00
Fedor Isakov
361fff7ec5
Drop usages of ListLiteral in tests. Testing BL typesystem.
2019-01-04 17:47:02 +01:00
Fedor Isakov
f855e5fa72
BL typesystem: drop usages of ListLiteral, replace with ListNode. Fix broken type inference of method calls and constructor invocations. A few minor fixes.
2019-01-04 17:46:37 +01:00
Fedor Isakov
b5552d5cd3
Cleanup module dependencies
2019-01-03 17:16:47 +01:00
Fedor Isakov
2fd4545be4
BL typechecking: simplifying promote (subclassing relation), implement LUB as raw types intersection, better support for raw classier types
2019-01-03 17:16:47 +01:00
Fedor Isakov
9a99a440ec
Testing BL typesystem. Disable Huge test when not in CI.
2019-01-03 17:16:47 +01:00
Fedor Isakov
b4693aac3c
Switch to the new conreactor version.
2018-12-28 11:57:27 +01:00
Fedor Isakov
cb1ea46af7
Typechecking templates: specify data types for logicals that are used for values instead of term.
2018-12-28 11:57:26 +01:00
Fedor Isakov
d64f469b19
Add tests for fitch sample project
2018-12-14 14:55:23 +01:00
grigorii.kirgizov
54af10dad0
add unquantified type annotations to lambda calculus
2018-12-05 16:38:32 +01:00
Fedor Isakov
debaa390e2
Tests of BL typechecking features. Primitive types.
2018-12-03 16:59:16 +01:00
Fedor Isakov
2205639acf
Add tests to build script for lambdacalc
2018-11-29 13:23:48 +01:00
Fedor Isakov
a1bd3024a5
Tests for lambdacalc sample. Annotate places where errors are expected.
2018-11-29 12:51:33 +01:00
Fedor Isakov
39f7ff6838
Ensure local type inference works in lambdacalc sample. Ensure type variable numbers are unique withing top Clause instance.
2018-11-29 12:16:38 +01:00
Fedor Isakov
f0bb068750
Fix instances of removed concepts and broken API calls after migration to 2018.3. Rebuild project.
2018-11-28 16:48:59 +01:00
Fedor Isakov
19ce84f7ef
Switch to 2018.3 RC. Apply all migrations.
2018-11-28 16:48:59 +01:00
Fedor Isakov
e9d5a05900
Typechecking BL: reimplement type inference, implement and test various missing features. Cleann up and restructure code.
2018-11-28 14:27:51 +01:00
Fedor Isakov
06f95c5870
Update build solution to reflect latest changes.
2018-11-04 13:10:40 +01:00
Fedor Isakov
18fbdbd50b
Use error annotation in tests instead of simply relying on typechecking failure.
2018-11-04 13:10:40 +01:00
Fedor Isakov
6788bcf7a1
Switch to latest reactor, update the API calls. Support EvaluationFailure and FailureHandler.
2018-11-04 13:10:40 +01:00
Fedor Isakov
075b34e24d
Replacing usages of deprecated concepts. Minor fixes.
2018-09-11 17:01:45 +02:00
Fedor Isakov
f12965898f
Remove usages of deprecated stuff in typechecking rules.
2018-09-11 15:37:39 +02:00
Fedor Isakov
0819ef0a40
Add a reference to the article on typechecking STLC to readme
2018-08-19 17:32:59 +02:00
Fedor Isakov
27becb70a1
Fix the wording in fitch sample README
2018-08-19 17:32:59 +02:00
Fedor Isakov
8cacd9c326
Ensure terms are copied "properly" without breaking Path's contract. Pending optimization.
2018-08-07 11:50:05 +02:00
Fedor Isakov
98dfe30756
Resaved all models
2018-08-03 11:48:36 +02:00
Fedor Isakov
d26805db7d
Switch to the latest version of reactor lib 0.9.1
2018-08-03 11:48:36 +02:00
Fedor Isakov
e2a68b4012
Fixes necessary for compatibility with MPS 2018.2
2018-07-22 16:51:10 +02:00
Fedor Isakov
1cb1472184
Name solutions and models consistently in samples (mpscore). Drop empty obsolete test solution.
2018-07-22 14:48:13 +02:00
Fedor Isakov
7c1cb3b684
Name solutions and models consistently in samples (fitch)
2018-07-22 14:48:12 +02:00
Fedor Isakov
a240f129c2
Name solutions and models consistently in samples (lambdacalc)
2018-07-22 11:26:12 +02:00
Fedor Isakov
0bacffb611
Move type setting operation to typechecking lang.
2018-07-22 11:09:49 +02:00
Fedor Isakov
430b081085
Rename sandbox to demo solution in fitch sample.
2018-07-21 13:50:54 +02:00
Fedor Isakov
689ae4776c
Give more sensible name to a sample demo solution and model.
2018-07-21 13:49:21 +02:00
Fedor Isakov
c7cc97fffb
Rename reporting runtim solution.
2018-07-21 13:29:40 +02:00
Fedor Isakov
6e00dcd58c
Fix handler activating constraints declared elsewhere.
2018-07-21 13:29:40 +02:00
Fedor Isakov
ea9919f38a
Bring the hierarchy of DataForm concepts in line with the runtime.
...
Merge DataForm constructors into logic language.
Repackaging logic runtime.
Drop obsolete code.
2018-07-21 13:29:22 +02:00
Fedor Isakov
3791a3b216
Auto-updated descriptors.
2018-07-20 10:51:53 +02:00
Fedor Isakov
814baf4bce
Update readme files.
2018-07-19 15:12:34 +02:00
Fedor Isakov
e29a0576e2
Rename the root project and artifacts to "coderules".
2018-07-18 15:54:52 +02:00
Fedor Isakov
d5b27ac6e2
Move sandbox solution to "solutions" folder.
2018-07-18 15:54:52 +02:00
Fedor Isakov
e03cd48125
Add fitch sample to the common build.
2018-07-18 15:54:52 +02:00
Fedor Isakov
061e75f3f5
Auto-updated files after switching to the latest plugin.
2018-07-18 15:54:51 +02:00
Fedor Isakov
776ba9282b
Re-save everything after switching to the newest typechecking plugin.
2018-07-18 15:54:51 +02:00
Fedor Isakov
b87b71f07c
Automatically migrated to the latest typechecking plugin.
2018-07-18 15:54:51 +02:00
Fedor Isakov
124cc3cd93
Switch to the latest typechecking plugin. Drop auto-triggering of checkAll constraint, use query instead. Switch to single stage.
2018-07-18 15:54:51 +02:00
Fedor Isakov
adfae88953
Fix imports and establish extends relation among handlers.
2018-07-18 15:54:51 +02:00
Fedor Isakov
7107dce378
Applied the migration.
2018-07-18 15:54:51 +02:00
Fedor Isakov
dc662b97b9
Convert to reporting expressions, drop obsolete constraints.
2018-07-18 15:54:51 +02:00
Fedor Isakov
9f1632b018
Updated to latest MPS and typechecking plugin.
2018-07-18 15:54:51 +02:00
Fedor Isakov
2aa168e32e
Docs on Herbrand and First Order Logics
2018-07-18 15:54:51 +02:00
Fedor Isakov
72b2f0d110
Fix the Equality Introduction rule.
2018-07-18 15:54:51 +02:00
Fedor Isakov
f070e7a34b
Implementation of First Order logic.
2018-07-18 15:54:51 +02:00
Fedor Isakov
25d0238155
Implementation of Herbrand logic, an example.
2018-07-18 15:54:51 +02:00
Fedor Isakov
848df81dd4
Refactor out abstract proof, provide a mechanism to filter passing rules by the proof kind.
2018-07-18 15:54:51 +02:00
Fedor Isakov
5a550836b6
A couple of renamings to straighten the nomenclature.
2018-07-18 15:54:51 +02:00
Fedor Isakov
908e557d72
A language for Herbrand logic.
2018-07-18 15:54:51 +02:00
Fedor Isakov
e3d2ac503b
Move inference rules to propositional logic language.
2018-07-18 15:54:51 +02:00
Fedor Isakov
e2ceb9b500
Some refactorings and renamings in preparation for intruduction of Herbrand logic language.
2018-07-18 15:54:50 +02:00
Fedor Isakov
aa3837cd72
Separate logic-related stuff from proof-related.
2018-07-18 15:54:50 +02:00
Fedor Isakov
929a017704
Drop *_old stuff and the migration logs.
2018-07-18 15:54:50 +02:00
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