Library FingerTree.FingerTree
Une interface non dépendante
Comme décrit précédemment, on peut agréger la mesure et le fingertree dans une paire dépendante pour donner une interface simplifiée aux dépendants.
Section FingerTree.
Context `(ma : Measured v A).
Definition FingerTree := { m : v & fingertree v A m }.
Notation " ts :| t " := (existT _ ts t) (at level 20).
Cela nous donne un type FingerTree v {mono} A {ma}, qu'on peut comparer au type
original dans . On a ajouté l'implémentation monoid et la
fonction de mesure ma comme paramètres explicites alors qu'en ils sont passés
implicitement à l'aide des classes de type à chaque fonction les manipulant.
On ne décrit pas le "repackaging" en détail, il s'agit just de décomposer un objet de type
FingerTree, appeler la fonction appropriée sur les fingertree et recomposer la paire dépendante.
En revanche un point important est que l'on peut exporter les vues sur les fingertree et retrouver
la mesure associée:
Program Definition tree_size (s : FingerTree) : nat :=
let '_ :| t := s in tree_size t.
Inductive left_view : Type :=
| nil_left : left_view | cons_left : A -> FingerTree -> left_view.
Lemma view_left_size : forall t x t', view_left t = cons_left x t' ->
tree_size t' < tree_size t.
Proof.
intros.
destruct t ; destruct t' ; simpl in *.
generalize H ; clear H.
remember (view_L f) as vf.
destruct vf ; simpl in * ; intros ; try discriminate.
symmetry in Heqvf.
pose (view_L_size_measure f Heqvf).
inversion H.
subst.
assert(Hi:=inj_pairT2 H3).
subst f0.
simpl.
omega.
Qed.
On peut aussi refaire le découpage par rapport à un prédicat sur les FingerTree.
On offre la même interface simplement typée qu'en en définissant la
fonction split_with p x. Cette fonction découpe n'importe quel arbre en regardant
tout d'abord s'il est vide et sinon en appelant la fonction fortement spécifiée split
avec un accumulateur vide ε. On crée alors une paire avec l'arbre à gauche et l'arbre droit
auquel on ajoute l'élément qui fait changer le prédicat de valeur. On oublie complètement
les propriétés données par la fonction split sur le résultat.
Program Definition split_with (p : v -> bool)
(x : FingerTree) : FingerTree * FingerTree :=
if is_empty_dec x then (empty, empty)
else let (l, x, r) := split p ε x in (l, cons x r).
End FingerTree.