Module Mlang.Mast_to_mir

Mast to Mir translation of M programs.

Translation context

General translation context

type translating_context = {
table_definition : bool;(*

true if translating an expression susceptible to contain a generic table index

idmap : Mir.idmap;(*

Current string-to-Mir.Variable.t mapping


Translation helpers

val get_var_from_name : Mir.idmap -> string Pos.marked -> Mir.Variable.t

Queries a type: Mir.variable.t from an type:idmap mapping, the name of a variable and the rule number from which the variable is requested. Returns the variable with the same name and highest rule number that is below the current rule number from where this variable is requested

Main translation function for expressions

Returns a map whose keys are dummy variables and whose values are the verification conditions.

Main translation function

val translate : Mast.program -> Mir.program

Main translation function from the M AST to the M Variable Graph. This function performs 6 linear passes on the input code:

  • get_constants gets the value of all constant variables, the values of which are needed to compute certain loop bounds;
  • get_variables_decl retrieves the declarations of all other variables and errors;
  • get_var_redefinitions incorporates into idmap all definitions inside rules along with their execution number;
  • get_var_data is the workhorse pass that translates all the expressions corresponding to the definitions;
  • add_dummy_definition_for_variable_declaration adds Undefined definitions placeholder for all variables declarations;
  • get_errors_conds parses the verification conditions definitions.