From ecc6c4aed2d7d7353e31d3f96c142c3645aca769 Mon Sep 17 00:00:00 2001 From: "grigorii.kirgizov" Date: Mon, 21 Jan 2019 13:21:06 +0300 Subject: [PATCH] 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. --- .../samples.lambdacalc/models/types.mps | 776 +++++++---- .../models/samples.lambdacalc.demo.mps | 1219 ++++++++++++++++- 2 files changed, 1741 insertions(+), 254 deletions(-) diff --git a/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps b/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps index 248266e0..b1405bca 100644 --- a/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps +++ b/samples/lambdacalc/languages/samples.lambdacalc/models/types.mps @@ -38,6 +38,7 @@ + @@ -99,6 +100,7 @@ + @@ -182,6 +184,7 @@ + @@ -210,7 +213,6 @@ - @@ -276,6 +278,7 @@ + @@ -358,12 +361,16 @@ + + + + @@ -378,6 +385,7 @@ + @@ -1038,7 +1046,10 @@ - + + + + @@ -1168,7 +1179,10 @@ - + + + + @@ -1459,6 +1473,15 @@ + + + + + + + + + @@ -1509,9 +1532,6 @@ - - - @@ -1564,7 +1584,7 @@ - + @@ -4405,7 +4425,7 @@ - + @@ -4414,6 +4434,39 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -5688,10 +5741,10 @@ - + @@ -6058,39 +6111,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -8473,7 +8493,7 @@ - + @@ -8595,7 +8615,7 @@ - + @@ -9942,6 +9962,29 @@ + + + + + + + + + + + + + + + + + + + + + + + @@ -10049,6 +10092,54 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -10060,6 +10151,16 @@ + + + + + + + + + + @@ -10116,9 +10217,13 @@ - - - + + + + + + + @@ -10150,6 +10255,24 @@ + + + + + + + + + + + + + + + + + + @@ -10363,11 +10486,6 @@ - - - - - @@ -10694,6 +10812,15 @@ + + + + + + + + + @@ -10915,57 +11042,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -11290,6 +11366,57 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -11308,6 +11435,9 @@ + + + @@ -11394,6 +11524,72 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -11707,78 +11903,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -11844,6 +11968,78 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -11895,7 +12091,7 @@ - + @@ -11985,12 +12181,6 @@ - - - - - - @@ -12001,7 +12191,7 @@ - + @@ -12045,7 +12235,7 @@ - + @@ -12059,11 +12249,6 @@ - - - - - @@ -12091,14 +12276,7 @@ - - - - - - - - + @@ -12132,12 +12310,6 @@ - - - - - - @@ -12239,12 +12411,6 @@ - - - - - - @@ -12367,6 +12533,11 @@ + + + + + @@ -12470,32 +12641,14 @@ - - - - - - - - - - - - - - - - - - - - + + - + - - + + @@ -12510,6 +12663,43 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -12548,8 +12738,8 @@ - - + + @@ -12561,8 +12751,8 @@ - - + + @@ -12576,18 +12766,38 @@ + + + + + + - - - - + + + + + + + + + + + + + + + + + + - - + + @@ -12596,6 +12806,61 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -12606,8 +12871,8 @@ - - + + @@ -12624,6 +12889,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 aadb41b4..d80f68cc 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 @@ -90,7 +90,7 @@ - + @@ -3848,13 +3848,158 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + - + @@ -3862,7 +4007,7 @@ - + @@ -3873,20 +4018,668 @@ - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -3953,7 +4746,7 @@ - + @@ -4058,12 +4851,12 @@ - + - + @@ -4081,6 +4874,412 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +