In the current setup, a task which depends on another task with multiple results is executed on each of these results and might produce multiple results as well.

There are cases where you want to restrict the results of a task by applying another task to it. Here is an example:

  • Task 1 calculates the type of an overloaded operator. The task has two results FunTy(IntTy(), IntTy()) and FunTy(FloatTy(), FloatTy()).
  • Task 2 rewrites task 1 to the first subterm. It has two results, IntTy() and FloatTy().
  • Task 3 rewrites task 1 to the second subterm. It has two results, IntTy() and FloatTy().
  • Task 4 calculated the type of a subexpression. It has a single result IntTy().
  • Task 5 matches task 2 with task 4. It succeeds on the first result of task 2, and fails on the second result. Thus, it has a single result IntTy().

The expression should have type IntTy(). However, there is no way to express this currently. Conceptually, task 3 has the result, but it should give only the first result, since task 5 only works on the first result of task 1.

In resolution tasks, this filtering is hardcoded into the task execution. A conceptual solution to this on task level would supersede this.

Submitted by Guido Wachsmuth on 10 December 2013 at 18:14

On 10 December 2013 at 22:00 Vlad Vergu commented:

I don’t entirely understand the example in the description.

I’ve also repeatedly run into the lack of a filter task. I’ve implemented a where task ( but it does not work for filtering over lists.

Let’s try to formalise this a bit. What we want is to have a task:

Filter: Result * Check -> Instruction

Its naive task creation factory will look like this:

task-create-filter(check|ctx) = ?result; <new-task(|ctx)> Filter(result, <check> result)

The evaluation:

perform-task(|n) = ?Filter(<id>, [_|_])

Where check and task-create-filter are Result -> Result. This will work fine if the source Result will get replaced by a single element. If however the source Result is in fact a list of terms then the task <check> result will succeed if it succeeds for at least one of these terms.

Would this maybe work:

	    Zip: Result * Result -> Instruction
	    Where: Result -> Instruction
	    (result1, result2) -> <new-task(|ctx)> Zip(result1, result2)
	  task-is-combinator = ?Zip(_, _)
	    Zip(r1, r2) -> <zip(id)> (r1, r2)
	    result -> <new-task(|ctx)> Where(result-and-status)
	      check-choice := <task-create-choice(|ctx)> [<check> result, TASKFAILURE()];
	      result-and-status := <new-task(|ctx)> Zip(result, check-choice)
	    Where((r1, status)) -> r1
	      <not(?TASKFAILURE())> status

The question is whether the check-choice will be single result or multiple results. That and whether it’s allowed to have a non-result (i.e. actual term) in the alternative of the choice.

Log in to post comments