adds tracing for markup strings (#67)

adds tracing for chapter 19

tests-system/lint-ug-examples/div_by_zero.rsl

@@ -0,0 +1,13 @@
+package Div_By_Zero
+
+type T {
+  x Integer
+  y Integer
+}
+
+checks T {
+  x > 2, fatal "x too small"
+  y > 2, fatal "y too small"
+
+  100 / (111 - x * y) > 0, "example"
+}

tests-system/lint-ug-examples/options

@@ -0,0 +1 @@
+--no-detailed-info

tests-system/lint-ug-examples/output

@@ -1,40 +1,25 @@
 type Q extends T {
      ^ lint-ug-examples/clarify_final.rsl:7: issue: consider clarifying that this record is final [clarify_final]
-     | Parent record Clarify_Final.T is final, making this record
-     | also final. Marking it explicitly as final
-     | clarifies this to casual readers.
 -x / 3 < 0, "non-obvious meaning"
 ^ lint-ug-examples/unary_minus_precedence.rsl:8: issue: expression means -(x / 3), place explicit brackets to clarify intent [unary_minus_precedence]
 description != null, "description cannot be empty"
             ^^ lint-ug-examples/always_true.rsl:12: issue: expression is always true [vcg-always-true]
 len(x) >= 3 implies x[3] > 0, "too small"
                      ^ lint-ug-examples/array_index.rsl:8: issue: array index could be larger than len(x) [vcg-array-index]
-                     | example record_type triggering error:
-                     |   T bad_potato {
-                     |     x = [1, 1, 1]
-                     |   }
+100 / (111 - x * y) > 0, "example"
+    ^ lint-ug-examples/div_by_zero.rsl:12: issue: divisor could be 0 [vcg-div-by-zero]
 len(description) >= 10, "too short"
     ^^^^^^^^^^^ lint-ug-examples/evaluation_of_null.rsl:8: issue: expression could be null [vcg-evaluation-of-null]
-              | example record_type triggering error:
-              |   Requirement bad_potato {
-              |     /* description is null */
-              |   }
 x Integer [10 .. 3]
                  ^ lint-ug-examples/impossible_array_types.rsl:4: issue: upper bound must be at least 10 [impossible_array_types]
 y Integer [0 .. 0]
                 ^ lint-ug-examples/impossible_array_types.rsl:5: issue: this array makes no sense [impossible_array_types]
 separator x
           ^ lint-ug-examples/separator_based_literal_ambiguity.rsl:5: issue: x separator after integer component creates ambiguities [separator_based_literal_ambiguity]
-          | For example 0x100 would be a base 16 literal
-          | instead of the tuple segment 0 x 100.
 x Integer [1 .. 1]
                 ^ lint-ug-examples/weird_array_types.rsl:4: issue: array of fixed size 1 should not be an array [weird_array_types]
-                | An array with a fixed size of 1 should not
-                | be an array at all.
 y Integer [0 .. 1]
                 ^ lint-ug-examples/weird_array_types.rsl:5: issue: consider making this array an optional Integer [weird_array_types]
-                | An array with 0 to 1 components should just
-                | be an optional Integer instead.
 abstract type T {
               ^ lint-ug-examples/abstract_leaf_types.rsl:3: issue: abstract type T does not have any extensions [abstract_leaf_types]
-Processed 13 models and 0 requirement files and found 11 warnings
+Processed 14 models and 0 requirement files and found 12 warnings

tests-system/lint-ug-examples/output.json

@@ -1,2 +1,2 @@
 {}
-Processed 13 models and 0 requirement files and found no issues
+Processed 14 models and 0 requirement files and found no issues

tests-system/lint-ug-examples/output.smtlib

@@ -1,40 +1,25 @@
 type Q extends T {
      ^ lint-ug-examples/clarify_final.rsl:7: issue: consider clarifying that this record is final [clarify_final]
-     | Parent record Clarify_Final.T is final, making this record
-     | also final. Marking it explicitly as final
-     | clarifies this to casual readers.
 -x / 3 < 0, "non-obvious meaning"
 ^ lint-ug-examples/unary_minus_precedence.rsl:8: issue: expression means -(x / 3), place explicit brackets to clarify intent [unary_minus_precedence]
 description != null, "description cannot be empty"
             ^^ lint-ug-examples/always_true.rsl:12: issue: expression is always true [vcg-always-true]
 len(x) >= 3 implies x[3] > 0, "too small"
                      ^ lint-ug-examples/array_index.rsl:8: issue: array index could be larger than len(x) [vcg-array-index]
-                     | example record_type triggering error:
-                     |   T bad_potato {
-                     |     x = [1, 1, 1]
-                     |   }
+100 / (111 - x * y) > 0, "example"
+    ^ lint-ug-examples/div_by_zero.rsl:12: issue: divisor could be 0 [vcg-div-by-zero]
 len(description) >= 10, "too short"
     ^^^^^^^^^^^ lint-ug-examples/evaluation_of_null.rsl:8: issue: expression could be null [vcg-evaluation-of-null]
-              | example record_type triggering error:
-              |   Requirement bad_potato {
-              |     /* description is null */
-              |   }
 x Integer [10 .. 3]
                  ^ lint-ug-examples/impossible_array_types.rsl:4: issue: upper bound must be at least 10 [impossible_array_types]
 y Integer [0 .. 0]
                 ^ lint-ug-examples/impossible_array_types.rsl:5: issue: this array makes no sense [impossible_array_types]
 separator x
           ^ lint-ug-examples/separator_based_literal_ambiguity.rsl:5: issue: x separator after integer component creates ambiguities [separator_based_literal_ambiguity]
-          | For example 0x100 would be a base 16 literal
-          | instead of the tuple segment 0 x 100.
 x Integer [1 .. 1]
                 ^ lint-ug-examples/weird_array_types.rsl:4: issue: array of fixed size 1 should not be an array [weird_array_types]
-                | An array with a fixed size of 1 should not
-                | be an array at all.
 y Integer [0 .. 1]
                 ^ lint-ug-examples/weird_array_types.rsl:5: issue: consider making this array an optional Integer [weird_array_types]
-                | An array with 0 to 1 components should just
-                | be an optional Integer instead.
 abstract type T {
               ^ lint-ug-examples/abstract_leaf_types.rsl:3: issue: abstract type T does not have any extensions [abstract_leaf_types]
-Processed 13 models and 0 requirement files and found 11 warnings
+Processed 14 models and 0 requirement files and found 12 warnings

tests-system/rbt-markup-string-errors/foo.rsl

@@ -0,0 +1,5 @@
+package Foo
+
+type T {
+    a Markup_String
+}

tests-system/rbt-markup-string-errors/foo.trlc

@@ -0,0 +1,13 @@
+package Foo
+
+T Bar {
+    a = "[[Bar"
+}
+
+T But {
+    a = "But]]"
+}
+
+T Baz {
+    a = "[[Baz[[But]]]]"
+}

tests-system/rbt-markup-string-errors/output

@@ -0,0 +1,7 @@
+a = "[[Bar"
+       ^^^ rbt-markup-string-errors/foo.trlc:4: error: expected ]], encountered end-of-string instead
+a = "But]]"
+        ^^ rbt-markup-string-errors/foo.trlc:8: error: opening [[ for this ]] found
+a = "[[Baz[[But]]]]"
+          ^^ rbt-markup-string-errors/foo.trlc:12: error: cannot nest reference lists
+Processed 1 model and 1 requirement file and found 3 errors

tests-system/rbt-markup-string-errors/output.brief

@@ -0,0 +1,3 @@
+rbt-markup-string-errors/foo.trlc:4:12: trlc error: expected ]], encountered end-of-string instead
+rbt-markup-string-errors/foo.trlc:8:13: trlc error: opening [[ for this ]] found
+rbt-markup-string-errors/foo.trlc:12:15: trlc error: cannot nest reference lists

tests-system/rbt-markup-string-errors/output.json

@@ -0,0 +1,7 @@
+a = "[[Bar"
+       ^^^ rbt-markup-string-errors/foo.trlc:4: error: expected ]], encountered end-of-string instead
+a = "But]]"
+        ^^ rbt-markup-string-errors/foo.trlc:8: error: opening [[ for this ]] found
+a = "[[Baz[[But]]]]"
+          ^^ rbt-markup-string-errors/foo.trlc:12: error: cannot nest reference lists
+Processed 1 model and 1 requirement file and found 3 errors

tests-system/rbt-markup-string-errors/output.smtlib

@@ -0,0 +1,7 @@
+a = "[[Bar"
+       ^^^ rbt-markup-string-errors/foo.trlc:4: error: expected ]], encountered end-of-string instead
+a = "But]]"
+        ^^ rbt-markup-string-errors/foo.trlc:8: error: opening [[ for this ]] found
+a = "[[Baz[[But]]]]"
+          ^^ rbt-markup-string-errors/foo.trlc:12: error: cannot nest reference lists
+Processed 1 model and 1 requirement file and found 3 errors

tests-system/rbt-markup-string-format/foo.rsl

@@ -0,0 +1,5 @@
+package Foo
+
+type T {
+    a Markup_String
+}

tests-system/rbt-markup-string-format/foo.trlc

@@ -0,0 +1,9 @@
+package Foo
+
+T Bar {
+    a = "bar [[Inline]]"
+}
+
+T Inline {
+    a = "inline"
+}

tests-system/rbt-markup-string-format/output

@@ -0,0 +1 @@
+Processed 1 model and 1 requirement file and found no issues

tests-system/rbt-markup-string-format/output.json

@@ -0,0 +1,9 @@
+{
+  "Bar": {
+    "a": "bar [[Inline]]"
+  },
+  "Inline": {
+    "a": "inline"
+  }
+}
+Processed 1 model and 1 requirement file and found no issues

tests-system/rbt-markup-string-format/output.smtlib

@@ -0,0 +1 @@
+Processed 1 model and 1 requirement file and found no issues

tests-system/rbt-markup-string-late-reference-resolution/foo.rsl

@@ -0,0 +1,5 @@
+package Foo
+
+type T {
+    a Markup_String
+}

tests-system/rbt-markup-string-late-reference-resolution/foo.trlc

@@ -0,0 +1,13 @@
+package Foo
+
+T Bar {
+    a = "[[Bar]]"
+}
+
+T But {
+    a = "[[Baz]]"
+}
+
+T Baz {
+    a = "[[Baz]]"
+}

tests-system/rbt-markup-string-late-reference-resolution/output

@@ -0,0 +1 @@
+Processed 1 model and 1 requirement file and found no issues

tests-system/rbt-markup-string-late-reference-resolution/output.json

@@ -0,0 +1,12 @@
+{
+  "Bar": {
+    "a": "[[Bar]]"
+  },
+  "Baz": {
+    "a": "[[Baz]]"
+  },
+  "But": {
+    "a": "[[Baz]]"
+  }
+}
+Processed 1 model and 1 requirement file and found no issues

tests-system/rbt-markup-string-late-reference-resolution/output.smtlib

@@ -0,0 +1 @@
+Processed 1 model and 1 requirement file and found no issues

tests-system/rbt-markup-string-resolution/foo.rsl

@@ -0,0 +1,5 @@
+package Foo
+
+type T {
+    a Markup_String
+}

tests-system/rbt-markup-string-resolution/foo.trlc

@@ -0,0 +1,5 @@
+package Foo
+
+T Bar {
+    a = "[[Bar]]"
+}

tests-system/rbt-markup-string-resolution/output

@@ -0,0 +1,3 @@
+a = "[[Foo.Bar]]"
+       ^^^ rbt-markup-string-resolution/potato.trlc:4: error: package must be imported before use
+Processed 2 models and 2 requirement files and found 1 error

tests-system/rbt-markup-string-resolution/output.brief

@@ -0,0 +1 @@
+rbt-markup-string-resolution/potato.trlc:4:12: trlc error: package must be imported before use

tests-system/rbt-markup-string-resolution/output.json

@@ -0,0 +1,3 @@
+a = "[[Foo.Bar]]"
+       ^^^ rbt-markup-string-resolution/potato.trlc:4: error: package must be imported before use
+Processed 2 models and 2 requirement files and found 1 error

tests-system/rbt-markup-string-resolution/output.smtlib

@@ -0,0 +1,3 @@
+a = "[[Foo.Bar]]"
+       ^^^ rbt-markup-string-resolution/potato.trlc:4: error: package must be imported before use
+Processed 2 models and 2 requirement files and found 1 error

tests-system/rbt-markup-string-resolution/potato.rsl

@@ -0,0 +1,5 @@
+package Potato
+
+type T {
+    a Markup_String
+}

tests-system/rbt-markup-string-resolution/potato.trlc

@@ -0,0 +1,5 @@
+package Potato
+
+T Kitten {
+    a = "[[Foo.Bar]]"
+}

tests-system/rbt-markup-string-types/foo.rsl

@@ -0,0 +1,5 @@
+package Foo
+
+type T {
+    a Markup_String
+}

tests-system/rbt-markup-string-types/foo.trlc

@@ -0,0 +1,9 @@
+package Foo
+
+T Bar {
+    a = "[[T]]"
+}
+
+T But {
+    a = "[[But]]"
+}

tests-system/rbt-markup-string-types/output

@@ -0,0 +1,3 @@
+a = "[[T]]"
+       ^ rbt-markup-string-types/foo.trlc:4: error: Record_Type T is not a Record_Object
+Processed 1 model and 1 requirement file and found 1 error

tests-system/rbt-markup-string-types/output.brief

@@ -0,0 +1 @@
+rbt-markup-string-types/foo.trlc:4:12: trlc error: Record_Type T is not a Record_Object

tests-system/rbt-markup-string-types/output.json

@@ -0,0 +1,3 @@
+a = "[[T]]"
+       ^ rbt-markup-string-types/foo.trlc:4: error: Record_Type T is not a Record_Object
+Processed 1 model and 1 requirement file and found 1 error

tests-system/rbt-markup-string-types/output.smtlib

@@ -0,0 +1,3 @@
+a = "[[T]]"
+       ^ rbt-markup-string-types/foo.trlc:4: error: Record_Type T is not a Record_Object
+Processed 1 model and 1 requirement file and found 1 error

trlc/parser.py

@@ -27,6 +27,8 @@
 
 
 class Markup_Token(Token_Base):
+    # lobster-trace: LRM.Markup_String_Format
+
     KIND = {
         "CHARACTER"          : "character",
         "REFLIST_BEGIN"      : "[[",
@@ -51,6 +53,8 @@ def file_location(self):
         return self.origin_location
 
     def token(self):
+        # lobster-trace: LRM.Markup_String_Errors
+
         if self.in_reflist:
             self.skip_whitespace()
         else:
@@ -249,6 +253,9 @@ def parse_qualified_name(self):
         # lobster-trace: LRM.Qualified_Name
         # lobster-trace: LRM.Valid_Qualifier
         # lobster-trace: LRM.Valid_Name
+        # lobster-trace: LRM.Markup_String_Resolution
+        # lobster-trace: LRM.Markup_String_Types
+
         self.match("REFLIST_IDENTIFIER")
         if self.peek("REFLIST_DOT"):
             package = self.parent.stab.lookup_direct(

trlc/trlc.py

@@ -456,6 +456,7 @@ def parse_trlc_files(self):
         return ok
 
     def resolve_record_references(self):
+        # lobster-trace: LRM.Markup_String_Late_Reference_Resolution
         # lobster-trace: LRM.Late_Reference_Checking
         ok = True
         for package in self.stab.values(ast.Package):