Commit 8ea9be8b authored by Heiko Becker's avatar Heiko Becker

WIP forgot possimps file

parent 7679dff6
Require Import Coq.PArith.PArith Coq.QArith.QArith Recdef.
Open Scope positive_scope.
Function splitFraction (num:positive) (den:positive)
{measure Pos.to_nat num}
: option (positive * positive * positive) :=
if (num <=? den)
then None
else
match splitFraction (num-den) (den) with
|None => Some (1%positive, (num-den), den)
|Some (p, num, den) => Some (p + 1, num, den)
end.
Proof.
intros.
rewrite <- Pos2Nat.inj_lt.
rewrite Pos.leb_gt in * |-.
rewrite Pos.lt_iff_add.
eexists.
rewrite Pos.sub_add; auto.
Defined.
Definition fractionBits (word_size:positive) (val:Q) :=
match val with
| Qmake num den =>
match num with
| Z0 => word_size
| Zpos x =>
match splitFraction x den with
|Some (full, num, den) =>
word_size - Pos.of_nat (Pos.size_nat full)
|None =>
word_size
end
| Zneg x =>
match splitFraction x den with
|Some (full, num, den) =>
word_size - Pos.of_nat (Pos.size_nat full)
|None =>
word_size
end
end
end.
Close Scope positive_scope.
\ No newline at end of file
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