Re: [isabelle] Parallel sequences
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
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and