Commit 2f413736 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add functions I.wider, I.cancel_add, and I.cancel_sub.

parent 587f4dba
......@@ -125,6 +125,20 @@ Definition subset xi yi :=
| _, _ => false
end.
Definition wider prec xi yi :=
match yi, xi with
| Inan, _ => false
| Ibnd yl yu, Inan => true
| Ibnd yl yu, Ibnd xl xu =>
let yw := F.sub rnd_NE prec yu yl in
if F.real yw then
match F.cmp (F.sub rnd_NE prec xu xl) yw with
| Xlt | Xeq => false
| _ => true
end
else false
end.
Definition join xi yi :=
match xi, yi with
| Ibnd xl xu, Ibnd yl yu =>
......@@ -327,6 +341,20 @@ Definition sub prec xi yi :=
| _, _ => Inan
end.
Definition cancel_add prec xi yi :=
match xi, yi with
| Ibnd xl xu, Ibnd yl yu =>
Ibnd (F.sub rnd_DN prec xl yl) (F.sub rnd_UP prec xu yu)
| _, _ => Inan
end.
Definition cancel_sub prec xi yi :=
match xi, yi with
| Ibnd xl xu, Ibnd yl yu =>
Ibnd (F.add rnd_DN prec xl yu) (F.add rnd_UP prec xu yl)
| _, _ => Inan
end.
Definition mul_mixed prec xi y :=
match xi with
| Ibnd xl xu =>
......
......@@ -380,6 +380,8 @@ Parameter mask_correct' :
Parameter precision : Type.
Parameter wider : precision -> type -> type -> bool.
Parameter neg : type -> type.
Parameter abs : type -> type.
Parameter pi : precision -> type.
......@@ -423,6 +425,9 @@ Parameter neg_correct' :
contains (convert (neg xi)) (Xneg x) ->
contains (convert xi) x.
Parameter cancel_add : precision -> type -> type -> type.
Parameter cancel_sub : precision -> type -> type -> type.
Parameter bounded : type -> bool.
Parameter lower_bounded : type -> bool.
Parameter upper_bounded : type -> bool.
......
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