Reimplement deep patterns using tries

[rolyp]

As per my "demand-indexed computation" experiment. Imported from rolyp/lambdacalc-old#4.

• Trie datatype, analogous to Constr:
  • Trie.Var maps any argument to a continuation, plus environment binding the variable
  • Trie.Prim (?) that demands a strict value of primitive type
• primitive operations
  • PrimOp should be an expression form?
  • prim ops as tries of ground type
  • delete Expr.OpName (consolidate with Expr.Var)
• Trie.Constr case via nested tries**
• new function application semantics, based on tries
• new match..as semantics, based on tries
• semantics on paper for demand-indexed self-explaining computation
• adapt above to work with environments rather than substitutions
• write-up:
  • minor corrections to self-explaining, demand-indexed
  • arbitrary ground types rather than just nat; unary primitives
  • drop de Bruijn indices in favour of explicit names
  • environment-based demand-indexed evaluation
  • compute output environment as part of the judgement?
  • define self-explaining as a function over a demand-indexed proof tree
  • delete self-explaining experiment? (its patterns won't be as nice as tries)
  • τ, υ to range over tries (υ for arbitrary tries, τ for non-empty ones)?
  • ρ, σ to range over environments?