Module Arg.Language

install target data_model specification

The toplevel function that is used to install the calling convention for the given target. The general syntax follows this structure,

describe t data @@ fun declare ->
let* arena1 = <arena-specification> in
let* arenaN = <arena-specification> in
let return ~alignment x = <statement> in
let arg ~alignment x = <statement> in
let finish = <finalization-procedure> in
let* () = <initialization-procedure> in
declare ~finish ~return arg

For example, the following specification describes ARM calling convention AAPCS32,

let define t =
  install t model @@ fun describe ->
  let* iargs = Arg.Arena.iargs t in
  let* irets = Arg.Arena.irets t in
  let rev = Theory.Endianness.(Theory.Target.endianness t = le) in
  let return ~alignment:_ size = select [
      C.Type.is_basic, select [
        is (size <= 32 * 2), Arg.registers ~rev  irets;
        otherwise, Arg.reference iargs;
      ];
      is (size <= 32), Arg.register irets;
      otherwise, Arg.reference iargs;
    ] in
  describe ~return @@ fun ~alignment _ ->
  sequence [
    is (alignment = 64), const (Arg.align_even iargs);
    always, choose [
      Arg.split_with_memory ~rev iargs;
      Arg.memory
    ];
  ]

sequence cmd executes a sequence of predicated statements.

Executes all commands in the specified order. A command's statement is executed if the commands predicate is evaluates to true. Otherwise the statement is skipped.

If an evaluated statement rejects a computation then the whole sequence will be rejected.

select t spec selects the first applicable option to pass t.

The form,

select [
  pred1, option1;
  pred2, option2;
  ...,...;
  predN, optionN;
]

Tries pred1 arg, pred2 arg, ..., predN arg in order until the first one that returns true and uses the corresponding option to pass the argument.

The computation is rejected if either the selected option rejects the computation or none options were selected.

case classifer commands case analysis.

The case combinator first classfies the argument using the classfier function, which shall return a polymoprhic variant, and then selects a command that matches the selected class.

Rejects the computation if there's no matching class.

any ps holds if any of ps holds.

all ps holds if all of ps hold.

neither ps holds if neither of ps hold.

is cnd holds if cnd holds.

Example,

[
  is (size > 64), memory;
  otherwise, registers;

]

otherwise is a predicate that is always true.

I.e., it is is true.

This predicate is supposed to be used with the select combinator as the last, catch-all, predicate, e.g.,

select arg [
  is_fundamental, pass_fundamental;
  is_floating, pass_floating;
  otherwise, pass_memory;
]

always is a predicate that is always true, i.e., is true.

never is a predicate that never holds, i.e., is false.

choose options tries options in order until the first on that is not rejected.

This combinator is like choice but is supposed to be used inside select, e.g.,

select arg [
  p1, choose [o1, o2];
  either [p2; p3], choose [o3,o4];
]

combine xs combines statements into a signle statement.

Evaluates statements in the order they are specified. If any of the statements rejects then the whole statement will be rejected.