feat: Add fp64 type support with IEEE 754 semantics

[fabiomadge]

This PR introduces native 64-bit floating-point (fp64) support to Dafny, implementing IEEE 754 double-precision semantics. This enables Dafny programs to work with floating-point arithmetic for numerical computations, scientific computing, and interfacing with external systems that use floating-point numbers.

Key Features

• Native fp64 type: A new built-in type representing IEEE 754 double-precision floating-point numbers
• Literal support: Floating-point literals with type inference (e.g., 1.0, 2.4e12)
• Approximate prefix operator: ~ prefix for literals that cannot be exactly represented (e.g., ~0.1, ~3.14159)
• Special values: Full support for NaN, positive/negative infinity, and signed zeros
• Static members: Classification predicates (IsNaN, IsInfinity, IsFinite, IsNormal, IsZero)
• Arithmetic operations: Standard IEEE 754 arithmetic with proper handling of special values
• Equality semantics: Hybrid approach - == with well-formedness preconditions, fp64.Equal() for IEEE 754 semantics

Implementation Details

• Parser & AST: Extended grammar to support approximate prefix (~) for inexact literals
• Type system: Integrated fp64 as a primitive type
• Resolver: Enhanced type resolution for fp64 expressions
• Verifier: Boogie translation with IEEE 754 semantics
• Code generation: C# backend support with System.Double mapping
• Runtime: Added FromDouble/ToDouble methods to BigRational

Testing

Test suite (10 test files) covering:

• Literal parsing and validation
• Special value handling (NaN, infinities, zeros)
• Classification predicates
• Arithmetic operations and equality semantics
• Type resolution
• Static member access
• Edge cases and error conditions

Documentation

Updated DafnyRef documentation:

• Types.md: Added fp64 section
• Expressions.md: Updated type conversion
• GrammarDetails.md: Added fp64 to reserved words and grammar

Breaking Changes

None - this is a purely additive feature.