import Mt.Task
import Mt.Utils

namespace Mt

/-- A single thread of the system. It consists of a task to
  execute and a blocking predicate. The system only
  iterates a thread if the blocking predicate holds -/
structure 
Thread: Spec → Type 1
Thread (
spec: Spec
spec : 
Spec: Type 1
Spec) where
  
T: {spec : Spec} → Thread spec → Type
T : 
Type: Type 1
Type
  
block_until: {spec : Spec} → Thread spec → spec.State → Bool
block_until : 
spec: Spec
spec.
State: Spec → Type
State -> 
Bool: Type
Bool
  
task: {spec : Spec} → (self : Thread spec) → TaskM spec self.T
task : 
TaskM: Spec → Type → Type
TaskM 
spec: Spec
spec 
T: Type
T

variable {
spec: Spec
spec : 
Spec: Type 1
Spec}
local 
instance: {spec : Spec} → IsReservation spec.Reservation
instance : 
IsReservation: Type → Type
IsReservation 
spec: Spec
spec.
Reservation: Spec → Type
Reservation :=
spec: Spec
spec.
is_reservation: (self : Spec) → IsReservation self.Reservation
is_reservation

def 
mk_thread: {T : Type} → TaskM spec T → Thread spec
mk_thread {
T: Type
T : 
Type: Type 1
Type} (
task: TaskM spec T
task : 
TaskM: Spec → Type → Type
TaskM 
spec: Spec
spec 
T: Type
T) : 
Thread: Spec → Type 1
Thread 
spec: Spec
spec := {
  
T: Type
T
  block_until :=λ 
_: ?m.550
_ => 
true: Bool
true
  
task: TaskM spec T
task }

namespace Thread

inductive 
IterationResult: Spec → Type 1
IterationResult (
spec: Spec
spec : 
Spec: Type 1
Spec) where
  | 
Done: {spec : Spec} → spec.State → IterationResult spec
Done : 
spec: Spec
spec.
State: Spec → Type
State -> 
IterationResult: Spec → Sort ?u.603
IterationResult 
spec: Spec
spec
  | 
Panic: {spec : Spec} → spec.State → IterationResult spec
Panic : 
spec: Spec
spec.
State: Spec → Type
State -> 
IterationResult: Spec → Sort ?u.603
IterationResult 
spec: Spec
spec
  | 
Running: {spec : Spec} → spec.State → Thread spec → IterationResult spec
Running : 
spec: Spec
spec.
State: Spec → Type
State -> 
Thread: Spec → Type 1
Thread 
spec: Spec
spec -> 
IterationResult: Spec → Sort ?u.603
IterationResult 
spec: Spec
spec

def 
IterationResult.state: {spec : Spec} → IterationResult spec → spec.State
IterationResult.state : 
IterationResult: Spec → Type 1
IterationResult 
spec: Spec
spec -> 
spec: Spec
spec.
State: Spec → Type
State
  | 
Done: {spec : Spec} → spec.State → IterationResult spec
Done 
state: spec.State
state => 
state: spec.State
state
  | 
Panic: {spec : Spec} → spec.State → IterationResult spec
Panic 
state: spec.State
state => 
state: spec.State
state
  | 
Running: {spec : Spec} → spec.State → Thread spec → IterationResult spec
Running 
state: spec.State
state _ => 
state: spec.State
state

def 
iterate: {spec : Spec} → Thread spec → spec.State → IterationResult spec
iterate : 
Thread: Spec → Type 1
Thread 
spec: Spec
spec -> 
spec: Spec
spec.
State: Spec → Type
State -> 
IterationResult: Spec → Type 1
IterationResult 
spec: Spec
spec
  | ⟨
T: Type
T, _, 
task: TaskM spec T
task⟩, 
state: spec.State
state =>
    match 
task: TaskM spec T
task.
iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → TaskM.IterationResult spec T
iterate 
state: spec.State
state with
    | 
TaskM.IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → TaskM.IterationResult spec T
TaskM.IterationResult.Done 
state': spec.State
state' _ => 
IterationResult.Done: {spec : Spec} → spec.State → IterationResult spec
IterationResult.Done 
state': spec.State
state'
    | 
TaskM.IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → TaskM.IterationResult spec T
TaskM.IterationResult.Panic 
state': spec.State
state' _ => 
IterationResult.Panic: {spec : Spec} → spec.State → IterationResult spec
IterationResult.Panic 
state': spec.State
state'
    | 
TaskM.IterationResult.Running: {spec : Spec} → {T : Type} → spec.State → (spec.State → Bool) → TaskM spec T → TaskM.IterationResult spec T
TaskM.IterationResult.Running 
state': spec.State
state' 
block_until: spec.State → Bool
block_until 
task: TaskM spec T
task => 
      
IterationResult.Running: {spec : Spec} → spec.State → Thread spec → IterationResult spec
IterationResult.Running 
state': spec.State
state' { 
T: Type
T, 
block_until: spec.State → Bool
block_until, 
task: TaskM spec T
task }

/-- Small wrapper around `TaskM.valid`. A thread is considered valid
  if its underlying task is valid and ensures that it drops its
  reservation in the end.
  
  To prove `Thread.valid`, you should unfold `Thread.valid`, for example
  using `rw [Thread.valid]` and continue applying the validation theoreoms
  for `TaskM.valid`, like `TaskM.valid_bind` -/
def 
valid: Thread spec → Prop
valid (
thread: Thread spec
thread : 
Thread: Spec → Type 1
Thread 
spec: Spec
spec) : 
Prop: Type
Prop :=
  
thread: Thread spec
thread.
task: {spec : Spec} → (self : Thread spec) → TaskM spec self.T
task.
valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid 
IsReservation.empty: {T : Type} → [self : IsReservation T] → T
IsReservation.empty
    
thread: Thread spec
thread.
block_until: {spec : Spec} → Thread spec → spec.State → Bool
block_until
    (λ 
_: ?m.2233
_ 
r: ?m.2236
r => 
r: ?m.2236
r = 
IsReservation.empty: {T : Type} → [self : IsReservation T] → T
IsReservation.empty)

end Thread

end Mt