# Copyright 2011  Petter Urkedal
#
# This file is part of the Viz Standard Library <http://www.vizlang.org/>.
#
# The Viz Standard Library (VSL) is free software: you can redistribute it
# and/or modify it under the terms of the GNU Lesser General Public License as
# published by the Free Software Foundation, either version 3 of the License,
# or (at your option) any later version.
#
# The VSL is distributed in the hope that it will be useful, but WITHOUT ANY
# WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
# FOR A PARTICULAR PURPOSE.  See the GNU Lesser General Public License for
# more details.
#
# You should have received a copy of the GNU Lesser General Public License
# along with the VSL.  If not, see <http://www.gnu.org/licenses/>.

open ubiquitous
open field_allocation
open record_sigs
open phantoms
open effect

sealed with
    include a_record_architecture

    type alignment := int
    type offset := int

    val record_size : is_record δ → offset
    val record_alignment : is_record δ → offset

    val field_offset : has_field δ δ' → offset

    val elements_offset : has_elements σ δ → offset

    val unsafe_conjecture_etype : int → is_record δ
    val unsafe_conjecture_field : is_record ε → offset → has_field δ ε

    in int8_t   include a_foreign_type.[t = int]
    in uint8_t  include a_foreign_type.[t = int]
    in int16_t  include a_foreign_type.[t = int]
    in uint16_t include a_foreign_type.[t = int]
    in int32_t  include a_foreign_type.[t = int32]
    in uint32_t include a_foreign_type.[t = nat32]
    in int64_t  include a_foreign_type.[t = int64]
    in uint64_t include a_foreign_type.[t = nat64]

    in sshort include a_foreign_type.[t = nint]
    in ushort include a_foreign_type.[t = nnat]
    in sint   include a_foreign_type.[t = nint]
    in uint   include a_foreign_type.[t = nnat]
    in slong  include a_foreign_type.[t = nint]
    in ulong  include a_foreign_type.[t = nnat]

    in ptrdiff_t include a_foreign_type.[t = nint]
    in size_t    include a_foreign_type.[t = nnat]
    in intptr_t  include a_foreign_type.[t = nint]
    in uintptr_t include a_foreign_type.[t = nnat]

type alignment := int
type offset := int
in offset include int

# 0.0.  Internal Helpers

let unbounded be -1
 ## The value used in place of the array size for spill-arrays.

in alignment
    include int
    let none be zero
    let is_none be eq zero

let align al' off
    let al be offset.of_int al'
    let 2'+ , 2'- be offset.add, offset.sub
    be offset.bitand (off + al - offset.one) (offset.bitnot (al - offset.one))

# 0.0.  Propositions

type is_record δ         inj record_sc : alignment → offset → is_record δ
type has_field δ ε       inj field_sc : offset → has_field δ ε
type has_components δ ε  inj components_sc : int → offset → has_components δ ε
type has_elements σ ε    inj elements_sc : offset → offset → has_elements σ ε

let unsafe_conjecture_etype s be record_sc (offset.as_int s) s

let record_size (record_sc al sz) be sz
let record_alignment (record_sc al sz) be al
let field_offset (field_sc off) be off
let elements_offset (elements_sc off sz) be off

let unsafe_conjecture_field d off be field_sc off

# 0.0.  Axioms

let field_is_transitive (field_sc offA) (field_sc offB)
    be field_sc (offset.add offA offB)
let components_are_elements (components_sc n sz)
    be elements_sc offset.zero sz

let record_ptr_ev r be unsafe_conjecture_etype memory.sizeof_ptr
let record_value_ev r be unsafe_conjecture_etype memory.sizeof_ptr
let forward_ptr_ev r be unsafe_conjecture_etype memory.sizeof_ptr
let forward_value_ev r be unsafe_conjecture_etype memory.sizeof_ptr

let unit_ev be record_sc alignment.one offset.zero
let value_ev be unsafe_conjecture_etype memory.sizeof_ptr

let int_ev be unsafe_conjecture_etype memory.sizeof_clong
let nint_ev be unsafe_conjecture_etype memory.sizeof_clong

# Compounds

let array_ev n (record_sc alE szE)
    be (record_sc alE (offset.mul (offset.of_int n) szE), components_sc n szE)
let spill_ev (record_sc alM szM) (record_sc alS szS)
    be (field_sc offset.zero, elements_sc (align alS szM) szS)
let spill_ptr_ev _ _ be unsafe_conjecture_etype memory.sizeof_ptr

sig a_fabric
    type ph := unit
    val ptr_ev : is_record (ptr_ph ph)
    val value_ev : is_record (value_ph ph)
    val acquire : is_record δ → io (has_field ph δ)
    val realize : io (is_record ph)

in! make_fabric.(A : a_field_allocator.[alignment = alignment]
				      .[offset = offset])
    let _state do ref.init (A.empty, false)

    let ptr_ev be record_ptr_ev ()
    let value_ev be record_value_ev ()

    let! acquire (record_sc al sz)
	let (state, complete) do ref.get _state
	if complete fail "Attempt to extend a realized record."
	let (offset, state') be A.alloc al sz state
	do ref.set _state (state', false)
	be field_sc offset

    let! realize
	let (state, complete) do ref.get _state
	if complete fail "Attempt to realize a record multiple times."
	do ref.set _state (state, true)
	be record_sc (A.alignment state) (A.size state)

in! fabric
    type ph := unit
    include! make_fabric.(monotonic_field_allocator.(int))


# 0.0.  Lens

in lens
    # Should be abstract, but value restriction kicks in below.
    type R Ψ δ := unit
    type r ψ δ := R (hot ψ) δ
    type t δ   := R cold δ

    val:cs cmp : R Ψ δ → R Ψ' δ → torder := "vsls_lens_cmp"
    val:cs _focus : offset → R Ψ δ → R Ψ δ' := "vsls_lens_focus"

    let focus_field (field_sc off) p be _focus off p
    let focus_component (components_sc _ sz) n p
	be _focus (offset.mul sz (offset.of_int n)) p
    let focus_element (elements_sc off sz) n p
	be _focus (offset.add off (offset.mul sz (offset.of_int n))) p

    let unsafe_defocus_field (field_sc off) p be _focus (offset.neg off) p

    val:cs get_ptr : t (ptr_ph δ) → t δ := "vsls_lens_load_ptr"
    val:cs load_ptr : r ψ (ptr_ph δ) → effect ψ (r ψ δ) := "vsls_lens_load_ptr"
    val:cs store_ptr : r ψ δ → r ψ (ptr_ph δ) → effect ψ unit
	    := "vsls_lens_store_ptr"

    val:cs get_value : t (value_ph α) → α := "vsls_lens_load_value"
    val:cs load_value : r ψ (value_ph α) → effect ψ α := "vsls_lens_load_value"
    val:cs store_value : α → r ψ (value_ph α) → effect ψ unit
	    := "vsls_lens_store_value"

    val:cs unsafe_get_null : unit → R Ψ δ := "vsls_lens_get_null"
    let unsafe_null be unsafe_get_null ()
    val:cs unsafe_cast : R Ψ δ → R Ψ δ' := "%identity"
    val:cs unsafe_freeze : R Ψ δ → t δ := "%identity"
    val:cs unsafe_thaw : R Ψ δ → r ψ δ := "%identity"


# 0.0.  Primitive Type Conversions

sig a_foreign_type
    type ph
    type t
    val ev : is_record ph
    val get : lens.t ph → t
    val load : lens.r ψ ph → effect ψ t
    val store : t → lens.r ψ ph → effect ψ unit


# 0.0.  Construction and Inspection

in record
    # Should be abstract, but value restriction kicks in below.
    type R Ψ δ := unit
    type r ψ δ := R (hot ψ) δ
    type t δ := R cold δ

    val:cs prim_alloc : offset → effect ψ (R Ψ δ) := "vsls_record_alloc"
    val:cs prim_alloc_finalized :
	    offset → (r ψ δ → unit) → effect ψ (r ψ δ) :=
	    "vsls_record_alloc_finalized"
    val:cs focus : R Ψ δ → lens.R Ψ δ := "vsls_record_focus"

    let alloc (record_sc al sz) be prim_alloc sz
    let alloc_finalized (record_sc al sz) f
	be prim_alloc_finalized sz (__builtin_effect_run ∘ f)

    let init (record_sc al sz) (f : ∀ψ. lens.r ψ δ → effect ψ α)
	be observe (that : ∀ψ. effect ψ (α × R Ψ δ)) which!
	let p do prim_alloc sz
	let x do f (focus p)
	be (x, p)

    let! alloc_spilled (record_sc al sz) n (record_sc alE szE)
	let offE be align alE sz
	do prim_alloc (offset.add offE (offset.mul (offset.of_int n) szE))

    let init_spilled (record_sc al sz) n (record_sc alE szE)
		     (f : ∀ψ. lens.r ψ (spill_ph δ ε) → effect ψ α)
	be observe (that : ∀ψ. effect ψ (α × R Ψ δ)) which!
	let offE be align alE sz
	let p do prim_alloc (offset.add offE (offset.mul (offset.of_int n) szE))
	let x do f (focus p)
	be (x, p)


# 0.0.0.  Generic Types

in int8_t
    type ph inj _int8_ph
    type t := int
    let ev be unsafe_conjecture_etype (offset.of_int 1)
    val:cs get : lens.t ph → t			:= "vsls_int8_t_load_int"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_int8_t_load_int"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_int8_t_store_int"
in uint8_t
    type ph inj _nat8_ph
    type t := int
    let ev be unsafe_conjecture_etype (offset.of_int 1)
    val:cs get : lens.t ph → t			:= "vsls_uint8_t_load_int"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_uint8_t_load_int"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_uint8_t_store_int"

in int16_t
    type ph inj _int16_ph
    type t := int
    let ev be unsafe_conjecture_etype (offset.of_int 2)
    val:cs get : lens.t ph → t			:= "vsls_int16_t_load_int"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_int16_t_load_int"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_int16_t_store_int"
in uint16_t
    type ph inj _nat16_ph
    type t := int
    let ev be unsafe_conjecture_etype (offset.of_int 2)
    val:cs get : lens.t ph → t			:= "vsls_uint16_t_load_int"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_uint16_t_load_int"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_uint16_t_store_int"

in int32_t
    type ph inj _int32_ph
    type t := int32
    let ev be unsafe_conjecture_etype (offset.of_int 4)
    val:cs get : lens.t ph → t			:= "vsls_xint32_t_load_int32"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_xint32_t_load_int32"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_xint32_t_store_int32"
in uint32_t
    type ph inj _nat32_ph
    type t := nat32
    let ev be unsafe_conjecture_etype (offset.of_int 4)
    val:cs get : lens.t ph → t			:= "vsls_xint32_t_load_int32"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_xint32_t_load_int32"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_xint32_t_store_int32"

in int64_t
    type ph inj _int64_ph
    type t := int64
    let ev be unsafe_conjecture_etype (offset.of_int 8)
    val:cs get : lens.t ph → int64		:= "vsls_xint64_t_load_int64"
    val:cs load : lens.r ψ ph → effect ψ int64	:= "vsls_xint64_t_load_int64"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_xint64_t_store_int64"
in uint64_t
    type ph inj _nat64_ph
    type t := nat64
    let ev be unsafe_conjecture_etype (offset.of_int 8)
    val:cs get : lens.t ph → t			:= "vsls_xint64_t_load_int64"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_xint64_t_load_int64"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_xint64_t_store_int64"

# 0.0.0.  C-Specific Types

in sshort
    type ph inj _sshort_ph
    type t := nint
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_cshort)
    val:cs get : lens.t ph → t			:= "vsls_sshort_load_nint"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_sshort_load_nint"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_sshort_store_nint"
in ushort
    type ph inj _ushort_ph
    type t := nnat
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_cshort)
    val:cs get : lens.t ph → t			:= "vsls_ushort_load_nnat"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_ushort_load_nnat"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_ushort_store_nnat"
in sint
    type ph inj _sint_ph
    type t := nint
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_cint)
    val:cs get : lens.t ph → t			:= "vsls_sint_load_nint"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_sint_load_nint"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_sint_store_nint"
in uint
    type ph inj _uint_ph
    type t := nnat
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_cint)
    val:cs get : lens.t ph → t			:= "vsls_uint_load_nnat"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_uint_load_nnat"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_uint_store_nnat"
in slong
    type ph inj _slong_ph
    type t := nint
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_clong)
    val:cs get : lens.t ph → t			:= "vsls_slong_load_nint"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_slong_load_nint"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_slong_store_nint"
in ulong
    type ph inj _ulong_ph
    type t := nnat
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_clong)
    val:cs get : lens.t ph → t			:= "vsls_ulong_load_nnat"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_ulong_load_nnat"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_ulong_store_nnat"
{#
in slonglong
    type ph inj _slonglong_ph
    type t := nint
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_clonglong)
    val:cs get : lens.t ph → t			:= "vsls_slonglong_load_nint"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_slonglong_load_nint"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_slonglong_store_nint"
in ulonglong
    type ph inj _ulonglong_ph
    type t := nint
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_clonglong)
    val:cs get : lens.t ph → t			:= "vsls_ulonglong_load_nint"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_ulonglong_load_nint"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_ulonglong_store_nint"
#}
in ptrdiff_t
    type ph inj _ptrdiff_t_ph
    type t := nint
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_ptrdiff_t)
    val:cs get : lens.t ph → t			:= "vsls_ptrdiff_t_load_nint"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_ptrdiff_t_load_nint"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_ptrdiff_t_store_nint"
in size_t
    type ph inj _size_t_ph
    type t := nnat
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_size_t)
    val:cs get : lens.t ph → t			:= "vsls_size_t_load_nnat"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_size_t_load_nnat"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_size_t_store_nnat"
in intptr_t
    type ph inj _sintptr_ph
    type t := nint
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_cintptr)
    val:cs get : lens.t ph → t			:= "vsls_intptr_t_load_nint"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_intptr_t_load_nint"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_intptr_t_store_nint"
in uintptr_t
    type ph inj _uintptr_ph
    type t := nnat
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_cintptr)
    val:cs get : lens.t ph → t			:= "vsls_uintptr_t_load_nnat"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_uintptr_t_load_nnat"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_uintptr_t_store_nnat"
{#
in sintmax
    type ph inj _sintmax_ph
    type t := nint
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_cintmax)
    val:cs get : lens.t ph → t			:= "vsls_sintmax_load_nint"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_sintmax_load_nint"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_sintmax_store_nint"
in uintmax
    type ph inj _uintmax_ph
    type t := nint
    let ev be unsafe_conjecture_etype (offset.of_int memory.sizeof_cintmax)
    val:cs get : lens.t ph → t			:= "vsls_uintmax_load_nint"
    val:cs load : lens.r ψ ph → effect ψ t	:= "vsls_uintmax_load_nint"
    val:cs store : t → lens.r ψ ph → effect ψ unit := "vsls_uintmax_store_nint"
#}