Remove the MonoJuvix intermediate language

[lukaszcz]

Monomorphisation seems unnecessary when compiling MicroJuvix to C. Polymorphic functions can be implemented in C by just casting fields and arguments of polymorphic types to an appropriate 'universal' type. For instance, assuming all objects handled by the C runtime are pointers into the heap, the translation of the program

inductive Nat {
   O : Nat;
   S : Nat -> Nat;
};

one : Nat;
one = ...
plus : Nat -> Nat -> Nat;
plus x y = ...

inductive Pair (A : Type) (B : Type) {
   fst : A;
   snd : B;
}; 

f : (A : Type) -> Pair Nat A -> Pair A Nat
f _ p = Pair (snd p) (plus (fst p) one)

would look something like

// the universal type
#define UT (void*)

#define TAG_NAT_O ...
#define TAG_NAT_S ...

typedef struct Nat{
   uint tag;
   struct Nat* S_arg;
} nat_t;

nat_t* one = ...;
nat_t* plus(nat_t* x, nat_t* y) { ... }

typedef struct Pair {
   UT fst, snd;
} pair_t;

pair_t* f(pair_t* p) {
   pair_t* r = malloc(sizeof(Pair));
   r->fst = p->snd;
   r->snd = (UT) plus((nat_t*)(p->fst), one);
   return r;
}

By changing UT, this method can be extended to handle unboxed values of "small" types which fit into the machine word (or several words). The only requirement on UT is that it needs to have enough bits to store pointers and all values of "small" types. This is a "standard" method, e.g., the OCaml compiler uses something similar (the OCaml compiler doesn't produce C code, but the general idea of datatype/function representation is similar).