feat: Use (wrapped) native strings instead of sequences of characters…

… in Python

Source/Dafny/Compilers/Compiler-python.cs

@@ -620,7 +620,7 @@ protected class ClassWriter : IClassWriter {
  var wStmts = wr.Fork();
  wr.Write($"raise {DafnyRuntimeModule}.HaltException(");
  if (tok != null) {
- wr.Write($"{DafnyRuntimeModule}.Seq(\"{Dafny.ErrorReporter.TokenToString(tok)}: \") + ");
+ wr.Write($"{DafnySeqClass}(\"{Dafny.ErrorReporter.TokenToString(tok)}: \") + ");
  }
 
  TrExpr(messageExpr, wr, false, wStmts);
@@ -716,7 +716,7 @@ protected class ClassWriter : IClassWriter {
  wr.Write($"'{(string)e.Value}'");
  break;
  case StringLiteralExpr str:
- wr.Write($"{DafnyRuntimeModule}.Seq(");
+ wr.Write($"{DafnySeqClass}(");
  TrStringLiteral(str, wr);
  wr.Write(")");
  break;
@@ -1257,6 +1257,9 @@ protected class ClassWriter : IClassWriter {
  wr.Write(open);
  TrExprList(elements, wr, inLetExprBody, wStmts, parens: false);
  wr.Write(close);
+ if (ct is SeqType && ct.TypeArgs.TrueForAll(ty => ty.IsCharType)) {
+ wr.Write(", isStr = True");
+ }
  wr.Write(")");
  }
 

Source/DafnyRuntime/DafnyRuntime.py

@@ -39,12 +39,26 @@ def _break(name):
 def _tail_call():
  raise TailCall()
 
+class String(str):
+ def __new__(cls, *args, **kw):
+ return super().__new__(cls, *args, **kw)
+
+ def __repr__(self):
+ return self
+
+ def __add__(self, other):
+ return String(super().__add__(other))
+
 class Seq(list):
- def __init__(self, __iterable = None, isStr = False):
+ def __new__(cls, __iterable = None, isStr = False):
  if __iterable is None:
  __iterable = []
- self.isStr = isinstance(__iterable, str) or isStr
- super().__init__(__iterable)
+ if isinstance(__iterable, str):
+ return String(__iterable)
+ elif isStr:
+ return String(''.join(__iterable))
+ else:
+ return super().__new__(cls, __iterable)
 
  @property
  def Elements(self):
@@ -54,13 +68,8 @@ def Elements(self):
  def UniqueElements(self):
  return set(self)
 
- def __repr__(self) -> str:
- if self.isStr:
- return ''.join(self)
- return super().__repr__()
-
  def __add__(self, other):
- return Seq(super().__add__(other), isStr=self.isStr and other.isStr)
+ return Seq(super().__add__(other))
 
  def __hash__(self) -> int:
  return hash(tuple(self))

Test/comp/Various.dfy

@@ -29,8 +29,13 @@ method LetExpr() {
  print (var a := A(0); var A(zero) := a; zero), "\n";
 }
 
+method PrintString() {
+ print [[], [] + "Hallo " + ['W', 'e', 'l', 't', '!']], "\n";
+}
+
 method Main() {
  Match((0,1));
  Countdown(1);
  LetExpr();
+ PrintString();
 }

Test/comp/Various.dfy.expect

@@ -6,27 +6,32 @@ match
 1
 Kablammo!!
 0
+[, Hallo Welt!]
 
 Dafny program verifier did not attempt verification
 match
 1
 Kablammo!!
 0
+[, Hallo Welt!]
 
 Dafny program verifier did not attempt verification
 match
 1
 Kablammo!!
 0
+[, Hallo Welt!]
 
 Dafny program verifier did not attempt verification
 match
 1
 Kablammo!!
 0
+[, Hallo Welt!]
 
 Dafny program verifier did not attempt verification
 match
 1
 Kablammo!!
 0
+[, Hallo Welt!]