[Agda] lists/vectors (interfacing with untrusted code)

[Amr Sabry]

I have obviously already interfaced with the Haskell code. Perhaps
showing the code would help:

I have this Agda function:

  swap : Vector HBit 32 -> Vector HBit 32

where HBit is essentially a bool with constructors O and I.

Now I want to interact with it from the command line.

I write some trivial Haskell code in PiLoop to read a string and convert
it to something of type [Bit] using a function called string2bitlist32

{-# IMPORT PiLoop #-} 

{-# COMPILED_DATA Bit PiLoop.HBit PiLoop.O PiLoop.I #-}

data Unit : Set where
  unit : Unit
{-# COMPILED_DATA Unit () () #-}

bit2char : Bit -> Char
bit2char O = '0'
bit2char I = '1'

bitvec2string : {n : ℕ} -> Vec Bit n -> S.String
bitvec2string bs = S.fromList (L.map bit2char (toList bs))

postulate string2bitlist32 : S.String -> L.List Bit 
{-# COMPILED string2bitlist32 PiLoop.string2bitlist32 #-}

postulate ainteract : (S.String -> S.String) -> Prim.IO Unit
{-# COMPILED ainteract interact #-}

bitlist2string : L.List Bit -> S.String
bitlist2string xs = S.fromList (L.map bit2char xs)

-- Now I need to take the result of the Haskell function
-- string2bitlist32 which we know is of length 32 and cast it to 'Vec
-- Bit 32'. If I can do that then I can write:

main = ainteract (\s -> bitvec2string (swab (CAST (string2bitlist32 s))))

If this approach is viable, I need that CAST. 

--Amr