升级Why3至最新版本后遇构造器未绑定等错误求修复

问题1：Unbound constructor Why3.Number.ConstReal #

旧版Why3的实数常量构造API在新版本中被完全重构：

• Why3.Number.ConstReal构造器已被移除
• real_const_dec的参数类型从字符串改为BigInt.t，接口逻辑也有调整

问题2：Ty.ty -> T.term与T.term类型不匹配 #

新版T.t_const的签名变更为需要显式传入类型参数，返回值是等待类型的函数；而T.t_app_infer要求传入直接的T.term类型参数。

完整修复代码 #

let why3_float f =
  let (f_frac, f_int) = modf f in
  let int_str = Printf.sprintf "%.0f" f_int in
  if f_int < 0.0 then
    let int_unsigned = String.sub int_str 1 (String.length int_str - 1) in
    let frac_str = String.sub (Printf.sprintf "%.3f" f_frac) 3 3 in
    -- 构造无符号部分的实数常量
    let pos_real = Why3.Number.real_const_dec (Why3.BigInt.of_string int_unsigned) (Why3.BigInt.of_string frac_str) None in
    -- 使用自动推导类型的常量构造函数
    let t_zero = T.t_const_infer Why3.Number.zero_real in
    let t_pos = T.t_const_infer pos_real in
    T.t_app_infer why3_rsub [t_zero; t_pos]
  else
    let frac_str = String.sub (Printf.sprintf "%.3f" f_frac) 2 3 in
    let real_val = Why3.Number.real_const_dec (Why3.BigInt.of_string int_str) (Why3.BigInt.of_string frac_str) None in
    T.t_const_infer real_val

关键修复点说明 #

1. 替换过时的实数构造逻辑

   • 用新版Why3.Number.real_const_dec构造十进制实数，参数改为BigInt.t类型（通过BigInt.of_string转换字符串）
   • 直接使用Why3.Number.zero_real获取0值常量，避免手动构造的繁琐和错误

2. 解决类型不匹配问题

   • 用T.t_const_infer替代T.t_const：该函数会自动推导常量的类型，直接返回T.term类型值，无需手动传入类型参数

3. 简化代码逻辑

   • 移除了旧版中手动构造real_value和RLitDec的复杂代码，改用官方提供的标准API，提升代码可读性和兼容性

内容的提问来源于stack exchange，提问作者qwerty