Skip to main content

🍃 _Set.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.Compare.
Require Proto_alpha.Environment.Error_monad.
Require Proto_alpha.Environment.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 := axiom "elements";
    S.min_elt m :=
      match M.(Map.S.min_binding) m with
      | NoneNone
      | Some (k,_)Some k
      end;
    S.min_elt_opt m :=
      match M.(Map.S.min_binding_opt) m with
      | NoneNone
      | Some (k,_)Some k
      end;
    S.max_elt m :=
      match M.(Map.S.max_binding) m with
      | NoneNone
      | Some (k,_)Some k
      end;
    S.max_elt_opt m :=
      match M.(Map.S.max_binding_opt) m with
      | NoneNone
      | Some (k,_)Some k
      end;
    S.choose m :=
      match M.(Map.S.choose) m with
      | NoneNone
      | Some (k,_)Some k
      end;
    S.choose_opt m :=
      match M.(Map.S.choose) m with
      | NoneNone
      | 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).