Commit 73c68674 authored by Artem Alimarine's avatar Artem Alimarine

no message

parent 6cd38a5f
definition module GenEq
import StdGeneric
generic gEq a :: a a -> Bool
// base cases
derive gEq Int, Char, Bool, Real, UNIT, PAIR, EITHER, CONS, FIELD, {}, {!}
// standard types
derive gEq [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
(===) infix 4 :: a a -> Bool | gEq{|*|} a
(=!=) infix 4 :: a a -> Bool | gEq{|*|} a
implementation module GenEq
import StdGeneric, StdBool, StdChar, StdInt, StdReal, StdClass, StdArray
generic gEq a :: a a -> Bool
gEq{|Int|} x y = x == y
gEq{|Char|} x y = x == y
gEq{|Bool|} x y = x == y
gEq{|Real|} x y = x == y
gEq{|UNIT|} UNIT UNIT = True
gEq{|PAIR|} fx fy (PAIR x1 y1) (PAIR x2 y2) = fx x1 x2 && fy y1 y2
gEq{|EITHER|} fl fr (LEFT x) (LEFT y) = fl x y
gEq{|EITHER|} fl fr (RIGHT x) (RIGHT y) = fr x y
gEq{|EITHER|} fl fr _ _ = False
gEq{|CONS|} f (CONS x) (CONS y) = f x y
gEq{|FIELD|} f (FIELD x) (FIELD y) = f x y
gEq{|{}|} f xs ys = eqArray f xs ys
gEq{|{!}|} f xs ys = eqArray f xs ys
derive gEq [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
(===) infix 4 :: a a -> Bool | gEq{|*|} a
(===) x y = gEq{|*|} x y
(=!=) infix 4 :: a a -> Bool | gEq{|*|} a
(=!=) x y = not (x === y)
eqArray f xs ys = size xs == size ys && eq 0 (size xs) xs ys
where
eq i n xs ys
| i == n = True
| i < n = f xs.[i] ys.[i] && eq (inc i) n xs ys
definition module GenIO
import StdMaybe
import StdGeneric
:: Pos
//--------------------------------------------------------------------
class OStream s where
streamWrite :: Char *s -> *s
class IStream s where
streamRead :: *s -> (Maybe Char, *s)
streamEnd :: *s -> (Bool, *s)
// stream with positioning
class RandomStream s where
streamGetPos :: *s -> (Pos, *s)
streamSetPos :: Pos *s -> *s
//--------------------------------------------------------------------
:: *StringStream
instance OStream StringStream, File
instance IStream StringStream, File
instance RandomStream StringStream, File
//--------------------------------------------------------------------
:: GenIOEnv // abstract environement
generic gOutput a :: GenIOEnv -> (a -> (*s -> *s)) | IStream s & RandomStream s
generic gInput a :: GenIOEnv -> (*s -> (Maybe a, *s)) | IStream s & RandomStream s
implementation module GenIO
import StdEnv, StdGeneric, StdMaybe
//--------------------------------------------------------------------------------
($) infixl 9
($) x y = y o x
(@) infix 8
(@) x y = x y
:: Pos :== Int
//--------------------------------------------------------------------------------
:: *StringStream = { ss_str :: !*String, ss_pos :: !Pos}
instance IStream StringStream where
streamRead s=:{ss_pos, ss_str}
#! size_str = size ss_str
| size_str == ss_pos
= (Nothing, {s & ss_str = ss_str})
| otherwise
#! ch = ss_str.[ss_pos]
= (Just ch, {s & ss_str = ss_str, ss_pos = inc ss_pos})
streamEnd s=:{ss_pos, ss_str}
#! size_str = size ss_str
= (size_str == ss_pos, {s & ss_str = ss_str})
instance OStream StringStream where
streamWrite ch s=:{ss_str, ss_pos}
#! new_str = realloc_if_needed ss_pos ss_str
= {s & ss_str = {new_str & [ss_pos] = ch}, ss_pos = inc ss_pos}
where
realloc_if_needed :: Int u:String -> v:String, [u <= v]
realloc_if_needed pos str
#! size_str = size str
| pos == size_str
#! new_str = createArray ((size_str + 1) * 3 /2) ' '
#! (new_str, str) = fill 0 size_str new_str str
= new_str
| otherwise
= str
fill i n new_str str
| i == n
= (new_str, str)
| otherwise
#! (ch, str) = str![i]
= ({new_str & [i] = ch}, str)
instance RandomStream StringStream where
streamGetPos s=:{ss_pos} = (ss_pos, s)
streamSetPos pos s = {s & ss_pos = pos}
//-----------------------------------------------------------------------
instance IStream File where
streamRead f
# (ok, c, f) = freadc f
| ok
= (Just c, f)
= (Nothing, f)
streamEnd f = fend f
instance OStream File where
streamWrite c f = fwritec c f
instance RandomStream File where
streamSetPos pos f
# (ok, f) = fseek f FSeekSet pos
| not ok
= abort "fseek failed\n"
= f
streamGetPos f = fposition f
//--------------------------------------------------------------------------------
:: Assoc = AssocNone | AssocLeft | AssocRight
:: GenIOEnv
= GIOE_None // initial env
| GIOE_Record // record constructor
| GIOE_Tuple // tuple constructor
| GIOE_Nonfix // normal nonfix constructor
| GIOE_Infix String Assoc Int // infix constructor
//--------------------------------------------------------------------------------
generic gOutput a :: GenIOEnv -> (a -> (*s -> *s)) | IStream s & RandomStream s
/*
gOutput{|Int|} env = undef
gOutput{|Real|} env = undef
gOutput{|Char|} env = undef
gOutput{|Bool|} env = undef
gOutput{|String|} env = undef
gOutput{|UNIT|} env = undef
gOutput{|PAIR|} fx fy env = undef
gOutput{|EITHER|} fl fr env = undef
gOutput{|CONS of d|} f env = undef
gOutput{|FIELD of d|} f env = undef
gOutput{|[]|} f env = undef
gOutput{|{}|} f env = undef
gOutput{|{!}|} f env = undef
*/
//--------------------------------------------------------------------------------
generic gInput a :: GenIOEnv -> (*s -> (Maybe a, *s)) | IStream s & RandomStream s
/*
gInput{|Int|} env = undef
gInput{|Real|} env = undef
gInput{|Char|} env = undef
gInput{|Bool|} env = undef
gInput{|String|} env = undef
gInput{|UNIT|} env = undef
gInput{|PAIR|} fx fy env = undef
gInput{|EITHER|} fl fr env = undef
gInput{|CONS of d|} f env = undef
gInput{|FIELD of d|} f env = undef
gInput{|[]|} f env = undef
gInput{|{}|} f env = undef
gInput{|{!}|} f env = undef
*/
//--------------------------------------------------------------------------------
definition module GenLexOrd
import StdGeneric, GenEq
:: LexOrd = LT |EQ | GT
derive gEq LexOrd
generic gLexOrd a b :: a b -> LexOrd
// base cases
derive gLexOrd Char, Bool, Int, Real, UNIT, PAIR, EITHER, FIELD, CONS, [], {}, {!}
// standard types
derive gLexOrd (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
(=?=) infix 4 :: a a -> LexOrd | gLexOrd{|*|} a
implementation module GenLexOrd
import StdInt, StdBool, StdReal, StdChar, StdClass, StdArray
import StdGeneric, GenEq
:: LexOrd = LT |EQ | GT
derive gEq LexOrd
generic gLexOrd a b :: a b -> LexOrd
gLexOrd{|Int|} x y
| x == y = EQ
| x < y = LT
= GT
gLexOrd{|Bool|} True True = EQ
gLexOrd{|Bool|} False True = LT
gLexOrd{|Bool|} True False = GT
gLexOrd{|Bool|} False False = EQ
gLexOrd{|Real|} x y
| x == y = EQ
| x < y = LT
= GT
gLexOrd{|Char|} x y
| x == y = EQ
| x < y = LT
= GT
gLexOrd{|UNIT|} UNIT UNIT = EQ
gLexOrd{|PAIR|} fx fy (PAIR x1 y1) (PAIR x2 y2) = case fx x1 x2 of
EQ -> fy y1 y2
LT -> LT
GT -> GT
gLexOrd{|EITHER|} fl fr (LEFT x) (LEFT y) = fl x y
gLexOrd{|EITHER|} fl fr (LEFT x) (RIGHT y) = LT
gLexOrd{|EITHER|} fl fr (RIGHT x) (LEFT y) = GT
gLexOrd{|EITHER|} fl fr (RIGHT x) (RIGHT y) = fr x y
gLexOrd{|CONS|} f (CONS x) (CONS y) = f x y
gLexOrd{|FIELD|} f (FIELD x) (FIELD y) = f x y
// Instance on standard lists is needed because
// standard lists have unnatural internal ordering of constructors: Cons < Nil,
// i.e Cons is LEFT and Nil is RIGHT in the generic representation.
// We want ordering Nil < Cons
gLexOrd{|[]|} f [] [] = EQ
gLexOrd{|[]|} f [] _ = LT
gLexOrd{|[]|} f _ [] = GT
gLexOrd{|[]|} f [x:xs] [y:ys] = gLexOrd{|*->*->*|} f (gLexOrd{|*->*|} f) (PAIR x xs) (PAIR y ys)
gLexOrd{|{}|} f xs ys = lexOrdArray f xs ys
gLexOrd{|{!}|} f xs ys = lexOrdArray f xs ys
// standard types
derive gLexOrd (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
(=?=) infix 4 :: a a -> LexOrd | gLexOrd{|*|} a
(=?=) x y = gLexOrd{|*|} x y
lexOrdArray f xs ys
#! size_xs = size xs
#! size_ys = size ys
| size_xs < size_ys = LT
| size_xs > size_ys = GT
| otherwise = lexord 0 size_xs xs ys
where
lexord i n xs ys
| i == n = EQ
| otherwise = case f xs.[i] ys.[i] of
LT -> LT
GT -> GT
EQ -> lexord (inc i) n xs ys
definition module GenLib
import StdGeneric
import GenEq
import GenLexOrd
import GenMap
import GenMapSt
import GenReduce
import GenZip
implementation module GenLib
\ No newline at end of file
definition module GenMap
import StdGeneric
generic gMap a b :: .a -> .b
derive gMap c, PAIR, EITHER, CONS, FIELD, {}, {!}
derive gMap [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
implementation module GenMap
import StdClass, StdArray, StdInt
import StdGeneric, _Array
generic gMap a b :: .a -> .b
gMap{|c|} x = x
gMap{|PAIR|} fx fy (PAIR x y) = PAIR (fx x) (fy y)
gMap{|EITHER|} fl fr (LEFT x) = LEFT (fl x)
gMap{|EITHER|} fl fr (RIGHT x) = RIGHT (fr x)
gMap{|CONS|} f (CONS x) = CONS (f x)
gMap{|FIELD|} f (FIELD x) = FIELD (f x)
gMap{|{}|} f xs = mapArray f xs
gMap{|{!}|} f xs = mapArray f xs
derive gMap [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
definition module GenMapSt
import StdGeneric
generic gMapLSt a b :: .a .st -> (.b, .st)
derive gMapLSt c, PAIR, EITHER, FIELD, CONS, {}, {!}
derive gMapLSt [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
generic gMapRSt a b :: .a .st -> (.b, .st)
derive gMapRSt c, PAIR, EITHER, FIELD, CONS, {}, {!}
derive gMapRSt [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
implementation module GenMapSt
import StdGeneric, _Array
derive bimap (,)
generic gMapLSt a b :: .a .st -> (.b, .st)
gMapLSt{|c|} x st = (x, st)
gMapLSt{|PAIR|} fx fy (PAIR x y) st
# (x, st) = fx x st
# (y, st) = fy y st
= (PAIR x y, st)
gMapLSt{|EITHER|} fl fr x st = mapStEITHER fl fr x st
gMapLSt{|CONS|} f x st = mapStCONS f x st
gMapLSt{|FIELD|} f x st = mapStFIELD f x st
gMapLSt{|{}|} f x st = mapArrayLSt f x st
gMapLSt{|{!}|} f x st = mapArrayLSt f x st
derive gMapLSt [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
generic gMapRSt a b :: .a .st -> (.b, .st)
gMapRSt{|c|} x st = (x, st)
gMapRSt{|PAIR|} fx fy (PAIR x y) st
# (y, st) = fy y st
# (x, st) = fx x st
= (PAIR x y, st)
gMapRSt{|EITHER|} fx fy x st = mapStEITHER fx fy x st
gMapRSt{|CONS|} f x st = mapStCONS f x st
gMapRSt{|FIELD|} f x st = mapStFIELD f x st
gMapRSt{|{}|} f x st = mapArrayRSt f x st
gMapRSt{|{!}|} f x st = mapArrayRSt f x st
derive gMapRSt [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
mapStEITHER fl fr (LEFT x) st
# (x, st) = fl x st
= (LEFT x, st)
mapStEITHER fl fr (RIGHT x) st
# (x, st) = fr x st
= (RIGHT x, st)
mapStCONS f (CONS x) st
# (x, st) = f x st
= (CONS x, st)
mapStFIELD f (FIELD x) st
# (x, st) = f x st
= (FIELD x, st)
\ No newline at end of file
definition module GenReduce
import StdGeneric
generic gReduce t :: (a a -> a) a t -> a
derive gReduce c, PAIR, EITHER, CONS, FIELD
derive gReduce [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
generic gReduceRSt t :: .t .st -> .st
derive gReduceRSt c, PAIR, EITHER, CONS, FIELD
derive gReduceRSt [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
generic gReduceLSt t :: .t .st -> .st
derive gReduceLSt c, PAIR, EITHER, CONS, FIELD
derive gReduceLSt [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
\ No newline at end of file
implementation module GenReduce
import StdGeneric, _Array
// or crush
generic gReduce t :: (a a -> a) a t -> a
gReduce{|c|} op e x = e
gReduce{|PAIR|} fx fy op e (PAIR x y) = op (fx op e x) (fy op e y)
gReduce{|EITHER|} fl fr op e (LEFT x) = fl op e x
gReduce{|EITHER|} fl fr op e (RIGHT x) = fr op e x
gReduce{|CONS|} f op e (CONS x) = f op e x
gReduce{|FIELD|} f op e (FIELD x) = f op e x
gReduce{|{}|} f op e x = reduceArray f op e x
gReduce{|{!}|} f op e x = reduceArray f op e x
derive gReduce [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
generic gReduceRSt t :: .t .st -> .st
gReduceRSt{|c|} x st = st
gReduceRSt{|PAIR|} fx fy (PAIR x y) st = fx x (fy y st)
gReduceRSt{|EITHER|} fl fr x st = reduceEITHER fl fr x st
gReduceRSt{|CONS|} f (CONS x) st = f x st
gReduceRSt{|FIELD|} f (FIELD x) st = f x st
gReduceRSt{|{}|} f xs st = reduceArrayRSt f xs st
gReduceRSt{|{!}|} f xs st = reduceArrayRSt f xs st
derive gReduceRSt [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
generic gReduceLSt t :: .t .st -> .st
gReduceLSt{|c|} x st = st
gReduceLSt{|PAIR|} fx fy (PAIR x y) st = fy y (fx x st)
gReduceLSt{|EITHER|} fl fr x st = reduceEITHER fl fr x st
gReduceLSt{|CONS|} f (CONS x) st = f x st
gReduceLSt{|FIELD|} f (FIELD x) st = f x st
gReduceLSt{|{}|} f xs st = reduceArrayLSt f xs st
gReduceLSt{|{!}|} f xs st = reduceArrayLSt f xs st
derive gReduceLSt [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
reduceEITHER fl fr (LEFT x) st = fl x st
reduceEITHER fl fr (RIGHT x) st = fr x st
\ No newline at end of file
definition module GenZip
import StdMaybe, StdGeneric
generic gZip a b c :: .a .b -> .c
derive gZip Int, Bool, Char, Real, UNIT, EITHER, PAIR, CONS, FIELD
derive gZip [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
generic gMaybeZip a b c :: .a .b -> Maybe .c
derive gMaybeZip Int, Char, Bool, Real, UNIT, EITHER, PAIR, CONS, FIELD
derive gMaybeZip [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
implementation module GenZip
import StdGeneric
import StdEnv
import StdMaybe
derive bimap Maybe
generic gZip a b c :: .a .b -> .c
gZip{|Int|} x y = if (x == y) x (abort "zip Int failed\n")
gZip{|Bool|} x y = if (x == y) x (abort "zip Bool failed\n")
gZip{|Char|} x y = if (x == y) x (abort "zip Char failed\n")
gZip{|Real|} x y = if (x == y) x (abort "zip Real failed\n")
gZip{|UNIT|} UNIT UNIT = UNIT
gZip{|PAIR|} fx fy (PAIR x1 y1) (PAIR x2 y2) = PAIR (fx x1 x2) (fy y1 y2)
gZip{|EITHER|} fl fr (LEFT x) (LEFT y) = LEFT (fl x y)
gZip{|EITHER|} fl fr (RIGHT x) (RIGHT y) = RIGHT (fr x y)
gZip{|EITHER|} fl fr _ _ = abort "gZip failed: EITHER does not match\n"
gZip{|CONS|} f (CONS x) (CONS y) = CONS (f x y)
gZip{|FIELD|} f (FIELD x) (FIELD y) = FIELD (f x y)
derive gZip [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
generic gMaybeZip a b c :: .a .b -> Maybe .c
gMaybeZip{|Int|} x y = if (x == y) (Just x) Nothing
gMaybeZip{|Bool|} x y = if (x == y) (Just x) Nothing
gMaybeZip{|Char|} x y = if (x == y) (Just x) Nothing
gMaybeZip{|Real|} x y = if (x == y) (Just x) Nothing
gMaybeZip{|UNIT|} UNIT UNIT = Just UNIT
gMaybeZip{|PAIR|} fx fy (PAIR x1 y1) (PAIR x2 y2) = zipMaybe PAIR (fx x1 x2) (fy y1 y2)
gMaybeZip{|EITHER|} fl fr (LEFT x) (LEFT y) = mapMaybe LEFT (fl x y)
gMaybeZip{|EITHER|} fl fr (RIGHT x) (RIGHT y) = mapMaybe RIGHT (fr x y)
gMaybeZip{|EITHER|} fl fr _ _ = Nothing
gMaybeZip{|CONS|} f (CONS x) (CONS y) = mapMaybe CONS (f x y)
gMaybeZip{|FIELD|} f (FIELD x) (FIELD y) = mapMaybe FIELD (f x y)
derive gMaybeZip [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
zipMaybe :: .(.a -> .(.b -> .c)) !(Maybe .a) (Maybe .b) -> (Maybe .c)
zipMaybe f (Just x) (Just y) = Just (f x y)
zipMaybe f _ _ = Nothing
definition module _Array
import StdArray
/*
class UnsafeArray a e | Array a e where
unsafeCreate :: !Int -> *(a .e)
unsafeUselect :: !u:(a .e) !Int -> *(.e, !u:(a .e))
instance UnsafeArray {} e, {!} e
mapArray :: (u:a -> v:b) w:(c u:a) -> x:(d v:b) | UnsafeArray c a & UnsafeArray d b, [w <= u,x <= v]
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]
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]
*/
class UnsafeArray a where
unsafeCreate :: !Int -> *(a .e)
unsafeUselect :: !u:(a .e) !Int -> *(.e, !u:(a .e))
instance UnsafeArray {}, {!}
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]
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]
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]
reduceArray :: ((.a -> u:(b -> b)) -> .(b -> .(c -> .a))) (.a -> u:(b -> b)) b .(d c) -> b | Array d c
reduceArrayLSt :: (u:a -> .(.b -> .b)) v:(c u:a) .b -> .b | UnsafeArray c & Array c a, [v <= u]
reduceArrayRSt :: (u:a -> .(.b -> .b)) v:(c u:a) .b -> .b | UnsafeArray c & Array c a, [v <= u]
implementation module _Array
import StdArray, StdInt, StdClass
instance UnsafeArray {} where
unsafeCreate size =
code
{
create_array_ _ 1 0
}
unsafeUselect arr index =
code
{
push_a 0
select _ 1 0
}
instance UnsafeArray {!} where
unsafeCreate size =
code
{
create_array_ _ 1 0
}
unsafeUselect arr index =
code
{
push_a 0
select _ 1 0
}
//mapArray :: (u:a -> v:b) w:(c u:a) -> x:(d v:b) | UnsafeArray c a & UnsafeArray d b, [w <= u,x <= v]
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]
mapArray f xs
#! (size_xs, xs) = usize xs
#! (xs, ys) = map f 0 size_xs xs (unsafeCreate size_xs)
= ys
where
map f i n xs ys
| i == n
= (xs, ys)
| otherwise
#! (x, xs) = unsafeUselect xs i
#! ys = update ys i (f x)
= map f (inc i) n xs ys
//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]
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]
mapArrayLSt f xs st
#! (size_xs, xs) = usize xs
#! (xs, ys, st) = map f 0 size_xs xs (unsafeCreate size_xs) st
= (ys, st)
where
map f i n xs ys st
| i == n
= (xs, ys, st)
| otherwise
#! (x, xs) = unsafeUselect xs i
#! (y, st) = f x st
#! ys = update ys i y
= map f (inc i) n xs ys st
//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]
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]
mapArrayRSt f xs st
#! (size_xs, xs) = usize xs
#! (xs, ys, st) = map f (size_xs - 1) xs (unsafeCreate size_xs) st
= (ys, st)
where
map f i xs ys st
| i < 0
= (xs, ys, st)
| otherwise
#! (x, xs) = unsafeUselect xs i
#! (y, st) = f x st
#! ys = update ys i y
= map f (dec i) xs ys st
reduceArray :: ((.a -> u:(b -> b)) -> .(b -> .(c -> .a))) (.a -> u:(b -> b)) b .(d c) -> b | Array d c
reduceArray f op e xs
= reduce f 0 (size xs) op e xs
where
reduce f i n op e xs
| i == n
= e
| otherwise
= op (f op e xs.[i]) (reduce f (inc i) n op e xs)
reduceArrayLSt :: (u:a -> .(.b -> .b)) v:(c u:a) .b -> .b | UnsafeArray c & Array c a, [v <= u]
reduceArrayLSt f xs st
#! (size_xs, xs) = usize xs
#! (xs, st) = reduce f 0 size_xs xs st
= st
where
reduce f i n xs st
| i == n
= (xs, st)
| otherwise
#! (x, xs) = unsafeUselect xs i
= reduce f (inc i) n xs (f x st)
reduceArrayRSt :: (u:a -> .(.b -> .b)) v:(c u:a) .b -> .b | UnsafeArray c & Array c a, [v <= u]
reduceArrayRSt f xs st
#! (size_xs, xs) = usize xs
#! (xs, st) = reduce f (dec size_xs) xs st
= st
where
reduce f i xs st
| i < 0
= (xs, st)
| otherwise
#! (x, xs) = unsafeUselect xs i