🍃 _Set.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.Map.
Import Error_monad.Notations.
Module S.
Record signature {elt t : Set} : Set := {
elt := elt;
t := t;
empty : t;
is_empty : t → bool;
mem : elt → t → bool;
add : elt → t → t;
singleton : elt → t;
remove : elt → t → t;
union : t → t → t;
inter : t → t → t;
disjoint : t → t → bool;
diff_value : t → t → t;
compare : t → t → int;
equal : t → t → bool;
subset : t → t → bool;
iter : (elt → unit) → t → unit;
iter_e :
∀ {trace : Set},
(elt → Pervasives.result unit trace) → t →
Pervasives.result unit trace;
iter_s : (elt → unit) → t → unit;
iter_p : (elt → unit) → t → unit;
iter_es :
∀ {trace : Set},
(elt → Pervasives.result unit trace) → t →
Pervasives.result unit trace;
map : (elt → elt) → t → t;
fold : ∀ {a : Set}, (elt → a → a) → t → a → a;
fold_e :
∀ {a trace : Set},
(elt → a → Pervasives.result a trace) → t → a →
Pervasives.result a trace;
fold_s : ∀ {a : Set}, (elt → a → a) → t → a → a;
fold_es :
∀ {a trace : Set},
(elt → a → Pervasives.result a trace) → t → a →
Pervasives.result a trace;
for_all : (elt → bool) → t → bool;
_exists : (elt → bool) → t → bool;
filter : (elt → bool) → t → t;
filter_map : (elt → option elt) → t → t;
partition : (elt → bool) → t → t × t;
cardinal : t → int;
elements : t → list elt;
min_elt : t → option elt;
min_elt_opt : t → option elt;
max_elt : t → option elt;
max_elt_opt : t → option elt;
choose : t → option elt;
choose_opt : t → option elt;
split : elt → t → t × bool × t;
find : elt → t → option elt;
find_opt : elt → t → option elt;
find_first : (elt → bool) → t → option elt;
find_first_opt : (elt → bool) → t → option elt;
find_last : (elt → bool) → t → option elt;
find_last_opt : (elt → bool) → t → option elt;
of_list : list elt → t;
to_seq_from : elt → t → Seq.t elt;
to_seq : t → Seq.t elt;
to_rev_seq : t → Seq.t elt;
add_seq : Seq.t elt → t → t;
of_seq : Seq.t elt → t;
iter_ep : (elt → M? unit) → t → M? unit;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
Definition Make {Ord_t : Set}
(Ord : Compare.COMPARABLE (t := Ord_t)) :
S (elt := Ord.(Compare.COMPARABLE.t)) (t := (Map.Make Ord).(Map.S.t) unit) :=
let M := Map.Make Ord in
{|
S.empty := M.(Map.S.empty);
S.is_empty := M.(Map.S.is_empty);
S.mem := M.(Map.S.mem);
S.add e s := M.(Map.S.add) e tt s;
S.singleton e := M.(Map.S.singleton) e tt;
S.remove k s := M.(Map.S.remove) k s;
S.union := axiom "union";
S.inter := axiom "inter";
S.disjoint := axiom "disjoint";
S.diff_value := axiom "diff_value";
S.compare m1 m2 :=
let f _ _ := 0 in
M.(Map.S.compare) f m1 m2;
S.equal m1 m2 :=
let f _ _ := true in
M.(Map.S.equal) f m1 m2;
S.subset := axiom "subset";
S.iter f v :=
let f' k _ := f k in
M.(Map.S.iter) f' v;
S.iter_e _ f m :=
let f' k _ := f k in
M.(Map.S.iter_e) f' m;
S.iter_s f m :=
let f' k _ := f k in
M.(Map.S.iter_s) f' m;
S.iter_p f m :=
let f' k _ := f k in
M.(Map.S.iter_p) f' m;
S.iter_es _ f m :=
let f' k _ := f k in
M.(Map.S.iter_es) f' m;
S.map := axiom "map";
S.fold {a} f m (acc : a) :=
let f' k _ acc := f k acc in
M.(Map.S.fold) f' m acc;
S.fold_e {a} _ f m (acc : a) :=
let f' k _ acc := f k acc in
M.(Map.S.fold_e) f' m acc;
S.fold_s {a} f m (acc : a) :=
let f' k _ acc := f k acc in
M.(Map.S.fold_s) f' m acc;
S.fold_es {a} _ f m (acc : a) :=
let f' k _ acc := f k acc in
M.(Map.S.fold_es) f' m acc;
S.for_all f v :=
let f' k _ := f k in
M.(Map.S.for_all) f' v;
S._exists f v :=
let f' k _ := f k in
M.(Map.S._exists) f' v;
S.filter f v :=
let f' k _ := f k in
M.(Map.S.filter) f' v;
S.filter_map f v :=
let f' k _ := Some tt in
M.(Map.S.filter_map) f' v;
S.partition f v :=
let f' k _ := f k in
M.(Map.S.partition) f' v;
S.cardinal := M.(Map.S.cardinal);
S.elements m :=
List.map fst m;
S.min_elt m :=
match M.(Map.S.min_binding) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.min_elt_opt m :=
match M.(Map.S.min_binding_opt) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.max_elt m :=
match M.(Map.S.max_binding) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.max_elt_opt m :=
match M.(Map.S.max_binding_opt) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.choose m :=
match M.(Map.S.choose) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.choose_opt m :=
match M.(Map.S.choose) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.split k v :=
let '(l, e, r) := M.(Map.S.split) k v in
match e with
| None ⇒ (l, false, r)
| Some _ ⇒ (l, true, r)
end;
S.find := axiom "find";
S.find_opt := axiom "find_opt";
S.find_first := axiom "find_first";
S.find_first_opt := axiom "find_first_opt";
S.find_last := axiom "find_last";
S.find_last_opt := axiom "find_last_opt";
S.of_list := axiom "of_list";
S.to_seq_from := axiom "to_seq_from";
S.to_seq := axiom "to_seq";
S.to_rev_seq := axiom "to_rev_seq";
S.add_seq := axiom "add_seq";
S.of_seq := axiom "of_seq";
S.iter_ep := axiom "iter_ep";
|}.
Definition Make_t {Ord_t : Set} (Ord : Compare.COMPARABLE (t := Ord_t)) : Set :=
(Make Ord).(S.t).
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Compare.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.Map.
Import Error_monad.Notations.
Module S.
Record signature {elt t : Set} : Set := {
elt := elt;
t := t;
empty : t;
is_empty : t → bool;
mem : elt → t → bool;
add : elt → t → t;
singleton : elt → t;
remove : elt → t → t;
union : t → t → t;
inter : t → t → t;
disjoint : t → t → bool;
diff_value : t → t → t;
compare : t → t → int;
equal : t → t → bool;
subset : t → t → bool;
iter : (elt → unit) → t → unit;
iter_e :
∀ {trace : Set},
(elt → Pervasives.result unit trace) → t →
Pervasives.result unit trace;
iter_s : (elt → unit) → t → unit;
iter_p : (elt → unit) → t → unit;
iter_es :
∀ {trace : Set},
(elt → Pervasives.result unit trace) → t →
Pervasives.result unit trace;
map : (elt → elt) → t → t;
fold : ∀ {a : Set}, (elt → a → a) → t → a → a;
fold_e :
∀ {a trace : Set},
(elt → a → Pervasives.result a trace) → t → a →
Pervasives.result a trace;
fold_s : ∀ {a : Set}, (elt → a → a) → t → a → a;
fold_es :
∀ {a trace : Set},
(elt → a → Pervasives.result a trace) → t → a →
Pervasives.result a trace;
for_all : (elt → bool) → t → bool;
_exists : (elt → bool) → t → bool;
filter : (elt → bool) → t → t;
filter_map : (elt → option elt) → t → t;
partition : (elt → bool) → t → t × t;
cardinal : t → int;
elements : t → list elt;
min_elt : t → option elt;
min_elt_opt : t → option elt;
max_elt : t → option elt;
max_elt_opt : t → option elt;
choose : t → option elt;
choose_opt : t → option elt;
split : elt → t → t × bool × t;
find : elt → t → option elt;
find_opt : elt → t → option elt;
find_first : (elt → bool) → t → option elt;
find_first_opt : (elt → bool) → t → option elt;
find_last : (elt → bool) → t → option elt;
find_last_opt : (elt → bool) → t → option elt;
of_list : list elt → t;
to_seq_from : elt → t → Seq.t elt;
to_seq : t → Seq.t elt;
to_rev_seq : t → Seq.t elt;
add_seq : Seq.t elt → t → t;
of_seq : Seq.t elt → t;
iter_ep : (elt → M? unit) → t → M? unit;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
Definition Make {Ord_t : Set}
(Ord : Compare.COMPARABLE (t := Ord_t)) :
S (elt := Ord.(Compare.COMPARABLE.t)) (t := (Map.Make Ord).(Map.S.t) unit) :=
let M := Map.Make Ord in
{|
S.empty := M.(Map.S.empty);
S.is_empty := M.(Map.S.is_empty);
S.mem := M.(Map.S.mem);
S.add e s := M.(Map.S.add) e tt s;
S.singleton e := M.(Map.S.singleton) e tt;
S.remove k s := M.(Map.S.remove) k s;
S.union := axiom "union";
S.inter := axiom "inter";
S.disjoint := axiom "disjoint";
S.diff_value := axiom "diff_value";
S.compare m1 m2 :=
let f _ _ := 0 in
M.(Map.S.compare) f m1 m2;
S.equal m1 m2 :=
let f _ _ := true in
M.(Map.S.equal) f m1 m2;
S.subset := axiom "subset";
S.iter f v :=
let f' k _ := f k in
M.(Map.S.iter) f' v;
S.iter_e _ f m :=
let f' k _ := f k in
M.(Map.S.iter_e) f' m;
S.iter_s f m :=
let f' k _ := f k in
M.(Map.S.iter_s) f' m;
S.iter_p f m :=
let f' k _ := f k in
M.(Map.S.iter_p) f' m;
S.iter_es _ f m :=
let f' k _ := f k in
M.(Map.S.iter_es) f' m;
S.map := axiom "map";
S.fold {a} f m (acc : a) :=
let f' k _ acc := f k acc in
M.(Map.S.fold) f' m acc;
S.fold_e {a} _ f m (acc : a) :=
let f' k _ acc := f k acc in
M.(Map.S.fold_e) f' m acc;
S.fold_s {a} f m (acc : a) :=
let f' k _ acc := f k acc in
M.(Map.S.fold_s) f' m acc;
S.fold_es {a} _ f m (acc : a) :=
let f' k _ acc := f k acc in
M.(Map.S.fold_es) f' m acc;
S.for_all f v :=
let f' k _ := f k in
M.(Map.S.for_all) f' v;
S._exists f v :=
let f' k _ := f k in
M.(Map.S._exists) f' v;
S.filter f v :=
let f' k _ := f k in
M.(Map.S.filter) f' v;
S.filter_map f v :=
let f' k _ := Some tt in
M.(Map.S.filter_map) f' v;
S.partition f v :=
let f' k _ := f k in
M.(Map.S.partition) f' v;
S.cardinal := M.(Map.S.cardinal);
S.elements m :=
List.map fst m;
S.min_elt m :=
match M.(Map.S.min_binding) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.min_elt_opt m :=
match M.(Map.S.min_binding_opt) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.max_elt m :=
match M.(Map.S.max_binding) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.max_elt_opt m :=
match M.(Map.S.max_binding_opt) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.choose m :=
match M.(Map.S.choose) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.choose_opt m :=
match M.(Map.S.choose) m with
| None ⇒ None
| Some (k,_) ⇒ Some k
end;
S.split k v :=
let '(l, e, r) := M.(Map.S.split) k v in
match e with
| None ⇒ (l, false, r)
| Some _ ⇒ (l, true, r)
end;
S.find := axiom "find";
S.find_opt := axiom "find_opt";
S.find_first := axiom "find_first";
S.find_first_opt := axiom "find_first_opt";
S.find_last := axiom "find_last";
S.find_last_opt := axiom "find_last_opt";
S.of_list := axiom "of_list";
S.to_seq_from := axiom "to_seq_from";
S.to_seq := axiom "to_seq";
S.to_rev_seq := axiom "to_rev_seq";
S.add_seq := axiom "add_seq";
S.of_seq := axiom "of_seq";
S.iter_ep := axiom "iter_ep";
|}.
Definition Make_t {Ord_t : Set} (Ord : Compare.COMPARABLE (t := Ord_t)) : Set :=
(Make Ord).(S.t).