🍃 FallbackArray.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.List.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.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
| O ⇒ nil
| S n' ⇒ d :: (mk_items n' d)
end.
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
| O ⇒ nil
| 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].
[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.
@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).
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 res ⇒ res
| None ⇒ r.(t.default)
end.
match List.nth r.(t.items) numb with
| Some res ⇒ res
| None ⇒ r.(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.
[iter f a] iterates [f] over the cells of [a] from the cell indexed
0 to the cell indexed [length a - 1].
[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)).
@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.
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