From c8233c24d76a3c49db51dc471b2000b2662475db Mon Sep 17 00:00:00 2001 From: "grigorii.kirgizov" Date: Fri, 11 Jan 2019 19:03:10 +0300 Subject: [PATCH] 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 --- .../samples.lambdacalc/models/types.mps | 1971 ++++++----------- 1 file changed, 655 insertions(+), 1316 deletions(-) diff --git a/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps b/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps index 63cd4659..97244ff3 100644 --- a/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps +++ b/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps @@ -454,7 +454,6 @@ - @@ -1435,7 +1434,7 @@ - + @@ -1445,11 +1444,6 @@ - - - - - @@ -2363,341 +2357,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -3712,16 +3371,6 @@ - - - - - - - - - - @@ -4261,7 +3910,7 @@ - + @@ -4362,155 +4011,188 @@ - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - + + + + + + + + + + + + - + - - - + + + - - - + + + - + + + + + + + - - - - - - - - - + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + @@ -4519,247 +4201,14 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + @@ -5154,136 +4603,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -5598,26 +4917,8 @@ - - - - - - - - - - - - - - - - - - - + @@ -5627,9 +4928,6 @@ - - - @@ -5663,9 +4961,6 @@ - - - @@ -5874,12 +5169,6 @@ - - - - - - @@ -5892,9 +5181,6 @@ - - - @@ -5917,237 +5203,133 @@ - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + - - - + + + - + - + - - - + + + - + - - - + + + - - - - - - - + + - - - + + + - - + + - + - + - - + + - + - + - - + + - + - - - - - - - - + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - - - + + + - - - - - - - - - - - - - - + + - - + + - - - - - - - + + - - - - + + + + - + - + - - - + + + - + - - - + + + @@ -6158,12 +5340,12 @@ - - - - - - + + + + + + @@ -6172,12 +5354,6 @@ - - - - - - @@ -6216,9 +5392,6 @@ - - - @@ -6243,12 +5416,6 @@ - - - - - - @@ -6261,9 +5428,6 @@ - - - @@ -6281,7 +5445,7 @@ - + @@ -6291,9 +5455,6 @@ - - - @@ -6313,12 +5474,6 @@ - - - - - - @@ -6331,9 +5486,6 @@ - - - @@ -6969,102 +6121,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -7281,94 +6337,83 @@ - - - - - - - - - - - - - - - - - - - + + + + + + + + - + - - + + - - + + - + - + - - - - + + + + - - - + + + - + - + - - - + + + - + - - - + + + - - - + + + - + - + - - - + + + - + - - - + + + @@ -7378,34 +6423,48 @@ - - - - - - + + + + + + - + - + - - - + + + - - + + - - + + - - + + + + + + + + + + + + + + + + @@ -7413,23 +6472,157 @@ - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - + + + + + + - + - + @@ -7596,16 +6789,22 @@ + + + + + + - - + + - + @@ -8195,6 +7394,158 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -8739,65 +8090,53 @@ - + - - - - - - - - - - - + + + + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - - - - - - + + + + + + + + + + + - - - - - - - - - - - - - - - -