Skip to main content

πŸƒΒ Map.v

Environment

Gitlab

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 {_ _}.

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.