From 5826a8eca62c5d4966d9db270d1d6f754e73028c Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 25 Sep 2024 10:18:24 -0400
Subject: [PATCH] format_type can now format range_typet

This adds formatting for range_typet as { from, ..., to }.
---
 src/util/format_type.cpp  |  6 ++++++
 unit/Makefile             |  1 +
 unit/util/format_type.cpp | 19 +++++++++++++++++++
 3 files changed, 26 insertions(+)
 create mode 100644 unit/util/format_type.cpp

diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp
index 11560c150ad..f2b495521c5 100644
--- a/src/util/format_type.cpp
+++ b/src/util/format_type.cpp
@@ -98,6 +98,12 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
     return os << "\xe2\x84\xa4"; // u+2124, 'Z'
   else if(id == ID_natural)
     return os << "\xe2\x84\x95"; // u+2115, 'N'
+  else if(id == ID_range)
+  {
+    auto &range_type = to_range_type(type);
+    return os << "{ " << range_type.get_from() << ", ..., "
+              << range_type.get_to() << " }";
+  }
   else if(id == ID_rational)
     return os << "\xe2\x84\x9a"; // u+211A, 'Q'
   else if(id == ID_mathematical_function)
diff --git a/unit/Makefile b/unit/Makefile
index 285bd40e043..b42983234a1 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -144,6 +144,7 @@ SRC += analyses/ai/ai.cpp \
        util/format.cpp \
        util/format_expr.cpp \
        util/format_number_range.cpp \
+       util/format_type.cpp \
        util/get_base_name.cpp \
        util/graph.cpp \
        util/help_formatter.cpp \
diff --git a/unit/util/format_type.cpp b/unit/util/format_type.cpp
new file mode 100644
index 00000000000..1ba74d76f59
--- /dev/null
+++ b/unit/util/format_type.cpp
@@ -0,0 +1,19 @@
+/*******************************************************************\
+
+ Module: Unit tests for `format` function on types
+
+ Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include <util/format.h>
+#include <util/format_type.h>
+#include <util/std_expr.h>
+
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("Format a range type", "[core][util][format_type]")
+{
+  auto type = range_typet(1, 10);
+  REQUIRE(format_to_string(type) == "{ 1, ..., 10 }");
+}