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

[Amr Sabry]

... because Agda complains that the type Vec cannot be translated to a
Haskell type. This seems to be a general problem with the way I am
approaching interfacing with untrusted code: typically I would expect
the Agda type to be something fancy that doesn't correspond to something
much less precise on the Haskell side.

--Amr

gallais @ ensl.org <guillaume.allais at ens-lyon.org> wrote:

> > 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