From 5560f9398bd29e468488446be71f85648851a78b Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 15 Feb 2021 22:26:29 +0000 Subject: Add PTree traversal functions for vericert monads --- src/common/Monad.v | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) (limited to 'src/common') diff --git a/src/common/Monad.v b/src/common/Monad.v index 03dd294..c42f4a3 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -1,4 +1,5 @@ -From Coq Require Import Lists.List. +From Coq Require Import BinNums Lists.List. +From compcert Require Import Maps. Module Type Monad. @@ -56,4 +57,22 @@ Module MonadExtra(M : Monad). | 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. -- cgit