grigorii.kirgizov
dba9a7ce26
lc: Provide visibility modifiers for helper constraint declarations
2019-02-13 12:23:13 +03:00
grigorii.kirgizov
e6b4a89da8
Run migration for adding default `public` visibility modifier
2019-02-12 19:02:34 +03:00
grigorii.kirgizov
e87c9654c1
lc: minor: Fix missed condition in guard on merging type constraints rule. Could have possibly led to bug in somewhere.
2019-02-06 16:00:31 +03:00
Fedor Isakov
0fcff76308
Re-save all models updated resolve info.
2019-02-06 13:22:32 +01:00
Fedor Isakov
b42d7553c8
Temporarily comment out an instance of let clause that produces different result in local inference.
2019-02-06 12:59:38 +01:00
Fedor Isakov
aa1a29a318
Make all tests in lambdacalc subproject pass including local inference.
2019-02-06 12:58:46 +01:00
grigorii.kirgizov
0cd29c5729
lc: Add type inference dependencies ('require' things) to output the same types for local type inf. Some renames.
...
Types from local & non-local type inf differ in 2 cases:
- different type variables names
- non-local typecheck fails, but some types still get to output
2019-02-05 13:03:51 +03:00
Fedor Isakov
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
Fedor Isakov
0fb0771ad7
Ensure parent of varRef is included into typechecking. This fixes some locally inferred types mismatch.
2019-02-02 16:11:38 +01:00
Fedor Isakov
6e85a2c4fa
Use custom matching strategy in lambdacalc tests.
2019-02-02 16:10:35 +01:00
Fedor Isakov
ebada478c6
Replace error annotation with suppress error annotation to indicate an expected constraint violation.
2019-02-01 14:17:57 +01:00
Fedor Isakov
e0b856634c
Add java plugin to all gradle scripts.
2019-02-01 14:15:57 +01:00
Fedor Isakov
38777cda51
Ensure failed test means failed build for all sample projects.
2019-02-01 14:15:04 +01:00
Fedor Isakov
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
Fedor Isakov
5b255f2a02
Fix references and introduce languages engaged on generation to keep compat. w/191 EAP.
2019-02-01 11:31:35 +01:00
Fedor Isakov
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
Fedor Isakov
81ee94c342
Fix gradle scripts to ensure model checker is run after everything else has heen built.
2019-01-31 17:39:39 +01:00
Fedor Isakov
a40e50bc53
Temprorarily suppress errors in two locations due to constraints violation (to be fixed).
2019-01-31 12:05:35 +01:00
Fedor Isakov
767444a5c0
Make LetClause able to suppress errors in its children.
2019-01-31 12:05:35 +01:00
Fedor Isakov
012b8963cb
Fix errors found by model checker in lambdacalc sample.
2019-01-31 12:05:21 +01:00
Fedor Isakov
9243c00c65
Fix issues found by model checker (ex typesystem).
2019-01-31 11:30:02 +01:00
grigorii.kirgizov
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
grigorii.kirgizov
172f74b6f8
lc: minor: Add some comments. Some cleanup.
2019-01-28 16:59:05 +03:00
grigorii.kirgizov
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
grigorii.kirgizov
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
grigorii.kirgizov
41e8d3d96e
lc: Fix forgotten typeOf rule for 'fix' operator. Add typeclasses tests to test suite.
2019-01-28 11:38:33 +03:00
grigorii.kirgizov
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
grigorii.kirgizov
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
grigorii.kirgizov
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
grigorii.kirgizov
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
grigorii.kirgizov
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
Fedor Isakov
37b6afa642
Enable back working tests in lambdacalc
2019-01-26 14:15:30 +01:00
Fedor Isakov
f3c2f53fa6
Temporarily disable failing tests in lambdacalc sample
2019-01-25 15:02:26 +01:00
Fedor Isakov
fc1fcaaf9d
Cleanup a test: better layout of nested lists.
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
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
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
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