Redex Features - racket/racket GitHub Wiki

Bigger projects:

• multi-hole evaluation contexts
  • being able to write up the pi-calculus in a natural way, with multi-hole contexts acting as congruence rules, could be a good goal here
  • This requires reworking the semantics for context matching
• cross-language metafunctions
  • example
    • direct extension of existing syntax -- just allow list of languages instead of a single language
    • qualify nonterminals in contract to resolve ambiguity, otherwise leave unqualified
    • would like to be able to define extended metafunctions that add another language
• matching on more than just sexprs: structs, sets, hashes
  • using this, incorporate some ideas from Jay's optimized Fedex system:
    • definition
    • use
    • uses structs to prevent duplicate checking of non-terminal matchedness, allows use to promise that there is only one deconstruction or one possible reduction
    • I've found this can give 100x speed improvements.
• "type-checking"-like thing for metafunctions: at the very least, every clause's pattern should have the same arity as the contract
  • even better: check that the clause's pattern is a refined version of the pattern from the contract (this may be hard)
  • "has some overlap with pattern contract" might be a more useful check
• test case simplification: given a predicate and a test case that fails to satisfy it; automatically shrink the test case to find a minimal example that still fails
  • good test case to aim for

Smaller projects:

• disable caching for individual metafunctions (but not the metafunctions they call)
  • note: this also requires that any metafunction that calls that metafunction also disables its caching
• 'traces' support for user-defined reduction relation applications (e.g. apply-reduction-relation*/random)
• coinductive judgement forms

Uncertain effort/scope:

• shortcut arrows that are actually useful
  • (There's already a macro hack by Ian for this; should be in redex-proper)
• general "debugging" friendliness
  • e.g. a "reasonable" means of introspecting the state of a reduction so that we don't have to e.g. put in nasty printing side-conditions
• figure out an Ott-like description for binding structure that can be added to a define-language and use that to automatically generate capture-avoiding substitution functions and alpha-equivalence predicates. Nominal logic should also be a good inspiration for this
• add some "drop the parens" support to typesetting. That is, let someone specify precedence declarations for productions in a grammar and then have the typesetting infrastructure drop parenthesis based on those declarations when rendering a term
• a distinction between introducing a new variable and matching on that variable: would prevent trying to bind to that variable twice.

Successes:

• don't-bind-don't-care construct https://github.com/plt/racket/pull/365
• 'traces' support for user-defined reduction relation applications https://github.com/plt/racket/pull/362