In looking at OCaml-generated x86 assembly last week, I noticed that having a language which keeps undefined identifiers in symbolic form can be handy. I started making notes in a Mathematica notebook to keep track of some heap shuffling code I was trying to understand. To explain the technique, let's use this OCaml snippet:
where the floating-point arithmetic becomes this x86 code:
((1.0 -. alpha) *. (Array.get y i))
In Mathematica, I translated lines of assembly into real assignments, using the literal register names for my variable names, except at the very beginning of the assembly fragement. For example, when starting the above fragment, eax points to the alpha value, so I would write the read reference to eax as alpha, without defining alpha. Similarly esi points to Array.get y i, so I was able to write this sequence:
fsub REAL8 PTR [eax]
fmul REAL8 PTR [esi]
It was interesting, a little startling actually, to see the original expression re-emerge by simulating running the code. I didn't get very far into it, but you can also do things like simulate writes to memory with a register transfer definition:
In a traditional language, eax has to be bound to a value. But in a symbolic language, eax can be a symbolic expression like _caml_young_ptr + 4.
Mem[eax] = 2301
Do my partial-evaluation readers have any remarks about this?