Fedor Isakov
|
f3c2f53fa6
|
Temporarily disable failing tests in lambdacalc sample
|
2019-01-25 15:02:26 +01:00 |
|
Fedor Isakov
|
934f98b717
|
Fix UnificationPredicate to delegate logical union logic to the underlying implementation.
Test unification failure on cycle detected.
|
2019-01-25 15:02:03 +01:00 |
|
Fedor Isakov
|
5771d78b24
|
Logical with assigned value has higher rank. Notifications are to be dispatched accordingly.
|
2019-01-25 13:52:10 +01:00 |
|
Fedor Isakov
|
e645ac8a70
|
Support for unassigned logical variables in unification. Fix cycle not detected.
|
2019-01-25 11:37:18 +01:00 |
|
Fedor Isakov
|
b523467c5f
|
Test a weird case of rule not triggered for a particular combination of constraints.
|
2019-01-24 16:01:55 +01:00 |
|
Fedor Isakov
|
181ccedd95
|
Establish the contract of OccurrenceMatcher to fail appropriately on unassigned logicals.
Fix processing of reactivated constraints in RuleMatcher, fix propagation history.
Minor code refactorings. Tests.
|
2019-01-24 12:03:04 +01:00 |
|
Fedor Isakov
|
fc1fcaaf9d
|
Cleanup a test: better layout of nested lists.
|
2019-01-21 11:20:30 +01:00 |
|
Fedor Isakov
|
e2ea78ef9e
|
Improve layout of constraints and dataforms. Get rid of unnecessary anchors and hacks.
|
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
|
27681ef80c
|
Switch substitution to work using equals predicate instead of equals() java method. Testing substitution on tricky cases.
|
2019-01-15 20:09:16 +01:00 |
|
Fedor Isakov
|
0b9fc55817
|
Make equals predicate respect trivial bindings: [X -> Y] where X is unified with Y. Tests.
|
2019-01-15 19:04:07 +01:00 |
|
Fedor Isakov
|
161f00355d
|
Fix equals predicate: make it conform to general contract of unification without additional bindings. Testing ask/tell eq.
|
2019-01-14 12:25:27 +01: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
|
6aa965c96c
|
Ignore commented out nodes while applying templates. Use node pointer to report locations of failed tests.
|
2019-01-13 15:14:14 +01:00 |
|
Fedor Isakov
|
197f09fb2b
|
Apply automatic migrations in the root project
|
2019-01-13 14:27:43 +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 |
|
Fedor Isakov
|
50487cd41c
|
Fix unification predicate implementation to properly process non-term arguments. Cleanup the code.
|
2019-01-13 14:26:35 +01:00 |
|
Fedor Isakov
|
29a44eac5d
|
Introduce automatic migration from eq to uni for basic scenario: logical on the left
|
2019-01-13 14:26:35 +01:00 |
|
Fedor Isakov
|
a46937b128
|
Change semantics of EqualsPredicate: ask returns true iff values are equal or the logicals are the same, tell throws exception if not
|
2019-01-13 14:26:35 +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
|
16153a23d1
|
Correctly display value assigned to a logical.
|
2019-01-09 13:01:57 +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 |
|
Fedor Isakov
|
bcb8efa653
|
Make editor for DataForm more usable, get rid of hacks in the layout. Introduce NewLineAttribute to manually insert new lines. Deprecate ListRole.
|
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 |