Skip to content

Pragmas in Juvix

Pragmas in Juvix are used to provide additional information to the compiler about how to handle specific identifiers or modules. They offer a way to control the compilation process and can be associated with identifiers by placing a pragma comment just before the identifier declaration.

Syntax of Pragma

The syntax for binding a pragma to an identifier is as follows:

{-# pragma_name: pragma_value #-}
identifier : Type;

For instance, the subsequent code associates the inline pragma with a value of true to the identifier f.

{-# inline: true #-}
f : Nat -> Nat

Multiple pragmas can be linked with a single identifier, delineated by commas:

{-# inline: true, unroll: 100 #-}
g : Nat -> Nat

Pragmas associated with a module are inherited by all definitions within the module, unless explicitly overridden. For example,

  {-# inline: true #-}
  module M;
    f : Nat -> Nat := <body-f>;
    g : Nat -> Nat := <body-g>;

    {-# inline: false #-}
    h : Nat -> Nat := <body-h>;
  end;

In this scenario, inlining is enabled for f, g and disabled for h.

Pragmas are mappings in YAML syntax, albeit the outermost braces are not mandated for the top-level mapping if it's on a single line. If the compiler encounters any unrecognized pragmas, they will be disregarded to ensure backwards compatibility. Although pragmas influence the compilation process, they don't carry any semantic significance - eliminating all pragmas should not alter the meaning of the program.

Available Pragmas

Herein, we enumerate all currently recognized pragmas in Juvix. In the descriptions below, b symbolizes a boolean (true or false), and n symbolizes a non-negative number.

Inlining Functions

  • inline: b

This pragma specifies whether a function should be inlined. If set to true, the function will invariably be inlined when fully applied. If set to false, the function will never be inlined, which also disables automatic inlining.

Inlining Partial Applications

  • inline: n

This variant of the inline pragma specifies that a partial application of the function with at least n explicit arguments should always be inlined. For example:

{-# inline: 2 #-}
compose {A B C} (f : B -> C) (g : A -> B) (x : A) : C :=
  f (g x);

In the expression compose f g, the function compose will be inlined, but in compose f, it won't be.

Unrolling Recursion

  • unroll: n

This pragma sets the maximum recursion unrolling depth to n. It only affects the vampir and geb backends.

Naming Function Arguments for Generated Code

  • argnames: [arg1, .., argn]

This pragma sets the names of function arguments in the generated output to arg1,..,argn. This is primarily useful with the vampir backend to name VampIR input variables.

Formatting

  • format: b

This pragma enables or disables formatting for the specified module. Adding the format: false pragma before a module makes the formatter ignore the module and output it verbatim.

Specializing Functions

  • Allows specialization on a per-trait or per-instance basis.