Compile blocks

The compile keyword has two arguments:

  • A name of an expression to be compiled.
  • A set of compilation rules using the format (backend -> string) where the string is the text we inline.

This is an example:

$ cat tests/positive/HelloWorld
...
axiom Action : Type;
compile Action {
  c -> "int";
};
...

The following Juvix examples are NOT valid.

  • One can not repeat backend inside a compile block.
...
axiom Action : Type;
compile Action {
 c -> "int";
 c -> "int";  --
};
...
  • One name, one compile block, no more.
...
axiom Action : Type;
compile Action {
 c -> "int";
};
compile Action {
 c -> "int";
};
...
  • A compile block must be in the same module as their name definition.
$ cat A.mjuvix
...
axiom Action : Type;
...

$ cat B.mjuvix
...
compile Action {
 c -> "int";
};
...