Skip to content

Expand failure tracking in NonDet #261

@michaelpj

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

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