Commit Graph

138 Commits

Author SHA1 Message Date
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