From 9f0640ab94741d1d369d089fec763c9156d6be4f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 19 Mar 2020 15:20:13 +0000 Subject: Lower case folders --- src/common/Helper.v | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 src/common/Helper.v (limited to 'src/common/Helper.v') diff --git a/src/common/Helper.v b/src/common/Helper.v new file mode 100644 index 0000000..d23dbe4 --- /dev/null +++ b/src/common/Helper.v @@ -0,0 +1,39 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * 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 + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +Module Option. + +Definition default {T : Type} (x : T) (u : option T) : T := + match u with + | Some y => y + | _ => x + end. + +Definition map {S : Type} {T : Type} (f : S -> T) (u : option S) : option T := + match u with + | Some y => Some (f y) + | _ => None + end. + +Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : option T := + match a with + | Some x => map (f x) b + | _ => None + end. + +End Option. -- cgit