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

[gallais at ensl.org]

What you are looking for is the COMPILED pragma:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ForeignFunctionInterface#COMPILED

--
gallais


On 15 October 2012 13:02, Amr Sabry <sabry at cs.indiana.edu> wrote:
> Hi,
>
> I don't want something of type:
>
>>   (xs : List Bool) -> Vector Bool (length xs)
>
> I really am looking for something of type:
>
>>   (xs : List Bool) -> Vector Bool 32
>
> More generally how do you guys interface between untrusted code and Agda
> code???
>
> --Amr
>
> Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com> wrote:
>
>> On Sat, Oct 13, 2012 at 7:45 PM, Amr Sabry <sabry at cs.indiana.edu> wrote:
>> > Hi all,
>> >
>> > Probably a fairly basic question...
>> >
>> > Say I have an Agda module that works with things of type
>> >
>> >   Vector Bool 32
>> >
>> > How does one write a complete program, i.e., an external Haskell
>> > wrapper, that interacts with this module? I am thinking of a Haskell
>> > wrapper that reads an arbitrary string, checks that the string length is
>> > 32, and if so calls the Agda code. This approach requires some
>> > function:
>> >
>> >   (xs : List Bool) -> Vector Bool 32
>>
>> I guess you can use the function fromList
>> http://www.cse.chalmers.se/~nad/listings/lib-0.6/Data.Vec.html#4403
>> instead.
>>
>> --
>> Andrés
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda