Library Adalloc
Require Import Bool.
Require Import Sumbool.
Require Import Arith.
Require Import NArith.
Require Import Ndigits.
Require Import Ndec.
Require Import Nnat.
Require Import Map.
Require Import Fset.
Section AdAlloc.
Variable A : Set.
Allocator: returns an address not in the domain of m.
This allocator is optimal in that it returns the lowest possible address,
in the usual ordering on integers. It is not the most efficient, however.
Fixpoint ad_alloc_opt (m:Map A) : ad :=
match m with
| M0 _ => N0
| M1 _ a _ => if Neqb a N0 then Npos 1 else N0
| M2 _ m1 m2 =>
Nmin (Ndouble (ad_alloc_opt m1))
(Ndouble_plus_one (ad_alloc_opt m2))
end.
Lemma ad_alloc_opt_allocates_1 :
forall m:Map A, MapGet A m (ad_alloc_opt m) = None.
Lemma ad_alloc_opt_allocates :
forall m:Map A, in_dom A (ad_alloc_opt m) m = false.
match m with
| M0 _ => N0
| M1 _ a _ => if Neqb a N0 then Npos 1 else N0
| M2 _ m1 m2 =>
Nmin (Ndouble (ad_alloc_opt m1))
(Ndouble_plus_one (ad_alloc_opt m2))
end.
Lemma ad_alloc_opt_allocates_1 :
forall m:Map A, MapGet A m (ad_alloc_opt m) = None.
Lemma ad_alloc_opt_allocates :
forall m:Map A, in_dom A (ad_alloc_opt m) m = false.
Moreover, this is optimal: all addresses below (ad_alloc_opt m)
are in dom m: