Mast_to_mir (mlang.Mlang.Mast_to

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

val translate_expression : 
  Mir.cat_variable_data Mir.CatVarMap.t ->
  Mir.idmap ->
  translating_context ->
  Mast.expression Pos.marked ->
  Mir.expression Pos.marked

Main translation function for expressions

val get_conds : 
  Mir.verif_domain Mast.DomainIdMap.t ->
  Mir.cat_variable_data Mir.CatVarMap.t ->
  Mir.Error.t list ->
  Mir.idmap ->
  Mast.program ->
  Mir.condition_data Mir.RuleMap.t

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.