floats iter 3.2: install neg/int_to_float/float_to_int_truncate/float_to_str/is_nan
This commit is contained in:
@@ -149,6 +149,68 @@ pub fn install(env: &mut crate::Env) {
|
||||
},
|
||||
);
|
||||
|
||||
// Iter 22-floats.3: Float-conversion and inspection builtins.
|
||||
// Codegen lowering lands in iter 4; iter 3 only registers types.
|
||||
// `neg` is polymorphic (`forall a. (a) -> a`) for the same reason
|
||||
// the widened `+` is — Int and Float negation share one symbol;
|
||||
// the spec section A3 also notes that `(- 0.0 x)` desugar is
|
||||
// wrong for `-0.0` (returns `+0.0` per IEEE rounding), so Float
|
||||
// negation needs its own builtin name.
|
||||
env.globals.insert(
|
||||
"neg".into(),
|
||||
Type::Forall {
|
||||
vars: vec!["a".into()],
|
||||
constraints: vec![],
|
||||
body: Box::new(Type::Fn {
|
||||
params: vec![Type::Var { name: "a".into() }],
|
||||
ret: Box::new(Type::Var { name: "a".into() }),
|
||||
effects: vec![],
|
||||
param_modes: vec![],
|
||||
ret_mode: ailang_core::ast::ParamMode::Implicit,
|
||||
}),
|
||||
},
|
||||
);
|
||||
env.globals.insert(
|
||||
"int_to_float".into(),
|
||||
Type::Fn {
|
||||
params: vec![Type::int()],
|
||||
ret: Box::new(Type::float()),
|
||||
effects: vec![],
|
||||
param_modes: vec![],
|
||||
ret_mode: ailang_core::ast::ParamMode::Implicit,
|
||||
},
|
||||
);
|
||||
env.globals.insert(
|
||||
"float_to_int_truncate".into(),
|
||||
Type::Fn {
|
||||
params: vec![Type::float()],
|
||||
ret: Box::new(Type::int()),
|
||||
effects: vec![],
|
||||
param_modes: vec![],
|
||||
ret_mode: ailang_core::ast::ParamMode::Implicit,
|
||||
},
|
||||
);
|
||||
env.globals.insert(
|
||||
"float_to_str".into(),
|
||||
Type::Fn {
|
||||
params: vec![Type::float()],
|
||||
ret: Box::new(Type::str_()),
|
||||
effects: vec![],
|
||||
param_modes: vec![],
|
||||
ret_mode: ailang_core::ast::ParamMode::Implicit,
|
||||
},
|
||||
);
|
||||
env.globals.insert(
|
||||
"is_nan".into(),
|
||||
Type::Fn {
|
||||
params: vec![Type::float()],
|
||||
ret: Box::new(Type::bool_()),
|
||||
effects: vec![],
|
||||
param_modes: vec![],
|
||||
ret_mode: ailang_core::ast::ParamMode::Implicit,
|
||||
},
|
||||
);
|
||||
|
||||
env.effect_ops.insert(
|
||||
"io/print_int".into(),
|
||||
EffectOpSig {
|
||||
@@ -207,6 +269,11 @@ pub fn list() -> Vec<(&'static str, &'static str)> {
|
||||
(">=", "forall a. (a, a) -> Bool"),
|
||||
("not", "(Bool) -> Bool"),
|
||||
("__unreachable__", "forall a. a"),
|
||||
("neg", "forall a. (a) -> a"),
|
||||
("int_to_float", "(Int) -> Float"),
|
||||
("float_to_int_truncate", "(Float) -> Int"),
|
||||
("float_to_str", "(Float) -> Str"),
|
||||
("is_nan", "(Float) -> Bool"),
|
||||
("io/print_int", "(Int) -> Unit !IO [effect op]"),
|
||||
("io/print_bool", "(Bool) -> Unit !IO [effect op]"),
|
||||
("io/print_str", "(Str) -> Unit !IO [effect op]"),
|
||||
@@ -309,4 +376,57 @@ mod tests {
|
||||
let ty = synth_in_builtins_env(&app("<", vec![lit_float(bits_a), lit_float(bits_b)]));
|
||||
assert_eq!(ty, Type::bool_(), "(< 1.5 2.5) must type as Bool");
|
||||
}
|
||||
|
||||
/// Iter 22-floats.3: `neg` is polymorphic — `forall a. (a) -> a`.
|
||||
/// Both `(neg 5) : Int` and `(neg 1.5) : Float` typecheck. The
|
||||
/// polymorphic shape is the same as the widened arithmetic ops, so
|
||||
/// Int and Float negation share one symbol; codegen dispatches on
|
||||
/// the resolved arg type at the call site (iter 4).
|
||||
#[test]
|
||||
fn install_neg_is_polymorphic() {
|
||||
let ty_int = synth_in_builtins_env(&app("neg", vec![lit_int(5)]));
|
||||
assert_eq!(ty_int, Type::int(), "(neg 5) must type as Int");
|
||||
let bits = 1.5_f64.to_bits();
|
||||
let ty_float = synth_in_builtins_env(&app("neg", vec![lit_float(bits)]));
|
||||
assert_eq!(ty_float, Type::float(), "(neg 1.5) must type as Float");
|
||||
}
|
||||
|
||||
/// Iter 22-floats.3: `int_to_float : (Int) -> Float`. The
|
||||
/// monomorphic conversion builtin — codegen lowers via `sitofp` in
|
||||
/// iter 4. Typecheck only validates the signature here.
|
||||
#[test]
|
||||
fn install_int_to_float_signature() {
|
||||
let ty = synth_in_builtins_env(&app("int_to_float", vec![lit_int(5)]));
|
||||
assert_eq!(ty, Type::float(), "(int_to_float 5) must type as Float");
|
||||
}
|
||||
|
||||
/// Iter 22-floats.3: `float_to_int_truncate : (Float) -> Int`.
|
||||
/// Saturating truncation toward zero per spec A4 — typecheck only
|
||||
/// validates the signature; semantics is iter 4's codegen lowering
|
||||
/// via `@llvm.fptosi.sat.i64.f64`.
|
||||
#[test]
|
||||
fn install_float_to_int_truncate_signature() {
|
||||
let bits = 1.5_f64.to_bits();
|
||||
let ty = synth_in_builtins_env(&app("float_to_int_truncate", vec![lit_float(bits)]));
|
||||
assert_eq!(ty, Type::int(), "(float_to_int_truncate 1.5) must type as Int");
|
||||
}
|
||||
|
||||
/// Iter 22-floats.3: `float_to_str : (Float) -> Str`. Codegen lowers
|
||||
/// via runtime C glue in iter 4; typecheck only validates the signature.
|
||||
#[test]
|
||||
fn install_float_to_str_signature() {
|
||||
let bits = 1.5_f64.to_bits();
|
||||
let ty = synth_in_builtins_env(&app("float_to_str", vec![lit_float(bits)]));
|
||||
assert_eq!(ty, Type::str_(), "(float_to_str 1.5) must type as Str");
|
||||
}
|
||||
|
||||
/// Iter 22-floats.3: `is_nan : (Float) -> Bool`. Codegen lowers to
|
||||
/// `fcmp uno double %x, %x` in iter 4 — typecheck only validates
|
||||
/// the signature here.
|
||||
#[test]
|
||||
fn install_is_nan_signature() {
|
||||
let bits = 1.5_f64.to_bits();
|
||||
let ty = synth_in_builtins_env(&app("is_nan", vec![lit_float(bits)]));
|
||||
assert_eq!(ty, Type::bool_(), "(is_nan 1.5) must type as Bool");
|
||||
}
|
||||
}
|
||||
|
||||
@@ -136,6 +136,47 @@ pub(crate) fn builtin_ail_type(name: &str) -> Option<Type> {
|
||||
constraints: vec![],
|
||||
body: Box::new(Type::Var { name: "a".into() }),
|
||||
},
|
||||
// Iter 22-floats.3: Float-conversion and inspection builtins.
|
||||
// Same lockstep with `crates/ailang-check/src/builtins.rs`.
|
||||
"neg" => Type::Forall {
|
||||
vars: vec!["a".into()],
|
||||
constraints: vec![],
|
||||
body: Box::new(Type::Fn {
|
||||
params: vec![Type::Var { name: "a".into() }],
|
||||
ret: Box::new(Type::Var { name: "a".into() }),
|
||||
effects: vec![],
|
||||
param_modes: vec![],
|
||||
ret_mode: ParamMode::Implicit,
|
||||
}),
|
||||
},
|
||||
"int_to_float" => Type::Fn {
|
||||
params: vec![Type::int()],
|
||||
ret: Box::new(Type::float()),
|
||||
effects: vec![],
|
||||
param_modes: vec![],
|
||||
ret_mode: ParamMode::Implicit,
|
||||
},
|
||||
"float_to_int_truncate" => Type::Fn {
|
||||
params: vec![Type::float()],
|
||||
ret: Box::new(Type::int()),
|
||||
effects: vec![],
|
||||
param_modes: vec![],
|
||||
ret_mode: ParamMode::Implicit,
|
||||
},
|
||||
"float_to_str" => Type::Fn {
|
||||
params: vec![Type::float()],
|
||||
ret: Box::new(Type::str_()),
|
||||
effects: vec![],
|
||||
param_modes: vec![],
|
||||
ret_mode: ParamMode::Implicit,
|
||||
},
|
||||
"is_nan" => Type::Fn {
|
||||
params: vec![Type::float()],
|
||||
ret: Box::new(Type::bool_()),
|
||||
effects: vec![],
|
||||
param_modes: vec![],
|
||||
ret_mode: ParamMode::Implicit,
|
||||
},
|
||||
_ => return None,
|
||||
})
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user