Hi, I am new to racket and use redex to implement an operational semantics of a minimal programming language. It has some complicated expressions and I am not sure how I could test the evaluation contexts of redex for them in a proper way?! Are the reduction-relation conntected to the evaluation contexts?

<https://github.com/lschuetze/plt-redex-fej/blob/master/src/fej.rkt#L47-L54> is the evaluation context and <https://github.com/lschuetze/plt-redex-fej/blob/master/src/fej-semantics.rkt#L39-L42> is where I want to apply it to a lkp(which is tested in <https://github.com/lschuetze/plt-redex-fej/blob/master/src/fej-semantics-test.rkt#L41-L43>).

I’m not exactly sure what your question is. Do your tests pass? Do they require evaluation context to be working properly in order to reduce?

The reduction-semantics uses a metafunction. Tests for the metafunction are passed. The test for the reduction-semantics returns got nothing. I am not sure how the reduction-semantics and evaluation contexts are related and how they complement each other.

It looks like you defined your reduction relation using in-hole and your evaluation contexts, which is how they should relate.

This is a very simple example, which uses reduction-relation and evaluation contexts: https://github.com/racket/redex/blob/master/redex-examples/redex/examples/arithmetic.rkt

Okay, that is how I already understood the relation between both. I think my problem is that in my calculus the new syntax is quite complicated due to call-by-value and mixins. Thus, it does have multiple seq’s of expressions/values for class instantiation and mixin class instantiation (i.e., (new E (new A ⊕ ) (new B ⊕) ⊕ ((new F ⊕ ) Z (new A ⊕ ) (new B ⊕))))for a type E+(F.Z)). This makes me wonder how I would define the evaluation context for that new expression.

The syntax itself does not seem so utterly complicated. e::= new C e ... ⊕ r ...) where (r ::= (v R v ...))and (v ::= (new C v ... ⊕ r ...)) .

Then the usual context for that would be something like: (new C v ... E e ... ⊕ r ...)

provided you want to evaluate those left to right

Yes, it should be left-to-right. I actually try to check/implement a paper here from someone else. r is defined as (r ::= (v R v ...))which mixes expressions and values.

I think that needs to be replaced by an expression and the value part is just used in v. And r also gets a evaluation context on its own. I disliked that mix from the beginning but wanted to stick with the paper as long as possible.

Otherwise, how should redex know how to handle the rpart in that expression?

I changed e to e ::= (new C e ... ⊕ (e R e ...) ...) and v to (v ::= (new C v ... ⊕ (v R v ...) ...)) but now it complains

> reduction-relation: in-hole’s first argument is expected to match exactly one hole, but it may match a hole many different ways ; in: ((in-hole E (lkp (new C v_0 … ⊕ (v_1 R v_2 …) …) f_i)) CT) Its midnight here now. I’ll stop for today. Redex is awesome but it really takes its time to get used to it :wink: