From 3c27aa79e1571ae7702f85d64d0754c03fc32d74 Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Sun, 5 Apr 2015 12:02:25 +0200 Subject: [PATCH] More strict checking of rules, fixing minor problems reported by model checker, minor update of the rules runner --- .../generator/template/main@generator.mps | 101 ++- .../jetbrains.mps.lang.typesystem2.mpl | 7 +- .../languageModels/typesystem.mps | 647 +++++++++++++++++- .../mps/lang/typesystem2/runtime/rule.mps | 247 ++++--- ....lang.typesystem2.samplechecker.runner.msd | 5 + .../lang/typesystem2/samplechecker/runner.mps | 12 +- .../lang/typesystem2/sampleplugin/plugin.mps | 148 ++-- .../languageModels/constraints.mps | 96 ++- .../mps/logic/builtin/unification.mps | 17 +- .../mps/typechecking/rule/generator.mps | 2 +- 10 files changed, 1092 insertions(+), 190 deletions(-) diff --git a/languages/jetbrains.mps.lang.typesystem2/generator/template/main@generator.mps b/languages/jetbrains.mps.lang.typesystem2/generator/template/main@generator.mps index c889934f..095f3b59 100644 --- a/languages/jetbrains.mps.lang.typesystem2/generator/template/main@generator.mps +++ b/languages/jetbrains.mps.lang.typesystem2/generator/template/main@generator.mps @@ -105,6 +105,7 @@ + @@ -293,6 +294,7 @@ + @@ -302,6 +304,7 @@ + @@ -309,6 +312,9 @@ + + + @@ -2476,6 +2482,7 @@ + @@ -2970,6 +2977,25 @@ + + + + + + + + + + + + + + + + + + + @@ -3625,6 +3651,10 @@ + + + + @@ -3750,15 +3780,15 @@ + + + - - - @@ -4335,8 +4365,24 @@ - - + + + + + + + + + + + + + + + + + + @@ -5187,9 +5233,6 @@ - - - @@ -5268,6 +5311,9 @@ + + + @@ -7194,7 +7240,28 @@ - + + + + + + + + + + + + + + + + + + + + + + @@ -7318,15 +7385,15 @@ + + + - - - @@ -7454,15 +7521,15 @@ + + + - - - @@ -7527,8 +7594,8 @@ - - + + diff --git a/languages/jetbrains.mps.lang.typesystem2/jetbrains.mps.lang.typesystem2.mpl b/languages/jetbrains.mps.lang.typesystem2/jetbrains.mps.lang.typesystem2.mpl index e4a84c9c..aee398df 100644 --- a/languages/jetbrains.mps.lang.typesystem2/jetbrains.mps.lang.typesystem2.mpl +++ b/languages/jetbrains.mps.lang.typesystem2/jetbrains.mps.lang.typesystem2.mpl @@ -60,11 +60,12 @@ - 2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel) - c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure) 26e8f4ce-2a35-4f44-8065-e5ba154b18e9(jetbrains.mps.lang.typesystem2.runtime) 6354ebe7-c22a-4a0f-ac54-50b52ab9b065(JDK) 35320f26-77cb-4c55-be9f-a97a27770af1(jetbrains.mps.logic) + 2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel) + c4803b19-6d89-4a3b-bf82-390769514add(jetbrains.mps.lang.typesystem2) + c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure) daafa647-f1f7-4b0b-b096-69cd7c8408c0(jetbrains.mps.baseLanguage.regexp) @@ -112,9 +113,9 @@ 7866978e-a0f0-4cc7-81bc-4d213d9375e1(jetbrains.mps.lang.smodel) - f3061a53-9226-4cc5-a443-f952ceaf5816(jetbrains.mps.baseLanguage) 83888646-71ce-4f1c-9c53-c54016f6ad4f(jetbrains.mps.baseLanguage.collections) 35320f26-77cb-4c55-be9f-a97a27770af1(jetbrains.mps.logic) + f3061a53-9226-4cc5-a443-f952ceaf5816(jetbrains.mps.baseLanguage) diff --git a/languages/jetbrains.mps.lang.typesystem2/languageModels/typesystem.mps b/languages/jetbrains.mps.lang.typesystem2/languageModels/typesystem.mps index 4a6eebe2..5279b128 100644 --- a/languages/jetbrains.mps.lang.typesystem2/languageModels/typesystem.mps +++ b/languages/jetbrains.mps.lang.typesystem2/languageModels/typesystem.mps @@ -6,19 +6,89 @@ - + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -33,9 +103,16 @@ + + + + + + + @@ -56,7 +133,27 @@ + + + + + + + + + + + + + + + + + + + + @@ -65,9 +162,15 @@ + + + + + + @@ -82,6 +185,13 @@ + + + + + + + @@ -219,5 +329,538 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/languages/jetbrains.mps.lang.typesystem2/runtime/models/jetbrains/mps/lang/typesystem2/runtime/rule.mps b/languages/jetbrains.mps.lang.typesystem2/runtime/models/jetbrains/mps/lang/typesystem2/runtime/rule.mps index ee83b1ee..afe7aaec 100644 --- a/languages/jetbrains.mps.lang.typesystem2/runtime/models/jetbrains/mps/lang/typesystem2/runtime/rule.mps +++ b/languages/jetbrains.mps.lang.typesystem2/runtime/models/jetbrains/mps/lang/typesystem2/runtime/rule.mps @@ -3134,9 +3134,53 @@ - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -3444,89 +3488,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -3564,8 +3525,11 @@ - - + + + + + @@ -3679,6 +3643,113 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.runner/jetbrains.mps.lang.typesystem2.samplechecker.runner.msd b/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.runner/jetbrains.mps.lang.typesystem2.samplechecker.runner.msd index 868b4ac6..a86025b7 100644 --- a/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.runner/jetbrains.mps.lang.typesystem2.samplechecker.runner.msd +++ b/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.runner/jetbrains.mps.lang.typesystem2.samplechecker.runner.msd @@ -11,6 +11,7 @@ 6354ebe7-c22a-4a0f-ac54-50b52ab9b065(JDK) a5478664-6b44-4c62-a9f7-434f8aa57eee(jetbrains.mps.logic.runtime) 6ed54515-acc8-4d1e-a16c-9fd6cfe951ea(MPS.Core) + 3ddddf69-9ff0-426b-9365-51ae7356fb82(jetbrains.mps.lang.typesystem2.sample) 7526e0cf-1ce7-46f8-a555-9eca1e06c23b(jetbrains.mps.unification.tree) b984ee52-f34d-4b6d-8812-866c1d3eae31(jetbrains.mps.jchr.runtime) @@ -19,13 +20,17 @@ 894463aa-8754-49c0-bf4b-6a32af66b376(jetbrains.mps.jchr) 35320f26-77cb-4c55-be9f-a97a27770af1(jetbrains.mps.logic) 760a0a8c-eabb-4521-8bfd-65db761a9ba3(jetbrains.mps.baseLanguage.logging) + 7866978e-a0f0-4cc7-81bc-4d213d9375e1(jetbrains.mps.lang.smodel) + + + diff --git a/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.runner/models/jetbrains/mps/lang/typesystem2/samplechecker/runner.mps b/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.runner/models/jetbrains/mps/lang/typesystem2/samplechecker/runner.mps index 1daf97f4..5032564b 100644 --- a/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.runner/models/jetbrains/mps/lang/typesystem2/samplechecker/runner.mps +++ b/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.runner/models/jetbrains/mps/lang/typesystem2/samplechecker/runner.mps @@ -6,6 +6,7 @@ + @@ -17,7 +18,6 @@ - @@ -273,9 +273,6 @@ - - - @@ -287,17 +284,20 @@ - + - + + + + diff --git a/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.sampleplugin/models/jetbrains/mps/lang/typesystem2/sampleplugin/plugin.mps b/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.sampleplugin/models/jetbrains/mps/lang/typesystem2/sampleplugin/plugin.mps index 2ebb94a3..f8a4340a 100644 --- a/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.sampleplugin/models/jetbrains/mps/lang/typesystem2/sampleplugin/plugin.mps +++ b/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.sampleplugin/models/jetbrains/mps/lang/typesystem2/sampleplugin/plugin.mps @@ -1669,10 +1669,51 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -1716,25 +1757,45 @@ - - - - - - + + + + - - + + - + + + + + + + + + + + + + + + + + + + + + + + @@ -2739,44 +2800,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -3541,8 +3564,13 @@ - - + + + + + + + @@ -3618,6 +3646,28 @@ + + + + + + + + + + + + + + + + + + + + + + diff --git a/languages/jetbrains.mps.logic/languageModels/constraints.mps b/languages/jetbrains.mps.logic/languageModels/constraints.mps index 922d5801..6d7bf7ea 100644 --- a/languages/jetbrains.mps.logic/languageModels/constraints.mps +++ b/languages/jetbrains.mps.logic/languageModels/constraints.mps @@ -11,13 +11,14 @@ - - + + + @@ -87,6 +88,9 @@ + + + @@ -99,6 +103,10 @@ + + + + @@ -250,20 +258,78 @@ - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - + + + + + + + + + + + + + + + + + + + + + diff --git a/languages/jetbrains.mps.logic/runtime/models/jetbrains/mps/logic/builtin/unification.mps b/languages/jetbrains.mps.logic/runtime/models/jetbrains/mps/logic/builtin/unification.mps index 692bf578..26bbc9f9 100644 --- a/languages/jetbrains.mps.logic/runtime/models/jetbrains/mps/logic/builtin/unification.mps +++ b/languages/jetbrains.mps.logic/runtime/models/jetbrains/mps/logic/builtin/unification.mps @@ -4392,12 +4392,11 @@ - - - + + - + @@ -4411,12 +4410,12 @@ - + - + @@ -4424,7 +4423,7 @@ - + @@ -4436,7 +4435,7 @@ - + @@ -4449,7 +4448,7 @@ - + diff --git a/solutions/jetbrains.mps.typechecking.rules/models/jetbrains/mps/typechecking/rule/generator.mps b/solutions/jetbrains.mps.typechecking.rules/models/jetbrains/mps/typechecking/rule/generator.mps index 75eb698b..0ccbe458 100644 --- a/solutions/jetbrains.mps.typechecking.rules/models/jetbrains/mps/typechecking/rule/generator.mps +++ b/solutions/jetbrains.mps.typechecking.rules/models/jetbrains/mps/typechecking/rule/generator.mps @@ -1179,7 +1179,7 @@ - +