🍃 Map.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Compare.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.List.
Import Error_monad.Notations.
Module S.
Record signature {key : Set} {t : Set → Set} : Set := {
key := key;
t := t;
empty : ∀ {a : Set}, t a;
is_empty : ∀ {a : Set}, t a → bool;
mem : ∀ {a : Set}, key → t a → bool;
add : ∀ {a : Set}, key → a → t a → t a;
update : ∀ {a : Set}, key → (option a → option a) → t a → t a;
singleton : ∀ {a : Set}, key → a → t a;
remove : ∀ {a : Set}, key → t a → t a;
merge :
∀ {a b c : Set},
(key → option a → option b → option c) → t a → t b → t c;
union :
∀ {a : Set}, (key → a → a → option a) → t a → t a → t a;
compare : ∀ {a : Set}, (a → a → int) → t a → t a → int;
equal : ∀ {a : Set}, (a → a → bool) → t a → t a → bool;
iter : ∀ {a : Set}, (key → a → unit) → t a → unit;
iter_e :
∀ {a trace : Set},
(key → a → Pervasives.result unit trace) → t a →
Pervasives.result unit trace;
iter_s : ∀ {a : Set}, (key → a → unit) → t a → unit;
iter_p : ∀ {a : Set}, (key → a → unit) → t a → unit;
iter_es :
∀ {a trace : Set},
(key → a → Pervasives.result unit trace) → t a →
Pervasives.result unit trace;
fold : ∀ {a b : Set}, (key → a → b → b) → t a → b → b;
fold_e :
∀ {a b trace : Set},
(key → a → b → Pervasives.result b trace) → t a → b →
Pervasives.result b trace;
fold_s :
∀ {a b : Set}, (key → a → b → b) → t a → b → b;
fold_es :
∀ {a b trace : Set},
(key → a → b → Pervasives.result b trace) → t a → b →
Pervasives.result b trace;
for_all : ∀ {a : Set}, (key → a → bool) → t a → bool;
_exists : ∀ {a : Set}, (key → a → bool) → t a → bool;
filter : ∀ {a : Set}, (key → a → bool) → t a → t a;
filter_map : ∀ {a b : Set}, (key → a → option b) → t a → t b;
partition : ∀ {a : Set}, (key → a → bool) → t a → t a × t a;
cardinal : ∀ {a : Set}, t a → int;
bindings : ∀ {a : Set}, t a → list (key × a);
min_binding : ∀ {a : Set}, t a → option (key × a);
min_binding_opt : ∀ {a : Set}, t a → option (key × a);
max_binding : ∀ {a : Set}, t a → option (key × a);
max_binding_opt : ∀ {a : Set}, t a → option (key × a);
choose : ∀ {a : Set}, t a → option (key × a);
choose_opt : ∀ {a : Set}, t a → option (key × a);
split : ∀ {a : Set}, key → t a → t a × option a × t a;
find : ∀ {a : Set}, key → t a → option a;
find_opt : ∀ {a : Set}, key → t a → option a;
find_first : ∀ {a : Set}, (key → bool) → t a → option (key × a);
find_first_opt : ∀ {a : Set}, (key → bool) → t a → option (key × a);
find_last : ∀ {a : Set}, (key → bool) → t a → option (key × a);
find_last_opt : ∀ {a : Set}, (key → bool) → t a → option (key × a);
map : ∀ {a b : Set}, (a → b) → t a → t b;
mapi : ∀ {a b : Set}, (key → a → b) → t a → t b;
to_seq : ∀ {a : Set}, t a → Seq.t (key × a);
to_rev_seq : ∀ {a : Set}, t a → Seq.t (key × a);
to_seq_from : ∀ {a : Set}, key → t a → Seq.t (key × a);
add_seq : ∀ {a : Set}, Seq.t (key × a) → t a → t a;
of_seq : ∀ {a : Set}, Seq.t (key × a) → t a;
iter_ep :
∀ {a _error: Set},
(key → a → Pervasives.result unit (Error_monad.trace _error)) →
t a →
Pervasives.result unit (Error_monad.trace _error);
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Compare.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.List.
Import Error_monad.Notations.
Module S.
Record signature {key : Set} {t : Set → Set} : Set := {
key := key;
t := t;
empty : ∀ {a : Set}, t a;
is_empty : ∀ {a : Set}, t a → bool;
mem : ∀ {a : Set}, key → t a → bool;
add : ∀ {a : Set}, key → a → t a → t a;
update : ∀ {a : Set}, key → (option a → option a) → t a → t a;
singleton : ∀ {a : Set}, key → a → t a;
remove : ∀ {a : Set}, key → t a → t a;
merge :
∀ {a b c : Set},
(key → option a → option b → option c) → t a → t b → t c;
union :
∀ {a : Set}, (key → a → a → option a) → t a → t a → t a;
compare : ∀ {a : Set}, (a → a → int) → t a → t a → int;
equal : ∀ {a : Set}, (a → a → bool) → t a → t a → bool;
iter : ∀ {a : Set}, (key → a → unit) → t a → unit;
iter_e :
∀ {a trace : Set},
(key → a → Pervasives.result unit trace) → t a →
Pervasives.result unit trace;
iter_s : ∀ {a : Set}, (key → a → unit) → t a → unit;
iter_p : ∀ {a : Set}, (key → a → unit) → t a → unit;
iter_es :
∀ {a trace : Set},
(key → a → Pervasives.result unit trace) → t a →
Pervasives.result unit trace;
fold : ∀ {a b : Set}, (key → a → b → b) → t a → b → b;
fold_e :
∀ {a b trace : Set},
(key → a → b → Pervasives.result b trace) → t a → b →
Pervasives.result b trace;
fold_s :
∀ {a b : Set}, (key → a → b → b) → t a → b → b;
fold_es :
∀ {a b trace : Set},
(key → a → b → Pervasives.result b trace) → t a → b →
Pervasives.result b trace;
for_all : ∀ {a : Set}, (key → a → bool) → t a → bool;
_exists : ∀ {a : Set}, (key → a → bool) → t a → bool;
filter : ∀ {a : Set}, (key → a → bool) → t a → t a;
filter_map : ∀ {a b : Set}, (key → a → option b) → t a → t b;
partition : ∀ {a : Set}, (key → a → bool) → t a → t a × t a;
cardinal : ∀ {a : Set}, t a → int;
bindings : ∀ {a : Set}, t a → list (key × a);
min_binding : ∀ {a : Set}, t a → option (key × a);
min_binding_opt : ∀ {a : Set}, t a → option (key × a);
max_binding : ∀ {a : Set}, t a → option (key × a);
max_binding_opt : ∀ {a : Set}, t a → option (key × a);
choose : ∀ {a : Set}, t a → option (key × a);
choose_opt : ∀ {a : Set}, t a → option (key × a);
split : ∀ {a : Set}, key → t a → t a × option a × t a;
find : ∀ {a : Set}, key → t a → option a;
find_opt : ∀ {a : Set}, key → t a → option a;
find_first : ∀ {a : Set}, (key → bool) → t a → option (key × a);
find_first_opt : ∀ {a : Set}, (key → bool) → t a → option (key × a);
find_last : ∀ {a : Set}, (key → bool) → t a → option (key × a);
find_last_opt : ∀ {a : Set}, (key → bool) → t a → option (key × a);
map : ∀ {a b : Set}, (a → b) → t a → t b;
mapi : ∀ {a b : Set}, (key → a → b) → t a → t b;
to_seq : ∀ {a : Set}, t a → Seq.t (key × a);
to_rev_seq : ∀ {a : Set}, t a → Seq.t (key × a);
to_seq_from : ∀ {a : Set}, key → t a → Seq.t (key × a);
add_seq : ∀ {a : Set}, Seq.t (key × a) → t a → t a;
of_seq : ∀ {a : Set}, Seq.t (key × a) → t a;
iter_ep :
∀ {a _error: Set},
(key → a → Pervasives.result unit (Error_monad.trace _error)) →
t a →
Pervasives.result unit (Error_monad.trace _error);
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
We define a simple version of maps, using sorted lists.
Module Make.
Class FArgs {t : Set} := {
Ord : Compare.COMPARABLE (t := t);
}.
Arguments Build_FArgs {_}.
Definition key `{FArgs} : Set := Ord.(Compare.COMPARABLE.t).
Definition t `{FArgs} (a : Set) : Set := list (key × a).
Definition compare_keys `{FArgs} (k1 k2 : key) : comparison :=
let z := Ord.(Compare.COMPARABLE.compare) k1 k2 in
if Z.eqb z 0 then
Eq
else if Z.leb z 0 then
Lt
else
Gt.
Definition empty `{FArgs} {a : Set} : t a :=
[].
Definition is_empty `{FArgs} {a : Set} (m : t a) : bool :=
match m with
| [] ⇒ true
| _ :: _ ⇒ false
end.
Fixpoint mem `{FArgs} {a : Set} (k : key) (m : t a) : bool :=
match m with
| [] ⇒ false
| (k', _) :: m ⇒
match compare_keys k k' with
| Lt ⇒ false
| Eq ⇒ true
| Gt ⇒ mem k m
end
end.
Fixpoint find `{FArgs} {a : Set} (k : key) (m : t a) : option a :=
match m with
| [] ⇒ None
| (k', v') :: m' ⇒
match compare_keys k k' with
| Lt ⇒ None
| Eq ⇒ Some v'
| Gt ⇒ find k m'
end
end.
Fixpoint add `{FArgs} {a : Set} (k : key) (v : a) (m : t a) : t a :=
match m with
| [] ⇒ [(k, v)]
| (k', v') :: m' ⇒
match compare_keys k k' with
| Gt ⇒ (k', v') :: add k v m'
| Eq ⇒ (k, v) :: m'
| Lt ⇒ (k, v) :: m
end
end.
Fixpoint remove `{FArgs} {a : Set} (k : key) (m : t a) : t a :=
match m with
| [] ⇒ m
| (k', v') :: m' ⇒
match compare_keys k k' with
| Lt ⇒ m
| Eq ⇒ m'
| Gt ⇒ (k', v') :: remove k m'
end
end.
Definition update `{FArgs} {a : Set} (k : key) (f : option a → option a)
(m : t a) : t a :=
match f (find k m) with
| None ⇒ remove k m
| Some v' ⇒ add k v' m
end.
Definition singleton `{FArgs} {a : Set} (k : key) (v : a) : t a :=
[(k, v)].
Fixpoint pick_opt `{FArgs} {a : Set} (k : key) (m : t a) : option a × t a :=
match m with
| [] ⇒ (None, m)
| (k', v') :: m' ⇒
match compare_keys k k' with
| Lt ⇒ (None, m)
| Eq ⇒ (Some v', m')
| Gt ⇒
let '(v, m') := pick_opt k m' in
(v, (k', v') :: m')
end
end.
Fixpoint merge `{FArgs} {a b c : Set}
(f : key → option a → option b → option c) (m1 : t a) (m2 : t b) : t c :=
match m1 with
| [] ⇒
List.filter_map
(fun '(k2, v2) ⇒
match f k2 None (Some v2) with
| None ⇒ None
| Some v ⇒ Some (k2, v)
end
)
m2
| (k1, v1) :: m1 ⇒
let '(v2, m2) := pick_opt k1 m2 in
let m := merge f m1 m2 in
match f k1 (Some v1) v2 with
| None ⇒ m
| Some v ⇒ add k1 v m
end
end.
Definition union `{FArgs} {a : Set} (f : key → a → a → option a)
(m1 m2 : t a) : t a :=
merge
(fun k v1 v2 ⇒
match v1, v2 with
| None, None ⇒ None
| Some v1, None ⇒ Some v1
| None, Some v2 ⇒ Some v2
| Some v1, Some v2 ⇒ f k v1 v2
end
)
m1 m2.
Fixpoint compare `{FArgs} {a : Set} (f : a → a → int) (m1 m2 : t a) : int :=
match m1, m2 with
| [], [] ⇒ 0
| _ :: _, [] ⇒ 1
| [], _ :: _ ⇒ -1
| (k1, v1) :: m1, (k2, v2) :: m2 ⇒
match compare_keys k1 k2 with
| Lt ⇒ -1
| Eq ⇒
let compare_values := f v1 v2 in
if Z.eqb compare_values 0 then
compare f m1 m2
else
compare_values
| Gt ⇒ 1
end
end.
Fixpoint equal `{FArgs} {a : Set} (f : a → a → bool) (m1 m2 : t a) : bool :=
match m1, m2 with
| [], [] ⇒ true
| _ :: _, [] | [], _ :: _ ⇒ false
| (k1, v1) :: m1, (k2, v2) :: m2 ⇒
match compare_keys k1 k2 with
| Eq ⇒
if f v1 v2 then
equal f m1 m2
else
false
| _ ⇒ false
end
end.
Fixpoint iter `{FArgs} {a : Set} (f : key → a → unit) (m : t a) : unit :=
match m with
| [] ⇒ tt
| (k, v) :: m ⇒
let _ : unit := f k v in
iter f m
end.
Parameter iter_e :
∀ `{FArgs} {a trace : Set},
(key → a → Pervasives.result unit trace) → t a →
Pervasives.result unit trace.
Parameter iter_s : ∀ `{FArgs} {a : Set},
(key → a → unit) → t a → unit.
Parameter iter_p : ∀ `{FArgs} {a : Set},
(key → a → unit) → t a → unit.
Parameter iter_es : ∀ `{FArgs} {a trace : Set},
(key → a → Pervasives.result unit trace) → t a →
Pervasives.result unit trace.
Definition fold `{FArgs} {a b : Set} (f : key → a → b → b) (m : t a)
(acc : b) : b :=
List.fold_left (fun acc '(k, v) ⇒ f k v acc) acc m.
Definition fold_e `{FArgs} {a b trace : Set}
(f : key → a → b → Pervasives.result b trace) (m : t a) (acc : b) :
Pervasives.result b trace :=
fold (fun k v acc ⇒ let? acc := acc in f k v acc) m (return? acc).
Definition fold_s :
∀ `{FArgs} {a b : Set},
(key → a → b → b) → t a → b → b :=
@fold.
Definition fold_es :
∀ `{FArgs} {a b trace : Set},
(key → a → b → Pervasives.result b trace) →
t a → b →
Pervasives.result b trace :=
@fold_e.
Fixpoint for_all `{FArgs} {a : Set} (p : key → a → bool) (m : t a) : bool :=
match m with
| [] ⇒ true
| (k, v) :: m ⇒ p k v && for_all p m
end.
Fixpoint _exists `{FArgs} {a : Set} (p : key → a → bool) (m : t a) : bool :=
match m with
| [] ⇒ false
| (k, v) :: m ⇒ p k v || _exists p m
end.
Fixpoint filter `{FArgs} {a : Set} (p : key → a → bool) (m : t a) : t a :=
match m with
| [] ⇒ m
| (k, v) :: m ⇒
let m := filter p m in
if p k v then
(k, v) :: m
else
m
end.
Fixpoint partition `{FArgs} {a : Set} (p : key → a → bool) (m : t a)
: t a × t a :=
match m with
| [] ⇒ ([], [])
| (k, v) :: m ⇒
let '(m_true, m_false) := partition p m in
if p k v then
((k, v) :: m_true, m_false)
else
(m_true, (k, v) :: m_false)
end.
Definition cardinal `{FArgs} {a : Set} (m : t a) : int :=
List.length m.
Definition bindings `{FArgs} {a : Set} (m : t a) : list (key × a) :=
m.
Definition min_binding `{FArgs} {a : Set} (m : t a) : option (key × a) :=
match m with
| [] ⇒ None
| binding :: _ ⇒ Some binding
end.
Fixpoint max_binding `{FArgs} {a : Set} (m : t a) : option (key × a) :=
match m with
| [] ⇒ None
| [binding] ⇒ Some binding
| _ :: (_ :: _) as m ⇒ max_binding m
end.
Definition choose : ∀ `{FArgs} {a : Set}, t a → option (key × a) :=
@min_binding.
Fixpoint split `{FArgs} {a : Set} (k : key) (m : t a)
: t a × option a × t a :=
match m with
| [] ⇒ ([], None, [])
| (k', v') :: m' ⇒
match compare_keys k k' with
| Lt ⇒ ([], None, m)
| Eq ⇒ ([], Some v', m')
| Gt ⇒
let '(m_lt, v, m_gt) := split k m' in
((k', v') :: m_lt, v, m_gt)
end
end.
Fixpoint find_first `{FArgs} {a : Set} (p : key → bool) (m : t a)
: option (key × a) :=
match m with
| [] ⇒ None
| (k, v) :: m ⇒
if p k then
Some (k, v)
else
find_first p m
end.
Fixpoint find_last `{FArgs} {a : Set} (p : key → bool) (m : t a)
: option (key × a) :=
match m with
| [] ⇒ None
| (k, v) :: m ⇒
match find_last p m with
| None ⇒
if p k then
Some (k, v)
else
None
| Some _ as result ⇒ result
end
end.
Fixpoint map `{FArgs} {a b : Set} (f : a → b) (m : t a) : t b :=
match m with
| [] ⇒ []
| (k, v) :: m ⇒ (k, f v) :: map f m
end.
Fixpoint mapi `{FArgs} {a b : Set} (f : key → a → b) (m : t a) : t b :=
match m with
| [] ⇒ []
| (k, v) :: m ⇒ (k, f k v) :: mapi f m
end.
Parameter to_seq : ∀ `{FArgs} {a : Set},
t a → Seq.t (key × a).
Parameter to_seq_from : ∀ `{FArgs} {a : Set},
key → t a → Seq.t (key × a).
Fixpoint add_seq_node `{FArgs} {a : Set} (s : Seq.node (key × a))
(m : t a) : t a :=
match s with
| Seq.Nil ⇒ m
| Seq.Cons (k, v) s' ⇒
let m' := add k v m in
add_seq_node (s' tt) m'
end.
Definition add_seq `{FArgs} {a : Set} (s : Seq.t (key × a))
(m : t a) : t a :=
add_seq_node (s tt) m.
Fixpoint of_seq_node `{FArgs} {a : Set}
(s : Seq.node (key × a)) : t a :=
match s with
| Seq.Nil ⇒ []
| Seq.Cons (k, v) s' ⇒ (k, v) :: of_seq_node (s' tt)
end.
Definition of_seq `{FArgs} {a : Set}
(s : Seq.t (key × a)) : t a := of_seq_node (s tt).
Parameter iter_ep : ∀ `{FArgs} {a _error : Set},
(key → a → Pervasives.result unit (Error_monad.trace _error)) →
t a →
Pervasives.result unit (Error_monad.trace _error).
Definition functor `(FArgs) :=
{|
S.empty _ := empty;
S.is_empty _ := is_empty;
S.mem _ := mem;
S.add _ := add;
S.update _ := update;
S.singleton _ := singleton;
S.remove _ := remove;
S.merge _ _ _:= merge;
S.union _ := union;
S.compare _ := compare;
S.equal _ := equal;
S.iter _ := iter;
S.iter_e _ _ := iter_e;
S.iter_s _ := iter_s;
S.iter_p _ := iter_p;
S.iter_es _ _ := iter_es;
S.fold _ _ := fold;
S.fold_e _ _ _ := fold_e;
S.fold_s _ _ := fold_s;
S.fold_es _ _ _ := fold_es;
S.for_all _ := for_all;
S._exists _ := _exists;
S.filter _ := filter;
S.filter_map _ _ := axiom;
S.partition _ := partition;
S.cardinal _ := cardinal;
S.bindings _ := bindings;
S.min_binding _ := min_binding;
S.min_binding_opt _ := min_binding;
S.max_binding _ := max_binding;
S.max_binding_opt _ := max_binding;
S.choose _ := choose;
S.choose_opt _ := choose;
S.split _ := split;
S.find _ := find;
S.find_opt _ := find;
S.find_first _ := find_first;
S.find_first_opt _ := find_first;
S.find_last _ := find_last;
S.find_last_opt _ := find_last;
S.map _ _ := map;
S.mapi _ _ := mapi;
S.to_seq _ := to_seq;
S.to_rev_seq _ := axiom;
S.to_seq_from _ := to_seq_from;
S.add_seq _ := add_seq;
S.of_seq _ := of_seq;
S.iter_ep _ _ := iter_ep;
|}.
End Make.
Definition Make_t {Ord_t : Set} (Ord : Compare.COMPARABLE (t := Ord_t)) :
Set → Set :=
let '_ := Make.Build_FArgs Ord in
Make.t.
Definition Make {Ord_t : Set}
(Ord : Compare.COMPARABLE (t := Ord_t))
: S (key := Ord.(Compare.COMPARABLE.t)) (t := Make_t Ord) :=
Make.functor (Make.Build_FArgs Ord).
#[global] Opaque Make.
Class FArgs {t : Set} := {
Ord : Compare.COMPARABLE (t := t);
}.
Arguments Build_FArgs {_}.
Definition key `{FArgs} : Set := Ord.(Compare.COMPARABLE.t).
Definition t `{FArgs} (a : Set) : Set := list (key × a).
Definition compare_keys `{FArgs} (k1 k2 : key) : comparison :=
let z := Ord.(Compare.COMPARABLE.compare) k1 k2 in
if Z.eqb z 0 then
Eq
else if Z.leb z 0 then
Lt
else
Gt.
Definition empty `{FArgs} {a : Set} : t a :=
[].
Definition is_empty `{FArgs} {a : Set} (m : t a) : bool :=
match m with
| [] ⇒ true
| _ :: _ ⇒ false
end.
Fixpoint mem `{FArgs} {a : Set} (k : key) (m : t a) : bool :=
match m with
| [] ⇒ false
| (k', _) :: m ⇒
match compare_keys k k' with
| Lt ⇒ false
| Eq ⇒ true
| Gt ⇒ mem k m
end
end.
Fixpoint find `{FArgs} {a : Set} (k : key) (m : t a) : option a :=
match m with
| [] ⇒ None
| (k', v') :: m' ⇒
match compare_keys k k' with
| Lt ⇒ None
| Eq ⇒ Some v'
| Gt ⇒ find k m'
end
end.
Fixpoint add `{FArgs} {a : Set} (k : key) (v : a) (m : t a) : t a :=
match m with
| [] ⇒ [(k, v)]
| (k', v') :: m' ⇒
match compare_keys k k' with
| Gt ⇒ (k', v') :: add k v m'
| Eq ⇒ (k, v) :: m'
| Lt ⇒ (k, v) :: m
end
end.
Fixpoint remove `{FArgs} {a : Set} (k : key) (m : t a) : t a :=
match m with
| [] ⇒ m
| (k', v') :: m' ⇒
match compare_keys k k' with
| Lt ⇒ m
| Eq ⇒ m'
| Gt ⇒ (k', v') :: remove k m'
end
end.
Definition update `{FArgs} {a : Set} (k : key) (f : option a → option a)
(m : t a) : t a :=
match f (find k m) with
| None ⇒ remove k m
| Some v' ⇒ add k v' m
end.
Definition singleton `{FArgs} {a : Set} (k : key) (v : a) : t a :=
[(k, v)].
Fixpoint pick_opt `{FArgs} {a : Set} (k : key) (m : t a) : option a × t a :=
match m with
| [] ⇒ (None, m)
| (k', v') :: m' ⇒
match compare_keys k k' with
| Lt ⇒ (None, m)
| Eq ⇒ (Some v', m')
| Gt ⇒
let '(v, m') := pick_opt k m' in
(v, (k', v') :: m')
end
end.
Fixpoint merge `{FArgs} {a b c : Set}
(f : key → option a → option b → option c) (m1 : t a) (m2 : t b) : t c :=
match m1 with
| [] ⇒
List.filter_map
(fun '(k2, v2) ⇒
match f k2 None (Some v2) with
| None ⇒ None
| Some v ⇒ Some (k2, v)
end
)
m2
| (k1, v1) :: m1 ⇒
let '(v2, m2) := pick_opt k1 m2 in
let m := merge f m1 m2 in
match f k1 (Some v1) v2 with
| None ⇒ m
| Some v ⇒ add k1 v m
end
end.
Definition union `{FArgs} {a : Set} (f : key → a → a → option a)
(m1 m2 : t a) : t a :=
merge
(fun k v1 v2 ⇒
match v1, v2 with
| None, None ⇒ None
| Some v1, None ⇒ Some v1
| None, Some v2 ⇒ Some v2
| Some v1, Some v2 ⇒ f k v1 v2
end
)
m1 m2.
Fixpoint compare `{FArgs} {a : Set} (f : a → a → int) (m1 m2 : t a) : int :=
match m1, m2 with
| [], [] ⇒ 0
| _ :: _, [] ⇒ 1
| [], _ :: _ ⇒ -1
| (k1, v1) :: m1, (k2, v2) :: m2 ⇒
match compare_keys k1 k2 with
| Lt ⇒ -1
| Eq ⇒
let compare_values := f v1 v2 in
if Z.eqb compare_values 0 then
compare f m1 m2
else
compare_values
| Gt ⇒ 1
end
end.
Fixpoint equal `{FArgs} {a : Set} (f : a → a → bool) (m1 m2 : t a) : bool :=
match m1, m2 with
| [], [] ⇒ true
| _ :: _, [] | [], _ :: _ ⇒ false
| (k1, v1) :: m1, (k2, v2) :: m2 ⇒
match compare_keys k1 k2 with
| Eq ⇒
if f v1 v2 then
equal f m1 m2
else
false
| _ ⇒ false
end
end.
Fixpoint iter `{FArgs} {a : Set} (f : key → a → unit) (m : t a) : unit :=
match m with
| [] ⇒ tt
| (k, v) :: m ⇒
let _ : unit := f k v in
iter f m
end.
Parameter iter_e :
∀ `{FArgs} {a trace : Set},
(key → a → Pervasives.result unit trace) → t a →
Pervasives.result unit trace.
Parameter iter_s : ∀ `{FArgs} {a : Set},
(key → a → unit) → t a → unit.
Parameter iter_p : ∀ `{FArgs} {a : Set},
(key → a → unit) → t a → unit.
Parameter iter_es : ∀ `{FArgs} {a trace : Set},
(key → a → Pervasives.result unit trace) → t a →
Pervasives.result unit trace.
Definition fold `{FArgs} {a b : Set} (f : key → a → b → b) (m : t a)
(acc : b) : b :=
List.fold_left (fun acc '(k, v) ⇒ f k v acc) acc m.
Definition fold_e `{FArgs} {a b trace : Set}
(f : key → a → b → Pervasives.result b trace) (m : t a) (acc : b) :
Pervasives.result b trace :=
fold (fun k v acc ⇒ let? acc := acc in f k v acc) m (return? acc).
Definition fold_s :
∀ `{FArgs} {a b : Set},
(key → a → b → b) → t a → b → b :=
@fold.
Definition fold_es :
∀ `{FArgs} {a b trace : Set},
(key → a → b → Pervasives.result b trace) →
t a → b →
Pervasives.result b trace :=
@fold_e.
Fixpoint for_all `{FArgs} {a : Set} (p : key → a → bool) (m : t a) : bool :=
match m with
| [] ⇒ true
| (k, v) :: m ⇒ p k v && for_all p m
end.
Fixpoint _exists `{FArgs} {a : Set} (p : key → a → bool) (m : t a) : bool :=
match m with
| [] ⇒ false
| (k, v) :: m ⇒ p k v || _exists p m
end.
Fixpoint filter `{FArgs} {a : Set} (p : key → a → bool) (m : t a) : t a :=
match m with
| [] ⇒ m
| (k, v) :: m ⇒
let m := filter p m in
if p k v then
(k, v) :: m
else
m
end.
Fixpoint partition `{FArgs} {a : Set} (p : key → a → bool) (m : t a)
: t a × t a :=
match m with
| [] ⇒ ([], [])
| (k, v) :: m ⇒
let '(m_true, m_false) := partition p m in
if p k v then
((k, v) :: m_true, m_false)
else
(m_true, (k, v) :: m_false)
end.
Definition cardinal `{FArgs} {a : Set} (m : t a) : int :=
List.length m.
Definition bindings `{FArgs} {a : Set} (m : t a) : list (key × a) :=
m.
Definition min_binding `{FArgs} {a : Set} (m : t a) : option (key × a) :=
match m with
| [] ⇒ None
| binding :: _ ⇒ Some binding
end.
Fixpoint max_binding `{FArgs} {a : Set} (m : t a) : option (key × a) :=
match m with
| [] ⇒ None
| [binding] ⇒ Some binding
| _ :: (_ :: _) as m ⇒ max_binding m
end.
Definition choose : ∀ `{FArgs} {a : Set}, t a → option (key × a) :=
@min_binding.
Fixpoint split `{FArgs} {a : Set} (k : key) (m : t a)
: t a × option a × t a :=
match m with
| [] ⇒ ([], None, [])
| (k', v') :: m' ⇒
match compare_keys k k' with
| Lt ⇒ ([], None, m)
| Eq ⇒ ([], Some v', m')
| Gt ⇒
let '(m_lt, v, m_gt) := split k m' in
((k', v') :: m_lt, v, m_gt)
end
end.
Fixpoint find_first `{FArgs} {a : Set} (p : key → bool) (m : t a)
: option (key × a) :=
match m with
| [] ⇒ None
| (k, v) :: m ⇒
if p k then
Some (k, v)
else
find_first p m
end.
Fixpoint find_last `{FArgs} {a : Set} (p : key → bool) (m : t a)
: option (key × a) :=
match m with
| [] ⇒ None
| (k, v) :: m ⇒
match find_last p m with
| None ⇒
if p k then
Some (k, v)
else
None
| Some _ as result ⇒ result
end
end.
Fixpoint map `{FArgs} {a b : Set} (f : a → b) (m : t a) : t b :=
match m with
| [] ⇒ []
| (k, v) :: m ⇒ (k, f v) :: map f m
end.
Fixpoint mapi `{FArgs} {a b : Set} (f : key → a → b) (m : t a) : t b :=
match m with
| [] ⇒ []
| (k, v) :: m ⇒ (k, f k v) :: mapi f m
end.
Parameter to_seq : ∀ `{FArgs} {a : Set},
t a → Seq.t (key × a).
Parameter to_seq_from : ∀ `{FArgs} {a : Set},
key → t a → Seq.t (key × a).
Fixpoint add_seq_node `{FArgs} {a : Set} (s : Seq.node (key × a))
(m : t a) : t a :=
match s with
| Seq.Nil ⇒ m
| Seq.Cons (k, v) s' ⇒
let m' := add k v m in
add_seq_node (s' tt) m'
end.
Definition add_seq `{FArgs} {a : Set} (s : Seq.t (key × a))
(m : t a) : t a :=
add_seq_node (s tt) m.
Fixpoint of_seq_node `{FArgs} {a : Set}
(s : Seq.node (key × a)) : t a :=
match s with
| Seq.Nil ⇒ []
| Seq.Cons (k, v) s' ⇒ (k, v) :: of_seq_node (s' tt)
end.
Definition of_seq `{FArgs} {a : Set}
(s : Seq.t (key × a)) : t a := of_seq_node (s tt).
Parameter iter_ep : ∀ `{FArgs} {a _error : Set},
(key → a → Pervasives.result unit (Error_monad.trace _error)) →
t a →
Pervasives.result unit (Error_monad.trace _error).
Definition functor `(FArgs) :=
{|
S.empty _ := empty;
S.is_empty _ := is_empty;
S.mem _ := mem;
S.add _ := add;
S.update _ := update;
S.singleton _ := singleton;
S.remove _ := remove;
S.merge _ _ _:= merge;
S.union _ := union;
S.compare _ := compare;
S.equal _ := equal;
S.iter _ := iter;
S.iter_e _ _ := iter_e;
S.iter_s _ := iter_s;
S.iter_p _ := iter_p;
S.iter_es _ _ := iter_es;
S.fold _ _ := fold;
S.fold_e _ _ _ := fold_e;
S.fold_s _ _ := fold_s;
S.fold_es _ _ _ := fold_es;
S.for_all _ := for_all;
S._exists _ := _exists;
S.filter _ := filter;
S.filter_map _ _ := axiom;
S.partition _ := partition;
S.cardinal _ := cardinal;
S.bindings _ := bindings;
S.min_binding _ := min_binding;
S.min_binding_opt _ := min_binding;
S.max_binding _ := max_binding;
S.max_binding_opt _ := max_binding;
S.choose _ := choose;
S.choose_opt _ := choose;
S.split _ := split;
S.find _ := find;
S.find_opt _ := find;
S.find_first _ := find_first;
S.find_first_opt _ := find_first;
S.find_last _ := find_last;
S.find_last_opt _ := find_last;
S.map _ _ := map;
S.mapi _ _ := mapi;
S.to_seq _ := to_seq;
S.to_rev_seq _ := axiom;
S.to_seq_from _ := to_seq_from;
S.add_seq _ := add_seq;
S.of_seq _ := of_seq;
S.iter_ep _ _ := iter_ep;
|}.
End Make.
Definition Make_t {Ord_t : Set} (Ord : Compare.COMPARABLE (t := Ord_t)) :
Set → Set :=
let '_ := Make.Build_FArgs Ord in
Make.t.
Definition Make {Ord_t : Set}
(Ord : Compare.COMPARABLE (t := Ord_t))
: S (key := Ord.(Compare.COMPARABLE.t)) (t := Make_t Ord) :=
Make.functor (Make.Build_FArgs Ord).
#[global] Opaque Make.