# 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 effect
open:c "stdint.h"
open:c "stddef.h"
use cabi.stub_prefix "cviz_"

# Z.  Direct Memory Access
#
# This provides direct accses to memory for the purpose of creating bindings
# to C libraries.  Naturally most if it is unsafe.


# Z.Z.  Size and Offset

type offset := int
type size := offset

in offset
    include int
    let scale n size be mul (of_int n) size


# Z.Z.  Pointer Objects

type:c ptr ψ := "void *"
 ## The type of a generic pointer.  This is always local to some pocket (ψ).

in ptr
    use cabi.stub_prefix "cviz_ptr_"

    val:cs cmp : ptr ψ → ptr ψ → torder
    val:cs eq : ptr ψ → ptr ψ → bool

    val:cs is_zero : ptr ψ → bool
     ## (is_zero p) is true iff (p) represents the (NULL) pointer.

    #?ffoc {#
    val zero : ptr ψ
     ## The null pointer.
    #?ffoc #}

    val:cs get_zero : pocket_tag ψ → ptr ψ
     ## This is a variant of (zero) to work around the value restriction in
     ## Camlviz.

    val:cs add : offset → ptr ψ → ptr ψ
     ## (ptr_add n p) translates (p) across (n) bytes.  If (p) points to garbage
     ## collected memory, this may cause the object to be freed, making subsequent
     ## access unsafe.

    val:cs diff : ptr ψ → ptr ψ → offset
     ## (ptr_diff p q) is the distance in bytes from (q) to (p).

    val:cs show : ptr ψ → string
     ## (show p) is a textual representation of (p), conventionally hexadecimal
     ## including a "0x" prefix.

val:cs unsafe_custom_address : α → effect ψ (ptr ψ)
 ## Assuming (x) is a custom object, (unsafe_custom_address x) is a pointer to
 ## the start of the custom data.

val:cs unsafe_custom_load_ptr : α → effect ψ (ptr ψ)
 ## Assuming (x) is a custom object, (unsafe_custom_load_ptr x) loads a
 ## pointer from the first slot of the custom data.  This is just a shortcut
 ## for (unsafe_load_ptr ∘ unsafe_custom_address).


# Z.Z.  Sizes of Elementary C Values

val:c sizeof_ptr : size := "(intnat)sizeof(void *)"
 ## The size of a pointer.

val:c sizeof_ptrdiff_t : size := "(intnat)sizeof(ptrdiff_t)"
 ## The size of the ptrdiff_t type.

val:c sizeof_size_t : size := "(intnat)sizeof(size_t)"
 ## The size of the size_t type.

val:c sizeof_cshort : size := "(intnat)sizeof(short)"
 ## The size of the C short and unsigned short types.

val:c sizeof_cint : size := "(intnat)sizeof(int)"
 ## The size of the C int and unsigned int types.

val:c sizeof_clong : size := "(intnat)sizeof(long)"
 ## The size of the C long and unsigned long types.

val:c sizeof_clonglong : size := "(intnat)sizeof(long long)"
 ## The size of the C long long and unsigned long long types.

val:c sizeof_cintptr : size := "(intnat)sizeof(intptr_t)"
 ## The size of the C intptr_t and uintptr_t types.

val:c sizeof_cintmax : size := "(intnat)sizeof(intmax_t)"
 ## The size of the C intmax_t and uintptr_t types.


# Z.Z.  Load and Store

val:cs unsafe_load_ptr   : offset → ptr ψ → effect ψ (ptr ψ)
val:cs unsafe_load_u8    : offset → ptr ψ → effect ψ int
val:cs unsafe_load_s8    : offset → ptr ψ → effect ψ int
val:cs unsafe_load_u16   : offset → ptr ψ → effect ψ int
val:cs unsafe_load_s16   : offset → ptr ψ → effect ψ int
val:cs unsafe_load_int32 : offset → ptr ψ → effect ψ int32
val:cs unsafe_load_int64 : offset → ptr ψ → effect ψ int64

val:cs unsafe_store_ptr   : offset → ptr ψ → ptr ψ → effect ψ unit
val:cs unsafe_store_8     : offset → ptr ψ → int   → effect ψ unit
val:cs unsafe_store_16    : offset → ptr ψ → int   → effect ψ unit
val:cs unsafe_store_int32 : offset → ptr ψ → int32 → effect ψ unit
val:cs unsafe_store_int64 : offset → ptr ψ → int64 → effect ψ unit


# Z.Z.  Auxiliary Functions

val:c unsafe_malloc : size → effect ψ (ptr ψ) := "malloc"
val:c unsafe_free : ptr ψ → effect ψ unit := "free"

val unsafe_lalloc : size → (ptr ψ → effect ψ α) → effect ψ α
let unsafe_lalloc size f
    be unsafe_malloc size >>= p ↦ f p >>= r ↦ unsafe_free p >> return r

val:c unsafe_copy_cstring : ptr ψ → ψ /~ string#v := "cviz_copy_ustring"