feat: Support more Alt-Ergo primitives

src/interface/term.ml

@@ -761,6 +761,9 @@ module type Ae_Arith = sig
     val to_real : t -> t
     (** Conversion from an integer term to a real term. *)
 
+    val abs : t -> t
+    (** Arithmetic absolute value. *)
+
   end
 
   module Real : sig
@@ -769,6 +772,12 @@ module type Ae_Arith = sig
     val div : t -> t -> t
     (** Exact division on reals. *)
 
+    val is_int : t -> t
+    (** Integer testing *)
+
+    val floor_to_int : t -> t
+    (** Greatest integer smaller than the given real *)
+
   end
 
 end
@@ -931,6 +940,46 @@ module type Ae_Bitv = sig
 
 end
 
+module type Ae_Float_Float = sig
+
+  type t
+  (** the type of terms *)
+
+  val roundNearestTiesToEven: t
+  (** constant for rounding mode RNE *)
+
+  val roundNearestTiesToAway: t
+  (** constant for rounding mode RNA *)
+
+  val roundTowardPositive: t
+  (** constant for rounding mode RTP *)
+
+  val roundTowardNegative: t
+  (** constant for rounding mode RTN *)
+
+  val roundTowardZero: t
+  (** constant for rounding mode RTZ *)
+
+end
+
+(* Minimum required to type Ae floats *)
+module type Ae_Float = sig
+
+  type t
+  (** The type of terms *)
+
+  type ty
+  (** The type of types. *)
+
+  val ty : t -> ty
+  (** Type of a term. *)
+
+  module Float : Ae_Float_Float with type t := t
+  (** Sub-module used for namespacing the floating number part
+      of the theory requirements *)
+
+end
+
 (** Minimum required to type tptp's tff *)
 module type Tptp_Tff_Core = sig
 

src/interface/ty.ml

@@ -232,6 +232,17 @@ module type Ae_Bitv = sig
 
 end
 
+(** Signature required by types for typing ae's floats *)
+module type Ae_Float = sig
+
+  type t
+  (** The type of types *)
+
+  val roundingMode: t
+  (** Type of the rounding modes *)
+
+end
+
 (** Signature required by types for typing tptp *)
 module type Tptp_Base = sig
 
@@ -432,6 +443,3 @@ module type Zf_Arith = sig
     (** The type of integers *)
 
 end
-
-
-

src/loop/typer.ml

@@ -20,6 +20,9 @@ module Ae_Arrays =
 module Ae_Bitv =
   Dolmen_type.Bitv.Ae.Tff(T)
     (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv)
+module Ae_Float =
+  Dolmen_type.Float.Ae.Tff(T)
+    (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term)
 
 (* Dimacs builtin *)
 module Dimacs =
@@ -1552,6 +1555,7 @@ module Typer(State : State.S) = struct
           Ae_Arith.parse;
           Ae_Arrays.parse;
           Ae_Bitv.parse;
+          Ae_Float.parse;
         ]) in
       T.empty_env ~order:First_order
         ~st:(State.get ty_state st).typer

src/typecheck/arith.ml

@@ -91,6 +91,19 @@ module Ae = struct
         | Type.Id { Id.ns = Value Hexadecimal; name = Simple name; } ->
           Type.builtin_term (Base.app0 (module Type) env s (T.real name))
 
+        | Type.Id { Id.ns = Term; name = Simple name; } ->
+          begin match name with
+          | "real_of_int" ->
+            Type.builtin_term (Base.term_app1 (module Type) env s T.Int.to_real)
+          | "int_floor" ->
+            Type.builtin_term (Base.term_app1 (module Type) env s T.Real.floor_to_int)
+          | "real_is_int" ->
+            Type.builtin_term (Base.term_app1 (module Type) env s T.Real.is_int)
+          | "abs_int" ->
+            Type.builtin_term (Base.term_app1 (module Type) env s T.Int.abs)
+          | _ -> `Not_found
+          end
+
         (* Arithmetic *)
         | Type.Builtin Term.Minus ->
           Type.builtin_term (Base.term_app1_ast (module Type) env s
@@ -186,8 +199,8 @@ module Ae = struct
             (parse_in_interval env ~strict_lower ~strict_upper)
         )
 
-        (* Catch-all *)
-        | _ -> `Not_found
+      (* Catch-all *)
+      | _ -> `Not_found
 
   end
 end
@@ -1288,4 +1301,3 @@ module Zf = struct
 
   end
 end
-

src/typecheck/float.ml

@@ -2,6 +2,46 @@
 module Id = Dolmen.Std.Id
 module Ast = Dolmen.Std.Term
 
+(* Ae floating point *)
+(* ************************************************************************ *)
+
+module Ae = struct
+
+  module Tff
+      (Type : Tff_intf.S)
+      (Ty : Dolmen.Intf.Ty.Ae_Float with type t := Type.Ty.t)
+      (T : Dolmen.Intf.Term.Ae_Float with type t := Type.T.t
+                                      and type ty := Type.Ty.t) = struct
+
+    module F = T.Float
+
+    let parse env s =
+      match s with
+
+      (* sorts *)
+      | Type.Id { ns = Sort; name = Simple "fpa_rounding_mode"; } ->
+        Type.builtin_ty (Base.app0 (module Type) env s Ty.roundingMode)
+
+      (* terms *)
+      | Type.Id { ns = Term; name = Simple name; } ->
+        begin match name with
+          | "NearestTiesToEven" ->
+            Type.builtin_term (Base.app0 (module Type) env s F.roundNearestTiesToEven)
+          | "NearestTiesToAway" ->
+            Type.builtin_term (Base.app0 (module Type) env s F.roundNearestTiesToAway)
+          | "Up" ->
+            Type.builtin_term (Base.app0 (module Type) env s F.roundTowardPositive)
+          | "Down" ->
+            Type.builtin_term (Base.app0 (module Type) env s F.roundTowardNegative)
+          | "ToZero" ->
+            Type.builtin_term (Base.app0 (module Type) env s F.roundTowardZero)
+          | _ -> `Not_found
+        end
+
+      | _ -> `Not_found
+  end
+end
+
 (* Smtlib Floating Point *)
 (* ************************************************************************ *)
 

src/typecheck/float.mli

@@ -1,3 +1,16 @@
+(** Ae floating point builtins *)
+module Ae : sig
+
+  module Tff
+      (Type : Tff_intf.S)
+      (Ty : Dolmen.Intf.Ty.Ae_Float with type t := Type.Ty.t)
+      (T : Dolmen.Intf.Term.Ae_Float with type t := Type.T.t
+                                          and type ty := Type.Ty.t) : sig
+
+    val parse : Type.builtin_symbols
+  end
+
+end
 
 (** Smtlib floating point builtins *)
 module Smtlib2 : sig

tests/typing/pass/ae/triggers/fpa-theory-2019-10-08-19h00.ae

@@ -9,23 +9,6 @@
 (*                                                                            *)
 (******************************************************************************)
 
-type fpa_rounding_mode =
-  (* five standard/why3 fpa rounding modes *)
-    NearestTiesToEven (*ne in Gappa: to nearest, tie breaking to even mantissas*)
-  | ToZero (* zr in Gappa: toward zero *)
-  | Up (* up in Gappa: toward plus infinity *)
-  | Down (* dn in Gappa: toward minus infinity *)
-  | NearestTiesToAway (* na : to nearest, tie breaking away from zero *)
-
-  (* additional Gappa rounding modes *)
-  | Aw (* aw in Gappa: away from zero **)
-  | Od (* od in Gappa: to odd mantissas *)
-  | No (* no in Gappa: to nearest, tie breaking to odd mantissas *)
-  | Nz (* nz in Gappa: to nearest, tie breaking toward zero *)
-  | Nd (* nd in Gappa: to nearest, tie breaking toward minus infinity *)
-  | Nu (* nu in Gappa: to nearest, tie breaking toward plus infinity *)
-
-
 (* the first argument is mantissas' size (including the implicit bit),
    the second one is the exp of the min representable normalized number,
    the third one is the rounding mode, and the last one is the real to
@@ -51,9 +34,6 @@ logic float64d: real -> real
 (* rounds to nearest integer depending on rounding mode *)
 logic integer_round: fpa_rounding_mode, real -> int
 
-(* type cast: from int to real *)
-logic real_of_int : int -> real
-
 (* abs value of a real *)
 logic abs_real : real -> real
 
@@ -66,12 +46,6 @@ logic sqrt_real_default : real -> real
 (* sqrt value of a real by excess *)
 logic sqrt_real_excess : real -> real
 
-(* abs value of an int *)
-logic abs_int : int -> int
-
-(* (integer) floor of a rational *)
-logic int_floor : real -> int
-
 (* (integer) ceiling of a rational *)
 logic int_ceil : real -> int