Data.Array

Data.Array.fm

import Data.Nat
import Data.InductionTree

Array : {A : Type, n : Nat} -> Type
  case/Nat n
  | succ => [x : Array(A, n.pred), Array(A, n.pred)]
  | zero => A
  : Type

// ::::::::::
// :: Fold ::
// ::::::::::

fold :
  { N  : Ind2
  , ~A : Type
  , ~B : Type
  , id : !(A -> B)
  , op : !(B -> B -> B)
  } -> ! { arr : Array(A, $ind2_depth(N)) } -> B
  dup op   = op
  dup id   = id
  let moti = {n} Array(A, $ind2_depth(n)) -> B
  let step = {~n, a, b, arr}
    get [x, y] = arr
    op(a(x), b(y))
  let base = {n} id(n)
  dup fold = (use(N))(~moti, #step, #base)
  # {arr} fold(arr)

// :::::::::::
// :: Query ::
// :::::::::::

Query : {A : Type, n : Nat} -> Type
  Array(A, n) -> [:A, Array(A, n)]

QueryBuilder : {A : Type, n : Nat} -> Type
  {~K : Type, edit : Query(A,n) -> K} -> K

query_builder.zero : {~A : Type, query : A -> [:A, A]} -> QueryBuilder(A, zero)
  {~K, edit} edit(query)

query_builder.succ :
  { ~A    : Type
  , ~n    : -Nat
  , side  : Num
  , build : QueryBuilder(A, +n)
  } -> QueryBuilder(A, succ(+n))
  {~K, edit}
  let F2 = &Query(&A,succ(+n))
  let f =
    if side: {arr : Array(A, succ(+n)), fn : Query(A,+n)}
      get [a, b] = arr
      get [w, b] = fn(b)
      [w, [a, b]]
    else:    {arr : Array(A, succ(+n)), fn : Query(A, +n)}
      get [a, b] = arr
      get [w, a] = fn(a)
      [w, [a, b]]
  edit(build(~&Query(&A,succ(+n)), {fn, arr} f(arr,fn)))

#query_builder*N : 
  ! {~A     : Type
    , path  : Num
    , query : A -> [:A, A]
    } -> [path : Num, QueryBuilder(A, $nat(N))]
  get [x, b] = query_builder(~&A, path, query)
  cpy rest   = x
  [ rest .>>>. 1
  , query_builder.succ(~&A, ~%$nat(+N), rest .&. 1, b)
  ]
halt:
  [path, query_builder.zero(~&A, query)]

//#query : 
//  {N : Ind} -> 
//  ! {~A     : Type
//    , path  : Num
//    , query : A -> [:A, A]
//    , array : Array(A, $nat(N))
//    } -> [arr : Array(A, $nat(N)), A]
//  let build  = $query_builder(N)
//  let fn     = snd(build(~&A, path, query))
//  get [a, b] = fn(~&Query(A,$nat(N)), {x}x, array)
//  [b, a]

#query :
  { N : Ind
  } ->
  ! {~A     : Type
    , path  : Num
    , query : A -> [:A, A]
    } -> Query(A,$nat(N))
  let build  = $query_builder(N)
  let fn     = snd(build(~&A, path, query))
  fn(~&Query(A,$nat(N)), {x}x)

#query.test : ![:Num, Array(Num, 0n4)]
  let arr = [[[[0,1],[2,3]],[[4,5],[6,7]]], [[[8,9],[10,11]],[[12,13],[14,15]]]]
  let qry = {x} cpy x = x; [x, x .+. 100] // adds 100 to elem, returns old value
  get [a, arr] = ($query*4)(~Num,  4, qry, arr)
  get [b, arr] = ($query*4)(~Num,  8, qry, arr)
  get [c, arr] = ($query*4)(~Num, 12, qry, arr)
  [a .+. b .+. c, arr]

// Sets value at position to `val`, returns old value
#set :
  { N    : Ind
  , ~A   : Type
  , copy : ! A -> [:A,A]
  } ->
  ! { path : Num
    , val : A
    } -> Query(A, $nat(N))
  ($query(N))(~&A, path, {x} [x, val])

// Mutates value at position with `fun`, returns old value
#mut :
  { N    : Ind
  , ~A   : Type
  , copy : ! A -> [:A,A]
  } ->
  !{ path : Num
   , fun : A -> A
   } -> Query(A, $nat(N))
  ($query(N))(~&A, path, {x} get [a,b] = ($#copy)(x); [a, fun(b)])

// Gets the value at position `val`
#got :
  { N    : Ind
  , ~A   : Type
  , copy : ! A -> [:A,A]
  } ->
  ! { path : Num
    } -> Query(A, $nat(N))
  ($query(N))(~&A, path, {x} ($#copy)(x))

#array.test : ![:Num, :Num, :Num, :Num, Num]
  // Prepares functions
  let cop = {x : Num} cpy x = x; [x, x]
  let set = set*8(~Num, #cop)
  let mut = mut*8(~Num, #cop)
  let got = got*8(~Num, #cop)

  // Creates array
  let arr = [[[[0,1],[2,3]],[[4,5],[6,7]]], [[[8,9],[10,11]],[[12,13],[14,15]]]]
  let arr = [arr, arr]
  let arr = [arr, arr]
  let arr = [arr, arr]
  let arr = [arr, arr]

  // Performs many operations
  get [a, arr] = ($set)(2, 100, arr)      // a = arr[2]; arr[2] = 100
  get [b, arr] = ($mut)(4, .+.(100), arr) // b = arr[4]; arr[4] = arr[4] + 100
  get [c, arr] = ($got)(2, arr)           // c = arr[2]
  get [d, arr] = ($got)(4, arr)           // d = arr[4]
  get [e, arr] = ($got)(6, arr)           // e = arr[6]
  get [e, arr] = ($got)(6, arr)           // e = arr[6]
  get [e, arr] = ($got)(6, arr)           // e = arr[6]
  get [e, arr] = ($got)(6, arr)           // e = arr[6]

  // Returns numbers
  [a, b, c, d, e]