From b06d11d9e12cae00475e8f9a5f69d42cf34ae729 Mon Sep 17 00:00:00 2001 From: Jason Gross 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 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'src/Util/Option.v') 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 -- cgit v1.2.3