A Tutorial on Programming Features in ATS:
<<< Previous 

Stack Allocation at Run-Time

In ATS, there is support for allocating memory at run-time in the stack frame of the calling function, and it is guaranteed by the type system of ATS that the memory thus allocated cannot be accessed once the calling function returns.

In the following contrived example, the implemented function name_of_month_1 allocates in its stack frame an array of size 12 that is initialized with the names of 12 months, and then returns the name of the ith month, where i is an integer between 1 and 12: 

fn name_of_month_1
  {i:int | 1 <= i; i <= 12} (i: int i): string = let
  var !p_arr with pf_arr = @[string](
    "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"
  ) // end of [var]
in
  p_arr->[i-1] // it can also be written as !p_arr[i-1]
end // end of [name_of_month_1]

The following syntax means that the starting address of the allocated array is stored in p_arr while the view of the array is stored in pf_arr: 

  var !p_arr with pf_arr = @[string](
    "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"
  ) // end of [var]

This allocated array is initialized with the strings representing the names of the 12 months: "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec".

A variant of the function name_of_month_1 is implemeneted as follows: 

fn name_of_month_2
  {i:int | 1 <= i; i < 12}
  (i: int i): string = let
  var !p_arr with pf_arr = @[string][12]("")
  val () = p_arr->[0] := "Jan"
  val () = p_arr->[1] := "Feb"
  val () = p_arr->[2] := "Mar"
  val () = p_arr->[3] := "Apr"
  val () = p_arr->[4] := "May"
  val () = p_arr->[5] := "Jun"
  val () = p_arr->[6] := "Jul"
  val () = p_arr->[7] := "Aug"
  val () = p_arr->[8] := "Sep"
  val () = p_arr->[9] := "Oct"
  val () = p_arr->[10] := "Nov"
  val () = p_arr->[11] := "Dec"
in
  p_arr->[i-1]
end // end of [name_of_month_2]

The following syntax means that the function name_of_month_2 allocates a string array of size 12 in its stack frame and initializes the array with the empty string: 

  var !p_arr with pf_arr = @[string][12]("")

The starting address and the view of the allocated array are stored in p_arr and pf_arr, respectively. If the following syntax is used: 

  var !p_arr with pf_arr = @[string][12]()

then the allocated array is uninitialized, that is, the view of the proof pf_arr is [string?][12] @ p_arr (instead of [string][12] @ p_arr).

When higher-order functions are employed in systems programming, it is often desirable to form closures in the stack frame of the calling function so as to avoid the need for memory allocation on heap. In the following example, the implemented function print_month_name forms a closure in its stack frame, which is then passed to a higher-order function iforeach_array_ptr_clo: 

fn print_month_names () = let
  var !p_arr with pf_arr = @[string](
    "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"
  ) // end of [var]
//
  var !p_clo with pf_clo = @lam // this closure is stack-allocated
    (i: sizeLt 12, x: &string): void =<clo1> (if i > 0 then print ", "; print x)
  // end of [var]
  val () = array_ptr_iforeach_clo<string> (!p_arr, !p_clo, 12)
//
  val () = print_newline ()
in
  // empty
end // end of [print_month_names]

Note that the keyword @lam (instead of lam) is used here to indicate that the closure is constructed in the stack frame of the function print_month_names.

<<< PreviousHome 
Cast FunctionsUp