diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-02-16 14:11:32 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-16 14:11:32 +0000 |
commit | 6a395495bd35bb7d4d2cc7d3271c9b588d466594 (patch) | |
tree | 0fcc285046352b9f677454eac3224ce5a90ba48e /src/common/Monad.v | |
parent | 5f1e7aa8fbc4a0e04d0b137410c13f3d8da4d987 (diff) | |
parent | b5c79cb4913087a0e4b577b5dff616fc88ee938b (diff) | |
download | vericert-6a395495bd35bb7d4d2cc7d3271c9b588d466594.tar.gz vericert-6a395495bd35bb7d4d2cc7d3271c9b588d466594.zip |
Merge branch 'michalis' of https://github.com/mpardalos/vericert into michalis-merge
Diffstat (limited to 'src/common/Monad.v')
-rw-r--r-- | src/common/Monad.v | 39 |
1 files changed, 35 insertions, 4 deletions
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. |