Theory AutoCorres2.Option_MonadND

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(* Option monad syntax plus the connection between the option monad and the nondet monad *)

theory Option_MonadND
  imports
  Reader_Monad
begin


definition
 ogets :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b option)"
where
 "ogets f ≡ (λs. Some (f s))"

definition
  ocatch :: "('s,('e + 'a)) lookup ⇒ ('e ⇒ ('s,'a) lookup) ⇒ ('s, 'a) lookup"
  (infix "<ocatch>" 10)
where
  "f <ocatch> handler ≡ do {
     x ← f;
     case x of Inr b ⇒ oreturn b | Inl e ⇒ handler e
   }"


definition
  odrop :: "('s, 'e + 'a) lookup ⇒ ('s, 'a) lookup"
where
  "odrop f ≡ do {
     x ← f;
     case x of Inr b ⇒ oreturn b | Inl e ⇒ ofail
   }"

definition
  osequence_x :: "('s, 'a) lookup list ⇒ ('s, unit) lookup"
where
  "osequence_x xs ≡ foldr (λx y. do { x; y }) xs (oreturn ())"

definition
  osequence :: "('s, 'a) lookup list ⇒ ('s, 'a list) lookup"
where
  "osequence xs ≡ let mcons = (λp q. p |>> (λx. q |>> (λy. oreturn (x#y))))
                 in foldr mcons xs (oreturn [])"

definition
  omap :: "('a ⇒ ('s,'b) lookup) ⇒ 'a list ⇒ ('s, 'b list) lookup"
where
  "omap f xs ≡ osequence (map f xs)"

definition
  opt_cons :: "'a option ⇒ 'a list ⇒ 'a list" (infixr "o#" 65)
where
  "opt_cons x xs ≡ case x of None ⇒ xs | Some x' ⇒ x' # xs"


end