From b06d11d9e12cae00475e8f9a5f69d42cf34ae729 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 11 Feb 2019 16:34:03 -0800
Subject: Add Option.{lift,map,combine}, List.Option.lift

These will be useful for extending the AST with `option` types.
---
 src/Util/Option.v     | 19 +++++++++++++++++++
 src/Util/OptionList.v |  5 +++++
 2 files changed, 24 insertions(+)

(limited to 'src/Util')

diff --git a/src/Util/Option.v b/src/Util/Option.v
index 2c6549cb6..2eae8d0e5 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -16,6 +16,19 @@ Definition option_beq_hetero {A B} (AB_beq : A -> B -> bool) (x : option A) (y :
        => false
      end.
 
+(** In general, [lift : M (option A) -> option (M A)].  This is a bit
+    confusing for [option] because [M = option].  We want to return
+    [None] if the thing contained in the [M (option A)] is [None], and
+    say [Some] otherwise. *)
+Definition lift {A} (x : option (option A)) : option (option A)
+  := match x with
+     | Some None => None (* the contained thing is bad/not present *)
+     | Some (Some x) => Some (Some x)
+     | None => Some None
+     end.
+
+Notation map := option_map (only parsing). (* so we have [Option.map] *)
+
 Definition bind {A B} (v : option A) (f : A -> option B) : option B
   := match v with
      | Some v => f v
@@ -45,6 +58,12 @@ Module Export Notations.
 End Notations.
 Local Open Scope option_scope.
 
+Definition combine {A B} (x : option A) (y : option B) : option (A * B)
+  := match x, y with
+     | Some x, Some y => Some (x, y)
+     | _, _ => None
+     end.
+
 Section Relations.
   Definition option_eq {A B} eq (x : option A) (y : option B) :=
     match x with
diff --git a/src/Util/OptionList.v b/src/Util/OptionList.v
index c2157346e..4b88dd9a3 100644
--- a/src/Util/OptionList.v
+++ b/src/Util/OptionList.v
@@ -25,6 +25,11 @@ Module Option.
          | x :: xs => (x <- x; @bind_list A B xs (fun xs => f (x :: xs)))
          end%option%list.
 
+    Definition lift {A} (ls : list (option A)) : option (list A)
+      := fold_right (fun x xs => x <- x; xs <- xs; Some (x :: xs))%option
+                    (Some nil)
+                    ls.
+
     Module Export Notations.
       Notation "A <-- X ; B" := (bind_list X (fun A => B%option)) : option_scope.
     End Notations.
-- 
cgit v1.2.3