From a2012219b78f12966f80f3ed03bb9ffa7107108d Mon Sep 17 00:00:00 2001 From: "grigorii.kirgizov" Date: Mon, 28 Jan 2019 13:32:32 +0300 Subject: [PATCH] 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. --- .../samples.lambdacalc/models/types.mps | 827 ++++++------------ .../models/samples.lambdacalc.demo.mps | 589 ++++++++++--- .../models/samples.lambdacalc.demo@tests.mps | 63 +- 3 files changed, 743 insertions(+), 736 deletions(-) diff --git a/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps b/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps index 4947d607..dc4b8f64 100644 --- a/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps +++ b/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps @@ -2040,118 +2040,122 @@ - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - + + + + - - - - - + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + - - - - - + + + + + @@ -6559,7 +6563,7 @@ - + @@ -6583,7 +6587,7 @@ - + @@ -6598,7 +6602,7 @@ - + @@ -6628,7 +6632,7 @@ - + @@ -6636,7 +6640,7 @@ - + @@ -6705,6 +6709,37 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -6723,15 +6758,9 @@ - - - - - - - - - + + + @@ -6760,6 +6789,22 @@ + + + + + + + + + + + + + + + + @@ -6780,7 +6825,7 @@ - + @@ -6788,7 +6833,7 @@ - + @@ -6845,7 +6890,7 @@ - + @@ -6905,7 +6950,7 @@ - + @@ -6914,14 +6959,6 @@ - - - - - - - - @@ -11619,16 +11656,13 @@ - + - - + + - - - - - + + @@ -11801,7 +11835,6 @@ - @@ -11856,212 +11889,76 @@ - + - - - - + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - - - - - - + + + + + + + + + + - - - - + + + + - - - - - - - - - - + + - - + + - - - - + + + + - - + + - - - - - - - - - - - - - - - - + + @@ -12069,220 +11966,39 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + @@ -12710,7 +12426,12 @@ - + + + + + + @@ -13009,6 +12730,11 @@ + + + + + @@ -13051,43 +12777,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -13115,12 +12804,6 @@ - - - - - - @@ -13138,6 +12821,11 @@ + + + + + @@ -13219,6 +12907,29 @@ + + + + + + + + + + + + + + + + + + + + + + + diff --git a/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo.mps b/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo.mps index c9cbefbd..0588a427 100644 --- a/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo.mps +++ b/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo.mps @@ -2208,6 +2208,9 @@ + + + @@ -2217,9 +2220,6 @@ - - - @@ -4534,6 +4534,9 @@ + + + @@ -4607,146 +4610,147 @@ - - - - - - - - - + + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + + + + + + + - - - - - + + + + + - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -4938,6 +4942,9 @@ + + + @@ -4949,7 +4956,7 @@ - + @@ -4979,7 +4986,7 @@ - + @@ -4996,9 +5003,6 @@ - - - @@ -5016,7 +5020,7 @@ - + @@ -5078,7 +5082,7 @@ - + @@ -5129,7 +5133,7 @@ - + @@ -5177,15 +5181,12 @@ - - - - + @@ -5257,7 +5258,7 @@ - + @@ -5288,6 +5289,9 @@ + + + @@ -5811,5 +5815,322 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo@tests.mps b/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo@tests.mps index 2c2ef7c7..9fba8e2b 100644 --- a/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo@tests.mps +++ b/samples/lambdacalc/solutions/samples.lambdacalc.demo/models/samples.lambdacalc.demo@tests.mps @@ -69,12 +69,6 @@ - - - - - - @@ -132,19 +126,9 @@ - - - - - - - - - - @@ -394,41 +378,32 @@ - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + - - - - + - - + + + + +