Re: [isabelle] Parallel sequences



Hi Omar,

Last year a student of mine implemented some parallel collection types
(including lazy sequences) on top of isaplib which is a small ML library
that is (mostly) source compatible with Isabelle/ML. You may find that code
useful:

https://github.com/iislucas/isaplib/tree/master/Concurrent

Best,

Aleks
On 12 May 2014 20:24, "Makarius" <makarius at sketis.net> wrote:

> On Mon, 12 May 2014, Omar Montano Rivas wrote:
>
>  I am currently working with sequences in Isabelle/ML
>> (src/Pure/General/seq.ML) and I was wondering if there is any support for
>> parallel execution of functions such as exists or forall for sequences,
>> e.g. ('a -> bool) -> 'a seq -> bool. I can see there is a library for
>> parallel lists (src/Pure/Concurrent/par_list.ML) but can not find
>> something similar for sequences.
>>
>
> The sequences of structure Seq are unbounded and lazy, and usually
> explored only to a certain point and then abandonned.
>
> It is not immediately obvious what should happen in parallel here, i.e.
> you need to determine more clearly what you need, and then it is probably
> feasible to imitate the Par_List implementation.
>
> The regular sequences are at the bottom of tactics and tacticals in
> Isabelle.  In http://isabelle.in.tum.de/repos/isabelle/file/
> Isabelle2013-2/src/Pure/goal.ML#l339 there are a few parallel combinators
> for that, but I avoided the above questions by restricting to result
> sequence to zero or one result (via DETERM / SINGLE).
>
>
>         Makarius
>
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.