Create Imp, a C-Like DSL

[enricozb]

Implement a C-like imperative DSL with u64 words, expressions (add, mul, etc.), statements and control flow (block, if, while). An Imp program is akin to a thread, and it has access to two external shared u64 arrays: local and global. It has the basic atomic operations, including atomic_exchange. Include an interpreter for IMP terms, a parser, a stringifier, and a compiler to C.

• [ ] Add types and notation
• [ ] Add an IMP program stringifier
• [ ] An IMP evaluator / interpreter
• [ ] IMP -> C transpiler

[enricozb]

PR (Add types and notation): https://github.com/HigherOrderCO/monobook/pull/36

[VictorTaelin]

Note that my current Imp type is AI-generated, do not assume it is one I particularly like. It has some weird stuff so feel free to reason about the problem follow the approach that works for you. I'm not used to creating imperative DSLs so I'm not strongly opinionated, but the way that makes sense to me is for Program to be a "procedure" (i.e., block of statements) which can have assignments, branching, loops; like a fragment of wasm instructions. I don't think we should implement the concept of functions on Imp at all. Instead, we can just use Agda functions. I think we should have 3 versions of Set/Get: one for registers, other for shared memory, and other for global memory (RSet/RGet, SSet/SGet, GSet/GGet). We should also have atomic functions for shared memory and global memory. We should also create a Monad to help us construct Programs with the do notation. Also, I think we should have only one integer type, u64. But take all of that as just inspiration. What matters the most is that we can have a procedural DSL which we can compile to C/CUDA/LLVM/etc.