Theory "errorStateMonad"

Parents list

Signature

Constant	Type
BIND	:(α -> (β # α) option) -> (β -> α -> (γ # α) option) -> α -> (γ # α) option
ES_APPLY	:(α -> ((γ -> β) # α) option) -> (α -> (γ # α) option) -> α -> (β # α) option
ES_CHOICE	:(β -> α option) -> (β -> α option) -> β -> α option
ES_FAIL	:β -> α option
ES_GUARD	:bool -> α -> (unit # α) option
ES_LIFT2	:(γ -> δ -> β) -> (α -> (γ # α) option) -> (α -> (δ # α) option) -> α -> (β # α) option
FOR	:num # num # (num -> 'state -> (unit # 'state) option) -> 'state -> (unit # 'state) option
FOREACH	:α list # (α -> 'state -> (unit # 'state) option) -> 'state -> (unit # 'state) option
IGNORE_BIND	:(β -> (α # β) option) -> (β -> (γ # β) option) -> β -> (γ # β) option
JOIN	:(α -> ((α -> (β # α) option) # α) option) -> α -> (β # α) option
MMAP	:(γ -> β) -> (α -> (γ # α) option) -> α -> (β # α) option
NARROW	:β -> (β # 'state -> (α # β # 'state) option) -> 'state -> (α # 'state) option
READ	:('state -> α) -> 'state -> (α # 'state) option
UNIT	:β -> α -> (β # α) option
WIDEN	:('state -> (α # 'state) option) -> β # 'state -> (α # β # 'state) option
WRITE	:('state -> 'state) -> 'state -> (unit # 'state) option
mapM	:(α -> β -> (γ # β) option) -> α list -> β -> (γ list # β) option
sequence	:(α -> (β # α) option) list -> α -> (β list # α) option

Definitions

UNIT_DEF

|- ∀x. UNIT x = (λs. SOME (x,s))

BIND_DEF

|- ∀g f s0. BIND g f s0 = case g s0 of NONE => NONE | SOME (b,s) => f b s

IGNORE_BIND_DEF

|- ∀f g. IGNORE_BIND f g = BIND f (λx. g)

MMAP_DEF

|- ∀f m. MMAP f m = BIND m (UNIT o f)

JOIN_DEF

|- ∀z. JOIN z = BIND z I

FOR_primitive_def

|- FOR =
   WFREC
     (@R.
        WF R ∧ ∀a j i. i ≠ j ⇒ R (if i < j then i + 1 else i − 1,j,a) (i,j,a))
     (λFOR a'.
        case a' of
          (i,j,a) =>
            I
              (if i = j then a i
               else
                 BIND (a i) (λu. FOR (if i < j then i + 1 else i − 1,j,a))))

FOREACH_primitive_def

|- FOREACH =
   WFREC (@R. WF R ∧ ∀h a t. R (t,a) (h::t,a))
     (λFOREACH a'.
        case a' of
          ([],a) => I (UNIT ())
        | (h::t,a) => I (BIND (a h) (λu. FOREACH (t,a))))

READ_def

|- ∀f. READ f = (λs. SOME (f s,s))

WRITE_def

|- ∀f. WRITE f = (λs. SOME ((),f s))

NARROW_def

|- ∀v f.
     NARROW v f =
     (λs. case f (v,s) of NONE => NONE | SOME (r,s1) => SOME (r,SND s1))

WIDEN_def

|- ∀f.
     WIDEN f =
     (λ(s1,s2). case f s2 of NONE => NONE | SOME (r,s3) => SOME (r,s1,s3))

sequence_def

|- sequence =
   FOLDR (λm ms. BIND m (λx. BIND ms (λxs. UNIT (x::xs)))) (UNIT [])

mapM_def

|- ∀f. mapM f = sequence o MAP f

ES_FAIL_DEF

|- ∀s. ES_FAIL s = NONE

ES_CHOICE_DEF

|- ∀xM yM s.
     ES_CHOICE xM yM s = case xM s of NONE => yM s | SOME v1 => SOME v1

ES_GUARD_DEF

|- ∀b. ES_GUARD b = if b then UNIT () else ES_FAIL

ES_APPLY_DEF

|- ∀fM xM. fM <*> xM = BIND fM (λf. BIND xM (λx. UNIT (f x)))

ES_LIFT2_DEF

|- ∀f xM yM. ES_LIFT2 f xM yM = MMAP f xM <*> yM

Theorems

FOR_ind

|- ∀P.
     (∀i j a. (i ≠ j ⇒ P (if i < j then i + 1 else i − 1,j,a)) ⇒ P (i,j,a)) ⇒
     ∀v v1 v2. P (v,v1,v2)

FOR_def

|- ∀j i a.
     FOR (i,j,a) =
     if i = j then a i
     else BIND (a i) (λu. FOR (if i < j then i + 1 else i − 1,j,a))

FOREACH_ind

|- ∀P. (∀a. P ([],a)) ∧ (∀h t a. P (t,a) ⇒ P (h::t,a)) ⇒ ∀v v1. P (v,v1)

FOREACH_def

|- (∀a. FOREACH ([],a) = UNIT ()) ∧
   ∀t h a. FOREACH (h::t,a) = BIND (a h) (λu. FOREACH (t,a))

BIND_LEFT_UNIT

|- ∀k x. BIND (UNIT x) k = k x

BIND_RIGHT_UNIT

|- ∀k. BIND k UNIT = k

BIND_ASSOC

|- ∀k m n. BIND k (λa. BIND (m a) n) = BIND (BIND k m) n

MMAP_ID

|- MMAP I = I

MMAP_COMP

|- ∀f g. MMAP (f o g) = MMAP f o MMAP g

MMAP_UNIT

|- ∀f. MMAP f o UNIT = UNIT o f

MMAP_JOIN

|- ∀f. MMAP f o JOIN = JOIN o MMAP (MMAP f)

JOIN_UNIT

|- JOIN o UNIT = I

JOIN_MMAP_UNIT

|- JOIN o MMAP UNIT = I

JOIN_MAP_JOIN

|- JOIN o MMAP JOIN = JOIN o JOIN

JOIN_MAP

|- ∀k m. BIND k m = JOIN (MMAP m k)

sequence_nil

|- sequence [] = UNIT []

mapM_nil

|- mapM f [] = UNIT []

mapM_cons

|- mapM f (x::xs) = BIND (f x) (λy. BIND (mapM f xs) (λys. UNIT (y::ys)))

ES_CHOICE_ASSOC

|- ES_CHOICE xM (ES_CHOICE yM zM) = ES_CHOICE (ES_CHOICE xM yM) zM

ES_CHOICE_FAIL_LID

|- ES_CHOICE ES_FAIL xM = xM

ES_CHOICE_FAIL_RID

|- ES_CHOICE xM ES_FAIL = xM

BIND_FAIL_L

|- BIND ES_FAIL fM = ES_FAIL

BIND_ESGUARD

|- (BIND (ES_GUARD F) fM = ES_FAIL) ∧ (BIND (ES_GUARD T) fM = fM ())

IGNORE_BIND_ESGUARD

|- (IGNORE_BIND (ES_GUARD F) xM = ES_FAIL) ∧
   (IGNORE_BIND (ES_GUARD T) xM = xM)

IGNORE_BIND_FAIL

|- (IGNORE_BIND ES_FAIL xM = ES_FAIL) ∧ (IGNORE_BIND xM ES_FAIL = ES_FAIL)

APPLY_UNIT

|- UNIT f <*> xM = MMAP f xM

APPLY_UNIT_UNIT

|- UNIT f <*> UNIT x = UNIT (f x)