- Inductive TreeFlags {T:Type} : Tree T -> Type :=
- | tf_leaf_true : forall x, TreeFlags (T_Leaf x)
- | tf_leaf_false : forall x, TreeFlags (T_Leaf x)
- | tf_branch : forall b1 b2, TreeFlags b1 -> TreeFlags b2 -> TreeFlags (b1,,b2).
-
- Fixpoint mkFlags {T}(f:T -> bool)(t:Tree T) : TreeFlags t :=
- match t as T return TreeFlags T with
- | T_Leaf x => if f x then tf_leaf_true x else tf_leaf_false x
- | T_Branch b1 b2 => tf_branch _ _ (mkFlags f b1) (mkFlags f b2)
- end.
-
- (* take and drop are not exact inverses *)
-
- (* drop replaces each leaf where the flag is set with a [] *)
- Fixpoint drop {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
- match tf with
- | tf_leaf_true x => []
- | tf_leaf_false x => Σ
- | tf_branch b1 b2 tb1 tb2 => (drop tb1),,(drop tb2)
- end.
-
- (* take returns only those leaves for which the flag is set; all others are omitted entirely from the tree *)
- Fixpoint take {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
- match tf with
- | tf_leaf_true x => Some Σ
- | tf_leaf_false x => None
- | tf_branch b1 b2 tb1 tb2 =>
- match take tb1 with
- | None => take tb2
- | Some b1' => match take tb2 with
- | None => Some b1'
- | Some b2' => Some (b1',,b2')
- end
- end
- end.
-
- Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
- match t with
- | None => []
- | Some x => x
- end.
-
- Definition setNone {T}(b:bool)(f:T -> bool) : ??T -> bool :=
- fun t =>
- match t with
- | None => b
- | Some x => f x
- end.
-
- (* "Arrange" objects are parametric in the type of the leaves of the tree *)
- Definition arrangeMap :
- forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
- Arrange Σ₁ Σ₂ ->
- Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
- intros.
- induction X; simpl.
- apply RCanL.
- apply RCanR.
- apply RuCanL.
- apply RuCanR.
- apply RAssoc.
- apply RCossa.
- apply RExch.
- apply RWeak.
- apply RCont.
- apply RLeft; auto.
- apply RRight; auto.
- eapply RComp; [ apply IHX1 | apply IHX2 ].
- Defined.
-
- Definition bnot (b:bool) : bool := if b then false else true.
-
- Definition swapMiddle {T} (a b c d:Tree ??T) :
- Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
- eapply RComp.
- apply RCossa.
- eapply RComp.
- eapply RLeft.
- eapply RComp.
- eapply RAssoc.
- eapply RRight.
- apply RExch.
- eapply RComp.
- eapply RLeft.
- eapply RCossa.
- eapply RAssoc.
- Defined.
-