Commit ce6dc6fd authored by Guillaume Melquiond's avatar Guillaume Melquiond

Improve alignment of definitions in Coq printer.

parent fde14c43
......@@ -150,56 +150,58 @@ Qed.
(* Why3 assumption *)
Definition of_real_post (m:floating_point.Rounding.mode) (x:R)
(res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m
x)) /\ (((exact res) = x) /\ ((model res) = x)).
(res:floating_point.DoubleFormat.double) : Prop :=
((value res) = (round m x)) /\ (((exact res) = x) /\ ((model res) = x)).
(* Why3 assumption *)
Definition add_post (m:floating_point.Rounding.mode)
(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m
((value x) + (value y))%R)) /\
(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double) : Prop :=
((value res) = (round m ((value x) + (value y))%R)) /\
(((exact res) = ((exact x) + (exact y))%R) /\
((model res) = ((model x) + (model y))%R)).
((model res) = ((model x) + (model y))%R)).
(* Why3 assumption *)
Definition sub_post (m:floating_point.Rounding.mode)
(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m
((value x) - (value y))%R)) /\
(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double) : Prop :=
((value res) = (round m ((value x) - (value y))%R)) /\
(((exact res) = ((exact x) - (exact y))%R) /\
((model res) = ((model x) - (model y))%R)).
((model res) = ((model x) - (model y))%R)).
(* Why3 assumption *)
Definition mul_post (m:floating_point.Rounding.mode)
(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m
((value x) * (value y))%R)) /\
(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double) : Prop :=
((value res) = (round m ((value x) * (value y))%R)) /\
(((exact res) = ((exact x) * (exact y))%R) /\
((model res) = ((model x) * (model y))%R)).
((model res) = ((model x) * (model y))%R)).
(* Why3 assumption *)
Definition div_post (m:floating_point.Rounding.mode)
(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m
((value x) / (value y))%R)) /\
(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double) : Prop :=
((value res) = (round m ((value x) / (value y))%R)) /\
(((exact res) = ((exact x) / (exact y))%R) /\
((model res) = ((model x) / (model y))%R)).
((model res) = ((model x) / (model y))%R)).
(* Why3 assumption *)
Definition neg_post (x:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double): Prop :=
((value res) = (-(value x))%R) /\ (((exact res) = (-(exact x))%R) /\
((model res) = (-(model x))%R)).
(res:floating_point.DoubleFormat.double) : Prop :=
((value res) = (-(value x))%R) /\
(((exact res) = (-(exact x))%R) /\ ((model res) = (-(model x))%R)).
(* Why3 assumption *)
Definition lt (x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double): Prop := ((value x) < (value y))%R.
(y:floating_point.DoubleFormat.double) : Prop :=
((value x) < (value y))%R.
(* Why3 assumption *)
Definition gt (x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double): Prop := ((value y) < (value x))%R.
(y:floating_point.DoubleFormat.double) : Prop :=
((value y) < (value x))%R.
......@@ -163,56 +163,58 @@ Qed.
(* Why3 assumption *)
Definition of_real_post (m:floating_point.Rounding.mode) (x:R)
(res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
x)) /\ (((exact res) = x) /\ ((model res) = x)).
(res:floating_point.SingleFormat.single) : Prop :=
((value res) = (round m x)) /\ (((exact res) = x) /\ ((model res) = x)).
(* Why3 assumption *)
Definition add_post (m:floating_point.Rounding.mode)
(x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
((value x) + (value y))%R)) /\
(x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single) : Prop :=
((value res) = (round m ((value x) + (value y))%R)) /\
(((exact res) = ((exact x) + (exact y))%R) /\
((model res) = ((model x) + (model y))%R)).
((model res) = ((model x) + (model y))%R)).
(* Why3 assumption *)
Definition sub_post (m:floating_point.Rounding.mode)
(x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
((value x) - (value y))%R)) /\
(x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single) : Prop :=
((value res) = (round m ((value x) - (value y))%R)) /\
(((exact res) = ((exact x) - (exact y))%R) /\
((model res) = ((model x) - (model y))%R)).
((model res) = ((model x) - (model y))%R)).
(* Why3 assumption *)
Definition mul_post (m:floating_point.Rounding.mode)
(x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
((value x) * (value y))%R)) /\
(x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single) : Prop :=
((value res) = (round m ((value x) * (value y))%R)) /\
(((exact res) = ((exact x) * (exact y))%R) /\
((model res) = ((model x) * (model y))%R)).
((model res) = ((model x) * (model y))%R)).
(* Why3 assumption *)
Definition div_post (m:floating_point.Rounding.mode)
(x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
((value x) / (value y))%R)) /\
(x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single) : Prop :=
((value res) = (round m ((value x) / (value y))%R)) /\
(((exact res) = ((exact x) / (exact y))%R) /\
((model res) = ((model x) / (model y))%R)).
((model res) = ((model x) / (model y))%R)).
(* Why3 assumption *)
Definition neg_post (x:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single): Prop :=
((value res) = (-(value x))%R) /\ (((exact res) = (-(exact x))%R) /\
((model res) = (-(model x))%R)).
(res:floating_point.SingleFormat.single) : Prop :=
((value res) = (-(value x))%R) /\
(((exact res) = (-(exact x))%R) /\ ((model res) = (-(model x))%R)).
(* Why3 assumption *)
Definition lt (x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single): Prop := ((value x) < (value y))%R.
(y:floating_point.SingleFormat.single) : Prop :=
((value x) < (value y))%R.
(* Why3 assumption *)
Definition gt (x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single): Prop := ((value y) < (value x))%R.
(y:floating_point.SingleFormat.single) : Prop :=
((value y) < (value x))%R.
......@@ -22,9 +22,9 @@ Require list.Reverse.
Require list.NumOcc.
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a))
(l2:(list a)): Prop := forall (x:a), ((list.NumOcc.num_occ x
l1) = (list.NumOcc.num_occ x l2)).
Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list a)) :
Prop :=
forall (x:a), ((list.NumOcc.num_occ x l1) = (list.NumOcc.num_occ x l2)).
(* Why3 goal *)
Lemma Permut_refl {a:Type} {a_WT:WhyType a} :
......
......@@ -19,9 +19,9 @@ Require map.Map.
Require map.Occ.
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (m1:(Z -> a)) (m2:(Z -> a)) (l:Z)
(u:Z): Prop := forall (v:a), ((map.Occ.occ v m1 l u) = (map.Occ.occ v m2 l
u)).
Definition permut {a:Type} {a_WT:WhyType a} (m1:Z -> a) (m2:Z -> a) (l:Z)
(u:Z) : Prop :=
forall (v:a), ((map.Occ.occ v m1 l u) = (map.Occ.occ v m2 l u)).
(* Why3 goal *)
Lemma permut_trans {a:Type} {a_WT:WhyType a} :
......
......@@ -44,7 +44,7 @@ Hint Unfold mem.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:a -> bool)
(s2:a -> bool) : Prop :=
(s2:a -> bool) : Prop :=
forall (x:a), (mem x s1) <-> (mem x s2).
Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).
......@@ -68,7 +68,7 @@ Qed.
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a} (s1:a -> bool) (s2:a -> bool) :
Prop :=
Prop :=
forall (x:a), (mem x s1) -> mem x s2.
(* Why3 goal *)
......
......@@ -755,7 +755,7 @@ let print_param_decl ~prev info fmt ls =
let print_logic_decl info fmt (ls,ld) =
let _, _, all_ty_params = ls_ty_vars ls in
let vl,e = open_ls_defn ld in
fprintf fmt "(* Why3 assumption *)@\n@[<hv 2>Definition @[%a%a%a :@ %a@] :=@ @[%a.@]@]@\n"
fprintf fmt "(* Why3 assumption *)@\n@[<hv 2>@[<4>Definition %a%a%a :@ %a@] :=@ @[%a.@]@]@\n"
print_ls ls
(print_tv_binders info ~whytypes:true ~implicit:true) all_ty_params
(print_list_pre space (print_vsty info)) vl
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment