2019-10-05 20:30:33 (GMT)
Hello everyone!
2019-10-05 21:17:32 (GMT)
howdy @Petar Vukmirovic :wave:
2019-10-05 21:17:54 (GMT)
Hi Simon!
2019-10-05 21:18:11 (GMT)
I was wondering if you know of any painless way to convert Iter.t to OSeq.t
2019-10-05 22:2:9 (GMT)
In other words
2019-10-05 22:2:18 (GMT)
If I do take on Iter.t
2019-10-05 22:2:35 (GMT)
will the next call to something on the same iterator
2019-10-05 22:2:43 (GMT)
move over the taken elements?
2019-10-05 22:19:42 (GMT)
Hmm, the distinction between Iter.t and OSeq.t (really, the standard Seq.t) is quite deep.
I think in Zipperposition, Iter.t makes sense in a lot of places. It's a bit like a foreach loop, but composable, and n-ary unification relies heavily on it (as well as things like traversing each subterm of each term of each lit of each clause in a set, say).
Of course, for HO unification you do want OSeq.t and it can't be easily obtained from Iter.t (it's a deep control inversion problem, really. Rust designers have had the same questions when they made their Iterator type). When do you need to convert from Iter.t to OSeq.t?
2019-10-05 22:30:51 (GMT)
If (as I suspect) you want to wrap n-ary unification of literals in a lazy stream unification, I think it's simpler to actually force the whole thing into a list and use OSeq.of_list. You make literal (syntactic) unification eager but retain some higher-level lazyness.
2019-10-07 8:8:13 (GMT)
(deleted)
2019-10-07 8:15:12 (GMT)
Hmm, the distinction between
Iter.tandOSeq.t(really, the standardSeq.t) is quite deep.
I think in Zipperposition,Iter.tmakes sense in a lot of places. It's a bit like a foreach loop, but composable, and n-ary unification relies heavily on it (as well as things like traversing each subterm of each term of each lit of each clause in a set, say).
Of course, for HO unification you do wantOSeq.tand it can't be easily obtained fromIter.t(it's a deep control inversion problem, really. Rust designers have had the same questions when they made theirIteratortype). When do you need to convert fromIter.ttoOSeq.t?
I solved my problem by using OSeq.merge function and returning subsequences for each step of unification.
2019-10-07 8:16:10 (GMT)
But thanks anyway it is good to know what is easily doable and what is not.