a40e50bc53
Temprorarily suppress errors in two locations due to constraints violation (to be fixed).
2019-01-31 12:05:35 +01:00
767444a5c0
Make LetClause able to suppress errors in its children.
2019-01-31 12:05:35 +01:00
012b8963cb
Fix errors found by model checker in lambdacalc sample.
2019-01-31 12:05:21 +01:00
24ac5447b3
Make ErrorAnnotation able to suppress errors.
2019-01-31 11:44:07 +01:00
9243c00c65
Fix issues found by model checker (ex typesystem).
2019-01-31 11:30:02 +01:00
dc1965fdc9
Introduce a test for running model checker on all models in the project as a part of CI.
2019-01-31 11:30:02 +01:00
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
172f74b6f8
lc: minor: Add some comments. Some cleanup.
2019-01-28 16:59:05 +03:00
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
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
41e8d3d96e
lc: Fix forgotten typeOf rule for 'fix' operator. Add typeclasses tests to test suite.
2019-01-28 11:38:33 +03:00
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
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
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
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
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
52348b2b38
Make comment look nicer with standard C-style representation.
...
Make Handler, MacroTable and their contents commentable.
2019-01-27 23:33:02 +01:00
613e895d17
Fix constraint rules editor to display "activate" section always.
...
Constraint rule to be entered with "on" keyword.
2019-01-27 22:56:07 +01:00
37b6afa642
Enable back working tests in lambdacalc
2019-01-26 14:15:30 +01:00
551a015ada
Fix unification predicate not doing occurrs check on tell.
2019-01-26 13:52:10 +01:00
f3c2f53fa6
Temporarily disable failing tests in lambdacalc sample
2019-01-25 15:02:26 +01:00
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
5771d78b24
Logical with assigned value has higher rank. Notifications are to be dispatched accordingly.
2019-01-25 13:52:10 +01:00
e645ac8a70
Support for unassigned logical variables in unification. Fix cycle not detected.
2019-01-25 11:37:18 +01:00
b523467c5f
Test a weird case of rule not triggered for a particular combination of constraints.
2019-01-24 16:01:55 +01:00
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
fc1fcaaf9d
Cleanup a test: better layout of nested lists.
2019-01-21 11:20:30 +01:00
e2ea78ef9e
Improve layout of constraints and dataforms. Get rid of unnecessary anchors and hacks.
2019-01-21 11:20:30 +01:00
5d5a102661
lc: minor: move Cons-list utils to its own handler
2019-01-16 18:19:11 +03:00
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
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
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
b0e5edb03a
lc: remove getType rule and translate type annotations to dataforms in macro; also minor changes
2019-01-16 11:48:09 +03:00
94659549bc
lc: fix failing test: fix usages of eq rule in subsumption
2019-01-16 11:14:41 +03:00
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
0b9fc55817
Make equals predicate respect trivial bindings: [X -> Y] where X is unified with Y. Tests.
2019-01-15 19:04:07 +01:00
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
7f7f290b01
Temporarily comment out two instances of let clause that produced errors in tests
2019-01-13 17:53:06 +01:00
dce532c5c7
Apply automatic migrations in lambdalc project
2019-01-13 17:53:01 +01:00
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
197f09fb2b
Apply automatic migrations in the root project
2019-01-13 14:27:43 +01:00
275070c786
Apply automatic migrations to mpscore subproject
2019-01-13 14:27:38 +01:00
08bed0c578
Apply automatic migrations to FitchProof subproject
2019-01-13 14:27:32 +01:00
50487cd41c
Fix unification predicate implementation to properly process non-term arguments. Cleanup the code.
2019-01-13 14:26:35 +01:00
29a44eac5d
Introduce automatic migration from eq to uni for basic scenario: logical on the left
2019-01-13 14:26:35 +01:00
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
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
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
eb80329a54
lc: change recover_varRef rule, propagate to recover_Var rule instead of duplicating it
2019-01-11 19:09:44 +03:00
fb4fe40973
lc: typeclasses: added structure, editor, constraints (mainly concerned with scoping) aspects
2019-01-11 19:09:44 +03:00
Fedor Isakov