d22abb3835
Drop instances of deprecated concepts in lambdacalc.
2020-04-13 17:58:33 +02:00
6a431fcb49
Rebuild project.
2020-03-31 18:44:07 +02:00
ffcc74459f
Migrate fitch samples to new expand/call macros.
2020-03-31 11:43:30 +02:00
6a53d15a21
Refactor: move logic related to tracking parent match from ControllerImpl to MatchJournal
...
Relates to machinery introduced in MPSCR-47.
Previously parent match was maintained in Controller on Java call stack.
Now this stack of parent matches is maintained manually in MatchJournal.
So MatchJournal gains new invariant: parentChunk()
returns correct parent after each logMatch() call.
Several tests fail, also need to maintain this
invariant after logActivation() calls.
2020-03-26 13:40:41 +03:00
b6aaec8870
Revert temporary workaround for MPSCR-51 from 16e39a93
2020-03-23 14:39:54 +03:00
16e39a9345
Check applicable scope for certain checking rules in BL (workaround for BL for MPSCR-51). Fix SubclassingUtil.
...
Modified TYPECHECK query to include "checkingScope" query parameter:
it is a root node for which program is generated (for local typechecking it's local node).
Rules additionally match on a constraint `checkDecls(node<>)` bearing this node,
so while rules will be generated for all scopes, only those in applicable scopes will run.
Also split rule for EnumConstantDeclaration on declration checking and just typing rule.
2020-03-17 17:54:38 +03:00
f2bb87e1b0
Apply migration to replace deprecated concept.
2020-02-26 15:03:31 +01:00
7ba7c983cb
Apply migration to use logical variable ref expression.
2020-02-24 22:57:05 +01:00
2c43762f93
Replace all instances of .pointer in constraints to node reference.
...
SNode is supported now directly as an argument to constraint/predicate.
Pointer operation is no longer necessary, as is node-ptr<> type for logical vars.
2020-02-20 11:59:28 +01:00
796ad9ad2c
Apply migration to drop ValueOfExpression.
2020-02-12 12:26:09 +01:00
1a6b107a76
Apply migration to replace condition block with if statement.
2020-02-07 13:14:46 +01:00
4a84ebce5f
Apply migration to switch to BodyBlock.
2020-02-06 12:55:32 +01:00
c353f89ea0
Apply migration to drop ParameterContainer.
2020-02-05 17:02:32 +01:00
3f51c1e5c1
Apply migration that replaces empty logical type with term type.
2020-02-05 12:34:20 +01:00
391c9053b5
Apply migrations after switch to MPS 193. Regenerate project.
2020-02-03 11:24:22 +01:00
c384785b12
Apply automatic migration.
2020-01-20 16:54:38 +01:00
85674ef077
Add explicit "test" facets to test solutions.
2019-11-24 17:58:15 +01:00
69bc34e8f9
Drop language j.m.l.smodel.types containing SNodeTypeOp that is no longer used.
2019-11-11 14:37:41 +01:00
ecd2594fed
Drop deprecated Reporting interface and all its usages.
...
Remove runtime solution that contained only Reporting.
2019-11-11 13:53:41 +01:00
3f1b65ada2
Fix the structural errors introduced by a badly run migration.
2019-11-06 12:05:18 +01:00
ad90a4cb77
Apply migration that replaces all instances of NodeAnchor with .pointer op.
2019-11-06 11:21:57 +01:00
daa1bdceb6
Update default jvm options for running tests to "-Xmx2048m".
2019-11-05 20:53:01 +01:00
f8dcf127db
Extend typechecking query TYPECHECK with a parameter to report types.
...
Reporting of calculated types is to be more explicit.
The not-so-obvious _type_.set() operation is to be phased out.
2019-10-10 17:30:11 +02:00
49518e0704
Switch to reactor version 0.9.14.
2019-09-30 16:44:36 +02:00
cdfe1f2c0c
Update language version after migrations from mps.logic lang
2019-09-11 13:24:02 +03:00
39fa007310
Run Splice migration on samples
2019-09-11 13:24:02 +03:00
5b5798dcad
Switch to reactor lib 0.9.13.
2019-09-10 18:37:11 +02:00
5eed118be0
Replace usages of deprecated reporting with error constraint.
...
Having to specify the target for reported messages is a redundancy.
It's better to rely on the built-in feedback mechanism and handle the
messages at the supervisor level.
2019-09-02 17:55:46 +02:00
0db213725e
fixup! Swith to using reactor lib 0.9.12.
2019-09-02 17:55:46 +02:00
d786ff43b9
Re-save all models, language name updated in .mpl files.
2019-08-20 23:11:19 +02:00
22ee175030
Fix script build (dangling node).
2019-08-20 23:11:19 +02:00
973b9c35d5
Rebuild project.
2019-08-14 13:29:22 +02:00
2ef8adfe5e
Switch to reactor 0.9.11
2019-07-30 13:48:08 +02:00
6384085b17
Rebuild project.
2019-07-30 12:24:25 +02:00
3a48c47880
Migration: "update versions in descriptors".
2019-07-30 11:49:26 +02:00
66c9222a95
Run migrations with MPS 2019.2 EAP3.
2019-07-26 17:27:18 +02:00
4e4e1f68ef
Fix buildscript dependencies.
2019-07-26 17:14:48 +02:00
79b08c6f83
Revert "Apply migrations from EAP3 and rebuild project."
...
This reverts commit 9c5bf858c3
2019-07-26 15:30:30 +02:00
9c5bf858c3
Apply migrations from EAP3 and rebuild project.
2019-07-19 12:28:27 +02:00
cd37daaa07
Apply migrations after switching to the latest EAP build of MPS.
2019-06-07 09:16:21 +02:00
17ed4642ae
Apply all available automatic migrations.
2019-06-05 16:16:00 +02:00
57de11c3fe
Rename all modules/models having prefix j.m.typechecking to j.m.coderules.typechecking. The former is reserved.
2019-06-05 16:15:59 +02:00
fe505792c6
A bunch of refactorings and renames in typechecking plugin.
...
Remove unused interfaces, merge classes with similar functionality, reduce the number of used classes.
2019-06-05 16:14:27 +02:00
d0ffcb66ef
Regenerated project.
2019-06-05 16:14:27 +02:00
3e1c9d6e89
Rebuild project.
2019-06-04 18:59:53 +02:00
bd1c56d9d0
Rename concept Handler -> RulesList
2019-05-09 17:30:14 +02:00
99ea2a7b71
Switch to the latest revision of reactor lib (0.9.9).
2019-04-24 21:21:03 +02:00
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
ab006cc8d9
Fix missing dependency.
2019-04-10 09:45:47 +02:00
ca0524599d
Switch to latest 2019.1 EAP and rebuild.
2019-04-09 16:51:31 +02:00
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
f6374635bb
Rebuild project.
2019-03-22 11:10:08 +01:00
83e5ce8c26
Switch to the latest conreactor version.
2019-02-15 17:15:16 +01:00
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
e0b856634c
Add java plugin to all gradle scripts.
2019-02-01 14:15:57 +01:00
38777cda51
Ensure failed test means failed build for all sample projects.
2019-02-01 14:15:04 +01:00
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
5b255f2a02
Fix references and introduce languages engaged on generation to keep compat. w/191 EAP.
2019-02-01 11:31:35 +01:00
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
81ee94c342
Fix gradle scripts to ensure model checker is run after everything else has heen built.
2019-01-31 17:39:39 +01:00
9243c00c65
Fix issues found by model checker (ex typesystem).
2019-01-31 11:30:02 +01:00
08bed0c578
Apply automatic migrations to FitchProof subproject
2019-01-13 14:27:32 +01:00
b7648ef5c3
Document judgements and reasonings in Fitch sample languages.
2019-01-07 11:03:55 +01:00
54165ad367
Add new samples to the tests
2019-01-06 16:39:15 +01:00
80e2b67d78
A couple of non-trivial examples of proofs.
2019-01-06 16:06:17 +01:00
2078606204
Fitch sample: fix relation name constraint.
2019-01-06 16:05:52 +01:00
cc4b335286
Introduce checking for instances of RuntimeErrorType during tests. Refactor test typechecking launcher.
2019-01-04 17:47:44 +01:00
b4693aac3c
Switch to the new conreactor version.
2018-12-28 11:57:27 +01:00
d64f469b19
Add tests for fitch sample project
2018-12-14 14:55:23 +01:00
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
19ce84f7ef
Switch to 2018.3 RC. Apply all migrations.
2018-11-28 16:48:59 +01:00
06f95c5870
Update build solution to reflect latest changes.
2018-11-04 13:10:40 +01:00
27becb70a1
Fix the wording in fitch sample README
2018-08-19 17:32:59 +02:00
98dfe30756
Resaved all models
2018-08-03 11:48:36 +02:00
d26805db7d
Switch to the latest version of reactor lib 0.9.1
2018-08-03 11:48:36 +02:00
e2a68b4012
Fixes necessary for compatibility with MPS 2018.2
2018-07-22 16:51:10 +02:00
7c1cb3b684
Name solutions and models consistently in samples (fitch)
2018-07-22 14:48:12 +02:00
0bacffb611
Move type setting operation to typechecking lang.
2018-07-22 11:09:49 +02:00
430b081085
Rename sandbox to demo solution in fitch sample.
2018-07-21 13:50:54 +02:00
c7cc97fffb
Rename reporting runtim solution.
2018-07-21 13:29:40 +02:00
6e00dcd58c
Fix handler activating constraints declared elsewhere.
2018-07-21 13:29:40 +02:00
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
3791a3b216
Auto-updated descriptors.
2018-07-20 10:51:53 +02:00
814baf4bce
Update readme files.
2018-07-19 15:12:34 +02:00
e29a0576e2
Rename the root project and artifacts to "coderules".
2018-07-18 15:54:52 +02:00
d5b27ac6e2
Move sandbox solution to "solutions" folder.
2018-07-18 15:54:52 +02:00
e03cd48125
Add fitch sample to the common build.
2018-07-18 15:54:52 +02:00
061e75f3f5
Auto-updated files after switching to the latest plugin.
2018-07-18 15:54:51 +02:00
776ba9282b
Re-save everything after switching to the newest typechecking plugin.
2018-07-18 15:54:51 +02:00
b87b71f07c
Automatically migrated to the latest typechecking plugin.
2018-07-18 15:54:51 +02:00
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
adfae88953
Fix imports and establish extends relation among handlers.
2018-07-18 15:54:51 +02:00
7107dce378
Applied the migration.
2018-07-18 15:54:51 +02:00
dc662b97b9
Convert to reporting expressions, drop obsolete constraints.
2018-07-18 15:54:51 +02:00
9f1632b018
Updated to latest MPS and typechecking plugin.
2018-07-18 15:54:51 +02:00
2aa168e32e
Docs on Herbrand and First Order Logics
2018-07-18 15:54:51 +02:00
72b2f0d110
Fix the Equality Introduction rule.
2018-07-18 15:54:51 +02:00
f070e7a34b
Implementation of First Order logic.
2018-07-18 15:54:51 +02:00
25d0238155
Implementation of Herbrand logic, an example.
2018-07-18 15:54:51 +02:00
848df81dd4
Refactor out abstract proof, provide a mechanism to filter passing rules by the proof kind.
2018-07-18 15:54:51 +02:00
5a550836b6
A couple of renamings to straighten the nomenclature.
2018-07-18 15:54:51 +02:00
908e557d72
A language for Herbrand logic.
2018-07-18 15:54:51 +02:00
e3d2ac503b
Move inference rules to propositional logic language.
2018-07-18 15:54:51 +02:00
e2ceb9b500
Some refactorings and renamings in preparation for intruduction of Herbrand logic language.
2018-07-18 15:54:50 +02:00
aa3837cd72
Separate logic-related stuff from proof-related.
2018-07-18 15:54:50 +02:00
929a017704
Drop *_old stuff and the migration logs.
2018-07-18 15:54:50 +02:00
cd0e7cc1b1
Introduce a language for propositional logic. Move relevant stuff there.
2018-07-18 15:54:50 +02:00
5353654e31
Migrate to MPS 2017.3.
2018-07-18 15:54:50 +02:00
db40250922
Proofread README file.
2018-07-18 15:54:50 +02:00
1d272127f9
Update the instructions for installing the typechecking plugin.
2018-07-18 15:54:50 +02:00
8683c18479
Completing the documentation. Fixed a sample. Some cosmetic improvements.
2018-07-18 15:54:50 +02:00
197241d37d
A few more samples.
2018-07-18 15:54:50 +02:00
4a9b422acd
Add README file.
2018-07-18 15:54:50 +02:00
08350e6c68
Cosmetic changes, some comments.
2018-07-18 15:54:50 +02:00
15d5a08bce
Completing the typesystem (OrElim, IffIntro, IffElim). Another couple of samples. Fix the Reiteration editor.
2018-07-18 15:54:50 +02:00
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
b4f3ae1ef6
Introduce reiteration. Assumption to be used only as a subproof start.
2018-07-18 15:54:50 +02:00
4c42629555
Rewritten the proof checker without the typeOf constraint, only assign type to the goal.
2018-07-18 15:54:50 +02:00
784a1cedd0
Refactor "conclusion" out to Reasoning.
...
Add typechecking (incomplete).
Optimize the editor.
2018-07-18 15:54:50 +02:00
d09373eaa9
Initial import
2018-07-18 15:54:50 +02:00
Fedor Isakov