Merge branch 'michalis' of https://github.com/mpardalos/vericert into michalis-merge

3 files changed, 71 insertions, 4 deletions

diff --git a/src/common/Maps.v b/src/common/Maps.v
index f0f264d..2db5114 100644
--- a/src/common/Maps.v
+++ b/src/common/Maps.v
@@ -61,4 +61,31 @@ Definition traverse (A B : Type) (f : positive -> A -> res B) m := xtraverse f m
 
 Definition traverse1 (A B : Type) (f : A -> res B) := traverse (fun _ => f).
 
+Definition filter (A: Type) (pred: PTree.elt -> A -> bool) (m: t A) : t A :=
+  PTree.map (fun _ a => snd a) (PTree.filter1 (fun a => pred (fst a) (snd a)) (PTree.map (fun i x => (i, x)) m)).
+
+Theorem filter_spec: forall (A: Type) (pred: PTree.elt -> A -> bool) (m: PTree.t A) (i: PTree.elt) (x : A),
+    (filter pred m) ! i =
+    match m ! i with
+    | None => None
+    | Some x => if pred i x then Some x else None
+    end.
+Proof.
+  intros.
+  unfold filter.
+
+  rewrite gmap.
+  unfold option_map.
+
+  rewrite gfilter1.
+
+  rewrite gmap.
+  unfold option_map.
+
+  destruct (m ! i).
+  - simpl.
+    destruct (pred i a); simpl; reflexivity.
+  - reflexivity.
+Qed.
+
 End PTree.
diff --git a/src/common/Monad.v b/src/common/Monad.v
index 5e8385e..68233b1 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.
 
@@ -48,19 +50,48 @@ Module MonadExtra(M : Monad).
   End MonadNotation.
   Import MonadNotation.
 
-  Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) :=
+  Fixpoint sequence {A: Type} (l: list (mon A)) {struct l}: mon (list A) :=
     match l with
     | nil => ret nil
     | x::xs =>
-      do r <- f x;
-      do rs <- traverselist f xs;
+      do r <- x;
+      do rs <- sequence xs;
       ret (r::rs)
     end.
 
+  Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) :=
+    sequence (map f l).
+
+  Fixpoint traverseoption {A B: Type} (f: A -> mon B) (opt: option A) {struct opt}: 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.
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index f2754be..a0d2af1 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -230,6 +230,15 @@ Definition join {A : Type} (a : option (option A)) : option A :=
   | Some a' => a'
   end.
 
+Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A) : list B :=
+  match l with
+  | nil => nil
+  | x::xs => match f x with
+           | None => map_option f xs
+           | Some x' => x'::map_option f xs
+           end
+  end.
+
 Module Notation.
 Notation "'do' X <- A ; B" := (bind A (fun X => B))
    (at level 200, X ident, A at level 100, B at level 200).