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
|
c5daa24ee8
|
Deprecate ListLiteral and ListExpression concepts (only used in BL typesystem)
|
2019-01-04 17:44:32 +01:00 |
|
Fedor Isakov
|
d74ad951e3
|
Drop a hack in ListNode implementation that would disallow nested lists
|
2019-01-04 17:43: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
|
32601dc96a
|
Deprecate unused methods in conreactor.
|
2019-01-03 17:16:47 +01:00 |
|
Fedor Isakov
|
63da3a7a6c
|
Minor optimization of terms representation in UI: hide uninitialized values
|
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
|
d5ed9d8fa0
|
Eliminate duplicate language aspect objects from lookup
|
2019-01-02 18:16:28 +01:00 |
|
Fedor Isakov
|
c87ca87a49
|
Cleanup in tests
|
2018-12-30 16:41:28 +01:00 |
|
Fedor Isakov
|
b4693aac3c
|
Switch to the new conreactor version.
|
2018-12-28 11:57:27 +01:00 |
|
Fedor Isakov
|
6e9966fe9d
|
Bump up conreactor version to 0.9.3.
|
2018-12-28 11:57:27 +01:00 |
|
Fedor Isakov
|
6953939e4a
|
Report unification of a logical with itself as a failure.
|
2018-12-28 11:57:27 +01:00 |
|
Fedor Isakov
|
6c0a9d404b
|
Properly process failed guard
|
2018-12-28 11:57:26 +01:00 |
|
Fedor Isakov
|
d61e8e1370
|
Ensure matched rule logical context provides all logicals with corresponding prototype meta-logicals.
|
2018-12-28 11:57:26 +01:00 |
|
Fedor Isakov
|
666f406335
|
Introduce VarSymbol interface to classify terms with "logical" symbol as wildcards in the term trie.
|
2018-12-28 11:57:26 +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
|
d74ec1d2f8
|
Introduce support for unification variables of arbitrary type, not just terms. Minor refactoring and cleanup.
|
2018-12-28 11:56:27 +01:00 |
|
Fedor Isakov
|
d64f469b19
|
Add tests for fitch sample project
|
2018-12-14 14:55:23 +01:00 |
|
Fedor Isakov
|
82b409cb86
|
Fix SubstituteUtil to match pattern using equals() instead of unification. Tests for SubstituteUtil.
|
2018-12-14 13:35:36 +01:00 |
|
Fedor Isakov
|
c22520fcc8
|
Fix EQ solver returning wrong value for two distinct free logicals. Testing EQ and UNI solvers on free logicals.
|
2018-12-13 18:24:53 +01:00 |
|
Fedor Isakov
|
380a9c003b
|
Switch to release build for 2018.3
|
2018-12-05 17:09:24 +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
|
d7c1f70287
|
Add testing of lambdacalc samples to root build script.
|
2018-11-29 14:42:23 +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
|
3e38d4aedd
|
Record a warning on local type inference yielding mismatched type in case ensureLocal flag is set to false.
|
2018-11-29 12:47:34 +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
|
e9c8fb87e5
|
Switch build dependency to MPS 2018.3 RC2.
|
2018-11-28 16:48:59 +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
|
f095c64abe
|
Rename 'isBound' predicate to 'isAssigned' (alias only, concept to be renamed still).
|
2018-11-27 15:10:48 +01:00 |
|
Fedor Isakov
|
8bc26f6cdd
|
Shorten the presentation of user terms in actiovation trace view. Filter out wildcards and empty lists.
|
2018-11-27 15:10:48 +01:00 |
|
Fedor Isakov
|
939262b4a5
|
Fix memleak by unregistering mouse listeners on treetable component dispose.
|
2018-11-27 15:10:14 +01:00 |
|
Fedor Isakov
|
9c4dad3e91
|
Enable use of input node in macro body. Allow specifying a subset of macro parameters in macro call.
|
2018-11-20 22:39:30 +01:00 |
|
Fedor Isakov
|
bfcf89e3df
|
Use stack to implement storage of template application session objects
|
2018-11-20 22:39:30 +01:00 |
|
Fedor Isakov
|
6778fab625
|
Use index to filter nodes on which FailureHandler should report error and clear failed state.
|
2018-11-20 22:39:30 +01:00 |
|
Fedor Isakov
|
8db1aead11
|
Fix propagate failure on on reactivated constraint. Always report a failure to avoid confusion with the trace view.
|
2018-11-20 22:39:30 +01:00 |
|
Fedor Isakov
|
087ccf4503
|
Fix matching single constraint on reactivation after a logical has been assigned.
|
2018-11-20 22:39:30 +01:00 |
|
Fedor Isakov
|
fc7b9d6caf
|
Always report a failure during evaluation as a warning
|
2018-11-20 22:39:29 +01:00 |