Redex Features

Erik Silkensen edited this page Jun 8, 2013 · 17 revisions

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
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:
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.