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

[gallais at ensl.org]

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

Why not giving string2bitlist32 the type S.String -> Vec Bit 32 ?

--
gallais


On 15 October 2012 13:13, Amr Sabry <sabry at cs.indiana.edu> wrote:
> 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