Merge pull request #260 from sepehr541/parsing-numbers-fix

fix parsing numbers with radix other than 10

Author: fhackett

src/pgo/parser/TLAParser.scala

@@ -138,23 +138,23 @@ trait TLAParser extends RegexParsers {
           regex(raw"\\[bB][01]+".r) ^^ { str =>
             (
               TLANumber.IntValue(
-                BigInt(str.stripPrefix("b").stripPrefix("B"), 2),
+                BigInt(str.stripPrefix("\\").stripPrefix("b").stripPrefix("B"), 2),
               ),
               TLANumber.BinarySyntax,
             )
           } |
           regex(raw"\\[oO][0-7]+".r) ^^ { str =>
             (
               TLANumber.IntValue(
-                BigInt(str.stripPrefix("o").stripPrefix("O"), 8),
+                BigInt(str.stripPrefix("\\").stripPrefix("o").stripPrefix("O"), 8),
               ),
               TLANumber.OctalSyntax,
             )
           } |
           regex(raw"\\[hH][0-9a-fA-F]+".r) ^^ { str =>
             (
               TLANumber.IntValue(
-                BigInt(str.stripPrefix("h").stripPrefix("H"), 16),
+                BigInt(str.stripPrefix("\\").stripPrefix("h").stripPrefix("H"), 16),
               ),
               TLANumber.HexadecimalSyntax,
             )

src/pgo/trans/TLARenderPass.scala

@@ -9,6 +9,12 @@ import pgo.model.pcal.*
 import pgo.model.tla.*
 import pgo.model.Definition
 import scala.annotation.tailrec
+import pgo.model.tla.TLANumber.{
+  DecimalSyntax,
+  BinarySyntax,
+  OctalSyntax,
+  HexadecimalSyntax,
+}
 
 object TLARenderPass:
   def describeQuantifierBound(qb: TLAQuantifierBound): Description =
@@ -53,11 +59,17 @@ object TLARenderPass:
           }""""
       case TLANumber(
             value,
-            _, /* force decimal representation, should be correct in most cases */
+            rep,
           ) =>
+        val (prefix, radix) = rep match
+          case DecimalSyntax     => ("", 10)
+          case BinarySyntax      => ("\\b", 2)
+          case OctalSyntax       => ("\\o", 8)
+          case HexadecimalSyntax => ("\\h", 16)
+
         value match {
           case TLANumber.IntValue(value) =>
-            value.toString().toDescription
+            s"$prefix${value.toString(radix)}".toDescription
           case TLANumber.DecimalValue(value) =>
             value.toString().toDescription
         }

test/files/tla/Numbers.tla

@@ -0,0 +1,15 @@
+---- MODULE Integers ----
+EXTENDS Naturals, Reals
+
+Int == 1
+Hex == \h1
+Bin == \b1
+Oct == \o1
+
+\* TODO: fix decimal
+\* go.parser.DefinitionLookupError: 
+\* identifier . does not refer to a known definition at /workspaces/pgo/test/files/tla/Numbers.tla:13.13-14
+
+\* Decimal == 1.1
+
+====

test/pgo/TLAUnitCoverageTests.scala

@@ -2,6 +2,15 @@ package pgo
 
 import pgo.model.SourceLocation.UnderlyingFile
 import pgo.parser.TLAParser
+import pgo.model.DefinitionOne
+import pgo.model.DefinitionComposite
+import pgo.model.tla.TLAOperatorDefinition
+import pgo.model.tla.TLANumber
+import pgo.model.tla.TLANumber.DecimalSyntax
+import pgo.model.tla.TLANumber.HexadecimalSyntax
+import pgo.model.tla.TLANumber.BinarySyntax
+import pgo.model.tla.TLANumber.OctalSyntax
+import pgo.model.tla.TLANumber.IntValue
 
 final class TLAUnitCoverageTests extends munit.FunSuite:
   def checkNames(tlaFile: os.Path, names: List[String])(using
@@ -32,3 +41,26 @@ final class TLAUnitCoverageTests extends munit.FunSuite:
       "Init",
     ),
   )
+
+  test("parsing numbers"):
+    val tlaFile = projectRoot / "test" / "files" / "tla" / "Numbers.tla"
+    val fileContents = os.read(tlaFile)
+    val underlyingFile = UnderlyingFile(tlaFile)
+    val module = TLAParser.readModule(underlyingFile, fileContents)
+
+    val values = module.units.view
+        .collect {
+          case op: TLAOperatorDefinition => op
+        }.map {
+          case TLAOperatorDefinition(name, args, body, isLocal) => body
+        }.collect {
+          case num: TLANumber => num 
+        }.toList
+    
+    val expected = List(
+        TLANumber(IntValue(1), DecimalSyntax),
+        TLANumber(IntValue(1), HexadecimalSyntax),
+        TLANumber(IntValue(1), BinarySyntax),
+        TLANumber(IntValue(1), OctalSyntax)
+    )
+    assertEquals(values, expected)