adds tracing for check files (#35)

adds tracing for chapter 9

tests-system/rbt-cannot-declare-in-check-file/foo.check

@@ -0,0 +1 @@
+package Foo

tests-system/rbt-cannot-declare-in-check-file/output

@@ -0,0 +1,3 @@
+package Foo
+        ^^^ rbt-cannot-declare-in-check-file/foo.check:1: error: unknown symbol Foo
+Processed 0 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/rbt-cannot-declare-in-check-file/output.brief

@@ -0,0 +1 @@
+rbt-cannot-declare-in-check-file/foo.check:1:9: trlc error: unknown symbol Foo

tests-system/rbt-cannot-declare-in-check-file/output.json

@@ -0,0 +1,3 @@
+package Foo
+        ^^^ rbt-cannot-declare-in-check-file/foo.check:1: error: unknown symbol Foo
+Processed 0 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/rbt-cannot-declare-in-check-file/output.smtlib

@@ -0,0 +1,3 @@
+package Foo
+        ^^^ rbt-cannot-declare-in-check-file/foo.check:1: error: unknown symbol Foo
+Processed 0 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/rbt-import-in-check/bar.rsl

@@ -0,0 +1 @@
+package Bar

tests-system/rbt-import-in-check/foo.check

@@ -0,0 +1,3 @@
+package Foo
+
+import Bar

tests-system/rbt-import-in-check/foo.rsl

@@ -0,0 +1 @@
+package Foo

tests-system/rbt-import-in-check/output

@@ -0,0 +1,3 @@
+import Bar
+^^^^^^ rbt-import-in-check/foo.check:3: error: expected keyword checks, encountered keyword import instead
+Processed 2 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/rbt-import-in-check/output.brief

@@ -0,0 +1 @@
+rbt-import-in-check/foo.check:3:1: trlc error: expected keyword checks, encountered keyword import instead

tests-system/rbt-import-in-check/output.json

@@ -0,0 +1,3 @@
+import Bar
+^^^^^^ rbt-import-in-check/foo.check:3: error: expected keyword checks, encountered keyword import instead
+Processed 2 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/rbt-import-in-check/output.smtlib

@@ -0,0 +1,3 @@
+import Bar
+^^^^^^ rbt-import-in-check/foo.check:3: error: expected keyword checks, encountered keyword import instead
+Processed 2 model(s), 1 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/simple/tracing

@@ -2,3 +2,5 @@ LRM.Layout
 LRM.File_Parsing_Order
 LRM.Preamble
 LRM.RSL_File
+LRM.Check_File
+LRM.Deprecated_Check_Files

trlc/parser.py

@@ -1583,6 +1583,7 @@ def parse_preamble(self, kind):
         assert kind in ("rsl", "check", "trlc")
         # lobster-trace: LRM.Layout
         # lobster-trace: LRM.Preamble
+        # lobster-trace: LRM.Cannot_Declare_In_Check_File
 
         # First, parse package indication, declaring the package if
         # needed
@@ -1665,6 +1666,7 @@ def parse_rsl_file(self):
         return ok
 
     def parse_check_file(self):
+        # lobster-trace: LRM.Check_File
         self.parse_preamble("check")
         self.cu.resolve_imports(self.mh, self.stab)
 
@@ -1674,6 +1676,7 @@ def parse_check_file(self):
             try:
                 n_block = self.parse_check_block()
                 self.cu.add_item(n_block)
+                # lobster-trace: LRM.Deprecated_Check_Files
                 if self.lint_mode:
                     self.mh.check(
                         n_block.location,
@@ -1689,6 +1692,7 @@ def parse_check_file(self):
                 # Recovery strategy is to look for the next check
                 # block
                 self.skip_until_newline()
+                # lobster-trace: LRM.Import_In_Check
                 while not self.peek_eof() and not self.peek_kw("checks"):
                     self.advance()
                     self.skip_until_newline()

trlc/trlc.py

@@ -350,6 +350,7 @@ def parse_rsl_files(self):
 
     def parse_check_files(self):
         # lobster-trace: LRM.Preamble
+        # lobster-trace: LRM.Check_File
 
         ok = True
         for name in sorted(self.check_files):