array.timl

(* Operations for length-indexed arrays *)

structure Array = struct

open Basic
open Nat
open List

fun empty_array ['a] () return array 'a {0} = __&empty_array
fun array ['a] {n : Nat} (len : nat {n}, v : 'a) = __&array (len, v)
fun length {len : Nat} (a : array _ {len}) = __&array_length a
       
fun sub ['a] {len who : Nat} {who < len} (a : array 'a {len}, n : nat {who}) return 'a using 0.0 =
    __&sub (a, n)

fun update ['a] {len who : Nat} {who < len} (a : array 'a {len}, n : nat {who}, x : 'a) return unit using 0.0 =
    __&update (a, n, x)

fun fromList ['a] {len : Nat} (l : list 'a {len}) return array 'a {len} using 8.0 * $len + 1.0 =
  case l of
      [] => empty_array ()
    | _ :: _ =>
      let
        val len = List.length l
        val arr = array (len, hd l)
        fun loop {len2 i : Nat} {i + len2 = len} (ls : list _ {len2}, i : nat {i}) return using 3.0 * $len2 =
          case ls of
              [] => ()
            | x :: ls => update (arr, i, x); loop (ls, i #+ #1)
        val () = loop (l, #0)
      in
        arr
      end

(* val a : array int {_} = empty_array () *)
(* val a = array (#10, 1) *)
(* val _ = __&sub (a, #5) *)
(* val () = __&update (a, #5, 3) *)
(* val a = fromList [1, 2] *)
(* val () = __&halt a *)
        
(* todo: shouldn't use List.tabulate which incurs extra space usage *)
fun tabulate ['a] {len : Nat} {m : Time} (n : nat {len}, f : nat_less_than {len} -- m --> 'a) return array 'a {len} using (m + $12) * $len + $4 =
  fromList <| List.tabulate (n, f)

fun appi ['a] {m : Time} {len : Nat} (f : nat_less_than {len} * 'a -- m --> unit) (a : array 'a {len}) return unit using (m + $4) * $len + 2.0 =
  let
    fun loop {n | n <= len} (n : nat {n}) (* return using (m + 4.0) * $n *) =
      ifdec n #<= #0 then ()
      else
        let return using (m + 4.0) * $n
          val n' = n #- #1
        in
          f (NatLT n', sub (a, n')); loop n'
        end
  in
    loop <| length a
  end

fun app ['a] {m : Time} {len : Nat} (f : 'a -- m --> unit) (a : array 'a {len}) return unit using (m + $5) * $len + $4 =
  appi (fn (_, x) => f x) a

fun modifyi ['a] {m : Time} {len : Nat} (f : nat_less_than {len} * 'a -- m --> 'a) (a : array 'a {len}) return unit using (m + $5) * $len + 2.0 =
  let
    fun loop {n | n <= len} (n : nat {n}) (* return using (m + 4.0) * $n *) =
      ifdec n #<= #0 then ()
      else
        let return using (m + 5.0) * $n
          val n' = n #- #1
          val v = f (NatLT n', sub (a, n'))
          val () = update (a, n', v)
        in
          loop n'
        end
  in
    loop <| length a
  end

fun modify_ ['a] {m : Time} {len : Nat} (f : 'a -- m --> 'a) (a : array 'a {len}) return unit using (m + $6) * $len + 4.0 =
  modifyi (fn (_, x) => f x) a

fun foldri ['a 'b] {m : Time} {len : Nat} (f : nat_less_than {len} * 'a * 'b -- m --> 'b) (x : 'b) (a : array 'a {len}) return 'b using (m + $5) * $len + 2.0 =
  let
    fun loop {n | n <= len} (n : nat {n}, acc) (* return using (m + 4.0) * $n *) =
      ifdec n #<= #0 then acc
      else
        let return using (m + 5.0) * $n
          val n' = n #- #1
          val acc = f (NatLT n', sub (a, n'), acc)
        in
          loop (n', acc)
        end
  in
    loop (length a, x)
  end

fun foldr ['a 'b] {m : Time} (f : 'a * 'b -- m --> 'b) (acc : 'b) {len : Nat} (a : array 'a {len}) return 'b using (m + $6) * $len + 5.0 =
  foldri (fn (_, x, acc) => f (x, acc)) acc a
  
fun foldli ['a 'b] {m : Time} {len : Nat} (f : nat_less_than {len} * 'a * 'b -- m --> 'b) (x : 'b) (a : array 'a {len}) return 'b using (m + $5) * $len + 2.0 =
  let
    val len = length a
    fun loop {n | n <= len} (n : nat {n}, acc) (* return using (m + 4.0) * $n *) =
      ifdec n #>= len then acc
      else
        let return using (m + 5.0) * $(len - n)
          val acc = f (NatLT n, sub (a, n), acc)
        in
          loop (n #+ #1, acc)
        end
  in
    loop (#0, x)
  end

fun foldl ['a 'b] {m : Time} (f : 'a * 'b -- m --> 'b) (acc : 'b) {len : Nat} (a : array 'a {len}) return 'b using (m + $6) * $len + 5.0 =
  foldli (fn (_, x, acc) => f (x, acc)) acc a

fun find ['a] {m : Time} (f : 'a -- m --> bool) {len : Nat} (a : array 'a {len}) return option 'a using (m + $7) * $len + 8.0 =
  foldl (fn (x, acc) => case acc of SOME _ => acc | NONE => if f x then SOME x else NONE) NONE {_} a

fun exi_sts ['a] {m : Time} (f : 'a -- m --> bool) {len : Nat} (a : array 'a {len}) return bool using (m + $8) * $len + 8.0 =
  foldl (fn (x, acc) => acc || f x) false {_} a

fun all ['a] {m : Time} (f : 'a -- m --> bool) {len : Nat} (a : array 'a {len}) return bool using (m + $8) * $len + 8.0 =
  foldl (fn (x, acc) => acc && f x) true {_} a

fun toList ['a] {len : Nat} (a : array 'a {len}) return list 'a {len} using 3.0 * $len + 2.0 =
  let
    fun loop {n | n <= len} {acc_len | n + acc_len = len} (n : nat {n}, acc : list _ {acc_len}) (* return list _ {len} *) (* using (m + 4.0) * $n *) =
      ifdec n #<= #0 then acc : list _ {len}
      else
        let return list _ {len} using 3.0 * $n
          val n' = n #- #1
          val acc = sub (a, n') :: acc
        in
          loop (n', acc)
        end
  in
    loop (length a, [])
  end
    
end