floats iter 1.1: Literal::Float variant + canonical hex serde + drift-test anchors

This commit is contained in:
2026-05-10 14:36:08 +02:00
parent cdc9d64169
commit ec2811194b
12 changed files with 83 additions and 2 deletions
+44 -1
View File
@@ -533,10 +533,42 @@ pub enum Pattern {
},
}
/// Private serde helper: emits a `u64` as a 16-character lowercase
/// hex JSON string and parses the same shape back. The
/// 16-character invariant covers the full `u64` range zero-padded
/// (`format!("{:016x}", 0u64) == "0000000000000000"`,
/// `format!("{:016x}", u64::MAX) == "ffffffffffffffff"`). Used by
/// [`Literal::Float`] so float bit patterns flow through the
/// canonical-JSON *string* path — guaranteeing bit stability across
/// `serde_json` versions and surfacing NaN / ±Inf, which JSON
/// numbers cannot represent.
mod hex_u64 {
use serde::{de::Error as DeError, Deserialize, Deserializer, Serializer};
pub fn serialize<S: Serializer>(value: &u64, s: S) -> Result<S::Ok, S::Error> {
s.serialize_str(&format!("{:016x}", value))
}
pub fn deserialize<'de, D: Deserializer<'de>>(d: D) -> Result<u64, D::Error> {
let s = <&str>::deserialize(d)?;
if s.len() != 16 {
return Err(D::Error::custom(format!(
"Float bits: expected 16 hex chars, got {}",
s.len()
)));
}
u64::from_str_radix(s, 16).map_err(D::Error::custom)
}
}
/// A literal value.
///
/// The JSON discriminator is the `kind` field. `Unit` carries no
/// payload and serializes as `{"kind":"unit"}`.
/// payload and serializes as `{"kind":"unit"}`. `Float` carries a
/// `u64` IEEE-754 binary64 bit pattern, serialized via the
/// [`hex_u64`] helper as a 16-character lowercase hex string —
/// canonical-JSON bytes therefore stay bit-stable for hashing and
/// can represent NaN / ±Inf (which JSON numbers cannot).
#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(tag = "kind", rename_all = "lowercase")]
pub enum Literal {
@@ -548,6 +580,12 @@ pub enum Literal {
Str { value: String },
/// The unit value `()`.
Unit,
/// IEEE-754 binary64 (LLVM `double`) carried as its bit pattern.
/// See [`hex_u64`] for the serialization rationale.
Float {
#[serde(with = "hex_u64")]
bits: u64,
},
}
/// A type expression.
@@ -632,6 +670,11 @@ impl Type {
pub fn str_() -> Type {
Type::Con { name: "Str".into(), args: vec![] }
}
/// Convenience constructor for `Float` (no args). IEEE-754
/// binary64. Parallel to [`Type::int`] / [`Type::bool_`].
pub fn float() -> Type {
Type::Con { name: "Float".into(), args: vec![] }
}
/// Iter 18a: build a `Type::Fn` with all parameter modes set to
/// `ParamMode::Implicit` and `ret_mode` set to `Implicit`. This is
+20
View File
@@ -132,4 +132,24 @@ mod tests {
assert!(!s.contains(' '));
assert!(!s.contains('\n'));
}
/// Iter 22-floats.1 RED: a `Literal::Float` carries the IEEE-754
/// binary64 bit pattern as a `u64`; canonical JSON encodes it as
/// `{"bits":"<16-lowercase-hex>","kind":"float"}` — string path,
/// NOT through `serde_json::Number` (which is not bit-stable for
/// floats and cannot represent NaN / ±Inf at all).
///
/// Pinned literal: `1.5_f64` → bit pattern `0x3FF8000000000000` →
/// hex string `"3ff8000000000000"`. Sorted-key order is
/// `bits` < `kind` lexicographically.
#[test]
fn float_literal_canonical_bytes() {
use crate::ast::Literal;
let lit = Literal::Float {
bits: 0x3ff8_0000_0000_0000u64,
};
let bytes = to_bytes(&lit);
let s = std::str::from_utf8(&bytes).unwrap();
assert_eq!(s, r#"{"bits":"3ff8000000000000","kind":"float"}"#);
}
}
+4 -1
View File
@@ -1058,7 +1058,10 @@ fn build_eq(scrutinee: Term, lit: &Literal) -> Term {
Literal::Unit => Term::Lit {
lit: Literal::Bool { value: true },
},
Literal::Int { .. } | Literal::Bool { .. } | Literal::Str { .. } => Term::App {
Literal::Int { .. }
| Literal::Bool { .. }
| Literal::Str { .. }
| Literal::Float { .. } => Term::App {
callee: Box::new(Term::Var {
name: "==".to_string(),
}),
+1
View File
@@ -116,6 +116,7 @@ fn lit_to_string(l: &Literal) -> String {
serde_json::to_string(value).unwrap()
}
Literal::Unit => "()".to_string(),
Literal::Float { bits } => format!("(float-bits 0x{:016x})", bits),
}
}