System Types

class nat:
    def __init__(self):
        """
        Creates a nat instance.
        
        Note: This constructor creates the type instance, not a value.
        Use nat.default() to get the default natural number value.
        """

    @staticmethod
    def default():
        """
        Returns the default natural number value.
        
        Returns:
        int: 0 (the default natural number)
        """

    @staticmethod
    def _Is(source__):
        """
        Tests if a value is a valid natural number.
        
        Parameters:
        - source__: int - Value to test
        
        Returns:
        bool: True if source__ >= 0 (is non-negative integer)
        """

from System_ import nat

# Get default natural number value
default_nat = nat.default()
print(default_nat)              # 0
print(type(default_nat))        # <class 'int'>

# Validate natural numbers
print(nat._Is(0))               # True (0 is natural)
print(nat._Is(5))               # True (positive integers are natural)
print(nat._Is(42))              # True
print(nat._Is(-1))              # False (negative numbers are not natural)
print(nat._Is(-10))             # False

# Create nat type instance (for type checking)
nat_type = nat()
print(type(nat_type))           # <class 'System_.nat'>

from System_ import nat

def process_natural_number(n):
    """
    Example function that processes natural numbers with validation.
    
    Parameters:
    - n: int - Input number to process
    
    Returns:
    int: Processed result if valid natural number
    
    Raises:
    ValueError: If n is not a natural number
    """
    if not nat._Is(n):
        raise ValueError(f"Expected natural number, got {n}")
    
    # Process the natural number
    return n * 2 + 1

# Valid usage
result1 = process_natural_number(5)
print(result1)  # 11

# Invalid usage
try:
    result2 = process_natural_number(-3)
except ValueError as e:
    print(f"Error: {e}")  # Error: Expected natural number, got -3

from System_ import nat

def validate_array_indices(indices):
    """
    Validates that all array indices are natural numbers.
    
    Parameters:
    - indices: List[int] - List of indices to validate
    
    Returns:
    bool: True if all indices are natural numbers
    """
    return all(nat._Is(index) for index in indices)

def safe_array_access(array, index):
    """
    Safe array access with natural number validation.
    
    Parameters:
    - array: List - Array to access
    - index: int - Index to access
    
    Returns:
    Any: Element at index if valid
    
    Raises:
    ValueError: If index is not a natural number or out of bounds
    """
    if not nat._Is(index):
        raise ValueError(f"Array index must be natural number, got {index}")
    
    if index >= len(array):
        raise ValueError(f"Index {index} out of bounds for array of length {len(array)}")
    
    return array[index]

# Example usage
test_array = ['a', 'b', 'c', 'd', 'e']
indices_to_test = [0, 2, 4, -1, 10]

print("Index validation:")
for idx in indices_to_test:
    if nat._Is(idx):
        print(f"  {idx}: Valid natural number")
    else:
        print(f"  {idx}: Invalid (not natural number)")

print("\nSafe array access:")
for idx in [0, 2, 4]:  # Valid natural numbers
    try:
        element = safe_array_access(test_array, idx)
        print(f"  array[{idx}] = '{element}'")
    except ValueError as e:
        print(f"  array[{idx}]: Error - {e}")

# Test invalid indices
for idx in [-1, 10]:  # Invalid or out of bounds
    try:
        element = safe_array_access(test_array, idx)
        print(f"  array[{idx}] = '{element}'")
    except ValueError as e:
        print(f"  array[{idx}]: Error - {e}")

from System_ import nat
from _dafny import defaults

def initialize_counters(count):
    """
    Initialize a list of counters with default natural number values.
    
    Parameters:
    - count: int - Number of counters to create
    
    Returns:
    List[int]: List of default natural number values
    """
    if not nat._Is(count):
        raise ValueError("Count must be a natural number")
    
    return [nat.default() for _ in range(count)]

def create_nat_tuple(size):
    """
    Create a tuple of natural numbers with default values.
    
    Parameters:
    - size: int - Size of tuple to create
    
    Returns:
    tuple: Tuple of default natural number values
    """
    if not nat._Is(size):
        raise ValueError("Size must be a natural number")
    
    # Create tuple factory for natural numbers
    nat_tuple_factory = defaults.tuple(*[nat.default for _ in range(size)])
    return nat_tuple_factory()

# Example usage
counters = initialize_counters(5)
print(f"Counters: {counters}")        # [0, 0, 0, 0, 0]

nat_tuple = create_nat_tuple(3)
print(f"Nat tuple: {nat_tuple}")      # (0, 0, 0)

# Validate the results
print("All counters are natural numbers:", 
      all(nat._Is(c) for c in counters))  # True

print("All tuple elements are natural numbers:",
      all(nat._Is(elem) for elem in nat_tuple))  # True

from System_ import nat
from typing import List, Union

def dafny_range(start: int, end: int) -> List[int]:
    """
    Creates a range of natural numbers with Dafny validation.
    
    Parameters:
    - start: int - Starting natural number (inclusive)
    - end: int - Ending natural number (exclusive)
    
    Returns:
    List[int]: List of natural numbers in range
    
    Raises:
    ValueError: If start or end are not natural numbers
    """
    if not nat._Is(start):
        raise ValueError(f"Start must be natural number, got {start}")
    if not nat._Is(end):
        raise ValueError(f"End must be natural number, got {end}")
    
    return list(range(start, end))

def sum_naturals(numbers: List[int]) -> int:
    """
    Sums a list of natural numbers.
    
    Parameters:
    - numbers: List[int] - List of natural numbers to sum
    
    Returns:
    int: Sum of natural numbers
    
    Raises:
    ValueError: If any number is not natural
    """
    for i, num in enumerate(numbers):
        if not nat._Is(num):
            raise ValueError(f"Element at index {i} is not natural: {num}")
    
    return sum(numbers)

# Example usage with validation
try:
    range_vals = dafny_range(2, 8)
    print(f"Range: {range_vals}")     # [2, 3, 4, 5, 6, 7]
    
    total = sum_naturals(range_vals)
    print(f"Sum: {total}")            # 27
    
    # This will raise an error
    invalid_range = dafny_range(-1, 5)
except ValueError as e:
    print(f"Validation error: {e}")

import System_
import _dafny

# System module types work with Dafny utilities
from System_ import nat
from _dafny import string_of, defaults

# Natural number with string conversion
n = nat.default()
print(string_of(n))                 # "0"

# Integration with default value system
nat_default = nat.default()
general_int_default = defaults.int()
print(nat_default == general_int_default)  # True (both are 0)

# Type validation in collections
natural_numbers = [nat.default(), 1, 2, 3, 4]
all_valid = all(nat._Is(x) for x in natural_numbers)
print(f"All are natural numbers: {all_valid}")  # True