Add Maps and HTL.v

1 files changed, 49 insertions, 0 deletions

diff --git a/src/common/Maps.v b/src/common/Maps.v
new file mode 100644
index 0000000..7a542b7
--- /dev/null
+++ b/src/common/Maps.v
@@ -0,0 +1,49 @@
+From coqup Require Import Coquplib.
+
+From compcert Require Export Maps.
+From compcert Require Import Errors.
+Import PTree.
+
+Set Implicit Arguments.
+
+Local Open Scope error_monad_scope.
+
+(** Instance of traverse for [PTree] and [Errors]. This should maybe be generalised
+    in the future. *)
+
+Module PTree.
+
+Fixpoint xtraverse (A B : Type) (f : positive -> A -> res B) (m : PTree.t A) (i : positive)
+         {struct m} : res (PTree.t B) :=
+  match m with
+  | Leaf => OK Leaf
+  | Node l o r =>
+    let newo :=
+        match o with
+        | None => OK None
+        | Some x =>
+          match f (prev i) x with
+          | Error err => Error err
+          | OK val => OK (Some val)
+          end
+        end in
+    match newo with
+    | OK no =>
+      do nl <- xtraverse f l (xO i);
+      do nr <- xtraverse f r (xI i);
+      OK (Node nl no nr)
+    | Error msg => Error msg
+    end
+  end.
+
+Definition traverse (A B : Type) (f : positive -> A -> res B) m := xtraverse f m xH.
+
+Definition traverse1 (A B : Type) (f : A -> res B) := traverse (fun _ => f).
+
+Lemma traverse1_inversion:
+  forall (A B : Type) (f : A -> res B) (i j : positive) (m : t A) (m' : t B),
+    traverse1 f m = OK m' ->
+    list_forall2 (fun x y => f (snd x) = OK (snd y) /\ fst x = fst y) (elements m) (elements m').
+Proof. Admitted.
+
+End PTree.