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.

[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]

:+1: @YaZko

[YaZko]

Hey, I'm wondering how we want to organize the new material. We have:

• Some extremely general stuff in sum.v that should clearly migrate to the library;
• Some very Asmspecific stuff: the syntax and denotation of blocks that lives in Asm.v;
• Some things clearly specific to the compiler, in Imp2Asm.v at the moment. But then things get a bit less clear in my mind. Imp2AsmBis.v, that should be renamed, strives to be a generic theory of linking. So it should morally be a functor parameterized by a type block and a function denote_b and some good properties on this denotation. However, both this theory and Asm's semantics depend on definitions like den and all its combinators, while we would like to define them independently from one another. So I guess the conclusion is that we should pull out another theory which is essentially the diagrammatic one that @Lysxia wrote this morning. If so, how should we name this entity?

[gmalecha]

This looks great.

[Lysxia]

What is going on with CI?

• Fails to build Basics_Functions, but I can't reproduce.

• The build of paco reports lots of warnings about hints being implicitly added to core, but I can't seem to trigger the warning even intentionally. Those warnings do not appear on paco's CI. https://travis-ci.org/snu-sf/paco

[Lysxia]

Travis is not building coq 8.8 and 8.9 but the master branch of coq on github in both cases...

[gmalecha]

This is a huge PR!

[gmalecha]

Is the plan to hold this until the deadline?

[Lysxia]

that sounds like a good plan!