# 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/>.


# 0.  Describing and Accessing Hierarchical Data
#
# This file defines an abstraction for describing, building, and accessing
# data.  It's tailored for native memory, but formulated generically enough to
# work for objects embedded e.g. in an interpreted language like JavaScript,
# or other virtual environments.
#
# Safety Remark.  Implementations of these signatures may be unsafe even if not
# indicated by the function names.  Issues include uninitialized references,
# unchecked array bounds, and over- and underflow during conversion.

# 0.0.  Status
#
# This interface and its implementations are experimental, and have some
# limitations.  In particular defining parametric types is currently
# unsupported.  This issue may be revisited when we have a compiler which is
# not subject to the value restriction.

# 0.0.  Concepts
#
# A record here refers to a layout of data which itself can be embedded in
# other records.  A record includes single primitive types and fixed-size
# arrays.  Variable-sized arrays are encoded as a "spill".
#
# A spill is a combination of two record descriptions.  An instance of a spill
# is an instance of the first record combined with any number of instances of
# the second record, indexed by an integer.  A spill encodes the common
# C-idiom of adding variable sized arrays as the last field of a struct.  A
# spill is not a record, since its size is unknown.

open prereq

# 0.0.  Phantom Types Used Below
#
# Phantom types are used to describe records which do not have a corresponding
# Viz type.  Below, type parameters (δ), (ε), and (ζ) run over phantoms
# describing records and (σ) runs over phantoms describing spills.

in phantoms

    # 0.0.0.  Phantoms for Pointers and Compounds

    type ptr_ph δ	inj _ptr_ph
    type value_ph α	inj _value_ph
    type array_ph δ	inj _array_ph
    type spill_ph δ ε	inj _spill_ph


# 0.0.  Record Architecture

sig a_record_architecture
    open phantoms

    # 0.0.0.  Propositions and Meta-Information about Records

    type is_record δ
      ## A value of type (is_record δ) witness the fact that (δ) is a record,
      ## and may carry information about the record needed by the
      ## implementation.

    type has_field δ ε
      ## A value of type (has_field δ ε) witness that (δ) has a field of type
      ## (ε), and also carries the information to select it.

    type has_components δ ε
      ## A value of type (has_components δ ε) witness the fact that (δ)
      ## contains a fixed number of components of type (ε), and may carry
      ## information needed to index them, such as the size of components and
      ## the number of components if bonds are checked.

    type has_elements σ ε
      ## A value of type (has_elements σ ε) witness that (σ) has a
      ## variable-sized array of elements of type (ε), and carry details to
      ## access it.  Typical implementations only populate this type where (σ)
      ## is a spill, as they require records to have fixed size.


    # 0.0.0.  Axioms and Meta-Information
    #
    # A record is described by producing evidence that it is a record, and
    # evidence for any fields, components, or elements it may have.  We use
    # the term evidence here as an informal term for an axiom or proof coupled
    # with meta-information used by the implementation.
    #
    # First, two generic facts:

    val field_is_transitive : has_field δ ε → has_field ε ζ → has_field δ ζ
     ## A lookup of a record field followed by a lookup within that record can
     ## be combined into one operation.

    val components_are_elements : has_components δ ε → has_elements δ ε
     ## Components of an array can be accessed as if they were part of a spill
     ## where the fixed part is the unit record.


    # 0.0.0.0.  Pointers

    val record_ptr_ev : is_record δ → is_record (ptr_ph δ)
     ## A pointer to a record is a record.

    val spill_ptr_ev :
	is_record δ → is_record ε → is_record (ptr_ph (spill_ph δ ε))
     ## A pointer to a spill is a record.


    # 0.0.0.0.  Compound Types

    val array_ev :
	int → is_record δ →
	is_record (array_ph δ) × has_components (array_ph δ) δ

    val spill_ev :
	is_record δ → is_record ε →
	has_field (spill_ph δ ε) δ × has_elements (spill_ph δ ε) ε

    in! fabric
	type ph
	val ptr_ev : is_record (ptr_ph ph)
	val acquire : is_record δ → io (has_field ph δ)
	val realize : io (is_record ph)


    # 0.0.0.  Lenses
    #
    # A lens can traverse the representation of an object, and provides
    # constant or mutable access.

    in lens
	type R Ψ δ
	type r ψ δ := R (hot ψ) δ
	type t δ   := R cold δ

	val cmp : R Ψ δ → R Ψ δ → torder

	val focus_field : has_field δ ε → R Ψ δ → R Ψ ε
	val focus_component : has_components δ ε → int → R Ψ δ → R Ψ ε
	val focus_element : has_elements σ ε → int → R Ψ σ → R Ψ ε

	val unsafe_defocus_field : has_field δ ε → R Ψ ε → R Ψ δ

	val get_ptr : t (ptr_ph δ) → t δ
	val load_ptr : r ψ (ptr_ph δ) → effect ψ (r ψ δ)
	val store_ptr : r ψ δ → r ψ (ptr_ph δ) → effect ψ unit

	val get_value : t (value_ph α) → α
	val load_value : r ψ (value_ph α) → effect ψ α
	val store_value : α → r ψ (value_ph α) → effect ψ unit

	val unsafe_null : R Ψ δ
	val unsafe_cast : R Ψ δ → R Ψ δ'
	val unsafe_freeze : R Ψ δ → t δ
	val unsafe_thaw : R Ψ δ → r ψ δ


    # 0.0.0.  Complete Objects
    #
    # Safety Remark.  Implementations of memory-allocating functions may pass
    # uninitialized data to the client.  Make sure to initialize all pointers.

    in record
	type R Ψ δ
	type r ψ δ := R (hot ψ) δ
	type t δ := R cold δ

	val alloc : is_record δ → effect ψ (r ψ δ)

	val alloc_finalized : is_record δ → (r ψ δ → effect ψ unit) →
			      effect ψ (r ψ δ)

	val init : is_record δ → (∀ψ. lens.r ψ δ → effect ψ α) → α × R Ψ δ
	 ## (init_record ev f) allocates an instance of (ev) and passes a
	 ## reference to (f) for initialization.  The value returned by (f) is
	 ## paired with the object handle as the result.

	val alloc_spilled :
	    is_record δ → int → is_record ε → effect ψ (r ψ (spill_ph δ ε))

	val init_spilled :
	    is_record δ → int → is_record ε →
	    (∀ψ. lens.r ψ (spill_ph δ ε) → effect ψ α) → α × R Ψ (spill_ph δ ε)
	 ## (init_spill ev n elt_ev f) allocates a spill with an instance of
	 ## (ev) and (n) instances of (elt_ev), initialized by (f), which
	 ## receives a reference lens to the newly allocated object.  The
	 ## result of (f) paired with the constructed object is returned.

	val focus : R Ψ δ → lens.R Ψ δ
	 ## Acquire read access to a constructed object.


    # 0.0.0.  Primitive Types

    val unit_ev : is_record unit

    val value_ev : is_record (value_ph α)

    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