Skip to main content

🍃 FallbackArray.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Proto_alpha.Environment.List.

This module implements arrays equipped with accessors that cannot raise exceptions. Reading out of the bounds of the arrays return a fallback value fixed at array construction time, writing out of the bounds of the arrays is ignored.
The type for arrays containing values of type [a].
Module t.
  Record record {a : Set} : Set := Build {
    items : list a;
    default : a }.
  Arguments record : clear implicits.
End t.
Definition t := t.record.

Fixpoint mk_items {a : Set} (n : nat) (d : a) : list a :=
  match n with
  | Onil
  | S n'd :: (mk_items n' d)
  end.

[make len v] builds an array [a] initialized [len] cells with [v]. The value [v] is the fallback (default) value for [a].
Definition make {a : Set} (i : int) (d : a) : t a :=
  @t.Build a (mk_items (Z.to_nat i) d) d.

[of_list ~fallback ~proj l] builds a fallback array [a] of length [List.length l] where each cell [i] is initialized by [proj (List.nth l i)] and the fallback value is [fallback].
Definition of_list {a b : Set} (fallback : b) (f : a b) (ls : list a) : t b :=
  @t.Build b (Lists.List.map f ls) fallback.

[fallback] returns the fallback (default) value for [a].
Definition fallback {a : Set} (r : t a) : a :=
  r.(t.default).

Definition length {a : Set} (r : t a) : int :=
  List.length r.(t.items).

[get a idx] returns the contents of the cell of index [idx] in [a]. If idx < 0 or idx >= length a, get a idx = fallback a.
Definition get {a : Set} (r : t a) (numb : int) : a :=
  match List.nth r.(t.items) numb with
  | Some resres
  | Noner.(t.default)
  end.

set a idx value updates the cell of index idx with value. If idx < 0 or idx >= length a, a is unchanged.
Parameter set : {a : Set}, t a int a unit.

[iter f a] iterates [f] over the cells of [a] from the cell indexed 0 to the cell indexed [length a - 1].
Parameter iter : {a : Set}, (a unit) t a unit.

[map f a] computes a new array obtained by applying [f] to each cell contents of [a]. Notice that the fallback value of the new array is [f (fallback a)].
Definition map {a b : Set} (f : a b) (r : t a) : t b :=
  @t.Build b (Lists.List.map f r.(t.items)) (f (@fallback a r)).

[fold f a init] traverses [a] from the cell indexed [0] to the cell indexed [length a - 1] and transforms [accu] into [f accu x] where [x] is the content of the cell under focus. [accu] is [init] on the first iteration.
Definition fold {a b : Set} (f : b a b) (r : t a) (ini : b) : b :=
  Lists.List.fold_left f r.(t.items) ini.

Fixpoint fold_map_aux {a b c : Set} (f : b a b × c) (ls : list a)
         (accu : b) (ct : t c) : b × t c :=
  match ls with
  | [](accu, ct)
  | p :: ps ⇒ @fold_map_aux a b c f ps (fst (f accu p))
                 (@t.Build c ((snd (f accu p)) :: ct.(t.items)) ct.(t.default))
  end.

[fold_map f a init fallback] traverses [a] from the cell indexed [0] to the cell indexed [length a - 1] and transforms [accu] into [fst (f accu x)] where [x] is the content of the cell under focus. [accu] is [init] on the first iteration. The function also returns a fresh array containing [snd (f accu x)] for each [x]. [fallback] is required to initialize a fresh array before it can be filled. We use auxillary function [fold_map_aux] to use [t c] as accumulator
Definition fold_map {a b c : Set} (f : b a b × c) (r : t a)
          (init : b) (flbck : c) : b × t c :=
  let res := @t.Build c nil flbck in
  @fold_map_aux a b c f r.(t.items) init res.