Skip to content

Expand failure tracking in NonDet #261

Description

@michaelpj

NonDets ability to track where you hit empty is quite nice, and helps with a classic problem of non-deterministic searches: knowing why you failed to find a solution.

However, the current approach only gives you call stacks. It would be nice in many cases to give a human-readable message or error.

I'm not really sure what the right design here is. The current version requires altering the calls to empty, which is a bit awkward and requires writing custom versions of Alternative functions. I wonder if we could do something like:

  • Add extra failure context to Empty.
  • empty sets empty failure context
  • Users can use interpose to add failure context to any failures within a lexical scope

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions