# [racket-dev] Redex for abstract machines / analysis prototypes

Machine semantics for real machines (like the JVM or Racket's VM) or non-standard semantics for an abstract interpretation (like what I end up getting into) can get up to monstrous numbers of components for each state that usually don't matter. I and I'm sure many others would appreciate a reduction relation language that is a little more like UIUC's K.
Here is a concrete suggestion of what I imagine (some support for patterns on hashes):
1) Add a pattern (hash (literal pat) ...) to match hashes up to the specified keys (hashes with more keys are still accepted).
2) Add rewrite rules for changing the current state.
-- (next-state (r r) ...)
-- (get r r)
-- (set r r r)
-- (set* r (r r) ...)
Where
(get r_0 r_1) is ,(hash-ref (term r_0) (term r_1) 'something-that-never-matches)
(set r_0 r_1 r_2) is ,(hash-set (term r_0) (term r_1) (term r_2))
(set* r_0 (r_k r_v) ...) is the obvious extension of set, but is annoying to write.
And assuming the LHS is named state,
(next-state (r_k r_v) ...) is (set* state (r_k r_v) ...)
Not-the-best-example-since-it's-so-minimal:
(define-language CEK
[e x (e e) lam]
[lam (lambda (x) e)]
[rho (hash)]
[kont mt (ar e rho kont) (fn e rho kont))])
(define R
(machine-step CEK
[--> (hash (C x) (E rho))
(next-state (C lam) (E rho*))
(where (lam rho*) (get rho x))]
[--> (hash (C (e_0 e_1)) (E rho) (K kont))
(next-state (C e_0) (K (ar e_1 rho kont)))]
[--> (hash (C lam) (E rho) (K (ar e rho_0 kont)))
(next-state (C e) (E rho_0) (K (fn lam rho kont)))]
[--> (hash (C v) (K (fn (lambda (x) e) rho kont)))
(next-state (C e) (E (set rho x (v rho))) (K kont))]))
(define (inject e) (term (set* #hash() (C ,e) (E #hash()) (K mt))))
Is this reasonably simple to add to Redex? It would be a very welcome addition.
-Ian