(*  Title:      JinjaThreads/J/JHeap.thy
    Author:     Andreas Lochbihler
*)

section ‹Abstract heap locales for source code programs›

theory JHeap
imports
  "../Common/Conform"
  Expr
begin

locale J_heap_base = heap_base +
  constrains addr2thread_id :: "('addr :: addr) → 'thread_id"
  and thread_id2addr :: "'thread_id → 'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap → htype → ('heap × 'addr) set"
  and typeof_addr :: "'heap → 'addr ⇀ htype"
  and heap_read :: "'heap → 'addr → addr_loc → 'addr val → bool"
  and heap_write :: "'heap → 'addr → addr_loc → 'addr val → 'heap → bool"

locale J_heap = heap + 
  constrains addr2thread_id :: "('addr :: addr) → 'thread_id"
  and thread_id2addr :: "'thread_id → 'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap → htype → ('heap × 'addr) set"
  and typeof_addr :: "'heap → 'addr ⇀ htype"
  and heap_read :: "'heap → 'addr → addr_loc → 'addr val → bool"
  and heap_write :: "'heap → 'addr → addr_loc → 'addr val → 'heap → bool"
  and P :: "'addr J_prog"

sublocale J_heap < J_heap_base .

locale J_heap_conf_base = heap_conf_base +
  constrains addr2thread_id :: "('addr :: addr) → 'thread_id"
  and thread_id2addr :: "'thread_id → 'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap → htype → ('heap × 'addr) set"
  and typeof_addr :: "'heap → 'addr ⇀ htype"
  and heap_read :: "'heap → 'addr → addr_loc → 'addr val → bool"
  and heap_write :: "'heap → 'addr → addr_loc → 'addr val → 'heap → bool"
  and hconf :: "'heap → bool"
  and P :: "'addr J_prog"

sublocale J_heap_conf_base < J_heap_base .

locale J_heap_conf = 
  J_heap_conf_base +
  heap_conf +
  constrains addr2thread_id :: "('addr :: addr) → 'thread_id"
  and thread_id2addr :: "'thread_id → 'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap → htype → ('heap × 'addr) set"
  and typeof_addr :: "'heap → 'addr ⇀ htype"
  and heap_read :: "'heap → 'addr → addr_loc → 'addr val → bool"
  and heap_write :: "'heap → 'addr → addr_loc → 'addr val → 'heap → bool"
  and hconf :: "'heap → bool"
  and P :: "'addr J_prog"

sublocale J_heap_conf < J_heap
by(unfold_locales)

locale J_progress =
  heap_progress +
  J_heap_conf_base +
  constrains addr2thread_id :: "('addr :: addr) → 'thread_id"
  and thread_id2addr :: "'thread_id → 'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap → htype → ('heap × 'addr) set"
  and typeof_addr :: "'heap → 'addr ⇀ htype"
  and heap_read :: "'heap → 'addr → addr_loc → 'addr val → bool"
  and heap_write :: "'heap → 'addr → addr_loc → 'addr val → 'heap → bool"
  and hconf :: "'heap → bool"
  and P :: "'addr J_prog"

sublocale J_progress < J_heap by(unfold_locales) 

locale J_conf_read =
  heap_conf_read +
  J_heap_conf +
  constrains addr2thread_id :: "('addr :: addr) → 'thread_id"
  and thread_id2addr :: "'thread_id → 'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap → htype → ('heap × 'addr) set"
  and typeof_addr :: "'heap → 'addr ⇀ htype"
  and heap_read :: "'heap → 'addr → addr_loc → 'addr val → bool"
  and heap_write :: "'heap → 'addr → addr_loc → 'addr val → 'heap → bool"
  and hconf :: "'heap → bool"
  and P :: "'addr J_prog"

sublocale J_conf_read < J_heap by(unfold_locales)

locale J_typesafe =
  heap_typesafe +
  J_conf_read +
  J_progress +
  constrains addr2thread_id :: "('addr :: addr) → 'thread_id"
  and thread_id2addr :: "'thread_id → 'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap → htype → ('heap × 'addr) set"
  and typeof_addr :: "'heap → 'addr ⇀ htype"
  and heap_read :: "'heap → 'addr → addr_loc → 'addr val → bool"
  and heap_write :: "'heap → 'addr → addr_loc → 'addr val → 'heap → bool"
  and hconf :: "'heap → bool"
  and P :: "'addr J_prog"

end