Source file float.ml

module Id = Dolmen.Std.Id
module Ast = Dolmen.Std.Term

(* Smtlib Floating Point *)
(* ************************************************************************ *)

module Smtlib2 = struct

  module Tff
      (Type : Tff_intf.S)
      (Ty : Dolmen.Intf.Ty.Smtlib_Float with type t := Type.Ty.t)
      (T : Dolmen.Intf.Term.Smtlib_Float with type t := Type.T.t
                                          and type ty := Type.Ty.t) = struct

    module B = T.Bitv
    module R = T.Real
    module F = T.Float

    type _ Type.err +=
      | Invalid_bin_char : char -> Ast.t Type.err
      | Invalid_hex_char : char -> Ast.t Type.err
      | Invalid_dec_char : char -> Ast.t Type.err

    let parse_int env ast s =
      match int_of_string s with
      | i when i >= 0 -> i
      | _ ->
        Type._error env (Ast ast)
          (Type.Expected ("a positive integer", None))
      | exception Failure _ ->
        Type._error env (Ast ast)
          (Type.Expected ("a positive integer", None))

    let parse_binary env s ast =
      match Misc.Bitv.parse_binary s with
      | s -> B.mk s
      | exception Misc.Bitv.Invalid_char c ->
        Type._error env (Ast ast) (Invalid_bin_char c)

    let parse_hexa env s ast =
      match Misc.Bitv.parse_hexa s with
      | s -> B.mk s
      | exception Misc.Bitv.Invalid_char c ->
        Type._error env (Ast ast) (Invalid_hex_char c)

    let indexed1 env mk i_s ast =
      let i = parse_int env ast i_s in
      mk i

    let indexed2 env mk i_s j_s ast =
      let i = parse_int env ast i_s in
      let j = parse_int env ast j_s in
      mk i j

    let to_fp env symbol e s = `Term (fun ast args ->
        let e = parse_int env ast e in
        let s = parse_int env ast s in
        let args = List.map (Type.parse_term env) args in
        match args with
        | [ a ] -> F.ieee_format_to_fp e s a
        | [ rm; b ] -> begin
            match Ty.view @@ T.ty b with
            | `Real -> F.real_to_fp e s rm b
            | `Bitv _ -> F.sbv_to_fp e s rm b
            | `Float (_,_) -> F.to_fp e s rm b
            | _ -> Type._error env (Ast ast) (
                Type.Expected ("a real, bitvector or float", Some (Term b)))
          end
        | _ -> Type._error env (Ast ast)
                 (Type.Bad_op_arity (symbol, [1; 2], List.length args))
      )

    let parse _version env s =
      match s with

      (* sorts *)
      | Type.Id { ns = Sort; name = Simple "Float16"; } ->
        `Ty (Base.app0 (module Type) env s (Ty.float 5 11))
      | Type.Id { ns = Sort; name = Simple "Float32"; } ->
        `Ty (Base.app0 (module Type) env s (Ty.float 8 24))
      | Type.Id { ns = Sort; name = Simple "Float64"; } ->
        `Ty (Base.app0 (module Type) env s (Ty.float 11 53))
      | Type.Id { ns = Sort; name = Simple "Float128"; } ->
        `Ty (Base.app0 (module Type) env s (Ty.float 15 113))
      | Type.Id { ns = Sort; name = Simple "RoundingMode"; } ->
        `Ty (Base.app0 (module Type) env s Ty.roundingMode)

      (* indexed sorts *)
      | Type.Id { ns = Sort; name = Indexed { basename; indexes; } } ->
        Base.parse_indexed basename indexes (function
            | "BitVec" -> `Unary (function n_s ->
                `Ty (Base.app0_ast (module Type) env s
                       (indexed1 env Ty.bitv n_s)))
            | "FloatingPoint" -> `Binary (fun n_e n_s ->
                `Ty (Base.app0_ast (module Type) env s
                       (indexed2 env Ty.float n_e n_s)))
            | _ -> `Not_indexed)
          ~err:(Base.bad_ty_index_arity (module Type) env)
          ~k:(function () -> `Not_found)


      (* Bitvector litterals *)
      | Type.Id { ns = Value Binary; name = Simple name; } ->
        `Term (Base.app0_ast (module Type) env s (parse_binary env name))
      | Type.Id { ns = Value Hexadecimal; name = Simple name; } ->
        `Term (Base.app0_ast (module Type) env s (parse_hexa env name))

      (* terms *)
      | Type.Id { ns = Term; name = Simple name; } ->
        begin match name with
          | "fp" ->
            `Term (Base.term_app3 (module Type) env s F.fp)
          | "RNE" | "roundNearestTiesToEven" ->
            `Term (Base.app0 (module Type) env s F.roundNearestTiesToEven)
          | "RNA" | "roundNearestTiesToAway" ->
            `Term (Base.app0 (module Type) env s F.roundNearestTiesToAway)
          | "RTP" | "roundTowardPositive" ->
            `Term (Base.app0 (module Type) env s F.roundTowardPositive)
          | "RTN" | "roundTowardNegative" ->
            `Term (Base.app0 (module Type) env s F.roundTowardNegative)
          | "RTZ" | "roundTowardZero" ->
            `Term (Base.app0 (module Type) env s F.roundTowardZero)
          | "fp.abs" ->
            `Term (Base.term_app1 (module Type) env s F.abs)
          | "fp.neg" ->
            `Term (Base.term_app1 (module Type) env s F.neg)
          | "fp.add" ->
            `Term (Base.term_app3 (module Type) env s F.add)
          | "fp.sub" ->
            `Term (Base.term_app3 (module Type) env s F.sub)
          | "fp.mul" ->
            `Term (Base.term_app3 (module Type) env s F.mul)
          | "fp.div" ->
            `Term (Base.term_app3 (module Type) env s F.div)
          | "fp.fma" ->
            `Term (Base.term_app4 (module Type) env s F.fma)
          | "fp.sqrt" ->
            `Term (Base.term_app2 (module Type) env s F.sqrt)
          | "fp.rem" ->
            `Term (Base.term_app2 (module Type) env s F.rem)
          | "fp.roundToIntegral" ->
            `Term (Base.term_app2 (module Type) env s F.roundToIntegral)
          | "fp.min" ->
            `Term (Base.term_app2 (module Type) env s F.min)
          | "fp.max" ->
            `Term (Base.term_app2 (module Type) env s F.max)
          | "fp.leq" ->
            `Term (Base.term_app_chain (module Type) env s F.leq)
          | "fp.lt" ->
            `Term (Base.term_app_chain (module Type) env s F.lt)
          | "fp.geq" ->
            `Term (Base.term_app_chain (module Type) env s F.geq)
          | "fp.gt" ->
            `Term (Base.term_app_chain (module Type) env s F.gt)
          | "fp.eq" ->
            `Term (Base.term_app_chain (module Type) env s F.eq)
          | "fp.isNormal" ->
            `Term (Base.term_app1 (module Type) env s F.isNormal)
          | "fp.isSubnormal" ->
            `Term (Base.term_app1 (module Type) env s F.isSubnormal)
          | "fp.isZero" ->
            `Term (Base.term_app1 (module Type) env s F.isZero)
          | "fp.isInfinite" ->
            `Term (Base.term_app1 (module Type) env s F.isInfinite)
          | "fp.isNaN" ->
            `Term (Base.term_app1 (module Type) env s F.isNaN)
          | "fp.isNegative" ->
            `Term (Base.term_app1 (module Type) env s F.isNegative)
          | "fp.isPositive" ->
            `Term (Base.term_app1 (module Type) env s F.isPositive)
          | "fp.to_real" ->
            `Term (Base.term_app1 (module Type) env s F.to_real)
          | _ -> `Not_found
        end
      | Type.Id { ns = Term; name = Indexed { basename; indexes; } } as symbol ->
        Base.parse_indexed basename indexes (function
            | "+oo" -> `Binary (fun e s ->
                `Term (Base.app0_ast (module Type) env symbol
                         (indexed2 env F.plus_infinity e s)))
            | "-oo" -> `Binary (fun e s ->
                `Term (Base.app0_ast (module Type) env symbol
                         (indexed2 env F.minus_infinity e s)))
            | "+zero" -> `Binary (fun e s ->
                `Term (Base.app0_ast (module Type) env symbol
                         (indexed2 env F.plus_zero e s)))
            | "-zero" -> `Binary (fun e s ->
                `Term (Base.app0_ast (module Type) env symbol
                         (indexed2 env F.minus_zero e s)))
            | "NaN" -> `Binary (fun e s ->
                `Term (Base.app0_ast (module Type) env symbol
                         (indexed2 env F.nan e s)))
            | "to_fp" -> `Binary (to_fp env symbol)
            | "to_fp_unsigned" -> `Binary (fun e s ->
                `Term (Base.term_app2_ast (module Type) env symbol
                         (indexed2 env F.ubv_to_fp e s)))
            | "fp.to_ubv" -> `Unary (fun n ->
                `Term (Base.term_app2_ast (module Type) env symbol
                         (indexed1 env F.to_ubv n)))
            | "fp.to_sbv" -> `Unary (fun n ->
                `Term (Base.term_app2_ast (module Type) env symbol
                         (indexed1 env F.to_sbv n)))
            | _ -> `Not_indexed)
          ~err:(Base.bad_term_index_arity (module Type) env)
          ~k:(function () -> `Not_found)

      | _ -> `Not_found

end

end