Merge branch 'gappa' into 'master'

Improve goals generated by the Gappa printer.

See merge request !103

lib/coq/real/RealInfix.v

@@ -15,10 +15,3 @@ Require Import BuiltIn.
 Require BuiltIn.
 Require real.Real.
 
-(* Why3 goal *)
-Lemma infix_mndt_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R).
-Proof.
-intros x y.
-reflexivity.
-Qed.
-

lib/isabelle/realizations.2018

@@ -7,7 +7,7 @@ f93d912698cd9b10846cd861492655f1c6cf9ab0  int/MinMax.xml
 9e550b757adffdb78db010e8aa14b85a065b3c60  int/Power.xml
 79ca42a9fba90deb0e8eb7fb5396de8a756ac969  bool/Bool.xml
 6bb79ae3bc3abb9b0710a2dfd58c0bd2c41b8f13  real/Real.xml
-657f5992027dc0d739351289093cac512a534fcb  real/RealInfix.xml
+f80da4609433de4d5ccb6ebbbe0fa954c5ed5187  real/RealInfix.xml
 c2410d334c7e0852086bb13cae1189f601f3b1c6  real/Abs.xml
 da70a842eac8ff6687f1d119c309be4c227976ff  real/MinMax.xml
 3cc6bd97503e596fae70c51ef1d5401a62114b94  real/FromInt.xml

src/printer/gappa.ml

@@ -245,7 +245,7 @@ let rec print_fmla info defs fmt f =
           let c2 = constant_value defs t2 in
           fprintf fmt "%a in [%s,%s]" term t1 c2 c2
         with Not_found ->
-          fprintf fmt "%a - %a in [0,0]" term t1 term t2
+          fprintf fmt "%a = %a" term t1 term t2
       end
   | Tapp (ls, [t1;t2]) when Mls.mem ls info.info_ops_of_rel ->
       let s,op,rev_op = try Mls.find ls info.info_ops_of_rel

src/transform/abstraction.ml

@@ -28,7 +28,8 @@ let abstraction (keep : lsymbol -> bool) =
     | _ ->
         let t = t_attr_set Sattr.empty t in
         let (ls, tabs) = try Hterm_nt_na.find term_table t with Not_found ->
-          let ls = create_lsymbol (id_fresh "abstr") [] t.t_ty in
+          let name = Format.asprintf "%a" Pretty.print_term t in
+          let ls = create_lsymbol (id_fresh name) [] t.t_ty in
           let tabs = t_app ls [] t.t_ty in
           Hterm_nt_na.add term_table t (ls, tabs);
           ls, tabs in

src/transform/eliminate_literal.ml

@@ -40,6 +40,12 @@ let add_literal (known_lit, decl as acc) t c ls_proj fin =
    NOTE: in this case, [add_literal] above is incorrect. *)
 let rec abstract_terms kn range_metas float_metas type_kept acc t =
   match t.t_node, t.t_ty with
+  | Tapp (ls, [{ t_node = Tconst (Number.ConstInt _ as c); t_ty = Some {ty_node = Tyapp (ts,[])} }]), _
+    when not (ts_equal ts ts_int || Sts.mem ts type_kept) && ls_equal ls (Mts.find ts range_metas) ->
+      acc, t_const c ty_int
+  | Tapp (ls, [{ t_node = Tconst (Number.ConstReal _ as c); t_ty = Some {ty_node = Tyapp (ts,[])} }]), _
+    when not (ts_equal ts ts_real || Sts.mem ts type_kept) && ls_equal ls (fst (Mts.find ts float_metas)) ->
+      acc, t_const c ty_int
   | Tconst (Number.ConstInt _ as c), Some {ty_node = Tyapp (ts,[])}
     when not (ts_equal ts ts_int || Sts.mem ts type_kept) ->
       let to_int = Mts.find ts range_metas in

stdlib/real.mlw

@@ -20,7 +20,6 @@ module Real
   val function  (*)  real real : real
   val predicate (<)  real real : bool
 
-  let (-)  (x y : real) = x + -y
   let predicate (>)  (x y : real) = y < x
   let predicate (<=) (x y : real) = x < y || x = y
   let predicate (>=) (x y : real) = y <= x
@@ -30,6 +29,10 @@ module Real
     function (-_) = (-_), function (+) = (+),
     function (*) = (*), predicate (<=) = (<=)
 
+  let (-) (x y : real)
+    ensures { result = x - y }
+  = x + -y
+
   val (/) (x y:real) : real
     requires { y <> 0.0 }
     ensures  { result = x / y }