a3/code/Generics/_Array.dcl

   1 definition module _Array
   2
   3 import StdArray
   4
   5 createArrayUnsafe :: .Int -> u:(a v:b) | Array a b, [u <= v]
   6
   7
   8 /*
   9 class UnsafeArray a e | Array a e where
  10         unsafeCreate                            :: !Int                         -> *(a .e)
  11         unsafeUselect                           :: !u:(a .e) !Int       -> *(.e, !u:(a .e))
  12
  13 instance UnsafeArray {} e, {!} e
  14
  15 mapArray :: (u:a -> v:b) w:(c u:a) -> x:(d v:b) | UnsafeArray c a & UnsafeArray d b, [w <= u,x <= v]
  16 mapArrayLSt :: (u:a -> .(.b -> (v:c,.b))) w:(d u:a) .b -> (x:(e v:c),.b) | UnsafeArray d a & UnsafeArray e c, [w <= u,x <= v]
  17 mapArrayRSt :: (u:a -> .(.b -> (v:c,.b))) w:(d u:a) .b -> (x:(e v:c),.b) | UnsafeArray d a & UnsafeArray e c, [w <= u,x <= v]
  18 */
  19
  20 class UnsafeArray a where
  21         unsafeCreate                            :: !Int                         -> *(a .e)
  22         unsafeUselect                           :: !u:(a .e) !Int       -> *(.e, !u:(a .e))
  23
  24 instance UnsafeArray {}, {!}
  25
  26 mapArray :: (u:a -> v:b) w:(c u:a) -> x:(d v:b) | Array d b & UnsafeArray c & UnsafeArray d & Array c a, [w <= u,x <= v]
  27 mapArrayLSt :: (u:a -> .(.b -> (v:c,.b))) w:(d u:a) .b -> (x:(e v:c),.b) | Array e c & UnsafeArray d & UnsafeArray e & Array d a, [w <= u,x <= v]
  28 mapArrayRSt :: (u:a -> .(.b -> (v:c,.b))) w:(d u:a) .b -> (x:(e v:c),.b) | Array e c & UnsafeArray d & UnsafeArray e & Array d a, [w <= u,x <= v]
  29 reduceArray :: ((.a -> u:(b -> b)) -> .(b -> .(c -> .a))) (.a -> u:(b -> b)) b .(d c) -> b | Array d c
  30 reduceArrayLSt :: (u:a -> .(.b -> .b)) v:(c u:a) .b -> .b | UnsafeArray c & Array c a, [v <= u]
  31 reduceArrayRSt :: (u:a -> .(.b -> .b)) v:(c u:a) .b -> .b | UnsafeArray c & Array c a, [v <= u]