/* -----------------------------------------------------------------------------
Copyright 2021 Kevin P. Barry

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
----------------------------------------------------------------------------- */

// Author: Kevin P. Barry [ta0kira@gmail.com]

// Random-access vector of values.
//
// Params:
// - #x: The value type contained.
concrete Vector<#x> {
  defines Default
  refines Append<#x>
  refines DefaultOrder<#x>
  // Does not duplicate individual elements.
  refines Duplicate
  refines Stack<#x>
  refines ReadAt<#x>
  refines WriteAt<#x>

  // Create an empty Vector.
  @type new () -> (#self)

  // Create a pre-sized vector of default values.
  //
  // Notes:
  // - #y.default() should return a distinct value each time if #y is mutable.
  //   This means that modifying one element should not change others.
  @category createSize<#y>
    #y defines Default
  (Int) -> (Vector<#y>)
}