Skip to main content

🍃 Map.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.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 :
       {_error a : Set},
      (key a Pervasives.result unit (list _error)) t a
      Pervasives.result unit (list _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
      | Ltfalse
      | Eqtrue
      | Gtmem 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
      | LtNone
      | EqSome v'
      | Gtfind 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
      | Ltm
      | Eqm'
      | 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
    | Noneremove 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
          | NoneNone
          | Some vSome (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
      | Nonem
      | Some vadd 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, NoneNone
        | Some v1, NoneSome v1
        | None, Some v2Some v2
        | Some v1, Some v2f 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.

  Fixpoint fold `{FArgs} {a b : Set} (f : key a b b) (m : t a)
    (acc : b) : b :=
    match m with
    | []acc
    | (k, v) :: m
      let acc := f k v acc in
      fold f m acc
    end.

  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 acclet? 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) :: mp 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) :: mp 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 mmax_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 resultresult
      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).

  Parameter add_seq : `{FArgs} {a : Set},
    Seq.t (key × a) t a t a.

  Parameter of_seq : `{FArgs} {a : Set},
    Seq.t (key × a) t a.

  Parameter iter_ep :
     `{FArgs} {_error a : Set},
    (key a Pervasives.result unit (list _error)) t a
    Pervasives.result unit (list _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)) :=
  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.