0
# Utility Functions
1

2
String conversion, character operations, quantification, and generator functions that provide essential utilities for Dafny runtime operations. These functions handle Dafny-specific string representations, Unicode operations, mathematical operations, and collection generation.
3

4
## Capabilities
5

6
### String Conversion and Representation
7

8
Functions for converting values to Dafny-specific string representations and handling UTF-16 encoding.
9

10
```python { .api }
11
def string_of(value) -> str:
12
    """
13
    Converts any value to its Dafny string representation.
14
    
15
    Parameters:
16
    - value: Any - The value to convert
17
    
18
    Returns:
19
    str: Dafny-specific string representation
20
    
21
    Behavior:
22
    - Objects with __dafnystr__(): Uses their method
23
    - None: Returns "null"
24
    - bool: Returns "true" or "false"  
25
    - str (char values): Converts via UTF-16
26
    - tuple: Returns (elem1, elem2, ...)
27
    - FunctionType: Returns "Function"
28
    - Other types: Uses str()
29
    """
30

31
def string_from_utf_16(utf_16_code_units):
32
    """
33
    Converts UTF-16 code units to a Python string.
34
    
35
    Parameters:
36
    - utf_16_code_units: Iterable of UTF-16 code units (characters)
37
    
38
    Returns:
39
    str: Decoded string with error handling for invalid sequences
40
    
41
    Note: Dafny strings are sequences of UTF-16 code units.
42
    Invalid sequences are replaced with replacement characters.
43
    """
44

45
def print(value):
46
    """
47
    Prints a value without trailing newline (overrides built-in print).
48
    
49
    Parameters:
50
    - value: Any - Value to print
51
    
52
    Returns:
53
    None
54
    
55
    Note: This replaces Python's built-in print to match Dafny's output behavior.
56
    """
57
```
58

59
#### Usage Examples
60

61
```python
62
from _dafny import string_of, string_from_utf_16, print, Seq, Set
63

64
# String conversion for various types
65
print(string_of(True))           # "true"
66
print(string_of(False))          # "false"
67
print(string_of(None))           # "null"
68
print(string_of((1, 2, 3)))      # "(1, 2, 3)"
69
print(string_of(lambda x: x))    # "Function"
70

71
# Dafny data structures have __dafnystr__ methods
72
seq = Seq([1, 2, 3])
73
set_val = Set([1, 2, 3])
74
print(string_of(seq))            # "[1, 2, 3]"
75
print(string_of(set_val))        # "{1, 2, 3}"
76

77
# UTF-16 string conversion
78
utf16_chars = ['H', 'e', 'l', 'l', 'o']
79
decoded = string_from_utf_16(utf16_chars)
80
print(decoded)                   # "Hello"
81

82
# Dafny-style printing (no trailing newline)
83
print("Hello")
84
print(" World")                  # Outputs: "Hello World"
85
```
86

87
### Unicode Character Operations
88

89
Functions for working with Unicode characters and code points, including character validation and generation.
90

91
```python { .api }
92
class CodePoint(str):
93
    """
94
    Unicode code point with Dafny-specific behavior.
95
    """
96
    escapes: dict = {
97
        '\n': "\\n", '\r': "\\r", '\t': "\\t", '\0': "\\0",
98
        '\'': "\\'", '\"': "\\\"", '\\': "\\\\"
99
    }
100

101
    def __escaped__(self):
102
        """Returns escaped version of character for display."""
103

104
    def __dafnystr__(self):
105
        """Returns Dafny string representation with single quotes."""
106

107
    def __add__(self, other):
108
        """Adds code points using plus_char."""
109

110
    def __sub__(self, other):
111
        """Subtracts code points using minus_char."""
112

113
    @staticmethod
114
    def is_code_point(i):
115
        """
116
        Tests if integer i is a valid Unicode code point.
117
        
118
        Parameters:
119
        - i: int - Integer to test
120
        
121
        Returns:
122
        bool: True if valid Unicode code point
123
        """
124
```
125

126
#### Usage Examples
127

128
```python
129
from _dafny import CodePoint
130

131
# Create code points
132
cp_a = CodePoint('A')
133
cp_newline = CodePoint('\n')
134

135
# String representations
136
print(cp_a.__dafnystr__())           # "'A'"
137
print(cp_newline.__dafnystr__())     # "'\n'" (escaped)
138

139
# Code point arithmetic
140
cp_b = cp_a + CodePoint('\x01')      # 'B' (A + 1)
141
cp_z = CodePoint('Z') - CodePoint('\x01')  # 'Y' (Z - 1)
142

143
# Validation
144
print(CodePoint.is_code_point(65))   # True (valid code point)
145
print(CodePoint.is_code_point(0x110000))  # False (beyond Unicode range)
146
```
147

148
### Quantification and Logic
149

150
Functions for implementing universal and existential quantification over collections.
151

152
```python { .api }
153
def quantifier(vals, frall, pred):
154
    """
155
    Implements universal and existential quantification.
156
    
157
    Parameters:
158
    - vals: Iterable - Values to quantify over
159
    - frall: bool - True for universal (∀), False for existential (∃)
160
    - pred: Function - Predicate function to test each value
161
    
162
    Returns:
163
    bool: Result of quantification
164
    
165
    Behavior:
166
    - Universal (frall=True): Returns True if pred(x) is True for all x in vals
167
    - Existential (frall=False): Returns True if pred(x) is True for any x in vals
168
    """
169
```
170

171
#### Usage Examples
172

173
```python
174
from _dafny import quantifier
175

176
# Universal quantification: all numbers are positive
177
numbers = [1, 2, 3, 4, 5]
178
all_positive = quantifier(numbers, True, lambda x: x > 0)
179
print(all_positive)  # True
180

181
# Existential quantification: some number is even
182
some_even = quantifier(numbers, False, lambda x: x % 2 == 0)
183
print(some_even)     # True
184

185
# Universal quantification that fails
186
all_even = quantifier(numbers, True, lambda x: x % 2 == 0)
187
print(all_even)      # False (not all numbers are even)
188

189
# Empty collection quantification
190
print(quantifier([], True, lambda x: False))   # True (vacuously true)
191
print(quantifier([], False, lambda x: True))   # False (no elements)
192
```
193

194
### Generator Functions
195

196
Functions that generate infinite or large collections for use in Dafny specifications and proofs.
197

198
```python { .api }
199
def AllBooleans():
200
    """
201
    Returns all boolean values.
202
    
203
    Returns:
204
    List[bool]: [False, True]
205
    """
206

207
def AllChars():
208
    """
209
    Returns generator yielding all UTF-16 characters.
210
    
211
    Returns:
212
    Generator[str]: Characters from \u0000 to \uFFFF
213
    """
214

215
def AllUnicodeChars():
216
    """
217
    Returns generator yielding all valid Unicode code points.
218
    
219
    Returns:
220
    Generator[CodePoint]: All valid Unicode code points as CodePoint objects
221
    """
222

223
def AllIntegers():
224
    """
225
    Returns generator yielding all integers in alternating order.
226
    
227
    Returns:
228
    Generator[int]: 0, -1, 1, -2, 2, -3, 3, ...
229
    """
230

231
def IntegerRange(lo, hi):
232
    """
233
    Returns range of integers with optional unbounded ends.
234
    
235
    Parameters:
236
    - lo: int or None - Lower bound (inclusive), None for unbounded below
237
    - hi: int or None - Upper bound (exclusive), None for unbounded above
238
    
239
    Returns:
240
    Generator[int] or range: Integer sequence within bounds
241
    """
242
```
243

244
#### Usage Examples
245

246
```python
247
from _dafny import AllBooleans, AllChars, AllUnicodeChars, AllIntegers, IntegerRange
248

249
# All boolean values
250
bools = AllBooleans()
251
print(bools)  # [False, True]
252

253
# First few UTF-16 characters  
254
chars_gen = AllChars()
255
first_chars = [next(chars_gen) for _ in range(5)]
256
print([ord(c) for c in first_chars])  # [0, 1, 2, 3, 4]
257

258
# First few Unicode code points
259
unicode_gen = AllUnicodeChars()
260
first_unicode = [next(unicode_gen) for _ in range(5)]
261
print([ord(c) for c in first_unicode])  # [0, 1, 2, 3, 4]
262

263
# All integers (alternating positive/negative)
264
int_gen = AllIntegers()
265
first_ints = [next(int_gen) for _ in range(10)]
266
print(first_ints)  # [0, -1, 1, -2, 2, -3, 3, -4, 4, -5]
267

268
# Integer ranges
269
finite_range = list(IntegerRange(3, 8))    # [3, 4, 5, 6, 7]
270
print(finite_range)
271

272
# Unbounded ranges (use carefully - infinite!)
273
up_from_10 = IntegerRange(10, None)        # 10, 11, 12, ...
274
down_to_5 = IntegerRange(None, 5)          # 4, 3, 2, 1, 0, -1, ...
275

276
# Take first few from unbounded range
277
first_up = [next(iter(up_from_10)) for _ in range(5)]
278
print(first_up)  # [10, 11, 12, 13, 14]
279
```
280

281
### Specialized Iterators
282

283
Additional iterator classes for specific mathematical sequences.
284

285
```python { .api }
286
class Doubler:
287
    """Iterator that yields powers of 2 starting from a given value."""
288
    
289
    def __init__(self, start):
290
        """
291
        Initialize with starting value.
292
        
293
        Parameters:
294
        - start: int - Starting value for geometric sequence
295
        """
296

297
    def __iter__(self):
298
        """
299
        Returns iterator yielding start, start*2, start*4, ...
300
        
301
        Returns:
302
        Iterator[int]: Geometric sequence with ratio 2
303
        """
304
```
305

306
#### Usage Examples
307

308
```python
309
from _dafny import Doubler
310

311
# Powers of 2 starting from 1
312
powers_of_2 = Doubler(1)
313
first_powers = [next(iter(powers_of_2)) for _ in range(8)]
314
print(first_powers)  # [1, 2, 4, 8, 16, 32, 64, 128]
315

316
# Powers of 2 starting from 3
317
powers_from_3 = Doubler(3)
318
first_from_3 = [next(iter(powers_from_3)) for _ in range(5)]
319
print(first_from_3)  # [3, 6, 12, 24, 48]
320

321
# Use in loops
322
for i, power in enumerate(Doubler(5)):
323
    if i >= 4:  # Stop after 4 iterations
324
        break
325
    print(f"2^{i} * 5 = {power}")
326
# Output:
327
# 2^0 * 5 = 5
328
# 2^1 * 5 = 10  
329
# 2^2 * 5 = 20
330
# 2^3 * 5 = 40
331
```
332

333
### Class Utilities
334

335
Utility classes that support Python class functionality within the Dafny runtime.
336

337
```python { .api }
338
class classproperty(property):
339
    """
340
    Descriptor that enables class-level properties (like @classmethod but for properties).
341
    
342
    Enables accessing properties on the class itself rather than instances.
343
    Used internally by the Dafny runtime for class-level constants and computed values.
344
    """
345
    
346
    def __get__(self, instance, owner):
347
        """
348
        Descriptor protocol implementation for class property access.
349
        
350
        Parameters:
351
        - instance: Instance accessing the property (ignored)
352
        - owner: Class accessing the property
353
        
354
        Returns:
355
        Result of calling the property getter on the owner class
356
        """
357
```
358

359
#### Usage Examples
360

361
```python
362
from _dafny import classproperty
363

364
class ExampleClass:
365
    _class_value = 42
366
    
367
    @classproperty
368
    def class_constant(cls):
369
        """Access a class-level constant."""
370
        return cls._class_value * 2
371

372
# Access class property
373
print(ExampleClass.class_constant)  # 84
374

375
# Works on instances too
376
instance = ExampleClass()
377
print(instance.class_constant)      # 84
378
```
379

380
### Default Value Generators
381

382
Functions that provide default values for Dafny types, used in initialization and compilation.
383

384
```python { .api }
385
class defaults:
386
    """Default value generators for various Dafny types."""
387
    
388
    @staticmethod
389
    def bool():
390
        """Returns default boolean value: False"""
391
    
392
    @staticmethod  
393
    def char():
394
        """Returns default character value: 'D'"""
395
    
396
    @staticmethod
397
    def codepoint():
398
        """Returns default CodePoint: CodePoint('D')"""
399
    
400
    @staticmethod
401
    def int():
402
        """Returns default integer value: 0"""
403
    
404
    @staticmethod
405
    def real():
406
        """Returns default real value: BigRational() (0/1)"""
407
    
408
    @staticmethod
409
    def pointer():
410
        """Returns default pointer value: None"""
411
    
412
    @staticmethod
413
    def tuple(*args):
414
        """
415
        Returns function that creates tuple with default values.
416
        
417
        Parameters:
418
        - args: Functions that return default values for tuple elements
419
        
420
        Returns:
421
        Function: Function that creates tuple with default values
422
        """
423
```
424

425
#### Usage Examples
426

427
```python
428
from _dafny import defaults, CodePoint, BigRational
429

430
# Basic default values
431
print(defaults.bool())       # False
432
print(defaults.char())       # 'D'
433
print(defaults.int())        # 0
434
print(defaults.pointer())    # None
435

436
# Complex default values
437
print(type(defaults.codepoint()))  # <class '_dafny.CodePoint'>
438
print(type(defaults.real()))       # <class '_dafny.BigRational'>
439

440
# Tuple defaults
441
tuple_factory = defaults.tuple(defaults.int, defaults.bool, defaults.char)
442
default_tuple = tuple_factory()
443
print(default_tuple)        # (0, False, 'D')
444

445
# Custom tuple defaults
446
custom_factory = defaults.tuple(
447
    lambda: 42,
448
    lambda: "hello", 
449
    defaults.real
450
)
451
custom_tuple = custom_factory()
452
print(custom_tuple)         # (42, 'hello', BigRational(0, 1))
453
```