merge for float types

drivers/gappa.drv

@@ -175,15 +175,15 @@ end
 
 theory ieee_float.GenericFloat
 
-  meta "instantiate : auto" prop zero_to_real
-  meta "instantiate : auto" prop is_finite
-  meta "instantiate : auto" prop lt_finite
-  meta "instantiate : auto" prop le_finite
-  meta "instantiate : auto" prop neg_finite
-  meta "instantiate : auto" prop add_finite
-  meta "instantiate : auto" prop sub_finite
-  meta "instantiate : auto" prop mul_finite
-  meta "instantiate : auto" prop div_finite
+  meta "instantiate:auto" prop zero_to_real
+  meta "instantiate:auto" prop is_finite
+  meta "instantiate:auto" prop lt_finite
+  meta "instantiate:auto" prop le_finite
+  meta "instantiate:auto" prop neg_finite
+  meta "instantiate:auto" prop add_finite
+  meta "instantiate:auto" prop sub_finite
+  meta "instantiate:auto" prop mul_finite
+  meta "instantiate:auto" prop div_finite
 
 end
 

src/mlw/ity.ml

@@ -636,6 +636,11 @@ let create_range_itysymbol id ir =
   mk_its ~ts ~nfr:false ~priv:false ~mut:false ~frg:false ~mfld:[] ~regs:[]
     ~aflg:[] ~rflg:[] ~def:(Range ir)
 
+let create_float_itysymbol id fp =
+  let ts = create_tysymbol id [] (Float fp) in
+  mk_its ~ts ~nfr:false ~priv:false ~mut:false ~frg:false ~mfld:[] ~regs:[]
+    ~aflg:[] ~rflg:[] ~def:(Float fp)
+
 let fields_of_invariant ftv flds invl =
   if invl = [] then Mpv.empty, flds else
   let fvs = Mpv.fold (fun v _ s -> Svs.add v.pv_vs s) flds Svs.empty in

src/mlw/ity.mli

@@ -132,6 +132,9 @@ val create_alias_itysymbol : preid -> tvsymbol list -> ity -> itysymbol
 val create_range_itysymbol : preid -> Number.int_range -> itysymbol
 (** [create_range_itysymbol id r] creates a new range type. *)
 
+val create_float_itysymbol : preid -> Number.float_format -> itysymbol
+(** [create_float_itysymbol id f] creates a new float type. *)
+
 val restore_its : tysymbol -> itysymbol
 (** raises [Not_found] if the argument is not a [its_ts] *)
 

src/mlw/pdecl.ml

@@ -38,6 +38,9 @@ let create_alias_decl id args ity =
 let create_range_decl id ir =
   mk_itd (create_range_itysymbol id ir) [] [] []
 
+let create_float_decl id fp =
+  mk_itd (create_float_itysymbol id fp) [] [] []
+
 let check_field stv f =
   let loc = f.pv_vs.vs_name.id_loc in
   let ftv = ity_freevars Stv.empty f.pv_ity in
@@ -330,7 +333,32 @@ let create_type_decl dl =
              in
              let minInt_decl = create_logic_decl [make_ls_defn lsminInt [] t] in
              abst, defn, td :: pjd :: maxInt_decl :: minInt_decl :: rest, meta :: metas
-          | Float _ -> assert false (* TODO *)
+          | Float fmt ->
+             let ts = s.its_ts in
+             let td = create_ty_decl ts in
+             let nm = ts.ts_name.id_string ^ "'real" in
+             let id = id_derive nm ts.ts_name in
+             let pj = create_fsymbol id [ty_app ts []] ty_real in
+             let pjd = create_param_decl pj in
+             let nm = ts.ts_name.id_string ^ "'isFinite" in
+             let id = id_derive nm ts.ts_name in
+             let iF = create_psymbol id [ty_app ts []] in
+             let iFd = create_param_decl iF in
+             let meta = Theory.(meta_float,[MAts ts; MAls pj; MAls iF]) in
+             (* create exponent digits attribute *)
+             let nm = ts.ts_name.id_string ^ "'eb" in
+             let id = id_derive nm ts.ts_name in
+             let ls = create_fsymbol id [] ty_int  in
+             let t = t_nat_const fmt.Number.fp_exponent_digits in
+             let eb_decl = create_logic_decl [make_ls_defn ls [] t] in
+             (* create significand digits attribute *)
+             let nm = ts.ts_name.id_string ^ "'sb" in
+             let id = id_derive nm ts.ts_name in
+             let ls = create_fsymbol id [] ty_int  in
+             let t = t_nat_const fmt.Number.fp_significand_digits in
+             let sb_decl = create_logic_decl [make_ls_defn ls [] t] in
+             abst, defn, td :: pjd :: iFd :: eb_decl :: sb_decl :: rest,
+             meta :: metas
           | NoDef -> assert false
         end
     | fl, _ when itd.itd_invariant <> [] ->

src/mlw/pdecl.mli

@@ -69,6 +69,9 @@ val create_alias_decl : preid -> tvsymbol list -> ity -> its_defn
 val create_range_decl : preid -> Number.int_range -> its_defn
 (** [create_range_decl id ir] creates a new range type declaration. *)
 
+val create_float_decl : preid -> Number.float_format -> its_defn
+(** [create_float_decl id fp] creates a new float type declaration. *)
+
 (** {2 Module declarations} *)
 
 type pdecl = private {

src/parser/typing.ml

@@ -894,9 +894,13 @@ let add_types muc tdl =
                   Number.ir_upper = hi } in
        let itd = create_range_decl id ir in
        Hstr.add hts x itd.itd_its; Hstr.add htd x itd
-    | TDfloat _ ->
+    | TDfloat (eb,sb) ->
        check_public ~loc d "Float";
-       assert false (* TODO *)
+       let fp = { Number.fp_exponent_digits = eb;
+                  Number.fp_significand_digits = sb } in
+       let itd = create_float_decl id fp in
+       Hstr.add hts x itd.itd_its; Hstr.add htd x itd
+
 
   and parse ~loc ~alias ~alg pty =
     let rec down = function

theories/floating_point.why

@@ -104,7 +104,7 @@ theory GenFloat
 
   predicate no_overflow (m:mode) (x:real) = abs (round m x) <= max
 
-  axiom Bounded_real_no_overflow :
+  axiom Bounded_real_no_overflow "W:non_conservative_extension:N":
     forall m:mode, x:real. abs x <= max -> no_overflow m x
 
   axiom Round_monotonic :

theories/ieee_float.why

@@ -285,9 +285,11 @@ theory GenericFloat
 
   axiom eq_refl: forall x. is_finite x -> x .= x
 
-  axiom eq_sym: forall x y. x .= y -> y .= x
+  axiom eq_sym "W:non_conservative_extension:N" :
+    forall x y. x .= y -> y .= x
 
-  axiom eq_trans: forall x y z. x .= y -> y .= z -> x .= z
+  axiom eq_trans "W:non_conservative_extension:N":
+    forall x y z. x .= y -> y .= z -> x .= z
 
   axiom eq_zero: zeroF .= (.- zeroF)