ink

inductive Mt.TaskM.impl.IterationResult (spec : Mt.Spec) (T : Type) : Type

• Done: {spec : Mt.Spec} → {T : Type} → spec.State → T → Mt.TaskM.impl.IterationResult spec T
• Panic: {spec : Mt.Spec} → {T : Type} → spec.State → String → Mt.TaskM.impl.IterationResult spec T
• Running: {spec : Mt.Spec} → {T : Type} → spec.State → (spec.State → Bool) → (spec.State → Mt.TaskM.impl.IterationResult spec T) → Mt.TaskM.impl.IterationResult spec T

ink

def Mt.TaskM.impl.TaskM (spec : Mt.Spec) (T : Type) : Type

Equations

• Mt.TaskM.impl.TaskM spec T = (spec.State → Mt.TaskM.impl.IterationResult spec T)

ink

def Mt.TaskM.impl.TaskM.atomic_read_modify_read {spec : Mt.Spec} {T : Type} (f : spec.State → T × spec.State) : Mt.TaskM.impl.TaskM spec T

Equations

• Mt.TaskM.impl.TaskM.atomic_read_modify_read f _fun_discr = let s := _fun_discr; match f s with | (t, s') => Mt.TaskM.impl.IterationResult.Done s' t

ink

def Mt.TaskM.impl.TaskM.panic {spec : Mt.Spec} {T : Type} (msg : String) : Mt.TaskM.impl.TaskM spec T

Equations

• Mt.TaskM.impl.TaskM.panic msg _fun_discr = let s := _fun_discr; Mt.TaskM.impl.IterationResult.Panic s msg

ink

def Mt.TaskM.impl.TaskM.atomic_assert {spec : Mt.Spec} (cond : spec.State → Bool) : Mt.TaskM.impl.TaskM spec Unit

Equations

• One or more equations did not get rendered due to their size.

ink

def Mt.TaskM.impl.TaskM.atomic_blocking_rmr {spec : Mt.Spec} {T : Type} (block_until : spec.State → Bool) (f : spec.State → T × spec.State) : Mt.TaskM.impl.TaskM spec T

Equations

• Mt.TaskM.impl.TaskM.atomic_blocking_rmr block_until f _fun_discr = let s := _fun_discr; Mt.TaskM.impl.IterationResult.Running s block_until (Mt.TaskM.impl.TaskM.atomic_read_modify_read f)

ink

inductive Mt.TaskM.impl.TaskM.is_direct_cont {spec : Mt.Spec} {T : Type} : Mt.TaskM.impl.TaskM spec T → Mt.TaskM.impl.TaskM spec T → Prop

• running: ∀ {spec : Mt.Spec} {T : Type} {p cont : Mt.TaskM.impl.TaskM spec T} {s s' : spec.State} {block_until : spec.State → Bool}, p s = Mt.TaskM.impl.IterationResult.Running s' block_until cont → Mt.TaskM.impl.TaskM.is_direct_cont cont p

ink

theorem Mt.TaskM.impl.TaskM.is_direct_cont.wf {spec : Mt.Spec} {T : Type} : WellFounded Mt.TaskM.impl.TaskM.is_direct_cont

ink

theorem Mt.TaskM.impl.TaskM.is_direct_cont.wf.helper {spec : Mt.Spec} {T : Type} (it : Mt.TaskM.impl.IterationResult spec T) (p : Mt.TaskM.impl.TaskM spec T) {s : spec.State} {block_until : spec.State → Bool} : it = Mt.TaskM.impl.IterationResult.Running s block_until p → Acc Mt.TaskM.impl.TaskM.is_direct_cont p

ink

instance Mt.TaskM.impl.TaskM.instWf {spec : Mt.Spec} {T : Type} : WellFoundedRelation (Mt.TaskM.impl.TaskM spec T)

Equations

• Mt.TaskM.impl.TaskM.instWf = { rel := Mt.TaskM.impl.TaskM.is_direct_cont, wf := (_ : WellFounded Mt.TaskM.impl.TaskM.is_direct_cont) }

ink

def Mt.TaskM.impl.TaskM.pure {spec : Mt.Spec} {T : Type} (t : T) : Mt.TaskM.impl.TaskM spec T

Equations

• Mt.TaskM.impl.TaskM.pure t s = Mt.TaskM.impl.IterationResult.Done s t

ink

def Mt.TaskM.impl.TaskM.bind {spec : Mt.Spec} {U : Type} {V : Type} (mu : Mt.TaskM.impl.TaskM spec U) (f : U → Mt.TaskM.impl.TaskM spec V) : Mt.TaskM.impl.TaskM spec V

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Mt.TaskM.impl.TaskM.bind_def {U : Type} {V : Type} {spec : Mt.Spec} {mu : Mt.TaskM.impl.TaskM spec U} {f : U → Mt.TaskM.impl.TaskM spec V} {s : spec.State} : Mt.TaskM.impl.TaskM.bind mu f s = let _discr := mu s; match mu s with | Mt.TaskM.impl.IterationResult.Done s' u => Mt.TaskM.impl.IterationResult.Running s' (fun x => true) (f u) | Mt.TaskM.impl.IterationResult.Panic s' msg => Mt.TaskM.impl.IterationResult.Panic s' msg | Mt.TaskM.impl.IterationResult.Running s' block_until cont => Mt.TaskM.impl.IterationResult.Running s' block_until (Mt.TaskM.impl.TaskM.bind cont f)

ink

theorem Mt.TaskM.impl.TaskM.bind_assoc {spec : Mt.Spec} {U : Type} {V : Type} {W : Type} (mu : Mt.TaskM.impl.TaskM spec U) (f : U → Mt.TaskM.impl.TaskM spec V) (g : V → Mt.TaskM.impl.TaskM spec W) : (Mt.TaskM.impl.TaskM.bind mu fun u => Mt.TaskM.impl.TaskM.bind (f u) g) = Mt.TaskM.impl.TaskM.bind (Mt.TaskM.impl.TaskM.bind mu f) g