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


On 12 May 2014 20:24, "Makarius" <makarius at> 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
> 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.