1 files changed, 31 insertions, 1 deletions
diff --git a/src/common/Monad.v b/src/common/Monad.v
index fcbe527..1801a63 100644
--- a/src/common/Monad.v
+++ b/src/common/Monad.v
@@ -1,6 +1,7 @@
 (*
  * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *               2021 Michalis Pardalos <mpardalos@gmail.com>
  *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
@@ -16,7 +17,8 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From Coq Require Import Lists.List.
+From Coq Require Import BinNums Lists.List.
+From compcert Require Import Maps.
 
 Module Type Monad.
 
@@ -57,10 +59,38 @@ Module MonadExtra(M : Monad).
       ret (r::rs)
     end.
 
+  Definition sequence {A} : list (mon A) -> mon (list A) := traverselist (fun x => x).
+
+  Definition traverseoption {A B: Type} (f: A -> mon B) (opt: option A) : mon (option B) :=
+    match opt with
+    | None => ret None
+    | Some x =>
+      do r <- f x;
+      ret (Some r)
+    end.
+
   Fixpoint collectlist {A : Type} (f : A -> mon unit) (l : list A) {struct l} : mon unit :=
     match l with
     | nil => ret tt
     | x::xs => do _ <- f x; collectlist f xs
     end.
 
+Fixpoint xtraverse_ptree {A B : Type} (f : positive -> A -> mon B) (m : PTree.t A) (i : positive)
+         {struct m} : mon (PTree.t B) :=
+  match m with
+  | PTree.Leaf => ret PTree.Leaf
+  | PTree.Node l o r =>
+    do no <- match o with
+        | None => ret None
+        | Some x => do no <- f (PTree.prev i) x; ret (Some no)
+        end;
+    do nl <- xtraverse_ptree f l (xO i);
+    do nr <- xtraverse_ptree f r (xI i);
+    ret (PTree.Node nl no nr)
+  end.
+
+Definition traverse_ptree {A B : Type} (f : positive -> A -> mon B) m := xtraverse_ptree f m xH.
+
+Definition traverse_ptree1 {A B : Type} (f : A -> mon B) := traverse_ptree (fun _ => f).
+
 End MonadExtra.