Compiler from Imp to Asm

[gmalecha]

Yannick and I wrote this compiler together. Yannick is working on cleaning up some of the definitions and we'll verify it. There are a few things left to do:

1. Write a compiler for expressions (this means that we need to come up with a scheme for defining temporaries.
2. Unifying the effects that the two languages use (e.g. Imp has errors, assembly doesn't, assembly has a heap, Imp doesn't).
3. Verify the compiler.

Some possible extensions:

1. I think we could use the same compiler structure to add other control flow, e.g. break, continue, etc.
2. Track local variables explicitly (similar to the way that LLVM works, though personally I would opt for continuations rather than phi nodes).

This isn't ready to merge yet

[YaZko]

1. I quickly drafted a very naïve scheme by simply assuming a reserved prefix "local". I think it should do the trick but I'll have to double check.

2. I removed errors from Imp. They were only used in the C-like evaluator assuming partial maps for the environment. I kept the Imp-like total maps for simplicity. If you feel that it's an oversimplification, we can roll back.
   I kept the heap for now, although the compiler currently allocate everything in the stack. Do we want to be fancier?

3. I cannot express the theorem right now, I need to parameterize the denotation of Imp rather than fix its effects as is right now.

N.B. : TODO: switch the domain of value from Nat to Z to be able to write factorial and odd/even.

[gmalecha]

1. I quickly drafted a very naïve scheme by simply assuming a reserved prefix "local". I think it should do the trick but I'll have to double check.

This should be fine.

2. I removed errors from Imp. They were only used in the C-like evaluator assuming partial maps for the environment. I kept the Imp-like total maps for simplicity. If you feel that it's an oversimplification, we can roll back.

Partial maps might be better in both cases but we can have the effect actually raise the error so that errors don't show up in the implementation.

I kept the heap for now, although the compiler currently allocate everything in the stack. Do we want to be fancier?

Either way. Dropping it or keeping it, as long as it is consistent shouldn't matter. Ultimately, it would be nice to have a language with a heap.

3. I cannot express the theorem right now, I need to parameterize the denotation of Imp rather than fix its effects as is right now.

The other option is to give an effect transformer from ImpEff into a parameterized effect. For example,

Definition to_param {E} {Estate : StateE ~> E} {... } : ImpEff ~> E :=
   fun _ e => match e with ... end.

N.B. : TODO: switch the domain of value from Nat to Z to be able to write factorial and odd/even.

[gmalecha]

ExtLib has a Show instance for nat.

[gmalecha]

I was actually wondering if we should take this as the primitive representation of asm programs.

[gmalecha]

All the re-associating in this definition has me wondering if we should define some new variant types for LocalOrImport and such.

[gmalecha]

The downside of this representation is that we can't really do anything interesting with it except for denote it since we can't inspect the c_label type. After we finish this, it might be better to switch labels to nat and make c_blocks be a finite map. This would allow us to implement transformations such as jump-tunneling, block merging, etc.

[gmalecha]

@Zdancewic personally, I like this way to write it better. It also has the benefit that type class resolution doesn't loop forever.

[YaZko]

Note that switching the representation of programs in Asm to the old definition of CR required to split their denotation in two, first to denote the program and then the main itself, since the latter is now a block and no longer a label.

[gmalecha]

Is the plan to hold this until the deadline?

[Lysxia]

that sounds like a good plan!