test025.idr

module Main

import Effects
import Effect.Memory
import Control.IOExcept
import Data.Vect

MemoryIO : Type -> Type -> Type -> Type
MemoryIO td ts r = { [ Dst ::: RAW_MEMORY td
                     , Src ::: RAW_MEMORY ts ] } Eff r

inpVect : Vect 5 Bits8
inpVect = map prim__truncInt_B8 [0, 1, 2, 3, 5]

sub1 : Vect n Bits8 -> Vect n Bits8
sub1 xs = map (prim__truncInt_B8 . (\ x => x - 1) . prim__zextB8_Int) xs

testMemory : MemoryIO () () (Vect 4 Int)
testMemory = do Src :- allocate 5
                Src :- poke 0 inpVect Oh
                Dst :- allocate 5
                Dst :- initialize (prim__truncInt_B8 1) 2 Oh
                move 2 2 3 Oh Oh
                Src :- free
                end <- Dst :- peek 4 (S Z) Oh
                Dst :- poke 4 (sub1 end) Oh
                res <- Dst :- peek 1 (S(S(S(S Z)))) Oh
                Dst :- free
                return (map (prim__zextB8_Int) res)

main : IO ()
main = ioe_run (runInit [Dst := (), Src := ()] testMemory)
               (\err => printLn err) (\ok => printLn ok)