Utility Functions

def string_of(value) -> str:
    """
    Converts any value to its Dafny string representation.
    
    Parameters:
    - value: Any - The value to convert
    
    Returns:
    str: Dafny-specific string representation
    
    Behavior:
    - Objects with __dafnystr__(): Uses their method
    - None: Returns "null"
    - bool: Returns "true" or "false"  
    - str (char values): Converts via UTF-16
    - tuple: Returns (elem1, elem2, ...)
    - FunctionType: Returns "Function"
    - Other types: Uses str()
    """

def string_from_utf_16(utf_16_code_units):
    """
    Converts UTF-16 code units to a Python string.
    
    Parameters:
    - utf_16_code_units: Iterable of UTF-16 code units (characters)
    
    Returns:
    str: Decoded string with error handling for invalid sequences
    
    Note: Dafny strings are sequences of UTF-16 code units.
    Invalid sequences are replaced with replacement characters.
    """

def print(value):
    """
    Prints a value without trailing newline (overrides built-in print).
    
    Parameters:
    - value: Any - Value to print
    
    Returns:
    None
    
    Note: This replaces Python's built-in print to match Dafny's output behavior.
    """

from _dafny import string_of, string_from_utf_16, print, Seq, Set

# String conversion for various types
print(string_of(True))           # "true"
print(string_of(False))          # "false"
print(string_of(None))           # "null"
print(string_of((1, 2, 3)))      # "(1, 2, 3)"
print(string_of(lambda x: x))    # "Function"

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

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

# Dafny-style printing (no trailing newline)
print("Hello")
print(" World")                  # Outputs: "Hello World"

class CodePoint(str):
    """
    Unicode code point with Dafny-specific behavior.
    """
    escapes: dict = {
        '\n': "\\n", '\r': "\\r", '\t': "\\t", '\0': "\\0",
        '\'': "\\'", '\"': "\\\"", '\\': "\\\\"
    }

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

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

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

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

    @staticmethod
    def is_code_point(i):
        """
        Tests if integer i is a valid Unicode code point.
        
        Parameters:
        - i: int - Integer to test
        
        Returns:
        bool: True if valid Unicode code point
        """

from _dafny import CodePoint

# Create code points
cp_a = CodePoint('A')
cp_newline = CodePoint('\n')

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

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

# Validation
print(CodePoint.is_code_point(65))   # True (valid code point)
print(CodePoint.is_code_point(0x110000))  # False (beyond Unicode range)

def quantifier(vals, frall, pred):
    """
    Implements universal and existential quantification.
    
    Parameters:
    - vals: Iterable - Values to quantify over
    - frall: bool - True for universal (∀), False for existential (∃)
    - pred: Function - Predicate function to test each value
    
    Returns:
    bool: Result of quantification
    
    Behavior:
    - Universal (frall=True): Returns True if pred(x) is True for all x in vals
    - Existential (frall=False): Returns True if pred(x) is True for any x in vals
    """

from _dafny import quantifier

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

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

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

# Empty collection quantification
print(quantifier([], True, lambda x: False))   # True (vacuously true)
print(quantifier([], False, lambda x: True))   # False (no elements)

def AllBooleans():
    """
    Returns all boolean values.
    
    Returns:
    List[bool]: [False, True]
    """

def AllChars():
    """
    Returns generator yielding all UTF-16 characters.
    
    Returns:
    Generator[str]: Characters from \u0000 to \uFFFF
    """

def AllUnicodeChars():
    """
    Returns generator yielding all valid Unicode code points.
    
    Returns:
    Generator[CodePoint]: All valid Unicode code points as CodePoint objects
    """

def AllIntegers():
    """
    Returns generator yielding all integers in alternating order.
    
    Returns:
    Generator[int]: 0, -1, 1, -2, 2, -3, 3, ...
    """

def IntegerRange(lo, hi):
    """
    Returns range of integers with optional unbounded ends.
    
    Parameters:
    - lo: int or None - Lower bound (inclusive), None for unbounded below
    - hi: int or None - Upper bound (exclusive), None for unbounded above
    
    Returns:
    Generator[int] or range: Integer sequence within bounds
    """

from _dafny import AllBooleans, AllChars, AllUnicodeChars, AllIntegers, IntegerRange

# All boolean values
bools = AllBooleans()
print(bools)  # [False, True]

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

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

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

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

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

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

class Doubler:
    """Iterator that yields powers of 2 starting from a given value."""
    
    def __init__(self, start):
        """
        Initialize with starting value.
        
        Parameters:
        - start: int - Starting value for geometric sequence
        """

    def __iter__(self):
        """
        Returns iterator yielding start, start*2, start*4, ...
        
        Returns:
        Iterator[int]: Geometric sequence with ratio 2
        """

from _dafny import Doubler

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

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

# Use in loops
for i, power in enumerate(Doubler(5)):
    if i >= 4:  # Stop after 4 iterations
        break
    print(f"2^{i} * 5 = {power}")
# Output:
# 2^0 * 5 = 5
# 2^1 * 5 = 10  
# 2^2 * 5 = 20
# 2^3 * 5 = 40

class classproperty(property):
    """
    Descriptor that enables class-level properties (like @classmethod but for properties).
    
    Enables accessing properties on the class itself rather than instances.
    Used internally by the Dafny runtime for class-level constants and computed values.
    """
    
    def __get__(self, instance, owner):
        """
        Descriptor protocol implementation for class property access.
        
        Parameters:
        - instance: Instance accessing the property (ignored)
        - owner: Class accessing the property
        
        Returns:
        Result of calling the property getter on the owner class
        """

from _dafny import classproperty

class ExampleClass:
    _class_value = 42
    
    @classproperty
    def class_constant(cls):
        """Access a class-level constant."""
        return cls._class_value * 2

# Access class property
print(ExampleClass.class_constant)  # 84

# Works on instances too
instance = ExampleClass()
print(instance.class_constant)      # 84

class defaults:
    """Default value generators for various Dafny types."""
    
    @staticmethod
    def bool():
        """Returns default boolean value: False"""
    
    @staticmethod  
    def char():
        """Returns default character value: 'D'"""
    
    @staticmethod
    def codepoint():
        """Returns default CodePoint: CodePoint('D')"""
    
    @staticmethod
    def int():
        """Returns default integer value: 0"""
    
    @staticmethod
    def real():
        """Returns default real value: BigRational() (0/1)"""
    
    @staticmethod
    def pointer():
        """Returns default pointer value: None"""
    
    @staticmethod
    def tuple(*args):
        """
        Returns function that creates tuple with default values.
        
        Parameters:
        - args: Functions that return default values for tuple elements
        
        Returns:
        Function: Function that creates tuple with default values
        """

from _dafny import defaults, CodePoint, BigRational

# Basic default values
print(defaults.bool())       # False
print(defaults.char())       # 'D'
print(defaults.int())        # 0
print(defaults.pointer())    # None

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

# Tuple defaults
tuple_factory = defaults.tuple(defaults.int, defaults.bool, defaults.char)
default_tuple = tuple_factory()
print(default_tuple)        # (0, False, 'D')

# Custom tuple defaults
custom_factory = defaults.tuple(
    lambda: 42,
    lambda: "hello", 
    defaults.real
)
custom_tuple = custom_factory()
print(custom_tuple)         # (42, 'hello', BigRational(0, 1))